rbc.h
External header file
rbcInt.h
Internal header file
rbcCnf.c
Conjunctive Normal Form (CNF) conversions.
rbcCnfCompact.c
Conjunctive Normal Form (CNF) conversions.
rbcCnfSimple.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, Marco Roveri


rbcInt.h

Internal header file

By: Armando Tacchella and Tommi Junttila

()
Control the way compact CNF conversion is performed
()
Get the right children.
()
Rbc interface to underlying package

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 if 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_CnfConversionAlgorithmFromStr()
Conversion from string to CNF conversion algorithm enumerative
Rbc_CnfConversionAlgorithm2Str()
Conversion from CNF conversion algorithm enumerative to string
Rbc_CnfGetValidRbc2CnfAlgorithms()
String of valid conversion algorithms

rbcCnfCompact.c

Conjunctive Normal Form (CNF) conversions.

By: Daniel Sheridan, Marco Roveri and Gavin Keighren

External functions included in this module:

Rbc_Convert2CnfCompact()
Translates the rbc into the corresponding (equisatisfiable) set of clauses.
CnfCompactPolSet()
Dfs Set for CNF conversion.
CnfCompactPolFirstBack()
Dfs FirstVisit and BackVisit for CNF conversion.
CnfCompactSet()
Dfs Set for CNF conversion.
CnfCompactFirst()
Dfs FirstVisit for CNF conversion.
CnfCompactBack()
Dfs BackVisit for CNF conversion.
CnfCompactLast()
Dfs LastVisit for CNF conversion.
CnfCompactCleanSet()
Dfs Set for cleaning.
CnfCompactCleanFirst()
Dfs FirstVisit for cleaning.
CnfEmpty()
Dfs empty function.
rename_clauses()
Renames a set of clauses.
disjunction()
Compute the disjunction of two clause sets
disjunction2()
Compute the disjunction of two clause sets
testSizes()
Check whether two clause sets are big enough to require renaming
CnfCompactCommit()
Extracts the cnf from the CLG

rbcCnfSimple.c

Conjunctive Normal Form (CNF) conversions.

By: Armando Tacchella, Tommi Junttila and Marco Roveri

External functions included in this module:

Rbc_Convert2CnfSimple()
Translates the rbc into the corresponding (equisatisfiable) set of clauses.
CnfSet()
Dfs Set for CNF conversion.
CnfFirst()
Dfs FirstVisit for CNF conversion.
CnfBack()
Dfs BackVisit for CNF conversion.
CnfLast()
Dfs LastVisit for CNF conversion.
SwapSign()
Swaps the sign of the argument.

rbcFormula.c

Formula constructors.

By: Armando Tacchella, Tommi Junttila, Michele Dorigatti

External functions included in this module:

()
Calls several minimization rules.
()
Calls several minimization rules.
()
Calls several minimization rules.
()
Gets the children of the given rbcs
()
The Biere/Brummayer asymm. contradiction (O2) reduction rule
()
The Biere/Brummayer idempotence (O2) reduction rule
()
The Biere/Brummayer asymm. substitution (O3) reduction rule
()
The Biere/Brummayer asymm. subsumption (O2) reduction rule
()
The Biere/Brummayer idempotence (O4) reduction rule
()
The Biere/Brummayer resolution (O3) reduction rule
()
The Biere/Brummayer symm. subsumption (O2) reduction rule
()
The Biere/Brummayer symm. substitution (O3) reduction rule
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.
Rbc_is_top()
Check if a rbc type is RBCTOP
Rbc_is_and()
Check if a rbc type is RBCAND
Rbc_is_iff()
Check if a rbc type is RBCIFF
Rbc_is_var()
Check if a rbc type is RBCVAR
Rbc_is_ite()
Check if a rbc type is RBCITE
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_ManagerReset()
Resets 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 2011/06/16 12h:15