Adding class Smt2 to handle declaration of logic and theory symbols

1 files changed, 11 insertions, 0 deletions

diff --git a/src/parser/parser.cpp b/src/parser/parser.cpp
index b4bafc953..a1d6398f0 100644
--- a/src/parser/parser.cpp
+++ b/src/parser/parser.cpp
@@ -210,6 +210,17 @@ void Parser::checkArity(Kind kind, unsigned int numArgs)
   }
 }
 
+void Parser::checkOperator(Kind kind, unsigned int numArgs) throw (ParserException) {
+  if( d_strictMode && d_logicOperators.find(kind) == d_logicOperators.end() ) {
+    parseError( "Operator is not defined in the current logic: " + kindToString(kind) );
+  }
+  checkArity(kind,numArgs);
+}
+
+void Parser::addOperator(Kind kind) {
+  d_logicOperators.insert(kind);
+}
+
 Command* Parser::nextCommand() throw(ParserException) {
   Debug("parser") << "nextCommand()" << std::endl;
   Command* cmd = NULL;