diff options
Diffstat (limited to 'src/parser/smt2/smt2.h')
-rw-r--r-- | src/parser/smt2/smt2.h | 40 |
1 files changed, 25 insertions, 15 deletions
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(); |