-
rbc.h
- External header file
-
rbcInt.h
- Internal header file
-
rbcCnf.c
- Conjunctive Normal Form (CNF) conversions.
-
rbcCnf.c
- Conjunctive Normal Form (CNF) conversions.
-
rbcCnf.c
- Conjunctive Normal Form (CNF) conversions.
-
rbcFormula.c
- Formula constructors.
-
rbcInline.c
- Implementaion of RBC inlining
-
rbcManager.c
- RBC manager main routines.
-
rbcOutput.c
- Formula output in various formats.
-
rbcStat.c
- RBC manager statistics.
-
rbcSubst.c
- Formula substitutions.
-
rbcUtils.c
- Some general functions working on RBCs
rbc.h
External header file
By: Armando Tacchella
rbcInt.h
Internal header file
By: Armando Tacchella and Tommi Junttila
-
()
- Controls the sign of an rbc.
-
()
- Control the kind of CNF conversion has to be used
rbcCnf.c
Conjunctive Normal Form (CNF) conversions.
By: Armando Tacchella, Tommi Junttila, Marco Roveri, Dan Sheridan
and Gavin Keighren
External functions included in this module:
- Rbc_Convert2Cnf()
- Rbc_CnfVar2RbcIndex()
- Rbc_RbcIndex2CnfVar()
-
Rbc_Convert2Cnf()
- Translates the rbc into the corresponding (equisatisfiable)
set of clauses.
-
Rbc_CnfVar2RbcIndex()
- Returns the RBC index corresponding to a particular CNF var
-
Rbc_RbcIndex2CnfVar()
- Returns the associated CNF variable of a given RBC index
-
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)
rbcCnf.c
Conjunctive Normal Form (CNF) conversions.
By: Daniel Sheridan, Marco Roveri and Gavin Keighren
External functions included in this module:
-
Rbc_Convert2Cnf()
- Translates the rbc into the corresponding (equisatisfiable)
set of clauses.
-
Rbc_CnfVar2RbcIndex()
- Returns the RBC index corresponding to a particular CNF var
-
Rbc_RbcIndex2CnfVar()
- Returns the associated CNF variable of a given RBC index
-
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)
rbcCnf.c
Conjunctive Normal Form (CNF) conversions.
By: Armando Tacchella, Tommi Junttila and Marco Roveri
External functions included in this module:
-
Rbc_Convert2Cnf()
- Translates the rbc into the corresponding (equisatisfiable)
set of clauses.
-
Rbc_CnfVar2RbcIndex()
- Returns the RBC index corresponding to a particular CNF var
-
Rbc_RbcIndex2CnfVar()
- Returns the associated CNF variable of a given RBC index
-
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)
rbcFormula.c
Formula constructors.
By: Armando Tacchella and Tommi Junttila
External functions included in this module:
- Rbc_GetOne() logical truth
- Rbc_GetZero() logical falsity
- Rbc_GetIthVar variables
- Rbc_MakeNot() negation
- Rbc_MakeAnd() conjunction
- Rbc_MakeOr() disjunction
- Rbc_MakeIff() coimplication
- Rbc_MakeXor() exclusive disjunction
- Rbc_MakeIte() if-then-else
- Rbc_GetLeftOpnd() return left operand
- Rbc_GetRightOpnd() return right operand
- Rbc_GetVarIndex() return the variable index
- Rbc_Mark() make a vertex permanent
- Rbc_Unmark() make a vertex volatile
-
Rbc_GetOne()
- Logical constant 1 (truth).
-
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_GetIthVar()
- Returns a variable.
-
Rbc_MakeNot()
- Returns the complement of an rbc.
-
Rbc_MakeAnd()
- Makes the conjunction of two rbcs.
-
Rbc_MakeOr()
- Makes the disjunction of two rbcs.
-
Rbc_MakeIff()
- Makes the coimplication of two rbcs.
-
Rbc_MakeXor()
- Makes the exclusive disjunction of two rbcs.
-
Rbc_MakeIte()
- Makes the if-then-else of three rbcs.
-
Rbc_GetLeftOpnd()
- Gets the left operand.
-
Rbc_GetRightOpnd()
- Gets the right operand.
-
Rbc_GetVarIndex()
- Gets the variable index.
-
Rbc_Mark()
- Makes a node permanent.
-
Rbc_Unmark()
- Makes a node volatile.
-
Reduce()
- Reduction (simplification) of rbcs.
rbcInline.c
Implementaion of RBC inlining
By: Roberto Cavada
See Alsorbc.h
-
RbcInline_apply_inlining()
- Calculates the inlining of the given formula
-
rbc_inlining_cache_init()
- Inline caching private service
-
rbc_inlining_cache_quit()
- Inline caching private service
-
rbc_inlining_cache_add_result()
- Inline caching private service
-
rbc_inlining_cache_lookup_result()
- Inline caching private service
rbcManager.c
RBC manager main routines.
By: Armando Tacchella
External procedures included in this module:
- Rbc_ManagerAlloc() allocates the manager;
- Rbc_ManagerReserve() makes room for more variables
- Rbc_ManagerCapacity() returns available variables
- Rbc_ManagerFree() deallocates the manager;
- Rbc_ManagerGC() forces internal garbage coll.
-
Rbc_ManagerAlloc()
- Creates a new RBC manager.
-
Rbc_ManagerReserve()
- Reserves more space for new variables.
-
Rbc_ManagerCapacity()
- Returns the current variable capacity of the rbc.
-
Rbc_ManagerFree()
- Deallocates an RBC manager.
-
Rbc_ManagerGC()
- Garbage collection in the RBC manager.
rbcOutput.c
Formula output in various formats.
By: Armando Tacchella
External functions included in this module:
- Rbc_OutputDaVinci()
- Rbc_OutputSexpr()
-
Rbc_OutputDaVinci()
- Print out an rbc using DaVinci graph format.
-
Rbc_OutputSexpr()
- Print out an rbc using LISP S-expressions.
-
DaVinciSet()
- Dfs Set for DaVinci output.
-
DaVinciFirst()
- Dfs FirstVisit for DaVinci output.
-
DaVinciBack()
- Dfs BackVisit for DaVinci output.
-
DaVinciLast()
- Dfs LastVisit for DaVinci output.
-
SexprSet()
- Dfs Set for Sexpr output.
-
SexprFirst()
- Dfs FirstVisit for Sexpr output.
-
SexprBack()
- Dfs BackVisit for Sexpr output.
-
SexprLast()
- Dfs LastVisit for Sexpr output.
-
Rbc_OutputGdl()
- Print out an rbc using Gdl graph format.
-
GdlSet()
- Dfs Set for Gdl output.
-
GdlFirst()
- Dfs FirstVisit for Gdl output.
-
GdlBack()
- Dfs BackVisit for Gdl output.
-
GdlLast()
- Dfs LastVisit for Gdl output.
rbcStat.c
RBC manager statistics.
By: Armando Tacchella
External functions included in this module:
-
Rbc_PrintStats()
- Prints various statistics.
rbcSubst.c
Formula substitutions.
By: Armando Tacchella and Tommi Junttila
External functions included in this module:
- Rbc_Subst() Substitute variables with variables
- Rbc_Shift() Shift the variables along an offset
- Rbc_SubstRbc() Substitute variables with formulas
-
Rbc_Subst()
- Creates a fresh copy G(Y) of the rbc F(X) such
that G(Y) = F(X)[Y/X
-
Rbc_LogicalSubst()
- Creates a fresh copy G(Y) of the rbc F(X) such
that G(Y) = F(X)[Y/X
-
Rbc_Shift()
- Creates a fresh copy G(X') of the rbc F(X) by shifting
each variable index of a certain amount.
-
Rbc_LogicalShift()
- 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_LogicalSubstRbc()
- Creates a fresh copy G(S) of the rbc F(X) such
that G(S) = F(X)[S/X
-
SubstSet()
- Dfs Set for substitution.
-
SubstFirst()
- Dfs FirstVisit for substitution.
-
SubstBack()
- Dfs BackVisit for substitution.
-
SubstLast()
- Dfs LastVisit for Substitution.
-
LogicalSubstLast()
- Dfs LastVisit for logical Substitution.
-
ShiftSet()
- Dfs Set for shifting.
-
ShiftFirst()
- Dfs FirstVisit for shifting.
-
ShiftBack()
- Dfs BackVisit for shifting.
-
ShiftLast()
- Dfs LastVisit for shifting.
-
LogicalShiftLast()
- Dfs LastVisit for logical shifting.
-
SubstRbcSet()
- Dfs Set for substitution (variables to formulas).
-
SubstRbcFirst()
- Dfs FirstVisit for substitution (variables to formulas).
-
SubstRbcBack()
- Dfs BackVisit for substRbcitution.
-
SubstRbcLast()
- Dfs LastVisit for SubstRbcitution.
-
LogicalSubstRbcLast()
- Dfs LastVisit for logical Rbc Substitution.
rbcUtils.c
Some general functions working on RBCs
By: Roberto Cavada
See Alsorbc.h
Last updated on 2009/03/04 13h:34