Pycarl formula

Number independent types

class FormulaType(*values)
AND = 8
BITVECTOR = 15
BOOL = 5
CONSTRAINT = 12
EXISTS = 1
FALSE = 4
FORALL = 2
IFF = 11
IMPLIES = 7
ITE = 0
NOT = 6
OR = 9
TRUE = 3
UEQ = 16
XOR = 10
class Relation(*values)
EQ = 0
GEQ = 5
GREATER = 3
LEQ = 4
LESS = 2
NEQ = 1
friendly_name(self: stormpy.pycarl.formula.Relation) → str

Number dependent types (gmp)

class Constraint(*args, **kwargs)

Overloaded function.

  1. __init__(self: stormpy.pycarl.formula.Constraint, arg0: bool) -> None

  2. __init__(self: stormpy.pycarl.formula.Constraint, var: stormpy.pycarl._pycarl_core.Variable, rel: stormpy.pycarl.formula.Relation, bound: stormpy.pycarl.gmp.Rational) -> None

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

property lhs
property relation
to_smt2(self: stormpy.pycarl.formula.Constraint) → str
class Formula(*args, **kwargs)

Overloaded function.

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

Create Formula given Boolean variable

  1. __init__(self: stormpy.pycarl.formula.Formula, arg0: stormpy.pycarl.formula.Constraint) -> None

  2. __init__(self: stormpy.pycarl.formula.Formula, arg0: stormpy.pycarl.formula.FormulaType, arg1: stormpy.pycarl.formula.Formula) -> None

  3. __init__(self: stormpy.pycarl.formula.Formula, arg0: stormpy.pycarl.formula.FormulaType, arg1: collections.abc.Sequence[stormpy.pycarl.formula.Formula]) -> None

  4. __init__(self: stormpy.pycarl.formula.Formula, arg0: bool) -> None

get_constraint(self: stormpy.pycarl.formula.Formula) → stormpy.pycarl.formula.Constraint

Get constraint of constraint formula

get_implication_conclusion(self: stormpy.pycarl.formula.Formula) → stormpy.pycarl.formula.Formula

Get conclusion of implication formula

get_implication_premise(self: stormpy.pycarl.formula.Formula) → stormpy.pycarl.formula.Formula

Get premise of implication formula

get_ite_condition(self: stormpy.pycarl.formula.Formula) → stormpy.pycarl.formula.Formula

Get condition of ITE formula

get_ite_first_case(self: stormpy.pycarl.formula.Formula) → stormpy.pycarl.formula.Formula

Get then case of ITE formula

get_ite_second_case(self: stormpy.pycarl.formula.Formula) → stormpy.pycarl.formula.Formula

Get else case of ITE formula

get_negation_subformula(self: stormpy.pycarl.formula.Formula) → stormpy.pycarl.formula.Formula

Get subformula of negation formula

get_subformulas(self: stormpy.pycarl.formula.Formula) → list[stormpy.pycarl.formula.Formula]

Get list of subformulas for n-ary formula

to_smt2(self: stormpy.pycarl.formula.Formula) → str
property type
class SimpleConstraint(*args, **kwargs)

Overloaded function.

  1. __init__(self: stormpy.pycarl.formula.SimpleConstraint, arg0: bool) -> None

  2. __init__(self: stormpy.pycarl.formula.SimpleConstraint, arg0: stormpy.pycarl.gmp.Polynomial, arg1: stormpy.pycarl.formula.Relation) -> None

lhs(self: stormpy.pycarl.formula.SimpleConstraint) → stormpy.pycarl.gmp.Polynomial

Get the left hand side of the constraint

rel(self: stormpy.pycarl.formula.SimpleConstraint) → stormpy.pycarl.formula.Relation

Get the relation of the constraint

class SimpleConstraintRatFunc(*args, **kwargs)

Overloaded function.

  1. __init__(self: stormpy.pycarl.formula.SimpleConstraintRatFunc, arg0: bool) -> None

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

