diff options
| author | Andres Noetzli <andres.noetzli@gmail.com> | 2019-03-12 22:48:21 -0700 |
|---|---|---|
| committer | Andres Noetzli <andres.noetzli@gmail.com> | 2019-03-12 22:48:21 -0700 |
| commit | ea1f76a2c9fc700aab017526a6232d6b03ed3194 (patch) | |
| tree | dabd97554425460cbaa02781d73fbd1a506bd62e | |
| parent | c8192051f922747280239d95b713777897af92bf (diff) | |
less aggressiverewInfer
| -rw-r--r-- | src/theory/strings/theory_strings.cpp | 39 |
1 files changed, 19 insertions, 20 deletions
diff --git a/src/theory/strings/theory_strings.cpp b/src/theory/strings/theory_strings.cpp index 3db8f39bb..d643fac70 100644 --- a/src/theory/strings/theory_strings.cpp +++ b/src/theory/strings/theory_strings.cpp @@ -2847,28 +2847,27 @@ void TheoryStrings::processNEqc( std::vector< std::vector< Node > > &normal_form EQUAL, TheoryStringsRewriter::mkConcat(STRING_CONCAT, normal_forms[i]), TheoryStringsRewriter::mkConcat(STRING_CONCAT, normal_forms[j])); - Node eqr = TheoryStringsRewriter::rewriteEqualityExt(eq); - if (eq != eqr) + eq = Rewriter::rewrite(eq); + if (eq.getKind() == EQUAL) { - eqr = Rewriter::rewrite(eqr); - std::vector<Node> antec; - getExplanationVectorForPrefixEq(normal_forms, - normal_form_src, - normal_forms_exp, - normal_forms_exp_depend, - i, - j, - -1, - -1, - false, - antec); - //antec.push_back(eq); - - if (getExtTheory()->isActive(eq)) { - getExtTheory()->markReduced(eq); + Node eqr = TheoryStringsRewriter::rewriteEqualityExt(eq); + if (eq != eqr) + { + eqr = Rewriter::rewrite(eqr); + std::vector<Node> antec; + getExplanationVectorForPrefixEq(normal_forms, + normal_form_src, + normal_forms_exp, + normal_forms_exp_depend, + i, + j, + -1, + -1, + false, + antec); + + sendInternalInference(antec, eqr, "__equality_rew"); } - sendInference(antec, eqr, "__equality_rew"); - return; } //process the reverse direction first (check for easy conflicts and inferences) |