Rbc_CnfConversionAlgorithm2Str()
Conversion from CNF conversion algorithm enumerative to string
Rbc_CnfConversionAlgorithmFromStr()
Conversion from string to CNF conversion algorithm enumerative
Rbc_CnfGetValidRbc2CnfAlgorithms()
String of valid conversion algorithms
Rbc_CnfVar2RbcIndex()
Returns the RBC index corresponding to a particular CNF var
Rbc_Convert2CnfCompact()
Translates the rbc into the corresponding (equisatisfiable) set of clauses.
Rbc_Convert2CnfSimple()
Translates the rbc into the corresponding (equisatisfiable) set of clauses.
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_IsConstant()
Returns true if the given rbc is a constant value, such as either False or True
Rbc_LogicalShift()
Creates a fresh copy G(X') of the rbc F(X) by shifting each variable index of a certain amount.
Rbc_LogicalSubstRbc()
Creates a fresh copy G(S) of the rbc F(X) such that G(S) = F(X)[S/X
Rbc_LogicalSubst()
Creates a fresh copy G(Y) of the rbc F(X) such that G(Y) = F(X)[Y/X
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.
Rbc_get_node_cnf()
Given a rbc node, this function returns the corrensponding CNF var it had been already allocated one. Otherwise it will allocate a new CNF var and will increment given maxvar value. If f is RBCDUMMY, a new variable will be always allocated (intended to be a non-terminal var, but a corresponding RBC var will be not allocated)
rbc_inlining_cache_add_result()
Inline caching private service
rbc_inlining_cache_init()
Inline caching private service
rbc_inlining_cache_lookup_result()
Inline caching private service
rbc_inlining_cache_quit()
Inline caching private service

Last updated on 2011/04/06 21h:12