CnfBack()
Dfs BackVisit for CNF conversion.
CnfCompactBack()
Dfs BackVisit for CNF conversion.
CnfCompactCleanFirst()
Dfs FirstVisit for cleaning.
CnfCompactCleanSet()
Dfs Set for cleaning.
CnfCompactCommit()
Extracts the cnf from the CLG
CnfCompactFirst()
Dfs FirstVisit for CNF conversion.
CnfCompactLast()
Dfs LastVisit for CNF conversion.
CnfCompactPolFirstBack()
Dfs FirstVisit and BackVisit for CNF conversion.
CnfCompactPolSet()
Dfs Set for CNF conversion.
CnfCompactSet()
Dfs Set for CNF conversion.
CnfEmpty()
Dfs empty function.
CnfFirst()
Dfs FirstVisit for CNF conversion.
CnfLast()
Dfs LastVisit for CNF conversion.
CnfSet()
Dfs Set for CNF conversion.
DaVinciBack()
Dfs BackVisit for DaVinci output.
DaVinciFirst()
Dfs FirstVisit for DaVinci output.
DaVinciLast()
Dfs LastVisit for DaVinci output.
DaVinciSet()
Dfs Set for DaVinci output.
GdlBack()
Dfs BackVisit for Gdl output.
GdlFirst()
Dfs FirstVisit for Gdl output.
GdlLast()
Dfs LastVisit for Gdl output.
GdlSet()
Dfs Set for Gdl output.
LogicalShiftLast()
Dfs LastVisit for logical shifting.
LogicalSubstLast()
Dfs LastVisit for logical Substitution.
LogicalSubstRbcLast()
Dfs LastVisit for logical Rbc Substitution.
RbcInline_apply_inlining()
Calculates the inlining of the given formula
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)
Reduce()
Reduction (simplification) of rbcs.
SexprBack()
Dfs BackVisit for Sexpr output.
SexprFirst()
Dfs FirstVisit for Sexpr output.
SexprLast()
Dfs LastVisit for Sexpr output.
SexprSet()
Dfs Set for Sexpr output.
ShiftBack()
Dfs BackVisit for shifting.
ShiftFirst()
Dfs FirstVisit for shifting.
ShiftLast()
Dfs LastVisit for shifting.
ShiftSet()
Dfs Set for shifting.
SubstBack()
Dfs BackVisit for substitution.
SubstFirst()
Dfs FirstVisit for substitution.
SubstLast()
Dfs LastVisit for Substitution.
SubstRbcBack()
Dfs BackVisit for substRbcitution.
SubstRbcFirst()
Dfs FirstVisit for substitution (variables to formulas).
SubstRbcLast()
Dfs LastVisit for SubstRbcitution.
SubstRbcSet()
Dfs Set for substitution (variables to formulas).
SubstSet()
Dfs Set for substitution.
SwapSign()
Swaps the sign of the argument.
disjunction2()
Compute the disjunction of two clause sets
disjunction()
Compute the disjunction of two clause sets
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
rename_clauses()
Renames a set of clauses.
testSizes()
Check whether two clause sets are big enough to require renaming
()
Control the kind of CNF conversion has to be used
()
Controls the sign of an rbc.

Last updated on 2009/03/04 12h:51