SMT-RAT  24.02
Toolbox for Strategic and Parallel Satisfiability-Modulo-Theories Solving
Arithmetic.h File Reference
#include "Common.h"
#include "AbstractTheory.h"
#include "ParserState.h"
Include dependency graph for Arithmetic.h:
This graph shows which files directly or indirectly include this file:

Go to the source code of this file.

Data Structures

struct  smtrat::parser::ArithmeticTheory
 Implements the theory of arithmetic, including LRA, LIA, NRA and NIA. More...
 

Namespaces

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

Typedefs

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