Averest


PropLogic Module

This module implements functions for dealing with propositional logic like computing truth tables, evaluating formulas by truth assignments, computing canonical CNF and DNF and the sequent calculus.

Types

Type Description

BddCallExpr

BddCallExpr is used by function MkBDDCallTable and abbreviates calls of a BDD function. There are three kinds of BddCallExpr:

  • BddArg(bddAdr) is simply an address of a Bdd as argument
  • BddCallApply(fName,cL,y) is a call of BDD algorithm fName with arguments cL and result y
  • BddCallNode(x,c1,c0,y) represents two calls c1 and c0 embedded in a BDD node with root x which yields then BDD node y.

SequentProofTree

type for sequent calculus proof trees; each node has either one, two or no successor nodes and consists of two sets of formulas. Moreover, each node is uniquely identified by an index. Leaf nodes are further separated into valid ones (NodeTrue) and invalid ones (NodeFalse).

Functions and values

Function or value Description

BDDAlgorithmsTool qscoll

Full Usage: BDDAlgorithmsTool qscoll

Parameters:

This cgi-function provides various BDD algorithms.

qscoll : NameValueCollection

BDDReorderingTool qscoll

Full Usage: BDDReorderingTool qscoll

Parameters:

This cgi-function is used to first construct the BDD of a formula with a specified variable ordering and the converts it to the BDD of another specified variable ordering by a sequence of swap operations. Afterwards, it applies sifting to optimize the second ordering.

qscoll : NameValueCollection

CanonicalCNFofBDD bddAdr

Full Usage: CanonicalCNFofBDD bddAdr

Parameters:
Returns: Set<Set<BoolExpr>>

This function derives a formula in conjunctive normal form from a BDD. The CNF is given as a set of sets of literals with an obvious meaning.

bddAdr : BddAdr
Returns: Set<Set<BoolExpr>>

CanonicalCNFofTruthTable atomL phi

Full Usage: CanonicalCNFofTruthTable atomL phi

Parameters:
Returns: Set<Set<BoolExpr>>

Compute canonical CNF by truth table, where the maxterms are ordered as given by atomL.

atomL : BoolExpr list
phi : BoolExpr
Returns: Set<Set<BoolExpr>>

CanonicalDNFofBDD bddAdr

Full Usage: CanonicalDNFofBDD bddAdr

Parameters:
Returns: Set<Set<BoolExpr>>

This function derives a formula in disjunctive normal form from a BDD. The DNF is given as a set of sets of literals with an obvious meaning.

bddAdr : BddAdr
Returns: Set<Set<BoolExpr>>

CanonicalDNFofTruthTable atomL phi

Full Usage: CanonicalDNFofTruthTable atomL phi

Parameters:
Returns: Set<Set<BoolExpr>>

Compute canonical DNF by truth table, where the minterms are ordered as given by atomL.

atomL : BoolExpr list
phi : BoolExpr
Returns: Set<Set<BoolExpr>>

CanonicalRMNF phi

Full Usage: CanonicalRMNF phi

Parameters:
Returns: Set<Set<BoolExpr>>

Compute Reed-Muller normal form directly from a formula, where the RMNF is encoded as sets of sets of variables where false is {}, true is {{}}, x is {{x}}, and !x is {{},{x}}. We define a n-ary XOR as XOR{} := false; XOR{m} := m; and otherwise the xor of the elements. Similarly, we have AND{} := true, AND{x} := x, etc.

phi : BoolExpr
Returns: Set<Set<BoolExpr>>

CanonicalSNFofBDD bddAdr

Full Usage: CanonicalSNFofBDD bddAdr

Parameters:
Returns: BoolExpr

This function derives a formula in Shannon normal form from a BDD. Of course, the formula can have an exponential size also for a small BDD.

bddAdr : BddAdr
Returns: BoolExpr

ComputeAllAssignments atomL

