Warning

Pycarl is now part of stormpy and this repository is no longer maintained. Please use the Github repository of stormpy instead.

Pycarl core

Number independent types

class pycarl.BoundType

Members:

STRICT

WEAK

INFTY

INFTY = <BoundType.INFTY: 2>
STRICT = <BoundType.STRICT: 0>
WEAK = <BoundType.WEAK: 1>
property name
property value
class pycarl.Interval
abs(self: pycarl.core.Interval) → pycarl.core.Interval
center(self: pycarl.core.Interval) → float
complement(self: pycarl.core.Interval, arg0: pycarl.core.Interval, arg1: pycarl.core.Interval) → bool
contains(*args, **kwargs)

Overloaded function.

  1. contains(self: pycarl.core.Interval, arg0: float) -> bool

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

diameter(self: pycarl.core.Interval) → float
difference(self: pycarl.core.Interval, arg0: pycarl.core.Interval, arg1: pycarl.core.Interval, arg2: pycarl.core.Interval) → bool
div(self: pycarl.core.Interval, arg0: pycarl.core.Interval) → pycarl.core.Interval
static emptyInterval() → pycarl.core.Interval
integralPart(self: pycarl.core.Interval) → pycarl.core.Interval
intersect(self: pycarl.core.Interval, arg0: pycarl.core.Interval) → pycarl.core.Interval
intersectsWith(self: pycarl.core.Interval, arg0: pycarl.core.Interval) → bool
inverse(self: pycarl.core.Interval) → pycarl.core.Interval
isClosedInterval(self: pycarl.core.Interval) → bool
isEmpty(self: pycarl.core.Interval) → bool
isHalfBounded(self: pycarl.core.Interval) → bool
isInfinite(self: pycarl.core.Interval) → bool
isNegative(self: pycarl.core.Interval) → bool
isOne(self: pycarl.core.Interval) → bool
isOpenInterval(self: pycarl.core.Interval) → bool
isPointInterval(self: pycarl.core.Interval) → bool
isPositive(self: pycarl.core.Interval) → bool
isProperSubset(self: pycarl.core.Interval, arg0: pycarl.core.Interval) → bool
isSemiNegative(self: pycarl.core.Interval) → bool
isSemiPositive(self: pycarl.core.Interval) → bool
isSubset(self: pycarl.core.Interval, arg0: pycarl.core.Interval) → bool
isUnbounded(self: pycarl.core.Interval) → bool
isZero(self: pycarl.core.Interval) → bool
lower(self: pycarl.core.Interval) → float
meets(self: pycarl.core.Interval, arg0: float) → bool
sample(self: pycarl.core.Interval, arg0: bool) → float
setLower(self: pycarl.core.Interval, arg0: float) → None
setUpper(self: pycarl.core.Interval, arg0: float) → None
symmetricDifference(self: pycarl.core.Interval, arg0: pycarl.core.Interval, arg1: pycarl.core.Interval, arg2: pycarl.core.Interval) → bool
static unboundedInterval() → pycarl.core.Interval
unite(self: pycarl.core.Interval, arg0: pycarl.core.Interval, arg1: pycarl.core.Interval, arg2: pycarl.core.Interval) → bool
upper(self: pycarl.core.Interval) → float
static zeroInterval() → pycarl.core.Interval
class pycarl.Monomial
property exponents
property tdeg
exception pycarl.NoPicklingSupport
class pycarl.Variable
property id
property is_no_variable
property name
property rank
property type
class pycarl.VariableType

Members:

BOOL

INT

REAL

BOOL = <VariableType.BOOL: 0>
INT = <VariableType.INT: 2>
REAL = <VariableType.REAL: 1>
property name
property value
pycarl.abs(arg0: pycarl.core.Interval) → pycarl.core.Interval
pycarl.carl_version()

Get Carl version. :return: Version of Carl.

pycarl.ceil(arg0: pycarl.core.Interval) → pycarl.core.Interval
pycarl.clear_monomial_pool() → None

Clear monomial pool and remove all monomials

pycarl.clear_pools()

Clear all pools.

pycarl.clear_variable_pool() → None

Clear variable pool and remove all variables

