Merge branch 'master' into splitEqRewsplitEqRew

20 files changed, 716 insertions, 801 deletions

diff --git a/src/expr/node.h b/src/expr/node.h
index f0ee7a56c..b8a665f0c 100644
--- a/src/expr/node.h
+++ b/src/expr/node.h
@@ -468,7 +468,8 @@ public:
   inline bool isClosure() const {
     assertTNodeNotExpired();
     return getKind() == kind::LAMBDA || getKind() == kind::FORALL
-           || getKind() == kind::EXISTS || getKind() == kind::CHOICE;
+           || getKind() == kind::EXISTS || getKind() == kind::CHOICE
+           || getKind() == kind::MATCH_BIND_CASE;
   }
 
   /**
diff --git a/src/expr/type_checker_template.cpp b/src/expr/type_checker_template.cpp
index 078c275f8..9ca5f00cc 100644
--- a/src/expr/type_checker_template.cpp
+++ b/src/expr/type_checker_template.cpp
@@ -16,13 +16,14 @@
 
 #line 18 "${template}"
 
-#include "expr/type_checker.h"
 #include "expr/node_manager.h"
 #include "expr/node_manager_attributes.h"
+#include "expr/type_checker.h"
+#include "expr/type_checker_util.h"
 
 ${typechecker_includes}
 
-#line 26 "${template}"
+#line 27 "${template}"
 
 namespace CVC4 {
 namespace expr {
@@ -43,7 +44,7 @@ TypeNode TypeChecker::computeType(NodeManager* nodeManager, TNode n, bool check)
 
 ${typerules}
 
-#line 47 "${template}"
+#line 48 "${template}"
 
   default:
     Debug("getType") << "FAILURE" << std::endl;
@@ -65,7 +66,7 @@ bool TypeChecker::computeIsConst(NodeManager* nodeManager, TNode n)
   switch(n.getKind()) {
 ${construles}
 
-#line 69 "${template}"
+#line 70 "${template}"
 
   default:;
   }
@@ -81,7 +82,7 @@ bool TypeChecker::neverIsConst(NodeManager* nodeManager, TNode n)
   switch(n.getKind()) {
 ${neverconstrules}
 
-#line 85 "${template}"
+#line 86 "${template}"
 
   default:;
   }
diff --git a/src/expr/type_checker_util.h b/src/expr/type_checker_util.h
new file mode 100644
index 000000000..fc5513d7b
--- /dev/null
+++ b/src/expr/type_checker_util.h
@@ -0,0 +1,203 @@
+/*********************                                                        */
+/*! \file type_checker_util.h
+ ** \verbatim
+ ** Top contributors (to current version):
+ **   Andres Noetzli
+ ** This file is part of the CVC4 project.
+ ** Copyright (c) 2009-2019 by the authors listed in the file AUTHORS
+ ** in the top-level source directory) and their institutional affiliations.
+ ** All rights reserved.  See the file COPYING in the top-level source
+ ** directory for licensing information.\endverbatim
+ **
+ ** \brief Templates for simple type rules
+ **
+ ** This file defines templates for simple type rules. If a kind has the a
+ ** type rule where each argument matches exactly a specific sort, these
+ ** templates can be used to define typechecks without writing dedicated classes
+ ** for them.
+ **/
+
+#include "cvc4_private.h"
+
+#include "expr/kind.h"
+#include "expr/node.h"
+#include "expr/node_manager.h"
+#include "expr/type_node.h"
+
+namespace CVC4 {
+namespace expr {
+
+/** Type check returns the builtin operator sort */
+struct RBuiltinOperator
+{
+  static TypeNode mkType(NodeManager* nm) { return nm->builtinOperatorType(); }
+};
+
+/** Type check returns the Boolean sort */
+struct RBool
+{
+  static TypeNode mkType(NodeManager* nm) { return nm->booleanType(); }
+};
+
+/** Type check returns the integer sort */
+struct RInteger
+{
+  static TypeNode mkType(NodeManager* nm) { return nm->integerType(); }
+};
+
+/** Type check returns the real sort */
+struct RReal
+{
+  static TypeNode mkType(NodeManager* nm) { return nm->realType(); }
+};
+
+/** Type check returns the regexp sort */
+struct RRegExp
+{
+  static TypeNode mkType(NodeManager* nm) { return nm->regExpType(); }
+};
+
+/** Type check returns the string sort */
+struct RString
+{
+  static TypeNode mkType(NodeManager* nm) { return nm->stringType(); }
+};
+
+/** Argument does not exist */
+struct ANone
+{
+  static bool checkArg(TNode n, size_t arg)
+  {
+    Assert(arg >= n.getNumChildren());
+    return true;
+  }
+  constexpr static const char* typeName = "<none>";
+};
+
+/** Argument is optional */
+template<class A>
+struct AOptional
+{
+  static bool checkArg(TNode n, size_t arg)
+  {
+    if (arg < n.getNumChildren()) {
+      return A::checkArg(n, arg);
+    }
+    return true;
+  }
+  constexpr static const char* typeName = A::typeName;
+};
+
+/** Argument is an integer */
+struct AInteger
+{
+  static bool checkArg(TNode n, size_t arg)
+  {
+    TypeNode t = n[arg].getType(true);
+    return t.isInteger();
+  }
+  constexpr static const char* typeName = "integer";
+};
+
+/** Argument is a real */
+struct AReal
+{
+  static bool checkArg(TNode n, size_t arg)
+  {
+    TypeNode t = n[arg].getType(true);
+    return t.isReal();
+  }
+  constexpr static const char* typeName = "real";
+};
+
+/** Argument is a regexp */
+struct ARegExp
+{
+  static bool checkArg(TNode n, size_t arg)
+  {
+    TypeNode t = n[arg].getType(true);
+    return t.isRegExp();
+  }
+  constexpr static const char* typeName = "regexp";
+};
+
+/** Argument is a string */
+struct AString
+{
+  static bool checkArg(TNode n, size_t arg)
+  {
+    TypeNode t = n[arg].getType(true);
+    return t.isString();
+  }
+  constexpr static const char* typeName = "string";
+};
+
+/** 
+ * The SimpleTypeRule template can be used to obtain a simple type rule by
+ * defining a return type and the argument types (up to three arguments are
+ * supported).
+ * */
+template <class R, class A0 = ANone, class A1 = ANone, class A2 = ANone>
+class SimpleTypeRule
+{
+ public:
+  static TypeNode computeType(NodeManager* nm, TNode n, bool check)
+  {
+    if (check)
+    {
+      if (!A0::checkArg(n, 0))
+      {
+        std::stringstream msg;
+        msg << "Expecting a " << A0::typeName
+            << " term as the first argument in '" << n.getKind() << "'";
+        throw TypeCheckingExceptionPrivate(n, msg.str());
+      }
+      if (!A1::checkArg(n, 1))
+      {
+        std::stringstream msg;
+        msg << "Expecting a " << A1::typeName
+            << " term as the second argument in '" << n.getKind() << "'";
+        throw TypeCheckingExceptionPrivate(n, msg.str());
+      }
+      if (!A2::checkArg(n, 2))
+      {
+        std::stringstream msg;
+        msg << "Expecting a " << A2::typeName
+            << " term as the third argument in '" << n.getKind() << "'";
+        throw TypeCheckingExceptionPrivate(n, msg.str());
+      }
+    }
+    return R::mkType(nm);
+  }
+};
+
+/** 
+ * The SimpleTypeRuleVar template can be used to obtain a simple type rule for
+ * operators with a variable number of arguments. It takes the return type and
+ * the type of the arguments as template parameters.
+ * */
+template <class R, class A>
+class SimpleTypeRuleVar
+{
+ public:
+  static TypeNode computeType(NodeManager* nm, TNode n, bool check)
+  {
+    if (check)
+    {
+      for (size_t i = 0, size = n.getNumChildren(); i < size; i++)
+      {
+        if (!A::checkArg(n, i))
+        {
+          std::stringstream msg;
+          msg << "Expecting a " << A::typeName << " term as argument " << i
+              << " in '" << n.getKind() << "'";
+          throw TypeCheckingExceptionPrivate(n, msg.str());
+        }
+      }
+    }
+    return R::mkType(nm);
+  }
+};
+
+}  // namespace expr
+}  // namespace CVC4
diff --git a/src/options/options_template.cpp b/src/options/options_template.cpp
index bfe4347d9..9e18dcb51 100644
--- a/src/options/options_template.cpp
+++ b/src/options/options_template.cpp
@@ -438,7 +438,7 @@ Languages currently supported as arguments to the -L / --lang option:\n\
   smt2.6 | smtlib2.6             SMT-LIB format 2.6\n\
   smt2.6.1 | smtlib2.6.1         SMT-LIB format 2.6 with support for the strings standard\n\
   tptp                           TPTP format (cnf, fof and tff)\n\
-  sygus                          SyGuS format\n\
+  sygus | sygus2                 SyGuS version 1.0 and 2.0 formats\n\
 \n\
 Languages currently supported as arguments to the --output-lang option:\n\
   auto                           match output language to input language\n\
diff --git a/src/parser/smt2/Smt2.g b/src/parser/smt2/Smt2.g
index 21e09317d..e838398ba 100644
--- a/src/parser/smt2/Smt2.g
+++ b/src/parser/smt2/Smt2.g
@@ -1096,13 +1096,13 @@ sygusGrammar[CVC4::Type & ret,
         PARSER_STATE->addSygusConstructorVariables(
             datatypes[dtProcessed], sygusVars, t);
       }
