wmpy.core.assignmentconverter.AssignmentConverter

class AssignmentConverter(enumerator)

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

Methods

convert

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

convert(truth_assignment, domain)

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

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

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.