pycarl.create_monomial(variable: pycarl.core.Variable, exponent: int) → pycarl.core.Monomial

Create monomial

pycarl.div(arg0: pycarl.core.Interval, arg1: pycarl.core.Interval) → pycarl.core.Interval
pycarl.floor(arg0: pycarl.core.Interval) → pycarl.core.Interval
pycarl.has_cln()

Check if pycarl has support for CLN. :return: True iff CLN is supported.

pycarl.has_parser()

Check if pycarl has parsing support. :return: True iff parsing is supported.

pycarl.isInteger(arg0: pycarl.core.Interval) → bool
pycarl.pow(arg0: pycarl.core.Interval, arg1: int) → pycarl.core.Interval
pycarl.print_info()

Print information about pycarl.

pycarl.quotient(arg0: pycarl.core.Interval, arg1: pycarl.core.Interval) → pycarl.core.Interval
pycarl.variable_with_name(arg0: str) → pycarl.core.Variable

Get a variable from the pool with the given name.

Number dependent types (gmp)

class pycarl.gmp.Factorization
class pycarl.gmp.FactorizedPolynomial

Represent a polynomial with its factorization

cache(self: pycarl.gmp.gmp.FactorizedPolynomial) → pycarl.gmp.gmp._FactorizationCache
property coefficient
constant_part(self: pycarl.gmp.gmp.FactorizedPolynomial) → pycarl.gmp.gmp.Rational
derive(self: pycarl.gmp.gmp.FactorizedPolynomial, variable: pycarl.core.Variable) → pycarl.gmp.gmp.FactorizedPolynomial

Compute the derivative

evaluate(self: pycarl.gmp.gmp.FactorizedPolynomial, arg0: Dict[pycarl.core.Variable, pycarl.gmp.gmp.Rational]) → pycarl.gmp.gmp.Rational
factorization(self: pycarl.gmp.gmp.FactorizedPolynomial) → pycarl.gmp.gmp.Factorization

Get factorization

gather_variables(self: pycarl.gmp.gmp.FactorizedPolynomial) → Set[pycarl.core.Variable]
is_constant(self: pycarl.gmp.gmp.FactorizedPolynomial) → bool
is_one(self: pycarl.gmp.gmp.FactorizedPolynomial) → bool
polynomial(self: pycarl.gmp.gmp.FactorizedPolynomial) → pycarl.gmp.gmp.Polynomial

Get underlying polynomial

to_smt2(self: pycarl.gmp.gmp.FactorizedPolynomial) → str
class pycarl.gmp.FactorizedRationalFunction

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

constant_part(self: pycarl.gmp.gmp.FactorizedRationalFunction) → pycarl.gmp.gmp.Rational
property denominator
derive(self: pycarl.gmp.gmp.FactorizedRationalFunction, variable: pycarl.core.Variable) → pycarl.gmp.gmp.FactorizedRationalFunction

Compute the derivative

evaluate(self: pycarl.gmp.gmp.FactorizedRationalFunction, arg0: Dict[pycarl.core.Variable, pycarl.gmp.gmp.Rational]) → pycarl.gmp.gmp.Rational
gather_variables(self: pycarl.gmp.gmp.FactorizedRationalFunction) → Set[pycarl.core.Variable]
is_constant(self: pycarl.gmp.gmp.FactorizedRationalFunction) → bool
property numerator
rational_function(self: pycarl.gmp.gmp.FactorizedRationalFunction) → pycarl.gmp.gmp.RationalFunction
to_smt2(self: pycarl.gmp.gmp.FactorizedRationalFunction) → str
class pycarl.gmp.Integer

Class wrapping gmp-integers

class pycarl.gmp.Interval
abs(self: pycarl.gmp.gmp.Interval) → pycarl.gmp.gmp.Interval
center(self: pycarl.gmp.gmp.Interval) → pycarl.gmp.gmp.Rational
complement(self: pycarl.gmp.gmp.Interval, arg0: pycarl.gmp.gmp.Interval, arg1: pycarl.gmp.gmp.Interval) → bool
contains(*args, **kwargs)

Overloaded function.

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

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

