Pycarl core

Number independent types

class BoundType(self: stormpy.pycarl._pycarl_core.BoundType, value: SupportsInt)

Members:

STRICT

WEAK

INFTY

INFTY = <BoundType.INFTY: 2>

STRICT = <BoundType.STRICT: 0>

WEAK = <BoundType.WEAK: 1>

property name

property value

class Interval(*args, **kwargs)

Overloaded function.

1. __init__(self: stormpy.pycarl._pycarl_core.Interval, arg0: typing.SupportsFloat) -> None

2. __init__(self: stormpy.pycarl._pycarl_core.Interval, arg0: typing.SupportsFloat, arg1: typing.SupportsFloat) -> None

3. __init__(self: stormpy.pycarl._pycarl_core.Interval, arg0: typing.SupportsFloat, arg1: stormpy.pycarl._pycarl_core.BoundType, arg2: typing.SupportsFloat, arg3: stormpy.pycarl._pycarl_core.BoundType) -> None

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.

1. contains(self: stormpy.pycarl._pycarl_core.Interval, arg0: typing.SupportsFloat) -> bool

2. 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: SupportsFloat) → bool

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

setLower(self: stormpy.pycarl._pycarl_core.Interval, arg0: SupportsFloat) → None

setUpper(self: stormpy.pycarl._pycarl_core.Interval, arg0: SupportsFloat) → 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(*args, **kwargs)

Overloaded function.

1. __init__(self: stormpy.pycarl._pycarl_core.Variable, other: stormpy.pycarl._pycarl_core.Variable) -> None

2. __init__(self: stormpy.pycarl._pycarl_core.Variable, name: str, type: stormpy.pycarl._pycarl_core.VariableType = <VariableType.REAL: 1>) -> None

3. __init__(self: stormpy.pycarl._pycarl_core.Variable, type: stormpy.pycarl._pycarl_core.VariableType = <VariableType.REAL: 1>) -> None

property id

property is_no_variable

property name

property rank

property type

class VariableType(self: stormpy.pycarl._pycarl_core.VariableType, value: SupportsInt)

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_parser_directory() → str | None

Return the carl-parser directory which is used by stormpy, or None if carl parser is not available.

Returns:

Carl-parser directory.

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: SupportsInt) → 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: SupportsInt) → 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(*args, **kwargs)

Represent a polynomial with its factorization

Overloaded function.

1. __init__(self: stormpy.pycarl.gmp.FactorizedPolynomial, number: stormpy.pycarl.gmp.Rational) -> None

Constructor

2. __init__(self: stormpy.pycarl.gmp.FactorizedPolynomial, polynomial: stormpy.pycarl.gmp.Polynomial, cache: stormpy.pycarl.gmp._FactorizationCache) -> None

