SMT-RAT  24.02
Toolbox for Strategic and Parallel Satisfiability-Modulo-Theories Solving
smtrat::parser::ArithmeticTheory Struct Reference

Implements the theory of arithmetic, including LRA, LIA, NRA and NIA. More...

#include <Arithmetic.h>

Inheritance diagram for smtrat::parser::ArithmeticTheory:
Collaboration diagram for smtrat::parser::ArithmeticTheory:

Public Member Functions

 ArithmeticTheory (ParserState *state)
 
bool declareVariable (const std::string &name, const carl::Sort &sort, types::VariableType &result, TheoryError &errors)
 Declare a new variable with the given name and the given sort. More...
 
bool handleITE (const FormulaT &ifterm, const types::TermType &thenterm, const types::TermType &elseterm, types::TermType &result, TheoryError &errors)
 Resolve an if-then-else operator. More...
 
bool handleDistinct (const std::vector< types::TermType > &arguments, types::TermType &result, TheoryError &errors)
 Resolve a distinct operator. More...
 
bool instantiate (const types::VariableType &var, const types::TermType &replacement, types::TermType &result, TheoryError &errors)
 Instantiate a variable within a term. More...
 
bool functionCall (const Identifier &identifier, const std::vector< types::TermType > &arguments, types::TermType &result, TheoryError &errors)
 Resolve another unknown function call. More...
 
bool declareQuantifiedTerm (const std::vector< std::pair< std::string, carl::Sort >> &vars, const carl::FormulaType &type, const types::TermType &term, types::TermType &result, TheoryError &errors)
 Resolve a quantified term. More...
 
void handleDivisions ()
 
virtual bool resolveSymbol (const Identifier &, types::TermType &, TheoryError &errors)
 Resolve a symbol that was not declared within the ParserState. More...
 
template<typename T , typename Builder >
FormulaT expandDistinct (const std::vector< T > &values, const Builder &neqBuilder)
 
virtual bool refreshVariable (const types::VariableType &, types::VariableType &, TheoryError &errors)
 

Static Public Member Functions

static void addSimpleSorts (qi::symbols< char, carl::Sort > &sorts)
 
static void addConstants (qi::symbols< char, types::ConstType > &)
 Initialize the global symbol table for constants. More...
 

Data Fields

std::map< std::string, arithmetic::OperatorTypeops
 
std::map< carl::Variable, std::tuple< FormulaT, Poly, Poly > > mITEs
 
std::map< carl::Variable, std::tuple< Poly, Poly > > mKnownDivisions
 
std::map< carl::Variable, std::tuple< Poly, Poly > > mNewDivisions
 
ParserStatestate
 

Private Member Functions

bool convertArguments (const arithmetic::OperatorType &op, const std::vector< types::TermType > &arguments, std::vector< Poly > &result, TheoryError &errors)
 
bool convertTerm (const types::TermType &term, Poly &result, bool allow_bool=false)
 
void addQuantifierToFormula (FormulaT &f)
 

Private Attributes

std::map< FormulaT, carl::Variable > mappedFormulas
 

Detailed Description

Implements the theory of arithmetic, including LRA, LIA, NRA and NIA.

Definition at line 16 of file Arithmetic.h.

Constructor & Destructor Documentation

◆ ArithmeticTheory()

smtrat::parser::ArithmeticTheory::ArithmeticTheory ( ParserState state)

Definition at line 165 of file Arithmetic.cpp.

Here is the call graph for this function:

Member Function Documentation

◆ addConstants()

static void smtrat::parser::AbstractTheory::addConstants ( qi::symbols< char, types::ConstType > &  )
inlinestaticinherited

Initialize the global symbol table for constants.

Definition at line 115 of file AbstractTheory.h.

◆ addQuantifierToFormula()

void smtrat::parser::ArithmeticTheory::addQuantifierToFormula ( FormulaT f)
private

◆ addSimpleSorts()

void smtrat::parser::ArithmeticTheory::addSimpleSorts ( qi::symbols< char, carl::Sort > &  sorts)
static

Definition at line 159 of file Arithmetic.cpp.

◆ convertArguments()

bool smtrat::parser::ArithmeticTheory::convertArguments ( const arithmetic::OperatorType op,
const std::vector< types::TermType > &  arguments,
std::vector< Poly > &  result,
TheoryError errors 
)
inlineprivate

Definition at line 53 of file Arithmetic.cpp.

Here is the call graph for this function:
Here is the caller graph for this function:

◆ convertTerm()

bool smtrat::parser::ArithmeticTheory::convertTerm ( const types::TermType term,
Poly result,
bool  allow_bool = false 
)
inlineprivate

Definition at line 8 of file Arithmetic.cpp.

Here is the call graph for this function:
Here is the caller graph for this function:

◆ declareQuantifiedTerm()

