diff options
author | Andrew Reynolds <andrew.j.reynolds@gmail.com> | 2019-08-23 17:27:05 -0500 |
---|---|---|
committer | GitHub <noreply@github.com> | 2019-08-23 17:27:05 -0500 |
commit | 0faead1572109c1d7cb3d67647da02d0b4600a20 (patch) | |
tree | e0bd28feb049be6a36a63fd73df37f9d3cc7aa54 /src/theory/strings | |
parent | eaf29fee0871f1b7a8c9cc7c208c6b6d5570bae5 (diff) |
Infer emptiness instead of splitting when a string equality rewrites to a constant (#3218)
Diffstat (limited to 'src/theory/strings')
-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 |
4 files changed, 42 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 |