Move equivalence class info to its own file in strings (#3799)

Code move only, no updates to behavior or content of code in this PR.

5 files changed, 228 insertions, 164 deletions

diff --git a/src/CMakeLists.txt b/src/CMakeLists.txt
index e8c38f39d..30cdf15b7 100644
--- a/src/CMakeLists.txt
+++ b/src/CMakeLists.txt
@@ -672,6 +672,8 @@ libcvc4_add_sources(
   theory/strings/core_solver.h
   theory/strings/extf_solver.cpp
   theory/strings/extf_solver.h
+  theory/strings/eqc_info.cpp
+  theory/strings/eqc_info.h
   theory/strings/infer_info.cpp
   theory/strings/infer_info.h
   theory/strings/inference_manager.cpp
diff --git a/src/theory/strings/eqc_info.cpp b/src/theory/strings/eqc_info.cpp
new file mode 100644
index 000000000..ab6d473bd
--- /dev/null
+++ b/src/theory/strings/eqc_info.cpp
@@ -0,0 +1,143 @@
+/*********************                                                        */
+/*! \file eqc_info.cpp
+ ** \verbatim
+ ** Top contributors (to current version):
+ **   Andrew Reynolds
+ ** 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 Implementation of equivalence class info for the theory of strings
+ **/
+
+#include "theory/strings/eqc_info.h"
+
+#include "theory/strings/theory_strings_utils.h"
+
+using namespace std;
+using namespace CVC4::context;
+using namespace CVC4::kind;
+
+namespace CVC4 {
+namespace theory {
+namespace strings {
+
+EqcInfo::EqcInfo(context::Context* c)
+    : d_lengthTerm(c),
+      d_codeTerm(c),
+      d_cardinalityLemK(c),
+      d_normalizedLength(c),
+      d_prefixC(c),
+      d_suffixC(c)
+{
+}
+
+Node EqcInfo::addEndpointConst(Node t, Node c, bool isSuf)
+{
+  // check conflict
+  Node prev = isSuf ? d_suffixC : d_prefixC;
+  if (!prev.isNull())
+  {
+    Trace("strings-eager-pconf-debug") << "Check conflict " << prev << ", " << t
+                                       << " post=" << isSuf << std::endl;
+    Node prevC = utils::getConstantEndpoint(prev, isSuf);
+    Assert(!prevC.isNull());
+    Assert(prevC.getKind() == CONST_STRING);
+    if (c.isNull())
+    {
+      c = utils::getConstantEndpoint(t, isSuf);
+      Assert(!c.isNull());
+    }
+    Assert(c.getKind() == CONST_STRING);
+    bool conflict = false;
+    // if the constant prefixes are different
+    if (c != prevC)
+    {
+      // conflicts between constants should be handled by equality engine
+      Assert(!t.isConst() || !prev.isConst());
+      Trace("strings-eager-pconf-debug")
+          << "Check conflict constants " << prevC << ", " << c << std::endl;
+      const String& ps = prevC.getConst<String>();
+      const String& cs = c.getConst<String>();
+      unsigned pvs = ps.size();
+      unsigned cvs = cs.size();
+      if (pvs == cvs || (pvs > cvs && t.isConst())
+          || (cvs > pvs && prev.isConst()))
+      {
+        // If equal length, cannot be equal due to node check above.
+        // If one is fully constant and has less length than the other, then the
+        // other will not fit and we are in conflict.
+        conflict = true;
+      }
+      else
+      {
+        const String& larges = pvs > cvs ? ps : cs;
+        const String& smalls = pvs > cvs ? cs : ps;
+        if (isSuf)
+        {
+          conflict = !larges.hasSuffix(smalls);
+        }
+        else
+        {
+          conflict = !larges.hasPrefix(smalls);
+        }
+      }
+      if (!conflict && (pvs > cvs || prev.isConst()))
+      {
+        // current is subsumed, either shorter prefix or the other is a full
+        // constant
+        return Node::null();
+      }
+    }
+    else if (!t.isConst())
+    {
+      // current is subsumed since the other may be a full constant
+      return Node::null();
+    }
+    if (conflict)
+    {
+      Trace("strings-eager-pconf")
+          << "Conflict for " << prevC << ", " << c << std::endl;
+      std::vector<Node> ccs;
+      Node r[2];
+      for (unsigned i = 0; i < 2; i++)
+      {
+        Node tp = i == 0 ? t : prev;
+        if (tp.getKind() == STRING_IN_REGEXP)
+        {
+          ccs.push_back(tp);
+          r[i] = tp[0];
+        }
+        else
+        {
+          r[i] = tp;
+        }
+      }
+      if (r[0] != r[1])
+      {
+        ccs.push_back(r[0].eqNode(r[1]));
+      }
+      Assert(!ccs.empty());
+      Node ret =
+          ccs.size() == 1 ? ccs[0] : NodeManager::currentNM()->mkNode(AND, ccs);
+      Trace("strings-eager-pconf")
+          << "String: eager prefix conflict: " << ret << std::endl;
+      return ret;
+    }
+  }
+  if (isSuf)
+  {
+    d_suffixC = t;
+  }
+  else
+  {
+    d_prefixC = t;
+  }
+  return Node::null();
+}
+
+}  // namespace strings
+}  // namespace theory
+}  // namespace CVC4
diff --git a/src/theory/strings/eqc_info.h b/src/theory/strings/eqc_info.h
new file mode 100644
index 000000000..241b7d523
--- /dev/null
+++ b/src/theory/strings/eqc_info.h
@@ -0,0 +1,81 @@
+/*********************                                                        */
+/*! \file eqc_info.h
+ ** \verbatim
+ ** Top contributors (to current version):
+ **   Andrew Reynolds
+ ** 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 Equivalence class info for the theory of strings
+ **/
+
+#include "cvc4_private.h"
+
+#ifndef CVC4__THEORY__STRINGS__EQC_INFO_H
+#define CVC4__THEORY__STRINGS__EQC_INFO_H
+
+#include <map>
+
+#include "context/cdo.h"
+#include "context/context.h"
+#include "expr/node.h"
+
+namespace CVC4 {
+namespace theory {
+namespace strings {
+
+/**
+ * SAT-context-dependent information about an equivalence class. This
+ * information is updated eagerly as assertions are processed by the theory of
+ * strings at standard effort.
+ */
+class EqcInfo
+{
+ public:
+  EqcInfo(context::Context* c);
+  ~EqcInfo() {}
+  /** add prefix constant
+   *
+   * This informs this equivalence class info that a term t in its
+   * equivalence class has a constant prefix (if isSuf=true) or suffix
+   * (if isSuf=false). The constant c (if non-null) is the value of that
+   * constant, if it has been computed already.
+   *
+   * If this method returns a non-null node ret, then ret is a conjunction
+   * corresponding to a conflict that holds in the current context.
+   */
+  Node addEndpointConst(Node t, Node c, bool isSuf);
+  /**
+   * If non-null, this is a term x from this eq class such that str.len( x )
+   * occurs as a term in this SAT context.
+   */
+  context::CDO<Node> d_lengthTerm;
+  /**
+   * If non-null, this is a term x from this eq class such that str.code( x )
+   * occurs as a term in this SAT context.
+   */
+  context::CDO<Node> d_codeTerm;
+  context::CDO<unsigned> d_cardinalityLemK;
+  context::CDO<Node> d_normalizedLength;
+  /**
+   * A node that explains the longest constant prefix known of this
+   * equivalence class. This can either be:
+   * (1) A term from this equivalence class, including a constant "ABC" or
+   * concatenation term (str.++ "ABC" ...), or
+   * (2) A membership of the form (str.in.re x R) where x is in this
+   * equivalence class and R is a regular expression of the form
+   * (str.to.re "ABC") or (re.++ (str.to.re "ABC") ...).
+   */
+  context::CDO<Node> d_prefixC;
+  /** same as above, for suffix. */
+  context::CDO<Node> d_suffixC;
+};
+
+}  // namespace strings
+}  // namespace theory
+}  // namespace CVC4
+
+#endif /* CVC4__THEORY__STRINGS__EQC_INFO_H */
diff --git a/src/theory/strings/solver_state.cpp b/src/theory/strings/solver_state.cpp
index 5eb0818b7..422c9e58b 100644
--- a/src/theory/strings/solver_state.cpp
+++ b/src/theory/strings/solver_state.cpp
@@ -24,120 +24,6 @@ namespace CVC4 {
 namespace theory {
 namespace strings {
 
-EqcInfo::EqcInfo(context::Context* c)
-    : d_lengthTerm(c),
-      d_codeTerm(c),
-      d_cardinalityLemK(c),
-      d_normalizedLength(c),
-      d_prefixC(c),
-      d_suffixC(c)
-{
-}
-
-Node EqcInfo::addEndpointConst(Node t, Node c, bool isSuf)
-{
-  // check conflict
-  Node prev = isSuf ? d_suffixC : d_prefixC;
-  if (!prev.isNull())
-  {
-    Trace("strings-eager-pconf-debug") << "Check conflict " << prev << ", " << t
-                                       << " post=" << isSuf << std::endl;
-    Node prevC = utils::getConstantEndpoint(prev, isSuf);
-    Assert(!prevC.isNull());
-    Assert(prevC.getKind() == CONST_STRING);
-    if (c.isNull())
-    {
-      c = utils::getConstantEndpoint(t, isSuf);
-      Assert(!c.isNull());
-    }
-    Assert(c.getKind() == CONST_STRING);
-    bool conflict = false;
-    // if the constant prefixes are different
-    if (c != prevC)
-    {
-      // conflicts between constants should be handled by equality engine
-      Assert(!t.isConst() || !prev.isConst());
-      Trace("strings-eager-pconf-debug")
-          << "Check conflict constants " << prevC << ", " << c << std::endl;
-      const String& ps = prevC.getConst<String>();
-      const String& cs = c.getConst<String>();
-      unsigned pvs = ps.size();
-      unsigned cvs = cs.size();
-      if (pvs == cvs || (pvs > cvs && t.isConst())
-          || (cvs > pvs && prev.isConst()))
-      {
-        // If equal length, cannot be equal due to node check above.
-        // If one is fully constant and has less length than the other, then the
-        // other will not fit and we are in conflict.
-        conflict = true;
-      }
-      else
-      {
-        const String& larges = pvs > cvs ? ps : cs;
-        const String& smalls = pvs > cvs ? cs : ps;
-        if (isSuf)
-        {
-          conflict = !larges.hasSuffix(smalls);
-        }
-        else
-        {
-          conflict = !larges.hasPrefix(smalls);
-        }
-      }
-      if (!conflict && (pvs > cvs || prev.isConst()))
-      {
-        // current is subsumed, either shorter prefix or the other is a full
-        // constant
-        return Node::null();
-      }
-    }
-    else if (!t.isConst())
-    {
-      // current is subsumed since the other may be a full constant
-      return Node::null();
-    }
-    if (conflict)
-    {
-      Trace("strings-eager-pconf")
-          << "Conflict for " << prevC << ", " << c << std::endl;
-      std::vector<Node> ccs;
-      Node r[2];
-      for (unsigned i = 0; i < 2; i++)
-      {
-        Node tp = i == 0 ? t : prev;
-        if (tp.getKind() == STRING_IN_REGEXP)
-        {
-          ccs.push_back(tp);
-          r[i] = tp[0];
-        }
-        else
-        {
-          r[i] = tp;
-        }
-      }
-      if (r[0] != r[1])
-      {
-        ccs.push_back(r[0].eqNode(r[1]));
-      }
-      Assert(!ccs.empty());
-      Node ret =
-          ccs.size() == 1 ? ccs[0] : NodeManager::currentNM()->mkNode(AND, ccs);
-      Trace("strings-eager-pconf")
-          << "String: eager prefix conflict: " << ret << std::endl;
-      return ret;
-    }
-  }
-  if (isSuf)
-  {
-    d_suffixC = t;
-  }
-  else
-  {
-    d_prefixC = t;
-  }
-  return Node::null();
-}
-
 SolverState::SolverState(context::Context* c,
                          eq::EqualityEngine& ee,
                          Valuation& v)
diff --git a/src/theory/strings/solver_state.h b/src/theory/strings/solver_state.h
index b295ba12d..e3fe432d3 100644
--- a/src/theory/strings/solver_state.h
+++ b/src/theory/strings/solver_state.h
@@ -19,66 +19,18 @@
 
 #include <map>
 
-#include "context/cdo.h"
 #include "context/context.h"
 #include "expr/node.h"
-#include "options/theory_options.h"
 #include "theory/theory_model.h"
 #include "theory/uf/equality_engine.h"
 #include "theory/valuation.h"
+#include "theory/strings/eqc_info.h"
 
 namespace CVC4 {
 namespace theory {
 namespace strings {
 
 /**
- * SAT-context-dependent information about an equivalence class. This
- * information is updated eagerly as assertions are processed by the theory of
- * strings at standard effort.
- */
-class EqcInfo
-{
- public:
-  EqcInfo(context::Context* c);
-  ~EqcInfo() {}
-  /** add prefix constant
-   *
-   * This informs this equivalence class info that a term t in its
-   * equivalence class has a constant prefix (if isSuf=true) or suffix
-   * (if isSuf=false). The constant c (if non-null) is the value of that
-   * constant, if it has been computed already.
-   *
-   * If this method returns a non-null node ret, then ret is a conjunction
-   * corresponding to a conflict that holds in the current context.
-   */
-  Node addEndpointConst(Node t, Node c, bool isSuf);
-  /**
-   * If non-null, this is a term x from this eq class such that str.len( x )
-   * occurs as a term in this SAT context.
-   */
-  context::CDO<Node> d_lengthTerm;
-  /**
-   * If non-null, this is a term x from this eq class such that str.code( x )
-   * occurs as a term in this SAT context.
-   */
-  context::CDO<Node> d_codeTerm;
-  context::CDO<unsigned> d_cardinalityLemK;
-  context::CDO<Node> d_normalizedLength;
-  /**
-   * A node that explains the longest constant prefix known of this
-   * equivalence class. This can either be:
-   * (1) A term from this equivalence class, including a constant "ABC" or
-   * concatenation term (str.++ "ABC" ...), or
-   * (2) A membership of the form (str.in.re x R) where x is in this
-   * equivalence class and R is a regular expression of the form
-   * (str.to.re "ABC") or (re.++ (str.to.re "ABC") ...).
-   */
-  context::CDO<Node> d_prefixC;
-  /** same as above, for suffix. */
-  context::CDO<Node> d_suffixC;
-};
-
-/**
  * Solver state for strings.
  *
  * The purpose of this class is track and provide query functions for the state
@@ -224,4 +176,4 @@ class SolverState
 }  // namespace theory
 }  // namespace CVC4
 
-#endif /* CVC4__THEORY__STRINGS__THEORY_STRINGS_H */
+#endif /* CVC4__THEORY__STRINGS__SOLVER_STATE_H */