Pycarl core¶

Number independent types¶

class BoundType¶

Members:

STRICT

WEAK

INFTY

INFTY = <BoundType.INFTY: 2>¶

STRICT = <BoundType.STRICT: 0>¶

WEAK = <BoundType.WEAK: 1>¶

property name¶

property value¶

class Interval¶

abs(self: stormpy.pycarl.pycarl_core.Interval) → stormpy.pycarl.pycarl_core.Interval¶

center(self: stormpy.pycarl.pycarl_core.Interval) → float¶

complement(self: stormpy.pycarl.pycarl_core.Interval, arg0: stormpy.pycarl.pycarl_core.Interval, arg1: stormpy.pycarl.pycarl_core.Interval) → bool¶

contains(*args, **kwargs)¶

Overloaded function.

contains(self: stormpy.pycarl.pycarl_core.Interval, arg0: float) -> bool
contains(self: stormpy.pycarl.pycarl_core.Interval, arg0: stormpy.pycarl.pycarl_core.Interval) -> bool

diameter(self: stormpy.pycarl.pycarl_core.Interval) → float¶

difference(self: stormpy.pycarl.pycarl_core.Interval, arg0: stormpy.pycarl.pycarl_core.Interval, arg1: stormpy.pycarl.pycarl_core.Interval, arg2: stormpy.pycarl.pycarl_core.Interval) → bool¶

div(self: stormpy.pycarl.pycarl_core.Interval, arg0: stormpy.pycarl.pycarl_core.Interval) → stormpy.pycarl.pycarl_core.Interval¶

static emptyInterval() → stormpy.pycarl.pycarl_core.Interval¶

integralPart(self: stormpy.pycarl.pycarl_core.Interval) → stormpy.pycarl.pycarl_core.Interval¶

intersect(self: stormpy.pycarl.pycarl_core.Interval, arg0: stormpy.pycarl.pycarl_core.Interval) → stormpy.pycarl.pycarl_core.Interval¶

intersectsWith(self: stormpy.pycarl.pycarl_core.Interval, arg0: stormpy.pycarl.pycarl_core.Interval) → bool¶

inverse(self: stormpy.pycarl.pycarl_core.Interval) → stormpy.pycarl.pycarl_core.Interval¶

isClosedInterval(self: stormpy.pycarl.pycarl_core.Interval) → bool¶

isEmpty(self: stormpy.pycarl.pycarl_core.Interval) → bool¶

isHalfBounded(self: stormpy.pycarl.pycarl_core.Interval) → bool¶

isInfinite(self: stormpy.pycarl.pycarl_core.Interval) → bool¶

isNegative(self: stormpy.pycarl.pycarl_core.Interval) → bool¶

isOne(self: stormpy.pycarl.pycarl_core.Interval) → bool¶

isOpenInterval(self: stormpy.pycarl.pycarl_core.Interval) → bool¶

isPointInterval(self: stormpy.pycarl.pycarl_core.Interval) → bool¶

isPositive(self: stormpy.pycarl.pycarl_core.Interval) → bool¶

isProperSubset(self: stormpy.pycarl.pycarl_core.Interval, arg0: stormpy.pycarl.pycarl_core.Interval) → bool¶

isSemiNegative(self: stormpy.pycarl.pycarl_core.Interval) → bool¶

isSemiPositive(self: stormpy.pycarl.pycarl_core.Interval) → bool¶

isSubset(self: stormpy.pycarl.pycarl_core.Interval, arg0: stormpy.pycarl.pycarl_core.Interval) → bool¶

isUnbounded(self: stormpy.pycarl.pycarl_core.Interval) → bool¶

isZero(self: stormpy.pycarl.pycarl_core.Interval) → bool¶

lower(self: stormpy.pycarl.pycarl_core.Interval) → float¶

meets(self: stormpy.pycarl.pycarl_core.Interval, arg0: float) → bool¶

sample(self: stormpy.pycarl.pycarl_core.Interval, arg0: bool) → float¶

setLower(self: stormpy.pycarl.pycarl_core.Interval, arg0: float) → None¶

setUpper(self: stormpy.pycarl.pycarl_core.Interval, arg0: float) → None¶

symmetricDifference(self: stormpy.pycarl.pycarl_core.Interval, arg0: stormpy.pycarl.pycarl_core.Interval, arg1: stormpy.pycarl.pycarl_core.Interval, arg2: stormpy.pycarl.pycarl_core.Interval) → bool¶

static unboundedInterval() → stormpy.pycarl.pycarl_core.Interval¶

unite(self: stormpy.pycarl.pycarl_core.Interval, arg0: stormpy.pycarl.pycarl_core.Interval, arg1: stormpy.pycarl.pycarl_core.Interval, arg2: stormpy.pycarl.pycarl_core.Interval) → bool¶

upper(self: stormpy.pycarl.pycarl_core.Interval) → float¶

static zeroInterval() → stormpy.pycarl.pycarl_core.Interval¶

class Monomial¶

property exponents¶

property tdeg¶

exception NoPicklingSupport¶

class Variable¶

property id¶

property is_no_variable¶

property name¶

property rank¶

property type¶

class VariableType¶

Members:

BOOL

INT

REAL

BOOL = <VariableType.BOOL: 0>¶

INT = <VariableType.INT: 2>¶

REAL = <VariableType.REAL: 1>¶

property name¶

property value¶

abs(arg0: stormpy.pycarl.pycarl_core.Interval) → stormpy.pycarl.pycarl_core.Interval¶

carl_version()¶: Get Carl version. :return: Version of Carl.

ceil(arg0: stormpy.pycarl.pycarl_core.Interval) → stormpy.pycarl.pycarl_core.Interval¶

clear_monomial_pool() → None¶: Clear monomial pool and remove all monomials

clear_pools()¶: Clear all pools.

clear_variable_pool() → None¶: Clear variable pool and remove all variables

create_monomial(variable: stormpy.pycarl.pycarl_core.Variable, exponent: int) → stormpy.pycarl.pycarl_core.Monomial¶: Create monomial

div(arg0: stormpy.pycarl.pycarl_core.Interval, arg1: stormpy.pycarl.pycarl_core.Interval) → stormpy.pycarl.pycarl_core.Interval¶

floor(arg0: stormpy.pycarl.pycarl_core.Interval) → stormpy.pycarl.pycarl_core.Interval¶

has_cln()¶: Check if pycarl has support for CLN. :return: True iff CLN is supported.

has_parser()¶: Check if pycarl has parsing support. :return: True iff parsing is supported.

isInteger(arg0: stormpy.pycarl.pycarl_core.Interval) → bool¶

pow(arg0: stormpy.pycarl.pycarl_core.Interval, arg1: int) → stormpy.pycarl.pycarl_core.Interval¶

print_info()¶: Print information about pycarl.

quotient(arg0: stormpy.pycarl.pycarl_core.Interval, arg1: stormpy.pycarl.pycarl_core.Interval) → stormpy.pycarl.pycarl_core.Interval¶

variable_with_name(arg0: str) → stormpy.pycarl.pycarl_core.Variable¶: Get a variable from the pool with the given name.

Number dependent types (gmp)¶

class Factorization¶

class FactorizedPolynomial¶

Represent a polynomial with its factorization

cache(self: stormpy.pycarl.gmp.FactorizedPolynomial) → stormpy.pycarl.gmp._FactorizationCache¶

property coefficient¶

constant_part(self: stormpy.pycarl.gmp.FactorizedPolynomial) → stormpy.pycarl.gmp.Rational¶

derive(self: stormpy.pycarl.gmp.FactorizedPolynomial, variable: stormpy.pycarl.pycarl_core.Variable) → stormpy.pycarl.gmp.FactorizedPolynomial¶: Compute the derivative

evaluate(self: stormpy.pycarl.gmp.FactorizedPolynomial, arg0: Dict[stormpy.pycarl.pycarl_core.Variable, stormpy.pycarl.gmp.Rational]) → stormpy.pycarl.gmp.Rational¶

factorization(self: stormpy.pycarl.gmp.FactorizedPolynomial) → stormpy.pycarl.gmp.Factorization¶: Get factorization

gather_variables(self: stormpy.pycarl.gmp.FactorizedPolynomial) → Set[stormpy.pycarl.pycarl_core.Variable]¶

is_constant(self: stormpy.pycarl.gmp.FactorizedPolynomial) → bool¶

is_one(self: stormpy.pycarl.gmp.FactorizedPolynomial) → bool¶

polynomial(self: stormpy.pycarl.gmp.FactorizedPolynomial) → stormpy.pycarl.gmp.Polynomial¶: Get underlying polynomial

to_smt2(self: stormpy.pycarl.gmp.FactorizedPolynomial) → str¶

class FactorizedRationalFunction¶

Represent a rational function, that is the fraction of two factorized polynomials

constant_part(self: stormpy.pycarl.gmp.FactorizedRationalFunction) → stormpy.pycarl.gmp.Rational¶

property denominator¶

derive(self: stormpy.pycarl.gmp.FactorizedRationalFunction, variable: stormpy.pycarl.pycarl_core.Variable) → stormpy.pycarl.gmp.FactorizedRationalFunction¶: Compute the derivative

evaluate(self: stormpy.pycarl.gmp.FactorizedRationalFunction, arg0: Dict[stormpy.pycarl.pycarl_core.Variable, stormpy.pycarl.gmp.Rational]) → stormpy.pycarl.gmp.Rational¶

gather_variables(self: stormpy.pycarl.gmp.FactorizedRationalFunction) → Set[stormpy.pycarl.pycarl_core.Variable]¶

is_constant(self: stormpy.pycarl.gmp.FactorizedRationalFunction) → bool¶

property numerator¶

rational_function(self: stormpy.pycarl.gmp.FactorizedRationalFunction) → stormpy.pycarl.gmp.RationalFunction¶

to_smt2(self: stormpy.pycarl.gmp.FactorizedRationalFunction) → str¶

class Integer¶: Class wrapping gmp-integers

class Interval¶

abs(self: stormpy.pycarl.gmp.Interval) → stormpy.pycarl.gmp.Interval¶

center(self: stormpy.pycarl.gmp.Interval) → stormpy.pycarl.gmp.Rational¶

complement(self: stormpy.pycarl.gmp.Interval, arg0: stormpy.pycarl.gmp.Interval, arg1: stormpy.pycarl.gmp.Interval) → bool¶

contains(*args, **kwargs)¶

Overloaded function.

contains(self: stormpy.pycarl.gmp.Interval, arg0: stormpy.pycarl.gmp.Rational) -> bool
contains(self: stormpy.pycarl.gmp.Interval, arg0: stormpy.pycarl.gmp.Interval) -> bool

diameter(self: stormpy.pycarl.gmp.Interval) → stormpy.pycarl.gmp.Rational¶

difference(self: stormpy.pycarl.gmp.Interval, arg0: stormpy.pycarl.gmp.Interval, arg1: stormpy.pycarl.gmp.Interval, arg2: stormpy.pycarl.gmp.Interval) → bool¶

div(self: stormpy.pycarl.gmp.Interval, arg0: stormpy.pycarl.gmp.Interval) → stormpy.pycarl.gmp.Interval¶

static emptyInterval() → stormpy.pycarl.gmp.Interval¶

integralPart(self: stormpy.pycarl.gmp.Interval) → stormpy.pycarl.gmp.Interval¶

intersect(self: stormpy.pycarl.gmp.Interval, arg0: stormpy.pycarl.gmp.Interval) → stormpy.pycarl.gmp.Interval¶

intersectsWith(self: stormpy.pycarl.gmp.Interval, arg0: stormpy.pycarl.gmp.Interval) → bool¶

inverse(self: stormpy.pycarl.gmp.Interval) → stormpy.pycarl.gmp.Interval¶

isClosedInterval(self: stormpy.pycarl.gmp.Interval) → bool¶

isEmpty(self: stormpy.pycarl.gmp.Interval) → bool¶

isHalfBounded(self: stormpy.pycarl.gmp.Interval) → bool¶

isInfinite(self: stormpy.pycarl.gmp.Interval) → bool¶

isNegative(self: stormpy.pycarl.gmp.Interval) → bool¶

isOne(self: stormpy.pycarl.gmp.Interval) → bool¶

isOpenInterval(self: stormpy.pycarl.gmp.Interval) → bool¶

isPointInterval(self: stormpy.pycarl.gmp.Interval) → bool¶

isPositive(self: stormpy.pycarl.gmp.Interval) → bool¶

isProperSubset(self: stormpy.pycarl.gmp.Interval, arg0: stormpy.pycarl.gmp.Interval) → bool¶

isSemiNegative(self: stormpy.pycarl.gmp.Interval) → bool¶

isSemiPositive(self: stormpy.pycarl.gmp.Interval) → bool¶

isSubset(self: stormpy.pycarl.gmp.Interval, arg0: stormpy.pycarl.gmp.Interval) → bool¶

isUnbounded(self: stormpy.pycarl.gmp.Interval) → bool¶

isZero(self: stormpy.pycarl.gmp.Interval) → bool¶

lower(self: stormpy.pycarl.gmp.Interval) → stormpy.pycarl.gmp.Rational¶

meets(self: stormpy.pycarl.gmp.Interval, arg0: stormpy.pycarl.gmp.Rational) → bool¶

sample(self: stormpy.pycarl.gmp.Interval, arg0: bool) → stormpy.pycarl.gmp.Rational¶

setLower(self: stormpy.pycarl.gmp.Interval, arg0: stormpy.pycarl.gmp.Rational) → None¶

setUpper(self: stormpy.pycarl.gmp.Interval, arg0: stormpy.pycarl.gmp.Rational) → None¶

symmetricDifference(self: stormpy.pycarl.gmp.Interval, arg0: stormpy.pycarl.gmp.Interval, arg1: stormpy.pycarl.gmp.Interval, arg2: stormpy.pycarl.gmp.Interval) → bool¶

static unboundedInterval() → stormpy.pycarl.gmp.Interval¶

unite(self: stormpy.pycarl.gmp.Interval, arg0: stormpy.pycarl.gmp.Interval, arg1: stormpy.pycarl.gmp.Interval, arg2: stormpy.pycarl.gmp.Interval) → bool¶

upper(self: stormpy.pycarl.gmp.Interval) → stormpy.pycarl.gmp.Rational¶

static zeroInterval() → stormpy.pycarl.gmp.Interval¶

class Polynomial¶

Represent a multivariate polynomial

constant_part(self: stormpy.pycarl.gmp.Polynomial) → stormpy.pycarl.gmp.Rational¶

degree(self: stormpy.pycarl.gmp.Polynomial, arg0: stormpy.pycarl.pycarl_core.Variable) → int¶

derive(self: stormpy.pycarl.gmp.Polynomial, variable: stormpy.pycarl.pycarl_core.Variable) → stormpy.pycarl.gmp.Polynomial¶: Compute the derivative

evaluate(self: stormpy.pycarl.gmp.Polynomial, arg0: Dict[stormpy.pycarl.pycarl_core.Variable, stormpy.pycarl.gmp.Rational]) → stormpy.pycarl.gmp.Rational¶

gather_variables(self: stormpy.pycarl.gmp.Polynomial) → Set[stormpy.pycarl.pycarl_core.Variable]¶

is_constant(self: stormpy.pycarl.gmp.Polynomial) → bool¶

property nr_terms¶

substitute(self: stormpy.pycarl.gmp.Polynomial, arg0: Dict[stormpy.pycarl.pycarl_core.Variable, stormpy.pycarl.gmp.Polynomial]) → stormpy.pycarl.gmp.Polynomial¶

to_smt2(self: stormpy.pycarl.gmp.Polynomial) → str¶

property total_degree¶

class Rational¶

Class wrapping gmp-rational numbers

property denominator¶

property nominator¶

property numerator¶

class RationalFunction¶

Represent a rational function, that is the fraction of two multivariate polynomials

constant_part(self: stormpy.pycarl.gmp.RationalFunction) → stormpy.pycarl.gmp.Rational¶

property denominator¶

derive(self: stormpy.pycarl.gmp.RationalFunction, variable: stormpy.pycarl.pycarl_core.Variable) → stormpy.pycarl.gmp.RationalFunction¶: Compute the derivative

evaluate(self: stormpy.pycarl.gmp.RationalFunction, arg0: Dict[stormpy.pycarl.pycarl_core.Variable, stormpy.pycarl.gmp.Rational]) → stormpy.pycarl.gmp.Rational¶

gather_variables(self: stormpy.pycarl.gmp.RationalFunction) → Set[stormpy.pycarl.pycarl_core.Variable]¶

is_constant(self: stormpy.pycarl.gmp.RationalFunction) → bool¶

property nominator¶

property numerator¶

to_smt2(self: stormpy.pycarl.gmp.RationalFunction) → str¶

class Term¶

property coeff¶

is_constant(self: stormpy.pycarl.gmp.Term) → bool¶

is_one(self: stormpy.pycarl.gmp.Term) → bool¶

property monomial¶

property tdeg¶

abs(arg0: stormpy.pycarl.gmp.Interval) → stormpy.pycarl.gmp.Interval¶

ceil(arg0: stormpy.pycarl.gmp.Interval) → stormpy.pycarl.gmp.Interval¶

