wmpy.core.inequality.Inequality

class Inequality(expr, parser)

Bases: object

Internal class for inequalities in the canonical form:

P {<,<=} 0

where P is a degree 1 polynomial.

strict

boolean flag, true when the inequality is <

mgr

pysmt formula manager

polynomial

the Polynomial P

Default constructor.

Parameters:

• expr (FNode) – the inequality in pysmt format

• parser (PolynomialParser) – a polynomial parser instance

Methods

to_numpy	Converts the inequality in numpy format:
to_pysmt	Converts the inequality in pysmt format.

to_numpy()

Converts the inequality in numpy format:

A {<=,<} b

Return type:

tuple[ndarray, float]

Returns:

A numpy array A, a scalar b

to_pysmt()

Converts the inequality in pysmt format.

Return type:

FNode

Returns:

Either a LT (less-than) or LE (less-or-equal-than) atom.