diameter(self: pycarl.gmp.gmp.Interval) → pycarl.gmp.gmp.Rational
difference(self: pycarl.gmp.gmp.Interval, arg0: pycarl.gmp.gmp.Interval, arg1: pycarl.gmp.gmp.Interval, arg2: pycarl.gmp.gmp.Interval) → bool
div(self: pycarl.gmp.gmp.Interval, arg0: pycarl.gmp.gmp.Interval) → pycarl.gmp.gmp.Interval
static emptyInterval() → pycarl.gmp.gmp.Interval
integralPart(self: pycarl.gmp.gmp.Interval) → pycarl.gmp.gmp.Interval
intersect(self: pycarl.gmp.gmp.Interval, arg0: pycarl.gmp.gmp.Interval) → pycarl.gmp.gmp.Interval
intersectsWith(self: pycarl.gmp.gmp.Interval, arg0: pycarl.gmp.gmp.Interval) → bool
inverse(self: pycarl.gmp.gmp.Interval) → pycarl.gmp.gmp.Interval
isClosedInterval(self: pycarl.gmp.gmp.Interval) → bool
isEmpty(self: pycarl.gmp.gmp.Interval) → bool
isHalfBounded(self: pycarl.gmp.gmp.Interval) → bool
isInfinite(self: pycarl.gmp.gmp.Interval) → bool
isNegative(self: pycarl.gmp.gmp.Interval) → bool
isOne(self: pycarl.gmp.gmp.Interval) → bool
isOpenInterval(self: pycarl.gmp.gmp.Interval) → bool
isPointInterval(self: pycarl.gmp.gmp.Interval) → bool
isPositive(self: pycarl.gmp.gmp.Interval) → bool
isProperSubset(self: pycarl.gmp.gmp.Interval, arg0: pycarl.gmp.gmp.Interval) → bool
isSemiNegative(self: pycarl.gmp.gmp.Interval) → bool
isSemiPositive(self: pycarl.gmp.gmp.Interval) → bool
isSubset(self: pycarl.gmp.gmp.Interval, arg0: pycarl.gmp.gmp.Interval) → bool
isUnbounded(self: pycarl.gmp.gmp.Interval) → bool
isZero(self: pycarl.gmp.gmp.Interval) → bool
lower(self: pycarl.gmp.gmp.Interval) → pycarl.gmp.gmp.Rational
meets(self: pycarl.gmp.gmp.Interval, arg0: pycarl.gmp.gmp.Rational) → bool
sample(self: pycarl.gmp.gmp.Interval, arg0: bool) → pycarl.gmp.gmp.Rational
setLower(self: pycarl.gmp.gmp.Interval, arg0: pycarl.gmp.gmp.Rational) → None
setUpper(self: pycarl.gmp.gmp.Interval, arg0: pycarl.gmp.gmp.Rational) → None
symmetricDifference(self: pycarl.gmp.gmp.Interval, arg0: pycarl.gmp.gmp.Interval, arg1: pycarl.gmp.gmp.Interval, arg2: pycarl.gmp.gmp.Interval) → bool
static unboundedInterval() → pycarl.gmp.gmp.Interval
unite(self: pycarl.gmp.gmp.Interval, arg0: pycarl.gmp.gmp.Interval, arg1: pycarl.gmp.gmp.Interval, arg2: pycarl.gmp.gmp.Interval) → bool
upper(self: pycarl.gmp.gmp.Interval) → pycarl.gmp.gmp.Rational
static zeroInterval() → pycarl.gmp.gmp.Interval
class pycarl.gmp.Polynomial

Represent a multivariate polynomial

constant_part(self: pycarl.gmp.gmp.Polynomial) → pycarl.gmp.gmp.Rational
degree(self: pycarl.gmp.gmp.Polynomial, arg0: pycarl.core.Variable) → int
derive(self: pycarl.gmp.gmp.Polynomial, variable: pycarl.core.Variable) → pycarl.gmp.gmp.Polynomial

Compute the derivative