create_factorized_polynomial(polynomial)¶

denominator(x)¶

div(arg0: stormpy.pycarl.gmp.Interval, arg1: stormpy.pycarl.gmp.Interval) → stormpy.pycarl.gmp.Interval¶

expand(x)¶

floor(arg0: stormpy.pycarl.gmp.Interval) → stormpy.pycarl.gmp.Interval¶

isInteger(arg0: stormpy.pycarl.gmp.Interval) → bool¶

numerator(x)¶

pow(arg0: stormpy.pycarl.gmp.Interval, arg1: int) → stormpy.pycarl.gmp.Interval¶

quotient(arg0: stormpy.pycarl.gmp.Interval, arg1: stormpy.pycarl.gmp.Interval) → stormpy.pycarl.gmp.Interval¶

Number dependent types (cln)¶

class Factorization¶

class FactorizedPolynomial¶

Represent a polynomial with its factorization

cache(self: stormpy.pycarl.cln.FactorizedPolynomial) → stormpy.pycarl.cln._FactorizationCache¶

property coefficient¶

constant_part(self: stormpy.pycarl.cln.FactorizedPolynomial) → stormpy.pycarl.cln.Rational¶

derive(self: stormpy.pycarl.cln.FactorizedPolynomial, variable: stormpy.pycarl.pycarl_core.Variable) → stormpy.pycarl.cln.FactorizedPolynomial¶: Compute the derivative

evaluate(self: stormpy.pycarl.cln.FactorizedPolynomial, arg0: Dict[stormpy.pycarl.pycarl_core.Variable, stormpy.pycarl.cln.Rational]) → stormpy.pycarl.cln.Rational¶

factorization(self: stormpy.pycarl.cln.FactorizedPolynomial) → stormpy.pycarl.cln.Factorization¶: Get factorization

gather_variables(self: stormpy.pycarl.cln.FactorizedPolynomial) → Set[stormpy.pycarl.pycarl_core.Variable]¶

is_constant(self: stormpy.pycarl.cln.FactorizedPolynomial) → bool¶

is_one(self: stormpy.pycarl.cln.FactorizedPolynomial) → bool¶

polynomial(self: stormpy.pycarl.cln.FactorizedPolynomial) → stormpy.pycarl.cln.Polynomial¶: Get underlying polynomial

to_smt2(self: stormpy.pycarl.cln.FactorizedPolynomial) → str¶

class FactorizedRationalFunction¶

Represent a rational function, that is the fraction of two factorized polynomials

constant_part(self: stormpy.pycarl.cln.FactorizedRationalFunction) → stormpy.pycarl.cln.Rational¶

property denominator¶

derive(self: stormpy.pycarl.cln.FactorizedRationalFunction, variable: stormpy.pycarl.pycarl_core.Variable) → stormpy.pycarl.cln.FactorizedRationalFunction¶: Compute the derivative

evaluate(self: stormpy.pycarl.cln.FactorizedRationalFunction, arg0: Dict[stormpy.pycarl.pycarl_core.Variable, stormpy.pycarl.cln.Rational]) → stormpy.pycarl.cln.Rational¶

gather_variables(self: stormpy.pycarl.cln.FactorizedRationalFunction) → Set[stormpy.pycarl.pycarl_core.Variable]¶

is_constant(self: stormpy.pycarl.cln.FactorizedRationalFunction) → bool¶

property numerator¶

rational_function(self: stormpy.pycarl.cln.FactorizedRationalFunction) → stormpy.pycarl.cln.RationalFunction¶

to_smt2(self: stormpy.pycarl.cln.FactorizedRationalFunction) → str¶

class Integer¶: Class wrapping cln-integers

class Interval¶

abs(self: stormpy.pycarl.cln.Interval) → stormpy.pycarl.cln.Interval¶

center(self: stormpy.pycarl.cln.Interval) → stormpy.pycarl.cln.Rational¶

complement(self: stormpy.pycarl.cln.Interval, arg0: stormpy.pycarl.cln.Interval, arg1: stormpy.pycarl.cln.Interval) → bool¶

contains(*args, **kwargs)¶

Overloaded function.

contains(self: stormpy.pycarl.cln.Interval, arg0: stormpy.pycarl.cln.Rational) -> bool
contains(self: stormpy.pycarl.cln.Interval, arg0: stormpy.pycarl.cln.Interval) -> bool