Full Usage: ComputeAllAssignments atomL

Parameters:
Returns: Map<BoolExpr, bool> list

Enumerate all assignments for the given list of atoms; an assignment is thereby a map that maps an atom of the given boolean expression to a boolean value.

atomL : BoolExpr list
Returns: Map<BoolExpr, bool> list

ComputeFDDs atomL rmfL

Full Usage: ComputeFDDs atomL rmfL

Parameters:
Returns: int list * Map<(BoolExpr * int * int), int>

ComputeFDDs computes the functional decision diagrams of Reed-Muller normal forms as computed by CanonicalRMNF following the variable order given by argument atomL (as always for decision diagrams, the leftmost atom in atomL is closest to the leaf nodes). The FDDs are stored in a map that maps a node address i to a triple (x,i1,i0) where x is the variable of the node, and i1,i0 are the addresses of the positive and negative subFDDs. The result is a pair (iL,m) where iL is the list of addresses of the FDDs and m is the map described before.

atomL : BoolExpr list
rmfL : Set<Set<BoolExpr>> list
Returns: int list * Map<(BoolExpr * int * int), int>

ComputeZDDs atomL bddL

Full Usage: ComputeZDDs atomL bddL

Parameters:
Returns: int list * Map<(BoolExpr * int * int), int>

ComputeZDDs computes for a given list of BDDs the corresponding ZDDs where the variable ordering atomL is followed (should be the one used by the BDDs, i.e., as always for decision diagrams, the leftmost atom in atomL is closest to the leaf nodes). Analogously to the FDDs, the ZDDs are stored in a map that maps a node address i to a triple (x,i1,i0) where x is the variable of the node, and i1,i0 are the addresses of the positive and negative subZDDs. The result is a pair (iL,m) where iL is the list of addresses of the ZDDs and m is the map described before.

atomL : BoolExpr list
bddL : BddAdr list
Returns: int list * Map<(BoolExpr * int * int), int>

DualRails inputSet posName negName phi

Full Usage: DualRails inputSet posName negName phi

Parameters:
    inputSet : Set<BoolExpr>
    posName : string -> string
    negName : string -> string
    phi : BoolExpr

Returns: BoolExpr * BoolExpr

Dual-rail encoding of a formula: If a variable x belongs to inputSet, it will be encoded as (x,!x) instead of (x+,x-).

inputSet : Set<BoolExpr>
posName : string -> string
negName : string -> string
phi : BoolExpr
Returns: BoolExpr * BoolExpr

EvalBoolExpr rho e

Full Usage: EvalBoolExpr rho e

Parameters:
Returns: bool

Evaluate a formula with respect to a given assignment of the atoms. It is expected that the given assignment is complete, i.e., that every atom of the given boolean expression is mapped to either true or false.

rho : Map<BoolExpr, bool>
e : BoolExpr
Returns: bool

FDD2Dot outStr writeLF (iL, fddMap)

Full Usage: FDD2Dot outStr writeLF (iL, fddMap)

Parameters:

Write a FDD as generated by function ComputeFDD to a DotFile.

outStr : TextWriter
writeLF : bool
iL : int list
fddMap : Map<(BoolExpr * int * int), int>

KarnaughVeitch atomL

Full Usage: KarnaughVeitch atomL

Parameters:
Returns: Map<BoolExpr, bool>[] * Map<BoolExpr, bool>[]

Computes a KV diagram for a given list of atoms. The KV diagram is given as two arrays (col,row) where col and row denote the column and row vectors, respectively, i.e., col[i] and row[j] denote the assignments to the variables in entry (i,j) of the KV diagram, and their union is therefore the assignment to be evaluated there.

atomL : BoolExpr list
Returns: Map<BoolExpr, bool>[] * Map<BoolExpr, bool>[]

LinearClauseForm phi

Full Usage: LinearClauseForm phi

