wmpy.enumeration.enumerator.Enumerator

class Enumerator(*args, **kwargs)[source]

Bases: Protocol

Protocol for classes that can enumerate partial truth assignments for weighted SMT formulas.

An Enumerator always contains:

weights: the weight function (a pysmt term) support: the support of the weight function (a pysmt formula) env: the pysmt environment

An Enumerator implements the ‘enumerate’ method that, given a query SMT formula, return all the truth assignments that are consistent with both support and query. In other terms, Enumerator returns a convex partitioning of the intersection of support and query.

Methods

enumerate

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

Attributes

env

support

weights

enumerate(query)[source]

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

Since the truth assignments (TA) might be partial, the number of unassigned Boolean variables is also returned.

Note: Enumerate can return any iterable type: list, tuple, generator, iterator, etc.

Parameters:

query (FNode) – the query as a pysmt formula

Returns:

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

  • NB is a non-negative integer representing the number of unassigned Boolean variables

Return type:

An iterable of tuples <TA, NB> where