Pycarl formula¶

Number independent types¶

class pycarl.formula.FormulaType¶

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 pycarl.formula.Relation¶

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>¶

name()¶

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

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

property value¶

Number dependent types (gmp)¶

class pycarl.gmp.formula.Constraint¶

property lhs¶

property relation¶

to_smt2(self: pycarl.gmp.formula.formula.Constraint) → str¶

class pycarl.gmp.formula.Formula¶

get_constraint(self: pycarl.gmp.formula.formula.Formula) → pycarl.gmp.formula.formula.Constraint¶: Get constraint of constraint formula

get_implication_conclusion(self: pycarl.gmp.formula.formula.Formula) → pycarl.gmp.formula.formula.Formula¶: Get conclusion of implication formula

get_implication_premise(self: pycarl.gmp.formula.formula.Formula) → pycarl.gmp.formula.formula.Formula¶: Get premise of implication formula

get_ite_condition(self: pycarl.gmp.formula.formula.Formula) → pycarl.gmp.formula.formula.Formula¶: Get condition of ITE formula

get_ite_first_case(self: pycarl.gmp.formula.formula.Formula) → pycarl.gmp.formula.formula.Formula¶: Get then case of ITE formula

get_ite_second_case(self: pycarl.gmp.formula.formula.Formula) → pycarl.gmp.formula.formula.Formula¶: Get else case of ITE formula

get_negation_subformula(self: pycarl.gmp.formula.formula.Formula) → pycarl.gmp.formula.formula.Formula¶: Get subformula of negation formula

get_subformulas(self: pycarl.gmp.formula.formula.Formula) → List[pycarl.gmp.formula.formula.Formula]¶: Get list of subformulas for n-ary formula

to_smt2(self: pycarl.gmp.formula.formula.Formula) → str¶

property type¶

class pycarl.gmp.formula.SimpleConstraint¶

lhs(self: pycarl.gmp.formula.formula.SimpleConstraint) → pycarl.gmp.gmp.Polynomial¶: Get the left hand side of the constraint

rel(self: pycarl.gmp.formula.formula.SimpleConstraint) → pycarl.formula.formula.Relation¶: Get the relation of the constraint

class pycarl.gmp.formula.SimpleConstraintRatFunc¶

lhs(self: pycarl.gmp.formula.formula.SimpleConstraintRatFunc) → pycarl.gmp.gmp.FactorizedRationalFunction¶: Get the left hand side of the constraint

rel(self: pycarl.gmp.formula.formula.SimpleConstraintRatFunc) → pycarl.formula.formula.Relation¶: Get the relation of the constraint

Number dependent types (cln)¶

class pycarl.cln.formula.Constraint¶

property lhs¶

property relation¶

to_smt2(self: pycarl.cln.formula.formula.Constraint) → str¶

class pycarl.cln.formula.Formula¶

get_constraint(self: pycarl.cln.formula.formula.Formula) → pycarl.cln.formula.formula.Constraint¶: Get constraint of constraint formula

get_implication_conclusion(self: pycarl.cln.formula.formula.Formula) → pycarl.cln.formula.formula.Formula¶: Get conclusion of implication formula

get_implication_premise(self: pycarl.cln.formula.formula.Formula) → pycarl.cln.formula.formula.Formula¶: Get premise of implication formula

get_ite_condition(self: pycarl.cln.formula.formula.Formula) → pycarl.cln.formula.formula.Formula¶: Get condition of ITE formula

get_ite_first_case(self: pycarl.cln.formula.formula.Formula) → pycarl.cln.formula.formula.Formula¶: Get then case of ITE formula

get_ite_second_case(self: pycarl.cln.formula.formula.Formula) → pycarl.cln.formula.formula.Formula¶: Get else case of ITE formula

get_negation_subformula(self: pycarl.cln.formula.formula.Formula) → pycarl.cln.formula.formula.Formula¶: Get subformula of negation formula

get_subformulas(self: pycarl.cln.formula.formula.Formula) → List[pycarl.cln.formula.formula.Formula]¶: Get list of subformulas for n-ary formula

to_smt2(self: pycarl.cln.formula.formula.Formula) → str¶

property type¶

class pycarl.cln.formula.SimpleConstraint¶

lhs(self: pycarl.cln.formula.formula.SimpleConstraint) → pycarl.cln.cln.Polynomial¶: Get the left hand side of the constraint

rel(self: pycarl.cln.formula.formula.SimpleConstraint) → pycarl.formula.formula.Relation¶: Get the relation of the constraint

class pycarl.cln.formula.SimpleConstraintRatFunc¶

lhs(self: pycarl.cln.formula.formula.SimpleConstraintRatFunc) → pycarl.cln.cln.FactorizedRationalFunction¶: Get the left hand side of the constraint

rel(self: pycarl.cln.formula.formula.SimpleConstraintRatFunc) → pycarl.formula.formula.Relation¶: Get the relation of the constraint