expressions

Tools for working with Boolean expressions.

expressions.bexpr module

Tools for interacting with Boolean expressions.

class tt.expressions.bexpr.BooleanExpression(expr)[source]

Bases: object

An interface for interacting with a Boolean expression.

Instances of BooleanExpression are meant to be immutable and can be instantiated from a few different representations of expressions. The simplest way to make an expression object is from a string:

>>> from tt import BooleanExpression
>>> BooleanExpression('(A or B) iff (C and D)')
<BooleanExpression "(A or B) iff (C and D)">

If you already have an instance of ExpressionTreeNode laying around, you can make a new expression object from that, too:

>>> from tt import ExpressionTreeNode
>>> tree_root = ExpressionTreeNode.build_tree(
...     ['A', 'B', 'or',
...      'C', 'D', 'and',
...      'iff'])
>>> BooleanExpression(tree_root)
<BooleanExpression "(A or B) iff (C and D)">

Additionally, any sub-tree node can be used to build an expression object. Continuing from above, let’s make a new expression object for each of the sub-expressions wrapped in parentheses:

>>> BooleanExpression(tree_root.l_child)
<BooleanExpression "A or B">
>>> BooleanExpression(tree_root.r_child)
<BooleanExpression "C and D">

Expressions also implement the equality and inequality operators (== and !=). Equality is determined by the same semantic structure and the same operand names; the string used to represent the operators in two expressions is not taken into account. Here’s a few examples:

>>> from tt import BooleanExpression as be
>>> be('A or B or C') == be('A or B or C')
True
>>> be('A or B or C') == be('A || B || C')
True
>>> be('A or B or C') == be('A or C or B')
False
Parameters:

expr (str or ExpressionTreeNode) – The expression representation from which this object is derived.

Raises:

It is important to note that aside from InvalidArgumentTypeError, all exceptions raised in expression initialization will be descendants of GrammarError.

__eq__(other)[source]

Return self==value.

__init__(expr)[source]

Initialize self. See help(type(self)) for accurate signature.

__ne__(other)[source]

Return self!=value.

__repr__()[source]

Return repr(self).

__str__()[source]

Return str(self).

constrain(**kwargs)[source]

A context manager to impose satisfiability constraints.

This is the interface for adding assumptions to the satisfiability solving functionality provided through the sat_one() and sat_all() methods.

It should be noted that this context manager is only designed to work with the satisfiability-related functionality of this class. Constrained symbol values will not have an effect on non-sat methods of this class. For example:

>>> from tt import BooleanExpression
>>> b = BooleanExpression('(A or B) and (C or D)')
>>> with b.constrain(A=1):
...     b.evaluate(A=0, B=1, C=1, D=0)
...
True

This context manager returns a reference to the same object upon which it is called. This behavior is designed with the following use case in mind:

>>> from tt import BooleanExpression
>>> with BooleanExpression('A or B').constrain(A=1, B=0) as b:
...     b.sat_one()
...
<BooleanValues [A=1, B=0]>
Parameters:

kwargs – Keys are names of symbols in this expression; the specified value for each of these keys will be added to the constraints attribute of this object for the duration of the context manager.

Returns:

A reference to the same object that called this method (i.e., self in the context of this method).

Return type:

BooleanExpression

Raises:
evaluate(**kwargs)[source]

Evaluate the Boolean expression for the passed keyword arguments.

This is a checked wrapper around the evaluate_unchecked() function.

Parameters:

kwargs – Keys are names of symbols in this expression; the specified value for each of these keys will be substituted into the expression for evaluation.

Returns:

The result of evaluating the expression.

Return type:

bool

Raises:

Usage:

>>> from tt import BooleanExpression
>>> b = BooleanExpression('A or B')
>>> b.evaluate(A=0, B=0)
False
>>> b.evaluate(A=1, B=0)
True
evaluate_unchecked(**kwargs)[source]

Evaluate the Boolean expression without checking the input.

This is used for evaluation by the evaluate() method, which validates the input kwargs before passing them to this method.

Parameters:kwargs – Keys are names of symbols in this expression; the specified value for each of these keys will be substituted into the expression for evaluation.
Returns:The Boolean result of evaluating the expression.
Return type:bool
is_cnf

Whether this expression is in conjunctive norma form or not.

Type:bool
>>> from tt import BooleanExpression
>>> b = BooleanExpression('(A or ~B) and (~C or D or E) and F')
>>> b.is_cnf
True
>>> b = BooleanExpression('A nand B')
>>> b.is_cnf
False
is_dnf

Whether this expression is in conjunctive normal form or not.

Type:bool
>>> from tt import BooleanExpression
>>> b = BooleanExpression('(A and B) or (~C and D)')
>>> b.is_dnf
True
>>> b = BooleanExpression('(op1 or !op2) and (op3 or op4)')
>>> b.is_dnf
False
iter_clauses()[source]

Iterate over the clauses in this expression.

An expression must be in conjunctive normal form (CNF) or disjunctive normal form (DNF) in order to iterate over its clauses. Here’s a simple example:

>>> from tt import BooleanExpression
>>> b = BooleanExpression('(~A or B) and (C or D) and (~E or ~F)')
>>> for clause in b.iter_clauses():
...     clause
...
<BooleanExpression "~A or B">
<BooleanExpression "C or D">
<BooleanExpression "~E or ~F">

