Boole Parser

The libmc.Boole class can be used to evaluate and convert propositional formulae given in the Boole format, introduced by the SAT solver frontend limboole.

Format

The Boole format has the following syntax in BNF:

expr    ::=  iff
iff     ::=  implies { "<->" implies }
implies ::=  or [ "->" or | "<-" or ]
or      ::=  and { "|" and }
and     ::=  not { "&" not }
not     ::=  basic | "!" not
basic   ::=  var | "(" expr ")"

Where var is a string over letters, digits and the following characters:

- _ . [ ] $ @

Note

The last character of var should be different from -!

Parsing

Parsing a Boole formula is done by creating a libmc.Boole object:

contradiction = Boole("a & !a")

tautology = Boole("a | !a")

equivalence = Boole("a <-> b")

Evaluation

evaluate() is used to evaluate a propositional formula under a given assignment and truthTable() to generate it’s truth table:

assert not contradiction.evaluate({ 'a': True })
assert not contradiction.evaluate({ 'a': False })
assert contradiction.truthTable() == [
    ((False,), False),
    ((True,), False)
]

assert tautology.evaluate({ 'a': True })
assert tautology.evaluate({ 'a': False })
assert tautology.truthTable() == [
    ((False,), True),
    ((True,), True)
]

assert equivalence.evaluate({ 'a': True, 'b': True })
assert not equivalence.evaluate({ 'a': True, 'b': False })
assert equivalence.truthTable() == [
    ((False, False), True),
    ((False, True), False),
    ((True, False), False),
    ((True, True), True)
]

Conversion

libmc.Boole also offers methods for converting a propositional formula into other representations.

To AIG

Convert a Boole formula to an AIG in the AIGER format with toAIG():

assert contradiction.toAIG() == """\
aag 3 1 0 1 1
2
4
4 2 3
"""

assert tautology.toAIG() == """\
aag 3 1 0 1 1
2
5
4 3 2
"""

assert equivalence.toAIG() == """\
aag 6 2 0 1 3
2
4
7
6 9 11
8 2 4
10 3 5
"""

To BDD

Convert a Boole formula to a BDD with toBDD():

assert contradiction.toBDD() is BDD.false()

assert tautology.toBDD() is BDD.true()

assert equivalence.toBDD() is ~(BDD(0) ^ BDD(1))