-    )*
+    )+
     RPAREN_TOK
     RPAREN_TOK
     {
       dtProcessed++;
     }
-  )*
+  )+
   RPAREN_TOK
   {
     if (dtProcessed != sortedVarNames.size())
@@ -1122,6 +1122,30 @@ sygusGrammar[CVC4::Type & ret,
       bool aci = allowConst.find(i)!=allowConst.end();
       Type btt = sortedVarNames[i].second;
       datatypes[i].setSygus(btt, bvl, aci, false);
+      Trace("parser-sygus2") << "- " << datatypes[i].getName()
+                             << ", #cons= " << datatypes[i].getNumConstructors()
+                             << ", aci= " << aci << std::endl;
+      // We can be in a case where the only rule specified was (Variable T)
+      // and there are no variables of type T, in which case this is a bogus
+      // grammar. This results in the error below.
+      // We can also be in a case where the only rule specified was
+      // (Constant T), in which case we have not yet added a constructor. We
+      // ensure an arbitrary constant is added in this case.
+      if (datatypes[i].getNumConstructors() == 0)
+      {
+        if (aci)
+        {
+          Expr c = btt.mkGroundTerm();
+          PARSER_STATE->addSygusConstructorTerm(datatypes[i], c, ntsToUnres);
+        }
+        else
+        {
+          std::stringstream se;
+          se << "Grouped rule listing for " << datatypes[i].getName()
+             << " produced an empty rule list.";
+          PARSER_STATE->parseError(se.str());
+        }
+      }
     }
     // pop scope from the pre-declaration
     PARSER_STATE->popScope();
@@ -1810,15 +1834,14 @@ termNonVariable[CVC4::Expr& expr, CVC4::Expr& expr2]
   std::string attr;
   Expr attexpr;
   std::vector<Expr> patexprs;
-  std::vector<Expr> patconds;
+  std::vector<Expr> matchcases;
   std::unordered_set<std::string> names;
   std::vector< std::pair<std::string, Expr> > binders;
-  int match_vindex = -1;
-  std::vector<Type> match_ptypes;
   Type type;
   Type type2;
   api::Term atomTerm;
   ParseOp p;
+  std::vector<Type> argTypes;
 }
   : LPAREN_TOK quantOp[kind]
     LPAREN_TOK sortedVarList[sortedVarNames] RPAREN_TOK
