CAL 3.0.0
An External Memory Decision Diagram Library
|
C++ wrapper for Cal_Bdd
, managing reference count with RAII.
More...
#include <calObj.hh>
Public Types | |
enum | Type_t { Zero = CAL_BDD_TYPE_ZERO , One = CAL_BDD_TYPE_ONE , Constant = CAL_BDD_TYPE_CONSTANT , Posvar = CAL_BDD_TYPE_POSVAR , Negvar = CAL_BDD_TYPE_NEGVAR , Overflow = CAL_BDD_TYPE_OVERFLOW , NonTerminal = CAL_BDD_TYPE_NONTERMINAL } |
Possible types a BDD can be. More... | |
using | Id_t = Cal_BddId_t |
Type of BDD identifiers, i.e. the variable name independent of the current variable ordering. | |
using | Index_t = Cal_BddIndex_t |
Type of BDD indices, i.e. their placement in the current variable ordering. | |
Public Member Functions | |
BDD () | |
The NULL BDD. | |
BDD (const BDD &other) | |
Copies ownership of another BDD. | |
BDD & | operator= (const BDD &other) |
Copy ownership of another BDD during assignment. | |
BDD (BDD &&other) | |
Move ownership of another BDD. | |
BDD & | operator= (BDD &&other) |
Move ownership of another BDD during assignment. | |
~BDD () | |
Decrement reference count upon leaving scope. | |
bool | IsOne () const |
true if the this BDD is constant one, false otherwise. | |
bool | IsZero () const |
true if the this BDD is constant zero, false otherwise. | |
bool | IsNull () const |
true if the this BDD is NULL, false otherwise. | |
bool | IsConst () const |
true if the this BDD is either constant one or constant zero, otherwise returns false . | |
bool | IsCube () const |
true if the this BDD is a cube, false otherwise. | |
bool | IsEqualTo (const BDD &other) const |
true if this BDD is equal to other , false otherwise. | |
bool | operator== (const BDD &other) const |
true if argument BDDs are equal, false otherwise. | |
bool | operator!= (const BDD &other) const |
false if argument BDDs are equal, true otherwise. | |
bool | DependsOn (const BDD &var) const |
true if this depends on var , false otherwise. | |
BDD | If () const |
BDD corresponding to the top variable of the this BDD. | |
Id_t | Id () const |
Returns the id of this BDD's top variable. | |
Index_t | Index () const |
Returns the index of this BDD's top variable. | |
BDD | Then () const |
The positive cofactor of this BDD with respect to its top variable. | |
BDD | Else () const |
The negative cofactor of this BDD with respect to its top variable. | |
Type_t | Type () const |
The BDD type (0, 1, +var, -var, overflow, nonterminal). | |
unsigned long | Size (bool negout=true) const |
This BDD's size. | |
double | SatisfyingFraction () const |
Fraction of valuations which make this BDD true. | |
BDD | Identity () const |
Duplicate of this BDD. | |
BDD | Regular () const |
Returns a BDD in positive form (regardless of this BDDs phase). | |
BDD | Not () const |
Complement of this BDD. | |
BDD | operator~ () const |
BDD | Compose (const BDD &g, const BDD &h) const |
Substitute a BDD variable by a function. | |
BDD | Intersects (const BDD &g) const |
Computes a BDD that implies conjunction of this and g . | |
BDD | Implies (const BDD &g) const |
Computes a BDD that implies conjunction of this and g.Not() . | |
BDD | ITE (const BDD &g, const BDD &h) const |
Logical If-Then-Else. | |
BDD | And (const BDD &g) const |
Logical AND operation. | |
BDD | operator& (const BDD &other) const |
BDD & | operator&= (const BDD &other) |
BDD | Nand (const BDD &g) const |
Logical Negated AND operation. | |
BDD | Or (const BDD &g) const |
Logical OR operation. | |
BDD | operator| (const BDD &other) const |
BDD & | operator|= (const BDD &other) |
BDD | Nor (const BDD &g) const |
Logical Negated OR operation. | |
BDD | Xor (const BDD &g) const |
Logical XOR operation. | |
BDD | operator^ (const BDD &other) const |
BDD & | operator^= (const BDD &other) |
BDD | Xnor (const BDD &g) const |
Logical Negated XOR operation. | |
BDD | Diff (const BDD &g) const |
Logical Difference operation. | |
BDD | operator- (const BDD &other) const |
BDD & | operator-= (const BDD &other) |
BDD | Satisfy () const |
A satisfying assignment of this BDD. | |
BDD | SatisfySupport () const |
Returns a special cube contained in this. | |
BDD | SwapVars (const BDD &g, const BDD &h) const |
The function obtained by swapping two variables. | |
BDD | Cofactor (const BDD &c) const |
Generalized cofactor of this with respect to c . | |
BDD | Reduce (const BDD &c) const |
A function that agrees with this for all valuations which satisfy c . | |
void | Print (FILE *fp=stdout) const |
Prints this BDD in the human readable form. | |
void | FunctionPrint (std::string &name) const |
Prints the function implemented by this BDD. | |
std::vector< long > | Profile (bool negout=true) const |
Obtain a vector with the number of nodes at each level in f. | |
void | PrintProfile (int lineLength=79, FILE *fp=stdout) const |
Prints a BDD in the human readable form. | |
std::vector< long > | FunctionProfile () const |
The number of subfunctions of this which may be obtained by restricting variables with an index lower than n. | |
void | PrintFunctionProfile (int lineLength=79, FILE *fp=stdout) const |
Similar to BDD::PrintProfile() but displays a function profile for this. | |
int | RefCount () const |
The reference count of this BDD. | |
std::string | ToString () const |
String representation of this BDD node. | |
Protected Member Functions | |
BDD (Cal_BddManager bddManager, Cal_Bdd bdd) | |
Wrap C API Cal_Bdd to be managed by this new BDD object. | |
C++ wrapper for Cal_Bdd
, managing reference count with RAII.
These BDDs are created from a Cal
object which owns the unique node table. Hence, the life-time of any BDD
object should not outlast its parent Cal
object. Doing so leads to undefined behaviour.
enum BDD::Type_t |
Possible types a BDD can be.
Enumerator | |
---|---|
Zero | The Zero terminal |
One | The One terminal |
Constant | Constant (Non-Boolean) |
Posvar | Positive variable |
Negvar | Negative variable |
Overflow | Invalid/Missing result due to Overflow |
NonTerminal | BDD type encompassing all other cases |
|
inlineprotected |
Wrap C API Cal_Bdd
to be managed by this new BDD
object.
This function does not increment the reference count of the given Cal_Bdd
, assuming the C API operation already has done so.
Generalized cofactor of this with respect to c
.
The constrain operator given by Coudert et al (ICCAD90) is used to find the generalized cofactor.
Substitute a BDD variable by a function.
g | Variable to be substituted. |
h | Function to substitute. |
|
inline |
The number of subfunctions of this which may be obtained by restricting variables with an index lower than n.
The nth entry of the function profile array is the number of subfunctions of this which may be obtained by restricting the variables whose index is less than n. An entry of zero indicates that this is independent of the variable with the corresponding index.
|
inline |
Returns the id of this BDD's top variable.
|
inline |
Duplicate of this BDD.
|
inline |
BDD corresponding to the top variable of the this BDD.
Computes a BDD that implies conjunction of this and g.Not()
.
Computes a BDD that implies conjunction of this and g
.
|
inline |
true
if the this BDD is either constant one or constant zero, otherwise returns false
.
|
inline |
true
if the this BDD is constant one, false
otherwise.
|
inline |
true
if the this BDD is constant zero, false
otherwise.
Logical If-Then-Else.
Returns the BDD for the logical operation f ? g : h
, i.e. f&g | ~f&h
.
|
inline |
false
if argument BDDs are equal, true
otherwise.
|
inline |
true
if argument BDDs are equal, false
otherwise.
|
inline |
|
inline |
Similar to BDD::PrintProfile()
but displays a function profile for this.
lineLength | The maximum line length. |
fp | Pointer to the FILE to output to (default stdout ). |
|
inline |
Prints a BDD in the human readable form.
lineLength | The maximum line length. |
fp | Pointer to the FILE to output to (default stdout ). |
|
inline |
Obtain a vector with the number of nodes at each level in f.
negout | If false then counting pretends the BDD does not have negative-output pointers (complement edges). |
A function that agrees with this for all valuations which satisfy c
.
The result is usually smaller in terms of number of BDD nodes than this. This operation is typically used in state space searches to simplify the representation for the set of states wich will be expanded at each step.
|
inline |
The reference count of this BDD.
The reference count is a value between 0 and 255. If a reference count is 255 then incrementing or decrementing it has no effect. This is to safe-guard constants and variables from being garbage collected.
|
inline |
Returns a BDD in positive form (regardless of this BDDs phase).
|
inline |
|
inline |
Fraction of valuations which make this BDD true.
f
is supposed to be a function of.
|
inline |
Returns a special cube contained in this.
The returned BDD which implies this, is true for some valuation on which f is true, which has at most one node at each level, and which has exactly one node corresponding to each variable which is associated with something in the current variable association.
|
inline |