wmpy.solvers.wmisolver.WMISolver

class WMISolver(enumerator, integrator=None)[source]

Bases: object

The class implements a WMI solver based on exhaustive enumeration.

The weighted model integral is solved sequentially: 1) enumerator first computes the set of satisfiable truth assignments (TAs); 2) the TAs are converted into convex integration problems and jointly passed to the integrator of choice.

The weight and its support are contained inside the enumerator, with the AssignmentConverter being in charge of converting TAs into <Polytope, Polynomial> pairs.

Default constructor.

Parameters:

  • enumerator (Enumerator) – the enumerator to use (default: TotalEnumerator)

  • integrator (Optional[Integrator]) – the integrator to use (default: RejectionIntegrator)

Methods

compute

Computes the weighted model integral of a given query formula.
DEF_ENUMERATOR

alias of TotalEnumerator

DEF_INTEGRATOR

alias of RejectionIntegrator

compute(query, domain)[source]

Computes the weighted model integral of a given query formula.

Parameters:

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

  • domain (Collection[FNode]) – the continuous integration domain (a list of pysmt real variables)

Returns:

“wmi”: the weighted model integral as a non-negative scalar value “npolys”: the number of convex fragments enumerated

Return type:

A dictionary containing the following entries