stormvogel.parametric.sympy_backend¶

Sympy implementation of the parametric backend.

Registers itself on import. Works whether or not pycarl / stormpy is available: the pycarl bridge methods import stormpy.pycarl lazily and only when called.

Classes¶

SympyBackend

Sympy-backed ParametricBackend.

Functions¶

`_is_zero_sympy`(→ bool)
`_free_symbol_names_sympy`(→ set[str])
`_degree_sympy`(→ int)
`_evaluate_sympy`(value, values)
`_numden_sympy`(→ tuple[sympy.Expr, sympy.Expr])
`_to_str_sympy`(→ str)

Module Contents¶

stormvogel.parametric.sympy_backend._is_zero_sympy(value: sympy.Expr) → bool¶

stormvogel.parametric.sympy_backend._free_symbol_names_sympy(value: sympy.Expr) → set[str]¶

stormvogel.parametric.sympy_backend._degree_sympy(value: sympy.Expr) → int¶

stormvogel.parametric.sympy_backend._evaluate_sympy(value: sympy.Expr, values: dict[str, stormvogel.parametric._backend.Number])¶

stormvogel.parametric.sympy_backend._numden_sympy(value: sympy.Expr) → tuple[sympy.Expr, sympy.Expr]¶

stormvogel.parametric.sympy_backend._to_str_sympy(value: sympy.Expr) → str¶

class stormvogel.parametric.sympy_backend.SympyBackend¶

Sympy-backed ParametricBackend.

name = 'sympy'¶

expr_types: tuple[type, Ellipsis]¶

symbol(name: str, **kwargs: Any) → sympy.Symbol¶

constant(n: stormvogel.parametric._backend.Number) → sympy.Expr¶

to_pycarl(value: Any, var_map: dict[str, Any]) → Any¶

Convert a sp.Expr into a pycarl factorized rational function, reusing the pycarl Variables in var_map.

var_map must be an ordered mapping (insertion order matters): we take its values as the polynomial-variable ordering, so that exponent tuples produced by sympy.Poly.terms() line up with the pycarl variable map.

static _poly_to_pycarl(expr: sympy.Expr, var_map: dict[str, Any]) → Any¶: Build a pycarl polynomial from a sympy polynomial expression, using the pycarl Variables in var_map in insertion order.

from_pycarl(pycarl_value: Any) → sympy.Expr¶

Convert a pycarl FactorizedRationalFunction (or bare RationalFunction / Polynomial) into a sp.Expr.

When the denominator is constant 1 and the numerator is constant, the plain Python number is returned instead so downstream code can treat it as a Number first-class.