Infer emptiness instead of splitting when a string equality rewrites to a constant...

diff --git a/src/theory/strings/infer_info.cpp b/src/theory/strings/infer_info.cpp
index a20f608a66d0262d1eb83a0915203c2d4e0c354e..b2c88d06871a8dfc254c30dd7926786329b21122 100644 (file)
--- a/src/theory/strings/infer_info.cpp
+++ b/src/theory/strings/infer_info.cpp
@@ -24,6 +24,7 @@ std::ostream& operator<<(std::ostream& out, Inference i)
 {
   switch (i)
   {
+    case INFER_INFER_EMP: out << "Infer-Emp"; break;
     case INFER_SSPLIT_CST_PROP: out << "S-Split(CST-P)-prop"; break;
     case INFER_SSPLIT_VAR_PROP: out << "S-Split(VAR)-prop"; break;
     case INFER_LEN_SPLIT: out << "Len-Split(Len)"; break;

diff --git a/src/theory/strings/infer_info.h b/src/theory/strings/infer_info.h
index 9b19eba4bf9c621f3359f9d16826c0d864049b50..745a499d3f122dd8e37e04bb28df8b3157c492fd 100644 (file)
--- a/src/theory/strings/infer_info.h
+++ b/src/theory/strings/infer_info.h
@@ -33,10 +33,17 @@ namespace strings {
 enum Inference
 {
   INFER_NONE = 0,
+  // infer empty, for example:
+  //     (~) x = ""
+  // This is inferred when we encounter an x such that x = "" rewrites to a
+  // constant. This inference is used for instance when we otherwise would have
+  // split on the emptiness of x but the rewriter tells us the emptiness of x
+  // can be inferred.
+  INFER_INFER_EMP = 1,
   // string split constant propagation, for example:
   //     x = y, x = "abc", y = y1 ++ "b" ++ y2
   //       implies y1 = "a" ++ y1'
-  INFER_SSPLIT_CST_PROP = 1,
+  INFER_SSPLIT_CST_PROP,
   // string split variable propagation, for example:
   //     x = y, x = x1 ++ x2, y = y1 ++ y2, len( x1 ) >= len( y1 )
   //       implies x1 = y1 ++ x1'

diff --git a/src/theory/strings/inference_manager.cpp b/src/theory/strings/inference_manager.cpp
index f064a26e2b7554943bb96c49561cbedf7bc9ba6b..6cc1e7b44abcfa0ad33640187f2105d213b21c3c 100644 (file)
--- a/src/theory/strings/inference_manager.cpp
+++ b/src/theory/strings/inference_manager.cpp
@@ -106,10 +106,6 @@ void InferenceManager::sendInference(const std::vector<Node>& exp,
                                      bool asLemma)
 {
   eq = eq.isNull() ? d_false : Rewriter::rewrite(eq);
-  if (eq == d_true)
-  {
-    return;
-  }
   if (Trace.isOn("strings-infer-debug"))
   {
     Trace("strings-infer-debug")
@@ -123,6 +119,10 @@ void InferenceManager::sendInference(const std::vector<Node>& exp,
       Trace("strings-infer-debug") << "  N:" << exp_n[i] << std::endl;
     }
   }
+  if (eq == d_true)
+  {
+    return;
+  }
   // check if we should send a lemma or an inference
   if (asLemma || eq == d_false || eq.getKind() == OR || !exp_n.empty()
       || options::stringInferAsLemmas())

diff --git a/src/theory/strings/theory_strings.cpp b/src/theory/strings/theory_strings.cpp
index 1eb2e8e008708287fed16cc9d67973ece22c9c65..2f51000abc6f2ffde6c89dbb10a5ee0d003f9c87 100644 (file)
--- a/src/theory/strings/theory_strings.cpp
+++ b/src/theory/strings/theory_strings.cpp
@@ -3160,8 +3160,9 @@ void TheoryStrings::processNEqc(std::vector<NormalForm>& normal_forms)
   unsigned max_index = 0;
   for (unsigned i = 0, size = pinfer.size(); i < size; i++)
   {
-    Trace("strings-solve") << "From " << pinfer[i].d_i << " / " << pinfer[i].d_j
-                           << " (rev=" << pinfer[i].d_rev << ") : ";
+    Trace("strings-solve") << "#" << i << ": From " << pinfer[i].d_i << " / "
+                           << pinfer[i].d_j << " (rev=" << pinfer[i].d_rev
+                           << ") : ";
     Trace("strings-solve") << pinfer[i].d_conc << " by " << pinfer[i].d_id
                            << std::endl;
     if (!set_use_index || pinfer[i].d_id < min_id
@@ -3173,6 +3174,7 @@ void TheoryStrings::processNEqc(std::vector<NormalForm>& normal_forms)
       set_use_index = true;
     }
   }
+  Trace("strings-solve") << "...choose #" << use_index << std::endl;
   doInferInfo(pinfer[use_index]);
 }
 
@@ -3400,9 +3402,32 @@ void TheoryStrings::processSimpleNEq(NormalForm& nfi,
                 Assert( other_str.getKind()!=kind::STRING_CONCAT, "Other string is not CONCAT." );
                 if( !d_equalityEngine.areDisequal( other_str, d_emptyString, true ) ){
                   Node eq = other_str.eqNode( d_emptyString );
+                  eq = Rewriter::rewrite(eq);
+                  if (eq.isConst())
+                  {
+                    // If the equality rewrites to a constant, we must use the
+                    // purify variable for this string to communicate that
+                    // we have inferred whether it is empty.
+                    Node p = d_sk_cache.mkSkolemCached(
+                        other_str, SkolemCache::SK_PURIFY, "lsym");
+                    Node pEq = p.eqNode(d_emptyString);
+                    // should not be constant
+                    Assert(!Rewriter::rewrite(pEq).isConst());
+                    // infer the purification equality, and the (dis)equality
+                    // with the empty string in the direction that the rewriter
+                    // inferred
+                    info.d_conc =
+                        nm->mkNode(AND,
+                                   p.eqNode(other_str),
+                                   !eq.getConst<bool>() ? pEq.negate() : pEq);
+                    info.d_id = INFER_INFER_EMP;
+                  }
+                  else
+                  {
+                    info.d_conc = nm->mkNode(OR, eq, eq.negate());
+                    info.d_id = INFER_LEN_SPLIT_EMP;
+                  }
                   //set info
-                  info.d_conc = NodeManager::currentNM()->mkNode( kind::OR, eq, eq.negate() );
-                  info.d_id = INFER_LEN_SPLIT_EMP;
                   info_valid = true;
                 }else{
                   if( !isRev ){  //FIXME

diff --git a/test/regress/CMakeLists.txt b/test/regress/CMakeLists.txt
index e3287983c62ae785437392bfa4f4fd45aa3ec99e..80b7c33bf3ee84d99d2265e71c6d45cabdb88b7e 100644 (file)
--- a/test/regress/CMakeLists.txt
+++ b/test/regress/CMakeLists.txt
@@ -1572,6 +1572,7 @@ set(regress_1_tests
   regress1/strings/issue2981.smt2
   regress1/strings/issue2982.smt2
   regress1/strings/issue3090.smt2
+  regress1/strings/issue3217.smt2
   regress1/strings/kaluza-fl.smt2
   regress1/strings/loop002.smt2
   regress1/strings/loop003.smt2

diff --git a/test/regress/regress1/strings/issue3217.smt2 b/test/regress/regress1/strings/issue3217.smt2
new file mode 100644 (file)
index 0000000..4fd3599
--- /dev/null
+++ b/test/regress/regress1/strings/issue3217.smt2
@@ -0,0 +1,13 @@
+(set-logic ALL_SUPPORTED)
+(set-option :strings-exp true)
+(set-info :status unsat)
+(declare-fun a () String)
+(declare-fun b () String)
+(declare-fun c () String)
+(declare-fun d () String)
+(assert 
+    (or 
+        (not (= ( str.suffixof "B" ( str.replace "A" b "B")) (= ( str.substr a 0 (str.len b)) "A"))) 
+        (not (= (not (= c "A")) ( str.suffixof "A" ( str.replace "A" c "B"))))))
+(assert (= a (str.++ (str.++ b "") d)))
+(check-sat)