wmpy.core.assignmentconverter.AssignmentConverter

class AssignmentConverter(enumerator, domain)[source]

Bases: object

This class is responsible of converting the pysmt assignments returned by an enumerator into pairs <Polytope, Polynomial>.

Default constructor.

Parameters:

  • enumerator (Enumerator) – the enumerator instance

  • domain (Collection[FNode]) – list of real variables in pysmt format

Methods

convert

Converts a truth assignment (as returned by an Enumerator) into a <Polytope, Polynomial> pair.
convert(truth_assignment)[source]

Converts a truth assignment (as returned by an Enumerator) into a <Polytope, Polynomial> pair.

Parameters:

truth_assignment (dict[FNode, bool]) – mapping pysmt atoms to bool

Return type:

tuple[Polytope, Polynomial]

Returns:

A convex integration problem as a pair of instances of Polytope and Polynomial. The two represent the convex integration bounds and integrand respectively.