wmpy.core.weights.Weights¶

class Weights(weight_func, env)[source]¶

Bases: object

This class encodes a piecewise weight function.

weight_func¶: the weight function in pysmt format

env¶: the pysmt environment

atoms_finder¶: TODO: add a bit of documentation for this

evaluator¶: internal class for function evaluation

Default constructor.

Parameters:

weight_func (FNode) – the pysmt expression representing the weight function
env (Environment) – the pysmt environment

Methods

`compute_skeleton`	Computes the "skeleton", a SMT formula that encodes the structure of the weight function.
`get_atoms`	Returns the atoms contained in the (conditions of the) weight expressions.
`weight_from_assignment`	Evaluates the weight function given a total truth assignment to its conditions.

compute_skeleton()[source]¶

Computes the “skeleton”, a SMT formula that encodes the structure of the weight function. Conjoining the skeleton with the support formula can be advantageous when using partial enumeration.

Return type:: FNode
Returns:: A pysmt formula that encodes the structure of the weight.

get_atoms()[source]¶

Returns the atoms contained in the (conditions of the) weight expressions.

Return type:: Collection[FNode]

weight_from_assignment(assignment)[source]¶

Evaluates the weight function given a total truth assignment to its conditions.

Parameters:: assignment (dict[FNode, bool]) – the truth assignment as returned by an Enumerator
Return type:: FNode
Returns:: A pysmt term that correspond to unconditional weight function obtained by assigning a truth value to the conditions.
Raises:: ValueError if the TA is not total. –