Pycarl formula

Number independent types

class pycarl.formula.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 pycarl.formula.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: handle) -> str

  2. __str__(self: pycarl.formula.formula.Relation) -> 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)