Refactor parser to define fewer tokens for symbols (#2936)

27 files changed, 459 insertions, 495 deletions

diff --git a/src/expr/symbol_table.cpp b/src/expr/symbol_table.cpp
index 600f666bc..dd75170b5 100644
--- a/src/expr/symbol_table.cpp
+++ b/src/expr/symbol_table.cpp
@@ -456,7 +456,7 @@ bool SymbolTable::Implementation::isBound(const string& name) const {
 
 bool SymbolTable::Implementation::isBoundDefinedFunction(
     const string& name) const {
-  CDHashMap<string, Expr>::iterator found = d_exprMap->find(name);
+  CDHashMap<string, Expr>::const_iterator found = d_exprMap->find(name);
   return found != d_exprMap->end() && d_functions->contains((*found).second);
 }
 
diff --git a/src/parser/parser.cpp b/src/parser/parser.cpp
index 28489154a..5e036ee69 100644
--- a/src/parser/parser.cpp
+++ b/src/parser/parser.cpp
@@ -47,8 +47,7 @@ Parser::Parser(api::Solver* solver,
                Input* input,
                bool strictMode,
                bool parseOnly)
-    : d_solver(solver),
-      d_resourceManager(d_solver->getExprManager()->getResourceManager()),
+    : d_resourceManager(solver->getExprManager()->getResourceManager()),
       d_input(input),
       d_symtabAllocated(),
       d_symtab(&d_symtabAllocated),
@@ -61,7 +60,8 @@ Parser::Parser(api::Solver* solver,
       d_parseOnly(parseOnly),
       d_canIncludeFile(true),
       d_logicIsForced(false),
-      d_forcedLogic()
+      d_forcedLogic(),
+      d_solver(solver)
 {
   d_input->setParser(*this);
 }
diff --git a/src/parser/parser.h b/src/parser/parser.h
index 826d460b2..fcc37d5d3 100644
--- a/src/parser/parser.h
+++ b/src/parser/parser.h
@@ -137,9 +137,6 @@ inline std::ostream& operator<<(std::ostream& out, SymbolType type) {
 class CVC4_PUBLIC Parser {
   friend class ParserBuilder;
 private:
- /** The API Solver object. */
- api::Solver* d_solver;
-
  /** The resource manager associated with this expr manager */
  ResourceManager* d_resourceManager;
 
@@ -244,6 +241,9 @@ private:
  Expr getSymbol(const std::string& var_name, SymbolType type);
 
 protected:
+ /** The API Solver object. */
+ api::Solver* d_solver;
+
  /**
   * Create a parser state.
   *
diff --git a/src/parser/smt2/Smt2.g b/src/parser/smt2/Smt2.g
index b224032e8..4a30841e6 100644
--- a/src/parser/smt2/Smt2.g
+++ b/src/parser/smt2/Smt2.g
@@ -891,14 +891,7 @@ sygusGTerm[CVC4::SygusGTerm& sgt, std::string& fun]
 }
   : LPAREN_TOK
     //read operator
-    ( builtinOp[k]{ 
-        Debug("parser-sygus") << "Sygus grammar " << fun << " : builtin op : "
-                              << name << std::endl;
-        sgt.d_name = kind::kindToString(k);
-        sgt.d_gterm_type = SygusGTerm::gterm_op;
-        sgt.d_expr = EXPR_MANAGER->operatorOf(k);
-      }
-     | SYGUS_LET_TOK LPAREN_TOK { 
+    ( SYGUS_LET_TOK LPAREN_TOK {
          sgt.d_name = std::string("let");
          sgt.d_gterm_type = SygusGTerm::gterm_let;
          PARSER_STATE->pushScope(true);
@@ -1645,12 +1638,6 @@ simpleSymbolicExprNoKeyword[CVC4::SExpr& sexpr]
         | DECLARE_DATATYPES_TOK | GET_MODEL_TOK | ECHO_TOK | REWRITE_RULE_TOK
         | REDUCTION_RULE_TOK | PROPAGATION_RULE_TOK | SIMPLIFY_TOK)
     { sexpr = SExpr(SExpr::Keyword(AntlrInput::tokenText($tok))); }
-  | builtinOp[k]
-    { std::stringstream ss;
-      ss << language::SetLanguage(CVC4::language::output::LANG_SMTLIB_V2_5)
-         << EXPR_MANAGER->mkConst(k);
-      sexpr = SExpr(ss.str());
-    }
   ;
 
 keyword[std::string& s]
@@ -1700,10 +1687,10 @@ termNonVariable[CVC4::Expr& expr, CVC4::Expr& expr2]
   Debug("parser") << "term: " << AntlrInput::tokenText(LT(1)) << std::endl;
   Kind kind = kind::NULL_EXPR;
   Expr op;
-  std::string name, name2;
+  std::string name;
   std::vector<Expr> args;
   std::vector< std::pair<std::string, Type> > sortedVarNames;
-  Expr f, f2, f3, f4;
+  Expr f, f2, f3;
   std::string attr;
   Expr attexpr;
   std::vector<Expr> patexprs;
@@ -1719,49 +1706,7 @@ termNonVariable[CVC4::Expr& expr, CVC4::Expr& expr2]
   Type type2;
   api::Term atomTerm;
 }
-  : /* a built-in operator application */
-    LPAREN_TOK builtinOp[kind] termList[args,expr] RPAREN_TOK
-    {
-      if( !PARSER_STATE->strictModeEnabled() &&
-          (kind == CVC4::kind::AND || kind == CVC4::kind::OR) &&
-          args.size() == 1) {
-        /* Unary AND/OR can be replaced with the argument.
-         * It just so happens expr should already be the only argument. */
-        assert( expr == args[0] );
-      } else if( CVC4::kind::isAssociative(kind) &&
-                 args.size() > EXPR_MANAGER->maxArity(kind) ) {
-        /* Special treatment for associative operators with lots of children */
-        expr = EXPR_MANAGER->mkAssociative(kind, args);
-      } else if( kind == CVC4::kind::MINUS && args.size() == 1 ) {
-        expr = MK_EXPR(CVC4::kind::UMINUS, args[0]);
-      }
-      else if ((kind == CVC4::kind::XOR || kind == CVC4::kind::MINUS
-                || kind == CVC4::kind::DIVISION)
-               && args.size() > 2)
-      {
-        /* left-associative, but CVC4 internally only supports 2 args */
-        expr = EXPR_MANAGER->mkLeftAssociative(kind,args);
-      } else if( kind == CVC4::kind::IMPLIES && args.size() > 2 ) {
-        /* right-associative, but CVC4 internally only supports 2 args */
-        expr = EXPR_MANAGER->mkRightAssociative(kind,args);
-      } else if( ( kind == CVC4::kind::EQUAL ||
-                   kind == CVC4::kind::LT || kind == CVC4::kind::GT ||
-                   kind == CVC4::kind::LEQ || kind == CVC4::kind::GEQ ) &&
-                 args.size() > 2 ) {
-        /* "chainable", but CVC4 internally only supports 2 args */
-        expr = MK_EXPR(MK_CONST(Chain(kind)), args);
-      } else if( PARSER_STATE->strictModeEnabled() && kind == CVC4::kind::ABS &&
-                 args.size() == 1 && !args[0].getType().isInteger() ) {
-        /* first, check that ABS is even defined in this logic */
-        PARSER_STATE->checkOperator(kind, args.size());
-        PARSER_STATE->parseError("abs can only be applied to Int, not Real, "
-                                 "while in strict SMT-LIB compliance mode");
-      } else {
-        PARSER_STATE->checkOperator(kind, args.size());
-        expr = MK_EXPR(kind, args);
-      }
-    }
-  | LPAREN_TOK AS_TOK ( termNonVariable[f, f2] | symbol[name,CHECK_DECLARED,SYM_VARIABLE] { readVariable = true; } ) 
+  : LPAREN_TOK AS_TOK ( termNonVariable[f, f2] | symbol[name,CHECK_DECLARED,SYM_VARIABLE] { readVariable = true; } )
     sortSymbol[type, CHECK_DECLARED] RPAREN_TOK
     {
       if(readVariable) {
@@ -1843,7 +1788,7 @@ termNonVariable[CVC4::Expr& expr, CVC4::Expr& expr2]
   | LPAREN_TOK functionName[name, CHECK_NONE]
     { isBuiltinOperator = PARSER_STATE->isOperatorEnabled(name);
       if(isBuiltinOperator) {
-        /* A built-in operator not already handled by the lexer */
+        /* A built-in operator */
         kind = PARSER_STATE->getOperatorKind(name);
       } else {
         /* A non-built-in function application */
@@ -1883,17 +1828,69 @@ termNonVariable[CVC4::Expr& expr, CVC4::Expr& expr2]
           PARSER_STATE->parseError("Cannot find unambiguous overloaded function for argument types.");
         }
       }
-      Kind lassocKind = CVC4::kind::UNDEFINED_KIND;
-      if (args.size() >= 2)
+
+      bool done = false;
+      if (isBuiltinOperator)
       {
-        if (kind == CVC4::kind::INTS_DIVISION
-            || (kind == CVC4::kind::BITVECTOR_XNOR && PARSER_STATE->v2_6()))
+        if (args.size() > 2)
         {
-          // Builtin operators that are not tokenized, are left associative,
-          // but not internally variadic must set this.
-          lassocKind = kind;
+          if (kind == CVC4::kind::INTS_DIVISION || kind == CVC4::kind::XOR
+              || kind == CVC4::kind::MINUS || kind == CVC4::kind::DIVISION
+              || (kind == CVC4::kind::BITVECTOR_XNOR && PARSER_STATE->v2_6()))
+          {
+            // Builtin operators that are not tokenized, are left associative,
+            // but not internally variadic must set this.
+            expr =
+                EXPR_MANAGER->mkLeftAssociative(kind, args);
+            done = true;
+          }
+          else if (kind == CVC4::kind::IMPLIES)
+          {
+            /* right-associative, but CVC4 internally only supports 2 args */
+            expr = EXPR_MANAGER->mkRightAssociative(kind, args);
+            done = true;
+          }
+          else if (kind == CVC4::kind::EQUAL || kind == CVC4::kind::LT
+                   || kind == CVC4::kind::GT || kind == CVC4::kind::LEQ
+                   || kind == CVC4::kind::GEQ)
+          {
+            /* "chainable", but CVC4 internally only supports 2 args */
+            expr = MK_EXPR(MK_CONST(Chain(kind)), args);
+            done = true;
+          }
+        }
+
+        if (!done)
+        {
+          if (CVC4::kind::isAssociative(kind)
+              && args.size() > EXPR_MANAGER->maxArity(kind))
+          {
+            /* Special treatment for associative operators with lots of children
+             */
+            expr = EXPR_MANAGER->mkAssociative(kind, args);
+          }
+          else if (!PARSER_STATE->strictModeEnabled()
+                   && (kind == CVC4::kind::AND || kind == CVC4::kind::OR)
+                   && args.size() == 1)
+          {
+            /* Unary AND/OR can be replaced with the argument.
+             * It just so happens expr should already be the only argument. */
+            assert(expr == args[0]);
+          }
+          else if (kind == CVC4::kind::MINUS && args.size() == 1)
+          {
+            expr = MK_EXPR(CVC4::kind::UMINUS, args[0]);
+          }
+          else
+          {
+            PARSER_STATE->checkOperator(kind, args.size());
+            expr = MK_EXPR(kind, args);
+          }
         }
-        else
+      }
+      else
+      {
+        if (args.size() >= 2)
         {
           // may be partially applied function, in this case we use HO_APPLY
           Type argt = args[0].getType();
@@ -1906,22 +1903,17 @@ termNonVariable[CVC4::Expr& expr, CVC4::Expr& expr2]
               Debug("parser") << " : #argTypes = " << arity;
               Debug("parser") << ", #args = " << args.size() - 1 << std::endl;
               // must curry the partial application
-              lassocKind = CVC4::kind::HO_APPLY;
+              expr =
+                  EXPR_MANAGER->mkLeftAssociative(CVC4::kind::HO_APPLY, args);
+              done = true;
             }
           }
         }
-      }
-      if (lassocKind != CVC4::kind::UNDEFINED_KIND)
-      {
-        expr = EXPR_MANAGER->mkLeftAssociative(lassocKind, args);
-      }
-      else
-      {
-        if (isBuiltinOperator)
+
+        if (!done)
         {
-          PARSER_STATE->checkOperator(kind, args.size());
+          expr = MK_EXPR(kind, args);
         }
-        expr = MK_EXPR(kind, args);
       }
     }
   | LPAREN_TOK
@@ -2023,9 +2015,11 @@ termNonVariable[CVC4::Expr& expr, CVC4::Expr& expr2]
           }
           binders.push_back(std::make_pair(name, expr)); } )+ )
     { // now implement these bindings
-      for(std::vector< std::pair<std::string, Expr> >::iterator
-            i = binders.begin(); i != binders.end(); ++i) {
-        PARSER_STATE->defineVar((*i).first, (*i).second);
+      for (const std::pair<std::string, Expr>& binder : binders)
+      {
+        {
+          PARSER_STATE->defineVar(binder.first, binder.second);
+        }
       }
     }
     RPAREN_TOK
@@ -2240,6 +2234,7 @@ termAtomic[CVC4::api::Term& atomTerm]
   Type type;
   Type type2;
   std::string s;
+  std::vector<uint64_t> numerals;
 }
     /* constants */
   : INTEGER_LITERAL
