Strings: Move implementation of type rules from header to .cpp file. (#6334)

3 files changed, 396 insertions, 316 deletions

diff --git a/src/CMakeLists.txt b/src/CMakeLists.txt
index fabff516f..c33110cc3 100644
--- a/src/CMakeLists.txt
+++ b/src/CMakeLists.txt
@@ -995,6 +995,7 @@ libcvc4_add_sources(
   theory/strings/theory_strings.h
   theory/strings/theory_strings_preprocess.cpp
   theory/strings/theory_strings_preprocess.h
+  theory/strings/theory_strings_type_rules.cpp
   theory/strings/theory_strings_type_rules.h
   theory/strings/theory_strings_utils.cpp
   theory/strings/theory_strings_utils.h
diff --git a/src/theory/strings/theory_strings_type_rules.cpp b/src/theory/strings/theory_strings_type_rules.cpp
new file mode 100644
index 000000000..7f7799b25
--- /dev/null
+++ b/src/theory/strings/theory_strings_type_rules.cpp
@@ -0,0 +1,373 @@
+/******************************************************************************
+ * Top contributors (to current version):
+ *   Andrew Reynolds, Aina Niemetz, Yoni Zohar
+ *
+ * This file is part of the cvc5 project.
+ *
+ * Copyright (c) 2009-2021 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.
+ * ****************************************************************************
+ *
+ * Typing rules for the theory of strings and regexps.
+ */
+#include "theory/strings/theory_strings_type_rules.h"
+
+#include <sstream>
+
+#include "expr/node_manager.h"
+#include "expr/sequence.h"
+#include "options/strings_options.h"
+
+namespace cvc5 {
+namespace theory {
+namespace strings {
+
+TypeNode StringConcatTypeRule::computeType(NodeManager* nodeManager,
+                                           TNode n,
+                                           bool check)
+{
+  TypeNode tret;
+  for (const Node& nc : n)
+  {
+    TypeNode t = nc.getType(check);
+    if (tret.isNull())
+    {
+      tret = t;
+      if (check)
+      {
+        if (!t.isStringLike())
+        {
+          throw TypeCheckingExceptionPrivate(
+              n, "expecting string-like terms in concat");
+        }
+      }
+      else
+      {
+        break;
+      }
+    }
+    else if (t != tret)
+    {
+      throw TypeCheckingExceptionPrivate(
+          n, "expecting all children to have the same type in concat");
+    }
+  }
+  return tret;
+}
+
+TypeNode StringSubstrTypeRule::computeType(NodeManager* nodeManager,
+                                           TNode n,
+                                           bool check)
+{
+  TypeNode t = n[0].getType(check);
+  if (check)
+  {
+    if (!t.isStringLike())
+    {
+      throw TypeCheckingExceptionPrivate(
+          n, "expecting a string-like term in substr");
+    }
+    TypeNode t2 = n[1].getType(check);
+    if (!t2.isInteger())
+    {
+      throw TypeCheckingExceptionPrivate(
+          n, "expecting an integer start term in substr");
+    }
+    t2 = n[2].getType(check);
+    if (!t2.isInteger())
+    {
+      throw TypeCheckingExceptionPrivate(
+          n, "expecting an integer length term in substr");
+    }
+  }
+  return t;
+}
+
+TypeNode StringUpdateTypeRule::computeType(NodeManager* nodeManager,
+                                           TNode n,
+                                           bool check)
+{
+  TypeNode t = n[0].getType(check);
+  if (check)
+  {
+    if (!t.isStringLike())
+    {
+      throw TypeCheckingExceptionPrivate(
+          n, "expecting a string-like term in update");
+    }
+    TypeNode t2 = n[1].getType(check);
+    if (!t2.isInteger())
+    {
+      throw TypeCheckingExceptionPrivate(
+          n, "expecting an integer start term in update");
+    }
+    t2 = n[2].getType(check);
+    if (!t2.isStringLike())
+    {
+      throw TypeCheckingExceptionPrivate(
+          n, "expecting an string-like replace term in update");
+    }
+  }
+  return t;
+}
+
+TypeNode StringAtTypeRule::computeType(NodeManager* nodeManager,
+                                       TNode n,
+                                       bool check)
+{
+  TypeNode t = n[0].getType(check);
+  if (check)
+  {
+    if (!t.isStringLike())
+    {
+      throw TypeCheckingExceptionPrivate(
+          n, "expecting a string-like term in str.at");
+    }
+    TypeNode t2 = n[1].getType(check);
+    if (!t2.isInteger())
+    {
+      throw TypeCheckingExceptionPrivate(
+          n, "expecting an integer start term in str.at");
+    }
+  }
+  return t;
+}
+
+TypeNode StringIndexOfTypeRule::computeType(NodeManager* nodeManager,
+                                            TNode n,
+                                            bool check)
+{
+  if (check)
+  {
+    TypeNode t = n[0].getType(check);
+    if (!t.isStringLike())
+    {
+      throw TypeCheckingExceptionPrivate(
+          n, "expecting a string-like term in indexof");
+    }
+    TypeNode t2 = n[1].getType(check);
+    if (t != t2)
+    {
+      throw TypeCheckingExceptionPrivate(
+          n,
+          "expecting a term in second argument of indexof that is the same "
+          "type as the first argument");
+    }
+    t = n[2].getType(check);
+    if (!t.isInteger())
+    {
+      throw TypeCheckingExceptionPrivate(
+          n, "expecting an integer term in third argument of indexof");
+    }
+  }
+  return nodeManager->integerType();
+}
+
+TypeNode StringReplaceTypeRule::computeType(NodeManager* nodeManager,
+                                            TNode n,
+                                            bool check)
+{
+  TypeNode t = n[0].getType(check);
+  if (check)
+  {
+    if (!t.isStringLike())
+    {
+      throw TypeCheckingExceptionPrivate(
+          n, "expecting a string-like term in replace");
+    }
+    TypeNode t2 = n[1].getType(check);
+    if (t != t2)
+    {
+      throw TypeCheckingExceptionPrivate(
+          n,
+          "expecting a term in second argument of replace that is the same "
+          "type as the first argument");
+    }
+    t2 = n[2].getType(check);
+    if (t != t2)
+    {
+      throw TypeCheckingExceptionPrivate(
+          n,
+          "expecting a term in third argument of replace that is the same "
+          "type as the first argument");
+    }
+  }
+  return t;
+}
+
+TypeNode StringStrToBoolTypeRule::computeType(NodeManager* nodeManager,
+                                              TNode n,
+                                              bool check)
+{
+  if (check)
+  {
+    TypeNode t = n[0].getType(check);
+    if (!t.isStringLike())
+    {
+      std::stringstream ss;
+      ss << "expecting a string-like term in argument of " << n.getKind();
+      throw TypeCheckingExceptionPrivate(n, ss.str());
+    }
+  }
+  return nodeManager->booleanType();
+}
+
+TypeNode StringStrToIntTypeRule::computeType(NodeManager* nodeManager,
+                                             TNode n,
+                                             bool check)
+{
+  if (check)
+  {
+    TypeNode t = n[0].getType(check);
+    if (!t.isStringLike())
+    {
+      std::stringstream ss;
+      ss << "expecting a string-like term in argument of " << n.getKind();
+      throw TypeCheckingExceptionPrivate(n, ss.str());
+    }
+  }
+  return nodeManager->integerType();
+}
+
+TypeNode StringStrToStrTypeRule::computeType(NodeManager* nodeManager,
+                                             TNode n,
+                                             bool check)
+{
+  TypeNode t = n[0].getType(check);
+  if (check)
+  {
+    if (!t.isStringLike())
+    {
+      std::stringstream ss;
+      ss << "expecting a string term in argument of " << n.getKind();
+      throw TypeCheckingExceptionPrivate(n, ss.str());
+    }
+  }
+  return t;
+}
+
+TypeNode StringRelationTypeRule::computeType(NodeManager* nodeManager,
+                                             TNode n,
+                                             bool check)
+{
+  if (check)
+  {
+    TypeNode t = n[0].getType(check);
+    if (!t.isStringLike())
+    {
+      throw TypeCheckingExceptionPrivate(
+          n, "expecting a string-like term in relation");
+    }
+    TypeNode t2 = n[1].getType(check);
+    if (t != t2)
+    {
+      throw TypeCheckingExceptionPrivate(
+          n, "expecting two terms of the same string-like type in relation");
+    }
+  }
+  return nodeManager->booleanType();
+}
+
+TypeNode RegExpRangeTypeRule::computeType(NodeManager* nodeManager,
+                                          TNode n,
+                                          bool check)
+{
+  if (check)
+  {
+    TNode::iterator it = n.begin();
+    unsigned ch[2];
+
+    for (int i = 0; i < 2; ++i)
+    {
+      TypeNode t = (*it).getType(check);
+      if (!t.isString())  // string-only
+      {
+        throw TypeCheckingExceptionPrivate(
+            n, "expecting a string term in regexp range");
+      }
+      if (!(*it).isConst())
+      {
+        throw TypeCheckingExceptionPrivate(
+            n, "expecting a constant string term in regexp range");
+      }
+      if ((*it).getConst<String>().size() != 1)
+      {
+        throw TypeCheckingExceptionPrivate(
+            n, "expecting a single constant string term in regexp range");
+      }
+      unsigned ci = (*it).getConst<String>().front();
+      ch[i] = ci;
+      ++it;
+    }
+    if (ch[0] > ch[1])
+    {
+      throw TypeCheckingExceptionPrivate(
+          n,
+          "expecting the first constant is less or equal to the second one in "
+          "regexp range");
+    }
+  }
+  return nodeManager->regExpType();
+}
+
+TypeNode ConstSequenceTypeRule::computeType(NodeManager* nodeManager,
+                                            TNode n,
+                                            bool check)
+{
+  Assert(n.getKind() == kind::CONST_SEQUENCE);
+  return nodeManager->mkSequenceType(n.getConst<Sequence>().getType());
+}
+
+TypeNode SeqUnitTypeRule::computeType(NodeManager* nodeManager,
+                                      TNode n,
+                                      bool check)
+{
+  return nodeManager->mkSequenceType(n[0].getType(check));
+}
+
+TypeNode SeqNthTypeRule::computeType(NodeManager* nodeManager,
+                                     TNode n,
+                                     bool check)
+{
+  TypeNode t = n[0].getType(check);
+  TypeNode t1 = t.getSequenceElementType();
+  if (check)
+  {
+    if (!t.isSequence())
+    {
+      throw TypeCheckingExceptionPrivate(n, "expecting a sequence in nth");
+    }
+    TypeNode t2 = n[1].getType(check);
+    if (!t2.isInteger())
+    {
+      throw TypeCheckingExceptionPrivate(
+          n, "expecting an integer start term in nth");
+    }
+  }
+  return t1;
+}
+
+Cardinality SequenceProperties::computeCardinality(TypeNode type)
+{
+  Assert(type.getKind() == kind::SEQUENCE_TYPE);
+  return Cardinality::INTEGERS;
+}
+/** A sequence is well-founded if its element type is */
+bool SequenceProperties::isWellFounded(TypeNode type)
+{
+  return type[0].isWellFounded();
+}
+/** Make ground term for sequence type (return the empty sequence) */
+Node SequenceProperties::mkGroundTerm(TypeNode type)
+{
+  Assert(type.isSequence());
+  // empty sequence
+  std::vector<Node> seq;
+  return NodeManager::currentNM()->mkConst(
+      Sequence(type.getSequenceElementType(), seq));
+}
+}  // namespace strings
+}  // namespace theory
+}  // namespace cvc5
diff --git a/src/theory/strings/theory_strings_type_rules.h b/src/theory/strings/theory_strings_type_rules.h
index 93c252942..496599252 100644
--- a/src/theory/strings/theory_strings_type_rules.h
+++ b/src/theory/strings/theory_strings_type_rules.h
@@ -14,405 +14,111 @@
  */
 
 #include "cvc4_private.h"
-#include "options/strings_options.h"
 
 #ifndef CVC5__THEORY__STRINGS__THEORY_STRINGS_TYPE_RULES_H
 #define CVC5__THEORY__STRINGS__THEORY_STRINGS_TYPE_RULES_H
 
-#include "expr/sequence.h"
+#include "expr/node.h"
 
 namespace cvc5 {
+
+class NodeManager;
+class TypeNode;
+
 namespace theory {
 namespace strings {
 
 class StringConcatTypeRule
 {
  public:
-  inline static TypeNode computeType(NodeManager* nodeManager,
-                                     TNode n,
-                                     bool check)
-  {
-    TypeNode tret;
-    for (const Node& nc : n)
-    {
-      TypeNode t = nc.getType(check);
-      if (tret.isNull())
-      {
-        tret = t;
-        if (check)
-        {
-          if (!t.isStringLike())
-          {
-            throw TypeCheckingExceptionPrivate(
-                n, "expecting string-like terms in concat");
-          }
-        }
-        else
-        {
-          break;
-        }
-      }
-      else if (t != tret)
-      {
-        throw TypeCheckingExceptionPrivate(
-            n, "expecting all children to have the same type in concat");
-      }
-    }
-    return tret;
-  }
+  static TypeNode computeType(NodeManager* nodeManager, TNode n, bool check);
 };
 
 class StringSubstrTypeRule
 {
  public:
-  inline static TypeNode computeType(NodeManager* nodeManager,
-                                     TNode n,
-                                     bool check)
-  {
-    TypeNode t = n[0].getType(check);
-    if (check)
-    {
-      if (!t.isStringLike())
-      {
-        throw TypeCheckingExceptionPrivate(
-            n, "expecting a string-like term in substr");
-      }
-      TypeNode t2 = n[1].getType(check);
-      if (!t2.isInteger())
-      {
-        throw TypeCheckingExceptionPrivate(
-            n, "expecting an integer start term in substr");
-      }
-      t2 = n[2].getType(check);
-      if (!t2.isInteger())
-      {
-        throw TypeCheckingExceptionPrivate(
-            n, "expecting an integer length term in substr");
-      }
-    }
-    return t;
-  }
+  static TypeNode computeType(NodeManager* nodeManager, TNode n, bool check);
 };
 
 class StringUpdateTypeRule
 {
  public:
-  inline static TypeNode computeType(NodeManager* nodeManager,
-                                     TNode n,
-                                     bool check)
-  {
-    TypeNode t = n[0].getType(check);
-    if (check)
-    {
-      if (!t.isStringLike())
-      {
-        throw TypeCheckingExceptionPrivate(
-            n, "expecting a string-like term in update");
-      }
-      TypeNode t2 = n[1].getType(check);
-      if (!t2.isInteger())
-      {
-        throw TypeCheckingExceptionPrivate(
-            n, "expecting an integer start term in update");
-      }
-      t2 = n[2].getType(check);
-      if (!t2.isStringLike())
-      {
-        throw TypeCheckingExceptionPrivate(
-            n, "expecting an string-like replace term in update");
-      }
-    }
-    return t;
-  }
+  static TypeNode computeType(NodeManager* nodeManager, TNode n, bool check);
 };
 
 class StringAtTypeRule
 {
  public:
-  inline static TypeNode computeType(NodeManager* nodeManager,
-                                     TNode n,
-                                     bool check)
-  {
-    TypeNode t = n[0].getType(check);
-    if (check)
-    {
-      if (!t.isStringLike())
-      {
-        throw TypeCheckingExceptionPrivate(
-            n, "expecting a string-like term in str.at");
-      }
-      TypeNode t2 = n[1].getType(check);
-      if (!t2.isInteger())
-      {
-        throw TypeCheckingExceptionPrivate(
-            n, "expecting an integer start term in str.at");
-      }
-    }
-    return t;
-  }
+  static TypeNode computeType(NodeManager* nodeManager, TNode n, bool check);
 };
 
 class StringIndexOfTypeRule
 {
  public:
-  inline static TypeNode computeType(NodeManager* nodeManager,
-                                     TNode n,
-                                     bool check)
-  {
-    if (check)
-    {
-      TypeNode t = n[0].getType(check);
-      if (!t.isStringLike())
-      {
-        throw TypeCheckingExceptionPrivate(
-            n, "expecting a string-like term in indexof");
-      }
-      TypeNode t2 = n[1].getType(check);
-      if (t != t2)
-      {
-        throw TypeCheckingExceptionPrivate(
-            n,
-            "expecting a term in second argument of indexof that is the same "
-            "type as the first argument");
-      }
-      t = n[2].getType(check);
-      if (!t.isInteger())
-      {
-        throw TypeCheckingExceptionPrivate(
-            n, "expecting an integer term in third argument of indexof");
-      }
-    }
-    return nodeManager->integerType();
-  }
+  static TypeNode computeType(NodeManager* nodeManager, TNode n, bool check);
 };
 
 class StringReplaceTypeRule
 {
  public:
-  inline static TypeNode computeType(NodeManager* nodeManager,
-                                     TNode n,
-                                     bool check)
-  {
-    TypeNode t = n[0].getType(check);
-    if (check)
-    {
-      if (!t.isStringLike())
-      {
-        throw TypeCheckingExceptionPrivate(
-            n, "expecting a string-like term in replace");
-      }
-      TypeNode t2 = n[1].getType(check);
-      if (t != t2)
-      {
-        throw TypeCheckingExceptionPrivate(
-            n,
-            "expecting a term in second argument of replace that is the same "
-            "type as the first argument");
-      }
-      t2 = n[2].getType(check);
-      if (t != t2)
-      {
-        throw TypeCheckingExceptionPrivate(
-            n,
-            "expecting a term in third argument of replace that is the same "
-            "type as the first argument");
-      }
-    }
-    return t;
-  }
+  static TypeNode computeType(NodeManager* nodeManager, TNode n, bool check);
 };
 
 class StringStrToBoolTypeRule
 {
  public:
-  inline static TypeNode computeType(NodeManager* nodeManager,
-                                     TNode n,
-                                     bool check)
-  {
-    if (check)
-    {
-      TypeNode t = n[0].getType(check);
-      if (!t.isStringLike())
-      {
-        std::stringstream ss;
-        ss << "expecting a string-like term in argument of " << n.getKind();
-        throw TypeCheckingExceptionPrivate(n, ss.str());
-      }
-    }
-    return nodeManager->booleanType();
-  }
+  static TypeNode computeType(NodeManager* nodeManager, TNode n, bool check);
 };
 
 class StringStrToIntTypeRule
 {
  public:
-  inline static TypeNode computeType(NodeManager* nodeManager,
-                                     TNode n,
-                                     bool check)
-  {
-    if (check)
-    {
-      TypeNode t = n[0].getType(check);
-      if (!t.isStringLike())
-      {
-        std::stringstream ss;
-        ss << "expecting a string-like term in argument of " << n.getKind();
-        throw TypeCheckingExceptionPrivate(n, ss.str());
-      }
-    }
-    return nodeManager->integerType();
-  }
+  static TypeNode computeType(NodeManager* nodeManager, TNode n, bool check);
 };
 
 class StringStrToStrTypeRule
 {
  public:
-  inline static TypeNode computeType(NodeManager* nodeManager,
-                                     TNode n,
-                                     bool check)
-  {
-    TypeNode t = n[0].getType(check);
-    if (check)
-    {
-      if (!t.isStringLike())
-      {
-        std::stringstream ss;
-        ss << "expecting a string term in argument of " << n.getKind();
-        throw TypeCheckingExceptionPrivate(n, ss.str());
-      }
-    }
-    return t;
-  }
+  static TypeNode computeType(NodeManager* nodeManager, TNode n, bool check);
 };
 
 class StringRelationTypeRule
 {
  public:
-  inline static TypeNode computeType(NodeManager* nodeManager,
-                                     TNode n,
-                                     bool check)
-  {
-    if (check)
-    {
-      TypeNode t = n[0].getType(check);
-      if (!t.isStringLike())
-      {
-        throw TypeCheckingExceptionPrivate(
-            n, "expecting a string-like term in relation");
-      }
-      TypeNode t2 = n[1].getType(check);
-      if (t != t2)
-      {
-        throw TypeCheckingExceptionPrivate(
-            n, "expecting two terms of the same string-like type in relation");
-      }
-    }
-    return nodeManager->booleanType();
-  }
+  static TypeNode computeType(NodeManager* nodeManager, TNode n, bool check);
 };
 
 class RegExpRangeTypeRule {
 public:
-  inline static TypeNode computeType(NodeManager* nodeManager, TNode n, bool check)
-  {
-    if( check ) {
-      TNode::iterator it = n.begin();
-      unsigned ch[2];
-
-      for(int i=0; i<2; ++i) {
-        TypeNode t = (*it).getType(check);
-        if (!t.isString())  // string-only
-        {
-          throw TypeCheckingExceptionPrivate(n, "expecting a string term in regexp range");
-        }
-        if (!(*it).isConst())
-        {
-          throw TypeCheckingExceptionPrivate(n, "expecting a constant string term in regexp range");
-        }
-        if( (*it).getConst<String>().size() != 1 ) {
-          throw TypeCheckingExceptionPrivate(n, "expecting a single constant string term in regexp range");
-        }
-        unsigned ci = (*it).getConst<String>().front();
-        ch[i] = ci;
-        ++it;
-      }
-      if(ch[0] > ch[1]) {
-        throw TypeCheckingExceptionPrivate(n, "expecting the first constant is less or equal to the second one in regexp range");
-      }
-    }
-    return nodeManager->regExpType();
-  }
+ static TypeNode computeType(NodeManager* nodeManager, TNode n, bool check);
 };
 
 class ConstSequenceTypeRule
 {
  public:
-  static TypeNode computeType(NodeManager* nodeManager,
-                                     TNode n,
-                                     bool check)
-  {
-    Assert(n.getKind() == kind::CONST_SEQUENCE);
-    return nodeManager->mkSequenceType(n.getConst<Sequence>().getType());
-  }
+  static TypeNode computeType(NodeManager* nodeManager, TNode n, bool check);
 };
 
 class SeqUnitTypeRule
 {
  public:
-  static TypeNode computeType(NodeManager* nodeManager,
-                                     TNode n,
-                                     bool check)
-  {
-    return nodeManager->mkSequenceType(n[0].getType(check));
-  }
+  static TypeNode computeType(NodeManager* nodeManager, TNode n, bool check);
 };
 
 class SeqNthTypeRule
 {
  public:
-  static TypeNode computeType(NodeManager* nodeManager, TNode n, bool check)
-  {
-    TypeNode t = n[0].getType(check);
-    TypeNode t1 = t.getSequenceElementType();
-    if (check)
-    {
-      if (!t.isSequence())
-      {
-        throw TypeCheckingExceptionPrivate(n, "expecting a sequence in nth");
-      }
-      TypeNode t2 = n[1].getType(check);
-      if (!t2.isInteger())
-      {
-        throw TypeCheckingExceptionPrivate(
-            n, "expecting an integer start term in nth");
-      }
-    }
-    return t1;
-  }
+  static TypeNode computeType(NodeManager* nodeManager, TNode n, bool check);
 };
 
 /** Properties of the sequence type */
 struct SequenceProperties
 {
-  static Cardinality computeCardinality(TypeNode type)
-  {
-    Assert(type.getKind() == kind::SEQUENCE_TYPE);
-    return Cardinality::INTEGERS;
-  }
+  static Cardinality computeCardinality(TypeNode type);
   /** A sequence is well-founded if its element type is */
-  static bool isWellFounded(TypeNode type)
-  {
-    return type[0].isWellFounded();
-  }
+  static bool isWellFounded(TypeNode type);
   /** Make ground term for sequence type (return the empty sequence) */
-  static Node mkGroundTerm(TypeNode type)
-  {
-    Assert(type.isSequence());
-    // empty sequence
-    std::vector<Node> seq;
-    return NodeManager::currentNM()->mkConst(
-        Sequence(type.getSequenceElementType(), seq));
-  }
+  static Node mkGroundTerm(TypeNode type);
 }; /* struct SequenceProperties */
 
 }  // namespace strings