Printable data wrapper for the Bdd record.

The binary decision diagram, as a Bdd type.

The formula represented as a unicode string for direct printing.

The formula represented as a string, formatted in LaTeX.

An assignment is a valuation for a set of variables, i.e. a valuation as to whether a variable is true or false.

The printable BDD can label their variables, instead of using integers. A VarLabeller type is a function that encodes a variable integer to its corresponding name.

Encode a labelled integer as a BDD variable. Note that the first labeller is for text, the second for LaTeX. The variable is indexed by any integer from 0 to 1.000.000.

>>> slabel n = "var" ++ (show n)
>>> tlabel n = "p_" ++ (show n)
>>> foo = varl slabel tlabel 0
>>> foo
var0
>>> tex foo
p_0

Encode an unlabelled integer as a BDD variable. The variable is indexed by any integer from 0 to 1.000.000.

True constant.

>>> top
⊤

False constant.

>>> bot
⊥

Negation.

>>> neg foo
¬(foo)

Conjunction.

>>> foo `con` bar
(foo ∧ bar)

Disjunction.

>>> foo `dis` bar
(foo ∨ bar)

Logical implication.

>>> foo `imp` bar
(foo ⟶ bar)

Logical bi-implication or equivalence.

>>> foo `equ` bar
(foo ⟷ bar)

Exlusive or.

>>> foo `xor` bar
(foo ⊻ bar)

Big (setwise) conjunction.

>>> conSet [foo, bar, baz]
(foo ∧ bar ∧ baz)

Big (setwise) disjunction.

>>> disSet [foo, bar, baz]
(foo ∨ bar ∨ baz)

Big (setwise) exclusive disjunction.

>>> xorSet [foo, bar, baz]
(foo ⊻ bar ⊻ baz)

Labelled binary universal quantification. Note that the first VarLabeller works for direct printing and the VarLabeller is for latex.

>>> slabel n = "var" ++ (show n)
>>> tlabel n = "p_" ++ (show n)
>>> foo = foralll slabel tlabel 0 $ varl slabel tlabel 0 `imp` varl slabel tlabel 1
>>> foo
∀var0(var0 ⟶ var1)
>>> tex foo
\\forall p_0 (p_0 \\rightarrow p_1)

Unlabelled binary universal quantification.

>>> forall 0 foo
∀0(foo)

Labelled binary existential quantification.

>>> slabel n = "var" ++ (show n)
>>> tlabel n = "p_" ++ (show n)
>>> foo = existsl slabel tlabel 0 $ (varl slabel tlabel 0) `imp` (varl slabel tlabel 1)
>>> foo
∃var0(var0 ⟶ var1)
>>> tex foo
\\exists (p_0 \\rightarrow p_1) 

Unlabelled binary existential quantification

>>> exists 0 foo
∃0(foo)

Labelled big binary universal quanficition.

>>> slabel n = "var" ++ (show n)
>>> tlabel n = "p_" ++ (show n)
>>> foo = forallSetl slabel tlabel [0, 1] $ (varl slabel tlabel 0) `imp` (varl slabel tlabel 1)
>>> foo
∀{var0, var1}(var0 ⟶ var1)
>>> tex foo
\\forall \\left{ p_0, p_1 \\right} (p_0 \\rightarrow p_1)

Unlabelled big binary universal quantification.

>>> forallSet [0,1,2] foo
∀{0,1,2}(foo)

Labelled big binary existential quantification.

>>> slabel n = "var" ++ (show n)
>>> tlabel n = "p_" ++ (show n)
>>> foo = existsSetl slabel tlabel [0, 1] $ (varl slabel tlabel 0) `imp` (varl slabel tlabel 1)
>>> foo
∃{var0, var1}(var0 ⟶ var1)
>>> tex foo
\\exists \\left{ p_0, p_1 \\right} (p_0 \\rightarrow p_1)

Unlabelled big binary existential quantification.

>>> existsSet [0,1,2] foo
∃{0,1,2}(foo)

Labelled substitution.

>>> label n = "var" ++ n
>>> subsitl label 0 top foo
[var0\⊤](foo)

Unlabelled substitution.

>>> substit 0 top foo
[0\⊤]foo

Returns all variables (without labels) that occur within the given BDD.

>>> allVarsOf (var 0 `imp` (var 1 `dis` var 2))
[0,1,2]

Evaluate a BDD, given an assignment. Returns Nothing if the assignment doesn't contain all variables of the BDD.

>>> evaluate (var 0 `imp` var 1) [(0, True), (1, False)]
Just False 
>>> evaluate (var 0 `imp` var 1) [(0, True)]
Nothing

Evaluates a BDD, given a total assignment function.

>>> evaluateFun (var 0 `imp` var 1) (\ x -> if x == 0 then True else False)
False