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()
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 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()
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()
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()
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/01/30 15h:04