Constructor

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: collections.abc.Mapping[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(*args, **kwargs)

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

Overloaded function.

1. __init__(self: stormpy.pycarl.gmp.FactorizedRationalFunction, arg0: stormpy.pycarl.gmp.FactorizedPolynomial) -> None

2. __init__(self: stormpy.pycarl.gmp.FactorizedRationalFunction, arg0: stormpy.pycarl.gmp.FactorizedPolynomial, arg1: stormpy.pycarl.gmp.FactorizedPolynomial) -> None

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: collections.abc.Mapping[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(*args, **kwargs)

Class wrapping gmp-integers

Overloaded function.

1. __init__(self: stormpy.pycarl.gmp.Integer, arg0: typing.SupportsInt) -> None

2. __init__(self: stormpy.pycarl.gmp.Integer, arg0: str) -> None

3. __init__(self: stormpy.pycarl.gmp.Integer, arg0: stormpy.pycarl.cln.Integer) -> None

class Interval(*args, **kwargs)

Overloaded function.

1. __init__(self: stormpy.pycarl.gmp.Interval, arg0: stormpy.pycarl.gmp.Rational) -> None

2. __init__(self: stormpy.pycarl.gmp.Interval, arg0: stormpy.pycarl.gmp.Rational, arg1: stormpy.pycarl.gmp.Rational) -> None

3. __init__(self: stormpy.pycarl.gmp.Interval, arg0: stormpy.pycarl.gmp.Rational, arg1: stormpy.pycarl._pycarl_core.BoundType, arg2: stormpy.pycarl.gmp.Rational, arg3: stormpy.pycarl._pycarl_core.BoundType) -> None

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.

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

2. 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(*args, **kwargs)

Represent a multivariate polynomial

Overloaded function.

1. __init__(self: stormpy.pycarl.gmp.Polynomial, arg0: stormpy.pycarl.gmp.Term) -> None

2. __init__(self: stormpy.pycarl.gmp.Polynomial, arg0: stormpy.pycarl._pycarl_core.Monomial) -> None

3. __init__(self: stormpy.pycarl.gmp.Polynomial, arg0: stormpy.pycarl._pycarl_core.Variable) -> None

4. __init__(self: stormpy.pycarl.gmp.Polynomial, arg0: stormpy.pycarl.gmp.Rational) -> None

5. __init__(self: stormpy.pycarl.gmp.Polynomial, arg0: collections.abc.Sequence[stormpy.pycarl.gmp.Term]) -> None

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: collections.abc.Mapping[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: collections.abc.Mapping[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(*args, **kwargs)

Class wrapping gmp-rational numbers

Overloaded function.

1. __init__(self: stormpy.pycarl.gmp.Rational, arg0: typing.SupportsFloat) -> None

2. __init__(self: stormpy.pycarl.gmp.Rational, arg0: typing.SupportsInt) -> None

3. __init__(self: stormpy.pycarl.gmp.Rational, arg0: stormpy.pycarl.gmp.Integer, arg1: stormpy.pycarl.gmp.Integer) -> None

4. __init__(self: stormpy.pycarl.gmp.Rational, arg0: str) -> None

5. __init__(self: stormpy.pycarl.gmp.Rational, arg0: stormpy.pycarl.cln.Rational) -> None

property denominator

property nominator

property numerator

class RationalFunction(*args, **kwargs)

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

Overloaded function.

1. __init__(self: stormpy.pycarl.gmp.RationalFunction, arg0: stormpy.pycarl._pycarl_core.Variable) -> None

2. __init__(self: stormpy.pycarl.gmp.RationalFunction, arg0: stormpy.pycarl.gmp.Polynomial) -> None

3. __init__(self: stormpy.pycarl.gmp.RationalFunction, arg0: stormpy.pycarl.gmp.Polynomial, arg1: stormpy.pycarl.gmp.Polynomial) -> None

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: collections.abc.Mapping[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(*args, **kwargs)

Overloaded function.

1. __init__(self: stormpy.pycarl.gmp.Term, arg0: stormpy.pycarl.gmp.Rational, arg1: stormpy.pycarl._pycarl_core.Monomial) -> None

2. __init__(self: stormpy.pycarl.gmp.Term, arg0: stormpy.pycarl._pycarl_core.Variable) -> None

3. __init__(self: stormpy.pycarl.gmp.Term, arg0: stormpy.pycarl.gmp.Rational) -> None

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: SupportsInt) → 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(*args, **kwargs)

Represent a polynomial with its factorization

Overloaded function.

1. __init__(self: stormpy.pycarl.cln.FactorizedPolynomial, number: stormpy.pycarl.cln.Rational) -> None

Constructor

2. __init__(self: stormpy.pycarl.cln.FactorizedPolynomial, polynomial: stormpy.pycarl.cln.Polynomial, cache: stormpy.pycarl.cln._FactorizationCache) -> None

Constructor

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: collections.abc.Mapping[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(*args, **kwargs)

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

Overloaded function.

1. __init__(self: stormpy.pycarl.cln.FactorizedRationalFunction, arg0: stormpy.pycarl.cln.FactorizedPolynomial) -> None

2. __init__(self: stormpy.pycarl.cln.FactorizedRationalFunction, arg0: stormpy.pycarl.cln.FactorizedPolynomial, arg1: stormpy.pycarl.cln.FactorizedPolynomial) -> None

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: collections.abc.Mapping[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(*args, **kwargs)

Class wrapping cln-integers

Overloaded function.

1. __init__(self: stormpy.pycarl.cln.Integer, arg0: typing.SupportsInt) -> None

2. __init__(self: stormpy.pycarl.cln.Integer, arg0: str) -> None

3. __init__(self: stormpy.pycarl.cln.Integer, arg0: __gmp_expr<__mpz_struct [1], __mpz_struct [1]>) -> None

class Interval(*args, **kwargs)

Overloaded function.

1. __init__(self: stormpy.pycarl.cln.Interval, arg0: stormpy.pycarl.cln.Rational) -> None

2. __init__(self: stormpy.pycarl.cln.Interval, arg0: stormpy.pycarl.cln.Rational, arg1: stormpy.pycarl.cln.Rational) -> None

3. __init__(self: stormpy.pycarl.cln.Interval, arg0: stormpy.pycarl.cln.Rational, arg1: stormpy.pycarl._pycarl_core.BoundType, arg2: stormpy.pycarl.cln.Rational, arg3: stormpy.pycarl._pycarl_core.BoundType) -> None

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.

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

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

diameter(self: stormpy.pycarl.cln.Interval) → stormpy.pycarl.cln.Rational

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

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

static emptyInterval() → stormpy.pycarl.cln.Interval

integralPart(self: stormpy.pycarl.cln.Interval) → stormpy.pycarl.cln.Interval

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

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

inverse(self: stormpy.pycarl.cln.Interval) → stormpy.pycarl.cln.Interval

isClosedInterval(self: stormpy.pycarl.cln.Interval) → bool

isEmpty(self: stormpy.pycarl.cln.Interval) → bool

isHalfBounded(self: stormpy.pycarl.cln.Interval) → bool

isInfinite(self: stormpy.pycarl.cln.Interval) → bool

isNegative(self: stormpy.pycarl.cln.Interval) → bool

isOne(self: stormpy.pycarl.cln.Interval) → bool

isOpenInterval(self: stormpy.pycarl.cln.Interval) → bool

isPointInterval(self: stormpy.pycarl.cln.Interval) → bool

isPositive(self: stormpy.pycarl.cln.Interval) → bool

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

isSemiNegative(self: stormpy.pycarl.cln.Interval) → bool

isSemiPositive(self: stormpy.pycarl.cln.Interval) → bool

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

isUnbounded(self: stormpy.pycarl.cln.Interval) → bool

isZero(self: stormpy.pycarl.cln.Interval) → bool

lower(self: stormpy.pycarl.cln.Interval) → stormpy.pycarl.cln.Rational

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

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

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

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

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

static unboundedInterval() → stormpy.pycarl.cln.Interval

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

upper(self: stormpy.pycarl.cln.Interval) → stormpy.pycarl.cln.Rational

static zeroInterval() → stormpy.pycarl.cln.Interval

class Polynomial(*args, **kwargs)

Represent a multivariate polynomial

Overloaded function.

1. __init__(self: stormpy.pycarl.cln.Polynomial, arg0: stormpy.pycarl.cln.Term) -> None

2. __init__(self: stormpy.pycarl.cln.Polynomial, arg0: stormpy.pycarl._pycarl_core.Monomial) -> None

3. __init__(self: stormpy.pycarl.cln.Polynomial, arg0: stormpy.pycarl._pycarl_core.Variable) -> None

4. __init__(self: stormpy.pycarl.cln.Polynomial, arg0: stormpy.pycarl.cln.Rational) -> None

5. __init__(self: stormpy.pycarl.cln.Polynomial, arg0: collections.abc.Sequence[stormpy.pycarl.cln.Term]) -> None

constant_part(self: stormpy.pycarl.cln.Polynomial) → stormpy.pycarl.cln.Rational

degree(self: stormpy.pycarl.cln.Polynomial, arg0: stormpy.pycarl._pycarl_core.Variable) → int

derive(self: stormpy.pycarl.cln.Polynomial, variable: stormpy.pycarl._pycarl_core.Variable) → stormpy.pycarl.cln.Polynomial

Compute the derivative

evaluate(self: stormpy.pycarl.cln.Polynomial, arg0: collections.abc.Mapping[stormpy.pycarl._pycarl_core.Variable, stormpy.pycarl.cln.Rational]) → stormpy.pycarl.cln.Rational

gather_variables(self: stormpy.pycarl.cln.Polynomial) → set[stormpy.pycarl._pycarl_core.Variable]

is_constant(self: stormpy.pycarl.cln.Polynomial) → bool

property nr_terms

substitute(self: stormpy.pycarl.cln.Polynomial, arg0: collections.abc.Mapping[stormpy.pycarl._pycarl_core.Variable, stormpy.pycarl.cln.Polynomial]) → stormpy.pycarl.cln.Polynomial

to_smt2(self: stormpy.pycarl.cln.Polynomial) → str

property total_degree

class Rational(*args, **kwargs)

Class wrapping cln-rational numbers

Overloaded function.

1. __init__(self: stormpy.pycarl.cln.Rational, arg0: typing.SupportsFloat) -> None

2. __init__(self: stormpy.pycarl.cln.Rational, arg0: typing.SupportsInt) -> None

3. __init__(self: stormpy.pycarl.cln.Rational, arg0: stormpy.pycarl.cln.Integer, arg1: stormpy.pycarl.cln.Integer) -> None

4. __init__(self: stormpy.pycarl.cln.Rational, arg0: str) -> None

5. __init__(self: stormpy.pycarl.cln.Rational, arg0: __gmp_expr<__mpq_struct [1], __mpq_struct [1]>) -> None

property denominator

is_minus_one(self: stormpy.pycarl.cln.Rational) → bool

is_one(self: stormpy.pycarl.cln.Rational) → bool

property nominator

property numerator

class RationalFunction(*args, **kwargs)

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

Overloaded function.

1. __init__(self: stormpy.pycarl.cln.RationalFunction, arg0: stormpy.pycarl._pycarl_core.Variable) -> None

2. __init__(self: stormpy.pycarl.cln.RationalFunction, arg0: stormpy.pycarl.cln.Polynomial) -> None

3. __init__(self: stormpy.pycarl.cln.RationalFunction, arg0: stormpy.pycarl.cln.Polynomial, arg1: stormpy.pycarl.cln.Polynomial) -> None

constant_part(self: stormpy.pycarl.cln.RationalFunction) → stormpy.pycarl.cln.Rational

property denominator

derive(self: stormpy.pycarl.cln.RationalFunction, variable: stormpy.pycarl._pycarl_core.Variable) → stormpy.pycarl.cln.RationalFunction

Compute the derivative

evaluate(self: stormpy.pycarl.cln.RationalFunction, arg0: collections.abc.Mapping[stormpy.pycarl._pycarl_core.Variable, stormpy.pycarl.cln.Rational]) → stormpy.pycarl.cln.Rational

gather_variables(self: stormpy.pycarl.cln.RationalFunction) → set[stormpy.pycarl._pycarl_core.Variable]

is_constant(self: stormpy.pycarl.cln.RationalFunction) → bool

property nominator

property numerator

to_smt2(self: stormpy.pycarl.cln.RationalFunction) → str

class Term(*args, **kwargs)

Overloaded function.

1. __init__(self: stormpy.pycarl.cln.Term, arg0: stormpy.pycarl.cln.Rational, arg1: stormpy.pycarl._pycarl_core.Monomial) -> None

2. __init__(self: stormpy.pycarl.cln.Term, arg0: stormpy.pycarl._pycarl_core.Variable) -> None

3. __init__(self: stormpy.pycarl.cln.Term, arg0: stormpy.pycarl.cln.Rational) -> None

property coeff

is_constant(self: stormpy.pycarl.cln.Term) → bool

is_one(self: stormpy.pycarl.cln.Term) → bool

property monomial

property tdeg

abs(arg0: stormpy.pycarl.cln.Interval) → stormpy.pycarl.cln.Interval

ceil(arg0: stormpy.pycarl.cln.Interval) → stormpy.pycarl.cln.Interval

create_factorized_polynomial(polynomial)

denominator(x)

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

expand(x)

floor(arg0: stormpy.pycarl.cln.Interval) → stormpy.pycarl.cln.Interval

isInteger(arg0: stormpy.pycarl.cln.Interval) → bool

numerator(x)

pow(arg0: stormpy.pycarl.cln.Interval, arg1: SupportsInt) → stormpy.pycarl.cln.Interval

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