Package org.batfish

Class MutableBDDInteger

java.lang.Object

org.batfish.BDDInteger

org.batfish.MutableBDDInteger

All Implemented Interfaces:

Serializable

public final class MutableBDDInteger
extends BDDInteger

See Also:

• Serialized Form

Field Summary

Fields inherited from class org.batfish.BDDInteger

_bitvec, _factory, _maxVal

Constructor Summary

Constructors

Constructor	Description
MutableBDDInteger(net.sf.javabdd.BDDFactory factory, int length)
MutableBDDInteger(net.sf.javabdd.BDDFactory factory, net.sf.javabdd.BDD[] bitvec)
MutableBDDInteger(MutableBDDInteger other)

Method Summary

Modifier and Type	Method	Description
MutableBDDInteger	add(BDDInteger other)
MutableBDDInteger	addClipping(BDDInteger other)
net.sf.javabdd.BDD	allDifferences(BDDInteger other)	Produces a BDD whose models represent all possible differences between the two BDDIntegers -- valuations of the BDD variables that cause the two BDDIntegers to have different values.
MutableBDDInteger	and(net.sf.javabdd.BDD pred)
boolean	equals(Object o)
protected net.sf.javabdd.BDD	firstBitsEqual(long value, int length)	Check if the first length bits match the BDDInteger representing the advertisement prefix.
void	free()	Free all the component BDDs in this BDDInteger.
Optional<Long>	getValueSatisfying(net.sf.javabdd.BDD bdd)	Find a representative value of the represented integer that satisfies a given constraint.
int	hashCode()
MutableBDDInteger	ite(net.sf.javabdd.BDD b, MutableBDDInteger other)
static MutableBDDInteger	makeFromIndex(net.sf.javabdd.BDDFactory factory, int length, int start, boolean reverse)	Create an integer, and initialize its values as "don't care" This requires knowing the start index variables the bitvector will use.
static MutableBDDInteger	makeFromValue(net.sf.javabdd.BDDFactory factory, int length, long value)	Create an integer and initialize it to a concrete value
long	satAssignmentToLong(net.sf.javabdd.BDD satAssignment)
void	setValue(long val)	Set this BDD to have an exact value
void	setValue(MutableBDDInteger other)
MutableBDDInteger	sub(BDDInteger other)
MutableBDDInteger	subClipping(BDDInteger other)
net.sf.javabdd.BDD	support()	Produces a BDD that represents the support (i.e., the set of BDD variables) of this BDD integer.
net.sf.javabdd.BDD	toBDD(IpWildcard ipWildcard)	Build a constraint that matches the IPs matched by the input IpWildcard.

Methods inherited from class org.batfish.BDDInteger

geq, getFactory, getValuesSatisfying, leq, range, satAssignmentToInt, size, toBDD, toBDD, value

Methods inherited from class java.lang.Object

clone, finalize, getClass, notify, notifyAll, toString, wait, wait, wait

Constructor Details

MutableBDDInteger

public MutableBDDInteger(net.sf.javabdd.BDDFactory factory,
 net.sf.javabdd.BDD[] bitvec)

MutableBDDInteger

public MutableBDDInteger(net.sf.javabdd.BDDFactory factory,
 int length)

MutableBDDInteger

public MutableBDDInteger(MutableBDDInteger other)

Method Details

makeFromIndex

public static MutableBDDInteger makeFromIndex(net.sf.javabdd.BDDFactory factory,
 int length,
 int start,
 boolean reverse)

Create an integer, and initialize its values as "don't care" This requires knowing the start index variables the bitvector will use.

makeFromValue

public static MutableBDDInteger makeFromValue(net.sf.javabdd.BDDFactory factory,
 int length,
 long value)

Create an integer and initialize it to a concrete value

setValue

public void setValue(long val)

Set this BDD to have an exact value

getValueSatisfying

public Optional<Long> getValueSatisfying(net.sf.javabdd.BDD bdd)

Description copied from class: BDDInteger

Find a representative value of the represented integer that satisfies a given constraint.

Specified by:

getValueSatisfying in class BDDInteger

satAssignmentToLong

public long satAssignmentToLong(net.sf.javabdd.BDD satAssignment)

Specified by:

satAssignmentToLong in class BDDInteger

firstBitsEqual

protected net.sf.javabdd.BDD firstBitsEqual(long value,
 int length)

Check if the first length bits match the BDDInteger representing the advertisement prefix.

Specified by:

firstBitsEqual in class BDDInteger

toBDD

public net.sf.javabdd.BDD toBDD(IpWildcard ipWildcard)

Description copied from class: BDDInteger

Build a constraint that matches the IPs matched by the input IpWildcard.

Specified by:

toBDD in class BDDInteger

add

public MutableBDDInteger add(BDDInteger other)

addClipping

public MutableBDDInteger addClipping(BDDInteger other)

free

public void free()

Free all the component BDDs in this BDDInteger. This instance is no longer safe to use unless re-initialized via, e.g., setValue(long).

ite

public MutableBDDInteger ite(net.sf.javabdd.BDD b,
 MutableBDDInteger other)

and

public MutableBDDInteger and(net.sf.javabdd.BDD pred)

Parameters:

pred - a predicate

Returns:

the same bitvector but restricted by pred.

allDifferences

public net.sf.javabdd.BDD allDifferences(BDDInteger other)

Produces a BDD whose models represent all possible differences between the two BDDIntegers -- valuations of the BDD variables that cause the two BDDIntegers to have different values. The two BDDIntegers are assumed to have the same length.

Parameters:

other - the second BDDInteger

Returns:

a predicate represented as a BDD

support

public net.sf.javabdd.BDD support()

Produces a BDD that represents the support (i.e., the set of BDD variables) of this BDD integer.

setValue

public void setValue(MutableBDDInteger other)

sub

public MutableBDDInteger sub(BDDInteger other)

subClipping

public MutableBDDInteger subClipping(BDDInteger other)

equals

public boolean equals(Object o)

Overrides:

equals in class Object

hashCode

public int hashCode()

Overrides:

hashCode in class Object