Index (mcp 1.0 API)

A B C D E F G H I L M N O P R S T U V W Z _
All Classes and Interfaces|All Packages|Constant Field Values|Serialized Form

A

add(BDDInteger) - Method in class org.batfish.MutableBDDInteger
addClipping(BDDInteger) - Method in class org.batfish.MutableBDDInteger
addLabel(String, LabelType, Label) - Method in class org.mcp.core.MCPLabels: Adds a domain variable to this class.
addVar(String, LabelType, Object) - Method in class org.mcp.core.MCPLabels: Adds a domain variable to the system.
allDifferences(BDDInteger) - Method in class org.batfish.MutableBDDInteger: 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.
and(BDD) - Method in class org.batfish.MutableBDDInteger
and(MCPBitVector) - Method in class org.mcp.core.MCPBitVector: Performs a logical AND with another MCPBitVector.
andWith(MCPBitVector) - Method in class org.mcp.core.MCPBitVector: Performs an in-place logical AND with another MCPBitVector (modifies this instance for SAT).
ANY - Static variable in class org.batfish.datamodel.IpWildcard
asLong() - Method in class org.batfish.datamodel.Ip
AUTO - Static variable in class org.batfish.datamodel.Ip
AUTOMATON - Enum constant in enum class org.mcp.variables.dynamics.OperableLabelType
AutomatonOperableLabel - Class in org.mcp.variables.dynamics
AutomatonOperableLabel(Automaton) - Constructor for class org.mcp.variables.dynamics.AutomatonOperableLabel

B

BDD - Enum constant in enum class org.mcp.core.MCPFactory.MCPType
BDD - Enum constant in enum class org.mcp.variables.dynamics.OperableLabelType
BDDDomain<T> - Class in org.batfish: Class that wraps a BDDInteger around a finite collection of values and provides an API for dealing directly with the values.
BDDDomain(BDDFactory, List<T>, int) - Constructor for class org.batfish.BDDDomain
BDDDomain(BDD, BDDDomain<T>) - Constructor for class org.batfish.BDDDomain
BDDDomain(BDDDomain<T>) - Constructor for class org.batfish.BDDDomain
bddFactory(int) - Static method in class org.batfish.BDDUtils: Create a new BDDFactory object with numVariables boolean variables.
BDDInteger - Class in org.batfish
BDDInteger(BDDFactory, BDD[]) - Constructor for class org.batfish.BDDInteger
BddOperableLabel - Class in org.mcp.variables.dynamics
BddOperableLabel(BDD) - Constructor for class org.mcp.variables.dynamics.BddOperableLabel
BDDUtils - Class in org.batfish: Various utility methods for working with BDDs.
BDDUtils() - Constructor for class org.batfish.BDDUtils
biimp(MCPBitVector) - Method in class org.mcp.core.MCPBitVector: Performs logical bi-implication (equivalence) with another MCPBitVector.
bitvector(BDDFactory, int, int, boolean) - Static method in class org.batfish.BDDUtils
bitvector(FormulaFactory, int, int, boolean) - Static method in class org.mcp.sat.SATUtils: Creates a bit vector of SAT variables.

C

clone() - Method in class org.mcp.variables.dynamics.OperableLabel
compareTo(Ip) - Method in class org.batfish.datamodel.Ip
compareTo(IpWildcard) - Method in class org.batfish.datamodel.IpWildcard
compareTo(Prefix) - Method in class org.batfish.datamodel.Prefix
computeLabels() - Method in class org.mcp.core.MCPLabels: Computes the ECs for each domain and updates the relevant maps.
concatBitvectors(BDD[]...) - Static method in class org.batfish.BDDUtils
concatBitvectors(Variable[]...) - Static method in class org.mcp.sat.SATUtils: Concatenates multiple bit vectors into a single array.
containsIp(Ip) - Method in class org.batfish.datamodel.IpWildcard
containsIp(Ip) - Method in class org.batfish.datamodel.Prefix
containsPrefix(Prefix) - Method in class org.batfish.datamodel.Prefix
convert() - Method in class org.mcp.variables.statics.IntegerSetLabel
convert() - Method in class org.mcp.variables.statics.IntegerSetSetLabel
convert() - Method in class org.mcp.variables.statics.Label
convert() - Method in class org.mcp.variables.statics.PrefixLabel
convert() - Method in class org.mcp.variables.statics.PrefixSetLabel
convert() - Method in class org.mcp.variables.statics.RangeLabel
convert() - Method in class org.mcp.variables.statics.RangeSetLabel
convert() - Method in class org.mcp.variables.statics.RegexpSetLabel
copy() - Method in class org.mcp.core.MCPBitVector: Returns a deep copy of this MCPBitVector.
copy() - Method in class org.mcp.core.MCPOperableLabel: Returns a copy of this MCPOperableLabel.
create(long) - Static method in class org.batfish.datamodel.Ip
create(Ip) - Static method in class org.batfish.datamodel.IpWildcard
create(Ip, int) - Static method in class org.batfish.datamodel.Prefix
create(Ip, Ip) - Static method in class org.batfish.datamodel.Prefix
create(Prefix) - Static method in class org.batfish.datamodel.IpWildcard
createSolver(FormulaFactory) - Static method in class org.mcp.sat.SATUtils: Creates a new SAT solver instance for the given formula factory.
createVar(OperableLabelType, Object) - Static method in class org.mcp.variables.dynamics.OperableLabelFactory
createVar(LabelType, Object) - Static method in class org.mcp.variables.statics.LabelFactory

