Do not mark string extended functions as eliminated after reduction lemmas (#4306)

The current policy marked extended functions in strings as "reduced" (eliminated) when we generated their reduction lemma. The upside is that the solver can effectively ignore them. The downside is that we cannot do context-dependent simplification on them, and hence we miss out conflicts during the remainder of the check-sat call.

This changes the policy so they are not marked as reduced. Instead, reduction lemmas are cached in the standard way while allowing context-dependent simplification.

2 files changed, 23 insertions, 15 deletions

diff --git a/src/theory/strings/extf_solver.cpp b/src/theory/strings/extf_solver.cpp
index 8ce2a3e81..0f4af2458 100644
--- a/src/theory/strings/extf_solver.cpp
+++ b/src/theory/strings/extf_solver.cpp
@@ -47,7 +47,8 @@ ExtfSolver::ExtfSolver(context::Context* c,
       d_statistics(statistics),
       d_preproc(&skc, u, statistics),
       d_hasExtf(c, false),
-      d_extfInferCache(c)
+      d_extfInferCache(c),
+      d_reduced(u)
 {
   d_extt->addFunctionKind(kind::STRING_SUBSTR);
   d_extt->addFunctionKind(kind::STRING_STRIDOF);
@@ -69,7 +70,7 @@ ExtfSolver::ExtfSolver(context::Context* c,
 
 ExtfSolver::~ExtfSolver() {}
 
-bool ExtfSolver::doReduction(int effort, Node n, bool& isCd)
+bool ExtfSolver::doReduction(int effort, Node n)
 {
   Assert(d_extfInfoTmp.find(n) != d_extfInfoTmp.end());
   if (!d_extfInfoTmp[n].d_modelActive)
@@ -77,6 +78,11 @@ bool ExtfSolver::doReduction(int effort, Node n, bool& isCd)
     // n is not active in the model, no need to reduce
     return false;
   }
+  if (d_reduced.find(n)!=d_reduced.end())
+  {
+    // already sent a reduction lemma
+    return false;
+  }
   // determine the effort level to process the extf at
   // 0 - at assertion time, 1+ - after no other reduction is applicable
   int r_effort = -1;
@@ -118,9 +124,9 @@ bool ExtfSolver::doReduction(int effort, Node n, bool& isCd)
             Node xneqs = x.eqNode(s).negate();
             d_im.sendInference(lexp, xneqs, Inference::CTN_NEG_EQUAL, true);
           }
-          // this depends on the current assertions, so we set that this
-          // inference is context-dependent.
-          isCd = true;
+          // this depends on the current assertions, so this
+          // inference is context-dependent
+          d_extt->markReduced(n, true);
           return true;
         }
         else
@@ -168,7 +174,7 @@ bool ExtfSolver::doReduction(int effort, Node n, bool& isCd)
     Trace("strings-red-lemma") << "Reduction (positive contains) lemma : " << n
                                << " => " << eq << std::endl;
     // context-dependent because it depends on the polarity of n itself
-    isCd = true;
+    d_extt->markReduced(n, true);
   }
   else if (k != kind::STRING_TO_CODE)
   {
@@ -190,7 +196,8 @@ bool ExtfSolver::doReduction(int effort, Node n, bool& isCd)
     d_im.sendInference(d_emptyVec, nnlem, Inference::REDUCTION, true);
     Trace("strings-extf-debug")
         << "  resolve extf : " << n << " based on reduction." << std::endl;
-    isCd = false;
+    // add as reduction lemma
+    d_reduced.insert(n);
   }
   return true;
 }
@@ -209,12 +216,10 @@ void ExtfSolver::checkExtfReductions(int effort)
     Trace("strings-process")
         << "  check " << n
         << ", active in model=" << d_extfInfoTmp[n].d_modelActive << std::endl;
-    // whether the reduction was context-dependent
-    bool isCd = false;
-    bool ret = doReduction(effort, n, isCd);
+    bool ret = doReduction(effort, n);
     if (ret)
     {
-      d_extt->markReduced(n, isCd);
+      // we do not mark as reduced, since we may want to evaluate
       if (d_im.hasProcessed())
       {
         return;
diff --git a/src/theory/strings/extf_solver.h b/src/theory/strings/extf_solver.h
index e7e2512bd..f0f0d790b 100644
--- a/src/theory/strings/extf_solver.h
+++ b/src/theory/strings/extf_solver.h
@@ -161,11 +161,12 @@ class ExtfSolver
    * This is called when an extended function application n is not able to be
    * simplified by context-depdendent simplification, and we are resorting to
    * expanding n to its full semantics via a reduction. This method returns
-   * true if it successfully reduced n by some reduction and sets isCd to
-   * true if the reduction was (SAT)-context-dependent, and false otherwise.
-   * The argument effort has the same meaning as in checkExtfReductions.
+   * true if it successfully reduced n by some reduction. If so, it either
+   * caches that the reduction lemma was sent, or marks n as reduced in this
+   * SAT-context. The argument effort has the same meaning as in
+   * checkExtfReductions.
    */
-  bool doReduction(int effort, Node n, bool& isCd);
+  bool doReduction(int effort, Node n);
   /** check extended function inferences
    *
    * This function makes additional inferences for n that do not contribute
@@ -205,6 +206,8 @@ class ExtfSolver
   context::CDO<bool> d_hasExtf;
   /** extended functions inferences cache */
   NodeSet d_extfInferCache;
+  /** The set of extended functions we have sent reduction lemmas for */
+  NodeSet d_reduced;
 };
 
 }  // namespace strings