prodigy.pgcl.pysmt.expr

Expression Translation

Translation of pGCL expressions to pySMT formulas.

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 prodigy.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:

  • context (TranslationContext)

  • expr (VarExpr | BoolLitExpr | NatLitExpr | RealLitExpr | UnopExpr | BinopExpr | CategoricalExpr | SubstExpr | TickExpr | FunctionCallExpr | InferExpr | SampleExpr)

  • is_expectation (bool)

  • allow_infinity (bool)

Return type:

FNode