Arithmetic.cpp File Reference

#include "Arithmetic.h"
#include "ParserState.h"
#include <carl-arith/core/Variable.h>
#include <smtrat-common/types.h>

Include dependency graph for Arithmetic.cpp:

Go to the source code of this file.

Data Structures
struct	smtrat::parser::ToRealInstantiator

Namespaces
	smtrat
	Class to create the formulas for axioms.
	smtrat::parser
	smtrat::parser::arithmetic

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