SMT-RAT
24.02
Toolbox for Strategic and Parallel Satisfiability-Modulo-Theories Solving
|
Implements the theory of arithmetic, including LRA, LIA, NRA and NIA. More...
#include <Arithmetic.h>
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::OperatorType > | ops |
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 |
ParserState * | state |
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 |
Implements the theory of arithmetic, including LRA, LIA, NRA and NIA.
Definition at line 16 of file Arithmetic.h.
smtrat::parser::ArithmeticTheory::ArithmeticTheory | ( | ParserState * | state | ) |
|
inlinestaticinherited |
Initialize the global symbol table for constants.
Definition at line 115 of file AbstractTheory.h.
|
private |
|
static |
Definition at line 159 of file Arithmetic.cpp.
|
inlineprivate |
Definition at line 53 of file Arithmetic.cpp.
|
inlineprivate |
Definition at line 8 of file Arithmetic.cpp.
|
virtual |
Resolve a quantified term.
Reimplemented from smtrat::parser::AbstractTheory.
Definition at line 451 of file Arithmetic.cpp.
|
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.
|
inlineinherited |
|
virtual |
Resolve another unknown function call.
Reimplemented from smtrat::parser::AbstractTheory.
Definition at line 279 of file Arithmetic.cpp.
|
virtual |
Resolve a distinct operator.
Reimplemented from smtrat::parser::AbstractTheory.
Definition at line 249 of file Arithmetic.cpp.
void smtrat::parser::ArithmeticTheory::handleDivisions | ( | ) |
|
virtual |
Resolve an if-then-else operator.
Reimplemented from smtrat::parser::AbstractTheory.
Definition at line 203 of file Arithmetic.cpp.
|
virtual |
Instantiate a variable within a term.
Reimplemented from smtrat::parser::AbstractTheory.
Definition at line 259 of file Arithmetic.cpp.
|
inlinevirtualinherited |
Reimplemented in smtrat::parser::BitvectorTheory.
Definition at line 88 of file AbstractTheory.h.
|
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.
|
private |
Definition at line 39 of file Arithmetic.h.
Definition at line 20 of file Arithmetic.h.
Definition at line 21 of file Arithmetic.h.
Definition at line 22 of file Arithmetic.h.
std::map<std::string, arithmetic::OperatorType> smtrat::parser::ArithmeticTheory::ops |
Definition at line 19 of file Arithmetic.h.
|
inherited |
Definition at line 37 of file AbstractTheory.h.