D

diff(MCPBitVector) - Method in class org.mcp.core.MCPBitVector: Computes the difference (this AND NOT other) with another MCPBitVector.
diffWith(MCPBitVector) - Method in class org.mcp.core.MCPBitVector: Computes the in-place difference (this AND NOT other) with another MCPBitVector (modifies this instance for SAT).
dot(BDD) - Method in class org.mcp.core.MCPFactory: Converts a BDD to the Graphviz DOT format for visualization.

E

ECEngine - Class in org.mcp.core: A utility class for computing Equivalence Classes (ECs) from a set of labels.
ECEngine(Set<Label>, Label) - Constructor for class org.mcp.core.ECEngine: Constructs ECs for the given set of labels.
equals(Object) - Method in class org.batfish.BDDDomain
equals(Object) - Method in class org.batfish.datamodel.Ip
equals(Object) - Method in class org.batfish.datamodel.IpWildcard
equals(Object) - Method in class org.batfish.datamodel.Prefix
equals(Object) - Method in class org.batfish.MutableBDDInteger
equals(Object) - Method in class org.mcp.core.MCPBitVector: Checks equality with another object.
equals(Object) - Method in class org.mcp.core.MCPOperableLabel: Checks equality with another object.
equals(Object) - Method in class org.mcp.sat.MutableSATInteger: Checks equality with another object.
equals(Object) - Method in class org.mcp.sat.SATDomain: Checks equality with another object.
equals(Object) - Method in class org.mcp.variables.dynamics.AutomatonOperableLabel
equals(Object) - Method in class org.mcp.variables.dynamics.BddOperableLabel
equals(Object) - Method in class org.mcp.variables.dynamics.MutableSetOperableLabel
equals(Object) - Method in class org.mcp.variables.dynamics.OperableLabel
equals(Object) - Method in class org.mcp.variables.statics.IntegerSetLabel
equals(Object) - Method in class org.mcp.variables.statics.IntegerSetSetLabel
equals(Object) - Method in class org.mcp.variables.statics.Label
equals(Object) - Method in class org.mcp.variables.statics.PrefixLabel
equals(Object) - Method in class org.mcp.variables.statics.PrefixSetLabel
equals(Object) - Method in class org.mcp.variables.statics.RangeLabel
equals(Object) - Method in class org.mcp.variables.statics.RangeSetLabel
equals(Object) - Method in class org.mcp.variables.statics.RegexpSetLabel

F

FIRST_CLASS_A_PRIVATE_IP - Static variable in class org.batfish.datamodel.Ip
FIRST_CLASS_B_PRIVATE_IP - Static variable in class org.batfish.datamodel.Ip
FIRST_CLASS_C_PRIVATE_IP - Static variable in class org.batfish.datamodel.Ip
FIRST_CLASS_E_EXPERIMENTAL_IP - Static variable in class org.batfish.datamodel.Ip
FIRST_MULTICAST_IP - Static variable in class org.batfish.datamodel.Ip
firstBitsEqual(long, int) - Method in class org.batfish.BDDInteger
firstBitsEqual(long, int) - Method in class org.batfish.MutableBDDInteger: Check if the first length bits match the BDDInteger representing the advertisement prefix.
firstBitsEqual(long, int) - Method in class org.mcp.sat.MutableSATInteger: Returns a formula representing the first length bits equal to the given value.
firstBitsEqual(long, int) - Method in class org.mcp.sat.SATInteger: Returns a formula representing the first length bits equal to the given value.
free() - Method in class org.batfish.MutableBDDInteger: Free all the component BDDs in this BDDInteger.

G

