probably.pysmt

Probably contains some utility functions to translate parts of a pGCL program to pySMT.

Translation Context

The translation of pGCL programs to pySMT requires a few details to be known: How to translate variables to pySMT, how to handle infinities, and so on. The TranslationContext handles all that.

class probably.pysmt.context.TranslationContext(variables, infinity=None, id_subst=None)[source]

Context used for translation of pGCL parts.

Parameters:
variables: Dict[str, FNode]
infinity: FNode
id_subst: Dict[FNode, FNode]
static from_program(program)[source]

Create a new TranslationContext from a pGCL program’s declared variables.

Parameters:

program (Program) –

Return type:

TranslationContext

Expression Translation

Translation of pGCL expressions to pySMT formulas.

probably.pysmt.expr.expr_to_pysmt(context, expr, *, is_expectation=False, allow_infinity=False)[source]

Translate a pGCL expression to a pySMT formula.

Note that substitution expressions are not allowed here (they are not supported in pySMT).

You can pass in the optional is_expectation parameter to have all integer values converted to real values.

If allow_infinity is True, then infinity expressions will be mapped directly to the infinity variable of the given TranslationContext. Take care to appropriately constrain the infinity variable! Note that arithmetic expressions may not contain infinity, to prevent expressions like infinity - infinity.

>>> from probably.pgcl.parser import parse_expr
>>> from pysmt.shortcuts import Symbol
>>> from pysmt.typing import INT

>>> expr = parse_expr("x + 4 * 13")
>>> context = TranslationContext({"x": Symbol("x", INT)})
>>> expr_to_pysmt(context, expr)
(x + (4 * 13))
Parameters:
Return type:

FNode