bool smtrat::parser::ArithmeticTheory::declareQuantifiedTerm ( const std::vector< std::pair< std::string, carl::Sort >> &  ,
const carl::FormulaType &  ,
const types::TermType ,
types::TermType ,
TheoryError errors 
)
virtual

Resolve a quantified term.

Reimplemented from smtrat::parser::AbstractTheory.

Definition at line 451 of file Arithmetic.cpp.

Here is the call graph for this function:

◆ declareVariable()

bool smtrat::parser::ArithmeticTheory::declareVariable ( const std::string &  ,
const carl::Sort &  ,
types::VariableType ,
TheoryError errors 
)
virtual

Declare a new variable with the given name and the given sort.

Reimplemented from smtrat::parser::AbstractTheory.

Definition at line 186 of file Arithmetic.cpp.

Here is the call graph for this function:

◆ expandDistinct()

template<typename T , typename Builder >
FormulaT smtrat::parser::AbstractTheory::expandDistinct ( const std::vector< T > &  values,
const Builder &  neqBuilder 
)
inlineinherited

Definition at line 72 of file AbstractTheory.h.

Here is the caller graph for this function:

◆ functionCall()

bool smtrat::parser::ArithmeticTheory::functionCall ( const Identifier ,
const std::vector< types::TermType > &  ,
types::TermType ,
TheoryError errors 
)
virtual

Resolve another unknown function call.

Reimplemented from smtrat::parser::AbstractTheory.

Definition at line 279 of file Arithmetic.cpp.

Here is the call graph for this function:

◆ handleDistinct()

bool smtrat::parser::ArithmeticTheory::handleDistinct ( const std::vector< types::TermType > &  ,
types::TermType ,
TheoryError errors 
)
virtual

Resolve a distinct operator.

Reimplemented from smtrat::parser::AbstractTheory.

Definition at line 249 of file Arithmetic.cpp.

Here is the call graph for this function:

◆ handleDivisions()

void smtrat::parser::ArithmeticTheory::handleDivisions ( )

◆ handleITE()

bool smtrat::parser::ArithmeticTheory::handleITE ( const FormulaT ,
const types::TermType ,
const types::TermType ,
types::TermType ,
TheoryError errors 
)
virtual

Resolve an if-then-else operator.

Reimplemented from smtrat::parser::AbstractTheory.

Definition at line 203 of file Arithmetic.cpp.

Here is the call graph for this function:

◆ instantiate()

bool smtrat::parser::ArithmeticTheory::instantiate ( const types::VariableType ,
const types::TermType ,
types::TermType ,
TheoryError errors 
)
virtual

Instantiate a variable within a term.

Reimplemented from smtrat::parser::AbstractTheory.

Definition at line 259 of file Arithmetic.cpp.

Here is the call graph for this function:

◆ refreshVariable()

virtual bool smtrat::parser::AbstractTheory::refreshVariable ( const types::VariableType ,
types::VariableType ,
TheoryError errors 
)
inlinevirtualinherited

Reimplemented in smtrat::parser::BitvectorTheory.

Definition at line 88 of file AbstractTheory.h.

Here is the call graph for this function:

◆ resolveSymbol()

virtual bool smtrat::parser::AbstractTheory::resolveSymbol ( const Identifier ,
types::TermType ,
TheoryError errors 
)
inlinevirtualinherited

Resolve a symbol that was not declared within the ParserState.

This might be a symbol that actually uses indices, for example bitvector constants.

Reimplemented in smtrat::parser::BitvectorTheory.

Definition at line 53 of file AbstractTheory.h.

Here is the call graph for this function:

Field Documentation

◆ mappedFormulas

std::map<FormulaT, carl::Variable> smtrat::parser::ArithmeticTheory::mappedFormulas
private

Definition at line 39 of file Arithmetic.h.

◆ mITEs

std::map<carl::Variable, std::tuple<FormulaT, Poly, Poly> > smtrat::parser::ArithmeticTheory::mITEs

Definition at line 20 of file Arithmetic.h.

◆ mKnownDivisions

std::map<carl::Variable, std::tuple<Poly, Poly> > smtrat::parser::ArithmeticTheory::mKnownDivisions

Definition at line 21 of file Arithmetic.h.

◆ mNewDivisions

std::map<carl::Variable, std::tuple<Poly, Poly> > smtrat::parser::ArithmeticTheory::mNewDivisions

Definition at line 22 of file Arithmetic.h.

◆ ops

std::map<std::string, arithmetic::OperatorType> smtrat::parser::ArithmeticTheory::ops

Definition at line 19 of file Arithmetic.h.

◆ state

ParserState* smtrat::parser::AbstractTheory::state
inherited

Definition at line 37 of file AbstractTheory.h.


The documentation for this struct was generated from the following files: