From: Guy Date: Fri, 15 Apr 2016 22:34:52 +0000 (-0700) Subject: Rolling back the rewrite code X-Git-Tag: cvc5-1.0.0~6049^2~65 X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=b53cb991585cf894eedd4600b2d4c79c27850a1b;p=cvc5.git Rolling back the rewrite code --- diff --git a/src/theory/arrays/theory_arrays.cpp b/src/theory/arrays/theory_arrays.cpp index 4d7fcff92..6add1b55f 100644 --- a/src/theory/arrays/theory_arrays.cpp +++ b/src/theory/arrays/theory_arrays.cpp @@ -2058,19 +2058,57 @@ void TheoryArrays::queueRowLemma(RowLemmaType lem) // TODO: maybe add triggers here if ((options::arraysEagerLemmas() || bothExist) && !d_proofsEnabled) { + // Make sure that any terms introduced by rewriting are appropriately stored in the equality database + Node aj2 = Rewriter::rewrite(aj); + if (aj != aj2) { + if (!ajExists) { + preRegisterTermInternal(aj); + } + if (!d_equalityEngine.hasTerm(aj2)) { + preRegisterTermInternal(aj2); + } + d_equalityEngine.assertEquality(aj.eqNode(aj2), true, d_true); + } + Node bj2 = Rewriter::rewrite(bj); + if (bj != bj2) { + if (!bjExists) { + preRegisterTermInternal(bj); + } + if (!d_equalityEngine.hasTerm(bj2)) { + preRegisterTermInternal(bj2); + } + d_equalityEngine.assertEquality(bj.eqNode(bj2), true, d_true); + } + if (aj2 == bj2) { + return; + } - if (!ajExists) { - preRegisterTermInternal(aj); + // construct lemma + Node eq1 = aj2.eqNode(bj2); + Node eq1_r = Rewriter::rewrite(eq1); + if (eq1_r == d_true) { + if (!d_equalityEngine.hasTerm(aj2)) { + preRegisterTermInternal(aj2); + } + if (!d_equalityEngine.hasTerm(bj2)) { + preRegisterTermInternal(bj2); + } + d_equalityEngine.assertEquality(eq1, true, d_true); + return; } - if (!bjExists) { - preRegisterTermInternal(bj); + + Node eq2 = i.eqNode(j); + Node eq2_r = Rewriter::rewrite(eq2); + if (eq2_r == d_true) { + d_equalityEngine.assertEquality(eq2, true, d_true); + return; } - Node lemma = nm->mkNode(kind::OR, i.eqNode(j), aj.eqNode(bj)); + Node lemma = nm->mkNode(kind::OR, eq2_r, eq1_r); Trace("arrays-lem")<<"Arrays::addRowLemma adding "<lemma(lemma, RULE_INVALID, false, false, true); + d_out->lemma(lemma); ++d_numRow; } else { @@ -2129,18 +2167,58 @@ bool TheoryArrays::dischargeLemmas() } } - if (!ajExists) { - preRegisterTermInternal(aj); + // Make sure that any terms introduced by rewriting are appropriately stored in the equality database + Node aj2 = Rewriter::rewrite(aj); + if (aj != aj2) { + if (!ajExists) { + preRegisterTermInternal(aj); + } + if (!d_equalityEngine.hasTerm(aj2)) { + preRegisterTermInternal(aj2); + } + d_equalityEngine.assertEquality(aj.eqNode(aj2), true, d_true); + } + Node bj2 = Rewriter::rewrite(bj); + if (bj != bj2) { + if (!bjExists) { + preRegisterTermInternal(bj); + } + if (!d_equalityEngine.hasTerm(bj2)) { + preRegisterTermInternal(bj2); + } + d_equalityEngine.assertEquality(bj.eqNode(bj2), true, d_true); + + } + if (aj2 == bj2) { + continue; + } + + // construct lemma + Node eq1 = aj2.eqNode(bj2); + Node eq1_r = Rewriter::rewrite(eq1); + if (eq1_r == d_true) { + if (!d_equalityEngine.hasTerm(aj2)) { + preRegisterTermInternal(aj2); + } + if (!d_equalityEngine.hasTerm(bj2)) { + preRegisterTermInternal(bj2); + } + d_equalityEngine.assertEquality(eq1, true, d_true); + continue; } - if (!bjExists) { - preRegisterTermInternal(bj); + + Node eq2 = i.eqNode(j); + Node eq2_r = Rewriter::rewrite(eq2); + if (eq2_r == d_true) { + d_equalityEngine.assertEquality(eq2, true, d_true); + continue; } - Node lem = nm->mkNode(kind::OR, i.eqNode(j), aj.eqNode(bj)); + Node lem = nm->mkNode(kind::OR, eq2_r, eq1_r); Trace("arrays-lem")<<"Arrays::addRowLemma adding "<lemma(lem, RULE_INVALID, false, false, true); + d_out->lemma(lem); ++d_numRow; lemmasAdded = true; if (options::arraysReduceSharing()) {