evaluate(self: pycarl.gmp.gmp.Polynomial, arg0: Dict[pycarl.core.Variable, pycarl.gmp.gmp.Rational]) → pycarl.gmp.gmp.Rational
gather_variables(self: pycarl.gmp.gmp.Polynomial) → Set[pycarl.core.Variable]
is_constant(self: pycarl.gmp.gmp.Polynomial) → bool
property nr_terms
substitute(self: pycarl.gmp.gmp.Polynomial, arg0: Dict[pycarl.core.Variable, pycarl.gmp.gmp.Polynomial]) → pycarl.gmp.gmp.Polynomial
to_smt2(self: pycarl.gmp.gmp.Polynomial) → str
property total_degree
class pycarl.gmp.Rational

Class wrapping gmp-rational numbers

property denominator
property nominator
property numerator
class pycarl.gmp.RationalFunction

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

constant_part(self: pycarl.gmp.gmp.RationalFunction) → pycarl.gmp.gmp.Rational
property denominator
derive(self: pycarl.gmp.gmp.RationalFunction, variable: pycarl.core.Variable) → pycarl.gmp.gmp.RationalFunction

Compute the derivative

evaluate(self: pycarl.gmp.gmp.RationalFunction, arg0: Dict[pycarl.core.Variable, pycarl.gmp.gmp.Rational]) → pycarl.gmp.gmp.Rational
gather_variables(self: pycarl.gmp.gmp.RationalFunction) → Set[pycarl.core.Variable]
is_constant(self: pycarl.gmp.gmp.RationalFunction) → bool
property nominator
property numerator
to_smt2(self: pycarl.gmp.gmp.RationalFunction) → str
class pycarl.gmp.Term
property coeff
is_constant(self: pycarl.gmp.gmp.Term) → bool
is_one(self: pycarl.gmp.gmp.Term) → bool
property monomial
property tdeg
pycarl.gmp.abs(arg0: pycarl.gmp.gmp.Interval) → pycarl.gmp.gmp.Interval
pycarl.gmp.ceil(arg0: pycarl.gmp.gmp.Interval) → pycarl.gmp.gmp.Interval
pycarl.gmp.create_factorized_polynomial(polynomial)
pycarl.gmp.denominator(x)
pycarl.gmp.div(arg0: pycarl.gmp.gmp.Interval, arg1: pycarl.gmp.gmp.Interval) → pycarl.gmp.gmp.Interval
pycarl.gmp.expand(x)
pycarl.gmp.floor(arg0: pycarl.gmp.gmp.Interval) → pycarl.gmp.gmp.Interval
pycarl.gmp.isInteger(arg0: pycarl.gmp.gmp.Interval) → bool
pycarl.gmp.numerator(x)
pycarl.gmp.pow(arg0: pycarl.gmp.gmp.Interval, arg1: int) → pycarl.gmp.gmp.Interval
pycarl.gmp.quotient(arg0: pycarl.gmp.gmp.Interval, arg1: pycarl.gmp.gmp.Interval) → pycarl.gmp.gmp.Interval

Number dependent types (cln)

class pycarl.cln.Factorization
class pycarl.cln.FactorizedPolynomial

Represent a polynomial with its factorization

cache(self: pycarl.cln.cln.FactorizedPolynomial) → pycarl.cln.cln._FactorizationCache
property coefficient
constant_part(self: pycarl.cln.cln.FactorizedPolynomial) → pycarl.cln.cln.Rational
derive(self: pycarl.cln.cln.FactorizedPolynomial, variable: pycarl.core.Variable) → pycarl.cln.cln.FactorizedPolynomial

Compute the derivative

evaluate(self: pycarl.cln.cln.FactorizedPolynomial, arg0: Dict[pycarl.core.Variable, pycarl.cln.cln.Rational]) → pycarl.cln.cln.Rational
factorization(self: pycarl.cln.cln.FactorizedPolynomial) → pycarl.cln.cln.Factorization

Get factorization

gather_variables(self: pycarl.cln.cln.FactorizedPolynomial) → Set[pycarl.core.Variable]
is_constant(self: pycarl.cln.cln.FactorizedPolynomial) → bool
is_one(self: pycarl.cln.cln.FactorizedPolynomial) → bool
polynomial(self: pycarl.cln.cln.FactorizedPolynomial) → pycarl.cln.cln.Polynomial