@@ -1912,107 +1935,92 @@ termNonVariable[CVC4::Expr& expr, CVC4::Expr& expr2]
     }
     LPAREN_TOK
     (
-      /* match cases */
-       LPAREN_TOK INDEX_TOK term[f, f2] {
-          if( match_vindex==-1 ){
-            match_vindex = (int)patexprs.size();
+      // case with non-nullary pattern
+      LPAREN_TOK LPAREN_TOK term[f, f2] {
+          args.clear();
+          PARSER_STATE->pushScope(true);
+          // f should be a constructor
+          type = f.getType();
+          Debug("parser-dt") << "Pattern head : " << f << " " << type << std::endl;
+          if (!type.isConstructor())
+          {
+            PARSER_STATE->parseError("Pattern must be application of a constructor or a variable.");
           }
-          patexprs.push_back( f );
-          patconds.push_back(MK_CONST(bool(true)));
+          if (Datatype::datatypeOf(f).isParametric())
+          {
+            type = Datatype::datatypeOf(f)[Datatype::indexOf(f)].getSpecializedConstructorType(expr.getType());
+          }
+          argTypes = static_cast<ConstructorType>(type).getArgTypes();
+        }
+        // arguments of the pattern
+        ( symbol[name,CHECK_NONE,SYM_VARIABLE] {
+            if (args.size() >= argTypes.size())
+            {
+              PARSER_STATE->parseError("Too many arguments for pattern.");
+            }
+            //make of proper type
+            Expr arg = PARSER_STATE->mkBoundVar(name, argTypes[args.size()]);
+            args.push_back( arg );
+          }
+        )*
+        RPAREN_TOK term[f3, f2] {
+          // make the match case
+          std::vector<Expr> cargs;
+          cargs.push_back(f);
+          cargs.insert(cargs.end(),args.begin(),args.end());
+          Expr c = MK_EXPR(kind::APPLY_CONSTRUCTOR,cargs);
+          Expr bvl = MK_EXPR(kind::BOUND_VAR_LIST,args);
+          Expr mc = MK_EXPR(kind::MATCH_BIND_CASE, bvl, c, f3);
+          matchcases.push_back(mc);
+          // now, pop the scope
+          PARSER_STATE->popScope();
         }
         RPAREN_TOK
-      | LPAREN_TOK LPAREN_TOK term[f, f2] {
-           args.clear();
-           PARSER_STATE->pushScope(true);
-           //f should be a constructor
-           type = f.getType();
-           Debug("parser-dt") << "Pattern head : " << f << " " << f.getType() << std::endl;
-           if( !type.isConstructor() ){
-             PARSER_STATE->parseError("Pattern must be application of a constructor or a variable.");
-           }
-           if( Datatype::datatypeOf(f).isParametric() ){
-             type = Datatype::datatypeOf(f)[Datatype::indexOf(f)].getSpecializedConstructorType(expr.getType());
-           }
-           match_ptypes = ((ConstructorType)type).getArgTypes();
-         }
-         //arguments
-         ( symbol[name,CHECK_NONE,SYM_VARIABLE] {
-             if( args.size()>=match_ptypes.size() ){
-               PARSER_STATE->parseError("Too many arguments for pattern.");
-             }
-             //make of proper type
-             Expr arg = PARSER_STATE->mkBoundVar(name, match_ptypes[args.size()]);
-             args.push_back( arg );
-           }
-         )*
-         RPAREN_TOK
-         term[f3, f2] {
-           const DatatypeConstructor& dtc = Datatype::datatypeOf(f)[Datatype::indexOf(f)];
-           if( args.size()!=dtc.getNumArgs() ){
-             PARSER_STATE->parseError("Bad number of arguments for application of constructor in pattern.");
-           }
-           //FIXME: make MATCH a kind and make this a rewrite
-           // build a lambda
-           std::vector<Expr> largs;
-           largs.push_back( MK_EXPR( CVC4::kind::BOUND_VAR_LIST, args ) );
-           largs.push_back( f3 );
-           std::vector< Expr > aargs;
-           aargs.push_back( MK_EXPR( CVC4::kind::LAMBDA, largs ) );
-           for( unsigned i=0; i<dtc.getNumArgs(); i++ ){
-             //can apply total version since we will be guarded by ITE condition
-             // however, we need to apply partial version since we don't have the internal selector available
-             aargs.push_back( MK_EXPR( CVC4::kind::APPLY_SELECTOR, dtc[i].getSelector(), expr ) );
-           }
-           patexprs.push_back( MK_EXPR( CVC4::kind::APPLY_UF, aargs ) );
-           patconds.push_back( MK_EXPR( CVC4::kind::APPLY_TESTER, dtc.getTester(), expr ) );
-         }
-         RPAREN_TOK
-         { PARSER_STATE->popScope(); }
-       | LPAREN_TOK symbol[name,CHECK_DECLARED,SYM_VARIABLE] {
-           f = PARSER_STATE->getVariable(name);
-           type = f.getType();
-           if( !type.isConstructor() || !((ConstructorType)type).getArgTypes().empty() ){
-             PARSER_STATE->parseError("Must apply constructors of arity greater than 0 to arguments in pattern.");
-           }
-         }
-         term[f3, f2] {
-           const DatatypeConstructor& dtc = Datatype::datatypeOf(f)[Datatype::indexOf(f)];
-           patexprs.push_back( f3 );
-           patconds.push_back( MK_EXPR( CVC4::kind::APPLY_TESTER, dtc.getTester(), expr ) );
-         }
-         RPAREN_TOK
-    )+
-    RPAREN_TOK RPAREN_TOK  {
-      if( match_vindex==-1 ){
-        const Datatype& dt = ((DatatypeType)expr.getType()).getDatatype();
-        std::map< unsigned, bool > processed;
-        unsigned count = 0;
-        //ensure that all datatype constructors are matched (to ensure exhaustiveness)
-        for( unsigned i=0; i<patconds.size(); i++ ){
-          unsigned curr_index = Datatype::indexOf(patconds[i].getOperator());
-          if( curr_index<0 && curr_index>=dt.getNumConstructors() ){
-            PARSER_STATE->parseError("Pattern is not legal for the head of a match.");
+      // case with nullary or variable pattern
+      | LPAREN_TOK symbol[name,CHECK_NONE,SYM_VARIABLE] {
+          if (PARSER_STATE->isDeclared(name,SYM_VARIABLE))
+          {
+            f = PARSER_STATE->getVariable(name);
+            type = f.getType();
+            if (!type.isConstructor() || 
+                !((ConstructorType)type).getArgTypes().empty())
+            {
+              PARSER_STATE->parseError("Must apply constructors of arity greater than 0 to arguments in pattern.");
+            }
+            // make nullary constructor application
+            f = MK_EXPR(kind::APPLY_CONSTRUCTOR, f);
           }
-          if( processed.find( curr_index )==processed.end() ){
-            processed[curr_index] = true;
-            count++;
+          else
+          {
+            // it has the type of the head expr
+            f = PARSER_STATE->mkBoundVar(name, expr.getType());
           }
         }
-        if( count!=dt.getNumConstructors() ){
-          PARSER_STATE->parseError("Patterns are not exhaustive in a match construct.");
-        }
-      }
-      //now, make the ITE
-      int end_index = match_vindex==-1 ? patexprs.size()-1 : match_vindex;
-      bool first_time = true;
-      for( int index = end_index; index>=0; index-- ){
-        if( first_time ){
-          expr = patexprs[index];
-          first_time = false;
-        }else{
-          expr = MK_EXPR( CVC4::kind::ITE, patconds[index], patexprs[index], expr );
+        term[f3, f2] {
+          Expr mc;
+          if (f.getKind() == kind::BOUND_VARIABLE)
+          {
+            Expr bvl = MK_EXPR(kind::BOUND_VAR_LIST, f);
+            mc = MK_EXPR(kind::MATCH_BIND_CASE, bvl, f, f3);
+          }
+          else
+          {
+            mc = MK_EXPR(kind::MATCH_CASE, f, f3);
+          }
+          matchcases.push_back(mc);
         }
+        RPAREN_TOK
+    )+
+    RPAREN_TOK RPAREN_TOK  {
+      //now, make the match
+      if (matchcases.empty())
+      {
+        PARSER_STATE->parseError("Must have at least one case in match.");
       }
+      std::vector<Expr> mchildren;
+      mchildren.push_back(expr);
+      mchildren.insert(mchildren.end(), matchcases.begin(), matchcases.end());
+      expr = MK_EXPR(kind::MATCH, mchildren);
     }
 
     /* attributed expressions */
diff --git a/src/printer/smt2/smt2_printer.cpp b/src/printer/smt2/smt2_printer.cpp
index df9bee981..013288880 100644
--- a/src/printer/smt2/smt2_printer.cpp
+++ b/src/printer/smt2/smt2_printer.cpp
@@ -540,7 +540,31 @@ void Smt2Printer::toStream(std::ostream& out,
     }
     return;
 
-  case kind::LAMBDA:
+  case kind::LAMBDA: out << smtKindString(k, d_variant) << " "; break;
+  case kind::MATCH:
+    out << smtKindString(k, d_variant) << " ";
+    toStream(out, n[0], toDepth, types, TypeNode::null());
+    out << " (";
+    for (size_t i = 1, nchild = n.getNumChildren(); i < nchild; i++)
+    {
+      if (i > 1)
+      {
+        out << " ";
+      }
+      toStream(out, n[i], toDepth, types, TypeNode::null());
+    }
+    out << "))";
+    return;
+  case kind::MATCH_BIND_CASE:
+    // ignore the binder
+    toStream(out, n[1], toDepth, types, TypeNode::null());
+    out << " ";
+    toStream(out, n[2], toDepth, types, TypeNode::null());
+    out << ")";
+    return;
+  case kind::MATCH_CASE:
+    // do nothing
+    break;
   case kind::CHOICE: out << smtKindString(k, d_variant) << " "; break;
 
   // arith theory
@@ -1030,6 +1054,7 @@ static string smtKindString(Kind k, Variant v)
 
   case kind::LAMBDA:
     return "lambda";
+  case kind::MATCH: return "match";
   case kind::CHOICE: return "choice";
 
   // arith theory
diff --git a/src/theory/arith/kinds b/src/theory/arith/kinds
index 95d1aa9c1..409534050 100644
--- a/src/theory/arith/kinds
+++ b/src/theory/arith/kinds
@@ -94,40 +94,40 @@ typerule POW ::CVC4::theory::arith::ArithOperatorTypeRule
 
 typerule CONST_RATIONAL ::CVC4::theory::arith::ArithConstantTypeRule
 
-typerule LT ::CVC4::theory::arith::ArithPredicateTypeRule
-typerule LEQ ::CVC4::theory::arith::ArithPredicateTypeRule
-typerule GT ::CVC4::theory::arith::ArithPredicateTypeRule
-typerule GEQ ::CVC4::theory::arith::ArithPredicateTypeRule
+typerule LT "SimpleTypeRule<RBool, AReal, AReal>"
+typerule LEQ "SimpleTypeRule<RBool, AReal, AReal>"
+typerule GT "SimpleTypeRule<RBool, AReal, AReal>"
+typerule GEQ "SimpleTypeRule<RBool, AReal, AReal>"
 
 typerule TO_REAL ::CVC4::theory::arith::ArithOperatorTypeRule
 typerule TO_INTEGER ::CVC4::theory::arith::ArithOperatorTypeRule
-typerule IS_INTEGER ::CVC4::theory::arith::ArithUnaryPredicateTypeRule
+typerule IS_INTEGER "SimpleTypeRule<RBool, AReal>"
 
-typerule ABS ::CVC4::theory::arith::IntOperatorTypeRule
-typerule INTS_DIVISION ::CVC4::theory::arith::IntOperatorTypeRule
-typerule INTS_MODULUS ::CVC4::theory::arith::IntOperatorTypeRule
-typerule DIVISIBLE ::CVC4::theory::arith::IntUnaryPredicateTypeRule
-typerule DIVISIBLE_OP ::CVC4::theory::arith::DivisibleOpTypeRule
+typerule ABS "SimpleTypeRule<RInteger, AInteger>"
+typerule INTS_DIVISION "SimpleTypeRule<RInteger, AInteger, AInteger>"
+typerule INTS_MODULUS "SimpleTypeRule<RInteger, AInteger, AInteger>"
+typerule DIVISIBLE "SimpleTypeRule<RBool, AInteger>"
+typerule DIVISIBLE_OP "SimpleTypeRule<RBuiltinOperator>"
 
 typerule DIVISION_TOTAL ::CVC4::theory::arith::ArithOperatorTypeRule
-typerule INTS_DIVISION_TOTAL ::CVC4::theory::arith::IntOperatorTypeRule
-typerule INTS_MODULUS_TOTAL ::CVC4::theory::arith::IntOperatorTypeRule
-
-typerule EXPONENTIAL ::CVC4::theory::arith::RealOperatorTypeRule
-typerule SINE ::CVC4::theory::arith::RealOperatorTypeRule
-typerule COSINE ::CVC4::theory::arith::RealOperatorTypeRule
-typerule TANGENT ::CVC4::theory::arith::RealOperatorTypeRule
-typerule COSECANT ::CVC4::theory::arith::RealOperatorTypeRule
-typerule SECANT ::CVC4::theory::arith::RealOperatorTypeRule
-typerule COTANGENT ::CVC4::theory::arith::RealOperatorTypeRule
-typerule ARCSINE ::CVC4::theory::arith::RealOperatorTypeRule
-typerule ARCCOSINE ::CVC4::theory::arith::RealOperatorTypeRule
-typerule ARCTANGENT ::CVC4::theory::arith::RealOperatorTypeRule
-typerule ARCCOSECANT ::CVC4::theory::arith::RealOperatorTypeRule
-typerule ARCSECANT ::CVC4::theory::arith::RealOperatorTypeRule
-typerule ARCCOTANGENT ::CVC4::theory::arith::RealOperatorTypeRule
-
-typerule SQRT ::CVC4::theory::arith::RealOperatorTypeRule
+typerule INTS_DIVISION_TOTAL "SimpleTypeRule<RInteger, AInteger, AInteger>"
+typerule INTS_MODULUS_TOTAL "SimpleTypeRule<RInteger, AInteger, AInteger>"
+
+typerule EXPONENTIAL "SimpleTypeRule<RReal, AReal>"
+typerule SINE "SimpleTypeRule<RReal, AReal>"
+typerule COSINE "SimpleTypeRule<RReal, AReal>"
+typerule TANGENT "SimpleTypeRule<RReal, AReal>"
+typerule COSECANT "SimpleTypeRule<RReal, AReal>"
+typerule SECANT "SimpleTypeRule<RReal, AReal>"
+typerule COTANGENT "SimpleTypeRule<RReal, AReal>"
+typerule ARCSINE "SimpleTypeRule<RReal, AReal>"
+typerule ARCCOSINE "SimpleTypeRule<RReal, AReal>"
+typerule ARCTANGENT "SimpleTypeRule<RReal, AReal>"
+typerule ARCCOSECANT "SimpleTypeRule<RReal, AReal>"
+typerule ARCSECANT "SimpleTypeRule<RReal, AReal>"
+typerule ARCCOTANGENT "SimpleTypeRule<RReal, AReal>"
+
+typerule SQRT "SimpleTypeRule<RReal, AReal>"
 
 nullaryoperator PI "pi"
 
diff --git a/src/theory/arith/theory_arith_type_rules.h b/src/theory/arith/theory_arith_type_rules.h
index c32b612e2..8b587c0fb 100644
--- a/src/theory/arith/theory_arith_type_rules.h
+++ b/src/theory/arith/theory_arith_type_rules.h
@@ -73,88 +73,6 @@ public:
   }
 };/* class ArithOperatorTypeRule */
 
-class IntOperatorTypeRule {
-public:
-  inline static TypeNode computeType(NodeManager* nodeManager, TNode n, bool check)
-  {
-    TNode::iterator child_it = n.begin();
-    TNode::iterator child_it_end = n.end();
-    if(check) {
-      for(; child_it != child_it_end; ++child_it) {
-        TypeNode childType = (*child_it).getType(check);
-        if (!childType.isInteger()) {
-          throw TypeCheckingExceptionPrivate(n, "expecting an integer subterm");
-        }
-      }
-    }
-    return nodeManager->integerType();
-  }
-};/* class IntOperatorTypeRule */
-
-class RealOperatorTypeRule {
-public:
-  inline static TypeNode computeType(NodeManager* nodeManager, TNode n, bool check)
-  {
-    TNode::iterator child_it = n.begin();
-    TNode::iterator child_it_end = n.end();
-    if(check) {
-      for(; child_it != child_it_end; ++child_it) {
-        TypeNode childType = (*child_it).getType(check);
-        if (!childType.isReal()) {
-          throw TypeCheckingExceptionPrivate(n, "expecting a real subterm");
-        }
-      }
-    }
-    return nodeManager->realType();
-  }
-};/* class RealOperatorTypeRule */
-
-class ArithPredicateTypeRule {
-public:
-  inline static TypeNode computeType(NodeManager* nodeManager, TNode n, bool check)
-  {
-    if( check ) {
-      TypeNode lhsType = n[0].getType(check);
-      if (!lhsType.isReal()) {
-        throw TypeCheckingExceptionPrivate(n, "expecting an arithmetic term on the left-hand-side");
-      }
-      TypeNode rhsType = n[1].getType(check);
-      if (!rhsType.isReal()) {
-        throw TypeCheckingExceptionPrivate(n, "expecting an arithmetic term on the right-hand-side");
-      }
-    }
-    return nodeManager->booleanType();
-  }
-};/* class ArithPredicateTypeRule */
-
-class ArithUnaryPredicateTypeRule {
-public:
-  inline static TypeNode computeType(NodeManager* nodeManager, TNode n, bool check)
-  {
-    if( check ) {
-      TypeNode t = n[0].getType(check);
-      if (!t.isReal()) {
-        throw TypeCheckingExceptionPrivate(n, "expecting an arithmetic term");
-      }
-    }
-    return nodeManager->booleanType();
-  }
-};/* class ArithUnaryPredicateTypeRule */
-
-class IntUnaryPredicateTypeRule {
-public:
-  inline static TypeNode computeType(NodeManager* nodeManager, TNode n, bool check)
-  {
-    if( check ) {
-      TypeNode t = n[0].getType(check);
-      if (!t.isInteger()) {
-        throw TypeCheckingExceptionPrivate(n, "expecting an integer term");
-      }
-    }
-    return nodeManager->booleanType();
-  }
-};/* class IntUnaryPredicateTypeRule */
-
 class RealNullaryOperatorTypeRule {
 public:
   inline static TypeNode computeType(NodeManager* nodeManager, TNode n, bool check)
@@ -169,18 +87,6 @@ public:
   }
 };/* class RealNullaryOperatorTypeRule */
 
-class DivisibleOpTypeRule
-{
- public:
-  inline static TypeNode computeType(NodeManager* nodeManager,
-                                     TNode n,
-                                     bool check)
-  {
-    Assert(n.getKind() == kind::DIVISIBLE_OP);
-    return nodeManager->builtinOperatorType();
-  }
-}; /* class DivisibleOpTypeRule */
-
 }/* CVC4::theory::arith namespace */
 }/* CVC4::theory namespace */
 }/* CVC4 namespace */
diff --git a/src/theory/bv/kinds b/src/theory/bv/kinds
index fe451603b..f9caf119a 100644
--- a/src/theory/bv/kinds
+++ b/src/theory/bv/kinds
@@ -222,19 +222,19 @@ typerule BITVECTOR_EAGER_ATOM ::CVC4::theory::bv::BitVectorEagerAtomTypeRule
 
 ### type rules for parameterized operator kinds -------------------------------
 
-typerule BITVECTOR_BITOF_OP ::CVC4::theory::bv::BitVectorBitOfOpTypeRule
+typerule BITVECTOR_BITOF_OP "SimpleTypeRule<RBuiltinOperator>"
 typerule BITVECTOR_BITOF ::CVC4::theory::bv::BitVectorBitOfTypeRule
-typerule BITVECTOR_EXTRACT_OP ::CVC4::theory::bv::BitVectorExtractOpTypeRule
+typerule BITVECTOR_EXTRACT_OP "SimpleTypeRule<RBuiltinOperator>"
 typerule BITVECTOR_EXTRACT ::CVC4::theory::bv::BitVectorExtractTypeRule
-typerule BITVECTOR_REPEAT_OP ::CVC4::theory::bv::BitVectorRepeatOpTypeRule
+typerule BITVECTOR_REPEAT_OP "SimpleTypeRule<RBuiltinOperator>"
 typerule BITVECTOR_REPEAT ::CVC4::theory::bv::BitVectorRepeatTypeRule
-typerule BITVECTOR_ROTATE_LEFT_OP ::CVC4::theory::bv::BitVectorRotateLeftOpTypeRule
+typerule BITVECTOR_ROTATE_LEFT_OP "SimpleTypeRule<RBuiltinOperator>"
 typerule BITVECTOR_ROTATE_LEFT ::CVC4::theory::bv::BitVectorFixedWidthTypeRule
-typerule BITVECTOR_ROTATE_RIGHT_OP ::CVC4::theory::bv::BitVectorRotateRightOpTypeRule
+typerule BITVECTOR_ROTATE_RIGHT_OP "SimpleTypeRule<RBuiltinOperator>"
 typerule BITVECTOR_ROTATE_RIGHT ::CVC4::theory::bv::BitVectorFixedWidthTypeRule
-typerule BITVECTOR_SIGN_EXTEND_OP ::CVC4::theory::bv::BitVectorSignExtendOpTypeRule
+typerule BITVECTOR_SIGN_EXTEND_OP "SimpleTypeRule<RBuiltinOperator>"
 typerule BITVECTOR_SIGN_EXTEND ::CVC4::theory::bv::BitVectorExtendTypeRule
-typerule BITVECTOR_ZERO_EXTEND_OP ::CVC4::theory::bv::BitVectorZeroExtendOpTypeRule
+typerule BITVECTOR_ZERO_EXTEND_OP "SimpleTypeRule<RBuiltinOperator>"
 typerule BITVECTOR_ZERO_EXTEND ::CVC4::theory::bv::BitVectorExtendTypeRule
 typerule INT_TO_BITVECTOR_OP ::CVC4::theory::bv::IntToBitVectorOpTypeRule
 typerule INT_TO_BITVECTOR ::CVC4::theory::bv::BitVectorConversionTypeRule
diff --git a/src/theory/bv/theory_bv_type_rules.h b/src/theory/bv/theory_bv_type_rules.h
index 64d04a37e..e56f752af 100644
--- a/src/theory/bv/theory_bv_type_rules.h
+++ b/src/theory/bv/theory_bv_type_rules.h
@@ -224,18 +224,6 @@ class BitVectorITETypeRule
 /* parameterized operator kinds                                               */
 /* -------------------------------------------------------------------------- */
 
-class BitVectorBitOfOpTypeRule
-{
- public:
-  inline static TypeNode computeType(NodeManager* nodeManager,
-                                     TNode n,
-                                     bool check)
-  {
-    Assert(n.getKind() == kind::BITVECTOR_BITOF_OP);
-    return nodeManager->builtinOperatorType();
-  }
-}; /* class BitVectorBitOfOpTypeRule */
-
 class BitVectorBitOfTypeRule
 {
  public:
@@ -262,18 +250,6 @@ class BitVectorBitOfTypeRule
   }
 }; /* class BitVectorBitOfTypeRule */
 
