diff options
| -rw-r--r-- | src/theory/strings/infer_info.cpp | 1 | ||||
| -rw-r--r-- | src/theory/strings/infer_info.h | 9 | ||||
| -rw-r--r-- | src/theory/strings/inference_manager.cpp | 8 | ||||
| -rw-r--r-- | src/theory/strings/theory_strings.cpp | 33 | ||||
| -rw-r--r-- | test/regress/CMakeLists.txt | 1 | ||||
| -rw-r--r-- | test/regress/regress1/strings/issue3217.smt2 | 13 |
6 files changed, 56 insertions, 9 deletions
diff --git a/src/theory/strings/infer_info.cpp b/src/theory/strings/infer_info.cpp index a20f608a6..b2c88d068 100644 --- 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 9b19eba4b..745a499d3 100644 --- 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 f064a26e2..6cc1e7b44 100644 --- 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 1eb2e8e00..2f51000ab 100644 --- 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 e3287983c..80b7c33bf 100644 --- 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 index 000000000..4fd35999d --- /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) |