From ce58453982ddd53a5fc08d9db4c6c3f49b852838 Mon Sep 17 00:00:00 2001 From: Gereon Kremer Date: Fri, 19 Feb 2021 09:34:36 +0100 Subject: [PATCH] Cleanup of inferences in arithmetic theory (#5927) This PR cleans up several issues in the arithmetic theory mostly related to its usage of InferenceId and the TheoryInferenceManager: remove the ArithLemma class and uses SimpleTheoryLemma instead only use NlLemma if we actually need it use proper InferenceIds everywhere remove unused code in the nonlinear extension --- src/CMakeLists.txt | 2 - src/theory/arith/arith_lemma.cpp | 28 -------- src/theory/arith/arith_lemma.h | 58 ----------------- src/theory/arith/arith_preprocess.cpp | 2 +- src/theory/arith/inference_manager.cpp | 31 ++++----- src/theory/arith/inference_manager.h | 21 +++--- src/theory/arith/nl/cad_solver.cpp | 7 +- src/theory/arith/nl/ext/factoring_check.cpp | 4 +- .../arith/nl/ext/monomial_bounds_check.cpp | 8 ++- src/theory/arith/nl/ext/monomial_check.cpp | 14 ++-- src/theory/arith/nl/ext/monomial_check.h | 4 +- src/theory/arith/nl/ext/split_zero_check.cpp | 3 +- .../arith/nl/ext/tangent_plane_check.cpp | 6 +- src/theory/arith/nl/iand_solver.cpp | 16 ++--- src/theory/arith/nl/icp/icp_solver.cpp | 6 +- src/theory/arith/nl/nl_lemma_utils.cpp | 2 +- src/theory/arith/nl/nl_lemma_utils.h | 19 ++---- src/theory/arith/nl/nl_model.cpp | 2 +- src/theory/arith/nl/nonlinear_extension.cpp | 65 ++----------------- src/theory/arith/nl/nonlinear_extension.h | 9 --- .../nl/transcendental/exponential_solver.cpp | 18 ++--- .../arith/nl/transcendental/sine_solver.cpp | 29 ++++----- .../transcendental/transcendental_state.cpp | 10 +-- src/theory/inference_id.cpp | 60 ++++++++++------- src/theory/inference_id.h | 16 +++-- 25 files changed, 152 insertions(+), 288 deletions(-) delete mode 100644 src/theory/arith/arith_lemma.cpp delete mode 100644 src/theory/arith/arith_lemma.h diff --git a/src/CMakeLists.txt b/src/CMakeLists.txt index 96f98bd4c..3bfb248a4 100644 --- a/src/CMakeLists.txt +++ b/src/CMakeLists.txt @@ -291,8 +291,6 @@ libcvc4_add_sources( theory/arith/approx_simplex.h theory/arith/arith_ite_utils.cpp theory/arith/arith_ite_utils.h - theory/arith/arith_lemma.cpp - theory/arith/arith_lemma.h theory/arith/arith_msum.cpp theory/arith/arith_msum.h theory/arith/arith_preprocess.cpp diff --git a/src/theory/arith/arith_lemma.cpp b/src/theory/arith/arith_lemma.cpp deleted file mode 100644 index 9b8222586..000000000 --- a/src/theory/arith/arith_lemma.cpp +++ /dev/null @@ -1,28 +0,0 @@ -/********************* */ -/*! \file arith_lemma.cpp - ** \verbatim - ** Top contributors (to current version): - ** Gereon Kremer - ** 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 ArithLemma class, derived from Lemma. - **/ - -#include "theory/arith/arith_lemma.h" - -namespace CVC4 { -namespace theory { -namespace arith { - -std::ostream& operator<<(std::ostream& out, const ArithLemma& al) -{ - return out << al.d_node; -} - -} // namespace arith -} // namespace theory -} // namespace CVC4 diff --git a/src/theory/arith/arith_lemma.h b/src/theory/arith/arith_lemma.h deleted file mode 100644 index e50df15c0..000000000 --- a/src/theory/arith/arith_lemma.h +++ /dev/null @@ -1,58 +0,0 @@ -/********************* */ -/*! \file arith_lemma.h - ** \verbatim - ** Top contributors (to current version): - ** Gereon Kremer - ** 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 ArithLemma class, derived from Lemma. - **/ - -#ifndef CVC4__THEORY__ARITH__ARITH_LEMMA_H -#define CVC4__THEORY__ARITH__ARITH_LEMMA_H - -#include -#include - -#include "expr/node.h" -#include "theory/inference_id.h" -#include "theory/inference_manager_buffered.h" -#include "theory/output_channel.h" -#include "theory/theory_inference.h" - -namespace CVC4 { -namespace theory { -namespace arith { - -/** - * The data structure for a single lemma to process by the arithmetic theory, - * derived from theory::SimpleTheoryLemma. - * - * This also includes the inference type that produced this lemma. - */ -class ArithLemma : public SimpleTheoryLemma -{ - public: - ArithLemma(Node n, - LemmaProperty p, - ProofGenerator* pg, - InferenceId inf = InferenceId::UNKNOWN) - : SimpleTheoryLemma(inf, n, p, pg) - { - } - virtual ~ArithLemma() {} -}; -/** - * Writes an arithmetic lemma to a stream. - */ -std::ostream& operator<<(std::ostream& out, const ArithLemma& al); - -} // namespace arith -} // namespace theory -} // namespace CVC4 - -#endif /* CVC4__THEORY__ARITH__ARITH_LEMMA_H */ diff --git a/src/theory/arith/arith_preprocess.cpp b/src/theory/arith/arith_preprocess.cpp index 80217195f..3e0937e8b 100644 --- a/src/theory/arith/arith_preprocess.cpp +++ b/src/theory/arith/arith_preprocess.cpp @@ -49,7 +49,7 @@ bool ArithPreprocess::reduceAssertion(TNode atom) // tn is of kind REWRITE, turn this into a LEMMA here TrustNode tlem = TrustNode::mkTrustLemma(tn.getProven(), tn.getGenerator()); // must preprocess - d_im.trustedLemma(tlem, InferenceId::UNKNOWN); + d_im.trustedLemma(tlem, InferenceId::ARITH_PP_ELIM_OPERATORS); // mark the atom as reduced d_reduced[atom] = true; return true; diff --git a/src/theory/arith/inference_manager.cpp b/src/theory/arith/inference_manager.cpp index c406c0ce6..c2001686b 100644 --- a/src/theory/arith/inference_manager.cpp +++ b/src/theory/arith/inference_manager.cpp @@ -29,8 +29,8 @@ InferenceManager::InferenceManager(TheoryArith& ta, { } -void InferenceManager::addPendingArithLemma(std::unique_ptr lemma, - bool isWaiting) +void InferenceManager::addPendingLemma(std::unique_ptr lemma, + bool isWaiting) { Trace("arith::infman") << "Add " << lemma->getId() << " " << lemma->d_node << (isWaiting ? " as waiting" : "") << std::endl; @@ -59,21 +59,22 @@ void InferenceManager::addPendingArithLemma(std::unique_ptr lemma, d_pendingLem.emplace_back(std::move(lemma)); } } -void InferenceManager::addPendingArithLemma(const ArithLemma& lemma, - bool isWaiting) +void InferenceManager::addPendingLemma(const SimpleTheoryLemma& lemma, + bool isWaiting) { - addPendingArithLemma(std::unique_ptr(new ArithLemma(lemma)), - isWaiting); + addPendingLemma( + std::unique_ptr(new SimpleTheoryLemma(lemma)), + isWaiting); } -void InferenceManager::addPendingArithLemma(const Node& lemma, - InferenceId inftype, - ProofGenerator* pg, - bool isWaiting, - LemmaProperty p) +void InferenceManager::addPendingLemma(const Node& lemma, + InferenceId inftype, + ProofGenerator* pg, + bool isWaiting, + LemmaProperty p) { - addPendingArithLemma( - std::unique_ptr(new ArithLemma(lemma, p, pg, inftype)), - isWaiting); + addPendingLemma(std::unique_ptr( + new SimpleTheoryLemma(inftype, lemma, p, pg)), + isWaiting); } void InferenceManager::flushWaitingLemmas() @@ -119,7 +120,7 @@ bool InferenceManager::cacheLemma(TNode lem, LemmaProperty p) return TheoryInferenceManager::cacheLemma(rewritten, p); } -bool InferenceManager::isEntailedFalse(const ArithLemma& lem) +bool InferenceManager::isEntailedFalse(const SimpleTheoryLemma& lem) { if (options::nlExtEntailConflicts()) { diff --git a/src/theory/arith/inference_manager.h b/src/theory/arith/inference_manager.h index ea3e1850a..f033c4a5c 100644 --- a/src/theory/arith/inference_manager.h +++ b/src/theory/arith/inference_manager.h @@ -20,7 +20,6 @@ #include #include -#include "theory/arith/arith_lemma.h" #include "theory/arith/arith_state.h" #include "theory/inference_id.h" #include "theory/arith/nl/nl_lemma_utils.h" @@ -55,24 +54,24 @@ class InferenceManager : public InferenceManagerBuffered * If isWaiting is true, the lemma is first stored as waiting lemma and only * added as pending lemma when calling flushWaitingLemmas. */ - void addPendingArithLemma(std::unique_ptr lemma, - bool isWaiting = false); + void addPendingLemma(std::unique_ptr lemma, + bool isWaiting = false); /** * Add a lemma as pending lemma to this inference manager. * If isWaiting is true, the lemma is first stored as waiting lemma and only * added as pending lemma when calling flushWaitingLemmas. */ - void addPendingArithLemma(const ArithLemma& lemma, bool isWaiting = false); + void addPendingLemma(const SimpleTheoryLemma& lemma, bool isWaiting = false); /** * Add a lemma as pending lemma to this inference manager. * If isWaiting is true, the lemma is first stored as waiting lemma and only * added as pending lemma when calling flushWaitingLemmas. */ - void addPendingArithLemma(const Node& lemma, - InferenceId inftype, - ProofGenerator* pg = nullptr, - bool isWaiting = false, - LemmaProperty p = LemmaProperty::NONE); + void addPendingLemma(const Node& lemma, + InferenceId inftype, + ProofGenerator* pg = nullptr, + bool isWaiting = false, + LemmaProperty p = LemmaProperty::NONE); /** * Flush all waiting lemmas to this inference manager (as pending @@ -112,10 +111,10 @@ class InferenceManager : public InferenceManagerBuffered * Checks whether the lemma is entailed to be false. In this case, it is a * conflict. */ - bool isEntailedFalse(const ArithLemma& lem); + bool isEntailedFalse(const SimpleTheoryLemma& lem); /** The waiting lemmas. */ - std::vector> d_waitingLem; + std::vector> d_waitingLem; }; } // namespace arith diff --git a/src/theory/arith/nl/cad_solver.cpp b/src/theory/arith/nl/cad_solver.cpp index 5418ea5bb..83ceb1182 100644 --- a/src/theory/arith/nl/cad_solver.cpp +++ b/src/theory/arith/nl/cad_solver.cpp @@ -92,8 +92,8 @@ void CadSolver::checkFull() { n = n.negate(); } - d_im.addPendingArithLemma(NodeManager::currentNM()->mkOr(mis), - InferenceId::ARITH_NL_CAD_CONFLICT); + d_im.addPendingLemma(NodeManager::currentNM()->mkOr(mis), + InferenceId::ARITH_NL_CAD_CONFLICT); } #else Warning() << "Tried to use CadSolver but libpoly is not available. Compile " @@ -140,7 +140,8 @@ void CadSolver::checkPartial() Trace("nl-cad") << "Excluding " << first_var << " -> " << interval.d_interval << " using " << lemma << std::endl; - d_im.addPendingArithLemma(lemma, InferenceId::ARITH_NL_CAD_EXCLUDED_INTERVAL); + d_im.addPendingLemma(lemma, + InferenceId::ARITH_NL_CAD_EXCLUDED_INTERVAL); } } } diff --git a/src/theory/arith/nl/ext/factoring_check.cpp b/src/theory/arith/nl/ext/factoring_check.cpp index 20f89aa82..7b4d98037 100644 --- a/src/theory/arith/nl/ext/factoring_check.cpp +++ b/src/theory/arith/nl/ext/factoring_check.cpp @@ -167,7 +167,7 @@ void FactoringCheck::check(const std::vector& asserts, proof->addStep( flem, PfRule::MACRO_SR_PRED_TRANSFORM, {split, k_eq}, {flem}); } - d_data->d_im.addPendingArithLemma( + d_data->d_im.addPendingLemma( flem, InferenceId::ARITH_NL_FACTOR, proof); } } @@ -186,7 +186,7 @@ Node FactoringCheck::getFactorSkolem(Node n, CDProof* proof) Node k_eq = k.eqNode(n); Trace("nl-ext-factor") << "...adding factor skolem " << k << " == " << n << std::endl; - d_data->d_im.addPendingArithLemma(k_eq, InferenceId::ARITH_NL_FACTOR, proof); + d_data->d_im.addPendingLemma(k_eq, InferenceId::ARITH_NL_FACTOR, proof); d_factor_skolem[n] = k; } else diff --git a/src/theory/arith/nl/ext/monomial_bounds_check.cpp b/src/theory/arith/nl/ext/monomial_bounds_check.cpp index 9ffaf53c1..46b1c991e 100644 --- a/src/theory/arith/nl/ext/monomial_bounds_check.cpp +++ b/src/theory/arith/nl/ext/monomial_bounds_check.cpp @@ -319,8 +319,10 @@ void MonomialBoundsCheck::checkBounds(const std::vector& asserts, << " (pre-rewrite : " << pr_iblem << ")" << std::endl; // Trace("nl-ext-bound-lemma") << " intro new // monomials = " << introNewTerms << std::endl; - d_data->d_im.addPendingArithLemma( - iblem, InferenceId::ARITH_NL_INFER_BOUNDS_NT, nullptr, introNewTerms); + d_data->d_im.addPendingLemma(iblem, + InferenceId::ARITH_NL_INFER_BOUNDS_NT, + nullptr, + introNewTerms); } } } @@ -478,7 +480,7 @@ void MonomialBoundsCheck::checkResBounds() rblem = Rewriter::rewrite(rblem); Trace("nl-ext-rbound-lemma") << "Resolution bound lemma : " << rblem << std::endl; - d_data->d_im.addPendingArithLemma( + d_data->d_im.addPendingLemma( rblem, InferenceId::ARITH_NL_RES_INFER_BOUNDS); } } diff --git a/src/theory/arith/nl/ext/monomial_check.cpp b/src/theory/arith/nl/ext/monomial_check.cpp index a007dd4a6..c6ee3d764 100644 --- a/src/theory/arith/nl/ext/monomial_check.cpp +++ b/src/theory/arith/nl/ext/monomial_check.cpp @@ -112,7 +112,7 @@ void MonomialCheck::checkMagnitude(unsigned c) } unsigned r = 1; - std::vector lemmas; + std::vector lemmas; // if (x,y,L) in cmp_infers, then x > y inferred as conclusion of L // in lemmas std::map > > cmp_infers; @@ -274,7 +274,7 @@ void MonomialCheck::checkMagnitude(unsigned c) { if (r_lemmas.find(lemmas[i].d_node) == r_lemmas.end()) { - d_data->d_im.addPendingArithLemma(lemmas[i]); + d_data->d_im.addPendingLemma(lemmas[i]); } } // could only take maximal lower/minimial lower bounds? @@ -295,7 +295,7 @@ int MonomialCheck::compareSign( { Node lemma = nm->mkAnd(exp).impNode(mkLit(oa, d_data->d_zero, status * 2)); - d_data->d_im.addPendingArithLemma(lemma, InferenceId::ARITH_NL_SIGN); + d_data->d_im.addPendingLemma(lemma, InferenceId::ARITH_NL_SIGN); } return status; } @@ -321,7 +321,7 @@ int MonomialCheck::compareSign( proof->addStep(conc, PfRule::MACRO_SR_PRED_INTRO, {prem}, {conc}); proof->addStep(lemma, PfRule::SCOPE, {conc}, {prem}); } - d_data->d_im.addPendingArithLemma(lemma, InferenceId::ARITH_NL_SIGN, proof); + d_data->d_im.addPendingLemma(lemma, InferenceId::ARITH_NL_SIGN, proof); } return 0; } @@ -342,7 +342,7 @@ bool MonomialCheck::compareMonomial( Node b, NodeMultiset& b_exp_proc, std::vector& exp, - std::vector& lem, + std::vector& lem, std::map > >& cmp_infers) { Trace("nl-ext-comp-debug") @@ -377,7 +377,7 @@ bool MonomialCheck::compareMonomial( NodeMultiset& b_exp_proc, int status, std::vector& exp, - std::vector& lem, + std::vector& lem, std::map > >& cmp_infers) { Trace("nl-ext-comp-debug") @@ -410,7 +410,7 @@ bool MonomialCheck::compareMonomial( Kind::IMPLIES, nm->mkAnd(exp), mkLit(oa, ob, status, true)); Trace("nl-ext-comp-lemma") << "comparison lemma : " << clem << std::endl; lem.emplace_back( - clem, LemmaProperty::NONE, nullptr, InferenceId::ARITH_NL_COMPARISON); + InferenceId::ARITH_NL_COMPARISON, clem, LemmaProperty::NONE, nullptr); cmp_infers[status][oa][ob] = clem; } return true; diff --git a/src/theory/arith/nl/ext/monomial_check.h b/src/theory/arith/nl/ext/monomial_check.h index ed8639ef2..51179826a 100644 --- a/src/theory/arith/nl/ext/monomial_check.h +++ b/src/theory/arith/nl/ext/monomial_check.h @@ -136,7 +136,7 @@ class MonomialCheck Node b, NodeMultiset& b_exp_proc, std::vector& exp, - std::vector& lem, + std::vector& lem, std::map > >& cmp_infers); /** helper function for above * @@ -154,7 +154,7 @@ class MonomialCheck NodeMultiset& b_exp_proc, int status, std::vector& exp, - std::vector& lem, + std::vector& lem, std::map > >& cmp_infers); /** Check whether we have already inferred a relationship between monomials * x and y based on the information in cmp_infers. This computes the diff --git a/src/theory/arith/nl/ext/split_zero_check.cpp b/src/theory/arith/nl/ext/split_zero_check.cpp index 2e3cb3cd1..1e9b444e3 100644 --- a/src/theory/arith/nl/ext/split_zero_check.cpp +++ b/src/theory/arith/nl/ext/split_zero_check.cpp @@ -45,7 +45,8 @@ void SplitZeroCheck::check() proof->addStep(lem, PfRule::SPLIT, {}, {eq}); } d_data->d_im.addPendingPhaseRequirement(eq, true); - d_data->d_im.addPendingArithLemma(lem, InferenceId::ARITH_NL_SPLIT_ZERO, proof); + d_data->d_im.addPendingLemma( + lem, InferenceId::ARITH_NL_SPLIT_ZERO, proof); } } } diff --git a/src/theory/arith/nl/ext/tangent_plane_check.cpp b/src/theory/arith/nl/ext/tangent_plane_check.cpp index a4642b73a..3d646a684 100644 --- a/src/theory/arith/nl/ext/tangent_plane_check.cpp +++ b/src/theory/arith/nl/ext/tangent_plane_check.cpp @@ -146,8 +146,10 @@ void TangentPlaneCheck::check(bool asWaitingLemmas) b_v, nm->mkConst(Rational(d == 0 ? -1 : 1))}); } - d_data->d_im.addPendingArithLemma( - tlem, InferenceId::ARITH_NL_TANGENT_PLANE, proof, asWaitingLemmas); + d_data->d_im.addPendingLemma(tlem, + InferenceId::ARITH_NL_TANGENT_PLANE, + proof, + asWaitingLemmas); } } } diff --git a/src/theory/arith/nl/iand_solver.cpp b/src/theory/arith/nl/iand_solver.cpp index ff51f7bb5..78ffb3c09 100644 --- a/src/theory/arith/nl/iand_solver.cpp +++ b/src/theory/arith/nl/iand_solver.cpp @@ -99,7 +99,7 @@ void IAndSolver::checkInitialRefine() Node lem = conj.size() == 1 ? conj[0] : nm->mkNode(AND, conj); Trace("iand-lemma") << "IAndSolver::Lemma: " << lem << " ; INIT_REFINE" << std::endl; - d_im.addPendingArithLemma(lem, InferenceId::ARITH_NL_IAND_INIT_REFINE); + d_im.addPendingLemma(lem, InferenceId::ARITH_NL_IAND_INIT_REFINE); } } } @@ -152,7 +152,7 @@ void IAndSolver::checkFullRefine() << "IAndSolver::Lemma: " << lem << " ; SUM_REFINE" << std::endl; // note that lemma can contain div/mod, and will be preprocessed in the // prop engine - d_im.addPendingArithLemma( + d_im.addPendingLemma( lem, InferenceId::ARITH_NL_IAND_SUM_REFINE, nullptr, true); } else if (options::iandMode() == options::IandMode::BITWISE) @@ -162,7 +162,7 @@ void IAndSolver::checkFullRefine() << "IAndSolver::Lemma: " << lem << " ; BITWISE_REFINE" << std::endl; // note that lemma can contain div/mod, and will be preprocessed in the // prop engine - d_im.addPendingArithLemma( + d_im.addPendingLemma( lem, InferenceId::ARITH_NL_IAND_BITWISE_REFINE, nullptr, true); } else @@ -172,11 +172,11 @@ void IAndSolver::checkFullRefine() Trace("iand-lemma") << "IAndSolver::Lemma: " << lem << " ; VALUE_REFINE" << std::endl; // value lemmas should not contain div/mod so we don't need to tag it with PREPROCESS - d_im.addPendingArithLemma(lem, - InferenceId::ARITH_NL_IAND_VALUE_REFINE, - nullptr, - true, - LemmaProperty::NONE); + d_im.addPendingLemma(lem, + InferenceId::ARITH_NL_IAND_VALUE_REFINE, + nullptr, + true, + LemmaProperty::NONE); } } } diff --git a/src/theory/arith/nl/icp/icp_solver.cpp b/src/theory/arith/nl/icp/icp_solver.cpp index af6093be1..af86d69fd 100644 --- a/src/theory/arith/nl/icp/icp_solver.cpp +++ b/src/theory/arith/nl/icp/icp_solver.cpp @@ -348,8 +348,8 @@ void ICPSolver::check() { mis.emplace_back(n.negate()); } - d_im.addPendingArithLemma(NodeManager::currentNM()->mkOr(mis), - InferenceId::ARITH_NL_ICP_CONFLICT); + d_im.addPendingLemma(NodeManager::currentNM()->mkOr(mis), + InferenceId::ARITH_NL_ICP_CONFLICT); did_progress = true; progress = false; break; @@ -360,7 +360,7 @@ void ICPSolver::check() std::vector lemmas = generateLemmas(); for (const auto& l : lemmas) { - d_im.addPendingArithLemma(l, InferenceId::ARITH_NL_ICP_PROPAGATION); + d_im.addPendingLemma(l, InferenceId::ARITH_NL_ICP_PROPAGATION); } } } diff --git a/src/theory/arith/nl/nl_lemma_utils.cpp b/src/theory/arith/nl/nl_lemma_utils.cpp index 8ae5ecc4b..7cb1da728 100644 --- a/src/theory/arith/nl/nl_lemma_utils.cpp +++ b/src/theory/arith/nl/nl_lemma_utils.cpp @@ -24,7 +24,7 @@ namespace nl { bool NlLemma::process(TheoryInferenceManager* im, bool asLemma) { - bool res = ArithLemma::process(im, asLemma); + bool res = SimpleTheoryLemma::process(im, asLemma); if (d_nlext != nullptr) { d_nlext->processSideEffect(*this); diff --git a/src/theory/arith/nl/nl_lemma_utils.h b/src/theory/arith/nl/nl_lemma_utils.h index 24302339c..277751fe8 100644 --- a/src/theory/arith/nl/nl_lemma_utils.h +++ b/src/theory/arith/nl/nl_lemma_utils.h @@ -19,8 +19,7 @@ #include #include "expr/node.h" -#include "theory/arith/arith_lemma.h" -#include "theory/output_channel.h" +#include "theory/theory_inference.h" namespace CVC4 { namespace theory { @@ -41,18 +40,14 @@ class NonlinearExtension; * - A set of secant points to record (for transcendental secant plane * inferences). */ -class NlLemma : public ArithLemma +class NlLemma : public SimpleTheoryLemma { public: - NlLemma(Node n, - LemmaProperty p, - ProofGenerator* pg, - InferenceId inf = InferenceId::UNKNOWN) - : ArithLemma(n, p, pg, inf) - { - } - NlLemma(Node n, InferenceId inf = InferenceId::UNKNOWN) - : ArithLemma(n, LemmaProperty::NONE, nullptr, inf) + NlLemma(InferenceId inf, + Node n, + LemmaProperty p = LemmaProperty::NONE, + ProofGenerator* pg = nullptr) + : SimpleTheoryLemma(inf, n, p, pg) { } ~NlLemma() {} diff --git a/src/theory/arith/nl/nl_model.cpp b/src/theory/arith/nl/nl_model.cpp index 79f2a2350..5c4140430 100644 --- a/src/theory/arith/nl/nl_model.cpp +++ b/src/theory/arith/nl/nl_model.cpp @@ -640,7 +640,7 @@ bool NlModel::solveEqualitySimple(Node eq, Node conf = seq.negate(); Trace("nl-ext-lemma") << "NlModel::Lemma : quadratic no root : " << conf << std::endl; - lemmas.push_back(conf); + lemmas.emplace_back(InferenceId::ARITH_NL_CM_QUADRATIC_EQ, conf); Trace("nl-ext-cms") << "...fail due to negative discriminant." << std::endl; return false; } diff --git a/src/theory/arith/nl/nonlinear_extension.cpp b/src/theory/arith/nl/nonlinear_extension.cpp index 36ddecee9..4d29f1955 100644 --- a/src/theory/arith/nl/nonlinear_extension.cpp +++ b/src/theory/arith/nl/nonlinear_extension.cpp @@ -106,63 +106,6 @@ void NonlinearExtension::computeRelevantAssertions( << " assertions" << std::endl; } -unsigned NonlinearExtension::filterLemma(NlLemma lem, std::vector& out) -{ - Trace("nl-ext-lemma-debug") - << "NonlinearExtension::Lemma pre-rewrite : " << lem.d_node << std::endl; - lem.d_node = Rewriter::rewrite(lem.d_node); - - if (d_im.hasCachedLemma(lem.d_node, lem.d_property)) - { - Trace("nl-ext-lemma-debug") - << "NonlinearExtension::Lemma duplicate : " << lem.d_node << std::endl; - return 0; - } - out.emplace_back(lem); - return 1; -} - -unsigned NonlinearExtension::filterLemmas(std::vector& lemmas, - std::vector& out) -{ - if (options::nlExtEntailConflicts()) - { - // check if any are entailed to be false - for (const NlLemma& lem : lemmas) - { - Node ch_lemma = lem.d_node.negate(); - ch_lemma = Rewriter::rewrite(ch_lemma); - Trace("nl-ext-et-debug") - << "Check entailment of " << ch_lemma << "..." << std::endl; - std::pair et = d_containing.getValuation().entailmentCheck( - options::TheoryOfMode::THEORY_OF_TYPE_BASED, ch_lemma); - Trace("nl-ext-et-debug") << "entailment test result : " << et.first << " " - << et.second << std::endl; - if (et.first) - { - Trace("nl-ext-et") << "*** Lemma entailed to be in conflict : " - << lem.d_node << std::endl; - // return just this lemma - if (filterLemma(lem, out) > 0) - { - lemmas.clear(); - return 1; - } - } - } - } - - unsigned sum = 0; - for (const NlLemma& lem : lemmas) - { - sum += filterLemma(lem, out); - d_containing.getOutputChannel().spendResource( - ResourceManager::Resource::ArithNlLemmaStep); - } - lemmas.clear(); - return sum; -} - void NonlinearExtension::getAssertions(std::vector& assertions) { Trace("nl-ext-assert-debug") << "Getting assertions..." << std::endl; @@ -293,7 +236,7 @@ bool NonlinearExtension::checkModel(const std::vector& assertions) bool ret = d_model.checkModel(passertions, tdegree, lemmas); for (const auto& al: lemmas) { - d_im.addPendingArithLemma(al); + d_im.addPendingLemma(al); } return ret; } @@ -500,8 +443,10 @@ bool NonlinearExtension::modelBasedRefinement() d_containing.getOutputChannel().requirePhase(literal, true); Trace("nl-ext-debug") << "Split on : " << literal << std::endl; Node split = literal.orNode(literal.negate()); - NlLemma nsplit(split, InferenceId::ARITH_NL_SHARED_TERM_VALUE_SPLIT); - d_im.addPendingArithLemma(nsplit, true); + d_im.addPendingLemma(split, + InferenceId::ARITH_NL_SHARED_TERM_VALUE_SPLIT, + nullptr, + true); } if (d_im.hasWaitingLemma()) { diff --git a/src/theory/arith/nl/nonlinear_extension.h b/src/theory/arith/nl/nonlinear_extension.h index a6b68d644..fba9e8e87 100644 --- a/src/theory/arith/nl/nonlinear_extension.h +++ b/src/theory/arith/nl/nonlinear_extension.h @@ -193,15 +193,6 @@ class NonlinearExtension /** compute relevant assertions */ void computeRelevantAssertions(const std::vector& assertions, std::vector& keep); - /** - * Potentially adds lemmas to the set out and clears lemmas. Returns - * the number of lemmas added to out. We do not add lemmas that have already - * been sent on the output channel of TheoryArith. - */ - unsigned filterLemmas(std::vector& lemmas, - std::vector& out); - /** singleton version of above */ - unsigned filterLemma(NlLemma lem, std::vector& out); /** run check strategy * diff --git a/src/theory/arith/nl/transcendental/exponential_solver.cpp b/src/theory/arith/nl/transcendental/exponential_solver.cpp index cc60d20fd..7f9d98fe1 100644 --- a/src/theory/arith/nl/transcendental/exponential_solver.cpp +++ b/src/theory/arith/nl/transcendental/exponential_solver.cpp @@ -45,8 +45,7 @@ void ExponentialSolver::doPurification(TNode a, TNode new_a, TNode y) // note we must do preprocess on this lemma Trace("nl-ext-lemma") << "NonlinearExtension::Lemma : purify : " << lem << std::endl; - NlLemma nlem(lem, LemmaProperty::NONE, nullptr, InferenceId::ARITH_NL_T_PURIFY_ARG); - d_data->d_im.addPendingArithLemma(nlem); + d_data->d_im.addPendingLemma(lem, InferenceId::ARITH_NL_T_PURIFY_ARG); } void ExponentialSolver::checkInitialRefine() @@ -71,7 +70,7 @@ void ExponentialSolver::checkInitialRefine() { // exp is always positive: exp(t) > 0 Node lem = nm->mkNode(Kind::GT, t, d_data->d_zero); - d_data->d_im.addPendingArithLemma( + d_data->d_im.addPendingLemma( lem, InferenceId::ARITH_NL_T_INIT_REFINE, nullptr); } { @@ -79,7 +78,7 @@ void ExponentialSolver::checkInitialRefine() Node lem = nm->mkNode(Kind::EQUAL, t[0].eqNode(d_data->d_zero), t.eqNode(d_data->d_one)); - d_data->d_im.addPendingArithLemma( + d_data->d_im.addPendingLemma( lem, InferenceId::ARITH_NL_T_INIT_REFINE, nullptr); } { @@ -87,7 +86,7 @@ void ExponentialSolver::checkInitialRefine() Node lem = nm->mkNode(Kind::EQUAL, nm->mkNode(Kind::LT, t[0], d_data->d_zero), nm->mkNode(Kind::LT, t, d_data->d_one)); - d_data->d_im.addPendingArithLemma( + d_data->d_im.addPendingLemma( lem, InferenceId::ARITH_NL_T_INIT_REFINE, nullptr); } { @@ -97,7 +96,7 @@ void ExponentialSolver::checkInitialRefine() nm->mkNode(Kind::LEQ, t[0], d_data->d_zero), nm->mkNode( Kind::GT, t, nm->mkNode(Kind::PLUS, t[0], d_data->d_one))); - d_data->d_im.addPendingArithLemma( + d_data->d_im.addPendingLemma( lem, InferenceId::ARITH_NL_T_INIT_REFINE, nullptr); } } @@ -162,8 +161,8 @@ void ExponentialSolver::checkMonotonic() nm->mkNode(Kind::GEQ, t, s)); Trace("nl-ext-exp") << "Monotonicity lemma : " << mono_lem << std::endl; - d_data->d_im.addPendingArithLemma(mono_lem, - InferenceId::ARITH_NL_T_MONOTONICITY); + d_data->d_im.addPendingLemma(mono_lem, + InferenceId::ARITH_NL_T_MONOTONICITY); } // store the previous values targ = sarg; @@ -190,7 +189,8 @@ void ExponentialSolver::doTangentLemma(TNode e, TNode c, TNode poly_approx) Trace("nl-ext-exp") << "*** Tangent plane lemma : " << lem << std::endl; Assert(d_data->d_model.computeAbstractModelValue(lem) == d_data->d_false); // Figure 3 : line 9 - d_data->d_im.addPendingArithLemma(lem, InferenceId::ARITH_NL_T_TANGENT, nullptr, true); + d_data->d_im.addPendingLemma( + lem, InferenceId::ARITH_NL_T_TANGENT, nullptr, true); } void ExponentialSolver::doSecantLemmas(TNode e, diff --git a/src/theory/arith/nl/transcendental/sine_solver.cpp b/src/theory/arith/nl/transcendental/sine_solver.cpp index 99bb093bb..0cca238b0 100644 --- a/src/theory/arith/nl/transcendental/sine_solver.cpp +++ b/src/theory/arith/nl/transcendental/sine_solver.cpp @@ -79,8 +79,7 @@ void SineSolver::doPhaseShift(TNode a, TNode new_a, TNode y) // note we must do preprocess on this lemma Trace("nl-ext-lemma") << "NonlinearExtension::Lemma : purify : " << lem << std::endl; - NlLemma nlem(lem, LemmaProperty::NONE, proof, InferenceId::ARITH_NL_T_PURIFY_ARG); - d_data->d_im.addPendingArithLemma(nlem); + d_data->d_im.addPendingLemma(lem, InferenceId::ARITH_NL_T_PURIFY_ARG, proof); } void SineSolver::checkInitialRefine() @@ -115,14 +114,14 @@ void SineSolver::checkInitialRefine() Node lem = nm->mkNode(Kind::AND, nm->mkNode(Kind::LEQ, t, d_data->d_one), nm->mkNode(Kind::GEQ, t, d_data->d_neg_one)); - d_data->d_im.addPendingArithLemma( - lem, InferenceId::ARITH_NL_T_INIT_REFINE); + d_data->d_im.addPendingLemma(lem, + InferenceId::ARITH_NL_T_INIT_REFINE); } { // sine symmetry: sin(t) - sin(-t) = 0 Node lem = nm->mkNode(Kind::PLUS, t, symn).eqNode(d_data->d_zero); - d_data->d_im.addPendingArithLemma( - lem, InferenceId::ARITH_NL_T_INIT_REFINE); + d_data->d_im.addPendingLemma(lem, + InferenceId::ARITH_NL_T_INIT_REFINE); } { // sine zero tangent: @@ -136,8 +135,8 @@ void SineSolver::checkInitialRefine() nm->mkNode(Kind::IMPLIES, nm->mkNode(Kind::LT, t[0], d_data->d_zero), nm->mkNode(Kind::GT, t, t[0]))); - d_data->d_im.addPendingArithLemma( - lem, InferenceId::ARITH_NL_T_INIT_REFINE); + d_data->d_im.addPendingLemma(lem, + InferenceId::ARITH_NL_T_INIT_REFINE); } { // sine pi tangent: @@ -157,8 +156,8 @@ void SineSolver::checkInitialRefine() nm->mkNode(Kind::LT, t, nm->mkNode(Kind::MINUS, d_data->d_pi, t[0])))); - d_data->d_im.addPendingArithLemma( - lem, InferenceId::ARITH_NL_T_INIT_REFINE); + d_data->d_im.addPendingLemma(lem, + InferenceId::ARITH_NL_T_INIT_REFINE); } { Node lem = @@ -171,8 +170,8 @@ void SineSolver::checkInitialRefine() nm->mkNode(Kind::EQUAL, nm->mkNode(Kind::GT, t[0], d_data->d_zero), nm->mkNode(Kind::GT, t, d_data->d_zero))); - d_data->d_im.addPendingArithLemma( - lem, InferenceId::ARITH_NL_T_INIT_REFINE); + d_data->d_im.addPendingLemma(lem, + InferenceId::ARITH_NL_T_INIT_REFINE); } } } @@ -311,8 +310,8 @@ void SineSolver::checkMonotonic() Trace("nl-ext-tf-mono") << "Monotonicity lemma : " << mono_lem << std::endl; - d_data->d_im.addPendingArithLemma(mono_lem, - InferenceId::ARITH_NL_T_MONOTONICITY); + d_data->d_im.addPendingLemma(mono_lem, + InferenceId::ARITH_NL_T_MONOTONICITY); } } // store the previous values @@ -352,7 +351,7 @@ void SineSolver::doTangentLemma(TNode e, TNode c, TNode poly_approx, int region) Trace("nl-ext-sine") << "*** Tangent plane lemma : " << lem << std::endl; Assert(d_data->d_model.computeAbstractModelValue(lem) == d_data->d_false); // Figure 3 : line 9 - d_data->d_im.addPendingArithLemma( + d_data->d_im.addPendingLemma( lem, InferenceId::ARITH_NL_T_TANGENT, nullptr, true); } diff --git a/src/theory/arith/nl/transcendental/transcendental_state.cpp b/src/theory/arith/nl/transcendental/transcendental_state.cpp index 032cf1411..35967a39a 100644 --- a/src/theory/arith/nl/transcendental/transcendental_state.cpp +++ b/src/theory/arith/nl/transcendental/transcendental_state.cpp @@ -179,7 +179,7 @@ void TranscendentalState::ensureCongruence(TNode a, } Node expn = exp.size() == 1 ? exp[0] : nm->mkNode(Kind::AND, exp); Node cong_lemma = expn.impNode(a.eqNode(aa)); - d_im.addPendingArithLemma(cong_lemma, InferenceId::ARITH_NL_CONGRUENCE); + d_im.addPendingLemma(cong_lemma, InferenceId::ARITH_NL_CONGRUENCE); } } else @@ -222,7 +222,7 @@ void TranscendentalState::getCurrentPiBounds() proof->addStep( pi_lem, PfRule::ARITH_TRANS_PI, {}, {d_pi_bound[0], d_pi_bound[1]}); } - d_im.addPendingArithLemma(pi_lem, InferenceId::ARITH_NL_T_PI_BOUND, proof); + d_im.addPendingLemma(pi_lem, InferenceId::ARITH_NL_T_PI_BOUND, proof); } std::pair TranscendentalState::getClosestSecantPoints(TNode e, @@ -319,7 +319,7 @@ NlLemma TranscendentalState::mkSecantLemma(TNode lower, lem = Rewriter::rewrite(lem); Trace("nl-trans-lemma") << "*** Secant plane lemma : " << lem << std::endl; Assert(d_model.computeAbstractModelValue(lem) == d_false); - return NlLemma(lem, LemmaProperty::NONE, nullptr, InferenceId::ARITH_NL_T_SECANT); + return NlLemma(InferenceId::ARITH_NL_T_SECANT, lem); } void TranscendentalState::doSecantLemmas(const std::pair& bounds, @@ -352,7 +352,7 @@ void TranscendentalState::doSecantLemmas(const std::pair& bounds, // The side effect says that if lem is added, then we should add the // secant point c for (tf,d). nlem.d_secantPoint.push_back(std::make_tuple(tf, d, center)); - d_im.addPendingArithLemma(nlem, true); + d_im.addPendingLemma(nlem, true); } // take the model value of upper (since may contain PI) @@ -371,7 +371,7 @@ void TranscendentalState::doSecantLemmas(const std::pair& bounds, // The side effect says that if lem is added, then we should add the // secant point c for (tf,d). nlem.d_secantPoint.push_back(std::make_tuple(tf, d, center)); - d_im.addPendingArithLemma(nlem, true); + d_im.addPendingLemma(nlem, true); } } diff --git a/src/theory/inference_id.cpp b/src/theory/inference_id.cpp index cb15b4326..0268fa31a 100644 --- a/src/theory/inference_id.cpp +++ b/src/theory/inference_id.cpp @@ -21,30 +21,42 @@ const char* toString(InferenceId i) { switch (i) { - case InferenceId::ARITH_NL_CONGRUENCE: return "CONGRUENCE"; - case InferenceId::ARITH_NL_SHARED_TERM_VALUE_SPLIT: return "SHARED_TERM_VALUE_SPLIT"; - case InferenceId::ARITH_NL_SPLIT_ZERO: return "SPLIT_ZERO"; - case InferenceId::ARITH_NL_SIGN: return "SIGN"; - case InferenceId::ARITH_NL_COMPARISON: return "COMPARISON"; - case InferenceId::ARITH_NL_INFER_BOUNDS: return "INFER_BOUNDS"; - case InferenceId::ARITH_NL_INFER_BOUNDS_NT: return "INFER_BOUNDS_NT"; - case InferenceId::ARITH_NL_FACTOR: return "FACTOR"; - case InferenceId::ARITH_NL_RES_INFER_BOUNDS: return "RES_INFER_BOUNDS"; - case InferenceId::ARITH_NL_TANGENT_PLANE: return "TANGENT_PLANE"; - case InferenceId::ARITH_NL_T_PURIFY_ARG: return "T_PURIFY_ARG"; - case InferenceId::ARITH_NL_T_INIT_REFINE: return "T_INIT_REFINE"; - case InferenceId::ARITH_NL_T_PI_BOUND: return "T_PI_BOUND"; - case InferenceId::ARITH_NL_T_MONOTONICITY: return "T_MONOTONICITY"; - case InferenceId::ARITH_NL_T_SECANT: return "T_SECANT"; - case InferenceId::ARITH_NL_T_TANGENT: return "T_TANGENT"; - case InferenceId::ARITH_NL_IAND_INIT_REFINE: return "IAND_INIT_REFINE"; - case InferenceId::ARITH_NL_IAND_VALUE_REFINE: return "IAND_VALUE_REFINE"; - case InferenceId::ARITH_NL_IAND_SUM_REFINE: return "IAND_SUM_REFINE"; - case InferenceId::ARITH_NL_IAND_BITWISE_REFINE: return "IAND_BITWISE_REFINE"; - case InferenceId::ARITH_NL_CAD_CONFLICT: return "CAD_CONFLICT"; - case InferenceId::ARITH_NL_CAD_EXCLUDED_INTERVAL: return "CAD_EXCLUDED_INTERVAL"; - case InferenceId::ARITH_NL_ICP_CONFLICT: return "ICP_CONFLICT"; - case InferenceId::ARITH_NL_ICP_PROPAGATION: return "ICP_PROPAGATION"; + case InferenceId::ARITH_PP_ELIM_OPERATORS: return "ARITH_PP_ELIM_OPERATORS"; + case InferenceId::ARITH_NL_CONGRUENCE: return "ARITH_NL_CONGRUENCE"; + case InferenceId::ARITH_NL_SHARED_TERM_VALUE_SPLIT: + return "ARITH_NL_SHARED_TERM_VALUE_SPLIT"; + case InferenceId::ARITH_NL_CM_QUADRATIC_EQ: + return "ARITH_NL_CM_QUADRATIC_EQ"; + case InferenceId::ARITH_NL_SPLIT_ZERO: return "ARITH_NL_SPLIT_ZERO"; + case InferenceId::ARITH_NL_SIGN: return "ARITH_NL_SIGN"; + case InferenceId::ARITH_NL_COMPARISON: return "ARITH_NL_COMPARISON"; + case InferenceId::ARITH_NL_INFER_BOUNDS: return "ARITH_NL_INFER_BOUNDS"; + case InferenceId::ARITH_NL_INFER_BOUNDS_NT: + return "ARITH_NL_INFER_BOUNDS_NT"; + case InferenceId::ARITH_NL_FACTOR: return "ARITH_NL_FACTOR"; + case InferenceId::ARITH_NL_RES_INFER_BOUNDS: + return "ARITH_NL_RES_INFER_BOUNDS"; + case InferenceId::ARITH_NL_TANGENT_PLANE: return "ARITH_NL_TANGENT_PLANE"; + case InferenceId::ARITH_NL_T_PURIFY_ARG: return "ARITH_NL_T_PURIFY_ARG"; + case InferenceId::ARITH_NL_T_INIT_REFINE: return "ARITH_NL_T_INIT_REFINE"; + case InferenceId::ARITH_NL_T_PI_BOUND: return "ARITH_NL_T_PI_BOUND"; + case InferenceId::ARITH_NL_T_MONOTONICITY: return "ARITH_NL_T_MONOTONICITY"; + case InferenceId::ARITH_NL_T_SECANT: return "ARITH_NL_T_SECANT"; + case InferenceId::ARITH_NL_T_TANGENT: return "ARITH_NL_T_TANGENT"; + case InferenceId::ARITH_NL_IAND_INIT_REFINE: + return "ARITH_NL_IAND_INIT_REFINE"; + case InferenceId::ARITH_NL_IAND_VALUE_REFINE: + return "ARITH_NL_IAND_VALUE_REFINE"; + case InferenceId::ARITH_NL_IAND_SUM_REFINE: + return "ARITH_NL_IAND_SUM_REFINE"; + case InferenceId::ARITH_NL_IAND_BITWISE_REFINE: + return "ARITH_NL_IAND_BITWISE_REFINE"; + case InferenceId::ARITH_NL_CAD_CONFLICT: return "ARITH_NL_CAD_CONFLICT"; + case InferenceId::ARITH_NL_CAD_EXCLUDED_INTERVAL: + return "ARITH_NL_CAD_EXCLUDED_INTERVAL"; + case InferenceId::ARITH_NL_ICP_CONFLICT: return "ARITH_NL_ICP_CONFLICT"; + case InferenceId::ARITH_NL_ICP_PROPAGATION: + return "ARITH_NL_ICP_PROPAGATION"; case InferenceId::ARRAYS_EXT: return "ARRAYS_EXT"; case InferenceId::ARRAYS_READ_OVER_WRITE: return "ARRAYS_READ_OVER_WRITE"; diff --git a/src/theory/inference_id.h b/src/theory/inference_id.h index 6dacee33c..2891d5132 100644 --- a/src/theory/inference_id.h +++ b/src/theory/inference_id.h @@ -41,12 +41,16 @@ namespace theory { enum class InferenceId { // ---------------------------------- arith theory - //-------------------- core + //-------------------- preprocessing + ARITH_PP_ELIM_OPERATORS, + //-------------------- nonlinear core // simple congruence x=y => f(x)=f(y) ARITH_NL_CONGRUENCE, // shared term value split (for naive theory combination) ARITH_NL_SHARED_TERM_VALUE_SPLIT, - //-------------------- incremental linearization solver + // checkModel found a conflict with a quadratic equality + ARITH_NL_CM_QUADRATIC_EQ, + //-------------------- nonlinear incremental linearization solver // splitting on zero (NlSolver::checkSplitZero) ARITH_NL_SPLIT_ZERO, // based on sign (NlSolver::checkMonomialSign) @@ -63,7 +67,7 @@ enum class InferenceId ARITH_NL_RES_INFER_BOUNDS, // tangent planes (NlSolver::checkTangentPlanes) ARITH_NL_TANGENT_PLANE, - //-------------------- transcendental solver + //-------------------- nonlinear transcendental solver // purification of arguments to transcendental functions ARITH_NL_T_PURIFY_ARG, // initial refinement (TranscendentalSolver::checkTranscendentalInitialRefine) @@ -76,7 +80,7 @@ enum class InferenceId ARITH_NL_T_TANGENT, // secant refinement, the dual of the above inference ARITH_NL_T_SECANT, - //-------------------- iand solver + //-------------------- nonlinear iand solver // initial refinements (IAndSolver::checkInitialRefine) ARITH_NL_IAND_INIT_REFINE, // value refinements (IAndSolver::checkFullRefine) @@ -85,12 +89,12 @@ enum class InferenceId ARITH_NL_IAND_SUM_REFINE, // bitwise refinements (IAndSolver::checkFullRefine) ARITH_NL_IAND_BITWISE_REFINE, - //-------------------- cad solver + //-------------------- nonlinear cad solver // conflict / infeasible subset obtained from cad ARITH_NL_CAD_CONFLICT, // excludes an interval for a single variable ARITH_NL_CAD_EXCLUDED_INTERVAL, - //-------------------- icp solver + //-------------------- nonlinear icp solver // conflict obtained from icp ARITH_NL_ICP_CONFLICT, // propagation / contraction of variable bounds from icp -- 2.30.2