-class BitVectorExtractOpTypeRule
-{
- public:
-  inline static TypeNode computeType(NodeManager* nodeManager,
-                                     TNode n,
-                                     bool check)
-  {
-    Assert(n.getKind() == kind::BITVECTOR_EXTRACT_OP);
-    return nodeManager->builtinOperatorType();
-  }
-}; /* class BitVectorExtractOpTypeRule */
-
 class BitVectorExtractTypeRule
 {
  public:
@@ -309,18 +285,6 @@ class BitVectorExtractTypeRule
   }
 }; /* class BitVectorExtractTypeRule */
 
-class BitVectorRepeatOpTypeRule
-{
- public:
-  inline static TypeNode computeType(NodeManager* nodeManager,
-                                     TNode n,
-                                     bool check)
-  {
-    Assert(n.getKind() == kind::BITVECTOR_REPEAT_OP);
-    return nodeManager->builtinOperatorType();
-  }
-}; /* class BitVectorRepeatOpTypeRule */
-
 class BitVectorRepeatTypeRule
 {
  public:
@@ -341,54 +305,6 @@ class BitVectorRepeatTypeRule
   }
 }; /* class BitVectorRepeatTypeRule */
 
-class BitVectorRotateLeftOpTypeRule
-{
- public:
-  inline static TypeNode computeType(NodeManager* nodeManager,
-                                     TNode n,
-                                     bool check)
-  {
-    Assert(n.getKind() == kind::BITVECTOR_ROTATE_LEFT_OP);
-    return nodeManager->builtinOperatorType();
-  }
-}; /* class BitVectorRotateLeftOpTypeRule */
-
-class BitVectorRotateRightOpTypeRule
-{
- public:
-  inline static TypeNode computeType(NodeManager* nodeManager,
-                                     TNode n,
-                                     bool check)
-  {
-    Assert(n.getKind() == kind::BITVECTOR_ROTATE_RIGHT_OP);
-    return nodeManager->builtinOperatorType();
-  }
-}; /* class BitVectorRotateRightOpTypeRule */
-
-class BitVectorSignExtendOpTypeRule
-{
- public:
-  inline static TypeNode computeType(NodeManager* nodeManager,
-                                     TNode n,
-                                     bool check)
-  {
-    Assert(n.getKind() == kind::BITVECTOR_SIGN_EXTEND_OP);
-    return nodeManager->builtinOperatorType();
-  }
-}; /* class BitVectorSignExtendOpTypeRule */
-
-class BitVectorZeroExtendOpTypeRule
-{
- public:
-  inline static TypeNode computeType(NodeManager* nodeManager,
-                                     TNode n,
-                                     bool check)
-  {
-    Assert(n.getKind() == kind::BITVECTOR_ZERO_EXTEND_OP);
-    return nodeManager->builtinOperatorType();
-  }
-}; /* class BitVectorZeroExtendOpTypeRule */
-
 class BitVectorExtendTypeRule
 {
  public:
diff --git a/src/theory/datatypes/datatypes_rewriter.cpp b/src/theory/datatypes/datatypes_rewriter.cpp
index ac3bff21b..802dedcbd 100644
--- a/src/theory/datatypes/datatypes_rewriter.cpp
+++ b/src/theory/datatypes/datatypes_rewriter.cpp
@@ -148,6 +148,96 @@ RewriteResponse DatatypesRewriter::postRewrite(TNode in)
       return RewriteResponse(REWRITE_AGAIN_FULL, ret);
     }
   }
+  else if (k == MATCH)
+  {
+    Trace("dt-rewrite-match") << "Rewrite match: " << in << std::endl;
+    Node h = in[0];
+    std::vector<Node> cases;
+    std::vector<Node> rets;
+    TypeNode t = h.getType();
+    const Datatype& dt = t.getDatatype();
+    for (size_t k = 1, nchild = in.getNumChildren(); k < nchild; k++)
+    {
+      Node c = in[k];
+      Node cons;
+      Kind ck = c.getKind();
+      if (ck == MATCH_CASE)
+      {
+        Assert(c[0].getKind() == APPLY_CONSTRUCTOR);
+        cons = c[0].getOperator();
+      }
+      else if (ck == MATCH_BIND_CASE)
+      {
+        if (c[1].getKind() == APPLY_CONSTRUCTOR)
+        {
+          cons = c[1].getOperator();
+        }
+      }
+      else
+      {
+        AlwaysAssert(false);
+      }
+      size_t cindex = 0;
+      // cons is null in the default case
+      if (!cons.isNull())
+      {
+        cindex = Datatype::indexOf(cons.toExpr());
+      }
+      Node body;
+      if (ck == MATCH_CASE)
+      {
+        body = c[1];
+      }
+      else if (ck == MATCH_BIND_CASE)
+      {
+        std::vector<Node> vars;
+        std::vector<Node> subs;
+        if (cons.isNull())
+        {
+          Assert(c[1].getKind() == BOUND_VARIABLE);
+          vars.push_back(c[1]);
+          subs.push_back(h);
+        }
+        else
+        {
+          for (size_t i = 0, vsize = c[0].getNumChildren(); i < vsize; i++)
+          {
+            vars.push_back(c[0][i]);
+            Node sc = nm->mkNode(
+                APPLY_SELECTOR_TOTAL,
+                Node::fromExpr(dt[cindex].getSelectorInternal(t.toType(), i)),
+                h);
+            subs.push_back(sc);
+          }
+        }
+        body =
+            c[2].substitute(vars.begin(), vars.end(), subs.begin(), subs.end());
+      }
+      if (!cons.isNull())
+      {
+        cases.push_back(mkTester(h, cindex, dt));
+      }
+      else
+      {
+        // variables have no constraints
+        cases.push_back(nm->mkConst(true));
+      }
+      rets.push_back(body);
+    }
+    Assert(!cases.empty());
+    // now make the ITE
+    std::reverse(cases.begin(), cases.end());
+    std::reverse(rets.begin(), rets.end());
+    Node ret = rets[0];
+    AlwaysAssert(cases[0].isConst() || cases.size() == dt.getNumConstructors());
+    for (unsigned i = 1, ncases = cases.size(); i < ncases; i++)
+    {
+      ret = nm->mkNode(ITE, cases[i], rets[i], ret);
+    }
+    Trace("dt-rewrite-match")
+        << "Rewrite match: " << in << " ... " << ret << std::endl;
+    return RewriteResponse(REWRITE_AGAIN_FULL, ret);
+  }
 
   if (k == kind::EQUAL)
   {
diff --git a/src/theory/datatypes/kinds b/src/theory/datatypes/kinds
index a0b00bcb0..22d13da0c 100644
--- a/src/theory/datatypes/kinds
+++ b/src/theory/datatypes/kinds
@@ -119,4 +119,23 @@ typerule DT_SYGUS_BOUND ::CVC4::theory::datatypes::DtSygusBoundTypeRule
 operator DT_SYGUS_EVAL 1: "datatypes sygus evaluation function"
 typerule DT_SYGUS_EVAL ::CVC4::theory::datatypes::DtSyguEvalTypeRule
 
+
+# Kinds for match terms. For example, the match term
+#   (match l (((cons h t) h) (nil 0))) 
+# is represented by the AST
+#   (MATCH l 
+#      (MATCH_BIND_CASE (BOUND_VAR_LIST h t) (cons h t) h)
+#      (MATCH_CASE nil 0)
+#   )
+# where notice that patterns with free variables use MATCH_BIND_CASE whereas
+# patterns with no free variables use MATCH_CASE.
+
+operator MATCH 2: "match construct"
+operator MATCH_CASE 2 "a match case"
+operator MATCH_BIND_CASE 3 "a match case with bound variables"
+
+typerule MATCH ::CVC4::theory::datatypes::MatchTypeRule
+typerule MATCH_CASE ::CVC4::theory::datatypes::MatchCaseTypeRule
+typerule MATCH_BIND_CASE ::CVC4::theory::datatypes::MatchBindCaseTypeRule
+
 endtheory
diff --git a/src/theory/datatypes/theory_datatypes_type_rules.h b/src/theory/datatypes/theory_datatypes_type_rules.h
index 22ac074f0..c8c16f368 100644
--- a/src/theory/datatypes/theory_datatypes_type_rules.h
+++ b/src/theory/datatypes/theory_datatypes_type_rules.h
@@ -427,7 +427,165 @@ class DtSyguEvalTypeRule
     }
     return TypeNode::fromType(dt.getSygusType());
   }
-}; /* class DtSygusBoundTypeRule */
+}; /* class DtSyguEvalTypeRule */
+
+class MatchTypeRule
+{
+ public:
+  static TypeNode computeType(NodeManager* nodeManager, TNode n, bool check)
+  {
+    Assert(n.getKind() == kind::MATCH);
+
+    TypeNode retType;
+
+    TypeNode headType = n[0].getType(check);
+    if (!headType.isDatatype())
+    {
+      throw TypeCheckingExceptionPrivate(n, "expecting datatype head in match");
+    }
+    const Datatype& hdt = headType.getDatatype();
+
+    std::unordered_set<unsigned> patIndices;
+    bool patHasVariable = false;
+    // the type of a match case list is the least common type of its cases
+    for (unsigned i = 1, nchildren = n.getNumChildren(); i < nchildren; i++)
+    {
+      Node nc = n[i];
+      if (check)
+      {
+        Kind nck = nc.getKind();
+        std::unordered_set<Node, NodeHashFunction> bvs;
+        if (nck == kind::MATCH_BIND_CASE)
+        {
+          for (const Node& v : nc[0])
+          {
+            Assert(v.getKind() == kind::BOUND_VARIABLE);
+            bvs.insert(v);
+          }
+        }
+        else if (nck != kind::MATCH_CASE)
+        {
+          throw TypeCheckingExceptionPrivate(
+              n, "expected a match case in match expression");
+        }
+        // get the pattern type
+        unsigned pindex = nck == kind::MATCH_CASE ? 0 : 1;
+        TypeNode patType = nc[pindex].getType();
+        // should be caught in the above call
+        if (!patType.isDatatype())
+        {
+          throw TypeCheckingExceptionPrivate(
+              n, "expecting datatype pattern in match");
+        }
+        Kind ncpk = nc[pindex].getKind();
+        if (ncpk == kind::APPLY_CONSTRUCTOR)
+        {
+          for (const Node& arg : nc[pindex])
+          {
+            if (bvs.find(arg) == bvs.end())
+            {
+              throw TypeCheckingExceptionPrivate(
+                  n,
+                  "expecting distinct bound variable as argument to "
+                  "constructor in pattern of match");
+            }
+            bvs.erase(arg);
+          }
+          unsigned ci = Datatype::indexOf(nc[pindex].getOperator().toExpr());
+          patIndices.insert(ci);
+        }
+        else if (ncpk == kind::BOUND_VARIABLE)
+        {
+          patHasVariable = true;
+        }
+        else
+        {
+          throw TypeCheckingExceptionPrivate(
+              n, "unexpected kind of term in pattern in match");
+        }
+        const Datatype& pdt = patType.getDatatype();
+        // compare datatypes instead of the types to catch parametric case,
+        // where the pattern has parametric type.
+        if (hdt != pdt)
+        {
+          std::stringstream ss;
+          ss << "pattern of a match case does not match the head type in match";
+          throw TypeCheckingExceptionPrivate(n, ss.str());
+        }
+      }
+      TypeNode currType = nc.getType(check);
+      if (i == 1)
+      {
+        retType = currType;
+      }
+      else
+      {
+        retType = TypeNode::leastCommonTypeNode(retType, currType);
+        if (retType.isNull())
+        {
+          throw TypeCheckingExceptionPrivate(
+              n, "incomparable types in match case list");
+        }
+      }
+    }
+    if (check)
+    {
+      if (!patHasVariable && patIndices.size() < hdt.getNumConstructors())
+      {
+        throw TypeCheckingExceptionPrivate(
+            n, "cases for match term are not exhaustive");
+      }
+    }
+    return retType;
+  }
+}; /* class MatchTypeRule */
+
+class MatchCaseTypeRule
+{
+ public:
+  inline static TypeNode computeType(NodeManager* nodeManager,
+                                     TNode n,
+                                     bool check)
+  {
+    Assert(n.getKind() == kind::MATCH_CASE);
+    if (check)
+    {
+      TypeNode patType = n[0].getType(check);
+      if (!patType.isDatatype())
+      {
+        throw TypeCheckingExceptionPrivate(
+            n, "expecting datatype pattern in match case");
+      }
+    }
+    return n[1].getType(check);
+  }
+}; /* class MatchCaseTypeRule */
+
+class MatchBindCaseTypeRule
+{
+ public:
+  inline static TypeNode computeType(NodeManager* nodeManager,
+                                     TNode n,
+                                     bool check)
+  {
+    Assert(n.getKind() == kind::MATCH_BIND_CASE);
+    if (check)
+    {
+      if (n[0].getKind() != kind::BOUND_VAR_LIST)
+      {
+        throw TypeCheckingExceptionPrivate(
+            n, "expected a bound variable list in match bind case");
+      }
+      TypeNode patType = n[1].getType(check);
+      if (!patType.isDatatype())
+      {
+        throw TypeCheckingExceptionPrivate(
+            n, "expecting datatype pattern in match bind case");
+      }
+    }
+    return n[2].getType(check);
+  }
+}; /* class MatchBindCaseTypeRule */
 
 } /* CVC4::theory::datatypes namespace */
 } /* CVC4::theory namespace */
diff --git a/src/theory/quantifiers/single_inv_partition.cpp b/src/theory/quantifiers/single_inv_partition.cpp
index 2bb05ad1b..c713ec1dd 100644
--- a/src/theory/quantifiers/single_inv_partition.cpp
+++ b/src/theory/quantifiers/single_inv_partition.cpp
@@ -371,6 +371,7 @@ bool SingleInvocationPartition::init(std::vector<Node>& funcs,
   else
   {
     Trace("si-prt") << "...failed." << std::endl;
+    return false;
   }
   return true;
 }
diff --git a/src/theory/strings/kinds b/src/theory/strings/kinds
index 715ea8f50..4e90d1583 100644
--- a/src/theory/strings/kinds
+++ b/src/theory/strings/kinds
@@ -55,7 +55,7 @@ constant CONST_STRING \
     "util/regexp.h" \
     "a string of characters"
 
-typerule CONST_STRING ::CVC4::theory::strings::StringConstantTypeRule
+typerule CONST_STRING "SimpleTypeRule<RString>"
 
 # equal equal / less than / output
 operator STRING_TO_REGEXP 1 "convert string to regexp"
@@ -73,41 +73,41 @@ operator REGEXP_SIGMA 0 "regexp all characters"
 
 #internal
 operator REGEXP_RV 1 "regexp rv (internal use only)"
-typerule REGEXP_RV ::CVC4::theory::strings::RegExpRVTypeRule
+typerule REGEXP_RV "SimpleTypeRule<RRegExp, AInteger>"
 
 #typerules
-typerule REGEXP_CONCAT ::CVC4::theory::strings::RegExpConcatTypeRule
-typerule REGEXP_UNION ::CVC4::theory::strings::RegExpUnionTypeRule
-typerule REGEXP_INTER ::CVC4::theory::strings::RegExpInterTypeRule
-typerule REGEXP_STAR ::CVC4::theory::strings::RegExpStarTypeRule
-typerule REGEXP_PLUS ::CVC4::theory::strings::RegExpPlusTypeRule
-typerule REGEXP_OPT ::CVC4::theory::strings::RegExpOptTypeRule
+typerule REGEXP_CONCAT "SimpleTypeRuleVar<RRegExp, ARegExp>"
+typerule REGEXP_UNION "SimpleTypeRuleVar<RRegExp, ARegExp>"
+typerule REGEXP_INTER "SimpleTypeRuleVar<RRegExp, ARegExp>"
+typerule REGEXP_STAR "SimpleTypeRule<RRegExp, ARegExp>"
+typerule REGEXP_PLUS "SimpleTypeRule<RRegExp, ARegExp>"
+typerule REGEXP_OPT "SimpleTypeRule<RRegExp, ARegExp>"
 typerule REGEXP_RANGE ::CVC4::theory::strings::RegExpRangeTypeRule
-typerule REGEXP_LOOP ::CVC4::theory::strings::RegExpLoopTypeRule
-
-typerule STRING_TO_REGEXP ::CVC4::theory::strings::StringToRegExpTypeRule
-
-typerule STRING_CONCAT ::CVC4::theory::strings::StringConcatTypeRule
-typerule STRING_LENGTH ::CVC4::theory::strings::StringLengthTypeRule
-typerule STRING_SUBSTR ::CVC4::theory::strings::StringSubstrTypeRule
-typerule STRING_CHARAT ::CVC4::theory::strings::StringCharAtTypeRule
-typerule STRING_STRCTN ::CVC4::theory::strings::StringRelationTypeRule
-typerule STRING_LT ::CVC4::theory::strings::StringRelationTypeRule
-typerule STRING_LEQ ::CVC4::theory::strings::StringRelationTypeRule
-typerule STRING_STRIDOF ::CVC4::theory::strings::StringIndexOfTypeRule
-typerule STRING_STRREPL ::CVC4::theory::strings::StringReplaceTypeRule
-typerule STRING_STRREPLALL ::CVC4::theory::strings::StringReplaceTypeRule
-typerule STRING_PREFIX ::CVC4::theory::strings::StringPrefixOfTypeRule
-typerule STRING_SUFFIX ::CVC4::theory::strings::StringSuffixOfTypeRule
-typerule STRING_ITOS ::CVC4::theory::strings::StringIntToStrTypeRule
-typerule STRING_STOI ::CVC4::theory::strings::StringStrToIntTypeRule
-typerule STRING_CODE ::CVC4::theory::strings::StringStrToIntTypeRule
-typerule STRING_TOUPPER ::CVC4::theory::strings::StringStrToStrTypeRule
-typerule STRING_TOLOWER ::CVC4::theory::strings::StringStrToStrTypeRule
-
-typerule STRING_IN_REGEXP ::CVC4::theory::strings::StringInRegExpTypeRule
-
-typerule REGEXP_EMPTY ::CVC4::theory::strings::EmptyRegExpTypeRule
-typerule REGEXP_SIGMA ::CVC4::theory::strings::SigmaRegExpTypeRule
+typerule REGEXP_LOOP "SimpleTypeRule<RRegExp, ARegExp, AInteger, AOptional<AInteger>>"
+
+typerule STRING_TO_REGEXP "SimpleTypeRule<RRegExp, AString>"
+
+typerule STRING_CONCAT "SimpleTypeRuleVar<RString, AString>"
+typerule STRING_LENGTH "SimpleTypeRule<RInteger, AString>"
+typerule STRING_SUBSTR "SimpleTypeRule<RString, AString, AInteger, AInteger>"
+typerule STRING_CHARAT "SimpleTypeRule<RString, AString, AInteger>"
+typerule STRING_STRCTN "SimpleTypeRule<RBool, AString, AString>"
+typerule STRING_LT "SimpleTypeRule<RBool, AString, AString>"
+typerule STRING_LEQ "SimpleTypeRule<RBool, AString, AString>"
+typerule STRING_STRIDOF "SimpleTypeRule<RInteger, AString, AString, AInteger>"
+typerule STRING_STRREPL "SimpleTypeRule<RString, AString, AString, AString>"
+typerule STRING_STRREPLALL "SimpleTypeRule<RString, AString, AString, AString>"
+typerule STRING_PREFIX "SimpleTypeRule<RBool, AString, AString>"
+typerule STRING_SUFFIX "SimpleTypeRule<RBool, AString, AString>"
+typerule STRING_ITOS "SimpleTypeRule<RString, AInteger>"
+typerule STRING_STOI "SimpleTypeRule<RInteger, AString>"
+typerule STRING_CODE "SimpleTypeRule<RInteger, AString>"
+typerule STRING_TOUPPER "SimpleTypeRule<RString, AString>"
+typerule STRING_TOLOWER "SimpleTypeRule<RString, AString>"
+
+typerule STRING_IN_REGEXP "SimpleTypeRule<RBool, AString, ARegExp>"
+
+typerule REGEXP_EMPTY "SimpleTypeRule<RRegExp>"
+typerule REGEXP_SIGMA "SimpleTypeRule<RRegExp>"
 
 endtheory