Get underlying polynomial

to_smt2(self: pycarl.cln.cln.FactorizedPolynomial) → str
class pycarl.cln.FactorizedRationalFunction

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

constant_part(self: pycarl.cln.cln.FactorizedRationalFunction) → pycarl.cln.cln.Rational
property denominator
derive(self: pycarl.cln.cln.FactorizedRationalFunction, variable: pycarl.core.Variable) → pycarl.cln.cln.FactorizedRationalFunction

Compute the derivative

evaluate(self: pycarl.cln.cln.FactorizedRationalFunction, arg0: Dict[pycarl.core.Variable, pycarl.cln.cln.Rational]) → pycarl.cln.cln.Rational
gather_variables(self: pycarl.cln.cln.FactorizedRationalFunction) → Set[pycarl.core.Variable]
is_constant(self: pycarl.cln.cln.FactorizedRationalFunction) → bool
property numerator
rational_function(self: pycarl.cln.cln.FactorizedRationalFunction) → pycarl.cln.cln.RationalFunction
to_smt2(self: pycarl.cln.cln.FactorizedRationalFunction) → str
class pycarl.cln.Integer

Class wrapping cln-integers

class pycarl.cln.Interval
abs(self: pycarl.cln.cln.Interval) → pycarl.cln.cln.Interval
center(self: pycarl.cln.cln.Interval) → pycarl.cln.cln.Rational
complement(self: pycarl.cln.cln.Interval, arg0: pycarl.cln.cln.Interval, arg1: pycarl.cln.cln.Interval) → bool
contains(*args, **kwargs)

Overloaded function.

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

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

diameter(self: pycarl.cln.cln.Interval) → pycarl.cln.cln.Rational
difference(self: pycarl.cln.cln.Interval, arg0: pycarl.cln.cln.Interval, arg1: pycarl.cln.cln.Interval, arg2: pycarl.cln.cln.Interval) → bool
div(self: pycarl.cln.cln.Interval, arg0: pycarl.cln.cln.Interval) → pycarl.cln.cln.Interval
static emptyInterval() → pycarl.cln.cln.Interval
integralPart(self: pycarl.cln.cln.Interval) → pycarl.cln.cln.Interval
intersect(self: pycarl.cln.cln.Interval, arg0: pycarl.cln.cln.Interval) → pycarl.cln.cln.Interval
intersectsWith(self: pycarl.cln.cln.Interval, arg0: pycarl.cln.cln.Interval) → bool
inverse(self: pycarl.cln.cln.Interval) → pycarl.cln.cln.Interval
isClosedInterval(self: pycarl.cln.cln.Interval) → bool
isEmpty(self: pycarl.cln.cln.Interval) → bool
isHalfBounded(self: pycarl.cln.cln.Interval) → bool
isInfinite(self: pycarl.cln.cln.Interval) → bool
isNegative(self: pycarl.cln.cln.Interval) → bool
isOne(self: pycarl.cln.cln.Interval) → bool
isOpenInterval(self: pycarl.cln.cln.Interval) → bool
isPointInterval(self: pycarl.cln.cln.Interval) → bool
isPositive(self: pycarl.cln.cln.Interval) → bool
isProperSubset(self: pycarl.cln.cln.Interval, arg0: pycarl.cln.cln.Interval) → bool
isSemiNegative(self: pycarl.cln.cln.Interval) → bool
isSemiPositive(self: pycarl.cln.cln.Interval) → bool
isSubset(self: pycarl.cln.cln.Interval, arg0: pycarl.cln.cln.Interval) → bool
isUnbounded(self: pycarl.cln.cln.Interval) → bool
isZero(self: pycarl.cln.cln.Interval) → bool
lower(self: pycarl.cln.cln.Interval) → pycarl.cln.cln.Rational
meets(self: pycarl.cln.cln.Interval, arg0: pycarl.cln.cln.Rational) → bool
sample(self: pycarl.cln.cln.Interval, arg0: bool) → pycarl.cln.cln.Rational
setLower(self: pycarl.cln.cln.Interval, arg0: pycarl.cln.cln.Rational) → None
setUpper(self: pycarl.cln.cln.Interval, arg0: pycarl.cln.cln.Rational) → None
symmetricDifference(self: pycarl.cln.cln.Interval, arg0: pycarl.cln.cln.Interval, arg1: pycarl.cln.cln.Interval, arg2: pycarl.cln.cln.Interval) → bool
static unboundedInterval() → pycarl.cln.cln.Interval
unite(self: pycarl.cln.cln.Interval, arg0: pycarl.cln.cln.Interval, arg1: pycarl.cln.cln.Interval, arg2: pycarl.cln.cln.Interval) → bool
upper(self: pycarl.cln.cln.Interval) → pycarl.cln.cln.Rational
static zeroInterval() → pycarl.cln.cln.Interval
class pycarl.cln.Polynomial