geq(long) - Method in class org.batfish.BDDInteger
getAllVariable(int, int) - Static method in class org.mcp.variables.statics.IntegerSetLabel
getAssignment(FormulaFactory, Formula, Variable[]) - Static method in class org.mcp.sat.SATUtils: Returns a satisfying assignment for the given formula and bit vector.
getBddFactory() - Method in class org.mcp.variables.dynamics.BddOperableLabel
getBddInteger() - Method in class org.mcp.variables.statics.PrefixLabel
getBDDResult(BDD) - Method in class org.mcp.core.MCPFactory: Returns a single satisfying assignment from a BDD as a map of domain names to integer values.
getBDDResults(BDD) - Method in class org.mcp.core.MCPFactory: Returns all possible satisfying assignments from a given BDD.
getBitAtPosition(long, int) - Static method in class org.batfish.datamodel.Ip: Return the boolean value of a bit at the given position.
getBitAtPosition(Ip, int) - Static method in class org.batfish.datamodel.Ip: See Ip.getBitAtPosition(long, int).
getBitvec() - Method in class org.mcp.sat.SATInteger: Returns the bit vector.
getClassMask() - Method in class org.batfish.datamodel.Ip
getClassNetworkSize() - Method in class org.batfish.datamodel.Ip: Returns the size of an IPv4 network in IPv4 Address Class of this Ip.
getDomainChildrenNodes(String) - Method in class org.mcp.core.MCPLabels: Gets the domain children nodes for a given domain.
getDomainNames() - Method in class org.mcp.core.MCPLabels
getECAutomata() - Method in class org.mcp.core.ECEngine: Returns a mapping from EC indices to their semantic representations.
getECs() - Method in class org.mcp.core.ECEngine: Returns a mapping from each label to the set of EC indices it covers.
getECs(String) - Method in class org.mcp.core.MCPLabels: Retrieves the set of ECs for a given domain.
getEndIp() - Method in class org.batfish.datamodel.Prefix
getFactory() - Method in class org.batfish.BDDInteger
getFactory() - Method in class org.mcp.core.MCPBitVector: Returns the factory (BDDFactory or FormulaFactory) associated with this bit vector.
getFactory() - Method in class org.mcp.core.MCPOperableLabel: Returns the factory (BDDFactory or FormulaFactory) associated with this label.
getFactory() - Method in class org.mcp.sat.SATInteger: Returns the formula factory.
getFalse() - Method in class org.mcp.core.MCPFactory: Returns a bit vector representing logical false for the current backend type.
getFirstHostIp() - Method in class org.batfish.datamodel.Prefix
getInteger() - Method in class org.batfish.BDDDomain
getInteger() - Method in class org.mcp.sat.SATDomain: Returns the underlying MutableSATInteger.
getIp() - Method in class org.batfish.datamodel.IpWildcard
getIsValidConstraint() - Method in class org.batfish.BDDDomain: Returns the constraint that represents any value within the domain.
getLabel(String, Label) - Method in class org.mcp.core.MCPFactory: Returns a bit vector representing the given label in the specified domain.
getLabelClass() - Method in enum class org.mcp.variables.statics.LabelType
getLabelECs(String, Label) - Method in class org.mcp.core.MCPLabels: Retrieves the set of ECs for a specific static variable within a given domain.
getLabelFillOtherDomain(String, Label) - Method in class org.mcp.core.MCPFactory: Returns a bit vector for the given label in one domain, and true in all other domains.
getLastHostIp() - Method in class org.batfish.datamodel.Prefix: Returns the last ip in the prefix that is not a broadcast address.
getMask() - Method in class org.batfish.datamodel.IpWildcard
getNetworkAddress(int) - Method in class org.batfish.datamodel.Ip
getNumBits() - Method in class org.mcp.core.MCPFactory: Returns the total number of bits used in the BDD or SAT representation.
getNumECs() - Method in class org.mcp.core.ECEngine: Returns the number of computed ECs.
getOne() - Method in class org.mcp.core.MCPFactory: Returns a bit vector representing logical one (true) for the current backend type.
getOperableLabelClass() - Method in enum class org.mcp.variables.dynamics.OperableLabelType
getPrefixLength() - Method in class org.batfish.datamodel.Prefix
getPrefixWildcard() - Method in class org.batfish.datamodel.Prefix
getSatFactory() - Method in class org.mcp.core.MCPFactory: Returns the SAT FormulaFactory if the backend type is SAT.
getStartIp() - Method in class org.batfish.datamodel.Prefix
getTrue() - Method in class org.mcp.core.MCPFactory: Returns a bit vector representing logical true for all domains.
getType() - Method in class org.mcp.core.MCPBitVector: Returns the backend type of this bit vector.
getValue() - Method in class org.mcp.core.MCPBitVector: Returns the underlying value (BDD or Formula) of this bit vector.
getValue() - Method in class org.mcp.core.MCPOperableLabel: Returns the underlying symbolic value.
getValue() - Method in class org.mcp.variables.dynamics.AutomatonOperableLabel
getValue() - Method in class org.mcp.variables.dynamics.BddOperableLabel
getValue() - Method in class org.mcp.variables.dynamics.MutableSetOperableLabel
getValue() - Method in class org.mcp.variables.dynamics.OperableLabel
getValue() - Method in class org.mcp.variables.statics.IntegerSetLabel
getValue() - Method in class org.mcp.variables.statics.IntegerSetSetLabel
getValue() - Method in class org.mcp.variables.statics.Label
getValue() - Method in class org.mcp.variables.statics.PrefixLabel
getValue() - Method in class org.mcp.variables.statics.PrefixSetLabel
getValue() - Method in class org.mcp.variables.statics.RangeLabel
getValue() - Method in class org.mcp.variables.statics.RangeSetLabel
getValue() - Method in class org.mcp.variables.statics.RegexpSetLabel
getValueClass() - Method in enum class org.mcp.variables.dynamics.OperableLabelType
getValueClass() - Method in enum class org.mcp.variables.statics.LabelType
getValueSatisfying(BDD) - Method in class org.batfish.BDDInteger: Find a representative value of the represented integer that satisfies a given constraint.
getValueSatisfying(BDD) - Method in class org.batfish.MutableBDDInteger
getValueSatisfying(Formula) - Method in class org.mcp.sat.SATInteger: Returns the value satisfying the given formula, or 0 if unsatisfiable.
getValueSatisfyingToInt(Formula) - Method in class org.mcp.sat.SATInteger: Converts a SAT assignment to an int value.
getValuesSatisfying(BDD, int) - Method in class org.batfish.BDDInteger: Return a list of values satisfying the input BDD, up to some maximum number.
getValuesSatisfying(Formula, int) - Method in class org.mcp.sat.SATInteger: Returns a list of values satisfying the input formula, up to a maximum number.
getVar(String, Object) - Method in class org.mcp.core.MCPFactory: Returns a bit vector representing the given value in the specified domain.
getVarECs(String, Object) - Method in class org.mcp.core.MCPLabels: Retrieves the set of ECs for a specific variable within a given domain.
getVarFillOtherDomain(String, Object) - Method in class org.mcp.core.MCPFactory: Returns a bit vector for the given value in one domain, and true in all other domains.
getWildcardMask() - Method in class org.batfish.datamodel.IpWildcard
getWildcardMaskAsIp() - Method in class org.batfish.datamodel.IpWildcard

H

hashCode() - Method in class org.batfish.BDDDomain
hashCode() - Method in class org.batfish.datamodel.Ip
hashCode() - Method in class org.batfish.datamodel.IpWildcard
hashCode() - Method in class org.batfish.datamodel.Prefix
hashCode() - Method in class org.batfish.MutableBDDInteger
hashCode() - Method in class org.mcp.core.MCPBitVector: Returns the hash code for this bit vector.
hashCode() - Method in class org.mcp.core.MCPOperableLabel: Returns the hash code for this label.
hashCode() - Method in class org.mcp.sat.MutableSATInteger: Returns the hash code for this MutableSATInteger.
hashCode() - Method in class org.mcp.sat.SATDomain: Returns the hash code for this SATDomain.
hashCode() - Method in class org.mcp.variables.dynamics.AutomatonOperableLabel
hashCode() - Method in class org.mcp.variables.dynamics.BddOperableLabel
hashCode() - Method in class org.mcp.variables.dynamics.MutableSetOperableLabel
hashCode() - Method in class org.mcp.variables.dynamics.OperableLabel
hashCode() - Method in class org.mcp.variables.statics.IntegerSetLabel
hashCode() - Method in class org.mcp.variables.statics.IntegerSetSetLabel
hashCode() - Method in class org.mcp.variables.statics.Label
hashCode() - Method in class org.mcp.variables.statics.PrefixLabel
hashCode() - Method in class org.mcp.variables.statics.PrefixSetLabel
hashCode() - Method in class org.mcp.variables.statics.RangeLabel
hashCode() - Method in class org.mcp.variables.statics.RangeSetLabel
hashCode() - Method in class org.mcp.variables.statics.RegexpSetLabel
HOST_SUBNET_MAX_PREFIX_LENGTH - Static variable in class org.batfish.datamodel.Prefix: /32s are loopback interfaces -- no hosts are connected.

I

id() - Method in class org.mcp.core.MCPBitVector: Returns a copy of this bit vector (for BDD, returns a new reference).
imp(MCPBitVector) - Method in class org.mcp.core.MCPBitVector: Performs logical implication (this => other).
impWith(MCPBitVector) - Method in class org.mcp.core.MCPBitVector: Performs in-place logical implication (this => other) (modifies this instance for SAT).
INTEGER_SET - Enum constant in enum class org.mcp.variables.dynamics.OperableLabelType
INTEGER_SET - Enum constant in enum class org.mcp.variables.statics.LabelType
INTEGER_SET_SET - Enum constant in enum class org.mcp.variables.statics.LabelType
IntegerSetLabel - Class in org.mcp.variables.statics
IntegerSetLabel(Sets.SetView<Integer>) - Constructor for class org.mcp.variables.statics.IntegerSetLabel
IntegerSetSetLabel - Class in org.mcp.variables.statics
IntegerSetSetLabel(Set<Sets.SetView<Integer>>) - Constructor for class org.mcp.variables.statics.IntegerSetSetLabel
inter(OperableLabel) - Method in class org.mcp.core.MCPOperableLabel: Returns the intersection of this label and another.
inter(OperableLabel) - Method in class org.mcp.variables.dynamics.AutomatonOperableLabel
inter(OperableLabel) - Method in class org.mcp.variables.dynamics.BddOperableLabel
inter(OperableLabel) - Method in class org.mcp.variables.dynamics.MutableSetOperableLabel
inter(OperableLabel) - Method in class org.mcp.variables.dynamics.OperableLabel
intersects(IpWildcard) - Method in class org.batfish.datamodel.IpWildcard
inverted() - Method in class org.batfish.datamodel.Ip
Ip - Class in org.batfish.datamodel: An IPv4 address
IpWildcard - Class in org.batfish.datamodel: An IP wildcard consisting of a IP address and a wildcard (also expressed as an IP address)
ipWithWildcardMask(Ip, long) - Static method in class org.batfish.datamodel.IpWildcard: Return an IpWildcard from the given IP address and wildcardMask.
ipWithWildcardMask(Ip, Ip) - Static method in class org.batfish.datamodel.IpWildcard: Return an IpWildcard from the given IP address and wildcardMask.
isBDD() - Method in class org.mcp.core.MCPBitVector: Checks if this bit vector uses the BDD backend.
isContain(String, Label, Label) - Method in class org.mcp.core.MCPLabels: Checks if one static variable contains another within a given domain.
isContradiction(Object) - Method in class org.mcp.core.MCPFactory: Checks if the given value is a contradiction (always false).
isEmpty() - Method in class org.mcp.core.MCPOperableLabel: Checks if this label represents the empty set.
isEmpty() - Method in class org.mcp.variables.dynamics.AutomatonOperableLabel
isEmpty() - Method in class org.mcp.variables.dynamics.BddOperableLabel
isEmpty() - Method in class org.mcp.variables.dynamics.MutableSetOperableLabel
isEmpty() - Method in class org.mcp.variables.dynamics.OperableLabel
isOne() - Method in class org.mcp.core.MCPBitVector: Checks if this bit vector represents logical true (tautology).
isPrefix() - Method in class org.batfish.datamodel.IpWildcard
isSAT() - Method in class org.mcp.core.MCPBitVector: Checks if this bit vector uses the SAT backend.
isSatisfying(Object) - Method in class org.mcp.core.MCPFactory: Checks if the given value is satisfiable.
isSatisfying(FormulaFactory, Formula) - Static method in class org.mcp.sat.SATUtils: Checks if the given formula is satisfiable.
isTautology(Object) - Method in class org.mcp.core.MCPFactory: Checks if the given value is a tautology (always true).
isZero() - Method in class org.mcp.core.MCPBitVector: Checks if this bit vector represents logical false (contradiction).
ite(BDD, MutableBDDInteger) - Method in class org.batfish.MutableBDDInteger

L

Label - Class in org.mcp.variables.statics
Label() - Constructor for class org.mcp.variables.statics.Label
LabelFactory - Class in org.mcp.variables.statics
LabelFactory() - Constructor for class org.mcp.variables.statics.LabelFactory
LabelType - Enum Class in org.mcp.variables.statics
leq(long) - Method in class org.batfish.BDDInteger
longestCommonPrefix(Prefix, Prefix) - Static method in class org.batfish.datamodel.Prefix: Return the longest prefix that contains both input prefixes.

M

makeFromIndex(BDDFactory, int, int, boolean) - Static method in class org.batfish.MutableBDDInteger: Create an integer, and initialize its values as "don't care" This requires knowing the start index variables the bitvector will use.
makeFromIndex(FormulaFactory, int, int, boolean) - Static method in class org.mcp.sat.MutableSATInteger: Creates a MutableSATInteger from a bitvector index.
makeFromValue(BDDFactory, int, long) - Static method in class org.batfish.MutableBDDInteger: Create an integer and initialize it to a concrete value
MAX - Static variable in class org.batfish.datamodel.Ip
MAX_PREFIX_LENGTH - Static variable in class org.batfish.datamodel.Prefix: Maximum prefix length (number of bits) for a IPv4 address, which is 32
MCPBitVector - Class in org.mcp.core: Represents a symbolic bit vector for sets of constraints, supporting both BDD and SAT backends.
MCPBitVector(Object, MCPFactory.MCPType) - Constructor for class org.mcp.core.MCPBitVector: Constructs a new MCPBitVector with the given value and backend type.
MCPBitVector(MCPBitVector) - Constructor for class org.mcp.core.MCPBitVector: Copy constructor.
MCPFactory - Class in org.mcp.core: The MCPFactory class extends MCPLabels and manages symbolic representations of sets of constraints.
MCPFactory() - Constructor for class org.mcp.core.MCPFactory: Constructs a new MCPFactory instance with BDD as the default backend.
MCPFactory(MCPFactory) - Constructor for class org.mcp.core.MCPFactory: Constructs a new MCPFactory instance by copying the state from another MCPFactory.
MCPFactory(MCPFactory.MCPType) - Constructor for class org.mcp.core.MCPFactory: Constructs a new MCPFactory instance with the specified backend type.
MCPFactory.MCPType - Enum Class in org.mcp.core
MCPLabels - Class in org.mcp.core: The MCPLabels class represents a collection of equivalence classes (ECs) across multiple domains.
MCPLabels() - Constructor for class org.mcp.core.MCPLabels: Constructs an MCPLabels object.
MCPOperableLabel - Class in org.mcp.core: MCPOperableLabel wraps an MCPBitVector and provides set operations (union, intersection, difference) for use in dynamic symbolic computations.
MCPOperableLabel(MCPBitVector) - Constructor for class org.mcp.core.MCPOperableLabel: Constructs a new MCPOperableLabel with the given symbolic value.
MCPOperableLabel(MCPOperableLabel) - Constructor for class org.mcp.core.MCPOperableLabel: Copy constructor.
minus(OperableLabel) - Method in class org.mcp.core.MCPOperableLabel: Returns the difference of this label and another (this \ other).
minus(OperableLabel) - Method in class org.mcp.variables.dynamics.AutomatonOperableLabel
minus(OperableLabel) - Method in class org.mcp.variables.dynamics.BddOperableLabel
minus(OperableLabel) - Method in class org.mcp.variables.dynamics.MutableSetOperableLabel
minus(OperableLabel) - Method in class org.mcp.variables.dynamics.OperableLabel
MULTICAST - Static variable in class org.batfish.datamodel.Prefix: Multicast IPs are in "244.0.0.0/4".
MutableBDDInteger - Class in org.batfish
MutableBDDInteger(BDDFactory, int) - Constructor for class org.batfish.MutableBDDInteger
MutableBDDInteger(BDDFactory, BDD[]) - Constructor for class org.batfish.MutableBDDInteger
MutableBDDInteger(MutableBDDInteger) - Constructor for class org.batfish.MutableBDDInteger
MutableSATInteger - Class in org.mcp.sat: MutableSATInteger represents a mutable bit-vector for SAT-based integer encoding.
MutableSATInteger(FormulaFactory, int) - Constructor for class org.mcp.sat.MutableSATInteger: Constructs a MutableSATInteger with the given length, initializing all bits as free variables.
MutableSATInteger(FormulaFactory, Variable[]) - Constructor for class org.mcp.sat.MutableSATInteger: Constructs a MutableSATInteger from a bit vector.
MutableSATInteger(MutableSATInteger) - Constructor for class org.mcp.sat.MutableSATInteger: Copy constructor.
MutableSetOperableLabel - Class in org.mcp.variables.dynamics
MutableSetOperableLabel(Sets.SetView<Integer>) - Constructor for class org.mcp.variables.dynamics.MutableSetOperableLabel

