diff options
author | Andres Noetzli <andres.noetzli@gmail.com> | 2018-06-04 19:28:44 -0700 |
---|---|---|
committer | Andrew Reynolds <andrew.j.reynolds@gmail.com> | 2018-06-04 21:28:44 -0500 |
commit | af5832b414fbee30904014aaf68a7f3b277b693d (patch) | |
tree | 5b6738aa895913c2858ff8751c573c51c6bd7b99 /src/parser | |
parent | 1e8a4e25751263a923a8d4cfd4d404fc0d24aa03 (diff) |
Only enable transcendentals if logic is N[I]RAT (#2052)
Diffstat (limited to 'src/parser')
-rw-r--r-- | src/parser/smt2/smt2.cpp | 15 | ||||
-rw-r--r-- | src/parser/smt2/smt2.h | 40 |
2 files changed, 38 insertions, 17 deletions
diff --git a/src/parser/smt2/smt2.cpp b/src/parser/smt2/smt2.cpp index cdb799864..2c7dfb333 100644 --- a/src/parser/smt2/smt2.cpp +++ b/src/parser/smt2/smt2.cpp @@ -51,8 +51,13 @@ void Smt2::addArithmeticOperators() { Parser::addOperator(kind::LEQ); Parser::addOperator(kind::GT); Parser::addOperator(kind::GEQ); - + + // NOTE: this operator is non-standard addOperator(kind::POW, "^"); +} + +void Smt2::addTranscendentalOperators() +{ addOperator(kind::EXPONENTIAL, "exp"); addOperator(kind::SINE, "sin"); addOperator(kind::COSINE, "cos"); @@ -66,7 +71,6 @@ void Smt2::addArithmeticOperators() { addOperator(kind::ARCCOSECANT, "arccsc"); addOperator(kind::ARCSECANT, "arcsec"); addOperator(kind::ARCCOTANGENT, "arccot"); - addOperator(kind::SQRT, "sqrt"); } @@ -249,6 +253,8 @@ void Smt2::addTheory(Theory theory) { Parser::addOperator(kind::DIVISION); break; + case THEORY_TRANSCENDENTALS: addTranscendentalOperators(); break; + case THEORY_QUANTIFIERS: break; @@ -486,6 +492,11 @@ void Smt2::setLogic(std::string name) { } else if(d_logic.areRealsUsed()) { addTheory(THEORY_REALS); } + + if (d_logic.areTranscendentalsUsed()) + { + addTheory(THEORY_TRANSCENDENTALS); + } } if(d_logic.isTheoryEnabled(theory::THEORY_ARRAYS)) { diff --git a/src/parser/smt2/smt2.h b/src/parser/smt2/smt2.h index 3def5696b..36c2479ad 100644 --- a/src/parser/smt2/smt2.h +++ b/src/parser/smt2/smt2.h @@ -40,21 +40,23 @@ class Smt2 : public Parser { friend class ParserBuilder; public: - enum Theory { - THEORY_ARRAYS, - THEORY_BITVECTORS, - THEORY_CORE, - THEORY_DATATYPES, - THEORY_INTS, - THEORY_REALS, - THEORY_REALS_INTS, - THEORY_QUANTIFIERS, - THEORY_SETS, - THEORY_STRINGS, - THEORY_UF, - THEORY_FP, - THEORY_SEP - }; + enum Theory + { + THEORY_ARRAYS, + THEORY_BITVECTORS, + THEORY_CORE, + THEORY_DATATYPES, + THEORY_INTS, + THEORY_REALS, + THEORY_TRANSCENDENTALS, + THEORY_REALS_INTS, + THEORY_QUANTIFIERS, + THEORY_SETS, + THEORY_STRINGS, + THEORY_UF, + THEORY_FP, + THEORY_SEP + }; private: bool d_logicSet; @@ -186,6 +188,12 @@ public: ss << "cannot declare or define symbol `" << name << "'; symbols starting with . and @ are reserved in SMT-LIB"; parseError(ss.str()); } + else if (isOperatorEnabled(name)) + { + std::stringstream ss; + ss << "Symbol `" << name << "' is shadowing a theory function symbol"; + parseError(ss.str()); + } } void includeFile(const std::string& filename); @@ -386,6 +394,8 @@ private: void addArithmeticOperators(); + void addTranscendentalOperators(); + void addBitvectorOperators(); void addStringOperators(); |