Do not mark extended functions as reduced based on decomposing contains (#5407)

Fixes #5381.

diff --git a/src/smt/check_models.cpp b/src/smt/check_models.cpp
index a55f53f962ca27cd493281bfa8fdf13660c8a582..612084de2f1adeb19cf38f968369555f9b6658c7 100644 (file)
--- a/src/smt/check_models.cpp
+++ b/src/smt/check_models.cpp
@@ -174,6 +174,7 @@ void CheckModels::checkModel(Model* m,
     Notice() << "SmtEngine::checkModel(): checking assertion " << assertion
              << std::endl;
     Node n = assertion;
+    Notice() << "SmtEngine::checkModel(): -- rewritten form is " << Rewriter::rewrite(n) << std::endl;
     Node nr = Rewriter::rewrite(substitutions.apply(n));
     if (nr.isConst() && nr.getConst<bool>())
     {

diff --git a/src/theory/strings/extf_solver.cpp b/src/theory/strings/extf_solver.cpp
index 53cd92ac238e82030fe07469b24c73f203dce6d8..531b281a75b394ee2dc2090973d51ebd804e602a 100644 (file)
--- a/src/theory/strings/extf_solver.cpp
+++ b/src/theory/strings/extf_solver.cpp
@@ -81,11 +81,13 @@ bool ExtfSolver::doReduction(int effort, Node n)
   if (!d_extfInfoTmp[n].d_modelActive)
   {
     // n is not active in the model, no need to reduce
+  Trace("strings-extf-debug") << "...skip due to model active" << std::endl;
     return false;
   }
   if (d_reduced.find(n)!=d_reduced.end())
   {
     // already sent a reduction lemma
+  Trace("strings-extf-debug") << "...skip due to reduced" << std::endl;
     return false;
   }
   // determine the effort level to process the extf at
@@ -157,6 +159,8 @@ bool ExtfSolver::doReduction(int effort, Node n)
   }
   if (effort != r_effort)
   {
+    
+  Trace("strings-extf-debug") << "...skip due to effort" << std::endl;
     // not the right effort level to reduce
     return false;
   }
@@ -202,6 +206,8 @@ bool ExtfSolver::doReduction(int effort, Node n)
     Trace("strings-red-lemma")
         << "Reduction_" << effort << " lemma : " << nnlem << std::endl;
     Trace("strings-red-lemma") << "...from " << n << std::endl;
+    Trace("strings-red-lemma")
+        << "Reduction_" << effort << " rewritten : " << Rewriter::rewrite(nnlem) << std::endl;
     d_im.sendInference(d_emptyVec, nnlem, Inference::REDUCTION, false, true);
     Trace("strings-extf-debug")
         << "  resolve extf : " << n << " based on reduction." << std::endl;
@@ -625,13 +631,13 @@ void ExtfSolver::checkExtfInference(Node n,
       }
       else
       {
-        // If we already know that s (does not) contain t, then n is redundant.
-        // For example, if str.contains( x, y ), str.contains( z, y ), and x=z
-        // are asserted in the current context, then str.contains( z, y ) is
-        // satisfied by all models of str.contains( x, y ) ^ x=z and thus can
-        // be ignored.
+        // If we already know that s (does not) contain t, then n may be
+        // redundant. However, we do not mark n as reduced here, since strings
+        // reductions may require dependencies between extended functions.
+        // Marking reduced here could lead to incorrect models if an
+        // extended function is marked reduced based on an assignment to
+        // something that depends on n.
         Trace("strings-extf-debug") << "  redundant." << std::endl;
-        d_extt.markReduced(n);
       }
     }
     return;

diff --git a/test/regress/CMakeLists.txt b/test/regress/CMakeLists.txt
index 58a43895e082b94137b2bd0fc95d6ac9ac2c7b16..9a0565d8ea1d2d90bc01ca956be2e0cf61baa918 100644 (file)
--- a/test/regress/CMakeLists.txt
+++ b/test/regress/CMakeLists.txt
@@ -2174,6 +2174,7 @@ set(regress_2_tests
   regress2/strings/cmu-prereg-fmf.smt2
   regress2/strings/cmu-repl-len-nterm.smt2
   regress2/strings/issue3203.smt2
+  regress2/strings/issue5381.smt2
   regress2/strings/issue918.smt2
   regress2/strings/non_termination_regular_expression6.smt2
   regress2/strings/range-perf.smt2

diff --git a/test/regress/regress2/strings/issue5381.smt2 b/test/regress/regress2/strings/issue5381.smt2
new file mode 100644 (file)
index 0000000..6efd22a
--- /dev/null
+++ b/test/regress/regress2/strings/issue5381.smt2
@@ -0,0 +1,30 @@
+; COMMAND-LINE: --strings-fmf --strings-exp
+; EXPECT: sat
+(set-logic QF_SLIA)
+(set-info :status sat)
+; required for solving the benchmark, although the original benchmark only has an error when this is disabled
+(set-option :strings-fmf true)
+(declare-fun a () String)
+(assert (not (= (ite (str.contains (str.++ (str.replace (str.substr
+ (str.substr (str.substr a 1 (- (str.len a) 1)) 0 (- (str.len
+ (str.substr a 1 (- (str.len a) 1))) 0)) 0 (- (+ (str.indexof (str.++
+ (str.replace (str.substr (str.substr a 1 (- (str.len a) 1)) 0 1) "A"
+ "") "") "D" 0) 1) 0)) "" "") (str.substr (str.substr (str.substr a 1
+ (- (str.len a) 1)) 1 (str.len (str.substr a 1 (- (str.len a) 1)))) 0
+ (str.len (str.substr (str.substr a 1 (- (str.len a) 1)) 0 (str.len
+ (str.substr a 1 (- (str.len a) 1))))))) "F") 1 0) 0)))
+(assert (= (ite (str.contains (str.substr (str.substr (str.substr a 1
+ (- (str.len a) 1)) (+ (str.indexof (str.substr a 1 (- (str.len a)
+ 1)) "A" 0) 1) (str.len (str.substr a 1 (- (str.len a) 1)))) 0 (-
+ (str.len (str.substr (str.substr a 1 (- (str.len a) 1)) 0 (str.len
+ (str.substr a 1 (- (str.len a) 1))))) (+ (str.indexof (str.substr
+ (str.substr a 1 (- (str.len a) 1)) 1 (str.len (str.substr a 1 (-
+ (str.len a) 1)))) "D" 0) 1))) "D") 1 0) 0))
+(assert (not (= (ite (str.contains (str.substr (str.substr a 1 (-
+ (str.len a) 1)) 0 (str.len (str.substr a 1 (- (str.len a) 1)))) "D")
+ 1 0) 0)))
+(assert (<= (+ (str.indexof (str.substr (str.substr a 1 (- (str.len a)
+ 1)) (+ (str.indexof (str.substr a 1 (- (str.len a) 1)) "A" 0) 1) (-
+ (str.len (str.substr a 1 (- (str.len a) 1))) 0)) "D" 0) 1) 0))
+(check-sat)
+(exit)