N

not() - Method in class org.mcp.core.MCPBitVector: Performs logical NOT on this bit vector.
numBits(int) - Static method in class org.batfish.BDDDomain: Returns the number of bits used to represent a domain of the given size.
numBits(int) - Static method in class org.mcp.sat.SATDomain: Returns the number of bits used to represent a domain of the given size.
numSubnetBits() - Method in class org.batfish.datamodel.Ip
numSubnetBitsToSubnetMask(int) - Static method in class org.batfish.datamodel.Ip

O

OperableLabel - Class in org.mcp.variables.dynamics
OperableLabel() - Constructor for class org.mcp.variables.dynamics.OperableLabel
OperableLabelFactory - Class in org.mcp.variables.dynamics
OperableLabelFactory() - Constructor for class org.mcp.variables.dynamics.OperableLabelFactory
OperableLabelType - Enum Class in org.mcp.variables.dynamics
or(MCPBitVector) - Method in class org.mcp.core.MCPBitVector: Performs a logical OR with another MCPBitVector.
org.batfish - package org.batfish: BDD-based symbolic primitives adapted for MCP network-policy reasoning.
org.batfish.datamodel - package org.batfish.datamodel: Lightweight IPv4 data model types used by symbolic encodings.
org.mcp.core - package org.mcp.core: Core abstractions for the MCP symbolic engine.
org.mcp.sat - package org.mcp.sat: SAT backend support for MCP symbolic domains and bit-vector encodings.
org.mcp.utils - package org.mcp.utils: General utility helpers for MCP modules.
org.mcp.variables - package org.mcp.variables: Type system for MCP symbolic variables.
org.mcp.variables.dynamics - package org.mcp.variables.dynamics
org.mcp.variables.statics - package org.mcp.variables.statics

P

parse(String) - Static method in class org.batfish.datamodel.Ip
parse(String) - Static method in class org.batfish.datamodel.IpWildcard
parse(String) - Static method in class org.batfish.datamodel.Prefix: Parse a Prefix from a string.
Prefix - Class in org.batfish.datamodel: An IPv4 Prefix
PREFIX - Enum constant in enum class org.mcp.variables.statics.LabelType
PREFIX_SET - Enum constant in enum class org.mcp.variables.statics.LabelType
PrefixLabel - Class in org.mcp.variables.statics
PrefixLabel(Prefix) - Constructor for class org.mcp.variables.statics.PrefixLabel
PrefixSetLabel - Class in org.mcp.variables.statics
PrefixSetLabel(Set<Prefix>) - Constructor for class org.mcp.variables.statics.PrefixSetLabel
Printer - Class in org.mcp.utils: Utility class for writing strings to files.
Printer() - Constructor for class org.mcp.utils.Printer

R

range(long, long) - Method in class org.batfish.BDDInteger
RANGE - Enum constant in enum class org.mcp.variables.statics.LabelType
RANGE_SET - Enum constant in enum class org.mcp.variables.dynamics.OperableLabelType
RANGE_SET - Enum constant in enum class org.mcp.variables.statics.LabelType
RangeLabel - Class in org.mcp.variables.statics
RangeLabel(Range<Integer>) - Constructor for class org.mcp.variables.statics.RangeLabel
RangeSetLabel - Class in org.mcp.variables.statics
RangeSetLabel(Set<Range<Integer>>) - Constructor for class org.mcp.variables.statics.RangeSetLabel
REGEXP - Enum constant in enum class org.mcp.variables.statics.LabelType
REGEXP_SET - Enum constant in enum class org.mcp.variables.statics.LabelType
RegexpSetLabel - Class in org.mcp.variables.statics
RegexpSetLabel(Set<String>) - Constructor for class org.mcp.variables.statics.RegexpSetLabel

S

SAT - Enum constant in enum class org.mcp.core.MCPFactory.MCPType
satAssignmentToInt(BDD) - Method in class org.batfish.BDDInteger
satAssignmentToLong(BDD) - Method in class org.batfish.BDDInteger
satAssignmentToLong(BDD) - Method in class org.batfish.MutableBDDInteger
satAssignmentToLong(Assignment) - Method in class org.mcp.sat.MutableSATInteger: Converts a SAT assignment to a long value.
satAssignmentToLong(Assignment) - Method in class org.mcp.sat.SATInteger: Converts a SAT assignment to a long value.
satAssignmentToValue(BDD) - Method in class org.batfish.BDDDomain
satAssignmentToValue(Formula) - Method in class org.mcp.sat.SATDomain: Decodes a SAT assignment to the corresponding value in the domain.
satCount() - Method in class org.mcp.core.MCPBitVector: Returns the number of satisfying assignments for this bit vector.
SATDomain<T> - Class in org.mcp.sat: SATDomain wraps a SATInteger around a finite collection of values and provides an API for working directly with those values in SAT-based symbolic computations.
SATDomain(FormulaFactory, List<T>, int) - Constructor for class org.mcp.sat.SATDomain: Constructs a SATDomain from a formula factory, value list, and bit index offset.
SATDomain(SATDomain<T>) - Constructor for class org.mcp.sat.SATDomain: Copy constructor.
SATInteger - Class in org.mcp.sat: Abstract base class for SAT-based integer encodings.
SATInteger(FormulaFactory, Variable[]) - Constructor for class org.mcp.sat.SATInteger: Constructs a SATInteger from a formula factory and bit vector.
SATUtils - Class in org.mcp.sat: Utility methods for SAT-based symbolic computations.
SATUtils() - Constructor for class org.mcp.sat.SATUtils
setBddFactory(BDDFactory) - Method in class org.mcp.variables.dynamics.BddOperableLabel
setBddFactory(BDDFactory) - Method in class org.mcp.variables.statics.PrefixLabel
setBddFactory(BDDFactory) - Method in class org.mcp.variables.statics.PrefixSetLabel
setFactory(Object) - Method in class org.mcp.core.MCPBitVector: Sets the factory (BDDFactory or FormulaFactory) for this bit vector.
setFactory(Object) - Method in class org.mcp.core.MCPOperableLabel: Sets the factory (BDDFactory or FormulaFactory) for this label.
setInteger(MutableBDDInteger) - Method in class org.batfish.BDDDomain
setInteger(MutableSATInteger) - Method in class org.mcp.sat.SATDomain: Sets the underlying MutableSATInteger.
setValue(long) - Method in class org.batfish.MutableBDDInteger: Set this BDD to have an exact value
setValue(MutableBDDInteger) - Method in class org.batfish.MutableBDDInteger
setValue(T) - Method in class org.batfish.BDDDomain
size() - Method in class org.batfish.BDDInteger: Returns the number of bits in this BDDInteger.
size() - Method in class org.mcp.sat.SATInteger: Returns the number of bits in this SATInteger.
strict(String) - Static method in class org.batfish.datamodel.Prefix: Parse a Prefix from a string.
sub(BDDInteger) - Method in class org.batfish.MutableBDDInteger
subClipping(BDDInteger) - Method in class org.batfish.MutableBDDInteger
subsetOf(IpWildcard) - Method in class org.batfish.datamodel.IpWildcard
supersetOf(IpWildcard) - Method in class org.batfish.datamodel.IpWildcard
support() - Method in class org.batfish.BDDDomain: Produces a BDD that represents the support (i.e., the set of BDD variables) of this domain.
support() - Method in class org.batfish.MutableBDDInteger: Produces a BDD that represents the support (i.e., the set of BDD variables) of this BDD integer.
swapPairing(BDD[], BDD[]) - Static method in class org.batfish.BDDUtils: Create a BDDPairing for swapping variables.
swapPairing(BDDFactory, Set<BDDVarPair>) - Static method in class org.batfish.BDDUtils: Create a BDDPairing for swapping variables.

T