Parameters:
Returns: BoolExpr * ((BoolExpr * BoolExpr) * Set<Set<BoolExpr>>) list

Generate linear clause forms for a given formula phi. The result is a pair (v,l) where v is the variable that finally abbreviates phi, and l is a list of pairs ((v,t),cl) where (v,t) represents an abbreviation v=t and cl is its corresponding clause set.

phi : BoolExpr
Returns: BoolExpr * ((BoolExpr * BoolExpr) * Set<Set<BoolExpr>>) list

LogicMinimizationTool qscoll

Full Usage: LogicMinimizationTool qscoll

Parameters:

This cgi-function is used for logic minimization using KV diagrams, the Quine/McCluskey table, or symbolic logic minimization.

qscoll : NameValueCollection

MkBDDCallTable vComp call

Full Usage: MkBDDCallTable vComp call

Parameters:
Returns: Map<BddCallExpr, BddCallExpr list>

This function explains the recursive calls of a BDD function like Apply. The function expects a call to such a BDD function as explained with type BddCallExpr. In case of Compose, the optional argument vComp must contain the BDD index of the variable that should be replaced in the BDD. The result is a table that maps a BddCallExpr to a list of such that explains the computations.

vComp : AtomIndex option
call : BddCallExpr
Returns: Map<BddCallExpr, BddCallExpr list>

MkCanonicalCNF atomL cnf

Full Usage: MkCanonicalCNF atomL cnf

Parameters:
Returns: BoolExpr

Construct a CNF formula of a set of sets representation (clause set), where the literals in the cubes are ordered as given by atomL.

atomL : BoolExpr list
cnf : Set<Set<BoolExpr>>
Returns: BoolExpr

MkCanonicalDNF atomL dnf

Full Usage: MkCanonicalDNF atomL dnf

Parameters:
Returns: BoolExpr

Construct a DNF formula of a set of sets representation, where the literals in the maxterms are ordered as given by atomL.

atomL : BoolExpr list
dnf : Set<Set<BoolExpr>>
Returns: BoolExpr

MkPrimImplicantBDD phi

Full Usage: MkPrimImplicantBDD phi

Parameters:
Returns: BoolExpr list list * BddAdr * BddAdr
phi : BoolExpr
Returns: BoolExpr list list * BddAdr * BddAdr

PartialEval rho e

Full Usage: PartialEval rho e

Parameters:
Returns: BoolExpr

Partial evaluation of a formula wrt. a partial variable assignment: Since the given assignment rho may not map every atom of the boolean expression to a boolean value, the result is just another boolean formula where the mapped atoms are replaced by constants and where simplifications were applied to propagate these constants.

rho : Map<BoolExpr, bool>
e : BoolExpr
Returns: BoolExpr

PrintKarnaughVeitch atomL (col, row) care phi

Full Usage: PrintKarnaughVeitch atomL (col, row) care phi

Parameters:

Print a KV diagram as constructed by KarnaughVeitch as a html table.

atomL : BoolExpr list
col : seq<Map<BoolExpr, bool>>
row : seq<Map<BoolExpr, bool>>
care : BoolExpr
phi : BoolExpr

PrintTruthTable atomL formulaL

Full Usage: PrintTruthTable atomL formulaL

Parameters:

Print the truth tables for the given functions as a html table.

atomL : BoolExpr list
formulaL : seq<BoolExpr>

PropLogicTool qscoll

Full Usage: PropLogicTool qscoll

Parameters:

PropLogicTool is the function to be called from the web page

qscoll : NameValueCollection

QuineCube2BitvecStr atomL (idx, arg3)

Full Usage: QuineCube2BitvecStr atomL (idx, arg3)

Parameters:
Returns: string

Convert a cube (idx,(pos,neg)) as used in the Quine table to a string. The index set idx is written as a set of integers {i1,...,iN} and the cube (pos,neg) itself is written as a bitvector with * whenever there is a don't care.

