smtrat::parser::arithmetic Namespace Reference

Typedefs
using	OperatorType = boost::variant< Poly::ConstructorOperation, carl::Relation >

Functions
FormulaT	makeConstraint (ArithmeticTheory &at, const Poly &lhs, const Poly &rhs, carl::Relation rel)
bool	isBooleanIdentity (const OperatorType &op, const std::vector< types::TermType > &arguments, TheoryError &errors)

Typedef Documentation

OperatorType

using smtrat::parser::arithmetic::OperatorType = typedef boost::variant<Poly::ConstructorOperation, carl::Relation>

Definition at line 11 of file Arithmetic.h.

Function Documentation

isBooleanIdentity()

bool smtrat::parser::arithmetic::isBooleanIdentity ( const OperatorType &  op, const std::vector< types::TermType > &  arguments, TheoryError &  errors  )

inline

Definition at line 134 of file Arithmetic.cpp.

Here is the call graph for this function:

Here is the caller graph for this function:

makeConstraint()

FormulaT smtrat::parser::arithmetic::makeConstraint ( ArithmeticTheory &  at, const Poly &  lhs, const Poly &  rhs, carl::Relation  rel  )

inline

Definition at line 68 of file Arithmetic.cpp.

Here is the call graph for this function:

Here is the caller graph for this function: