From: Andrew Reynolds Date: Tue, 22 Dec 2020 14:24:24 +0000 (-0600) Subject: Make theory preprocess rewrite equalities a preprocessing pass (#5711) X-Git-Tag: cvc5-1.0.0~2411 X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=a129c57;p=cvc5.git Make theory preprocess rewrite equalities a preprocessing pass (#5711) Some theories rewrite equalities during ppRewrite. An example is arithmetic with the option arith-rewrite-eq, which rewrites (= x y) to (and (>= x y) (<= x y)) during theory preprocessing. This PR makes it so that ppRewrite is only called on equalities in preprocessing, during a new preprocessing pass "TheoryRewriteEq". On the other hand, ppRewrite is never called on new equalities generated in lemmas from TheoryEngine. In detail, the motivation for this change: (1) Rewriting equalities during ppRewrite is dangerous since it may break invariants wrt theory combination. In particular, equalities in splitting lemmas originating from theory combination must not be theory-preprocessed, or else we may be non-terminating or solution unsound. This can happen if a theory requests a split on (= x y) but is not notified of this atom when another theory rewrites (= x y) during ppRewrite. (2) After this PR, we can simplify our policy for all lemmas generated, in particular, we can say that all lemmas must be theory preprocessed before their literals are asserted to TheoryEngine. This is now possible as the invariant cannot be broken (theoryRewriteEq is relegated to the preprocessor, which is only applied once). This will make LemmaProperty::PREPROCESS obsolete, which in turn will simplify several lemma caches for nonlinear and quantifiers. It will also significantly simplify proof production for the theory preprocessor (which maintains two stacks of utilities for preprocessed vs non-preprocessed lemmas). (3) Simplifications to the above policy will make it significantly easier to implement theory-preprocessing apply when literals are asserted. It is currently not possible to implement this in a coherent way without tracking which literals were a part of lemmas marked as "do not theory-preprocess". --- diff --git a/src/CMakeLists.txt b/src/CMakeLists.txt index 82e88f330..0fb505823 100644 --- a/src/CMakeLists.txt +++ b/src/CMakeLists.txt @@ -108,6 +108,8 @@ libcvc4_add_sources( preprocessing/passes/synth_rew_rules.h preprocessing/passes/theory_preprocess.cpp preprocessing/passes/theory_preprocess.h + preprocessing/passes/theory_rewrite_eq.cpp + preprocessing/passes/theory_rewrite_eq.h preprocessing/passes/unconstrained_simplifier.cpp preprocessing/passes/unconstrained_simplifier.h preprocessing/preprocessing_pass.cpp diff --git a/src/preprocessing/passes/theory_rewrite_eq.cpp b/src/preprocessing/passes/theory_rewrite_eq.cpp new file mode 100644 index 000000000..68006b67f --- /dev/null +++ b/src/preprocessing/passes/theory_rewrite_eq.cpp @@ -0,0 +1,113 @@ +/********************* */ +/*! \file theory_rewrite_eq.cpp + ** \verbatim + ** Top contributors (to current version): + ** Andrew Reynolds + ** This file is part of the CVC4 project. + ** Copyright (c) 2009-2020 by the authors listed in the file AUTHORS + ** in the top-level source directory and their institutional affiliations. + ** All rights reserved. See the file COPYING in the top-level source + ** directory for licensing information.\endverbatim + ** + ** \brief The TheoryRewriteEq preprocessing pass + **/ + +#include "preprocessing/passes/theory_rewrite_eq.h" + +#include "theory/theory_engine.h" + +using namespace CVC4::theory; + +namespace CVC4 { +namespace preprocessing { +namespace passes { + +TheoryRewriteEq::TheoryRewriteEq(PreprocessingPassContext* preprocContext) + : PreprocessingPass(preprocContext, "theory-rewrite-eq"){}; + +PreprocessingPassResult TheoryRewriteEq::applyInternal( + AssertionPipeline* assertions) +{ + // apply ppRewrite to all equalities in assertions + for (std::size_t i = 0, size = assertions->size(); i < size; ++i) + { + Node assertion = (*assertions)[i]; + TrustNode trn = rewriteAssertion(assertion); + if (!trn.isNull()) + { + // replace based on the trust node + assertions->replaceTrusted(i, trn); + } + } + return PreprocessingPassResult::NO_CONFLICT; +} + +theory::TrustNode TheoryRewriteEq::rewriteAssertion(TNode n) +{ + NodeManager* nm = NodeManager::currentNM(); + TheoryEngine* te = d_preprocContext->getTheoryEngine(); + std::unordered_map visited; + std::unordered_map::iterator it; + std::vector visit; + TNode cur; + visit.push_back(n); + do + { + cur = visit.back(); + visit.pop_back(); + it = visited.find(cur); + + if (it == visited.end()) + { + if (cur.getKind() == kind::EQUAL) + { + // 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(); + } + else + { + visited[cur] = Node::null(); + visit.push_back(cur); + visit.insert(visit.end(), cur.begin(), cur.end()); + } + } + else if (it->second.isNull()) + { + Node ret = cur; + bool childChanged = false; + std::vector children; + if (cur.getMetaKind() == kind::metakind::PARAMETERIZED) + { + children.push_back(cur.getOperator()); + } + for (const Node& cn : cur) + { + it = visited.find(cn); + Assert(it != visited.end()); + Assert(!it->second.isNull()); + childChanged = childChanged || cn != it->second; + children.push_back(it->second); + } + if (childChanged) + { + ret = nm->mkNode(cur.getKind(), children); + } + visited[cur] = ret; + } + } while (!visit.empty()); + Assert(visited.find(n) != visited.end()); + Assert(!visited.find(n)->second.isNull()); + Node ret = visited[n]; + if (ret == n) + { + return TrustNode::null(); + } + // can make proof producing by providing a term conversion generator here + return TrustNode::mkTrustRewrite(n, ret, nullptr); +} + +} // namespace passes +} // namespace preprocessing +} // namespace CVC4 diff --git a/src/preprocessing/passes/theory_rewrite_eq.h b/src/preprocessing/passes/theory_rewrite_eq.h new file mode 100644 index 000000000..bc4027310 --- /dev/null +++ b/src/preprocessing/passes/theory_rewrite_eq.h @@ -0,0 +1,56 @@ +/********************* */ +/*! \file theory_rewrite_eq.h + ** \verbatim + ** Top contributors (to current version): + ** Andrew Reynolds + ** This file is part of the CVC4 project. + ** Copyright (c) 2009-2020 by the authors listed in the file AUTHORS + ** in the top-level source directory and their institutional affiliations. + ** All rights reserved. See the file COPYING in the top-level source + ** directory for licensing information.\endverbatim + ** + ** \brief The TheoryRewriteEq preprocessing pass + **/ + +#include "cvc4_private.h" + +#ifndef CVC4__PREPROCESSING__PASSES__THEORY_REWRITE_EQ_H +#define CVC4__PREPROCESSING__PASSES__THEORY_REWRITE_EQ_H + +#include "preprocessing/preprocessing_pass.h" +#include "preprocessing/preprocessing_pass_context.h" +#include "theory/trust_node.h" + +namespace CVC4 { +namespace preprocessing { +namespace passes { + +/** + * Implements the preprocessing pass for called ppRewrite on all equalities + * in the input. This is required to be a preprocessing pass since it is not + * recommended that ppRewrite is called on equalities generated in lemmas (e.g. + * it may interfere with equality splitting in theory combination). + */ +class TheoryRewriteEq : public PreprocessingPass +{ + public: + TheoryRewriteEq(PreprocessingPassContext* preprocContext); + + protected: + PreprocessingPassResult applyInternal( + AssertionPipeline* assertionsToPreprocess) override; + /** + * Rewrite the assertion based on rewriting equalities based on theory + * specific rewriting. + * An example is removing arithmetic equalities via: + * (= x y) ---> (and (>= x y) (<= x y)) + * Returns the trust node corresponding to the rewrite. + */ + theory::TrustNode rewriteAssertion(TNode assertion); +}; + +} // namespace passes +} // namespace preprocessing +} // namespace CVC4 + +#endif /* CVC4__PREPROCESSING__PASSES__THEORY_REWRITE_EQ_H */ diff --git a/src/preprocessing/preprocessing_pass_registry.cpp b/src/preprocessing/preprocessing_pass_registry.cpp index 46c1fff68..b21d4e30c 100644 --- a/src/preprocessing/preprocessing_pass_registry.cpp +++ b/src/preprocessing/preprocessing_pass_registry.cpp @@ -53,6 +53,7 @@ #include "preprocessing/passes/sygus_inference.h" #include "preprocessing/passes/synth_rew_rules.h" #include "preprocessing/passes/theory_preprocess.h" +#include "preprocessing/passes/theory_rewrite_eq.h" #include "preprocessing/passes/unconstrained_simplifier.h" #include "preprocessing/preprocessing_pass.h" @@ -149,6 +150,7 @@ PreprocessingPassRegistry::PreprocessingPassRegistry() registerPassInfo("bool-to-bv", callCtor); registerPassInfo("ho-elim", callCtor); registerPassInfo("fun-def-fmf", callCtor); + registerPassInfo("theory-rewrite-eq", callCtor); } } // namespace preprocessing diff --git a/src/smt/process_assertions.cpp b/src/smt/process_assertions.cpp index 8b9b0a53c..7fd1db797 100644 --- a/src/smt/process_assertions.cpp +++ b/src/smt/process_assertions.cpp @@ -317,6 +317,9 @@ 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 diff --git a/src/theory/arith/theory_arith.cpp b/src/theory/arith/theory_arith.cpp index d1dd4bb63..7437ce223 100644 --- a/src/theory/arith/theory_arith.cpp +++ b/src/theory/arith/theory_arith.cpp @@ -112,8 +112,9 @@ TrustNode TheoryArith::ppRewrite(TNode atom) if (options::arithRewriteEq()) { - if (atom.getKind() == kind::EQUAL && atom[0].getType().isReal()) + if (atom.getKind() == kind::EQUAL) { + Assert(atom[0].getType().isReal()); Node leq = NodeBuilder<2>(kind::LEQ) << atom[0] << atom[1]; Node geq = NodeBuilder<2>(kind::GEQ) << atom[0] << atom[1]; TrustNode tleq = ppRewriteTerms(leq); @@ -138,10 +139,7 @@ TrustNode TheoryArith::ppRewrite(TNode atom) TrustNode TheoryArith::ppRewriteTerms(TNode n) { - if (Theory::theoryOf(n) != THEORY_ARITH) - { - return TrustNode::null(); - } + Assert(Theory::theoryOf(n) == THEORY_ARITH); // Eliminate operators recursively. Notice we must do this here since other // theories may generate lemmas that involve non-standard operators. For // example, quantifier instantiation may use TO_INTEGER terms; SyGuS may diff --git a/src/theory/theory.h b/src/theory/theory.h index 6256360e4..a9783c19c 100644 --- a/src/theory/theory.h +++ b/src/theory/theory.h @@ -721,15 +721,20 @@ class Theory { TrustSubstitutionMap& outSubstitutions); /** - * Given an atom of the theory coming from the input formula, this - * method can be overridden in a theory implementation to rewrite - * the atom into an equivalent form. This is only called just - * before an input atom to the engine. This method returns a TrustNode of - * kind TrustNodeKind::REWRITE, which carries information about the proof - * generator for the rewrite. Similarly to expandDefinition, this method may - * return the null TrustNode if atom is unchanged. - */ - virtual TrustNode ppRewrite(TNode atom) { return TrustNode::null(); } + * Given a term of the theory coming from the input formula or + * from a lemma generated during solving, this method can be overridden in a + * theory implementation to rewrite the term into an equivalent form. + * + * This method returns a TrustNode of kind TrustNodeKind::REWRITE, which + * carries information about the proof generator for the rewrite, which can + * be the null TrustNode if n is unchanged. + * + * Notice this method is used both in the "theory rewrite equalities" + * preprocessing pass, where n is an equality from the input formula, + * and in theory preprocessing, where n is a (non-equality) term occurring + * in the input or generated in a lemma. + */ + virtual TrustNode ppRewrite(TNode n) { return TrustNode::null(); } /** * Notify preprocessed assertions. Called on new assertions after diff --git a/src/theory/theory_engine.cpp b/src/theory/theory_engine.cpp index 941d900d3..5206ed7ae 100644 --- a/src/theory/theory_engine.cpp +++ b/src/theory/theory_engine.cpp @@ -852,6 +852,12 @@ theory::Theory::PPAssertStatus TheoryEngine::solve( return solveStatus; } +theory::TrustNode TheoryEngine::ppRewriteEquality(TNode eq) +{ + Assert(eq.getKind() == kind::EQUAL); + return theoryOf(eq)->ppRewrite(eq); +} + void TheoryEngine::notifyPreprocessedAssertions( const std::vector& assertions) { // call all the theories diff --git a/src/theory/theory_engine.h b/src/theory/theory_engine.h index bade5a206..41f8372a9 100644 --- a/src/theory/theory_engine.h +++ b/src/theory/theory_engine.h @@ -439,7 +439,11 @@ class TheoryEngine { bool isProofEnabled() const; public: - + /** + * Preprocess rewrite equality, called by the preprocessor to rewrite + * equalities appearing in the input. + */ + theory::TrustNode ppRewriteEquality(TNode eq); /** Notify (preprocessed) assertions. */ void notifyPreprocessedAssertions(const std::vector& assertions); diff --git a/src/theory/theory_preprocessor.cpp b/src/theory/theory_preprocessor.cpp index 7c917dff5..c56554b53 100644 --- a/src/theory/theory_preprocessor.cpp +++ b/src/theory/theory_preprocessor.cpp @@ -450,6 +450,23 @@ Node TheoryPreprocessor::preprocessWithProof(Node term) // be steps from the same term to multiple rewritten forms, which would be // the case if we registered a preprocessing step for a non-rewritten term. Assert(term == Rewriter::rewrite(term)); + // We never call ppRewrite on equalities here, since equalities have a + // special status. In particular, notice that theory preprocessing can be + // called on all formulas asserted to theory engine, including those generated + // as new literals appearing in lemmas. Calling ppRewrite on equalities is + // incompatible with theory combination where a split on equality requested + // by a theory could be preprocessed to something else, thus making theory + // combination either non-terminating or result in solution soundness. + // Notice that an alternative solution is to ensure that certain lemmas + // (e.g. splits from theory combination) can never have theory preprocessing + // applied to them. However, it is more uniform to say that theory + // preprocessing is applied to all formulas. This makes it so that e.g. + // theory solvers do not need to specify whether they want their lemmas to + // be theory-preprocessed or not. + if (term.getKind() == kind::EQUAL) + { + return term; + } // call ppRewrite for the given theory TrustNode trn = d_engine.theoryOf(term)->ppRewrite(term); if (trn.isNull()) diff --git a/test/regress/regress1/quantifiers/qbv-simple-2vars-vo.smt2 b/test/regress/regress1/quantifiers/qbv-simple-2vars-vo.smt2 index 31cc96325..f291ec0ec 100644 --- a/test/regress/regress1/quantifiers/qbv-simple-2vars-vo.smt2 +++ b/test/regress/regress1/quantifiers/qbv-simple-2vars-vo.smt2 @@ -1,4 +1,4 @@ -; COMMAND-LINE: --cegqi-bv --cegqi-bv-ineq=keep +; COMMAND-LINE: --cegqi-bv --cegqi-bv-ineq=keep -q ; EXPECT: sat (set-logic BV) (set-info :status sat) diff --git a/test/regress/regress1/quantifiers/qbv-subcall.smt2 b/test/regress/regress1/quantifiers/qbv-subcall.smt2 index 5d6881411..42a93921b 100644 --- a/test/regress/regress1/quantifiers/qbv-subcall.smt2 +++ b/test/regress/regress1/quantifiers/qbv-subcall.smt2 @@ -1,3 +1,5 @@ +; COMMAND-LINE: -q +; EXPECT: sat (set-logic BV) (set-info :status sat) (declare-fun k_141 () (_ BitVec 16)) diff --git a/test/regress/regress1/quantifiers/smtcomp-qbv-053118.smt2 b/test/regress/regress1/quantifiers/smtcomp-qbv-053118.smt2 index 6cbe4db5c..d8bb5fcaf 100644 --- a/test/regress/regress1/quantifiers/smtcomp-qbv-053118.smt2 +++ b/test/regress/regress1/quantifiers/smtcomp-qbv-053118.smt2 @@ -1,3 +1,5 @@ +; COMMAND-LINE: -q +; EXPECT: sat (set-info :smt-lib-version 2.6) (set-logic BV) (set-info :status sat)