Move check memberships to reg exp solver (#3793)

There was previously a function in TheoryStrings to make the proper call to checkMembership. In the refactored code, this is no longer necessary and the interface to RegExp can be simplified.

6 files changed, 62 insertions, 45 deletions

diff --git a/src/theory/strings/extf_solver.cpp b/src/theory/strings/extf_solver.cpp
index e22528490..6ab74cf9a 100644
--- a/src/theory/strings/extf_solver.cpp
+++ b/src/theory/strings/extf_solver.cpp
@@ -668,6 +668,11 @@ const std::map<Node, ExtfInfoTmp>& ExtfSolver::getInfo() const
 }
 bool ExtfSolver::hasExtendedFunctions() const { return d_hasExtf.get(); }
 
+std::vector<Node> ExtfSolver::getActive(Kind k) const
+{
+  return d_extt->getActive(k);
+}
+
 }  // namespace strings
 }  // namespace theory
 }  // namespace CVC4
diff --git a/src/theory/strings/extf_solver.h b/src/theory/strings/extf_solver.h
index e0e41bc3d..4c848f430 100644
--- a/src/theory/strings/extf_solver.h
+++ b/src/theory/strings/extf_solver.h
@@ -145,6 +145,11 @@ class ExtfSolver
   const std::map<Node, ExtfInfoTmp>& getInfo() const;
   /** Are there any active extended functions? */
   bool hasExtendedFunctions() const;
+  /**
+   * Get the function applications of kind k that are active in the current
+   * context (see ExtTheory::getActive).
+   */
+  std::vector<Node> getActive(Kind k) const;
 
  private:
   /** do reduction
diff --git a/src/theory/strings/regexp_solver.cpp b/src/theory/strings/regexp_solver.cpp
index e4fe2cf17..5b41feacb 100644
--- a/src/theory/strings/regexp_solver.cpp
+++ b/src/theory/strings/regexp_solver.cpp
@@ -36,11 +36,13 @@ namespace strings {
 RegExpSolver::RegExpSolver(TheoryStrings& p,
                            SolverState& s,
                            InferenceManager& im,
+                           ExtfSolver& es,
                            context::Context* c,
                            context::UserContext* u)
     : d_parent(p),
       d_state(s),
       d_im(im),
+      d_esolver(es),
       d_regexp_ucached(u),
       d_regexp_ccached(c),
       d_processed_memberships(c)
@@ -57,6 +59,37 @@ Node RegExpSolver::mkAnd(Node c1, Node c2)
   return NodeManager::currentNM()->mkNode(AND, c1, c2);
 }
 
+void RegExpSolver::checkMemberships()
+{
+  // add the memberships
+  std::vector<Node> mems = d_esolver.getActive(STRING_IN_REGEXP);
+  // maps representatives to regular expression memberships in that class
+  std::map<Node, std::vector<Node> > assertedMems;
+  const std::map<Node, ExtfInfoTmp>& einfo = d_esolver.getInfo();
+  std::map<Node, ExtfInfoTmp>::const_iterator it;
+  for (unsigned i = 0; i < mems.size(); i++)
+  {
+    Node n = mems[i];
+    Assert(n.getKind() == STRING_IN_REGEXP);
+    it = einfo.find(n);
+    Assert(it != einfo.end());
+    if (!it->second.d_const.isNull())
+    {
+      bool pol = it->second.d_const.getConst<bool>();
+      Trace("strings-process-debug")
+          << "  add membership : " << n << ", pol = " << pol << std::endl;
+      Node r = d_state.getRepresentative(n[0]);
+      assertedMems[r].push_back(pol ? n : n.negate());
+    }
+    else
+    {
+      Trace("strings-process-debug")
+          << "  irrelevant (non-asserted) membership : " << n << std::endl;
+    }
+  }
+  check(assertedMems);
+}
+
 void RegExpSolver::check(const std::map<Node, std::vector<Node> >& mems)
 {
   bool addedLemma = false;
diff --git a/src/theory/strings/regexp_solver.h b/src/theory/strings/regexp_solver.h
index a43ea516a..4880af905 100644
--- a/src/theory/strings/regexp_solver.h
+++ b/src/theory/strings/regexp_solver.h
@@ -23,6 +23,7 @@
 #include "context/cdlist.h"
 #include "context/context.h"
 #include "expr/node.h"
+#include "theory/strings/extf_solver.h"
 #include "theory/strings/inference_manager.h"
 #include "theory/strings/regexp_operation.h"
 #include "theory/strings/solver_state.h"
@@ -47,10 +48,22 @@ class RegExpSolver
   RegExpSolver(TheoryStrings& p,
                SolverState& s,
                InferenceManager& im,
+               ExtfSolver& es,
                context::Context* c,
                context::UserContext* u);
   ~RegExpSolver() {}
 
+  /** check regular expression memberships
+   *
+   * This checks the satisfiability of all regular expression memberships
+   * of the form (not) s in R. We use various heuristic techniques based on
+   * unrolling, combined with techniques from Liang et al, "A Decision Procedure
+   * for Regular Membership and Length Constraints over Unbounded Strings",
+   * FroCoS 2015.
+   */
+  void checkMemberships();
+
+ private:
   /** check
    *
    * Tells this solver to check whether the regular expressions in mems
@@ -63,8 +76,6 @@ class RegExpSolver
    * engine of the theory of strings.
    */
   void check(const std::map<Node, std::vector<Node>>& mems);