diff --git a/src/theory/strings/theory_strings_type_rules.h b/src/theory/strings/theory_strings_type_rules.h
index de77315fc..497366f40 100644
--- a/src/theory/strings/theory_strings_type_rules.h
+++ b/src/theory/strings/theory_strings_type_rules.h
@@ -9,9 +9,9 @@
  ** All rights reserved.  See the file COPYING in the top-level source
  ** directory for licensing information.\endverbatim
  **
- ** \brief Typing and cardinality rules for the theory of arrays
+ ** \brief Typing rules for the theory of strings and regexps
  **
- ** Typing and cardinality rules for the theory of arrays.
+ ** Typing rules for the theory of strings and regexps
  **/
 
 #include "cvc4_private.h"
@@ -24,344 +24,6 @@ namespace CVC4 {
 namespace theory {
 namespace strings {
 
-class StringConstantTypeRule {
-public:
-  inline static TypeNode computeType(NodeManager* nodeManager, TNode n, bool check)
-  {
-    return nodeManager->stringType();
-  }
-};
-
-class StringConcatTypeRule {
-public:
-  inline static TypeNode computeType(NodeManager* nodeManager, TNode n, bool check)
-  {
-    if( check ){
-      TNode::iterator it = n.begin();
-      TNode::iterator it_end = n.end();
-      int size = 0;
-      for (; it != it_end; ++ it) {
-       TypeNode t = (*it).getType(check);
-       if (!t.isString()) {
-         throw TypeCheckingExceptionPrivate(n, "expecting string terms in string concat");
-       }
-       ++size;
-      }
-      if(size < 2) {
-        throw TypeCheckingExceptionPrivate(n, "expecting at least 2 terms in string concat");
-      }
-    }
-    return nodeManager->stringType();
-  }
-};
-
-class StringLengthTypeRule {
-public:
-  inline static TypeNode computeType(NodeManager* nodeManager, TNode n, bool check)
-  {
-    if( check ) {
-      TypeNode t = n[0].getType(check);
-      if (!t.isString()) {
-        throw TypeCheckingExceptionPrivate(n, "expecting string terms in string length");
-      }
-    }
-    return nodeManager->integerType();
-  }
-};
-
-class StringSubstrTypeRule {
-public:
-  inline static TypeNode computeType(NodeManager* nodeManager, TNode n, bool check)
-  {
-    if( check ) {
-      TypeNode t = n[0].getType(check);
-      if (!t.isString()) {
-        throw TypeCheckingExceptionPrivate(n, "expecting a string term in substr");
-      }
-      t = n[1].getType(check);
-      if (!t.isInteger()) {
-        throw TypeCheckingExceptionPrivate(n, "expecting a start int term in substr");
-      }
-      t = n[2].getType(check);
-      if (!t.isInteger()) {
-        throw TypeCheckingExceptionPrivate(n, "expecting a length int term in substr");
-      }
-    }
-    return nodeManager->stringType();
-  }
-};
-
-class StringRelationTypeRule
-{
- public:
-  inline static TypeNode computeType(NodeManager* nodeManager, TNode n, bool check)
-  {
-    if( check ) {
-      TypeNode t = n[0].getType(check);
-      if (!t.isString()) {
-        throw TypeCheckingExceptionPrivate(
-            n, "expecting a string term in string relation");
-      }
-      t = n[1].getType(check);
-      if (!t.isString()) {
-        throw TypeCheckingExceptionPrivate(
-            n, "expecting a string term in string relation");
-      }
-    }
-    return nodeManager->booleanType();
-  }
-};
-
-class StringCharAtTypeRule {
-public:
-  inline static TypeNode computeType(NodeManager* nodeManager, TNode n, bool check)
-  {
-    if( check ) {
-      TypeNode t = n[0].getType(check);
-      if (!t.isString()) {
-        throw TypeCheckingExceptionPrivate(n, "expecting a string term in string char at 0");
-      }
-      t = n[1].getType(check);
-      if (!t.isInteger()) {
-        throw TypeCheckingExceptionPrivate(n, "expecting an integer term in string char at 1");
-      }
-    }
-    return nodeManager->stringType();
-  }
-};
-
-class StringIndexOfTypeRule {
-public:
-  inline static TypeNode computeType(NodeManager* nodeManager, TNode n, bool check)
-  {
-    if( check ) {
-      TypeNode t = n[0].getType(check);
-      if (!t.isString()) {
-        throw TypeCheckingExceptionPrivate(n, "expecting a string term in string indexof 0");
-      }
-      t = n[1].getType(check);
-      if (!t.isString()) {
-        throw TypeCheckingExceptionPrivate(n, "expecting a string term in string indexof 1");
-      }
-      t = n[2].getType(check);
-      if (!t.isInteger()) {
-        throw TypeCheckingExceptionPrivate(n, "expecting an integer term in string indexof 2");
-      }
-    }
-    return nodeManager->integerType();
-  }
-};
-
-class StringReplaceTypeRule {
-public:
-  inline static TypeNode computeType(NodeManager* nodeManager, TNode n, bool check)
-  {
-    if( check ) {
-      TypeNode t = n[0].getType(check);
-      if (!t.isString()) {
-        throw TypeCheckingExceptionPrivate(n, "expecting a string term in string replace 0");
-      }
-      t = n[1].getType(check);
-      if (!t.isString()) {
-        throw TypeCheckingExceptionPrivate(n, "expecting a string term in string replace 1");
-      }
-      t = n[2].getType(check);
-      if (!t.isString()) {
-        throw TypeCheckingExceptionPrivate(n, "expecting a string term in string replace 2");
-      }
-    }
-    return nodeManager->stringType();
-  }
-};
-
-class StringPrefixOfTypeRule {
-public:
-  inline static TypeNode computeType(NodeManager* nodeManager, TNode n, bool check)
-  {
-    if( check ) {
-      TypeNode t = n[0].getType(check);
-      if (!t.isString()) {
-        throw TypeCheckingExceptionPrivate(n, "expecting a string term in string prefixof 0");
-      }
-      t = n[1].getType(check);
-      if (!t.isString()) {
-        throw TypeCheckingExceptionPrivate(n, "expecting a string term in string prefixof 1");
-      }
-    }
-    return nodeManager->booleanType();
-  }
-};
-
-class StringSuffixOfTypeRule {
-public:
-  inline static TypeNode computeType(NodeManager* nodeManager, TNode n, bool check)
-  {
-    if( check ) {
-      TypeNode t = n[0].getType(check);
-      if (!t.isString()) {
-        throw TypeCheckingExceptionPrivate(n, "expecting a string term in string suffixof 0");
-      }
-      t = n[1].getType(check);
-      if (!t.isString()) {
-        throw TypeCheckingExceptionPrivate(n, "expecting a string term in string suffixof 1");
-      }
-    }
-    return nodeManager->booleanType();
-  }
-};
-
-class StringIntToStrTypeRule {
-public:
-  inline static TypeNode computeType(NodeManager* nodeManager, TNode n, bool check)
-  {
-    if( check ) {
-      TypeNode t = n[0].getType(check);
-      if (!t.isInteger()) {
-        throw TypeCheckingExceptionPrivate(n, "expecting an integer term in int to string 0");
-      }
-    }
-    return nodeManager->stringType();
-  }
-};
-
-class StringStrToIntTypeRule {
-public:
-  inline static TypeNode computeType(NodeManager* nodeManager, TNode n, bool check)
-  {
-    if( check ) {
-      TypeNode t = n[0].getType(check);
-      if (!t.isString()) {
-        std::stringstream ss;
-        ss << "expecting a string term in argument of " << n.getKind();
-        throw TypeCheckingExceptionPrivate(n, ss.str());
-      }
-    }
-    return nodeManager->integerType();
-  }
-};
-
-class StringStrToStrTypeRule
-{
- public:
-  inline static TypeNode computeType(NodeManager* nodeManager,
-                                     TNode n,
-                                     bool check)
-  {
-    if (check)
-    {
-      TypeNode t = n[0].getType(check);
-      if (!t.isString())
-      {
-        std::stringstream ss;
-        ss << "expecting a string term in argument of " << n.getKind();
-        throw TypeCheckingExceptionPrivate(n, ss.str());
-      }
-    }
-    return nodeManager->stringType();
-  }
-};
-
-class RegExpConcatTypeRule {
-public:
-  inline static TypeNode computeType(NodeManager* nodeManager, TNode n, bool check)
-  {
-    if( check ) {
-      TNode::iterator it = n.begin();
-      TNode::iterator it_end = n.end();
-      int size = 0;
-      for (; it != it_end; ++ it) {
-         TypeNode t = (*it).getType(check);
-         if (!t.isRegExp()) {
-           throw TypeCheckingExceptionPrivate(n, "expecting regexp terms in regexp concat");
-         }
-         ++size;
-      }
-      if(size < 2) {
-         throw TypeCheckingExceptionPrivate(n, "expecting at least 2 terms in regexp concat");
-      }
-    }
-    return nodeManager->regExpType();
-  }
-};
-
-class RegExpUnionTypeRule {
-public:
-  inline static TypeNode computeType(NodeManager* nodeManager, TNode n, bool check)
-  {
-    if( check ) {
-      TNode::iterator it = n.begin();
-      TNode::iterator it_end = n.end();
-      for (; it != it_end; ++ it) {
-         TypeNode t = (*it).getType(check);
-         if (!t.isRegExp()) {
-           throw TypeCheckingExceptionPrivate(n, "expecting regexp terms");
-         }
-      }
-    }
-    return nodeManager->regExpType();
-  }
-};
-
-class RegExpInterTypeRule {
-public:
-  inline static TypeNode computeType(NodeManager* nodeManager, TNode n, bool check)
-  {
-    if( check ) {
-      TNode::iterator it = n.begin();
-      TNode::iterator it_end = n.end();
-      for (; it != it_end; ++ it) {
-       TypeNode t = (*it).getType(check);
-       if (!t.isRegExp()) {
-         throw TypeCheckingExceptionPrivate(n, "expecting regexp terms");
-       }
-      }
-    }
-    return nodeManager->regExpType();
-  }
-};
-
-class RegExpStarTypeRule {
-public:
-  inline static TypeNode computeType(NodeManager* nodeManager, TNode n, bool check)
-  {
-    if( check ) {
-      TypeNode t = n[0].getType(check);
-      if (!t.isRegExp()) {
-        throw TypeCheckingExceptionPrivate(n, "expecting regexp terms");
-      }
-    }
-    return nodeManager->regExpType();
-  }
-};
-
-class RegExpPlusTypeRule {
-public:
-  inline static TypeNode computeType(NodeManager* nodeManager, TNode n, bool check)
-  {
-    if( check ) {
-      TypeNode t = n[0].getType(check);
-      if (!t.isRegExp()) {
-        throw TypeCheckingExceptionPrivate(n, "expecting regexp terms");
-      }
-    }
-    return nodeManager->regExpType();
-  }
-};
-
-class RegExpOptTypeRule {
-public:
-  inline static TypeNode computeType(NodeManager* nodeManager, TNode n, bool check)
-  {
-    if( check ) {
-      TypeNode t = n[0].getType(check);
-      if (!t.isRegExp()) {
-        throw TypeCheckingExceptionPrivate(n, "expecting regexp terms");
-      }
-    }
-    return nodeManager->regExpType();
-  }
-};
-
 class RegExpRangeTypeRule {
 public:
   inline static TypeNode computeType(NodeManager* nodeManager, TNode n, bool check)
@@ -401,112 +63,6 @@ public:
   }
 };
 
-class RegExpLoopTypeRule {
-public:
-  inline static TypeNode computeType(NodeManager* nodeManager, TNode n, bool check)
-  {
-    if( check ) {
-      TNode::iterator it = n.begin();
-      TNode::iterator it_end = n.end();
-      TypeNode t = (*it).getType(check);
-      if (!t.isRegExp()) {
-        throw TypeCheckingExceptionPrivate(n, "expecting a regexp term in regexp loop 1");
-      }
-      ++it; t = (*it).getType(check);
-      if (!t.isInteger()) {
-        throw TypeCheckingExceptionPrivate(n, "expecting an integer term in regexp loop 2");
-      }
-      //if(!(*it).isConst()) {
-        //throw TypeCheckingExceptionPrivate(n, "expecting an const integer term in regexp loop 2");
-      //}
-      ++it;
-      if(it != it_end) {
-        t = (*it).getType(check);
-        if (!t.isInteger()) {
-          throw TypeCheckingExceptionPrivate(n, "expecting an integer term in regexp loop 3");
-        }
-        //if(!(*it).isConst()) {
-          //throw TypeCheckingExceptionPrivate(n, "expecting an const integer term in regexp loop 3");
-        //}
-        //if(++it != it_end) {
-        //  throw TypeCheckingExceptionPrivate(n, "too many regexp");
-        //}
-      }
-    }
-    return nodeManager->regExpType();
-  }
-};
-
-class StringToRegExpTypeRule {
-public:
-  inline static TypeNode computeType(NodeManager* nodeManager, TNode n, bool check)
-  {
-    if( check ) {
-      TypeNode t = n[0].getType(check);
-      if (!t.isString()) {
-        throw TypeCheckingExceptionPrivate(n, "expecting string terms");
-      }
-      //if( (*it).getKind() != kind::CONST_STRING ) {
-      //  throw TypeCheckingExceptionPrivate(n, "expecting constant string terms");
-      //}
-    }
-    return nodeManager->regExpType();
-  }
-};
-
-class StringInRegExpTypeRule {
-public:
-  inline static TypeNode computeType(NodeManager* nodeManager, TNode n, bool check)
-  {
-    if( check ) {
-      TNode::iterator it = n.begin();
-      TypeNode t = (*it).getType(check);
-      if (!t.isString()) {
-        throw TypeCheckingExceptionPrivate(n, "expecting string terms");
-      }
-      ++it;
-      t = (*it).getType(check);
-      if (!t.isRegExp()) {
-        throw TypeCheckingExceptionPrivate(n, "expecting regexp terms");
-      }
-    }
-    return nodeManager->booleanType();
-  }
-};
-
-class EmptyRegExpTypeRule {
-public:
-  inline static TypeNode computeType(NodeManager* nodeManager, TNode n, bool check)
-  {
-    Assert(n.getKind() == kind::REGEXP_EMPTY);
-    return nodeManager->regExpType();
-  }
-};
-
-class SigmaRegExpTypeRule {
-public:
-  inline static TypeNode computeType(NodeManager* nodeManager, TNode n, bool check)
-  {
-    Assert(n.getKind() == kind::REGEXP_SIGMA);
-    return nodeManager->regExpType();
-  }
-};
-
-class RegExpRVTypeRule {
-public:
-  inline static TypeNode computeType(NodeManager* nodeManager, TNode n, bool check)
-  {
-    if( check ) {
-      TypeNode t = n[0].getType(check);
-      if (!t.isInteger()) {
-        throw TypeCheckingExceptionPrivate(n, "expecting an integer term in RV");
-      }
-    }
-    return nodeManager->regExpType();
-  }
-};
-
-
 }/* CVC4::theory::strings namespace */
 }/* CVC4::theory namespace */
 }/* CVC4 namespace */