Represent a multivariate polynomial

constant_part(self: pycarl.cln.cln.Polynomial) → pycarl.cln.cln.Rational
degree(self: pycarl.cln.cln.Polynomial, arg0: pycarl.core.Variable) → int
derive(self: pycarl.cln.cln.Polynomial, variable: pycarl.core.Variable) → pycarl.cln.cln.Polynomial

Compute the derivative

evaluate(self: pycarl.cln.cln.Polynomial, arg0: Dict[pycarl.core.Variable, pycarl.cln.cln.Rational]) → pycarl.cln.cln.Rational
gather_variables(self: pycarl.cln.cln.Polynomial) → Set[pycarl.core.Variable]
is_constant(self: pycarl.cln.cln.Polynomial) → bool
property nr_terms
substitute(self: pycarl.cln.cln.Polynomial, arg0: Dict[pycarl.core.Variable, pycarl.cln.cln.Polynomial]) → pycarl.cln.cln.Polynomial
to_smt2(self: pycarl.cln.cln.Polynomial) → str
property total_degree
class pycarl.cln.Rational

Class wrapping cln-rational numbers

property denominator
is_minus_one(self: pycarl.cln.cln.Rational) → bool
is_one(self: pycarl.cln.cln.Rational) → bool
property nominator
property numerator
class pycarl.cln.RationalFunction

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

constant_part(self: pycarl.cln.cln.RationalFunction) → pycarl.cln.cln.Rational
property denominator
derive(self: pycarl.cln.cln.RationalFunction, variable: pycarl.core.Variable) → pycarl.cln.cln.RationalFunction

Compute the derivative

evaluate(self: pycarl.cln.cln.RationalFunction, arg0: Dict[pycarl.core.Variable, pycarl.cln.cln.Rational]) → pycarl.cln.cln.Rational
gather_variables(self: pycarl.cln.cln.RationalFunction) → Set[pycarl.core.Variable]
is_constant(self: pycarl.cln.cln.RationalFunction) → bool
property nominator
property numerator
to_smt2(self: pycarl.cln.cln.RationalFunction) → str
class pycarl.cln.Term
property coeff
is_constant(self: pycarl.cln.cln.Term) → bool
is_one(self: pycarl.cln.cln.Term) → bool
property monomial
property tdeg
pycarl.cln.abs(arg0: pycarl.cln.cln.Interval) → pycarl.cln.cln.Interval
pycarl.cln.ceil(arg0: pycarl.cln.cln.Interval) → pycarl.cln.cln.Interval
pycarl.cln.create_factorized_polynomial(polynomial)
pycarl.cln.denominator(x)
pycarl.cln.div(arg0: pycarl.cln.cln.Interval, arg1: pycarl.cln.cln.Interval) → pycarl.cln.cln.Interval
pycarl.cln.expand(x)
pycarl.cln.floor(arg0: pycarl.cln.cln.Interval) → pycarl.cln.cln.Interval
pycarl.cln.isInteger(arg0: pycarl.cln.cln.Interval) → bool
pycarl.cln.numerator(x)
pycarl.cln.pow(arg0: pycarl.cln.cln.Interval, arg1: int) → pycarl.cln.cln.Interval
pycarl.cln.quotient(arg0: pycarl.cln.cln.Interval, arg1: pycarl.cln.cln.Interval) → pycarl.cln.cln.Interval