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.

diff --git a/src/theory/strings/extf_solver.cpp b/src/theory/strings/extf_solver.cpp
index 8ce2a3e812053ee21802baaa68d7685099fe3136..0f4af245817d6a9ee0e5e69669dbede0988a49eb 100644 (file)
--- 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 e7e2512bde8dfc4fac8ffc6a3901d207af63b3dc..f0f0d790b2431e777c716a95605c495e8579ec81 100644 (file)
--- 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