Fix extended function decomposition (#2960)

Fixes #2958.

The issue was: we had substr(x,0,2) in R, and the "derivable substitution" modifed this to substr(substr(x,0,2),0,2) in R, since substr(x,0,2) was the representative of x (which is a bad choice, but regardless is legal). Then decomposition inference asked "can i reduce substr(substr(x,0,2),0,2) in R"? It determines substr(substr(x,0,2),0,2) in R rewrites to substr(x,0,2) in R, which is already true. However, substr(x,0,2) in R was what we started with.

The fix makes things much more conservative: we never mark extended functions reduced based on decomposition, since there isnt a strong argument based on an ordering.

diff --git a/src/theory/strings/theory_strings.cpp b/src/theory/strings/theory_strings.cpp
index 6333bfee15a35091479a904949815f523392e2ae..8731bd1a5cc05d13b8574946fc952216de2b105c 100644 (file)
--- a/src/theory/strings/theory_strings.cpp
+++ b/src/theory/strings/theory_strings.cpp
@@ -1705,8 +1705,8 @@ void TheoryStrings::checkExtfEval( int effort ) {
       }
       else
       {
-        bool reduced = false;
-        if (!einfo.d_const.isNull() && nrc.getType().isBoolean())
+        // if this was a predicate which changed after substitution + rewriting
+        if (!einfo.d_const.isNull() && nrc.getType().isBoolean() && nrc != n)
         {
           bool pol = einfo.d_const == d_true;
           Node nrcAssert = pol ? nrc : nrc.negate();
@@ -1716,23 +1716,15 @@ void TheoryStrings::checkExtfEval( int effort ) {
           Trace("strings-extf-debug") << "  decomposable..." << std::endl;
           Trace("strings-extf") << "  resolve extf : " << sn << " -> " << nrc
                                 << ", const = " << einfo.d_const << std::endl;
-          reduced = sendInternalInference(
+          // We send inferences internal here, which may help show unsat.
+          // However, we do not make a determination whether n can be marked
+          // reduced since this argument may be circular: we may infer than n
+          // can be reduced to something else, but that thing may argue that it
+          // can be reduced to n, in theory.
+          sendInternalInference(
               einfo.d_exp, nrcAssert, effort == 0 ? "EXTF_d" : "EXTF_d-N");
-          if (!reduced)
-          {
-            Trace("strings-extf") << "EXT: could not fully reduce ";
-            Trace("strings-extf")
-                << nAssert << " via " << nrcAssert << std::endl;
-          }
-        }
-        if (reduced)
-        {
-          getExtTheory()->markReduced(n);
-        }
-        else
-        {
-          to_reduce = nrc;
         }
+        to_reduce = nrc;
       }
     }else{
       to_reduce = sterms[i];

diff --git a/test/regress/CMakeLists.txt b/test/regress/CMakeLists.txt
index 97ca9a1be8ff2d664a052d15114ef7241712aa9c..25c0e92aa8605b84000a1c5c6f3cca88590a50ab 100644 (file)
--- a/test/regress/CMakeLists.txt
+++ b/test/regress/CMakeLists.txt
@@ -832,6 +832,7 @@ set(regress_0_tests
   regress0/strings/ilc-like.smt2
   regress0/strings/indexof-sym-simp.smt2
   regress0/strings/issue1189.smt2
+  regress0/strings/issue2958.smt2
   regress0/strings/itos-entail.smt2
   regress0/strings/leadingzero001.smt2
   regress0/strings/loop001.smt2

diff --git a/test/regress/regress0/strings/issue2958.smt2 b/test/regress/regress0/strings/issue2958.smt2
new file mode 100644 (file)
index 0000000..7ed5ef7
--- /dev/null
+++ b/test/regress/regress0/strings/issue2958.smt2
@@ -0,0 +1,7 @@
+(set-info :smt-lib-version 2.5)
+(set-logic QF_SLIA)
+(set-info :status unsat)
+(declare-const x String)
+(assert (not (str.prefixof "ab" x)))
+(assert (str.in.re (str.substr x 0 2) (re.++ (str.to.re "ab") (re.* (str.to.re "dcab")))))
+(check-sat)