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();