diff --git a/test/regress/CMakeLists.txt b/test/regress/CMakeLists.txt
index cdf93384e..b47d22492 100644
--- a/test/regress/CMakeLists.txt
+++ b/test/regress/CMakeLists.txt
@@ -1685,6 +1685,7 @@ set(regress_1_tests
   regress1/sygus/issue3201.smt2
   regress1/sygus/issue3205.smt2
   regress1/sygus/issue3247.smt2
+  regress1/sygus/issue3320-quant.sy
   regress1/sygus/large-const-simp.sy
   regress1/sygus/let-bug-simp.sy
   regress1/sygus/list-head-x.sy
@@ -1697,6 +1698,7 @@ set(regress_1_tests
   regress1/sygus/nia-max-square-ns.sy
   regress1/sygus/no-flat-simp.sy
   regress1/sygus/no-mention.sy
+  regress1/sygus/only-const-grammar.sy
   regress1/sygus/parity-si-rcons.sy
   regress1/sygus/pbe_multi.sy
   regress1/sygus/phone-1-long.sy
diff --git a/test/regress/regress1/datatypes/dt-color-2.6.smt2 b/test/regress/regress1/datatypes/dt-color-2.6.smt2
index f6148994e..f5d8129ae 100644
--- a/test/regress/regress1/datatypes/dt-color-2.6.smt2
+++ b/test/regress/regress1/datatypes/dt-color-2.6.smt2
@@ -11,7 +11,7 @@
 
 (assert (or (distinct a b c d)
  (< (match a ((red 5) (green 3) (blue 2))) 0)
- (< (match b ((red 2) (_ 1))) 0)
+ (< (match b ((red 2) (x 1))) 0)
  ))
 
 (check-sat)
diff --git a/test/regress/regress1/sygus/issue3320-quant.sy b/test/regress/regress1/sygus/issue3320-quant.sy
new file mode 100644
index 000000000..a7b76182e
--- /dev/null
+++ b/test/regress/regress1/sygus/issue3320-quant.sy
@@ -0,0 +1,9 @@
+; EXPECT: unsat
+; COMMAND-LINE: --sygus-out=status
+(set-logic LIA)
+(declare-var x Int)
+(declare-var y Int)
+(synth-fun myfun ((x Int) (y Int)) Bool)
+(constraint (exists ((x Int) (y Int)) (myfun x y)))
+(constraint (exists ((x Int) (y Int)) (not (myfun x y))))
+(check-synth)
diff --git a/test/regress/regress1/sygus/only-const-grammar.sy b/test/regress/regress1/sygus/only-const-grammar.sy
new file mode 100644
index 000000000..25effd154
--- /dev/null
+++ b/test/regress/regress1/sygus/only-const-grammar.sy
@@ -0,0 +1,20 @@
+; EXPECT: unsat
+; COMMAND-LINE: --sygus-out=status --lang=sygus2
+(set-logic LIA)
+
+(synth-fun f ((x Int) (y Int)) Int
+  ((Start Int) (CInt Int))
+  (
+    (Start Int ((+ x CInt)))
+    (CInt Int ((Constant Int)))
+  )
+)
+
+(declare-var x Int)
+(declare-var y Int)
+
+(constraint (= (f 0 0) 2))
+
+(constraint (= (f 1 1) 3))
+
+(check-synth)