From: Andrew Reynolds Date: Thu, 14 Jan 2021 13:28:55 +0000 (-0600) Subject: Updates to theory preprocess equality (#5776) X-Git-Tag: cvc5-1.0.0~2378 X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=eb6155c5f078a26b7cdddddad6e209fad0f825f8;p=cvc5.git Updates to theory preprocess equality (#5776) This makes 3 changes related to arithmetic preprocessing of equalities which revert to the original behavior of master before a129c57. For background, the commit a129c57 unintentionally changed the default behavior slightly in 3 ways (each corrected in this PR), which led a performance regression on QF_LIA in current master. The 3 fixes are: (1) Rewrite equalities should be applied as a post-rewrite, not a pre-rewrite in the theory-rewrite-eq preprocessing pass. This is particularly important for equalities between ITE terms that contain other equalities recursively. (2) theory-rewrite-eq should apply after rewriting and just before the normal theory preprocessing. (3) The arith-brab test should call ppRewrite on the arithmetic equality it introduces, as it has a choice of whether to eliminate the equality before the lemma is sent out. --- diff --git a/src/preprocessing/passes/theory_rewrite_eq.cpp b/src/preprocessing/passes/theory_rewrite_eq.cpp index 190b33684..68de75194 100644 --- a/src/preprocessing/passes/theory_rewrite_eq.cpp +++ b/src/preprocessing/passes/theory_rewrite_eq.cpp @@ -59,13 +59,9 @@ theory::TrustNode TheoryRewriteEq::rewriteAssertion(TNode n) if (it == visited.end()) { - // don't consider Boolean equality - if (cur.getKind() == kind::EQUAL && !cur[0].getType().isBoolean()) + if (cur.getNumChildren()==0) { - // For example, (= x y) ---> (and (>= x y) (<= x y)) - theory::TrustNode trn = te->ppRewriteEquality(cur); - // can make proof producing by using proof generator from trn - visited[cur] = trn.isNull() ? Node(cur) : trn.getNode(); + visited[cur] = cur; } else { @@ -95,6 +91,13 @@ theory::TrustNode TheoryRewriteEq::rewriteAssertion(TNode n) { ret = nm->mkNode(cur.getKind(), children); } + if (ret.getKind() == kind::EQUAL && !ret[0].getType().isBoolean()) + { + // For example, (= x y) ---> (and (>= x y) (<= x y)) + theory::TrustNode trn = te->ppRewriteEquality(ret); + // can make proof producing by using proof generator from trn + ret = trn.isNull() ? Node(ret) : trn.getNode(); + } visited[cur] = ret; } } while (!visit.empty()); diff --git a/src/smt/process_assertions.cpp b/src/smt/process_assertions.cpp index 0bbc2eeae..6d6c81e3c 100644 --- a/src/smt/process_assertions.cpp +++ b/src/smt/process_assertions.cpp @@ -317,10 +317,7 @@ bool ProcessAssertions::apply(Assertions& as) { d_passes["ho-elim"]->apply(&assertions); } - - // rewrite equalities based on theory-specific rewriting - d_passes["theory-rewrite-eq"]->apply(&assertions); - + // begin: INVARIANT to maintain: no reordering of assertions or // introducing new ones @@ -332,6 +329,8 @@ bool ProcessAssertions::apply(Assertions& as) // ensure rewritten d_passes["rewrite"]->apply(&assertions); + // rewrite equalities based on theory-specific rewriting + d_passes["theory-rewrite-eq"]->apply(&assertions); // apply theory preprocess, which includes ITE removal d_passes["theory-preprocess"]->apply(&assertions); // This is needed because when solving incrementally, removeITEs may diff --git a/src/theory/arith/theory_arith_private.cpp b/src/theory/arith/theory_arith_private.cpp index d1068c6ac..7b0096f30 100644 --- a/src/theory/arith/theory_arith_private.cpp +++ b/src/theory/arith/theory_arith_private.cpp @@ -3694,6 +3694,13 @@ Node TheoryArithPrivate::branchIntegerVariable(ArithVar x) const { lem = nm->mkNode(kind::OR, ub, lb); Node eq = Rewriter::rewrite( nm->mkNode(kind::EQUAL, var, mkRationalNode(nearest))); + // Also preprocess it before we send it out. This is important since + // arithmetic may prefer eliminating equalities. + if (Theory::theoryOf(eq) == THEORY_ARITH) + { + TrustNode teq = d_containing.ppRewrite(eq); + eq = teq.isNull() ? eq : teq.getNode(); + } Node literal = d_containing.getValuation().ensureLiteral(eq); d_containing.getOutputChannel().requirePhase(literal, true); lem = nm->mkNode(kind::OR, literal, lem); diff --git a/src/theory/engine_output_channel.cpp b/src/theory/engine_output_channel.cpp index cb346d02d..0aa56a381 100644 --- a/src/theory/engine_output_channel.cpp +++ b/src/theory/engine_output_channel.cpp @@ -69,7 +69,7 @@ void EngineOutputChannel::safePoint(ResourceManager::Resource r) theory::LemmaStatus EngineOutputChannel::lemma(TNode lemma, LemmaProperty p) { - Debug("theory::lemma") << "EngineOutputChannel<" << d_theory << ">::lemma(" + Trace("theory::lemma") << "EngineOutputChannel<" << d_theory << ">::lemma(" << lemma << ")" << ", properties = " << p << std::endl; ++d_statistics.lemmas; @@ -86,12 +86,12 @@ theory::LemmaStatus EngineOutputChannel::lemma(TNode lemma, LemmaProperty p) theory::LemmaStatus EngineOutputChannel::splitLemma(TNode lemma, bool removable) { - Debug("theory::lemma") << "EngineOutputChannel<" << d_theory << ">::lemma(" + Trace("theory::lemma") << "EngineOutputChannel<" << d_theory << ">::lemma(" << lemma << ")" << std::endl; ++d_statistics.lemmas; d_engine->d_outputChannelUsed = true; - Debug("pf::explain") << "EngineOutputChannel::splitLemma( " << lemma << " )" + Trace("pf::explain") << "EngineOutputChannel::splitLemma( " << lemma << " )" << std::endl; TrustNode tlem = TrustNode::mkTrustLemma(lemma); LemmaProperty p = removable ? LemmaProperty::REMOVABLE : LemmaProperty::NONE; @@ -101,7 +101,7 @@ theory::LemmaStatus EngineOutputChannel::splitLemma(TNode lemma, bool removable) bool EngineOutputChannel::propagate(TNode literal) { - Debug("theory::propagate") << "EngineOutputChannel<" << d_theory + Trace("theory::propagate") << "EngineOutputChannel<" << d_theory << ">::propagate(" << literal << ")" << std::endl; ++d_statistics.propagations; d_engine->d_outputChannelUsed = true; @@ -134,7 +134,7 @@ void EngineOutputChannel::demandRestart() void EngineOutputChannel::requirePhase(TNode n, bool phase) { - Debug("theory") << "EngineOutputChannel::requirePhase(" << n << ", " << phase + Trace("theory") << "EngineOutputChannel::requirePhase(" << n << ", " << phase << ")" << std::endl; ++d_statistics.requirePhase; d_engine->getPropEngine()->requirePhase(n, phase); @@ -174,7 +174,7 @@ void EngineOutputChannel::trustedConflict(TrustNode pconf) LemmaStatus EngineOutputChannel::trustedLemma(TrustNode plem, LemmaProperty p) { - Debug("theory::lemma") << "EngineOutputChannel<" << d_theory + Trace("theory::lemma") << "EngineOutputChannel<" << d_theory << ">::trustedLemma(" << plem << ")" << std::endl; Assert(plem.getKind() == TrustNodeKind::LEMMA); if (plem.getGenerator() != nullptr)