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).

3 files changed, 25 insertions, 3 deletions

diff --git a/src/theory/strings/extf_solver.cpp b/src/theory/strings/extf_solver.cpp
index 55985406e..dd4144313 100644
--- 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 656bb5880..38b741ced 100644
--- 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
index 000000000..b584c0fb1
--- /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)