Introduce template classes for simple type rules (#2835)

This commit introduces two template classes `SimpleTypeRule` and
`SimpleTypeRuleVar` to help define simple type rules without writing
lots of redundant code. The main advantages of this approach are:

- Less code
- More consistent error reporting
- Easier to extend type checking with other functionality (e.g. getting
the type of a symbol)

2 files changed, 36 insertions, 480 deletions

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 */