wmpy.enumerationΒΆ
The wmpy.enumeration submodule handles anything related to the enumeration of truth assignment of weighted SMT formulas.
It exposes:
Enumerator: a generic enumerator protocol
SAEnumerator: SOTA structure-aware partial enumerator implemented on top of the MathSAT SMT solver
TotalEnumerator: a baseline total enumerator implemented on top of the Z3 SMT solver
AsynchWrapper: an enumeration wrapper that enables asynchronous solving