Module com.github.javabdd
Package com.github.javabdd

Class BDDFactory

java.lang.Object
com.github.javabdd.BDDFactory
Direct Known Subclasses:
BDDFactoryIntImpl
public abstract class BDDFactory extends Object
Interface for the creation and manipulation of BDDs.
See Also:

  • Field Details

    • and

      public static final BDDFactory.BDDOp and
      Logical 'and'.

    • xor

      public static final BDDFactory.BDDOp xor
      Logical 'xor'.

    • or

      public static final BDDFactory.BDDOp or
      Logical 'or'.

    • nand

      public static final BDDFactory.BDDOp nand
      Logical 'nand'.

    • nor

      public static final BDDFactory.BDDOp nor
      Logical 'nor'.

    • imp

      public static final BDDFactory.BDDOp imp
      Logical 'implication'.

    • biimp

      public static final BDDFactory.BDDOp biimp
      Logical 'bi-implication'.

    • diff

      public static final BDDFactory.BDDOp diff
      Set difference.

    • less

      public static final BDDFactory.BDDOp less
      Less than.

    • invimp

      public static final BDDFactory.BDDOp invimp
      Inverse implication.

    • tokenizer

      protected StringTokenizer tokenizer
      Used for tokenization during loading.

    • REORDER_NONE

      public static final BDDFactory.ReorderMethod REORDER_NONE
      No reordering.

    • REORDER_WIN2

      public static final BDDFactory.ReorderMethod REORDER_WIN2
      Reordering using a sliding window of 2.

    • REORDER_WIN2ITE

      public static final BDDFactory.ReorderMethod REORDER_WIN2ITE
      Reordering using a sliding window of 2, iterating until no further progress.

    • REORDER_WIN3

      public static final BDDFactory.ReorderMethod REORDER_WIN3
      Reordering using a sliding window of 3.

    • REORDER_WIN3ITE

      public static final BDDFactory.ReorderMethod REORDER_WIN3ITE
      Reordering using a sliding window of 3, iterating until no further progress.

    • REORDER_SIFT

      public static final BDDFactory.ReorderMethod REORDER_SIFT
      Reordering where each block is moved through all possible positions. The best of these is then used as the new position. Potentially a very slow but good method.

    • REORDER_SIFTITE

      public static final BDDFactory.ReorderMethod REORDER_SIFTITE
      Same as REORDER_SIFT, but the process is repeated until no further progress is done. Can be extremely slow.

    • REORDER_RANDOM

      public static final BDDFactory.ReorderMethod REORDER_RANDOM
      Selects a random position for each variable. Mostly used for debugging purposes.

    • gcstats

      protected BDDFactory.GCStats gcstats
      Singleton object for GC statistics.

    • reorderstats

      protected BDDFactory.ReorderStats reorderstats
      Singleton object for reorder statistics.

    • cachestats

      protected BDDFactory.CacheStats cachestats
      Singleton object for operator cache statistics.

    • maxusedbddnodesstats

      protected BDDFactory.MaxUsedBddNodesStats maxusedbddnodesstats
      Singleton object for maximum used BDD nodes statistics.

    • maxmemorystats

      protected BDDFactory.MaxMemoryStats maxmemorystats
      Singleton object for maximum memory usage statistics.

    • domain

      protected BDDDomain[] domain

    • fdvarnum

      protected int fdvarnum

    • firstbddvar

      protected int firstbddvar

    • gcCallbacks

      protected List<BDDFactory.GCStatsCallback> gcCallbacks
      The registered garbage collection statistics callbacks, or null if none registered.

    • reorderCallbacks

      protected List<BDDFactory.ReorderStatsCallback> reorderCallbacks
      The registered variable reorder statistics callbacks, or null if none registered.

    • resizeCallbacks

      protected List<BDDFactory.ResizeStatsCallback> resizeCallbacks
      The registered node table resize statistics callbacks, or null if none registered.

    • cacheCallbacks

      protected List<BDDFactory.CacheStatsCallback> cacheCallbacks
      The registered operator cache statistics callbacks, or null if none registered.

    • maxUsedBddNodesCallbacks

      protected List<BDDFactory.MaxUsedBddNodesStatsCallback> maxUsedBddNodesCallbacks
      The registered maximum BDD nodes usage statistics callbacks, or null if none registered.

    • maxMemoryCallbacks

      protected List<BDDFactory.MaxMemoryStatsCallback> maxMemoryCallbacks
      The registered maximum memory usage statistics callbacks, or null if none registered.

    • continuousCallbacks

      protected List<BDDFactory.ContinuousStatsCallback> continuousCallbacks
      The registered continuously BDD nodes usage and BDD operations statistics callbacks, or null if none registered.

  • Constructor Details

    • BDDFactory

      protected BDDFactory()
      Construct a new BDDFactory.

  • Method Details

    • getProperty

      public static final String getProperty(String key, String def)

    • init

      public static BDDFactory init(int nodenum, int cachesize)
      Initializes a BDD factory with the given initial node table size and operation cache size. Uses the "java" factory.
      Parameters:
      nodenum - initial node table size
      cachesize - operation cache size
      Returns:
      BDD factory object

    • init

      public static BDDFactory init(String bddpackage, int nodenum, int cachesize)
      Initializes a BDD factory of the given type with the given initial node table size and operation cache size. The type is a string that can be "j", "java", "test", "typed", or a name of a class that has an init() method that returns a BDDFactory. If it fails, it falls back to the "java" factory.
      Parameters:
      bddpackage - BDD package string identifier
      nodenum - initial node table size
      cachesize - operation cache size
      Returns:
      BDD factory object

    • isZDD

      public boolean isZDD()
      Returns true if this is a ZDD factory, false otherwise.
      Returns:
      true if this is a ZDD factory, false otherwise

    • zero

      public abstract BDD zero()
      Get the constant false BDD.

      Compare to bdd_false.

      Returns:
      constant false BDD

    • one

      public abstract BDD one()
      Get the constant true BDD.

      Compare to bdd_true.

      Returns:
      constant true BDD

    • universe

      public BDD universe()
      Get the constant universe BDD. (The universe BDD differs from the one BDD in ZDD mode.)

      Compare to bdd_true.

      Returns:
      constant universe BDD

    • emptySet

      public BDDVarSet emptySet()
      Get an empty BDDVarSet.

      Compare to bdd_true.

      Returns:
      empty BDDVarSet

    • buildCube

      public BDD buildCube(int value, List<BDD> variables)
      Build a cube from an array of variables.

      Compare to bdd_buildcube.

      Parameters:
      value - bitset
      variables - BDDs for variables
      Returns:
      cube

    • buildCube

      public BDD buildCube(int value, int[] variables)
      Build a cube from an array of variables.

      Compare to bdd_ibuildcube.

      Parameters:
      value - bitset
      variables - variables indices
      Returns:
      cube

    • makeSet

      public BDDVarSet makeSet(int[] varset)
      Builds a BDD variable set from an integer array. The integer array varset holds the variable numbers. The BDD variable set is represented by a conjunction of all the variables in their positive form.

      Compare to bdd_makeset.

      Parameters:
      varset - variable array
      Returns:
      BDD variable set

    • initialize

      protected abstract void initialize(int nodenum, int cachesize)
      Compare to bdd_init.
      Parameters:
      nodenum - the initial number of BDD nodes
      cachesize - the size of caches used by the BDD operators

    • isInitialized

      public abstract boolean isInitialized()
      Returns true if this BDD factory is initialized, false otherwise.

      Compare to bdd_isrunning.

      Returns:
      true if this BDD factory is initialized

    • reset

      public void reset()
      Reset the BDD factory to its initial state. Everything is reallocated from scratch. This is like calling done() followed by initialize().

    • done

      public abstract void done()
      This function frees all memory used by the BDD package and resets the package to its uninitialized state. The BDD package is no longer usable after this call.

      Compare to bdd_done.

    • setError

      public abstract void setError(int code)
      Sets the error condition. This will cause the BDD package to throw an exception at the next garbage collection.
      Parameters:
      code - the error code to set

    • clearError

      public abstract void clearError()
      Clears any outstanding error condition.

    • setMaxNodeNum

      public abstract int setMaxNodeNum(int size)
      Set the maximum available number of BDD nodes.

      Compare to bdd_setmaxnodenum.

      Parameters:
      size - maximum number of nodes
      Returns:
      old value

    • setMinFreeNodes

      public abstract double setMinFreeNodes(double x)
      Set minimum percentage of nodes to be reclaimed after a garbage collection. If this percentage is not reclaimed, the node table will be grown. The range of x is 0..1. The default is .20.

      Compare to bdd_setminfreenodes.

      Parameters:
      x - number from 0 to 1
      Returns:
      old value

    • setMaxIncrease

      public abstract int setMaxIncrease(int x)
      Set maximum number of nodes by which to increase node table after a garbage collection.

      Compare to bdd_setmaxincrease.

      Parameters:
      x - maximum number of nodes by which to increase node table
      Returns:
      old value

    • setIncreaseFactor

      public abstract double setIncreaseFactor(double x)
      Set factor by which to increase node table after a garbage collection. The amount of growth is still limited by setMaxIncrease().
      Parameters:
      x - factor by which to increase node table after GC
      Returns:
      old value

    • setCacheRatio

      public abstract double setCacheRatio(double x)
      Sets the cache ratio for the operator caches. When the node table grows, operator caches will also grow to maintain the ratio. A ratio of 0.5 leads to caches that are half the node table size, while a ratio of 2.0 leads to caches that are twice the node table size.

      Compare to bdd_setcacheratio.

      Parameters:
      x - cache ratio
      Returns:
      old cache ratio

    • setNodeTableSize

      public abstract int setNodeTableSize(int n)
      Sets the node table size.
      Parameters:
      n - new size of table
      Returns:
      old size of table

    • setCacheSize

      public abstract int setCacheSize(int n)
      Sets cache size.
      Parameters:
      n - new cache size
      Returns:
      old cache size

    • varNum

      public abstract int varNum()
      Returns the number of defined variables.

      Compare to bdd_varnum.

      Returns:
      number of defined variables

    • setVarNum

      public abstract int setVarNum(int num)
      Set the number of used BDD variables. It can be called more than one time, but only to increase the number of variables.

      Compare to bdd_setvarnum.

      Parameters:
      num - new number of BDD variables
      Returns:
      old number of BDD variables

    • extVarNum

      public int extVarNum(int num)
      Add extra BDD variables. Extends the current number of allocated BDD variables with num extra variables.

      Compare to bdd_extvarnum.

      Parameters:
      num - number of BDD variables to add
      Returns:
      old number of BDD variables

    • ithVar

      public abstract BDD ithVar(int var)
      Returns a BDD representing the I'th variable. (One node with the children true and false.) The requested variable must be in the (zero-indexed) range defined by setVarNum.

      Compare to bdd_ithvar.

      Parameters:
      var - the variable number
      Returns:
      the I'th variable on success, otherwise the constant false BDD

    • nithVar

      public abstract BDD nithVar(int var)
      Returns a BDD representing the negation of the I'th variable. (One node with the children false and true.) The requested variable must be in the (zero-indexed) range defined by setVarNum.

      Compare to bdd_nithvar.

      Parameters:
      var - the variable number
      Returns:
      the negated I'th variable on success, otherwise the constant false BDD

    • printAll

      public abstract void printAll()
      Prints all used entries in the node table.

      Compare to bdd_printall.

    • printTable

      public abstract void printTable(BDD b)
      Prints the node table entries used by a BDD.

      Compare to bdd_printtable.

      Parameters:
      b - BDD

    • load

      public BDD load(String filename) throws IOException
      Loads a BDD from a file.

      Compare to bdd_load.

      Parameters:
      filename - filename
      Returns:
      BDD
      Throws:
      IOException - In case of an I/O error.

    • load

      public BDD load(BufferedReader ifile) throws IOException
      Loads a BDD from the given input.

      Compare to bdd_load.

      Parameters:
      ifile - reader
      Returns:
      BDD
      Throws:
      IOException - In case of an I/O error.

    • load

      public BDD load(BufferedReader ifile, int[] translate) throws IOException
      Loads a BDD from the given input, translating BDD variables according to the given map.

      Compare to bdd_load.

      Parameters:
      ifile - reader
      translate - variable translation map
      Returns:
      BDD
      Throws:
      IOException - In case of an I/O error.

    • readNext

      protected String readNext(BufferedReader ifile) throws IOException
      Read the next token from the file.
      Parameters:
      ifile - reader
      Returns:
      next string token
      Throws:
      IOException - In case of an I/O error.

    • loadhash_get

      protected BDD loadhash_get(BDDFactory.LoadHash[] lh_table, int lh_nodenum, int key)
      Gets a BDD from the load hash table.
      Parameters:
      lh_table - load hash table
      lh_nodenum - node number
      key - key
      Returns:
      BDD

    • save

      public void save(String filename, BDD var) throws IOException
      Saves a BDD to a file.

      Compare to bdd_save.

      Parameters:
      filename - filename
      var - BDD
      Throws:
      IOException - In case of an I/O error.

    • save

      public void save(BufferedWriter out, BDD r) throws IOException
      Saves a BDD to an output writer.

      Compare to bdd_save.

      Parameters:
      out - writer
      r - BDD
      Throws:
      IOException - In case of an I/O error.

    • save_rec

      protected int save_rec(BufferedWriter out, BitSet visited, BDD root) throws IOException
      Helper function for save().
      Parameters:
      out - writer
      visited - visited nodes bitset
      root - root BDD
      Returns:
      bitset index
      Throws:
      IOException - In case of an I/O error.

    • level2Var

      public abstract int level2Var(int level)
      Convert from a BDD level to a BDD variable.

      Compare to bdd_level2var.

      Parameters:
      level - BDD level
      Returns:
      BDD variable

    • var2Level

      public abstract int var2Level(int var)
      Convert from a BDD variable to a BDD level.

      Compare to bdd_var2level.

      Parameters:
      var - BDD variable
      Returns:
      BDD level

    • reorder

      public abstract void reorder(BDDFactory.ReorderMethod m)
      Reorder the BDD with the given method.

      Compare to bdd_reorder.

      Parameters:
      m - reorder method

    • autoReorder

      public abstract void autoReorder(BDDFactory.ReorderMethod method)
      Enables automatic reordering. If method is REORDER_NONE then automatic reordering is disabled.

      Compare to bdd_autoreorder.

      Parameters:
      method - reorder method

    • autoReorder

      public abstract void autoReorder(BDDFactory.ReorderMethod method, int max)
      Enables automatic reordering with the given (maximum) number of reorderings. If method is REORDER_NONE then automatic reordering is disabled.

      Compare to bdd_autoreorder_times.

      Parameters:
      method - reorder method
      max - maximum number of reorderings

    • getReorderMethod

      public abstract BDDFactory.ReorderMethod getReorderMethod()
      Returns the current reorder method as defined by autoReorder.

      Compare to bdd_getreorder_method.

      Returns:
      ReorderMethod

    • getReorderTimes

      public abstract int getReorderTimes()
      Returns the number of allowed reorderings left. This value can be defined by autoReorder.

      Compare to bdd_getreorder_times.

      Returns:
      number of allowed reorderings left

    • disableReorder

      public abstract void disableReorder()
      Disable automatic reordering until enableReorder is called. Reordering is enabled by default as soon as any variable blocks have been defined.

      Compare to bdd_disable_reorder.

    • enableReorder

      public abstract void enableReorder()
      Enable automatic reordering after a call to disableReorder.

      Compare to bdd_enable_reorder.

    • reorderVerbose

      public abstract int reorderVerbose(int v)
      Enables verbose information about reordering. A value of zero means no information, one means some information and greater than one means lots of information.
      Parameters:
      v - the new verbose level
      Returns:
      the old verbose level

    • setVarOrder

      public abstract void setVarOrder(int[] neworder)
      This function sets the current variable order to be the one defined by neworder. The variable parameter neworder is interpreted as a sequence of variable indices and the new variable order is exactly this sequence. The array must contain all the variables defined so far. If, for instance the current number of variables is 3 and neworder contains [1; 0; 2] then the new variable order is v1 < v0 < v2.

      Note that this operation must walk through the node table many times, and therefore it is much more efficient to call this when the node table is small.

      Parameters:
      neworder - new variable order

    • getVarOrder

      public int[] getVarOrder()
      Gets the current variable order.
      Returns:
      variable order

    • makePair

      public abstract BDDPairing makePair()
      Make a new BDDPairing object.

      Compare to bdd_newpair.

      Returns:
      BDD pairing

    • makePair

      public BDDPairing makePair(int oldvar, int newvar)
      Make a new pairing that maps from one variable to another.
      Parameters:
      oldvar - old variable
      newvar - new variable
      Returns:
      BDD pairing

    • makePair

      public BDDPairing makePair(int oldvar, BDD newvar)
      Make a new pairing that maps from one variable to another BDD.
      Parameters:
      oldvar - old variable
      newvar - new BDD
      Returns:
      BDD pairing

    • makePair

      public BDDPairing makePair(BDDDomain oldvar, BDDDomain newvar)
      Make a new pairing that maps from one BDD domain to another.
      Parameters:
      oldvar - old BDD domain
      newvar - new BDD domain
      Returns:
      BDD pairing

    • swapVar

      public abstract void swapVar(int v1, int v2)
      Swap two variables.

      Compare to bdd_swapvar.

      Parameters:
      v1 - first variable
      v2 - second variable

    • addVarBlock

      public void addVarBlock(BDDVarSet var, boolean fixed)
      Adds a new variable block for reordering.

      Creates a new variable block with the variables in the variable set var. The variables in var must be contiguous.

      The fixed parameter sets the block to be fixed (no reordering of its child blocks is allowed) or free.

      Compare to bdd_addvarblock.

      Parameters:
      var - variable
      fixed - fixed or free

    • addVarBlock

      public abstract void addVarBlock(int first, int last, boolean fixed)
      Adds a new variable block for reordering.

      Creates a new variable block with the variables numbered first through last, inclusive.

      The fixed parameter sets the block to be fixed (no reordering of its child blocks is allowed) or free.

      Compare to bdd_intaddvarblock.

      Parameters:
      first - first variable number
      last - last variable number
      fixed - fixed or free

    • varBlockAll

      public abstract void varBlockAll()
      Add a variable block for all variables.

      Adds a variable block for all BDD variables declared so far. Each block contains one variable only. More variable blocks can be added later with the use of addVarBlock -- in this case the tree of variable blocks will have the blocks of single variables as the leafs.

      Compare to bdd_varblockall.

    • clearVarBlocks

      public abstract void clearVarBlocks()
      Clears all the variable blocks that have been defined by calls to addVarBlock.

      Compare to bdd_clrvarblocks.

    • printOrder

      public abstract void printOrder()
      Prints an indented list of the variable blocks.

      Compare to bdd_printorder.

    • nodeCount

      public abstract int nodeCount(Collection<BDD> r)
      Counts the number of shared nodes in a collection of BDDs. Counts all distinct nodes that are used in the BDDs -- if a node is used in more than one BDD then it only counts once.

      Compare to bdd_anodecount.

      Parameters:
      r - collection of BDDs
      Returns:
      number of shared nodes

    • getNodeTableSize

      public abstract int getNodeTableSize()
      Get the number of allocated nodes. This includes both dead and active nodes.

      Compare to bdd_getallocnum.

      Returns:
      number of allocated nodes

    • getNodeNum

      public abstract int getNodeNum()
      Get the number of active nodes in use. Note that dead nodes that have not been reclaimed yet by a garbage collection are counted as active.

      Compare to bdd_getnodenum.

      Returns:
      number of active nodes in use

    • getCacheSize

      public abstract int getCacheSize()
      Get the current size of the cache, in entries.
      Returns:
      size of cache

    • reorderGain

      public abstract int reorderGain()
      Calculate the gain in size after a reordering. The value returned is (100*(A-B))/A, where A is previous number of used nodes and B is current number of used nodes.

      Compare to bdd_reorder_gain.

      Returns:
      gain in size after a reordering

    • printStat

      public abstract void printStat()
      Print cache statistics.

      Compare to bdd_printstat.

    • getCacheStats

      public BDDFactory.CacheStats getCacheStats()
      Return the current operator cache statistics for this BDD factory.
      Returns:
      operator cache statistics

    • getMaxUsedBddNodesStats

      public BDDFactory.MaxUsedBddNodesStats getMaxUsedBddNodesStats()
      Return the current maximum used BDD nodes statistics for this BDD factory.
      Returns:
      maximum used BDD nodes statistics

    • getMaxMemoryStats

      public BDDFactory.MaxMemoryStats getMaxMemoryStats()
      Return the current maximum memory usage statistics for this BDD factory.
      Returns:
      maximum memory usage statistics

    • createDomain

      protected BDDDomain createDomain(int a, BigInteger b)
      Implementors must implement this factory method to create BDDDomain objects of the correct type.
      Parameters:
      a - index of this domain
      b - size of this domain
      Returns:
      BDD domain

    • extDomain

      public BDDDomain extDomain(long domainSize)
      Creates a new finite domain block of the given size. Allocates log 2 (|domainSize|) BDD variables for the domain.
      Parameters:
      domainSize - domainSize
      Returns:
      BDD domain

    • extDomain

      public BDDDomain extDomain(BigInteger domainSize)

    • extDomain

      public BDDDomain[] extDomain(int[] dom)
      Extends the set of finite domain blocks with domains of the given sizes. Each entry in domainSizes is the size of a new finite domain which later on can be used for finite state machine traversal and other operations on finite domains. Each domain allocates log 2 (|domainSizes[i]|) BDD variables to be used later. The ordering is interleaved for the domains defined in each call to extDomain. This means that assuming domain D0 needs 2 BDD variables x1 and x2 , and another domain D1 needs 4 BDD variables y1, y2, y3 and y4, then the order then will be x1, y1, x2, y2, y3, y4. The new domains are returned in order. The BDD variables needed to encode the domain are created for the purpose and do not interfere with the BDD variables already in use.

      Compare to fdd_extdomain.

      Parameters:
      dom - domain sizes
      Returns:
      BDD domains

    • extDomain

      public BDDDomain[] extDomain(long[] dom)

    • extDomain

      public BDDDomain[] extDomain(BigInteger[] domainSizes)

    • overlapDomain

      public BDDDomain overlapDomain(BDDDomain d1, BDDDomain d2)
      This function takes two finite domain blocks and merges them into a new one, such that the new one is encoded using both sets of BDD variables.

      Compare to fdd_overlapdomain.

      Parameters:
      d1 - first domain
      d2 - second domain
      Returns:
      BDD domain

    • makeSet

      public BDDVarSet makeSet(BDDDomain[] v)
      Returns a BDD defining all the variable sets used to define the variable blocks in the given array.

      Compare to fdd_makeset.

      Parameters:
      v - variable block array
      Returns:
      BDD variable set

    • clearAllDomains

      public void clearAllDomains()
      Clear all allocated finite domain blocks that were defined by extDomain() or overlapDomain().

      Compare to fdd_clearall.

    • numberOfDomains

      public int numberOfDomains()
      Returns the number of finite domain blocks defined by calls to extDomain().

      Compare to fdd_domainnum.

      Returns:
      number of finite domain blocks

    • getDomain

      public BDDDomain getDomain(int i)
      Returns the ith finite domain block, as defined by calls to extDomain().
      Parameters:
      i - index
      Returns:
      finite domain block

    • makeVarOrdering

      public int[] makeVarOrdering(boolean reverseLocal, String ordering)
      Creates a variable ordering from a string. The resulting order can be passed into setVarOrder(). Example: in the order "A_BxC_DxExF", the bits for A are first, followed by the bits for B and C interleaved, followed by the bits for D, E, and F interleaved.

      Obviously, domain names cannot contain the 'x' or '_' characters.

      Parameters:
      reverseLocal - whether to reverse the bits of each domain
      ordering - string representation of ordering
      Returns:
      int[] of ordering
      See Also:

    • createBitVector

      protected BDDBitVector createBitVector(int a)
      Implementors must implement this factory method to create BDDBitVector objects of the correct type.
      Parameters:
      a - bit number
      Returns:
      BDD bit vector

    • buildVector

      public BDDBitVector buildVector(int bitnum, boolean b)
      Build a bit vector that is constant true or constant false.

      Compare to bvec_true, bvec_false.

      Parameters:
      bitnum - bit number
      b - bit value
      Returns:
      BDD bit vector

    • constantVector

      public BDDBitVector constantVector(int bitnum, long val)
      Build a bit vector that corresponds to a constant value.

      Compare to bvec_con.

      Parameters:
      bitnum - bit number
      val - bit value
      Returns:
      BDD bit vector

    • constantVector

      public BDDBitVector constantVector(int bitnum, BigInteger val)

    • buildVector

      public BDDBitVector buildVector(int bitnum, int offset, int step)
      Build a bit vector using variables offset, offset+step, offset+2*step, ... , offset+(bitnum-1)*step.

      Compare to bvec_var.

      Parameters:
      bitnum - bit number
      offset - offset
      step - step
      Returns:
      BDD bit vector

    • buildVector

      public BDDBitVector buildVector(BDDDomain d)
      Build a bit vector using variables from the given BDD domain.

      Compare to bvec_varfdd.

      Parameters:
      d - BDD domain
      Returns:
      BDD bit vector

    • buildVector

      public BDDBitVector buildVector(int[] var)
      Build a bit vector using the given variables.

      compare to bvec_varvec.

      Parameters:
      var - variables
      Returns:
      BDD bit vector

    • registerGcStatsCallback

      public void registerGcStatsCallback(BDDFactory.GCStatsCallback callback)
      Register a garbage collection statistics callback.
      Parameters:
      callback - The callback to register.

    • registerReorderStatsCallback

      public void registerReorderStatsCallback(BDDFactory.ReorderStatsCallback callback)
      Register a variable reorder statistics callback.
      Parameters:
      callback - The callback to register.

    • registerResizeStatsCallback

      public void registerResizeStatsCallback(BDDFactory.ResizeStatsCallback callback)
      Register a node table resize statistics callback.
      Parameters:
      callback - The callback to register.

    • registerCacheStatsCallback

      public void registerCacheStatsCallback(BDDFactory.CacheStatsCallback callback)
      Register an operator cache statistics callback.
      Parameters:
      callback - The callback to register.

    • registerMaxUsedBddNodesStatsCallback

      public void registerMaxUsedBddNodesStatsCallback(BDDFactory.MaxUsedBddNodesStatsCallback callback)
      Register a maximum BDD nodes usage statistics callback.
      Parameters:
      callback - The callback to register.

    • registerMaxMemoryStatsCallback

      public void registerMaxMemoryStatsCallback(BDDFactory.MaxMemoryStatsCallback callback)
      Register a maximum memory usage statistics callback.
      Parameters:
      callback - The callback to register.

    • registerContinuousStatsCallback

      public void registerContinuousStatsCallback(BDDFactory.ContinuousStatsCallback callback)
      Register a continuously BDD nodes usage and BDD operations statistics callback.
      Parameters:
      callback - The callback to register.

    • unregisterGcStatsCallback

      public void unregisterGcStatsCallback(BDDFactory.GCStatsCallback callback)
      Unregister a garbage collection statistics callback.
      Parameters:
      callback - The callback to unregister.
      Throws:
      IllegalArgumentException - If callback is not registered.

    • unregisterReorderStatsCallback

      public void unregisterReorderStatsCallback(BDDFactory.ReorderStatsCallback callback)
      Unregister a variable reorder statistics callback.
      Parameters:
      callback - The callback to unregister.
      Throws:
      IllegalArgumentException - If callback is not registered.

    • unregisterResizeStatsCallback

      public void unregisterResizeStatsCallback(BDDFactory.ResizeStatsCallback callback)
      Unregister a node table resize statistics callback.
      Parameters:
      callback - The callback to unregister.
      Throws:
      IllegalArgumentException - If callback is not registered.

    • unregisterCacheStatsCallback

      public void unregisterCacheStatsCallback(BDDFactory.CacheStatsCallback callback)
      Unregister an operator cache statistics callback.
      Parameters:
      callback - The callback to unregister.
      Throws:
      IllegalArgumentException - If callback is not registered.

    • unregisterMaxUsedBddNodesStatsCallback

      public void unregisterMaxUsedBddNodesStatsCallback(BDDFactory.MaxUsedBddNodesStatsCallback callback)
      Unregister a maximum BDD nodes usage statistics callback.
      Parameters:
      callback - The callback to unregister.
      Throws:
      IllegalArgumentException - If callback is not registered.

    • unregisterMaxMemoryStatsCallback

      public void unregisterMaxMemoryStatsCallback(BDDFactory.MaxMemoryStatsCallback callback)
      Unregister a maximum memory usage statistics callback.
      Parameters:
      callback - The callback to unregister.
      Throws:
      IllegalArgumentException - If callback is not registered.

    • unregisterContinuousStatsCallback

      public void unregisterContinuousStatsCallback(BDDFactory.ContinuousStatsCallback callback)
      Unregister a continuously BDD nodes usage and BDD operations statistics callback.
      Parameters:
      callback - The callback to unregister.
      Throws:
      IllegalArgumentException - If callback is not registered.

    • hasGcStatsCallback

      public boolean hasGcStatsCallback()
      Returns whether this BDD factory has a registered garbage collection statistics callback.
      Returns:
      true if such a callback is registered, false otherwise.

    • hasReorderStatsCallback

      public boolean hasReorderStatsCallback()
      Returns whether this BDD factory has a registered variable reorder statistics callback.
      Returns:
      true if such a callback is registered, false otherwise.

    • hasResizeStatsCallback

      public boolean hasResizeStatsCallback()
      Returns whether this BDD factory has a registered node table resize statistics callback.
      Returns:
      true if such a callback is registered, false otherwise.

    • hasCacheStatsCallback

      public boolean hasCacheStatsCallback()
      Returns whether this BDD factory has a registered operator cache statistics callback.
      Returns:
      true if such a callback is registered, false otherwise.

    • hasMaxUsedBddNodesStatsCallback

      public boolean hasMaxUsedBddNodesStatsCallback()
      Returns whether this BDD factory has a registered maximum BDD nodes usage statistics callback.
      Returns:
      true if such a callback is registered, false otherwise.

    • hasMaxMemoryStatsCallback

      public boolean hasMaxMemoryStatsCallback()
      Returns whether this BDD factory has a registered maximum memory usage statistics callback.
      Returns:
      true if such a callback is registered, false otherwise.

    • hasContinuousStatsCallback

      public boolean hasContinuousStatsCallback()
      Returns whether this BDD factory has a registered continuously BDD nodes usage and BDD operations statistics callback.
      Returns:
      true if such a callback is registered, false otherwise.

    • invokeGcStatsCallbacks

      public void invokeGcStatsCallbacks(boolean pre)
      Invoke all registered garbage collection statistics callbacks.
      Parameters:
      pre - Whether this callback is invoked before (true) or after (false) garbage collection.

    • invokeReorderStatsCallbacks

      public void invokeReorderStatsCallbacks(boolean pre)
      Invoke all registered variable reorder statistics callbacks.
      Parameters:
      pre - Whether this callback is invoked before (true) or after (false) reordering.

    • invokeResizeStatsCallbacks

      public void invokeResizeStatsCallbacks(int oldsize, int newsize)
      Invoke all registered node table resize statistics callbacks.
      Parameters:
      oldsize - The old node table size.
      newsize - The new node table size.

    • invokeCacheStatsCallbacks

      public void invokeCacheStatsCallbacks()
      Invoke all registered operator cache statistics callbacks.

    • invokeMaxUsedBddNodesStatsCallbacks

      public void invokeMaxUsedBddNodesStatsCallbacks()
      Invoke all registered maximum BDD nodes usage statistics callbacks.

    • invokeMaxMemoryStatsCallbacks

      public void invokeMaxMemoryStatsCallbacks()
      Invoke all registered maximum memory usage statistics callbacks.

    • invokeContinuousStatsCallbacks

      public void invokeContinuousStatsCallbacks(int usedBddNodes, long opMiss)
      Invoke all registered continuously BDD nodes usage and BDD operations statistics callbacks.
      Parameters:
      usedBddNodes - The number of currently used BDD nodes. Represents a platform-independent measure that approximates memory use.
      opMiss - The number of BDD operations performed until now that could not be taken from the operation cache. Represents a platform-independent measure of approximates running time.

    • defaultGcStatsCallback

      public static void defaultGcStatsCallback(BDDFactory.GCStats stats, boolean pre)
      Default garbage collection statistics callback.
      Parameters:
      stats - The statistics.
      pre - Whether this callback is invoked before (true) or after (false) garbage collection.

    • defaultReorderStatsCallback

      public static void defaultReorderStatsCallback(BDDFactory.ReorderStats stats, boolean pre)
      Default variable reorder statistics callback.
      Parameters:
      stats - The statistics.
      pre - Whether this callback is invoked before (true) or after (false) reordering.

    • defaultResizeStatsCallback

      public static void defaultResizeStatsCallback(int oldsize, int newsize)
      Default node table resize statistics callback.
      Parameters:
      oldsize - The old node table size.
      newsize - The new node table size.

    • defaultCacheStatsCallback

      public static void defaultCacheStatsCallback(BDDFactory.CacheStats stats)
      Default operator cache statistics callback.
      Parameters:
      stats - The statistics.

    • defaultMaxUsedBddNodesStatsCallback

      public static void defaultMaxUsedBddNodesStatsCallback(BDDFactory.MaxUsedBddNodesStats stats)
      Default maximum BDD nodes usage statistics callback.
      Parameters:
      stats - The statistics.

    • defaultMaxMemoryStatsCallback

      public static void defaultMaxMemoryStatsCallback(BDDFactory.MaxMemoryStats stats)
      Default maximum memory usage statistics callback.
      Parameters:
      stats - The statistics.

    • defaultContinuousStatsCallback

      public static void defaultContinuousStatsCallback(int usedBddNodes, long opMiss)
      Default continuously BDD nodes usage and BDD operations statistics callback.
      Parameters:
      usedBddNodes - The number of currently used BDD nodes. Represents a platform-independent measure that approximates memory use.
      opMiss - The number of BDD operations performed until now that could not be taken from the operation cache. Represents a platform-independent measure of approximates running time.