Pycarl formula

Number independent types

class FormulaType

Members:

ITE

EXISTS

FORALL

TRUE

FALSE

BOOL

NOT

IMPLIES

AND

OR

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

Members:

EQ

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>

name()

__str__(*args, **kwargs) Overloaded function.

1. __str__(self: stormpy.pycarl.formula.Relation) -> str

2. __str__(self: handle) -> str

property value

Number dependent types (gmp)

class Constraint

property lhs

property relation

to_smt2(self: stormpy.pycarl.formula.Constraint) → str

class Formula

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

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

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

property lhs

property relation

to_smt2(self: stormpy.pycarl.formula.Constraint) → str

class Formula

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

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

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