Pycarl formula¶

Number independent types¶

class FormulaType(self: stormpy.pycarl.formula.FormulaType, value: SupportsInt)¶

Members:

ITE

EXISTS

FORALL

TRUE

FALSE

BOOL

NOT

IMPLIES

AND

XOR

IFF

CONSTRAINT

BITVECTOR

UEQ

AND = <FormulaType.AND: 8>¶

BITVECTOR = <FormulaType.BITVECTOR: 15>¶

BOOL = <FormulaType.BOOL: 5>¶

CONSTRAINT = <FormulaType.CONSTRAINT: 12>¶

EXISTS = <FormulaType.EXISTS: 1>¶

FALSE = <FormulaType.FALSE: 4>¶

FORALL = <FormulaType.FORALL: 2>¶

IFF = <FormulaType.IFF: 11>¶

IMPLIES = <FormulaType.IMPLIES: 7>¶

ITE = <FormulaType.ITE: 0>¶

NOT = <FormulaType.NOT: 6>¶

OR = <FormulaType.OR: 9>¶

TRUE = <FormulaType.TRUE: 3>¶

UEQ = <FormulaType.UEQ: 16>¶

XOR = <FormulaType.XOR: 10>¶

property name¶

property value¶

class Relation(self: stormpy.pycarl.formula.Relation, value: SupportsInt)¶

Members:

NEQ

LESS

LEQ

GREATER

GEQ

EQ = <Relation.EQ: 0>¶

GEQ = <Relation.GEQ: 5>¶

GREATER = <Relation.GREATER: 3>¶

LEQ = <Relation.LEQ: 4>¶

LESS = <Relation.LESS: 2>¶

NEQ = <Relation.NEQ: 1>¶

property name¶

property value¶

Number dependent types (gmp)¶

class Constraint(*args, **kwargs)¶

Overloaded function.

__init__(self: stormpy.pycarl.formula.Constraint, arg0: bool) -> None
__init__(self: stormpy.pycarl.formula.Constraint, var: stormpy.pycarl._pycarl_core.Variable, rel: stormpy.pycarl.formula.Relation, bound: stormpy.pycarl.gmp.Rational) -> None
__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.

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

Create Formula given Boolean variable

__init__(self: stormpy.pycarl.formula.Formula, arg0: stormpy.pycarl.formula.Constraint) -> None
__init__(self: stormpy.pycarl.formula.Formula, arg0: stormpy.pycarl.formula.FormulaType, arg1: stormpy.pycarl.formula.Formula) -> None
__init__(self: stormpy.pycarl.formula.Formula, arg0: stormpy.pycarl.formula.FormulaType, arg1: collections.abc.Sequence[stormpy.pycarl.formula.Formula]) -> None
__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.

__init__(self: stormpy.pycarl.formula.SimpleConstraint, arg0: bool) -> None
__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.

__init__(self: stormpy.pycarl.formula.SimpleConstraintRatFunc, arg0: bool) -> None
__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.

__init__(self: stormpy.pycarl.formula.Constraint, arg0: bool) -> None
__init__(self: stormpy.pycarl.formula.Constraint, var: stormpy.pycarl._pycarl_core.Variable, rel: stormpy.pycarl.formula.Relation, bound: stormpy.pycarl.cln.Rational) -> None
__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.

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

Create Formula given Boolean variable

__init__(self: stormpy.pycarl.formula.Formula, arg0: stormpy.pycarl.formula.Constraint) -> None
__init__(self: stormpy.pycarl.formula.Formula, arg0: stormpy.pycarl.formula.FormulaType, arg1: stormpy.pycarl.formula.Formula) -> None
__init__(self: stormpy.pycarl.formula.Formula, arg0: stormpy.pycarl.formula.FormulaType, arg1: collections.abc.Sequence[stormpy.pycarl.formula.Formula]) -> None
__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.

__init__(self: stormpy.pycarl.formula.SimpleConstraint, arg0: bool) -> None
__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.

__init__(self: stormpy.pycarl.formula.SimpleConstraintRatFunc, arg0: bool) -> None
__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