atomL : BoolExpr list
idx : Set<'a>
arg2 : Set<BoolExpr> * Set<BoolExpr>
Returns: string

QuineCube2Minterm atomL (idx, arg3)

Full Usage: QuineCube2Minterm atomL (idx, arg3)

Parameters:
Returns: BoolExpr

Convert a cube (idx,(pos,neg)) as used in the Quine table to a boolean expression where the literals occur as specified by the variable order atomL.

atomL : BoolExpr list
idx : 'a
arg2 : Set<BoolExpr> * Set<BoolExpr>
Returns: BoolExpr

QuineMcCluskeyMinimalDNF atomL care phi

Full Usage: QuineMcCluskeyMinimalDNF atomL care phi

Parameters:
Returns: (Set<int> * (Set<BoolExpr> * Set<BoolExpr>)) list list list * (BoolExpr * (Set<int> * (Set<BoolExpr> * Set<BoolExpr>))) list * BoolExpr * Set<Set<BoolExpr>> * Set<BoolExpr>

The following function computes minimal DNFs for a given formula phi with a care set care, where the ordering of atoms atomL is respected. The function applies first the Quine method QuineTable to compute all cubes (implicants) of care->phi, and extracts then the prime cubes with function QuineTablePrimeImplicants where each prime cube is associated with a new boolean variable PI[i]. After this, it generates a formula coverPhi in CNF over the variables PI[i] such that coverPhi has a disjunct for each model of care&phi and that contains all PI[i] that cover that model. The formula coverPhi is then converted to DNF (in sets of sets representation) so that minimal DNFs for phi wrt. care can be derived. The function finally returns a tuple (qt,primeCubes,coverPhi,dnfCover,minDNFs) with:

  • qt is the Quine table as generated by function QuineTable.
  • primeCubes is a list of pairs (PI[i],pc[i]) where pi is a variable associated with prime cube pc[i].
  • coverPhi is the cover formula using variables PI[i] in CNF.
  • dnfCover is the set of set representation of coverPhi.
  • minDNFs is the list of minimal DNFs of phi wrt. care set care.

atomL : BoolExpr list
care : BoolExpr
phi : BoolExpr
Returns: (Set<int> * (Set<BoolExpr> * Set<BoolExpr>)) list list list * (BoolExpr * (Set<int> * (Set<BoolExpr> * Set<BoolExpr>))) list * BoolExpr * Set<Set<BoolExpr>> * Set<BoolExpr>

QuineTable atomL phi

Full Usage: QuineTable atomL phi

Parameters:
Returns: (Set<int> * (Set<BoolExpr> * Set<BoolExpr>)) list list list

Compute the Quine table: The function expects a formula phi and its variable order order atomL. It computes the Quine table that contains all implicants of phi as a list of list of lists [I0;...;In] where each Ik is the list of list of implicants of order k, i.e., where k variables are don't cares, hence, I0 are all full models of phi. Each Ik=[Lk0;...;Lkj] is partitioned into levels Lki according to the number of atoms made true (zero in Lk0 up to j in Lkj]. Each Lki is finally a list of cubes, where a cube (idx,(pos,neg)) is given by the sets of atoms (pos,neg) made true and false by the cube, respectively. The index idx is a set of integers that uniquely represents the cube; it is the union of binary numbers that an be derived when all don't cares are replaced by either true and false (following the order atomL).

atomL : BoolExpr list
phi : BoolExpr
Returns: (Set<int> * (Set<BoolExpr> * Set<BoolExpr>)) list list list

QuineTable2Html atomL qt

Full Usage: QuineTable2Html atomL qt

Parameters:

Print a Quine table as a html table

atomL : BoolExpr list
qt : (Set<int> * (Set<BoolExpr> * Set<BoolExpr>)) list list list

QuineTablePrimeImplicants qt

Full Usage: QuineTablePrimeImplicants qt

