wmpy.solvers.wmisolver.WMISolver

class WMISolver(enumerator, domain, integrator=None)

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) – an instance of Enumerator (support, weight)

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

• integrator (Optional[Integrator]) – an Integrator instance (default: RejectionIntegrator)

Methods

compute

Computes the weighted model integral of a given query formula.

DEF_INTEGRATOR

alias of RejectionIntegrator

compute(query)

Computes the weighted model integral of a given query formula.

Parameters:

query (FNode) – the query as a pysmt formula

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