wmpy.enumeration.total.TotalEnumerator

class TotalEnumerator(support, weight=None, env=None)[source]

Bases: object

This class implements a baseline total enumerator using the Z3 SMT solver.

Default constructor.

Parameters:

  • weights – the weight function as a pysmt term

  • support (FNode) – the support of the weight function (a pysmt formula)

  • env (Optional[Environment]) – the pysmt environment (optional)

Methods

enumerate

Enumerates (possibly partial) truth assignments for the given formula.
enumerate(query)[source]

Enumerates (possibly partial) truth assignments for the given formula.

Since the truth assignments (TA) are always total, the number of unassigned Boolean variables is always 0.

Parameters:

query (FNode) – the query (a pysmt formula)

Returns:

  • TA is a dictionary {pysmt_atom : bool} representing (partial) truth assignment

Return type:

An iterable of tuples <TA, 0> where