Don't tokenize SET_THEORY operators in smt2 parser

3 files changed, 193 insertions, 145 deletions

diff --git a/src/parser/smt2/Smt2.g b/src/parser/smt2/Smt2.g
index 6e9f04ce9..f1acac6ba 100644
--- a/src/parser/smt2/Smt2.g
+++ b/src/parser/smt2/Smt2.g
@@ -770,6 +770,7 @@ term[CVC4::Expr& expr, CVC4::Expr& expr2]
   std::vector< std::pair<std::string, Expr> > binders;
   Type type;
   std::string s;
+  bool isBuiltinOperator = false;
 }
   : /* a built-in operator application */
     LPAREN_TOK builtinOp[kind] termList[args,expr] RPAREN_TOK
@@ -835,7 +836,6 @@ term[CVC4::Expr& expr, CVC4::Expr& expr2]
       } else if(f.getKind() == CVC4::kind::EMPTYSET) {
         Debug("parser") << "Empty set encountered: " << f << " "
                           << f2 << " " << type <<  std::endl;
-        // TODO: what is f2 about, should we add some assertions?
         expr = MK_CONST( ::CVC4::EmptySet(type) );
       } else {
         if(f.getType() != type) {
@@ -879,34 +879,44 @@ term[CVC4::Expr& expr, CVC4::Expr& expr2]
         expr = MK_EXPR(kind, args);
       }
     }
-  | /* A non-built-in function application */
-    LPAREN_TOK
-    functionName[name, CHECK_DECLARED]
-    { PARSER_STATE->checkFunctionLike(name);
-      const bool isDefinedFunction =
-        PARSER_STATE->isDefinedFunction(name);
-      if(isDefinedFunction) {
-        expr = PARSER_STATE->getFunction(name);
-        kind = CVC4::kind::APPLY;
+  | LPAREN_TOK functionName[name, CHECK_NONE]
+    { isBuiltinOperator = PARSER_STATE->isOperatorEnabled(name);
+      if(isBuiltinOperator) {
+        /* A built-in operator not already handled by the lexer */
+        kind = PARSER_STATE->getOperatorKind(name);
       } else {
-        expr = PARSER_STATE->getVariable(name);
-        Type t = expr.getType();
-        if(t.isConstructor()) {
-          kind = CVC4::kind::APPLY_CONSTRUCTOR;
-        } else if(t.isSelector()) {
-          kind = CVC4::kind::APPLY_SELECTOR;
-        } else if(t.isTester()) {
-          kind = CVC4::kind::APPLY_TESTER;
+        /* A non-built-in function application */
+        PARSER_STATE->checkDeclaration(name, CHECK_DECLARED, SYM_VARIABLE);
+        PARSER_STATE->checkFunctionLike(name);
+        const bool isDefinedFunction =
+          PARSER_STATE->isDefinedFunction(name);
+        if(isDefinedFunction) {
+          expr = PARSER_STATE->getFunction(name);
+          kind = CVC4::kind::APPLY;
         } else {
-          kind = CVC4::kind::APPLY_UF;
+          expr = PARSER_STATE->getVariable(name);
+          Type t = expr.getType();
+          if(t.isConstructor()) {
+            kind = CVC4::kind::APPLY_CONSTRUCTOR;
+          } else if(t.isSelector()) {
+            kind = CVC4::kind::APPLY_SELECTOR;
+          } else if(t.isTester()) {
+            kind = CVC4::kind::APPLY_TESTER;
+          } else {
+            kind = CVC4::kind::APPLY_UF;
+          }
         }
+        args.push_back(expr);
       }
-      args.push_back(expr);
-    }
+        }
     termList[args,expr] RPAREN_TOK
     { Debug("parser") << "args has size " << args.size() << std::endl << "expr is " << expr << std::endl;
-      for(std::vector<Expr>::iterator i = args.begin(); i != args.end(); ++i)
+      for(std::vector<Expr>::iterator i = args.begin(); i != args.end(); ++i) {
         Debug("parser") << "++ " << *i << std::endl;
+      }
+      if(isBuiltinOperator) {
+        PARSER_STATE->checkOperator(kind, args.size());
+      }
       expr = MK_EXPR(kind, args); }
 
   | /* An indexed function application */
@@ -1283,14 +1293,6 @@ builtinOp[CVC4::Kind& kind]
                      if(PARSER_STATE->strictModeEnabled()) {
                        PARSER_STATE->parseError("bv2nat and int2bv are not part of SMT-LIB, and aren't available in SMT-LIB strict compliance mode");
                      } }
-  //NEW string
-  //STRCONS_TOK    { $kind = CVC4::kind::STRING_CONCAT; }
-  //STRREVCONS_TOK { $kind = CVC4::kind::STRING_CONCAT; }
-  //STRHEAD_TOK    { $kind = CVC4::kind::STRING_CONCAT; }
-  //STRTAIL_TOK    { $kind = CVC4::kind::STRING_CONCAT; }
-  //STRLAST_TOK    { $kind = CVC4::kind::STRING_CONCAT; }
-  //STRFIRST_TOK   { $kind = CVC4::kind::STRING_CONCAT; }
-  //OLD string
   | STRCON_TOK     { $kind = CVC4::kind::STRING_CONCAT; }
   | STRLEN_TOK     { $kind = CVC4::kind::STRING_LENGTH; }
   | STRSUB_TOK     { $kind = CVC4::kind::STRING_SUBSTR; }
@@ -1311,12 +1313,6 @@ builtinOp[CVC4::Kind& kind]
   | REPLUS_TOK     { $kind = CVC4::kind::REGEXP_PLUS; }
   | REOPT_TOK      { $kind = CVC4::kind::REGEXP_OPT; }
   | RERANGE_TOK    { $kind = CVC4::kind::REGEXP_RANGE; }
-  | SETUNION_TOK  { $kind = CVC4::kind::UNION; }
-  | SETINT_TOK    { $kind = CVC4::kind::INTERSECTION; }
-  | SETMINUS_TOK  { $kind = CVC4::kind::SETMINUS; }
-  | SETSUB_TOK    { $kind = CVC4::kind::SUBSET; }
-  | SETIN_TOK     { $kind = CVC4::kind::MEMBER; }
-  | SETSINGLETON_TOK { $kind = CVC4::kind::SET_SINGLETON; }
 
   // NOTE: Theory operators go here
   ;
@@ -1338,18 +1334,6 @@ functionName[std::string& name, CVC4::parser::DeclarationCheck check]
   ;
 
 /**
- * Matches an previously declared function symbol (returning an Expr)
- */
-functionSymbol[CVC4::Expr& fun]
-@declarations {
-  std::string name;
-}
-  : functionName[name,CHECK_DECLARED]
-    { PARSER_STATE->checkFunctionLike(name);
-      fun = PARSER_STATE->getVariable(name); }
-  ;
-
-/**
  * Matches a sequence of sort symbols and fills them into the given
  * vector.
  */
@@ -1421,12 +1405,14 @@ sortSymbol[CVC4::Type& t, CVC4::parser::DeclarationCheck check]
     }
   | LPAREN_TOK symbol[name,CHECK_NONE,SYM_SORT] sortList[args] RPAREN_TOK
     {
-      if(name == "Array") {
+      if(name == "Array" &&
+         PARSER_STATE->isTheoryEnabled(Smt2::THEORY_ARRAYS) ) {
         if(args.size() != 2) {
           PARSER_STATE->parseError("Illegal array type.");
         }
         t = EXPR_MANAGER->mkArrayType( args[0], args[1] );
-      } else if(name == "Set") {
+      } else if(name == "Set" &&
+                PARSER_STATE->isTheoryEnabled(Smt2::THEORY_SETS) ) {
         if(args.size() != 1) {
           PARSER_STATE->parseError("Illegal set type.");
         }
@@ -1682,15 +1668,6 @@ BVSGE_TOK : 'bvsge';
 BV2NAT_TOK : 'bv2nat';
 INT2BV_TOK : 'int2bv';
 
-//STRING
-//NEW
-//STRCONS_TOK : 'str.cons';
-//STRREVCONS_TOK : 'str.revcons';
-//STRHEAD_TOK : 'str.head';
-//STRTAIL_TOK : 'str.tail';
-//STRLAST_TOK : 'str.last';
-//STRFIRST_TOK : 'str.first';
-//OLD
 STRCON_TOK : 'str.++';
 STRLEN_TOK : 'str.len';
 STRSUB_TOK : 'str.substr' ;
@@ -1714,13 +1691,10 @@ RERANGE_TOK : 're.range';
 RENOSTR_TOK : 're.nostr';
 REALLCHAR_TOK : 're.allchar';
 
-SETUNION_TOK: 'union';
-SETINT_TOK: 'intersection';
-SETMINUS_TOK: 'setminus';
-SETSUB_TOK: 'subseteq';
-SETIN_TOK: 'in';
-SETSINGLETON_TOK: 'setenum';
-EMPTYSET_TOK: 'emptyset';
+EMPTYSET_TOK: 'emptyset'; // Other set theory operators are not
+                          // tokenized and handled directly when
+                          // processing a term
+
 
 /**
  * A sequence of printable ASCII characters (except backslash) that starts
diff --git a/src/parser/smt2/smt2.cpp b/src/parser/smt2/smt2.cpp
index b1621e9e5..b59880a5e 100644
--- a/src/parser/smt2/smt2.cpp
+++ b/src/parser/smt2/smt2.cpp
@@ -37,111 +37,121 @@ Smt2::Smt2(ExprManager* exprManager, Input* input, bool strictMode, bool parseOn
 }
 
 void Smt2::addArithmeticOperators() {
-  addOperator(kind::PLUS);
-  addOperator(kind::MINUS);
-  addOperator(kind::UMINUS);
-  addOperator(kind::MULT);
-  addOperator(kind::LT);
-  addOperator(kind::LEQ);
-  addOperator(kind::GT);
-  addOperator(kind::GEQ);
+  Parser::addOperator(kind::PLUS);
+  Parser::addOperator(kind::MINUS);
+  Parser::addOperator(kind::UMINUS);
+  Parser::addOperator(kind::MULT);
+  Parser::addOperator(kind::LT);
+  Parser::addOperator(kind::LEQ);
+  Parser::addOperator(kind::GT);
+  Parser::addOperator(kind::GEQ);
 }
 
 void Smt2::addBitvectorOperators() {
-  addOperator(kind::BITVECTOR_CONCAT);
-  addOperator(kind::BITVECTOR_AND);
-  addOperator(kind::BITVECTOR_OR);
-  addOperator(kind::BITVECTOR_XOR);
-  addOperator(kind::BITVECTOR_NOT);
-  addOperator(kind::BITVECTOR_NAND);
-  addOperator(kind::BITVECTOR_NOR);
-  addOperator(kind::BITVECTOR_XNOR);
-  addOperator(kind::BITVECTOR_COMP);
-  addOperator(kind::BITVECTOR_MULT);
-  addOperator(kind::BITVECTOR_PLUS);
-  addOperator(kind::BITVECTOR_SUB);
-  addOperator(kind::BITVECTOR_NEG);
-  addOperator(kind::BITVECTOR_UDIV);
-  addOperator(kind::BITVECTOR_UREM);
-  addOperator(kind::BITVECTOR_SDIV);
-  addOperator(kind::BITVECTOR_SREM);
-  addOperator(kind::BITVECTOR_SMOD);
-  addOperator(kind::BITVECTOR_SHL);
-  addOperator(kind::BITVECTOR_LSHR);
-  addOperator(kind::BITVECTOR_ASHR);
-  addOperator(kind::BITVECTOR_ULT);
-  addOperator(kind::BITVECTOR_ULE);
-  addOperator(kind::BITVECTOR_UGT);
-  addOperator(kind::BITVECTOR_UGE);
-  addOperator(kind::BITVECTOR_SLT);
-  addOperator(kind::BITVECTOR_SLE);
-  addOperator(kind::BITVECTOR_SGT);
-  addOperator(kind::BITVECTOR_SGE);
-  addOperator(kind::BITVECTOR_BITOF);
-  addOperator(kind::BITVECTOR_EXTRACT);
-  addOperator(kind::BITVECTOR_REPEAT);
-  addOperator(kind::BITVECTOR_ZERO_EXTEND);
-  addOperator(kind::BITVECTOR_SIGN_EXTEND);
-  addOperator(kind::BITVECTOR_ROTATE_LEFT);
-  addOperator(kind::BITVECTOR_ROTATE_RIGHT);
-
-  addOperator(kind::INT_TO_BITVECTOR);
-  addOperator(kind::BITVECTOR_TO_NAT);
+  Parser::addOperator(kind::BITVECTOR_CONCAT);
+  Parser::addOperator(kind::BITVECTOR_AND);
+  Parser::addOperator(kind::BITVECTOR_OR);
+  Parser::addOperator(kind::BITVECTOR_XOR);
+  Parser::addOperator(kind::BITVECTOR_NOT);
+  Parser::addOperator(kind::BITVECTOR_NAND);
+  Parser::addOperator(kind::BITVECTOR_NOR);
+  Parser::addOperator(kind::BITVECTOR_XNOR);
+  Parser::addOperator(kind::BITVECTOR_COMP);
+  Parser::addOperator(kind::BITVECTOR_MULT);
+  Parser::addOperator(kind::BITVECTOR_PLUS);
+  Parser::addOperator(kind::BITVECTOR_SUB);
+  Parser::addOperator(kind::BITVECTOR_NEG);
+  Parser::addOperator(kind::BITVECTOR_UDIV);
+  Parser::addOperator(kind::BITVECTOR_UREM);
+  Parser::addOperator(kind::BITVECTOR_SDIV);
+  Parser::addOperator(kind::BITVECTOR_SREM);
+  Parser::addOperator(kind::BITVECTOR_SMOD);
+  Parser::addOperator(kind::BITVECTOR_SHL);
+  Parser::addOperator(kind::BITVECTOR_LSHR);
+  Parser::addOperator(kind::BITVECTOR_ASHR);
+  Parser::addOperator(kind::BITVECTOR_ULT);
+  Parser::addOperator(kind::BITVECTOR_ULE);
+  Parser::addOperator(kind::BITVECTOR_UGT);
+  Parser::addOperator(kind::BITVECTOR_UGE);
+  Parser::addOperator(kind::BITVECTOR_SLT);
+  Parser::addOperator(kind::BITVECTOR_SLE);
+  Parser::addOperator(kind::BITVECTOR_SGT);
+  Parser::addOperator(kind::BITVECTOR_SGE);
+  Parser::addOperator(kind::BITVECTOR_BITOF);
+  Parser::addOperator(kind::BITVECTOR_EXTRACT);
+  Parser::addOperator(kind::BITVECTOR_REPEAT);
+  Parser::addOperator(kind::BITVECTOR_ZERO_EXTEND);
+  Parser::addOperator(kind::BITVECTOR_SIGN_EXTEND);
+  Parser::addOperator(kind::BITVECTOR_ROTATE_LEFT);
+  Parser::addOperator(kind::BITVECTOR_ROTATE_RIGHT);
+
+  Parser::addOperator(kind::INT_TO_BITVECTOR);
+  Parser::addOperator(kind::BITVECTOR_TO_NAT);
 }
 
 void Smt2::addStringOperators() {
-  addOperator(kind::STRING_CONCAT);
-  addOperator(kind::STRING_LENGTH);
-  //addOperator(kind::STRING_IN_REGEXP);
+  Parser::addOperator(kind::STRING_CONCAT);
+  Parser::addOperator(kind::STRING_LENGTH);
 }
 
 void Smt2::addTheory(Theory theory) {
   switch(theory) {
+  case THEORY_ARRAYS:
+    Parser::addOperator(kind::SELECT);
+    Parser::addOperator(kind::STORE);
+    break;
+
+  case THEORY_BITVECTORS:
+    addBitvectorOperators();
+    break;
+
   case THEORY_CORE:
     defineType("Bool", getExprManager()->booleanType());
     defineVar("true", getExprManager()->mkConst(true));
     defineVar("false", getExprManager()->mkConst(false));
-    addOperator(kind::AND);
-    addOperator(kind::DISTINCT);
-    addOperator(kind::EQUAL);
-    addOperator(kind::IFF);
-    addOperator(kind::IMPLIES);
-    addOperator(kind::ITE);
-    addOperator(kind::NOT);
-    addOperator(kind::OR);
-    addOperator(kind::XOR);
-    break;
-
-  case THEORY_ARRAYS:
-    addOperator(kind::SELECT);
-    addOperator(kind::STORE);
+    Parser::addOperator(kind::AND);
+    Parser::addOperator(kind::DISTINCT);
+    Parser::addOperator(kind::EQUAL);
+    Parser::addOperator(kind::IFF);
+    Parser::addOperator(kind::IMPLIES);
+    Parser::addOperator(kind::ITE);
+    Parser::addOperator(kind::NOT);
+    Parser::addOperator(kind::OR);
+    Parser::addOperator(kind::XOR);
     break;
 
   case THEORY_REALS_INTS:
     defineType("Real", getExprManager()->realType());
-    addOperator(kind::DIVISION);
-    addOperator(kind::TO_INTEGER);
-    addOperator(kind::IS_INTEGER);
-    addOperator(kind::TO_REAL);
+    Parser::addOperator(kind::DIVISION);
+    Parser::addOperator(kind::TO_INTEGER);
+    Parser::addOperator(kind::IS_INTEGER);
+    Parser::addOperator(kind::TO_REAL);
     // falling through on purpose, to add Ints part of Reals_Ints
-
   case THEORY_INTS:
     defineType("Int", getExprManager()->integerType());
     addArithmeticOperators();
-    addOperator(kind::INTS_DIVISION);
-    addOperator(kind::INTS_MODULUS);
-    addOperator(kind::ABS);
-    addOperator(kind::DIVISIBLE);
+    Parser::addOperator(kind::INTS_DIVISION);
+    Parser::addOperator(kind::INTS_MODULUS);
+    Parser::addOperator(kind::ABS);
+    Parser::addOperator(kind::DIVISIBLE);
     break;
 
   case THEORY_REALS:
     defineType("Real", getExprManager()->realType());
     addArithmeticOperators();
-    addOperator(kind::DIVISION);
+    Parser::addOperator(kind::DIVISION);
     break;
 
-  case THEORY_BITVECTORS:
-    addBitvectorOperators();
+  case THEORY_QUANTIFIERS:
+    break;
+
+  case THEORY_SETS:
+    addOperator(kind::UNION, "union");
+    addOperator(kind::INTERSECTION, "intersection");
+    addOperator(kind::SETMINUS, "setminus");
+    addOperator(kind::SUBSET, "subseteq");
+    addOperator(kind::MEMBER, "in");
+    addOperator(kind::SET_SINGLETON, "setenum");
     break;
 
   case THEORY_STRINGS:
@@ -149,7 +159,8 @@ void Smt2::addTheory(Theory theory) {
     addStringOperators();
     break;
 
-  case THEORY_QUANTIFIERS:
+  case THEORY_UF:
+    Parser::addOperator(kind::APPLY_UF);
     break;
 
   default:
@@ -159,6 +170,54 @@ void Smt2::addTheory(Theory theory) {
   }
 }
 
+void Smt2::addOperator(Kind kind, const std::string& name) {
+  Debug("parser") << "Smt2::addOperator( " << kind << ", " << name << " )"
+                  << std::endl;
+  Parser::addOperator(kind);
+  operatorKindMap[name] = kind;
+}
+
+Kind Smt2::getOperatorKind(const std::string& name) const {
+  // precondition: isOperatorEnabled(name)
+  return operatorKindMap.find(name)->second;
+}
+
+bool Smt2::isOperatorEnabled(const std::string& name) const {
+  return operatorKindMap.find(name) != operatorKindMap.end();
+}
+
+bool Smt2::isTheoryEnabled(Theory theory) const {
+  switch(theory) {
+  case THEORY_ARRAYS:
+    return d_logic.isTheoryEnabled(theory::THEORY_ARRAY);
+  case THEORY_BITVECTORS:
+    return d_logic.isTheoryEnabled(theory::THEORY_BV);
+  case THEORY_CORE:
+    return true;
+  case THEORY_INTS:
+    return d_logic.isTheoryEnabled(theory::THEORY_ARITH) &&
+      d_logic.areIntegersUsed() && ( !d_logic.areRealsUsed() );
+  case THEORY_REALS:
+    return d_logic.isTheoryEnabled(theory::THEORY_ARITH) &&
+      ( !d_logic.areIntegersUsed() ) && d_logic.areRealsUsed();
+  case THEORY_REALS_INTS:
+    return d_logic.isTheoryEnabled(theory::THEORY_ARITH) &&
+      d_logic.areIntegersUsed() && d_logic.areRealsUsed();
+  case THEORY_QUANTIFIERS:
+    return d_logic.isQuantified();
+  case THEORY_SETS:
+    return d_logic.isTheoryEnabled(theory::THEORY_SETS);
+  case THEORY_STRINGS:
+    return d_logic.isTheoryEnabled(theory::THEORY_STRINGS);
+  case THEORY_UF:
+    return d_logic.isTheoryEnabled(theory::THEORY_UF);
+  default:
+    std::stringstream ss;
+    ss << "internal error: unsupported theory " << theory;
+    throw ParserException(ss.str());
+  }
+}
+
 bool Smt2::logicIsSet() {
   return d_logicSet;
 }
@@ -171,7 +230,7 @@ void Smt2::setLogic(const std::string& name) {
   addTheory(THEORY_CORE);
 
   if(d_logic.isTheoryEnabled(theory::THEORY_UF)) {
-    addOperator(kind::APPLY_UF);
+    addTheory(THEORY_UF);
   }
 
   if(d_logic.isTheoryEnabled(theory::THEORY_ARITH)) {
@@ -194,6 +253,10 @@ void Smt2::setLogic(const std::string& name) {
     addTheory(THEORY_BITVECTORS);
   }
 
+  if(d_logic.isTheoryEnabled(theory::THEORY_SETS)) {
+    addTheory(THEORY_SETS);
+  }
+
   if(d_logic.isTheoryEnabled(theory::THEORY_STRINGS)) {
     addTheory(THEORY_STRINGS);
   }
diff --git a/src/parser/smt2/smt2.h b/src/parser/smt2/smt2.h
index 837adb15c..969892c5f 100644
--- a/src/parser/smt2/smt2.h
+++ b/src/parser/smt2/smt2.h
@@ -44,12 +44,15 @@ public:
     THEORY_REALS,
     THEORY_REALS_INTS,
     THEORY_QUANTIFIERS,
-    THEORY_STRINGS
+    THEORY_SETS,
+    THEORY_STRINGS,
+    THEORY_UF
   };
 
 private:
   bool d_logicSet;
   LogicInfo d_logic;
+  std::hash_map<std::string, Kind, StringHashFunction> operatorKindMap;
 
 protected:
   Smt2(ExprManager* exprManager, Input* input, bool strictMode = false, bool parseOnly = false);
@@ -62,6 +65,14 @@ public:
    */
   void addTheory(Theory theory);
 
+  void addOperator(Kind k, const std::string& name);
+
+  Kind getOperatorKind(const std::string& name) const;
+
+  bool isOperatorEnabled(const std::string& name) const;
+
+  bool isTheoryEnabled(Theory theory) const;
+
   bool logicIsSet();
 
   /**