toBDD(Ip) - Method in class org.batfish.BDDInteger: Build a constraint that matches the input Ip.
toBDD(IpWildcard) - Method in class org.batfish.BDDInteger: Build a constraint that matches the IPs matched by the input IpWildcard.
toBDD(IpWildcard) - Method in class org.batfish.MutableBDDInteger
toBDD(Prefix) - Method in class org.batfish.BDDInteger: Build a constraint that matches the set of IPs contained by the input Prefix.
toPrefix() - Method in class org.batfish.datamodel.Ip
toPrefix() - Method in class org.batfish.datamodel.IpWildcard
toString() - Method in class org.batfish.datamodel.Ip
toString() - Method in class org.batfish.datamodel.IpWildcard
toString() - Method in class org.batfish.datamodel.Prefix
toString() - Method in class org.mcp.core.MCPBitVector: Returns a string representation of this bit vector.
toString() - Method in class org.mcp.core.MCPOperableLabel: Returns a string representation of this label.
toString() - Method in class org.mcp.variables.dynamics.AutomatonOperableLabel
toString() - Method in class org.mcp.variables.dynamics.BddOperableLabel
toString() - Method in class org.mcp.variables.dynamics.MutableSetOperableLabel
toString() - Method in class org.mcp.variables.dynamics.OperableLabel
tryParse(String) - Static method in class org.batfish.datamodel.Ip: Return an Optional Ip from a string, or Optional.empty() if the string does not represent an Ip.
tryParse(String) - Static method in class org.batfish.datamodel.Prefix: Return an Optional Prefix from a string, or Optional.empty() if the string does not represent a Prefix.

U

union(Set<String>) - Static method in class org.mcp.variables.statics.RegexpSetLabel
union(OperableLabel) - Method in class org.mcp.core.MCPOperableLabel: Returns the union of this label and another.
union(OperableLabel) - Method in class org.mcp.variables.dynamics.AutomatonOperableLabel
union(OperableLabel) - Method in class org.mcp.variables.dynamics.BddOperableLabel
union(OperableLabel) - Method in class org.mcp.variables.dynamics.MutableSetOperableLabel
union(OperableLabel) - Method in class org.mcp.variables.dynamics.OperableLabel
updates() - Method in class org.mcp.core.MCPFactory: Updates the internal state of the MCPFactory.

V

valid() - Method in class org.batfish.datamodel.Ip
value(long) - Method in class org.batfish.BDDInteger
value(long) - Method in class org.mcp.sat.SATInteger: Returns a formula representing the exact value.
value(T) - Method in class org.batfish.BDDDomain
value(T) - Method in class org.mcp.sat.SATDomain: Returns a formula representing the assignment of the given value.
valueOf(String) - Static method in enum class org.mcp.core.MCPFactory.MCPType: Returns the enum constant of this class with the specified name.
valueOf(String) - Static method in enum class org.mcp.variables.dynamics.OperableLabelType: Returns the enum constant of this class with the specified name.
valueOf(String) - Static method in enum class org.mcp.variables.statics.LabelType: Returns the enum constant of this class with the specified name.
values() - Static method in enum class org.mcp.core.MCPFactory.MCPType: Returns an array containing the constants of this enum class, in the order they are declared.
values() - Static method in enum class org.mcp.variables.dynamics.OperableLabelType: Returns an array containing the constants of this enum class, in the order they are declared.
values() - Static method in enum class org.mcp.variables.statics.LabelType: Returns an array containing the constants of this enum class, in the order they are declared.

W

withFactory(Object) - Method in class org.mcp.core.MCPBitVector: Returns a new MCPBitVector with the same value and the given factory set.
writeStringToFile(String, String) - Static method in class org.mcp.utils.Printer: Writes the given string content to the specified file path.

Z

ZERO - Static variable in class org.batfish.datamodel.Ip
ZERO - Static variable in class org.batfish.datamodel.Prefix: A "0.0.0.0/0" prefix

_

_bitvec - Variable in class org.batfish.BDDInteger
_bitvec - Variable in class org.mcp.sat.SATInteger: Bit vector representing the integer (each bit is a SAT variable).
_domainNames - Variable in class org.mcp.core.MCPLabels: Domain name to variable type.
_domainToBDDFactory - Variable in class org.mcp.core.MCPLabels: Domain name to BDDFactory (for BDD dynamic domains).
_domainToECs - Variable in class org.mcp.core.MCPLabels: Domain name to set of EC indices.
_domainToLabels - Variable in class org.mcp.core.MCPLabels: Domain name to set of static variables.
_domainToLabelToECs - Variable in class org.mcp.core.MCPLabels: Domain name to mapping from static variable to its EC indices.
_domainToObjectToLabel - Variable in class org.mcp.core.MCPLabels: Domain name to mapping from object to static variable.
_domainToStandardECs - Variable in class org.mcp.core.MCPLabels: Domain name to EC engine.
_domainToTrueVariable - Variable in class org.mcp.core.MCPLabels: Domain name to the "true" static variable.
_factory - Variable in class org.batfish.BDDInteger
_factory - Variable in class org.mcp.sat.SATInteger: Formula factory for creating SAT formulas.
_maxVal - Variable in class org.batfish.BDDInteger
_maxVal - Variable in class org.mcp.sat.SATInteger: Maximum value representable by this SATInteger.

A B C D E F G H I L M N O P R S T U V W Z _
All Classes and Interfaces|All Packages|Constant Field Values|Serialized Form