@@ -2254,65 +2249,24 @@ termAtomic[CVC4::api::Term& atomTerm]
                                         SOLVER->getRealSort());
     }
 
-  // Pi constant
-  | REAL_PI_TOK { atomTerm = SOLVER->mkPi(); }
-
   // Constants using indexed identifiers, e.g. (_ +oo 8 24) (positive infinity
   // as a 32-bit floating-point constant)
   | LPAREN_TOK INDEX_TOK 
-    ( bvLit=SIMPLE_SYMBOL size=INTEGER_LITERAL 
-      {
-        if(AntlrInput::tokenText($bvLit).find("bv") == 0)
-        {
-          std::string bvStr = AntlrInput::tokenTextSubstr($bvLit, 2);
-          uint32_t bvSize = AntlrInput::tokenToUnsigned($size);
-          atomTerm = SOLVER->mkBitVector(bvSize, bvStr, 10);
-        }
-        else
-        {
-           PARSER_STATE->parseError("Unexpected symbol `" +
-                                    AntlrInput::tokenText($bvLit) + "'");
-        }
-      }
-
-    // Floating-point constants
-    | FP_PINF_TOK eb=INTEGER_LITERAL sb=INTEGER_LITERAL
-      {
-        atomTerm = SOLVER->mkPosInf(AntlrInput::tokenToUnsigned($eb),
-                                AntlrInput::tokenToUnsigned($sb));
-      }
-    | FP_NINF_TOK eb=INTEGER_LITERAL sb=INTEGER_LITERAL
-      {
-        atomTerm = SOLVER->mkNegInf(AntlrInput::tokenToUnsigned($eb),
-                                AntlrInput::tokenToUnsigned($sb));
-      }
-    | FP_NAN_TOK eb=INTEGER_LITERAL sb=INTEGER_LITERAL
-      {
-        atomTerm = SOLVER->mkNaN(AntlrInput::tokenToUnsigned($eb),
-                             AntlrInput::tokenToUnsigned($sb));
-      }
-    | FP_PZERO_TOK eb=INTEGER_LITERAL sb=INTEGER_LITERAL
-      {
-        atomTerm = SOLVER->mkPosZero(AntlrInput::tokenToUnsigned($eb),
-                                 AntlrInput::tokenToUnsigned($sb));
-      }
-    | FP_NZERO_TOK eb=INTEGER_LITERAL sb=INTEGER_LITERAL
-      {
-        atomTerm = SOLVER->mkNegZero(AntlrInput::tokenToUnsigned($eb),
-                                 AntlrInput::tokenToUnsigned($sb));
-      }
-
-    // Empty heap constant in seperation logic
-    | EMP_TOK
+    ( EMP_TOK
       sortSymbol[type,CHECK_DECLARED]
       sortSymbol[type2,CHECK_DECLARED]
       {
+        // Empty heap constant in seperation logic
         api::Term v1 = SOLVER->mkConst(api::Sort(type), "_emp1");
         api::Term v2 = SOLVER->mkConst(api::Sort(type2), "_emp2");
         atomTerm = SOLVER->mkTerm(api::SEP_EMP, v1, v2);
       }
-
-    // NOTE: Theory parametric constants go here
+    | sym=SIMPLE_SYMBOL nonemptyNumeralList[numerals]
+      {
+        atomTerm =
+          PARSER_STATE->mkIndexedConstant(AntlrInput::tokenText($sym),
+                                          numerals);
+      }
     )
     RPAREN_TOK
 
@@ -2330,42 +2284,9 @@ termAtomic[CVC4::api::Term& atomTerm]
       atomTerm = SOLVER->mkBitVector(binStr, 2);
     }
 
-  // Floating-point rounding mode constants
-  | FP_RNE_TOK      { atomTerm = SOLVER->mkRoundingMode(api::ROUND_NEAREST_TIES_TO_EVEN); }
-  | FP_RNA_TOK      { atomTerm = SOLVER->mkRoundingMode(api::ROUND_NEAREST_TIES_TO_AWAY); }
-  | FP_RTP_TOK      { atomTerm = SOLVER->mkRoundingMode(api::ROUND_TOWARD_POSITIVE); }
-  | FP_RTN_TOK      { atomTerm = SOLVER->mkRoundingMode(api::ROUND_TOWARD_NEGATIVE); }
-  | FP_RTZ_TOK      { atomTerm = SOLVER->mkRoundingMode(api::ROUND_TOWARD_ZERO); }
-  | FP_RNE_FULL_TOK { atomTerm = SOLVER->mkRoundingMode(api::ROUND_NEAREST_TIES_TO_EVEN); }
-  | FP_RNA_FULL_TOK { atomTerm = SOLVER->mkRoundingMode(api::ROUND_NEAREST_TIES_TO_AWAY); }
-  | FP_RTP_FULL_TOK { atomTerm = SOLVER->mkRoundingMode(api::ROUND_TOWARD_POSITIVE); }
-  | FP_RTN_FULL_TOK { atomTerm = SOLVER->mkRoundingMode(api::ROUND_TOWARD_NEGATIVE); }
-  | FP_RTZ_FULL_TOK { atomTerm = SOLVER->mkRoundingMode(api::ROUND_TOWARD_ZERO); }
-
   // String constant
   | str[s,false] { atomTerm = SOLVER->mkString(s, true); }
 