-
- private:
   /**
    * Check memberships in equivalence class for regular expression
    * inclusion.
@@ -106,6 +117,8 @@ class RegExpSolver
   SolverState& d_state;
   /** the output channel of the parent of this object */
   InferenceManager& d_im;
+  /** reference to the extended function solver of the parent */
+  ExtfSolver& d_esolver;
   // check membership constraints
   Node mkAnd(Node c1, Node c2);
   /**
diff --git a/src/theory/strings/theory_strings.cpp b/src/theory/strings/theory_strings.cpp
index 5be2f96d4..d3d75a98d 100644
--- a/src/theory/strings/theory_strings.cpp
+++ b/src/theory/strings/theory_strings.cpp
@@ -79,7 +79,7 @@ TheoryStrings::TheoryStrings(context::Context* c,
       d_bsolver(c, u, d_state, d_im),
       d_csolver(c, u, d_state, d_im, d_sk_cache, d_bsolver),
       d_esolver(nullptr),
-      d_regexp_solver(*this, d_state, d_im, c, u),
+      d_rsolver(nullptr),
       d_stringsFmf(c, u, valuation, d_sk_cache),
       d_strategy_init(false)
 {
@@ -87,6 +87,7 @@ TheoryStrings::TheoryStrings(context::Context* c,
   ExtTheory* extt = getExtTheory();
   d_esolver.reset(new ExtfSolver(
       c, u, d_state, d_im, d_sk_cache, d_bsolver, d_csolver, extt));
+  d_rsolver.reset(new RegExpSolver(*this, d_state, d_im, *d_esolver, c, u));
   getExtTheory()->addFunctionKind(kind::STRING_SUBSTR);
   getExtTheory()->addFunctionKind(kind::STRING_STRIDOF);
   getExtTheory()->addFunctionKind(kind::STRING_ITOS);
@@ -726,37 +727,6 @@ bool TheoryStrings::needsCheckLastEffort() {
   return false;
 }
 
-void TheoryStrings::checkMemberships()
-{
-  // add the memberships
-  std::vector<Node> mems = getExtTheory()->getActive(kind::STRING_IN_REGEXP);
-  // maps representatives to regular expression memberships in that class
-  std::map<Node, std::vector<Node> > assertedMems;
-  const std::map<Node, ExtfInfoTmp>& einfo = d_esolver->getInfo();
-  std::map<Node, ExtfInfoTmp>::const_iterator it;
-  for (unsigned i = 0; i < mems.size(); i++)
-  {
-    Node n = mems[i];
-    Assert(n.getKind() == STRING_IN_REGEXP);
-    it = einfo.find(n);
-    Assert(it != einfo.end());
-    if (!it->second.d_const.isNull())
-    {
-      bool pol = it->second.d_const.getConst<bool>();
-      Trace("strings-process-debug")
-          << "  add membership : " << n << ", pol = " << pol << std::endl;
-      Node r = d_state.getRepresentative(n[0]);
-      assertedMems[r].push_back(pol ? n : n.negate());
-    }
-    else
-    {
-      Trace("strings-process-debug")
-          << "  irrelevant (non-asserted) membership : " << n << std::endl;
-    }
-  }
-  d_regexp_solver.check(assertedMems);
-}
-
 /** Conflict when merging two constants */
 void TheoryStrings::conflict(TNode a, TNode b){
   if (!d_state.isInConflict())
@@ -1223,7 +1193,7 @@ void TheoryStrings::runInferStep(InferStep s, int effort)
     case CHECK_LENGTH_EQC: d_csolver.checkLengthsEqc(); break;
     case CHECK_REGISTER_TERMS_NF: checkRegisterTermsNormalForms(); break;
     case CHECK_EXTF_REDUCTION: d_esolver->checkExtfReductions(effort); break;
-    case CHECK_MEMBERSHIP: checkMemberships(); break;
+    case CHECK_MEMBERSHIP: d_rsolver->checkMemberships(); break;
     case CHECK_CARDINALITY: d_bsolver.checkCardinality(); break;
     default: Unreachable(); break;
   }
diff --git a/src/theory/strings/theory_strings.h b/src/theory/strings/theory_strings.h
index f40af6e67..e0fca1b2e 100644
--- a/src/theory/strings/theory_strings.h
+++ b/src/theory/strings/theory_strings.h
@@ -344,7 +344,7 @@ private:
    */
   std::unique_ptr<ExtfSolver> d_esolver;
   /** regular expression solver module */
-  RegExpSolver d_regexp_solver;
+  std::unique_ptr<RegExpSolver> d_rsolver;
   /** regular expression elimination module */
   RegExpElimination d_regexp_elim;
   /** Strings finite model finding decision strategy */
@@ -392,15 +392,6 @@ private:
    * there does not exist a term of the form str.len(si) in the current context.
    */
   void checkRegisterTermsNormalForms();
-  /** check regular expression memberships
-   *
-   * This checks the satisfiability of all regular expression memberships
-   * of the form (not) s in R. We use various heuristic techniques based on
-   * unrolling, combined with techniques from Liang et al, "A Decision Procedure
-   * for Regular Membership and Length Constraints over Unbounded Strings",
-   * FroCoS 2015.
-   */
-  void checkMemberships();
   //-----------------------end inference steps
 
   //-----------------------representation of the strategy