Add switches to toggle eager and inclusion solvers (#7784)

diff --git a/src/options/strings_options.toml b/src/options/strings_options.toml
index 05025708b344c614345036c6e25b86882ed7fed1..74112b2862af47e11c5c02a5f65f8657f082239c 100644 (file)
--- a/src/options/strings_options.toml
+++ b/src/options/strings_options.toml
@@ -208,6 +208,22 @@ name   = "Strings Theory"
   default    = "false"
   help       = "use regular expressions for eager length conflicts"
 
+[[option]]
+  name       = "stringEagerSolver"
+  category   = "regular"
+  long       = "strings-eager-solver"
+  type       = "bool"
+  default    = "true"
+  help       = "use the eager solver"
+
+[[option]]
+  name       = "stringRegexpInclusion"
+  category   = "regular"
+  long       = "strings-regexp-inclusion"
+  type       = "bool"
+  default    = "true"
+  help       = "use regular expression inclusion"
+
 [[option]]
   name       = "seqArray"
   category   = "expert"

diff --git a/src/theory/strings/regexp_solver.cpp b/src/theory/strings/regexp_solver.cpp
index 24ce64842154fd9fe886a5adb005c5c75f284a10..9a13aeab3f02a5b1147c7e81a25aa7388ebc2ec7 100644 (file)
--- a/src/theory/strings/regexp_solver.cpp
+++ b/src/theory/strings/regexp_solver.cpp
@@ -115,7 +115,7 @@ bool RegExpSolver::checkInclInter(
     std::vector<Node> mems2 = mr.second;
     Trace("regexp-process")
         << "Memberships(" << mr.first << ") = " << mr.second << std::endl;
-    if (!checkEqcInclusion(mems2))
+    if (options().strings.stringRegexpInclusion && !checkEqcInclusion(mems2))
     {
       // conflict discovered, return
       return true;

diff --git a/src/theory/strings/theory_strings.cpp b/src/theory/strings/theory_strings.cpp
index 8b496b725006e7717932dbe31ba851d320d9f202..25db8d1904518e840e913a101520b867c62f4ed3 100644 (file)
--- a/src/theory/strings/theory_strings.cpp
+++ b/src/theory/strings/theory_strings.cpp
@@ -59,7 +59,9 @@ TheoryStrings::TheoryStrings(Env& env, OutputChannel& out, Valuation valuation)
       d_rewriter(env.getRewriter(),
                  &d_statistics.d_rewrites,
                  d_termReg.getAlphabetCardinality()),
-      d_eagerSolver(env, d_state, d_termReg),
+      d_eagerSolver(options().strings.stringEagerSolver
+                        ? new EagerSolver(env, d_state, d_termReg)
+                        : nullptr),
       d_extTheoryCb(),
       d_im(env, *this, d_state, d_termReg, d_extTheory, d_statistics),
       d_extTheory(env, d_extTheoryCb, d_im),
@@ -651,7 +653,10 @@ void TheoryStrings::notifyFact(TNode atom,
                                TNode fact,
                                bool isInternal)
 {
-  d_eagerSolver.notifyFact(atom, polarity, fact, isInternal);
+  if (d_eagerSolver)
+  {
+    d_eagerSolver->notifyFact(atom, polarity, fact, isInternal);
+  }
   // process pending conflicts due to reasoning about endpoints
   if (!d_state.isInConflict() && d_state.hasPendingConflict())
   {
@@ -769,7 +774,10 @@ void TheoryStrings::eqNotifyNewClass(TNode t){
       ei->d_codeTerm = t[0];
     }
   }
-  d_eagerSolver.eqNotifyNewClass(t);
+  if (d_eagerSolver)
+  {
+    d_eagerSolver->eqNotifyNewClass(t);
+  }
 }
 
 void TheoryStrings::eqNotifyMerge(TNode t1, TNode t2)
@@ -782,7 +790,10 @@ void TheoryStrings::eqNotifyMerge(TNode t1, TNode t2)
   // always create it if e2 was non-null
   EqcInfo* e1 = d_state.getOrMakeEqcInfo(t1);
 
-  d_eagerSolver.eqNotifyMerge(e1, t1, e2, t2);
+  if (d_eagerSolver)
+  {
+    d_eagerSolver->eqNotifyMerge(e1, t1, e2, t2);
+  }
 
   // add information from e2 to e1
   if (!e2->d_lengthTerm.get().isNull())

diff --git a/src/theory/strings/theory_strings.h b/src/theory/strings/theory_strings.h
index 21db7da0c3dbae51e32ff04e0ed8432d2c459d57..dd15e08ecb09c35ceef07fb1fcefffe3ab995dea 100644 (file)
--- a/src/theory/strings/theory_strings.h
+++ b/src/theory/strings/theory_strings.h
@@ -259,7 +259,7 @@ class TheoryStrings : public Theory {
   /** The theory rewriter for this theory. */
   StringsRewriter d_rewriter;
   /** The eager solver */
-  EagerSolver d_eagerSolver;
+  std::unique_ptr<EagerSolver> d_eagerSolver;
   /** The extended theory callback */
   StringsExtfCallback d_extTheoryCb;
   /** The (custom) output channel of the theory of strings */