wmpy.solvers.wmsampler.WMSampler

class WMSampler(enumerator, domain, integrator=None, seed=None)[source]

Bases: object

The class implements a sampling algorithm for weighted SMT formulas.

The algorithm is divided: 1) an offline preprocessing phase, enumerating the convex regions and computing their relative mass via WMI 2) an online sampling phase, where the information above determines the different subsamples’ sizes

Default constructor. Solves the preprocessing step by solving WMI. Uses this information for constructing a weighted strata for subsequent sampling efforts.

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: LatteIntegrator)

  • seed (Optional[int]) – the seed number (optional)

Methods

sample

Draws a sample from (support, weight) in two phases.
DEF_INTEGRATOR

alias of LattEIntegrator

sample(n_samples, max_iterations=1)[source]

Draws a sample from (support, weight) in two phases.

The subsample ratios are determined based on the strata precomputed at construction. Convex subsampling is carried over using rejection sampling.

The procedure tries to satisfy the subsample size requirement up to max_iterations, returning M <= n_samples points.

Parameters:

  • n_samples (int) – desired sample size

  • max_iterations (int) – maximum number of attempts (default: 1)

Return type:

ndarray

Returns:

A numpy array with shape (M, N).