wmpy.enumeration.sae.SAEnumerator

class SAEnumerator(support, weight=None, env=None, max_queue_size=1)[source]

Bases: object

This class implements the Structure-Aware partial enumerator described in:

“Enhancing SMT-based Weighted Model Integration by structure awareness” (Spallitta et al., 2024).

In contrast with the baseline TotalEnumerator, this enumerator: - uses MathSAT partial WMI enumeration - accounts for the structure of the weight function (i.e. its skeleton) in order to minimize the number of truth assignment returned.

TODO: better describe the effect of ‘max_queue_size’ (wouldn’t it be more clear to have a boolean flag ‘blocking’ instead?) and why its there.

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)

  • max_queue_size (int) – maximum number of assignments to compute in parallel (optional): 1 means we will compute the assignments one by one. 0 means no limit.

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) might be partial, the number of unassigned Boolean variables is also returned.

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