Formula¶

Warning

The stormpy developer API is internal and can be subject to change.

class Formula(arg0: stormpy.numbers.Variable)¶

class Formula(arg0: stormpy.numbers.developer.formula.Constraint)

class Formula( arg0: stormpy.numbers.developer.formula.FormulaType, arg1: stormpy.numbers.developer.formula.Formula, )

class Formula( arg0: stormpy.numbers.developer.formula.FormulaType, arg1: collections.abc.Sequence[stormpy.numbers.developer.formula.Formula], )

class Formula(arg0: bool)

Bases: pybind11_object

Create Formula given Boolean variable

get_constraint( self: stormpy.numbers.developer.formula.Formula, ) → stormpy.numbers.developer.formula.Constraint¶: Get constraint of constraint formula

get_implication_conclusion( self: stormpy.numbers.developer.formula.Formula, ) → stormpy.numbers.developer.formula.Formula¶: Get conclusion of implication formula

get_implication_premise( self: stormpy.numbers.developer.formula.Formula, ) → stormpy.numbers.developer.formula.Formula¶: Get premise of implication formula

get_ite_condition( self: stormpy.numbers.developer.formula.Formula, ) → stormpy.numbers.developer.formula.Formula¶: Get condition of ITE formula

get_ite_first_case( self: stormpy.numbers.developer.formula.Formula, ) → stormpy.numbers.developer.formula.Formula¶: Get then case of ITE formula

get_ite_second_case( self: stormpy.numbers.developer.formula.Formula, ) → stormpy.numbers.developer.formula.Formula¶: Get else case of ITE formula

get_negation_subformula( self: stormpy.numbers.developer.formula.Formula, ) → stormpy.numbers.developer.formula.Formula¶: Get subformula of negation formula

get_subformulas( self: stormpy.numbers.developer.formula.Formula, ) → list[stormpy.numbers.developer.formula.Formula]¶: Get list of subformulas for n-ary formula

to_smt2(self: stormpy.numbers.developer.formula.Formula) → str¶

property type¶