Parameters:
Returns: (BoolExpr * (Set<int> * (Set<BoolExpr> * Set<BoolExpr>))) list

Get the prime implicants of a formula phi from its Quine table: We check whether the index set of a cube is contained in one of the other cube's index set of the next level. If so, it is not a prime implicant, since it has been used to construct that higher cube. The function returns a list of tuples (piv,(idx,(pos,neg))) where piv is a boolean variable generated for the prime implicant (idx,(pos,neg)).

qt : (Set<int> * (Set<BoolExpr> * Set<BoolExpr>)) list list list
Returns: (BoolExpr * (Set<int> * (Set<BoolExpr> * Set<BoolExpr>))) list

RMNF2Str rmf

Full Usage: RMNF2Str rmf

Parameters:
Returns: string

This function converts a Reed-Muller form given in set representation to a string where xor is printed as ⊕.

rmf : Set<Set<BoolExpr>>
Returns: string

SequentCalculusProof i (leftSet, rightSet)

Full Usage: SequentCalculusProof i (leftSet, rightSet)

Parameters:
Returns: int * SequentProofTree

Construct a proof tree for the validity of a given formula; the function expects an index i for the root node and the goal of the root node.

i : int
leftSet : Set<BoolExpr>
rightSet : Set<BoolExpr>
Returns: int * SequentProofTree

SequentProofTree2Dot ostr p

Full Usage: SequentProofTree2Dot ostr p

Parameters:

write proof tree to a dot file

ostr : TextWriter
p : SequentProofTree

SolveBoolExprByBDDs e

Full Usage: SolveBoolExprByBDDs e

Parameters:
Returns: Map<BoolExpr, bool> option

Solves a propositional logic formula phi by means of the BDD package. If there is no model, the result is None, otherwise, a model is returned as a mapping of BoolExpr to boolean truth values.

e : BoolExpr
Returns: Map<BoolExpr, bool> option

SolveBoolExprBySatSolver e

Full Usage: SolveBoolExprBySatSolver e

Parameters:
Returns: Map<BoolExpr, bool> option

Solves a propositional logic formula phi by means of the SAT solver. If there is no model, the result is None, otherwise, a model is returned as a mapping of BoolExpr to boolean truth values.

e : BoolExpr
Returns: Map<BoolExpr, bool> option

ZDD2Dot outStr writeLF (iL, zddMap)

Full Usage: ZDD2Dot outStr writeLF (iL, zddMap)

Parameters:

Write a ZDD as generated by function ComputeZDD to a DotFile.

outStr : TextWriter
writeLF : bool
iL : int list
zddMap : Map<(BoolExpr * int * int), int>

getRMNF uniqueTable i

Full Usage: getRMNF uniqueTable i

Parameters:
    uniqueTable : Map<(BoolExpr * int * int), int>
    i : int

Returns: Set<Set<BoolExpr>>

Extract a Reed-Muller form set representation from a graph (FDD) given in a unique table as returned by functions ComputeFDDs and ComputeZDDs.

uniqueTable : Map<(BoolExpr * int * int), int>
i : int
Returns: Set<Set<BoolExpr>>

getSNFofZDD uniqueTable atomL i

Full Usage: getSNFofZDD uniqueTable atomL i

Parameters:
Returns: BoolExpr

Extract a Shannon normal representation from a decision diagram (read as ZDD) given in a unique table as returned by functions ComputeFDDs and ComputeZDDs. The ordering given in atomL should be consistent with the one used in the ZDDs, i.e., leftmost atom in atomL should be closest to the leaf nodes.

uniqueTable : Map<(BoolExpr * int * int), int>
atomL : BoolExpr list
i : int
Returns: BoolExpr

printSNF indent phi

Full Usage: printSNF indent phi

Parameters:

This function prints a formula in Shannon normal form such that the cofactors are printed in different lines with suitable indentation.

indent : string
phi : BoolExpr