In the case of an ambiguous expression form (between CNF and DNF), the clauses will be interpreted to be in CNF form. For example:

>>> b = BooleanExpression('A and ~B and C')
>>> b.is_cnf
True
>>> b.is_dnf
True
>>> print(', '.join(str(clause) for clause in b.iter_clauses()))
A, ~B, C

If you want to enforce a specific CNF or DNF interpretation of the clauses, take a look at iter_cnf_clauses() and iter_dnf_clauses().

Returns:An iterator of expression objects, each representing a separate clause of this expression.
Return type:Iterator[BooleanExpression]
Raises:RequiresNormalFormError – If this expression is not in conjunctive or disjunctive normal form.
iter_cnf_clauses()[source]

Iterate over the CNF clauses in this expression.

>>> from tt import BooleanExpression
>>> b = BooleanExpression('(A or B) and ~C')
>>> for clause in b.iter_cnf_clauses():
...     print(clause)
...
A or B
~C
Returns:An iterator of expression objects, each representing a separate CNF clause of this expression.
Return type:Iterator[BooleanExpression]
Raises:RequiresNormalFormError – If this expression is not in conjunctive normal form.
iter_dnf_clauses()[source]

Iterate over the DNF clauses in this expression.

>>> from tt import BooleanExpression
>>> b = BooleanExpression('(A and ~B) or (C and D and E)')
>>> for clause in b.iter_dnf_clauses():
...     print(clause)
...
A and ~B
C and D and E
Returns:An iterator of expression objects, each representing a separate DNF clause of this expression.
Return type:Iterator[BooleanExpression]
Raises:RequiresNormalFormError – If this expression is not in disjunctive normal form.
postfix_tokens

Similar to the tokens attribute, but in postfix order.

Type:List[str]
>>> from tt import BooleanExpression
>>> b = BooleanExpression('A xor (B or C)')
>>> b.postfix_tokens
['A', 'B', 'C', 'or', 'xor']
raw_expr

The raw string expression, parsed upon initialization.

This is what you pass into the BooleanExpression constructor; it is kept on the object as an attribute for convenience.

Type:str
>>> from tt import BooleanExpression
>>> b = BooleanExpression('A nand B')
>>> b.raw_expr
'A nand B'
sat_all()[source]

Find all combinations of inputs that satisfy this expression.

Under the hood, this method is using the functionality exposed in tt’s satisfiability.picosat module.

Here’s a simple example of iterating through a few SAT solutions:

>>> from tt import BooleanExpression
>>> b = BooleanExpression('(A xor B) and (C xor D)')
>>> for solution in b.sat_all():
...     print(solution)
...
A=1, B=0, C=1, D=0
A=1, B=0, C=0, D=1
A=0, B=1, C=0, D=1
A=0, B=1, C=1, D=0

We can also constrain away a few of those solutions:

>>> with b.constrain(A=1, C=0):
...     for solution in b.sat_all():
...         print(solution)
...
A=1, B=0, C=0, D=1
Returns:An iterator of namedtuple-like objects representing satisfying combinations of inputs; if no satisfying solutions exist, the iterator will be empty.
Return type:Iterator[namedtuple -like objects]
Raises:NoEvaluationVariationError – If this is an expression of only constants.
sat_one()[source]

Find a combination of inputs that satisfies this expression.

Under the hood, this method is using the functionality exposed in tt’s satisfiability.picosat module.

Here’s a simple example of satisfying an expression:

>>> from tt import BooleanExpression
>>> b = BooleanExpression('A xor 1')
>>> b.sat_one()
<BooleanValues [A=0]>

Don’t forget about the utility provided by the constrain() context manager:

>>> b = BooleanExpression('(A nand B) iff C')
>>> with b.constrain(A=1, C=1):
...     b.sat_one()
...
<BooleanValues [A=1, B=0, C=1]>

Finally, here’s an example when the expression cannot be satisfied:

>>> with BooleanExpression('A xor 1').constrain(A=1) as b:
...     b.sat_one() is None
...
True
Returns:namedtuple-like object representing a satisfying set of values (see boolean_variables_factory for more information about the type of object returned); None will be returned if no satisfiable set of inputs exists.
Return type:namedtuple-like object or None
Raises:NoEvaluationVariationError – If this is an expression of only constants.
symbols

The list of unique symbols present in this expression.

The order of the symbols in this list matches the order of symbol appearance in the original expression.

Type:List[str]
>>> from tt import BooleanExpression
>>> b = BooleanExpression('A xor (B or C)')
>>> b.symbols
['A', 'B', 'C']
tokens

The parsed, non-whitespace tokens of an expression.

Type:List[str]
>>> from tt import BooleanExpression
>>> b = BooleanExpression('A xor (B or C)')
>>> b.tokens
['A', 'xor', '(', 'B', 'or', 'C', ')']
tree

The tree node representing the root of the tree of this expression.

Type:ExpressionTreeNode
>>> from tt import BooleanExpression
>>> b = BooleanExpression('A xor (B or C)')
>>> print(b.tree)
xor
`----A
`----or
     `----B
     `----C