lhs(self: stormpy.pycarl.formula.SimpleConstraintRatFunc) → stormpy.pycarl.gmp.FactorizedRationalFunction

Get the left hand side of the constraint

rel(self: stormpy.pycarl.formula.SimpleConstraintRatFunc) → stormpy.pycarl.formula.Relation

Get the relation of the constraint

Number dependent types (cln)

class Constraint(*args, **kwargs)

Overloaded function.

  1. __init__(self: stormpy.pycarl.formula.Constraint, arg0: bool) -> None

  2. __init__(self: stormpy.pycarl.formula.Constraint, var: stormpy.pycarl._pycarl_core.Variable, rel: stormpy.pycarl.formula.Relation, bound: stormpy.pycarl.cln.Rational) -> None

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

property lhs
property relation
to_smt2(self: stormpy.pycarl.formula.Constraint) → str
class Formula(*args, **kwargs)

Overloaded function.

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

Create Formula given Boolean variable

  1. __init__(self: stormpy.pycarl.formula.Formula, arg0: stormpy.pycarl.formula.Constraint) -> None

  2. __init__(self: stormpy.pycarl.formula.Formula, arg0: stormpy.pycarl.formula.FormulaType, arg1: stormpy.pycarl.formula.Formula) -> None

  3. __init__(self: stormpy.pycarl.formula.Formula, arg0: stormpy.pycarl.formula.FormulaType, arg1: collections.abc.Sequence[stormpy.pycarl.formula.Formula]) -> None

  4. __init__(self: stormpy.pycarl.formula.Formula, arg0: bool) -> None

get_constraint(self: stormpy.pycarl.formula.Formula) → stormpy.pycarl.formula.Constraint

Get constraint of constraint formula

get_implication_conclusion(self: stormpy.pycarl.formula.Formula) → stormpy.pycarl.formula.Formula

Get conclusion of implication formula

get_implication_premise(self: stormpy.pycarl.formula.Formula) → stormpy.pycarl.formula.Formula

Get premise of implication formula

get_ite_condition(self: stormpy.pycarl.formula.Formula) → stormpy.pycarl.formula.Formula

Get condition of ITE formula

get_ite_first_case(self: stormpy.pycarl.formula.Formula) → stormpy.pycarl.formula.Formula

Get then case of ITE formula

get_ite_second_case(self: stormpy.pycarl.formula.Formula) → stormpy.pycarl.formula.Formula

Get else case of ITE formula

get_negation_subformula(self: stormpy.pycarl.formula.Formula) → stormpy.pycarl.formula.Formula

Get subformula of negation formula

get_subformulas(self: stormpy.pycarl.formula.Formula) → list[stormpy.pycarl.formula.Formula]

Get list of subformulas for n-ary formula

to_smt2(self: stormpy.pycarl.formula.Formula) → str
property type
class SimpleConstraint(*args, **kwargs)

Overloaded function.

  1. __init__(self: stormpy.pycarl.formula.SimpleConstraint, arg0: bool) -> None

  2. __init__(self: stormpy.pycarl.formula.SimpleConstraint, arg0: stormpy.pycarl.cln.Polynomial, arg1: stormpy.pycarl.formula.Relation) -> None

lhs(self: stormpy.pycarl.formula.SimpleConstraint) → stormpy.pycarl.cln.Polynomial

Get the left hand side of the constraint

rel(self: stormpy.pycarl.formula.SimpleConstraint) → stormpy.pycarl.formula.Relation

Get the relation of the constraint

class SimpleConstraintRatFunc(*args, **kwargs)

Overloaded function.

  1. __init__(self: stormpy.pycarl.formula.SimpleConstraintRatFunc, arg0: bool) -> None

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

lhs(self: stormpy.pycarl.formula.SimpleConstraintRatFunc) → stormpy.pycarl.cln.FactorizedRationalFunction

Get the left hand side of the constraint

rel(self: stormpy.pycarl.formula.SimpleConstraintRatFunc) → stormpy.pycarl.formula.Relation

Get the relation of the constraint