-
Rbc_CnfVar2RbcIndex()
- Returns the RBC index corresponding to a particular CNF var
-
Rbc_Convert2Cnf()
- Translates the rbc into the corresponding (equisatisfiable)
set of clauses.
-
Rbc_GetIthVar()
- Returns a variable.
-
Rbc_GetLeftOpnd()
- Gets the left operand.
-
Rbc_GetOne()
- Logical constant 1 (truth).
-
Rbc_GetRightOpnd()
- Gets the right operand.
-
Rbc_GetVarIndex()
- Gets the variable index.
-
Rbc_GetZero()
- Logical constant 0 (falsity).
-
Rbc_MakeAnd()
- Makes the conjunction of two rbcs.
-
Rbc_MakeIff()
- Makes the coimplication of two rbcs.
-
Rbc_MakeIte()
- Makes the if-then-else of three rbcs.
-
Rbc_MakeNot()
- Returns the complement of an rbc.
-
Rbc_MakeOr()
- Makes the disjunction of two rbcs.
-
Rbc_MakeXor()
- Makes the exclusive disjunction of two rbcs.
-
Rbc_ManagerAlloc()
- Creates a new RBC manager.
-
Rbc_ManagerCapacity()
- Returns the current variable capacity of the rbc.
-
Rbc_ManagerFree()
- Deallocates an RBC manager.
-
Rbc_ManagerGC()
- Garbage collection in the RBC manager.
-
Rbc_ManagerReserve()
- Reserves more space for new variables.
-
Rbc_Mark()
- Makes a node permanent.
-
Rbc_OutputDaVinci()
- Print out an rbc using DaVinci graph format.
-
Rbc_OutputGdl()
- Print out an rbc using Gdl graph format.
-
Rbc_OutputSexpr()
- Print out an rbc using LISP S-expressions.
-
Rbc_PrintStats()
- Prints various statistics.
-
Rbc_RbcIndex2CnfVar()
- Returns the associated CNF variable of a given RBC index
-
Rbc_Shift()
- Creates a fresh copy G(X') of the rbc F(X) by shifting
each variable index of a certain amount.
-
Rbc_SubstRbc()
- Creates a fresh copy G(S) of the rbc F(X) such
that G(S) = F(X)[S/X
-
Rbc_Subst()
- Creates a fresh copy G(Y) of the rbc F(X) such
that G(Y) = F(X)[Y/X
-
Rbc_Unmark()
- Makes a node volatile.
Last updated on 2005/07/18 15h:57