-  // Regular expression constants
-  | RENOSTR_TOK { atomTerm = SOLVER->mkRegexpEmpty(); }
-  | REALLCHAR_TOK { atomTerm = SOLVER->mkRegexpSigma(); }
-
-  // Set constants
-  | EMPTYSET_TOK { atomTerm = SOLVER->mkEmptySet(SOLVER->getNullSort()); }
-  | UNIVSET_TOK
-    {
-      // the Boolean sort is a placeholder here since we don't have type info
-      // without type annotation
-      atomTerm = SOLVER->mkUniverseSet(SOLVER->getBooleanSort());
-    }
-
-  // Separation logic constants
-  | NILREF_TOK
-    {
-      // the Boolean sort is a placeholder here since we don't have type info
-      // without type annotation
-      atomTerm = SOLVER->mkSepNil(SOLVER->getBooleanSort());
-    }
-
   // NOTE: Theory constants go here
     
   // Empty tuple constant
@@ -2525,64 +2446,10 @@ indexedFunctionName[CVC4::Expr& op, CVC4::Kind& kind]
 @init {
   Expr expr;
   Expr expr2;
+  std::vector<uint64_t> numerals;
 }
   : LPAREN_TOK INDEX_TOK
-    ( 'extract' n1=INTEGER_LITERAL n2=INTEGER_LITERAL
-      { op = MK_CONST(BitVectorExtract(AntlrInput::tokenToUnsigned($n1),
-                                       AntlrInput::tokenToUnsigned($n2))); }
-    | 'repeat' n=INTEGER_LITERAL
-      { op = MK_CONST(BitVectorRepeat(AntlrInput::tokenToUnsigned($n))); }
-    | 'zero_extend' n=INTEGER_LITERAL
-      { op = MK_CONST(BitVectorZeroExtend(AntlrInput::tokenToUnsigned($n))); }
-    | 'sign_extend' n=INTEGER_LITERAL
-      { op = MK_CONST(BitVectorSignExtend(AntlrInput::tokenToUnsigned($n))); }
-    | 'rotate_left' n=INTEGER_LITERAL
-      { op = MK_CONST(BitVectorRotateLeft(AntlrInput::tokenToUnsigned($n))); }
-    | 'rotate_right' n=INTEGER_LITERAL
-      { op = MK_CONST(BitVectorRotateRight(AntlrInput::tokenToUnsigned($n))); }
-    | DIVISIBLE_TOK n=INTEGER_LITERAL
-      { op = MK_CONST(Divisible(AntlrInput::tokenToUnsigned($n))); }
-    | INT2BV_TOK n=INTEGER_LITERAL
-      { op = MK_CONST(IntToBitVector(AntlrInput::tokenToUnsigned($n)));
-        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");
-        } }
-    | FP_TO_FP_TOK eb=INTEGER_LITERAL sb=INTEGER_LITERAL
-      { op = MK_CONST(FloatingPointToFPGeneric(
-                AntlrInput::tokenToUnsigned($eb),
-                AntlrInput::tokenToUnsigned($sb)));
-      }
-    | FP_TO_FPBV_TOK eb=INTEGER_LITERAL sb=INTEGER_LITERAL
-      { op = MK_CONST(FloatingPointToFPIEEEBitVector(
-                AntlrInput::tokenToUnsigned($eb),
-                AntlrInput::tokenToUnsigned($sb)));
-      }
-    | FP_TO_FPFP_TOK eb=INTEGER_LITERAL sb=INTEGER_LITERAL
-      { op = MK_CONST(FloatingPointToFPFloatingPoint(
-                AntlrInput::tokenToUnsigned($eb),
-                AntlrInput::tokenToUnsigned($sb)));
-      }
-    | FP_TO_FPR_TOK eb=INTEGER_LITERAL sb=INTEGER_LITERAL
-      { op = MK_CONST(FloatingPointToFPReal(AntlrInput::tokenToUnsigned($eb),
-                                            AntlrInput::tokenToUnsigned($sb)));
-      }
-    | FP_TO_FPS_TOK eb=INTEGER_LITERAL sb=INTEGER_LITERAL
-      { op = MK_CONST(FloatingPointToFPSignedBitVector(
-                AntlrInput::tokenToUnsigned($eb),
-                AntlrInput::tokenToUnsigned($sb)));
-      }
-    | FP_TO_FPU_TOK eb=INTEGER_LITERAL sb=INTEGER_LITERAL
-      { op = MK_CONST(FloatingPointToFPUnsignedBitVector(
-                AntlrInput::tokenToUnsigned($eb),
-                AntlrInput::tokenToUnsigned($sb)));
-      }
-    | FP_TO_UBV_TOK m=INTEGER_LITERAL
-      { op = MK_CONST(FloatingPointToUBV(AntlrInput::tokenToUnsigned($m))); }
-    | FP_TO_SBV_TOK m=INTEGER_LITERAL
-      { op = MK_CONST(FloatingPointToSBV(AntlrInput::tokenToUnsigned($m))); }
-    | TESTER_TOK term[expr, expr2] { 
+    ( TESTER_TOK term[expr, expr2] {
         if( expr.getKind()==kind::APPLY_CONSTRUCTOR && expr.getNumChildren()==0 ){
           //for nullary constructors, must get the operator
           expr = expr.getOperator();
@@ -2598,26 +2465,16 @@ indexedFunctionName[CVC4::Expr& op, CVC4::Kind& kind]
         //put m in op so that the caller (termNonVariable) can deal with this case
         op = MK_CONST(Rational(AntlrInput::tokenToUnsigned($m)));
       } 
-    | badIndexedFunctionName
+    | sym=SIMPLE_SYMBOL nonemptyNumeralList[numerals]
+      {
+        op = PARSER_STATE->mkIndexedOp(AntlrInput::tokenText($sym), numerals)
+                 .getExpr();
+      }
     )
     RPAREN_TOK
   ;
 
 /**
- * Matches an erroneous indexed function name (and args) for better
- * error reporting.
- */
-badIndexedFunctionName
-@declarations {
-  std::string name;
-}
-  : id=(SIMPLE_SYMBOL | QUOTED_SYMBOL | UNTERMINATED_QUOTED_SYMBOL)
-    { PARSER_STATE->parseError(std::string("Unknown indexed function `") +
-          AntlrInput::tokenText($id) + "'");
-    }
-  ;
-
-/**
  * Matches a sequence of terms and puts them into the formulas
  * vector.
  * @param formulas the vector to fill with terms
@@ -2682,56 +2539,6 @@ str[std::string& s, bool fsmtlib]
     }
   ;
 
-/**
- * Matches a builtin operator symbol and sets kind to its associated Expr kind.
- */
-builtinOp[CVC4::Kind& kind]
-@init {
-  Debug("parser") << "builtin: " << AntlrInput::tokenText(LT(1)) << std::endl;
-}
-  : NOT_TOK      { $kind = CVC4::kind::NOT;     }
-  | IMPLIES_TOK  { $kind = CVC4::kind::IMPLIES; }
-  | AND_TOK      { $kind = CVC4::kind::AND;     }
-  | OR_TOK       { $kind = CVC4::kind::OR;      }
-  | XOR_TOK      { $kind = CVC4::kind::XOR;     }
-  | EQUAL_TOK    { $kind = CVC4::kind::EQUAL;   }
-  | DISTINCT_TOK { $kind = CVC4::kind::DISTINCT; }
-  | ITE_TOK      { $kind = CVC4::kind::ITE; }
-  | GREATER_THAN_TOK
-                 { $kind = CVC4::kind::GT; }
-  | GREATER_THAN_EQUAL_TOK
-                 { $kind = CVC4::kind::GEQ; }
-  | LESS_THAN_EQUAL_TOK
-                 { $kind = CVC4::kind::LEQ; }
-  | LESS_THAN_TOK
-                 { $kind = CVC4::kind::LT; }
-  | PLUS_TOK     { $kind = CVC4::kind::PLUS; }
-  | MINUS_TOK    { $kind = CVC4::kind::MINUS; }
-  | STAR_TOK     { $kind = CVC4::kind::MULT; }
-  | DIV_TOK      { $kind = CVC4::kind::DIVISION; }
-
-  | BV2NAT_TOK
-    { $kind = CVC4::kind::BITVECTOR_TO_NAT;
-      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");
-      }
-    }
-
-  | DTSIZE_TOK       { $kind = CVC4::kind::DT_SIZE; }
-  | FMFCARD_TOK      { $kind = CVC4::kind::CARDINALITY_CONSTRAINT; }
-  | FMFCARDVAL_TOK   { $kind = CVC4::kind::CARDINALITY_VALUE; }
-  | INST_CLOSURE_TOK { $kind = CVC4::kind::INST_CLOSURE; }
-  
-  // NOTE: Theory operators no longer go here, add to smt2.cpp. Only
-  // special cases may go here. When this comment was written (2015
-  // Apr), the special cases were: core theory operators, arith
-  // operators which start with symbols like * / + >= etc, quantifier
-  // theory operators, and operators which depended on parser's state
-  // to accept or reject.
-  ;
-
 quantOp[CVC4::Kind& kind]
 @init {
   Debug("parser") << "quant: " << AntlrInput::tokenText(LT(1)) << std::endl;
@@ -2923,10 +2730,10 @@ symbol[std::string& id,
         PARSER_STATE->checkDeclaration(id, check, type);
       }
     }
-  | ( 'repeat' { id = "repeat"; }
+  |
     /* these are keywords in SyGuS but we don't want to inhibit their
      * use as symbols in SMT-LIB */
-    | SET_OPTIONS_TOK { id = "set-options"; }
+    ( SET_OPTIONS_TOK { id = "set-options"; }
     | DECLARE_VAR_TOK { id = "declare-var"; }
     | DECLARE_PRIMED_VAR_TOK { id = "declare-primed-var"; }
     | SYNTH_FUN_TOK { id = "synth-fun"; }
@@ -3049,7 +2856,6 @@ GET_UNSAT_CORE_TOK : 'get-unsat-core';
 EXIT_TOK : 'exit';
 RESET_TOK : { PARSER_STATE->v2_5() }? 'reset';
 RESET_ASSERTIONS_TOK : 'reset-assertions';
-ITE_TOK : 'ite';
 LET_TOK : { !PARSER_STATE->sygus() }? 'let';
 SYGUS_LET_TOK : { PARSER_STATE->sygus() }? 'let';
 ATTRIBUTE_TOK : '!';
@@ -3065,7 +2871,7 @@ GET_OPTION_TOK : 'get-option';
 PUSH_TOK : 'push';
 POP_TOK : 'pop';
 AS_TOK : 'as';
-CONST_TOK : 'const';
+CONST_TOK : { !PARSER_STATE->strictModeEnabled() }? 'const';
 
 // extended commands
 DECLARE_CODATATYPE_TOK : { PARSER_STATE->v2_6() || PARSER_STATE->sygus() }? 'declare-codatatype';
@@ -3093,17 +2899,16 @@ INCLUDE_TOK : 'include';
 GET_QE_TOK : 'get-qe';
 GET_QE_DISJUNCT_TOK : 'get-qe-disjunct';
 DECLARE_HEAP : 'declare-heap';
-EMP_TOK : 'emp';
 
 // SyGuS commands
-SYNTH_FUN_TOK : 'synth-fun';
-SYNTH_INV_TOK : 'synth-inv';
-CHECK_SYNTH_TOK : 'check-synth';
-DECLARE_VAR_TOK : 'declare-var';
-DECLARE_PRIMED_VAR_TOK : 'declare-primed-var';
-CONSTRAINT_TOK : 'constraint';
-INV_CONSTRAINT_TOK : 'inv-constraint';
-SET_OPTIONS_TOK : 'set-options';
+SYNTH_FUN_TOK : { PARSER_STATE->sygus() }? 'synth-fun';
+SYNTH_INV_TOK : { PARSER_STATE->sygus() }? 'synth-inv';
+CHECK_SYNTH_TOK : { PARSER_STATE->sygus() }? 'check-synth';
+DECLARE_VAR_TOK : { PARSER_STATE->sygus() }? 'declare-var';
+DECLARE_PRIMED_VAR_TOK : { PARSER_STATE->sygus() }? 'declare-primed-var';
+CONSTRAINT_TOK : { PARSER_STATE->sygus() }? 'constraint';
+INV_CONSTRAINT_TOK : { PARSER_STATE->sygus() }? 'inv-constraint';
+SET_OPTIONS_TOK : { PARSER_STATE->sygus() }? 'set-options';
 SYGUS_CONSTANT_TOK : { PARSER_STATE->sygus() }? 'Constant';
 SYGUS_VARIABLE_TOK : { PARSER_STATE->sygus() }? 'Variable';
 SYGUS_INPUT_VARIABLE_TOK : { PARSER_STATE->sygus() }? 'InputVariable';
@@ -3117,80 +2922,12 @@ ATTRIBUTE_INST_LEVEL : ':quant-inst-max-level';
 ATTRIBUTE_RR_PRIORITY : ':rr-priority';
 
 // operators (NOTE: theory symbols go here)
-AMPERSAND_TOK     : '&';
-AND_TOK           : 'and';
-AT_TOK            : '@';
-DISTINCT_TOK      : 'distinct';
-DIV_TOK           : '/';
-EQUAL_TOK         : '=';
 EXISTS_TOK        : 'exists';
 FORALL_TOK        : 'forall';
-GREATER_THAN_TOK  : '>';
-GREATER_THAN_EQUAL_TOK  : '>=';
-IMPLIES_TOK       : '=>';
-LESS_THAN_TOK     : '<';
-LESS_THAN_EQUAL_TOK     : '<=';
-MINUS_TOK         : '-';
-NOT_TOK           : 'not';
-OR_TOK            : 'or';
-// PERCENT_TOK       : '%';
-PLUS_TOK          : '+';
-//POUND_TOK         : '#';
-STAR_TOK          : '*';
-// TILDE_TOK         : '~';
-XOR_TOK           : 'xor';
-
-
-DIVISIBLE_TOK : 'divisible';
-
-BV2NAT_TOK : 'bv2nat';
-INT2BV_TOK : 'int2bv';
-
-RENOSTR_TOK : 're.nostr';
-REALLCHAR_TOK : 're.allchar';
-
-DTSIZE_TOK : 'dt.size';
-
-FMFCARD_TOK : 'fmf.card';
-FMFCARDVAL_TOK : 'fmf.card.val';
-
-INST_CLOSURE_TOK : 'inst-closure';
 
-EMPTYSET_TOK: { PARSER_STATE->isTheoryEnabled(Smt2::THEORY_SETS) }? 'emptyset';
-UNIVSET_TOK: { PARSER_STATE->isTheoryEnabled(Smt2::THEORY_SETS) }? 'univset';
-NILREF_TOK: { PARSER_STATE->isTheoryEnabled(Smt2::THEORY_SEP) }? 'sep.nil';
+EMP_TOK : { PARSER_STATE->isTheoryEnabled(Smt2::THEORY_SEP) }? 'emp';
 TUPLE_CONST_TOK: { PARSER_STATE->isTheoryEnabled(Smt2::THEORY_DATATYPES) }? 'mkTuple';
 TUPLE_SEL_TOK: { PARSER_STATE->isTheoryEnabled(Smt2::THEORY_DATATYPES) }? 'tupSel';
-// Other set theory operators are not
-// tokenized and handled directly when
-// processing a term
-
-REAL_PI_TOK : 'real.pi';
-
-FP_PINF_TOK : '+oo';
-FP_NINF_TOK : '-oo';
-FP_PZERO_TOK : '+zero';
-FP_NZERO_TOK : '-zero';
-FP_NAN_TOK : { PARSER_STATE->isTheoryEnabled(Smt2::THEORY_FP) }? 'NaN';
-
-FP_TO_FP_TOK : { PARSER_STATE->isTheoryEnabled(Smt2::THEORY_FP) }? 'to_fp';
-FP_TO_FPBV_TOK : { PARSER_STATE->isTheoryEnabled(Smt2::THEORY_FP) }? 'to_fp_bv';
-FP_TO_FPFP_TOK : { PARSER_STATE->isTheoryEnabled(Smt2::THEORY_FP) }? 'to_fp_fp';
-FP_TO_FPR_TOK : { PARSER_STATE->isTheoryEnabled(Smt2::THEORY_FP) }? 'to_fp_real';
-FP_TO_FPS_TOK : { PARSER_STATE->isTheoryEnabled(Smt2::THEORY_FP) }? 'to_fp_signed';
-FP_TO_FPU_TOK : { PARSER_STATE->isTheoryEnabled(Smt2::THEORY_FP) }? 'to_fp_unsigned';
-FP_TO_UBV_TOK : { PARSER_STATE->isTheoryEnabled(Smt2::THEORY_FP) }? 'fp.to_ubv';
-FP_TO_SBV_TOK : { PARSER_STATE->isTheoryEnabled(Smt2::THEORY_FP) }? 'fp.to_sbv';
-FP_RNE_TOK : { PARSER_STATE->isTheoryEnabled(Smt2::THEORY_FP) }? 'RNE';
-FP_RNA_TOK : { PARSER_STATE->isTheoryEnabled(Smt2::THEORY_FP) }? 'RNA';
-FP_RTP_TOK : { PARSER_STATE->isTheoryEnabled(Smt2::THEORY_FP) }? 'RTP';
-FP_RTN_TOK : { PARSER_STATE->isTheoryEnabled(Smt2::THEORY_FP) }? 'RTN';
-FP_RTZ_TOK : { PARSER_STATE->isTheoryEnabled(Smt2::THEORY_FP) }? 'RTZ';
-FP_RNE_FULL_TOK : { PARSER_STATE->isTheoryEnabled(Smt2::THEORY_FP) }? 'roundNearestTiesToEven';
-FP_RNA_FULL_TOK : { PARSER_STATE->isTheoryEnabled(Smt2::THEORY_FP) }? 'roundNearestTiesToAway';
-FP_RTP_FULL_TOK : { PARSER_STATE->isTheoryEnabled(Smt2::THEORY_FP) }? 'roundTowardPositive';
-FP_RTN_FULL_TOK : { PARSER_STATE->isTheoryEnabled(Smt2::THEORY_FP) }? 'roundTowardNegative';
-FP_RTZ_FULL_TOK : { PARSER_STATE->isTheoryEnabled(Smt2::THEORY_FP) }? 'roundTowardZero';
 
 HO_ARROW_TOK : { PARSER_STATE->getLogic().isHigherOrder() }? '->';
 HO_LAMBDA_TOK : { PARSER_STATE->getLogic().isHigherOrder() }? 'lambda';
@@ -3223,8 +2960,8 @@ KEYWORD
  * digit, and is not the special reserved symbols '!' or '_'.
  */
 SIMPLE_SYMBOL
-  : (ALPHA | SYMBOL_CHAR) (ALPHA | DIGIT | SYMBOL_CHAR)+
-  | ALPHA
+  : ALPHA (ALPHA | DIGIT | SYMBOL_CHAR)*
+  | SYMBOL_CHAR (ALPHA | DIGIT | SYMBOL_CHAR)+
   | SYMBOL_CHAR_NOUNDERSCORE_NOATTRIBUTE
   ;
 
diff --git a/src/parser/smt2/smt2.cpp b/src/parser/smt2/smt2.cpp
index 2e1abf710..12b43f346 100644
--- a/src/parser/smt2/smt2.cpp
+++ b/src/parser/smt2/smt2.cpp
@@ -15,7 +15,6 @@
  **/
 #include "parser/smt2/smt2.h"
 
-#include "api/cvc4cpp.h"
 #include "expr/type.h"
 #include "options/options.h"
 #include "parser/antlr_input.h"
@@ -45,17 +44,21 @@ Smt2::Smt2(api::Solver* solver, Input* input, bool strictMode, bool parseOnly)
 }
 
 void Smt2::addArithmeticOperators() {
-  Parser::addOperator(kind::PLUS);
-  Parser::addOperator(kind::MINUS);
+  addOperator(kind::PLUS, "+");
+  addOperator(kind::MINUS, "-");
+  // kind::MINUS is converted to kind::UMINUS if there is only a single operand
   Parser::addOperator(kind::UMINUS);
-  Parser::addOperator(kind::MULT);
-  Parser::addOperator(kind::LT);
-  Parser::addOperator(kind::LEQ);
-  Parser::addOperator(kind::GT);
-  Parser::addOperator(kind::GEQ);
-
-  // NOTE: this operator is non-standard
-  addOperator(kind::POW, "^");
+  addOperator(kind::MULT, "*");
+  addOperator(kind::LT, "<");
+  addOperator(kind::LEQ, "<=");
+  addOperator(kind::GT, ">");
+  addOperator(kind::GEQ, ">=");
+
+  if (!strictModeEnabled())
+  {
+    // NOTE: this operator is non-standard
+    addOperator(kind::POW, "^");
+  }
 }
 
 void Smt2::addTranscendentalOperators()
@@ -76,6 +79,14 @@ void Smt2::addTranscendentalOperators()
   addOperator(kind::SQRT, "sqrt");
 }
 
+void Smt2::addQuantifiersOperators()
+{
+  if (!strictModeEnabled())
+  {
+    addOperator(kind::INST_CLOSURE, "inst-closure");
+  }
+}
+
 void Smt2::addBitvectorOperators() {
   addOperator(kind::BITVECTOR_CONCAT, "concat");
   addOperator(kind::BITVECTOR_NOT, "bvnot");
@@ -108,17 +119,39 @@ void Smt2::addBitvectorOperators() {
   addOperator(kind::BITVECTOR_SGE, "bvsge");
   addOperator(kind::BITVECTOR_REDOR, "bvredor");
   addOperator(kind::BITVECTOR_REDAND, "bvredand");
+  addOperator(kind::BITVECTOR_TO_NAT, "bv2nat");
+
+  addIndexedOperator(
+      kind::BITVECTOR_EXTRACT, api::BITVECTOR_EXTRACT_OP, "extract");
+  addIndexedOperator(
+      kind::BITVECTOR_REPEAT, api::BITVECTOR_REPEAT_OP, "repeat");
+  addIndexedOperator(kind::BITVECTOR_ZERO_EXTEND,
+                     api::BITVECTOR_ZERO_EXTEND_OP,
+                     "zero_extend");
+  addIndexedOperator(kind::BITVECTOR_SIGN_EXTEND,
+                     api::BITVECTOR_SIGN_EXTEND_OP,
+                     "sign_extend");
+  addIndexedOperator(kind::BITVECTOR_ROTATE_LEFT,
+                     api::BITVECTOR_ROTATE_LEFT_OP,
+                     "rotate_left");
+  addIndexedOperator(kind::BITVECTOR_ROTATE_RIGHT,
+                     api::BITVECTOR_ROTATE_RIGHT_OP,
+                     "rotate_right");
+  addIndexedOperator(
+      kind::INT_TO_BITVECTOR, api::INT_TO_BITVECTOR_OP, "int2bv");
+}
 
-  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);
+void Smt2::addDatatypesOperators()
+{
+  Parser::addOperator(kind::APPLY_CONSTRUCTOR);
+  Parser::addOperator(kind::APPLY_TESTER);
+  Parser::addOperator(kind::APPLY_SELECTOR);
+  Parser::addOperator(kind::APPLY_SELECTOR_TOTAL);
 
-  Parser::addOperator(kind::INT_TO_BITVECTOR);
-  Parser::addOperator(kind::BITVECTOR_TO_NAT);
+  if (!strictModeEnabled())
+  {
+    addOperator(kind::DT_SIZE, "dt.size");
+  }
 }
 
 void Smt2::addStringOperators() {
@@ -194,14 +227,32 @@ void Smt2::addFloatingPointOperators() {
   addOperator(kind::FLOATINGPOINT_ISPOS, "fp.isPositive");
   addOperator(kind::FLOATINGPOINT_TO_REAL, "fp.to_real");
 
-  Parser::addOperator(kind::FLOATINGPOINT_TO_FP_GENERIC);
-  Parser::addOperator(kind::FLOATINGPOINT_TO_FP_IEEE_BITVECTOR);
-  Parser::addOperator(kind::FLOATINGPOINT_TO_FP_FLOATINGPOINT);
-  Parser::addOperator(kind::FLOATINGPOINT_TO_FP_REAL);
-  Parser::addOperator(kind::FLOATINGPOINT_TO_FP_SIGNED_BITVECTOR);
-  Parser::addOperator(kind::FLOATINGPOINT_TO_FP_UNSIGNED_BITVECTOR);
-  Parser::addOperator(kind::FLOATINGPOINT_TO_UBV);
-  Parser::addOperator(kind::FLOATINGPOINT_TO_SBV);
+  addIndexedOperator(kind::FLOATINGPOINT_TO_FP_GENERIC,
+                     api::FLOATINGPOINT_TO_FP_GENERIC_OP,
+                     "to_fp");
+  addIndexedOperator(kind::FLOATINGPOINT_TO_FP_UNSIGNED_BITVECTOR,
+                     api::FLOATINGPOINT_TO_FP_UNSIGNED_BITVECTOR_OP,
+                     "to_fp_unsigned");
+  addIndexedOperator(
+      kind::FLOATINGPOINT_TO_UBV, api::FLOATINGPOINT_TO_UBV_OP, "fp.to_ubv");
+  addIndexedOperator(
+      kind::FLOATINGPOINT_TO_SBV, api::FLOATINGPOINT_TO_SBV_OP, "fp.to_sbv");
+
+  if (!strictModeEnabled())
+  {
+    addIndexedOperator(kind::FLOATINGPOINT_TO_FP_IEEE_BITVECTOR,
+                       api::FLOATINGPOINT_TO_FP_IEEE_BITVECTOR_OP,
+                       "to_fp_bv");
+    addIndexedOperator(kind::FLOATINGPOINT_TO_FP_FLOATINGPOINT,
+                       api::FLOATINGPOINT_TO_FP_FLOATINGPOINT_OP,
+                       "to_fp_fp");
+    addIndexedOperator(kind::FLOATINGPOINT_TO_FP_REAL,
+                       api::FLOATINGPOINT_TO_FP_REAL_OP,
+                       "to_fp_real");
+    addIndexedOperator(kind::FLOATINGPOINT_TO_FP_SIGNED_BITVECTOR,
+                       api::FLOATINGPOINT_TO_FP_SIGNED_BITVECTOR_OP,
+                       "to_fp_signed");
+  }
 }
 
 void Smt2::addSepOperators() {
@@ -230,19 +281,19 @@ void Smt2::addTheory(Theory theory) {
     defineType("Bool", getExprManager()->booleanType());
     defineVar("true", getExprManager()->mkConst(true));
     defineVar("false", getExprManager()->mkConst(false));
-    Parser::addOperator(kind::AND);
-    Parser::addOperator(kind::DISTINCT);
-    Parser::addOperator(kind::EQUAL);
-    Parser::addOperator(kind::IMPLIES);
-    Parser::addOperator(kind::ITE);
-    Parser::addOperator(kind::NOT);
-    Parser::addOperator(kind::OR);
-    Parser::addOperator(kind::XOR);
+    addOperator(kind::AND, "and");
+    addOperator(kind::DISTINCT, "distinct");
+    addOperator(kind::EQUAL, "=");
+    addOperator(kind::IMPLIES, "=>");
+    addOperator(kind::ITE, "ite");
+    addOperator(kind::NOT, "not");
+    addOperator(kind::OR, "or");
+    addOperator(kind::XOR, "xor");
     break;
 
   case THEORY_REALS_INTS:
     defineType("Real", getExprManager()->realType());
-    Parser::addOperator(kind::DIVISION);
+    addOperator(kind::DIVISION, "/");
     addOperator(kind::TO_INTEGER, "to_int");
     addOperator(kind::IS_INTEGER, "is_int");
     addOperator(kind::TO_REAL, "to_real");
@@ -253,21 +304,36 @@ void Smt2::addTheory(Theory theory) {
     addOperator(kind::INTS_DIVISION, "div");
     addOperator(kind::INTS_MODULUS, "mod");
     addOperator(kind::ABS, "abs");
-    Parser::addOperator(kind::DIVISIBLE);
+    addIndexedOperator(kind::DIVISIBLE, api::DIVISIBLE_OP, "divisible");
     break;
 
   case THEORY_REALS:
     defineType("Real", getExprManager()->realType());
     addArithmeticOperators();
-    Parser::addOperator(kind::DIVISION);
+    addOperator(kind::DIVISION, "/");
+    if (!strictModeEnabled())
+    {
+      addOperator(kind::ABS, "abs");
+    }
     break;
 
-  case THEORY_TRANSCENDENTALS: addTranscendentalOperators(); break;
-
-  case THEORY_QUANTIFIERS:
+  case THEORY_TRANSCENDENTALS:
+    defineVar("real.pi",
+              getExprManager()->mkNullaryOperator(getExprManager()->realType(),
+                                                  CVC4::kind::PI));
+    addTranscendentalOperators();
     break;
 
+  case THEORY_QUANTIFIERS: addQuantifiersOperators(); break;
+
   case THEORY_SETS:
+    defineVar("emptyset",
+              d_solver->mkEmptySet(d_solver->getNullSort()).getExpr());
+    // the Boolean sort is a placeholder here since we don't have type info
+    // without type annotation
+    defineVar("univset",
+              d_solver->mkUniverseSet(d_solver->getBooleanSort()).getExpr());
+
     addOperator(kind::UNION, "union");
     addOperator(kind::INTERSECTION, "intersection");
     addOperator(kind::SETMINUS, "setminus");
@@ -287,10 +353,7 @@ void Smt2::addTheory(Theory theory) {
   {
     const std::vector<Type> types;
     defineType("Tuple", getExprManager()->mkTupleType(types));
-    Parser::addOperator(kind::APPLY_CONSTRUCTOR);
-    Parser::addOperator(kind::APPLY_TESTER);
-    Parser::addOperator(kind::APPLY_SELECTOR);
-    Parser::addOperator(kind::APPLY_SELECTOR_TOTAL);
+    addDatatypesOperators();
     break;
   }
 
@@ -298,11 +361,21 @@ void Smt2::addTheory(Theory theory) {
     defineType("String", getExprManager()->stringType());
     defineType("RegLan", getExprManager()->regExpType());
     defineType("Int", getExprManager()->integerType());
+
+    defineVar("re.nostr", d_solver->mkRegexpEmpty().getExpr());
+    defineVar("re.allchar", d_solver->mkRegexpSigma().getExpr());
+
     addStringOperators();
     break;
 
   case THEORY_UF:
     Parser::addOperator(kind::APPLY_UF);
+
+    if (!strictModeEnabled() && d_logic.hasCardinalityConstraints())
+    {
+      addOperator(kind::CARDINALITY_CONSTRAINT, "fmf.card");
+      addOperator(kind::CARDINALITY_VALUE, "fmf.card.val");
+    }
     break;
 
   case THEORY_FP:
@@ -311,10 +384,41 @@ void Smt2::addTheory(Theory theory) {
     defineType("Float32", getExprManager()->mkFloatingPointType(8, 24));
     defineType("Float64", getExprManager()->mkFloatingPointType(11, 53));
     defineType("Float128", getExprManager()->mkFloatingPointType(15, 113));
+
+    defineVar(
+        "RNE",
+        d_solver->mkRoundingMode(api::ROUND_NEAREST_TIES_TO_EVEN).getExpr());
+    defineVar(
+        "roundNearestTiesToEven",
+        d_solver->mkRoundingMode(api::ROUND_NEAREST_TIES_TO_EVEN).getExpr());
+    defineVar(
+        "RNA",
+        d_solver->mkRoundingMode(api::ROUND_NEAREST_TIES_TO_AWAY).getExpr());
+    defineVar(
+        "roundNearestTiesToAway",
+        d_solver->mkRoundingMode(api::ROUND_NEAREST_TIES_TO_AWAY).getExpr());
+    defineVar("RTP",
+              d_solver->mkRoundingMode(api::ROUND_TOWARD_POSITIVE).getExpr());
+    defineVar("roundTowardPositive",
+              d_solver->mkRoundingMode(api::ROUND_TOWARD_POSITIVE).getExpr());
+    defineVar("RTN",
+              d_solver->mkRoundingMode(api::ROUND_TOWARD_NEGATIVE).getExpr());
+    defineVar("roundTowardNegative",
+              d_solver->mkRoundingMode(api::ROUND_TOWARD_NEGATIVE).getExpr());
+    defineVar("RTZ",
+              d_solver->mkRoundingMode(api::ROUND_TOWARD_ZERO).getExpr());
+    defineVar("roundTowardZero",
+              d_solver->mkRoundingMode(api::ROUND_TOWARD_ZERO).getExpr());
+
     addFloatingPointOperators();
     break;
     
   case THEORY_SEP:
+    // the Boolean sort is a placeholder here since we don't have type info
+    // without type annotation
+    defineVar("sep.nil",
+              d_solver->mkSepNil(d_solver->getBooleanSort()).getExpr());
+
     addSepOperators();
     break;
     
@@ -332,6 +436,14 @@ void Smt2::addOperator(Kind kind, const std::string& name) {
   operatorKindMap[name] = kind;
 }
 
+void Smt2::addIndexedOperator(Kind tKind,
+                              api::Kind opKind,
+                              const std::string& name)
+{
+  Parser::addOperator(tKind);
+  d_indexedOpKindMap[name] = opKind;
+}
+
 Kind Smt2::getOperatorKind(const std::string& name) const {
   // precondition: isOperatorEnabled(name)
   return operatorKindMap.find(name)->second;
@@ -395,6 +507,66 @@ Expr Smt2::getExpressionForNameAndType(const std::string& name, Type t) {
   }
 }
 
+api::Term Smt2::mkIndexedConstant(const std::string& name,
+                                  const std::vector<uint64_t>& numerals)
+{
+  if (isTheoryEnabled(THEORY_FP))
+  {
+    if (name == "+oo")
+    {
+      return d_solver->mkPosInf(numerals[0], numerals[1]);
+    }
+    else if (name == "-oo")
+    {
+      return d_solver->mkNegInf(numerals[0], numerals[1]);
+    }
+    else if (name == "NaN")
+    {
+      return d_solver->mkNaN(numerals[0], numerals[1]);
+    }
+    else if (name == "+zero")
+    {
+      return d_solver->mkPosZero(numerals[0], numerals[1]);
+    }
+    else if (name == "-zero")
+    {
+      return d_solver->mkNegZero(numerals[0], numerals[1]);
+    }
+  }
+
+  if (isTheoryEnabled(THEORY_BITVECTORS) && name.find("bv") == 0)
+  {
+    std::string bvStr = name.substr(2);
+    return d_solver->mkBitVector(numerals[0], bvStr, 10);
+  }
+
+  // NOTE: Theory parametric constants go here
+
+  parseError(std::string("Unknown indexed literal `") + name + "'");
+  return api::Term();
+}
+
+api::OpTerm Smt2::mkIndexedOp(const std::string& name,
+                              const std::vector<uint64_t>& numerals)
+{
+  const auto& kIt = d_indexedOpKindMap.find(name);
+  if (kIt != d_indexedOpKindMap.end())
+  {
+    api::Kind k = (*kIt).second;
+    if (numerals.size() == 1)
+    {
+      return d_solver->mkOpTerm(k, numerals[0]);
+    }
+    else if (numerals.size() == 2)
+    {
+      return d_solver->mkOpTerm(k, numerals[0], numerals[1]);
+    }
+  }
+
+  parseError(std::string("Unknown indexed function `") + name + "'");
+  return api::OpTerm();
+}
+
 Expr Smt2::mkDefineFunRec(
     const std::string& fname,
     const std::vector<std::pair<std::string, Type> >& sortedVarNames,
@@ -1233,5 +1405,5 @@ InputLanguage Smt2::getLanguage() const
   return em->getOptions().getInputLanguage();
 }
 
-}/* CVC4::parser namespace */
+}  // namespace parser
 }/* CVC4 namespace */
diff --git a/src/parser/smt2/smt2.h b/src/parser/smt2/smt2.h
index ee694db06..d4d310b89 100644
--- a/src/parser/smt2/smt2.h
+++ b/src/parser/smt2/smt2.h
@@ -25,6 +25,7 @@
 #include <unordered_map>
 #include <utility>
 
+#include "api/cvc4cpp.h"
 #include "parser/parser.h"
 #include "parser/smt1/smt1.h"
 #include "theory/logic_info.h"
@@ -40,32 +41,38 @@ class Solver;
 
 namespace parser {
 
-class Smt2 : public Parser {
+class Smt2 : public Parser
+{
   friend class ParserBuilder;
 
-public:
- 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:
+ public:
+  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;
   LogicInfo d_logic;
   std::unordered_map<std::string, Kind> operatorKindMap;
+  /**
+   * Maps indexed symbols to the kind of the operator (e.g. "extract" to
+   * BITVECTOR_EXTRACT_OP).
+   */
+  std::unordered_map<std::string, api::Kind> d_indexedOpKindMap;
   std::pair<Expr, std::string> d_lastNamedTerm;
   // for sygus
   std::vector<Expr> d_sygusVars, d_sygusVarPrimed, d_sygusConstraints,
@@ -87,6 +94,20 @@ private:
 
   void addOperator(Kind k, const std::string& name);
 
+  /**
+   * Registers an indexed function symbol.
+   *
+   * @param tKind The kind of the term that uses the operator kind (e.g.
+   *              BITVECTOR_EXTRACT). NOTE: this is an internal kind for now
+   *              because that is what we use to create expressions. Eventually
+   *              it will be an api::Kind.
+   * @param opKind The kind of the operator term (e.g. BITVECTOR_EXTRACT_OP)
+   * @param name The name of the symbol (e.g. "extract")
+   */
+  void addIndexedOperator(Kind tKind,
+                          api::Kind opKind,
+                          const std::string& name);
+
   Kind getOperatorKind(const std::string& name) const;
 
   bool isOperatorEnabled(const std::string& name) const;
@@ -96,24 +117,47 @@ private:
   bool logicIsSet() override;
 
   /**
-   * Returns the expression that name should be interpreted as. 
+   * Creates an indexed constant, e.g. (_ +oo 8 24) (positive infinity
+   * as a 32-bit floating-point constant).
+   *
+   * @param name The name of the constant (e.g. "+oo")
+   * @param numerals The parameters for the constant (e.g. [8, 24])
+   * @return The term corresponding to the constant or a parse error if name is
+   *         not valid.
+   */
+  api::Term mkIndexedConstant(const std::string& name,
+                              const std::vector<uint64_t>& numerals);
+
+  /**
+   * Creates an indexed operator term, e.g. (_ extract 5 0).
+   *
+   * @param name The name of the operator (e.g. "extract")
+   * @param numerals The parameters for the operator (e.g. [5, 0])
+   * @return The operator term corresponding to the indexed operator or a parse
+   *         error if the name is not valid.
+   */
+  api::OpTerm mkIndexedOp(const std::string& name,
+                          const std::vector<uint64_t>& numerals);
+
+  /**
+   * Returns the expression that name should be interpreted as.
    */
   Expr getExpressionForNameAndType(const std::string& name, Type t) override;
 
   /** Make function defined by a define-fun(s)-rec command.
-  *
-  * fname : the name of the function.
-  * sortedVarNames : the list of variable arguments for the function.
-  * t : the range type of the function we are defining.
-  *
-  * This function will create a bind a new function term to name fname.
-  * The type of this function is
-  * Parser::mkFlatFunctionType(sorts,t,flattenVars),
-  * where sorts are the types in the second components of sortedVarNames.
-  * As descibed in Parser::mkFlatFunctionType, new bound variables may be
-  * added to flattenVars in this function if the function is given a function
-  * range type.
-  */
+   *
+   * fname : the name of the function.
+   * sortedVarNames : the list of variable arguments for the function.
+   * t : the range type of the function we are defining.
+   *
+   * This function will create a bind a new function term to name fname.
+   * The type of this function is
+   * Parser::mkFlatFunctionType(sorts,t,flattenVars),
+   * where sorts are the types in the second components of sortedVarNames.
+   * As descibed in Parser::mkFlatFunctionType, new bound variables may be
+   * added to flattenVars in this function if the function is given a function
+   * range type.
+   */
   Expr mkDefineFunRec(
       const std::string& fname,
       const std::vector<std::pair<std::string, Type> >& sortedVarNames,
@@ -122,21 +166,21 @@ private:
 
   /** Push scope for define-fun-rec
    *
-  * This calls Parser::pushScope(bindingLevel) and sets up
-  * initial information for reading a body of a function definition
-  * in the define-fun-rec and define-funs-rec command.
-  * The input parameters func/flattenVars are the result
-  * of a call to mkDefineRec above.
-  *
-  * func : the function whose body we are defining.
-  * sortedVarNames : the list of variable arguments for the function.
-  * flattenVars : the implicit variables introduced when defining func.
-  *
-  * This function:
-  * (1) Calls Parser::pushScope(bindingLevel).
-  * (2) Computes the bound variable list for the quantified formula
-  *     that defined this definition and stores it in bvs.
-  */
+   * This calls Parser::pushScope(bindingLevel) and sets up
+   * initial information for reading a body of a function definition
+   * in the define-fun-rec and define-funs-rec command.
+   * The input parameters func/flattenVars are the result
+   * of a call to mkDefineRec above.
+   *
+   * func : the function whose body we are defining.
+   * sortedVarNames : the list of variable arguments for the function.
+   * flattenVars : the implicit variables introduced when defining func.
+   *
+   * This function:
+   * (1) Calls Parser::pushScope(bindingLevel).
+   * (2) Computes the bound variable list for the quantified formula
+   *     that defined this definition and stores it in bvs.
+   */
   void pushDefineFunRecScope(
       const std::vector<std::pair<std::string, Type> >& sortedVarNames,
       Expr func,
@@ -161,7 +205,8 @@ private:
    */
   const LogicInfo& getLogic() const { return d_logic; }
 
-  bool v2_0() const {
+  bool v2_0() const
+  {
     return getLanguage() == language::input::LANG_SMTLIB_V2_0;
   }
   /**
@@ -400,8 +445,12 @@ private:
 
   void addTranscendentalOperators();
 
+  void addQuantifiersOperators();
+
   void addBitvectorOperators();
 
+  void addDatatypesOperators();
+
   void addStringOperators();
 
   void addFloatingPointOperators();
@@ -409,7 +458,7 @@ private:
   void addSepOperators();
 
   InputLanguage getLanguage() const;
-};/* class Smt2 */
+}; /* class Smt2 */
 
 }/* CVC4::parser namespace */
 }/* CVC4 namespace */
diff --git a/test/regress/regress0/bv/core/constant_core.smt2 b/test/regress/regress0/bv/core/constant_core.smt2
index c7a5a605f..1e2bcde68 100644
--- a/test/regress/regress0/bv/core/constant_core.smt2
+++ b/test/regress/regress0/bv/core/constant_core.smt2
@@ -12,4 +12,4 @@
 (not (= (_ bv0 3) x))
 ))
 (check-sat)
-(exit)
\ No newline at end of file
+(exit)
diff --git a/test/regress/regress0/expect/scrub.08.sy b/test/regress/regress0/expect/scrub.08.sy
index 24a0aab2e..aec265f2b 100644
--- a/test/regress/regress0/expect/scrub.08.sy
+++ b/test/regress/regress0/expect/scrub.08.sy
@@ -8,5 +8,5 @@
 (declare-var n Int)
 
 (synth-fun f ((n Int)) Int)
-(constraint (= (/ n n) 1))
+(constraint (= (div n n) 1))
 (check-synth)
diff --git a/test/regress/regress0/nl/nta/real-pi.smt2 b/test/regress/regress0/nl/nta/real-pi.smt2
index a303f48b1..4163e09f9 100644
--- a/test/regress/regress0/nl/nta/real-pi.smt2
+++ b/test/regress/regress0/nl/nta/real-pi.smt2
@@ -1,6 +1,6 @@
 ; COMMAND-LINE: --nl-ext --no-check-models
 ; EXPECT: sat
-(set-logic QF_NRA)
+(set-logic QF_NRAT)
 (set-info :status sat)
 (assert (<= 3.0 real.pi))
 (assert (<= real.pi 4.0))
diff --git a/test/regress/regress0/strings/bug613.smt2 b/test/regress/regress0/strings/bug613.smt2
index 506076cd6..09c5e9a2a 100644
--- a/test/regress/regress0/strings/bug613.smt2
+++ b/test/regress/regress0/strings/bug613.smt2
@@ -1,4 +1,4 @@
-(set-logic QF_S)
+(set-logic QF_SLIA)
 (set-info :status sat)
 (set-option :strings-exp true)
 
diff --git a/test/regress/regress0/strings/str004.smt2 b/test/regress/regress0/strings/str004.smt2
index 8a03f4481..21570a2da 100644
--- a/test/regress/regress0/strings/str004.smt2
+++ b/test/regress/regress0/strings/str004.smt2
@@ -1,4 +1,4 @@
-(set-logic QF_S)
+(set-logic QF_SLIA)
 (set-info :status unsat)
 
 (declare-fun xx () String)
diff --git a/test/regress/regress0/strings/type001.smt2 b/test/regress/regress0/strings/type001.smt2
index 89191ac34..36a6aaec1 100644
--- a/test/regress/regress0/strings/type001.smt2
+++ b/test/regress/regress0/strings/type001.smt2
@@ -1,5 +1,5 @@
 (set-info :smt-lib-version 2.5)
-(set-logic QF_S)
+(set-logic QF_SLIA)
 (set-info :status sat)
 (set-option :strings-exp true)
 
diff --git a/test/regress/regress0/strings/unsound-0908.smt2 b/test/regress/regress0/strings/unsound-0908.smt2
index 2b25e6dc8..9c91d135f 100644
--- a/test/regress/regress0/strings/unsound-0908.smt2
+++ b/test/regress/regress0/strings/unsound-0908.smt2
@@ -1,4 +1,4 @@
-(set-logic QF_S)
+(set-logic QF_SLIA)
 (set-info :status sat)
 (declare-const x String)
 (assert (= (str.len x) 1))
diff --git a/test/regress/regress1/strings/artemis-0512-nonterm.smt2 b/test/regress/regress1/strings/artemis-0512-nonterm.smt2
index a3cca23a2..328317ea4 100644
--- a/test/regress/regress1/strings/artemis-0512-nonterm.smt2
+++ b/test/regress/regress1/strings/artemis-0512-nonterm.smt2
@@ -1,5 +1,5 @@
 (set-info :smt-lib-version 2.5)
-(set-logic QF_S)
+(set-logic QF_SLIA)
 (set-option :strings-exp true)
 (set-info :status unsat)
 
diff --git a/test/regress/regress1/strings/at001.smt2 b/test/regress/regress1/strings/at001.smt2
index 2ecbcc993..04933b8f7 100644
--- a/test/regress/regress1/strings/at001.smt2
+++ b/test/regress/regress1/strings/at001.smt2
@@ -1,4 +1,4 @@
-(set-logic QF_S)
+(set-logic QF_SLIA)
 (set-info :status sat)
 
 (declare-fun x () String)
diff --git a/test/regress/regress1/strings/fmf002.smt2 b/test/regress/regress1/strings/fmf002.smt2
index ab3dc2ae2..2f2209ae7 100644
--- a/test/regress/regress1/strings/fmf002.smt2
+++ b/test/regress/regress1/strings/fmf002.smt2
@@ -1,5 +1,5 @@
 (set-info :smt-lib-version 2.5)
-(set-logic QF_S)
+(set-logic QF_SLIA)
 (set-option :strings-exp true)
 (set-option :strings-fmf true)
 (set-info :status sat)
diff --git a/test/regress/regress1/strings/issue2429-code.smt2 b/test/regress/regress1/strings/issue2429-code.smt2
index 2d906c1fd..9dc29794e 100644
--- a/test/regress/regress1/strings/issue2429-code.smt2
+++ b/test/regress/regress1/strings/issue2429-code.smt2
@@ -1,4 +1,4 @@
-(set-logic QF_S)
+(set-logic QF_SLIA)
 (set-option :strings-exp true)
 (set-option :produce-models true)
 (set-info :status sat)
diff --git a/test/regress/regress1/strings/kaluza-fl.smt2 b/test/regress/regress1/strings/kaluza-fl.smt2
index 20c2e6aa4..d277d85e6 100644
--- a/test/regress/regress1/strings/kaluza-fl.smt2
+++ b/test/regress/regress1/strings/kaluza-fl.smt2
@@ -1,5 +1,5 @@
 (set-info :smt-lib-version 2.5)
-(set-logic QF_S)
+(set-logic QF_SLIA)
 (set-info :status sat)
 
 (declare-fun I0_15 () Int)
diff --git a/test/regress/regress1/strings/loop005.smt2 b/test/regress/regress1/strings/loop005.smt2
index 039409ea6..cc115ebf4 100644
--- a/test/regress/regress1/strings/loop005.smt2
+++ b/test/regress/regress1/strings/loop005.smt2
@@ -1,4 +1,4 @@
-(set-logic QF_S)
+(set-logic QF_SLIA)
 (set-info :status sat)
 
 (declare-fun x () String)
diff --git a/test/regress/regress1/strings/loop007.smt2 b/test/regress/regress1/strings/loop007.smt2
index a97d97d54..492162ae6 100644
--- a/test/regress/regress1/strings/loop007.smt2
+++ b/test/regress/regress1/strings/loop007.smt2
@@ -1,4 +1,4 @@
-(set-logic QF_S)
+(set-logic QF_SLIA)
 (set-option :strings-exp true)
 (set-info :status sat)
 
diff --git a/test/regress/regress1/strings/loop008.smt2 b/test/regress/regress1/strings/loop008.smt2
index f84ba442b..672ecd371 100644
--- a/test/regress/regress1/strings/loop008.smt2
+++ b/test/regress/regress1/strings/loop008.smt2
@@ -1,4 +1,4 @@
-(set-logic QF_S)
+(set-logic QF_SLIA)
 (set-option :strings-exp true)
 (set-info :status sat)
 
diff --git a/test/regress/regress1/strings/re-agg-total1.smt2 b/test/regress/regress1/strings/re-agg-total1.smt2
index 4e5b21c0f..2950066a0 100644
--- a/test/regress/regress1/strings/re-agg-total1.smt2
+++ b/test/regress/regress1/strings/re-agg-total1.smt2
@@ -1,5 +1,5 @@
 (set-info :smt-lib-version 2.6)
-(set-logic QF_S)
+(set-logic QF_SLIA)
 (set-info :status unsat)
 (set-option :strings-exp true)
 (set-option :re-elim-agg true)
diff --git a/test/regress/regress1/strings/reloop.smt2 b/test/regress/regress1/strings/reloop.smt2
index 967e564ce..22537b957 100644
--- a/test/regress/regress1/strings/reloop.smt2
+++ b/test/regress/regress1/strings/reloop.smt2
@@ -1,5 +1,5 @@
 (set-info :smt-lib-version 2.5)
-(set-logic QF_S)
+(set-logic QF_SLIA)
 (set-option :strings-exp true)
 (set-info :status sat)
 
diff --git a/test/regress/regress1/strings/substr001.smt2 b/test/regress/regress1/strings/substr001.smt2
index 78f3ffee7..47fa995ff 100644
--- a/test/regress/regress1/strings/substr001.smt2
+++ b/test/regress/regress1/strings/substr001.smt2
@@ -1,4 +1,4 @@
-(set-logic QF_S)
+(set-logic QF_SLIA)
 (set-info :status sat)
 
 (declare-fun x () String)
diff --git a/test/regress/regress1/strings/type002.smt2 b/test/regress/regress1/strings/type002.smt2
index 458ac75fe..3b46b25a8 100644
--- a/test/regress/regress1/strings/type002.smt2
+++ b/test/regress/regress1/strings/type002.smt2
@@ -1,5 +1,5 @@
 (set-info :smt-lib-version 2.5)
-(set-logic QF_S)
+(set-logic QF_SLIA)
 (set-info :status sat)
 (set-option :strings-exp true)
 
diff --git a/test/regress/regress1/strings/type003.smt2 b/test/regress/regress1/strings/type003.smt2
index 4185041f7..332ec3ec3 100644
--- a/test/regress/regress1/strings/type003.smt2
+++ b/test/regress/regress1/strings/type003.smt2
@@ -1,5 +1,5 @@
 (set-info :smt-lib-version 2.5)
-(set-logic QF_S)
+(set-logic QF_SLIA)
 (set-info :status sat)
 (set-option :strings-exp true)
 
diff --git a/test/unit/parser/parser_black.h b/test/unit/parser/parser_black.h
index 33ad3740a..f2f5f24b6 100644
--- a/test/unit/parser/parser_black.h
+++ b/test/unit/parser/parser_black.h
@@ -138,6 +138,12 @@ class ParserBlack
                            .withInputLanguage(d_lang)
                            .build();
 
+      if (d_lang == LANG_SMTLIB_V2)
+      {
+        // Use QF_LIA to make multiplication ("*") available
+        static_cast<Smt2*>(parser)->setLogic("QF_LIA");
+      }
+
       TS_ASSERT(!parser->done());
       setupContext(*parser);
       TS_ASSERT(!parser->done());