Package org.batfish

Class BDDInteger

java.lang.Object
org.batfish.BDDInteger
All Implemented Interfaces:
Serializable
Direct Known Subclasses:
MutableBDDInteger
public abstract class BDDInteger extends Object implements Serializable
See Also:

  • Field Summary

    Fields
    Modifier and Type
    Field
    Description
    protected final net.sf.javabdd.BDD[]
    _bitvec
     
    protected final net.sf.javabdd.BDDFactory
    _factory
     
    protected final long
    _maxVal
     

  • Constructor Summary

    Constructors
    Modifier
    Constructor
    Description
    protected
    BDDInteger(net.sf.javabdd.BDDFactory factory, net.sf.javabdd.BDD[] bitvec)
     

  • Method Summary

    Modifier and Type
    Method
    Description
    protected abstract net.sf.javabdd.BDD
    firstBitsEqual(long val, int length)
     
    net.sf.javabdd.BDD
    geq(long val)
     
    net.sf.javabdd.BDDFactory
    getFactory()
     
    abstract Optional<Long>
    getValueSatisfying(net.sf.javabdd.BDD bdd)
    Find a representative value of the represented integer that satisfies a given constraint.
    List<Long>
    getValuesSatisfying(net.sf.javabdd.BDD bdd, int max)
    Return a list of values satisfying the input BDD, up to some maximum number.
    net.sf.javabdd.BDD
    leq(long val)
     
    net.sf.javabdd.BDD
    range(long a, long b)
     
    int
    satAssignmentToInt(net.sf.javabdd.BDD bdd)
     
    abstract long
    satAssignmentToLong(net.sf.javabdd.BDD satAssignment)
     
    int
    size()
    Returns the number of bits in this BDDInteger.
    final net.sf.javabdd.BDD
    toBDD(Ip ip)
    Build a constraint that matches the input Ip.
    abstract net.sf.javabdd.BDD
    toBDD(IpWildcard ipWildcard)
    Build a constraint that matches the IPs matched by the input IpWildcard.
    final net.sf.javabdd.BDD
    toBDD(Prefix prefix)
    Build a constraint that matches the set of IPs contained by the input Prefix.
    final net.sf.javabdd.BDD
    value(long val)
     

    Methods inherited from class java.lang.Object

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

  • Field Details

    • _factory

      protected final net.sf.javabdd.BDDFactory _factory

    • _bitvec

      protected final net.sf.javabdd.BDD[] _bitvec

    • _maxVal

      protected final long _maxVal

  • Constructor Details

    • BDDInteger

      protected BDDInteger(net.sf.javabdd.BDDFactory factory, net.sf.javabdd.BDD[] bitvec)

  • Method Details

    • size

      public int size()
      Returns the number of bits in this BDDInteger.

    • getValueSatisfying

      public abstract Optional<Long> getValueSatisfying(net.sf.javabdd.BDD bdd)
      Find a representative value of the represented integer that satisfies a given constraint.

    • satAssignmentToLong

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

    • satAssignmentToInt

      public int satAssignmentToInt(net.sf.javabdd.BDD bdd)

    • getValuesSatisfying

      public List<Long> getValuesSatisfying(net.sf.javabdd.BDD bdd, int max)
      Return a list of values satisfying the input BDD, up to some maximum number.
      Parameters:
      bdd - A constraint on this.
      max - The maximum number of values desired.
      Returns:
      The satisfying values.

    • toBDD

      public final net.sf.javabdd.BDD toBDD(Prefix prefix)
      Build a constraint that matches the set of IPs contained by the input Prefix.

    • toBDD

      public final net.sf.javabdd.BDD toBDD(Ip ip)
      Build a constraint that matches the input Ip.

    • firstBitsEqual

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

    • toBDD

      public abstract net.sf.javabdd.BDD toBDD(IpWildcard ipWildcard)
      Build a constraint that matches the IPs matched by the input IpWildcard.

    • value

      public final net.sf.javabdd.BDD value(long val)

    • leq

      public net.sf.javabdd.BDD leq(long val)

    • geq

      public net.sf.javabdd.BDD geq(long val)

    • range

      public net.sf.javabdd.BDD range(long a, long b)

    • getFactory

      public net.sf.javabdd.BDDFactory getFactory()