Avoid circular dependencies for justifying reductions in strings extf eval (#4415)

An incorrect answer of "sat" could be found after 8 seconds on the given benchmark (with --strings-fmf) due to a circular justification for why an extended function was reduced. In particular, we ran checkExtfInference on the same term twice and then marked it as reduced since we had already seen it. This makes the code more conservative.

Notice I'm making the code doubly conservative in case there is any chance for duplication again (e.g. if ExtTheory provides duplicate terms).

diff --git a/src/theory/strings/extf_solver.cpp b/src/theory/strings/extf_solver.cpp
index 55985406ed78135d7bb2d0a5eb80563c0443ba8c..dd41443131d70ad4e0c4e99077dc26fe6d9a2335 100644 (file)
--- a/src/theory/strings/extf_solver.cpp
+++ b/src/theory/strings/extf_solver.cpp
@@ -235,6 +235,8 @@ void ExtfSolver::checkExtfEval(int effort)
   NodeManager* nm = NodeManager::currentNM();
   bool has_nreduce = false;
   std::vector<Node> terms = d_extt.getActive();
+  // the set of terms we have done extf inferences for
+  std::unordered_set<Node, NodeHashFunction> inferProcessed;
   for (const Node& n : terms)
   {
     // Setup information about n, including if it is equal to a constant.
@@ -415,16 +417,22 @@ void ExtfSolver::checkExtfEval(int effort)
               effort == 0 ? Inference::EXTF_D : Inference::EXTF_D_N;
           d_im.sendInternalInference(einfo.d_exp, nrcAssert, infer);
         }
-        to_reduce = nrc;
+        // We must use the original n here to avoid circular justifications for
+        // why extended functions are reduced below. In particular, to_reduce
+        // should never be a duplicate of another term considered in the block
+        // of code for checkExtfInference below.
+        to_reduce = n;
       }
     }
     else
     {
       to_reduce = n;
     }
-    // if not reduced
-    if (!to_reduce.isNull())
+    // if not reduced and not processed
+    if (!to_reduce.isNull()
+        && inferProcessed.find(to_reduce) == inferProcessed.end())
     {
+      inferProcessed.insert(to_reduce);
       Assert(effort < 3);
       if (effort == 1)
       {

diff --git a/test/regress/CMakeLists.txt b/test/regress/CMakeLists.txt
index 656bb5880ad4534a0a46edc1f3e21dfe5dc3c204..38b741ced84083b8bccae54f08bc08f025183e3a 100644 (file)
--- a/test/regress/CMakeLists.txt
+++ b/test/regress/CMakeLists.txt
@@ -2114,6 +2114,7 @@ set(regress_3_tests
   regress3/sixfuncs.sy
   regress3/strings-any-term.sy
   regress3/strings/extf_d_perf.smt2
+  regress3/strings/unsat-circ-reduce.smt2
 )
 
 #-----------------------------------------------------------------------------#

diff --git a/test/regress/regress3/strings/unsat-circ-reduce.smt2 b/test/regress/regress3/strings/unsat-circ-reduce.smt2
new file mode 100644 (file)
index 0000000..b584c0f
--- /dev/null
+++ b/test/regress/regress3/strings/unsat-circ-reduce.smt2
@@ -0,0 +1,13 @@
+; COMMAND-LINE: --strings-exp --no-re-elim
+; EXPECT: unsat
+(set-logic QF_SLIA)
+(set-info :status unsat)
+(declare-fun x () String)
+(assert (not (=                                                                                                                                                     
+(let ((_let_0 (re.* re.allchar ))) 
+(str.in_re x (re.++ re.allchar  _let_0 (str.to_re "AC") _let_0 (str.to_re "CA") _let_0)))                                        
+(let ((_let_0 (+ 0 1))) (let ((_let_1 (str.indexof x "AC" _let_0))) (and (not (= _let_1 (- 1))) (not (= (str.indexof x "CA" (+ _let_1 (str.len "AC"))) (- 1))))))   
+)))        
+(assert (<= (str.len x) 8))
+; adding --strings-fmf to command line above incorrectly said "sat" for this at ad0b69e6
+(check-sat)