Merge from quantifiers2-trunkmerge branch.

Adds TheoryQuantifiers and TheoryRewriteRules, QuantifiersEngine, and other infrastructure.

Adds theory instantiators to many theories.

Adds the UF strong solver.

7 files changed, 292 insertions, 64 deletions

diff --git a/src/parser/cvc/Cvc.g b/src/parser/cvc/Cvc.g
index 1f0e6b890..2988ae4ef 100644
--- a/src/parser/cvc/Cvc.g
+++ b/src/parser/cvc/Cvc.g
@@ -1066,13 +1066,13 @@ restrictedTypePossiblyFunctionLHS[CVC4::Type& t,
          PARSER_STATE->isDeclared(id, SYM_SORT)) {
         Debug("parser-param") << "param: getSort " << id << " " << types.size() << " " << PARSER_STATE->getArity( id )
                               << " " << PARSER_STATE->isDeclared(id, SYM_SORT) << std::endl;
-        if( types.size()>0 ){
+        if(types.size() > 0) {
           t = PARSER_STATE->getSort(id, types);
         }else{
           t = PARSER_STATE->getSort(id);
         }
       } else {
-        if( types.empty() ){
+        if(types.empty()) {
           t = PARSER_STATE->mkUnresolvedType(id);
           Debug("parser-param") << "param: make unres type " << id << std::endl;
         }else{
@@ -1236,22 +1236,36 @@ prefixFormula[CVC4::Expr& f]
   std::vector<std::string> ids;
   std::vector<Expr> terms;
   std::vector<Type> types;
+  std::vector<Expr> bvs;
   Type t;
+  Kind k;
+  Expr ipl;
 }
     /* quantifiers */
-  : FORALL_TOK { PARSER_STATE->pushScope(); } LPAREN
-    boundVarDecl[ids,t] (COMMA boundVarDecl[ids,t])* RPAREN
-    COLON instantiationPatterns? formula[f]
-    { PARSER_STATE->popScope();
-      UNSUPPORTED("quantifiers not supported yet");
-      f = EXPR_MANAGER->mkVar(EXPR_MANAGER->booleanType());
+  : ( FORALL_TOK { k = kind::FORALL; } | EXISTS_TOK { k = kind::EXISTS; } )
+    { PARSER_STATE->pushScope(); } LPAREN
+    boundVarDecl[ids,t]
+    { for(std::vector<std::string>::const_iterator i = ids.begin(); i != ids.end(); ++i) {
+        bvs.push_back(PARSER_STATE->mkVar(*i, t));
+      }
+      ids.clear();
     }
-  | EXISTS_TOK { PARSER_STATE->pushScope(); } LPAREN
-    boundVarDecl[ids,t] (COMMA boundVarDecl[ids,t])* RPAREN
-    COLON instantiationPatterns? formula[f]
+    ( COMMA boundVarDecl[ids,t]
+      {
+        for(std::vector<std::string>::const_iterator i = ids.begin(); i != ids.end(); ++i) {
+          bvs.push_back(PARSER_STATE->mkVar(*i, t));
+        }
+        ids.clear();
+      }
+    )* RPAREN {
+      terms.push_back( EXPR_MANAGER->mkExpr( kind::BOUND_VAR_LIST, bvs ) ); }
+    COLON instantiationPatterns[ipl]? formula[f]
     { PARSER_STATE->popScope();
-      UNSUPPORTED("quantifiers not supported yet");
-      f = EXPR_MANAGER->mkVar(EXPR_MANAGER->booleanType());
+      terms.push_back(f);
+      if(! ipl.isNull()) {
+        terms.push_back(ipl);
+      }
+      f = MK_EXPR(k, terms);
     }
 
    /* lets: letDecl defines the variables and functionss, we just
@@ -1283,11 +1297,20 @@ prefixFormula[CVC4::Expr& f]
     }
   ;
 
-instantiationPatterns
+instantiationPatterns[ CVC4::Expr& expr ]
 @init {
+  std::vector<Expr> args;
   Expr f;
+  std::vector<Expr> patterns;
 }
-  : ( PATTERN_TOK LPAREN formula[f] (COMMA formula[f])* RPAREN COLON )+
+  : ( PATTERN_TOK LPAREN formula[f] { args.push_back( f ); } (COMMA formula[f] { args.push_back( f ); } )* RPAREN COLON
+      { patterns.push_back( EXPR_MANAGER->mkExpr( kind::INST_PATTERN, args ) );
+        args.clear();
+      } )+
+    { if(! patterns.empty()) {
+       expr = EXPR_MANAGER->mkExpr( kind::INST_PATTERN_LIST, patterns );
+       }
+    }
   ;
 
 /**
@@ -1417,7 +1440,7 @@ tupleStore[CVC4::Expr& f]
   Expr f2;
 }
   : k=numeral ASSIGN_TOK uminusTerm[f2]
-    { 
+    {
       Type t = f.getType();
       if(! t.isDatatype()) {
         PARSER_STATE->parseError("tuple-update applied to non-tuple");
@@ -1456,7 +1479,7 @@ recordStore[CVC4::Expr& f]
   Expr f2;
 }
   : identifier[id,CHECK_NONE,SYM_VARIABLE] ASSIGN_TOK uminusTerm[f2]
-    { 
+    {
       Type t = f.getType();
       if(! t.isDatatype()) {
         PARSER_STATE->parseError("record-update applied to non-record");
diff --git a/src/parser/smt/Smt.g b/src/parser/smt/Smt.g
index 6dd4e78f3..568f3bb92 100644
--- a/src/parser/smt/Smt.g
+++ b/src/parser/smt/Smt.g
@@ -244,6 +244,19 @@ annotatedFormula[CVC4::Expr& expr]
       }
     }
 
+  | /* A quantifier */
+    LPAREN_TOK
+    ( FORALL_TOK { kind = kind::FORALL; } | EXISTS_TOK { kind = kind::EXISTS; } )
+    { PARSER_STATE->pushScope(); }
+    ( LPAREN_TOK let_identifier[name,CHECK_NONE] t=sortSymbol RPAREN_TOK
+      { args.push_back(PARSER_STATE->mkVar(name, t)); }
+    )+
+    annotatedFormula[expr] RPAREN_TOK
+    { args.push_back(expr);
+      expr = MK_EXPR(kind, args);
+      PARSER_STATE->popScope();
+    }
+
   | /* A non-built-in function application */
 
     // Semantic predicate not necessary if parenthesized subexpressions
diff --git a/src/parser/smt/smt.cpp b/src/parser/smt/smt.cpp
index c3b81655c..4d3c1d086 100644
--- a/src/parser/smt/smt.cpp
+++ b/src/parser/smt/smt.cpp
@@ -29,6 +29,10 @@ namespace parser {
 
 std::hash_map<const std::string, Smt::Logic, CVC4::StringHashFunction> Smt::newLogicMap() {
   std::hash_map<const std::string, Smt::Logic, CVC4::StringHashFunction> logicMap;
+  logicMap["AUFLIA"] = AUFLIA;
+  logicMap["AUFLIRA"] = AUFLIRA;
+  logicMap["AUFNIRA"] = AUFNIRA;
+  logicMap["LRA"] = LRA;
   logicMap["QF_AX"] = QF_AX;
   logicMap["QF_BV"] = QF_BV;
   logicMap["QF_IDL"] = QF_IDL;
@@ -54,6 +58,9 @@ std::hash_map<const std::string, Smt::Logic, CVC4::StringHashFunction> Smt::newL
   logicMap["QF_UFNIRA"] = QF_UFNIRA;
   logicMap["QF_AUFLIA"] = QF_AUFLIA;
   logicMap["QF_AUFLIRA"] = QF_AUFLIRA;
+  logicMap["UFNIA"] = UFNIA;
+  logicMap["UFNIRA"] = UFNIRA;
+  logicMap["UFLRA"] = UFLRA;
   logicMap["QF_ALL_SUPPORTED"] = QF_ALL_SUPPORTED;
   logicMap["ALL_SUPPORTED"] = ALL_SUPPORTED;
   return logicMap;
@@ -109,6 +116,22 @@ void Smt::addTheory(Theory theory) {
     break;
   }
 
+  case THEORY_BITVECTOR_ARRAYS_EX: {
+    Unimplemented("Cannot yet handle SMT-LIBv1 bitvector arrays (i.e., the BitVector_ArraysEx theory)");
+    //addOperator(kind::SELECT);
+    //addOperator(kind::STORE);
+    break;
+  }
+
+  case THEORY_INT_INT_REAL_ARRAY_ARRAYS_EX: {
+    defineType("Array1", getExprManager()->mkArrayType(getSort("Int"), getSort("Real")));
+    defineType("Array2", getExprManager()->mkArrayType(getSort("Int"), getSort("Array1")));
+    addOperator(kind::SELECT);
+    addOperator(kind::STORE);
+    break;
+  }
+
+  case THEORY_INT_ARRAYS:
   case THEORY_INT_ARRAYS_EX: {
     defineType("Array", getExprManager()->mkArrayType(getExprManager()->integerType(), getExprManager()->integerType()));
 
@@ -140,6 +163,9 @@ void Smt::addTheory(Theory theory) {
   case THEORY_BITVECTORS:
     break;
 
+  case THEORY_QUANTIFIERS:
+    break;
+
   default:
     Unhandled(theory);
   }
@@ -244,13 +270,14 @@ void Smt::setLogic(const std::string& name) {
     break;
 
   case QF_AUFLIRA:
-    addTheory(THEORY_ARRAYS_EX);
+    addTheory(THEORY_INT_INT_REAL_ARRAY_ARRAYS_EX);
     addUf();
     addTheory(THEORY_INTS);
     addTheory(THEORY_REALS);
     break;
 
   case ALL_SUPPORTED:
+    addTheory(THEORY_QUANTIFIERS);
     /* fall through */
   case QF_ALL_SUPPORTED:
     addTheory(THEORY_ARRAYS_EX);
@@ -261,14 +288,41 @@ void Smt::setLogic(const std::string& name) {
     break;
 
   case AUFLIA:
+    addUf();
+    addTheory(THEORY_INTS);
+    addTheory(THEORY_INT_ARRAYS_EX);
+    addTheory(THEORY_QUANTIFIERS);
+    break;
+
   case AUFLIRA:
   case AUFNIRA:
+    addUf();
+    addTheory(THEORY_INTS);
+    addTheory(THEORY_REALS);
+    addTheory(THEORY_INT_INT_REAL_ARRAY_ARRAYS_EX);
+    addTheory(THEORY_QUANTIFIERS);
+    break;
+
   case LRA:
-  case UFLRA:
   case UFNIA:
-    Unhandled(name);
+    addUf();
+    addTheory(THEORY_INTS);
+    addTheory(THEORY_QUANTIFIERS);
+    break;
+  case UFNIRA:
+    addUf();
+    addTheory(THEORY_INTS);
+    addTheory(THEORY_REALS);
+    addTheory(THEORY_QUANTIFIERS);
+    break;
+
+  case UFLRA:
+    addUf();
+    addTheory(THEORY_REALS);
+    addTheory(THEORY_QUANTIFIERS);
+    break;
   }
-}
+}/* Smt::setLogic() */
 
 }/* CVC4::parser namespace */
 }/* CVC4 namespace */
diff --git a/src/parser/smt/smt.h b/src/parser/smt/smt.h
index d77808930..7b1dfc345 100644
--- a/src/parser/smt/smt.h
+++ b/src/parser/smt/smt.h
@@ -65,6 +65,7 @@ public:
     QF_UFNIRA, // nonstandard
     QF_UFNRA,
     UFLRA,
+    UFNIRA, // nonstandard
     UFNIA,
     QF_ALL_SUPPORTED, // nonstandard
     ALL_SUPPORTED // nonstandard
@@ -75,7 +76,7 @@ public:
     THEORY_ARRAYS_EX,
     THEORY_BITVECTORS,
     THEORY_BITVECTORS_32,
-    THEORY_BITVECTORS_ARRAYS_EX,
+    THEORY_BITVECTOR_ARRAYS_EX,
     THEORY_EMPTY,
     THEORY_INTS,
     THEORY_INT_ARRAYS,
@@ -83,6 +84,7 @@ public:
     THEORY_INT_INT_REAL_ARRAY_ARRAYS_EX,
     THEORY_REALS,
     THEORY_REALS_INTS,
+    THEORY_QUANTIFIERS
   };
 
 private:
diff --git a/src/parser/smt2/Smt2.g b/src/parser/smt2/Smt2.g
index 7a7c7df62..59b6715b9 100644
--- a/src/parser/smt2/Smt2.g
+++ b/src/parser/smt2/Smt2.g
@@ -136,7 +136,10 @@ using namespace CVC4::parser;
  * @return the parsed expression, or the Null Expr if we've reached the end of the input
  */
 parseExpr returns [CVC4::parser::smt2::myExpr expr]
-  : term[expr]
+@declarations {
+  Expr expr2;
+}
+  : term[expr, expr2]
   | EOF
   ;
 
@@ -156,7 +159,7 @@ command returns [CVC4::Command* cmd = NULL]
 @declarations {
   std::string name;
   std::vector<std::string> names;
-  Expr expr;
+  Expr expr, expr2;
   Type t;
   std::vector<Expr> terms;
   std::vector<Type> sorts;
@@ -258,7 +261,7 @@ command returns [CVC4::Command* cmd = NULL]
         terms.push_back(PARSER_STATE->mkVar((*i).first, (*i).second));
       }
     }
-    term[expr]
+    term[expr, expr2]
     { PARSER_STATE->popScope();
       // declare the name down here (while parsing term, signature
       // must not be extended with the name itself; no recursion
@@ -287,7 +290,7 @@ command returns [CVC4::Command* cmd = NULL]
     { cmd = new GetAssignmentCommand; }
   | /* assertion */
     ASSERT_TOK { PARSER_STATE->checkThatLogicIsSet(); }
-    term[expr]
+    term[expr, expr2]
     { cmd = new AssertCommand(expr); }
   | /* checksat */
     CHECKSAT_TOK { PARSER_STATE->checkThatLogicIsSet(); }
@@ -359,7 +362,7 @@ extendedCommand[CVC4::Command*& cmd]
 @declarations {
   std::vector<CVC4::Datatype> dts;
   Type t;
-  Expr e;
+  Expr e, e2;
   SExpr sexpr;
   std::string name;
   std::vector<std::string> names;
@@ -420,7 +423,7 @@ symbolicExpr[CVC4::SExpr& sexpr]
  * Matches a term.
  * @return the expression representing the formula
  */
-term[CVC4::Expr& expr]
+term[CVC4::Expr& expr, CVC4::Expr& expr2]
 @init {
   Debug("parser") << "term: " << AntlrInput::tokenText(LT(1)) << std::endl;
   Kind kind;
@@ -428,6 +431,11 @@ term[CVC4::Expr& expr]
   std::string name;
   std::vector<Expr> args;
   SExpr sexpr;
+  std::vector< std::pair<std::string, Type> > sortedVarNames;
+  Expr f, f2;
+  std::string attr;
+  Expr attexpr;
+  std::vector<Expr> attexprs;
 }
   : /* a built-in operator application */
     LPAREN_TOK builtinOp[kind] termList[args,expr] RPAREN_TOK
@@ -456,10 +464,45 @@ term[CVC4::Expr& expr]
         expr = MK_EXPR(kind, args);
       }
     }
-
+  | LPAREN_TOK quantOp[kind]
+    LPAREN_TOK sortedVarList[sortedVarNames] RPAREN_TOK
+    {
+      PARSER_STATE->pushScope();
+      for(std::vector<std::pair<std::string, CVC4::Type> >::const_iterator i =
+            sortedVarNames.begin(), iend = sortedVarNames.end();
+          i != iend;
+          ++i) {
+        args.push_back(PARSER_STATE->mkVar((*i).first, (*i).second));
+      }
+      Expr bvl = MK_EXPR(kind::BOUND_VAR_LIST, args);
+      args.clear();
+      args.push_back(bvl);
+    }
+    term[f, f2] RPAREN_TOK
+    {
+      PARSER_STATE->popScope();
+      switch(f.getKind()) {
+      case CVC4::kind::RR_REWRITE:
+      case CVC4::kind::RR_REDUCTION:
+      case CVC4::kind::RR_DEDUCTION:
+        if(kind == CVC4::kind::EXISTS) {
+          PARSER_STATE->parseError("Use Exists instead of Forall for a rewrite rule.");
+        }
+        args.push_back(f2); // guards
+        args.push_back(f); // rule
+        expr = MK_EXPR(CVC4::kind::REWRITE_RULE, args);
+        break;
+      default:
+        args.push_back(f);
+        if(! f2.isNull()){
+          args.push_back(f2);
+        }
+        expr = MK_EXPR(kind, args);
+      }
+    }
   | /* A non-built-in function application */
     LPAREN_TOK
-    functionName[name,CHECK_DECLARED]
+    functionName[name, CHECK_DECLARED]
     { PARSER_STATE->checkFunctionLike(name);
       const bool isDefinedFunction =
         PARSER_STATE->isDefinedFunction(name);
@@ -469,13 +512,13 @@ term[CVC4::Expr& expr]
       } else {
         expr = PARSER_STATE->getVariable(name);
         Type t = expr.getType();
-        if( t.isConstructor() ){
+        if(t.isConstructor()) {
           kind = CVC4::kind::APPLY_CONSTRUCTOR;
-        }else if( t.isSelector() ){
+        } else if(t.isSelector()) {
           kind = CVC4::kind::APPLY_SELECTOR;
-        }else if( t.isTester() ){
+        } else if(t.isTester()) {
           kind = CVC4::kind::APPLY_TESTER;
-        }else{
+        } else {
           kind = CVC4::kind::APPLY_UF;
         }
       }
@@ -494,10 +537,10 @@ term[CVC4::Expr& expr]
   | /* a let binding */
     LPAREN_TOK LET_TOK LPAREN_TOK
     { PARSER_STATE->pushScope(); }
-    ( LPAREN_TOK symbol[name,CHECK_UNDECLARED,SYM_VARIABLE] term[expr] RPAREN_TOK
+    ( LPAREN_TOK symbol[name,CHECK_UNDECLARED,SYM_VARIABLE] term[expr, f2] RPAREN_TOK
       { PARSER_STATE->defineVar(name,expr); } )+
     RPAREN_TOK
-    term[expr]
+    term[expr, f2]
     RPAREN_TOK
     { PARSER_STATE->popScope(); }
 
@@ -519,26 +562,45 @@ term[CVC4::Expr& expr]
     }
 
     /* attributed expressions */
-  | LPAREN_TOK ATTRIBUTE_TOK term[expr] KEYWORD symbolicExpr[sexpr] RPAREN_TOK
-    { std::string attr = AntlrInput::tokenText($KEYWORD);
-      if(attr == ":named") {
-        name = sexpr.getValue();
-        // FIXME ensure expr is a closed subterm
-        // check that sexpr is a fresh function symbol
-        PARSER_STATE->checkDeclaration(name, CHECK_UNDECLARED, SYM_VARIABLE);
-        // define it
-        Expr func = PARSER_STATE->mkFunction(name, expr.getType());
-        // bind name to expr with define-fun
-        Command* c =
-          new DefineNamedFunctionCommand(name, func, std::vector<Expr>(), expr);
-        PARSER_STATE->preemptCommand(c);
-      } else {
-        std::stringstream ss;
-        ss << "Attribute `" << attr << "' not supported";
-        PARSER_STATE->parseError(ss.str());
+  | LPAREN_TOK ATTRIBUTE_TOK term[expr, f2]
+    ( attribute[expr, attexpr,attr]
+      { if(! attexpr.isNull()) {
+          attexprs.push_back(attexpr);
+        }
       }
-    }
+    )+ RPAREN_TOK
+    {
+      if(attr == ":rewrite-rule") {
+        Expr guard;
+        Expr body;
+        if(expr[1].getKind() == kind::IMPLIES ||
+           expr[1].getKind() == kind::IFF ||
+           expr[1].getKind() == kind::EQUAL) {
+          guard = expr[0];
+          body = expr[1];
+        } else {
+          guard = MK_CONST(bool(true));
+          body = expr;
+        }
+        expr2 = guard;
+        args.push_back(body[0]);
+        args.push_back(body[1]);
+        if(!f2.isNull()) {
+          args.push_back(f2);
+        }
+
+        if     ( body.getKind()==kind::IMPLIES )    kind = kind::RR_DEDUCTION;
+        else if( body.getKind()==kind::IFF )        kind = kind::RR_REDUCTION;
+        else if( body.getKind()==kind::EQUAL )      kind = kind::RR_REWRITE;
+        else PARSER_STATE->parseError("Error parsing rewrite rule.");
 
+        expr = MK_EXPR( kind, args );
+      } else if(! attexprs.empty()) {
+        if(attexprs[0].getKind() == kind::INST_PATTERN) {
+          expr2 = MK_EXPR(kind::INST_PATTERN_LIST, attexprs);
+        }
+      }
+    }
     /* constants */
   | INTEGER_LITERAL
     { expr = MK_CONST( AntlrInput::tokenToInteger($INTEGER_LITERAL) ); }
@@ -570,6 +632,46 @@ term[CVC4::Expr& expr]
   ;
 
 /**
+ * Read attribute
+ */
+attribute[CVC4::Expr& expr,CVC4::Expr& retExpr, std::string& attr]
+@init {
+  SExpr sexpr;
+  Expr patexpr;
+  std::vector<Expr> patexprs;
+  Expr e2;
+}
+: KEYWORD
+  { attr = AntlrInput::tokenText($KEYWORD); }
+  symbolicExpr[sexpr]
+  { if(attr == ":named") {
+      std::string name = sexpr.getValue();
+      // FIXME ensure expr is a closed subterm
+      // check that sexpr is a fresh function symbol
+      PARSER_STATE->checkDeclaration(name, CHECK_UNDECLARED, SYM_VARIABLE);
+      // define it
+      Expr func = PARSER_STATE->mkFunction(name, expr.getType());
+      // bind name to expr with define-fun
+      Command* c =
+        new DefineNamedFunctionCommand(name, func, std::vector<Expr>(), expr);
+      PARSER_STATE->preemptCommand(c);
+    } else {
+      std::stringstream ss;
+      ss << "Attribute `" << attr << "' not supported";
+      PARSER_STATE->parseError(ss.str());
+    }
+  }
+  | ATTRIBUTE_PATTERN_TOK LPAREN_TOK ( term[patexpr, e2] { patexprs.push_back( patexpr ); }  )+ RPAREN_TOK
+    {
+      attr = std::string(":pattern");
+      retExpr = MK_EXPR(kind::INST_PATTERN, patexprs);
+    }
+  | ATTRIBUTE_REWRITE_RULE {
+    attr = std::string(":rewrite-rule");
+  }
+  ;
+
+/**
  * Matches a bit-vector operator (the ones parametrized by numbers)
  */
 indexedFunctionName[CVC4::Expr& op]
@@ -613,7 +715,10 @@ badIndexedFunctionName
 /* NOTE: We pass an Expr in here just to avoid allocating a fresh Expr every
  * time through this rule. */
 termList[std::vector<CVC4::Expr>& formulas, CVC4::Expr& expr]
-  : ( term[expr] { formulas.push_back(expr); } )+
+@declarations {
+  Expr expr2;
+}
+  : ( term[expr, expr2] { formulas.push_back(expr); } )+
   ;
 
 /**
@@ -693,6 +798,14 @@ builtinOp[CVC4::Kind& kind]
   // NOTE: Theory operators go here
   ;
 
+quantOp[CVC4::Kind& kind]
+@init {
+  Debug("parser") << "quant: " << AntlrInput::tokenText(LT(1)) << std::endl;
+}
+  : EXISTS_TOK      { $kind = CVC4::kind::EXISTS; }
+  | FORALL_TOK    { $kind = CVC4::kind::FORALL; }
+  ;
+
 /**
  * Matches a (possibly undeclared) function symbol (returning the string)
  * @param check what kind of check to do with the symbol
@@ -760,12 +873,12 @@ sortSymbol[CVC4::Type& t, CVC4::parser::DeclarationCheck check]
   std::vector<uint64_t> numerals;
 }
   : sortName[name,CHECK_NONE]
-  	{ 
-  	  if( check == CHECK_DECLARED || PARSER_STATE->isDeclared(name, SYM_SORT) ){ 
-  	    t = PARSER_STATE->getSort(name);                                          
-  	  }else{                                                                    
-  	    t = PARSER_STATE->mkUnresolvedType(name);                                 
-  	  }                                          
+  	{
+  	  if( check == CHECK_DECLARED || PARSER_STATE->isDeclared(name, SYM_SORT) ){
+  	    t = PARSER_STATE->getSort(name);
+  	  }else{
+  	    t = PARSER_STATE->mkUnresolvedType(name);
+  	  }
   	}
   | LPAREN_TOK INDEX_TOK symbol[name,CHECK_NONE,SYM_SORT] nonemptyNumeralList[numerals] RPAREN_TOK
     {
@@ -929,6 +1042,10 @@ POP_TOK : 'pop';
 DECLARE_DATATYPES_TOK : 'declare-datatypes';
 ECHO_TOK : 'echo';
 
+// attributes
+ATTRIBUTE_PATTERN_TOK : ':pattern';
+ATTRIBUTE_REWRITE_RULE : ':rewrite-rule';
+
 // operators (NOTE: theory symbols go here)
 AMPERSAND_TOK     : '&';
 AND_TOK           : 'and';
diff --git a/src/parser/smt2/smt2.cpp b/src/parser/smt2/smt2.cpp
index 709ba087f..549878e46 100644
--- a/src/parser/smt2/smt2.cpp
+++ b/src/parser/smt2/smt2.cpp
@@ -86,6 +86,9 @@ void Smt2::addTheory(Theory theory) {
   case THEORY_BITVECTORS:
     break;
 
+  case THEORY_QUANTIFIERS:
+    break;
+
   default:
     Unhandled(theory);
   }
@@ -195,6 +198,7 @@ void Smt2::setLogic(const std::string& name) {
     break;
 
   case Smt::ALL_SUPPORTED:
+    addTheory(THEORY_QUANTIFIERS);
     /* fall through */
   case Smt::QF_ALL_SUPPORTED:
     addTheory(THEORY_ARRAYS);
@@ -208,11 +212,25 @@ void Smt2::setLogic(const std::string& name) {
   case Smt::AUFLIRA:
   case Smt::AUFNIRA:
   case Smt::LRA:
-  case Smt::UFLRA:
   case Smt::UFNIA:
-    Unhandled(name);
+  case Smt::UFNIRA:
+  case Smt::UFLRA:
+    if(d_logic != Smt::AUFLIA && d_logic != Smt::UFNIA) {
+      addTheory(THEORY_REALS);
+    }
+    if(d_logic != Smt::LRA) {
+      addOperator(kind::APPLY_UF);
+      if(d_logic != Smt::UFLRA) {
+        addTheory(THEORY_INTS);
+        if(d_logic != Smt::UFNIA && d_logic != Smt::UFNIRA) {
+          addTheory(THEORY_ARRAYS);
+        }
+      }
+    }
+    addTheory(THEORY_QUANTIFIERS);
+    break;
   }
-}
+}/* Smt2::setLogic() */
 
 void Smt2::setInfo(const std::string& flag, const SExpr& sexpr) {
   // TODO: ???
diff --git a/src/parser/smt2/smt2.h b/src/parser/smt2/smt2.h
index b71f63558..9d33e3e62 100644
--- a/src/parser/smt2/smt2.h
+++ b/src/parser/smt2/smt2.h
@@ -41,6 +41,7 @@ public:
     THEORY_INTS,
     THEORY_REALS,
     THEORY_REALS_INTS,
+    THEORY_QUANTIFIERS,
   };
 
 private: