From: Gereon Kremer Date: Wed, 2 Sep 2020 13:48:12 +0000 (+0200) Subject: Add ArithLemma and arith::InferenceManager (#4960) X-Git-Tag: cvc5-1.0.0~2921 X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=02e682821028bc704c57a762dadeb6f82bb70ebf;p=cvc5.git Add ArithLemma and arith::InferenceManager (#4960) This PR adds a new ArithLemma that is essentiall NlLemma, but derived from the new theory::Lemma and meant to be used all across the arithmetic theory. Also, based on theory::InferenceManagerBuffered this PR adds arith::InferenceManager that shall become the sole interface between the arithmetic theory and the OutputChannel. --- diff --git a/src/CMakeLists.txt b/src/CMakeLists.txt index 7a383d0c8..2da04ce66 100644 --- a/src/CMakeLists.txt +++ b/src/CMakeLists.txt @@ -251,6 +251,8 @@ 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_rewriter.cpp @@ -287,6 +289,8 @@ libcvc4_add_sources( theory/arith/fc_simplex.h theory/arith/infer_bounds.cpp theory/arith/infer_bounds.h + theory/arith/inference_manager.cpp + theory/arith/inference_manager.h theory/arith/linear_equality.cpp theory/arith/linear_equality.h theory/arith/matrix.cpp diff --git a/src/theory/arith/arith_lemma.cpp b/src/theory/arith/arith_lemma.cpp new file mode 100644 index 000000000..9bd4df255 --- /dev/null +++ b/src/theory/arith/arith_lemma.cpp @@ -0,0 +1,28 @@ +/********************* */ +/*! \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 new file mode 100644 index 000000000..a06cb83f3 --- /dev/null +++ b/src/theory/arith/arith_lemma.h @@ -0,0 +1,61 @@ +/********************* */ +/*! \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/arith/nl/inference.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, + nl::Inference inf = nl::Inference::UNKNOWN) + : SimpleTheoryLemma(n, p, pg), d_inference(inf) + { + } + virtual ~ArithLemma() {} + + /** The inference id for the lemma */ + nl::Inference d_inference; +}; +/** + * 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/inference_manager.cpp b/src/theory/arith/inference_manager.cpp new file mode 100644 index 000000000..f026aa374 --- /dev/null +++ b/src/theory/arith/inference_manager.cpp @@ -0,0 +1,143 @@ +/********************* */ +/*! \file inference_manager.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 Implementation of the inference manager for the theory of strings. + **/ + +#include "theory/arith/inference_manager.h" + +#include "options/arith_options.h" +#include "theory/arith/theory_arith.h" +#include "theory/rewriter.h" + +namespace CVC4 { +namespace theory { +namespace arith { + +InferenceManager::InferenceManager(TheoryArith& ta, + ArithState& astate, + ProofNodeManager* pnm) + : InferenceManagerBuffered(ta, astate, pnm), d_lemmasPp(ta.getUserContext()) +{ +} + +void InferenceManager::addPendingArithLemma(std::shared_ptr lemma, + bool isWaiting) +{ + lemma->d_node = Rewriter::rewrite(lemma->d_node); + if (hasCachedLemma(lemma->d_node, lemma->d_property)) + { + return; + } + if (isEntailedFalse(*lemma)) + { + if (isWaiting) + { + d_waitingLem.clear(); + } + else + { + d_pendingLem.clear(); + d_theoryState.notifyInConflict(); + } + } + if (isWaiting) + { + d_waitingLem.emplace_back(std::move(lemma)); + } + else + { + addPendingLemma(std::move(lemma)); + } +} +void InferenceManager::addPendingArithLemma(const ArithLemma& lemma, + bool isWaiting) +{ + addPendingArithLemma(std::make_shared(lemma), isWaiting); +} +void InferenceManager::addPendingArithLemma(const Node& lemma, + nl::Inference inftype, + bool isWaiting) +{ + addPendingArithLemma(std::make_shared( + lemma, LemmaProperty::NONE, nullptr, inftype), + isWaiting); +} + +void InferenceManager::flushWaitingLemmas() +{ + for (auto& lem : d_waitingLem) + { + addPendingLemma(std::move(lem)); + } + d_waitingLem.clear(); +} + +void InferenceManager::addConflict(const Node& conf, nl::Inference inftype) +{ + conflict(Rewriter::rewrite(conf)); +} + +std::size_t InferenceManager::numWaitingLemmas() const +{ + return d_waitingLem.size(); +} + +bool InferenceManager::hasCachedLemma(TNode lem, LemmaProperty p) +{ + if (isLemmaPropertyPreprocess(p)) + { + return d_lemmasPp.find(lem) != d_lemmasPp.end(); + } + return TheoryInferenceManager::hasCachedLemma(lem, p); +} + +bool InferenceManager::cacheLemma(TNode lem, LemmaProperty p) +{ + if (isLemmaPropertyPreprocess(p)) + { + if (d_lemmasPp.find(lem) != d_lemmasPp.end()) + { + return false; + } + d_lemmasPp.insert(lem); + return true; + } + return TheoryInferenceManager::cacheLemma(lem, p); +} + +bool InferenceManager::isEntailedFalse(const ArithLemma& lem) +{ + if (options::nlExtEntailConflicts()) + { + Node ch_lemma = lem.d_node.negate(); + ch_lemma = Rewriter::rewrite(ch_lemma); + Trace("arith-inf-manager") << "InferenceManager::Check entailment of " + << ch_lemma << "..." << std::endl; + + std::pair et = d_theory.getValuation().entailmentCheck( + options::TheoryOfMode::THEORY_OF_TYPE_BASED, ch_lemma); + Trace("arith-inf-manager") << "entailment test result : " << et.first << " " + << et.second << std::endl; + if (et.first) + { + Trace("arith-inf-manager") + << "*** Lemma entailed to be in conflict : " << lem.d_node + << std::endl; + return true; + } + } + return false; +} + +} // namespace arith +} // namespace theory +} // namespace CVC4 diff --git a/src/theory/arith/inference_manager.h b/src/theory/arith/inference_manager.h new file mode 100644 index 000000000..3b7190826 --- /dev/null +++ b/src/theory/arith/inference_manager.h @@ -0,0 +1,116 @@ +/********************* */ +/*! \file inference_manager.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 Customized inference manager for the theory of nonlinear arithmetic + **/ + +#include "cvc4_private.h" + +#ifndef CVC4__THEORY__ARITH__INFERENCE_MANAGER_H +#define CVC4__THEORY__ARITH__INFERENCE_MANAGER_H + +#include +#include + +#include "theory/arith/arith_lemma.h" +#include "theory/arith/arith_state.h" +#include "theory/arith/nl/inference.h" +#include "theory/arith/nl/nl_lemma_utils.h" +#include "theory/inference_manager_buffered.h" + +namespace CVC4 { +namespace theory { +namespace arith { + +class TheoryArith; + +/** + * A specialized variant of the InferenceManagerBuffered, tailored to the + * arithmetic theory. + * + * It adds some convenience methods to send ArithLemma and adds a mechanism for + * waiting lemmas that can be flushed into the pending lemmas of the this + * buffered inference manager. + * It also extends the caching mechanism of TheoryInferenceManager to cache + * preprocessing lemmas and non-preprocessing lemmas separately. For the former, + * it uses the cache provided by the TheoryInferenceManager base class. + */ +class InferenceManager : public InferenceManagerBuffered +{ + using NodeSet = context::CDHashSet; + + public: + InferenceManager(TheoryArith& ta, ArithState& astate, ProofNodeManager* pnm); + + /** + * Add a lemma as pending lemma to the 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(std::shared_ptr lemma, + bool isWaiting = false); + /** + * Add a lemma as pending lemma to the 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); + /** + * Add a lemma as pending lemma to the 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, + nl::Inference inftype, + bool isWaiting = false); + + /** + * Flush all waiting lemmas to the this inference manager (as pending + * lemmas). To actually send them, call doPendingLemmas() afterwards. + */ + void flushWaitingLemmas(); + + /** Add a conflict to the this inference manager. */ + void addConflict(const Node& conf, nl::Inference inftype); + + /** Returns the number of pending lemmas. */ + std::size_t numWaitingLemmas() const; + + /** Checks whether the given lemma is already present in the cache. */ + virtual bool hasCachedLemma(TNode lem, LemmaProperty p) override; + + protected: + /** + * Adds the given lemma to the cache. Returns true if it has not been in the + * cache yet. + */ + virtual bool cacheLemma(TNode lem, LemmaProperty p) override; + + private: + /** + * Checks whether the lemma is entailed to be false. In this case, it is a + * conflict. + */ + bool isEntailedFalse(const ArithLemma& lem); + + /** The waiting lemmas. */ + std::vector> d_waitingLem; + + /** cache of all preprocessed lemmas sent on the output channel + * (user-context-dependent) */ + NodeSet d_lemmasPp; +}; + +} // namespace arith +} // namespace theory +} // namespace CVC4 + +#endif diff --git a/src/theory/arith/nl/cad_solver.cpp b/src/theory/arith/nl/cad_solver.cpp index b1f0894fb..ac939c341 100644 --- a/src/theory/arith/nl/cad_solver.cpp +++ b/src/theory/arith/nl/cad_solver.cpp @@ -95,7 +95,7 @@ std::vector CadSolver::checkFull() { lems.emplace_back(nm->mkNode(Kind::OR, mis), Inference::CAD_CONFLICT); } - Trace("nl-cad") << "UNSAT with MIS: " << lems.back().d_lemma << std::endl; + Trace("nl-cad") << "UNSAT with MIS: " << lems.back().d_node << std::endl; } return lems; #else diff --git a/src/theory/arith/nl/nl_lemma_utils.cpp b/src/theory/arith/nl/nl_lemma_utils.cpp index 49eec186e..58a552815 100644 --- a/src/theory/arith/nl/nl_lemma_utils.cpp +++ b/src/theory/arith/nl/nl_lemma_utils.cpp @@ -15,20 +15,26 @@ #include "theory/arith/nl/nl_lemma_utils.h" #include "theory/arith/nl/nl_model.h" +#include "theory/arith/nl/nonlinear_extension.h" namespace CVC4 { namespace theory { namespace arith { namespace nl { -LemmaProperty NlLemma::getLemmaProperty() const +bool NlLemma::process(TheoryInferenceManager* im) { - return d_preprocess ? LemmaProperty::PREPROCESS : LemmaProperty::NONE; + bool res = ArithLemma::process(im); + if (d_nlext != nullptr) + { + d_nlext->processSideEffect(*this); + } + return res; } std::ostream& operator<<(std::ostream& out, NlLemma& n) { - out << n.d_lemma; + out << n.d_node; return out; } diff --git a/src/theory/arith/nl/nl_lemma_utils.h b/src/theory/arith/nl/nl_lemma_utils.h index f40857fda..c6c22c3c6 100644 --- a/src/theory/arith/nl/nl_lemma_utils.h +++ b/src/theory/arith/nl/nl_lemma_utils.h @@ -17,7 +17,9 @@ #include #include + #include "expr/node.h" +#include "theory/arith/arith_lemma.h" #include "theory/arith/nl/inference.h" #include "theory/output_channel.h" @@ -27,6 +29,7 @@ namespace arith { namespace nl { class NlModel; +class NonlinearExtension; /** * The data structure for a single lemma to process by the non-linear solver, @@ -39,19 +42,24 @@ class NlModel; * - A set of secant points to record (for transcendental secant plane * inferences). */ -struct NlLemma +class NlLemma : public ArithLemma { - NlLemma(Node lem, Inference id = Inference::UNKNOWN) - : d_id(id), d_lemma(lem), d_preprocess(false) + public: + NlLemma(Node n, + LemmaProperty p, + ProofGenerator* pg, + nl::Inference inf = nl::Inference::UNKNOWN) + : ArithLemma(n, p, pg, inf) + { + } + NlLemma(Node n, nl::Inference inf = nl::Inference::UNKNOWN) + : ArithLemma(n, LemmaProperty::NONE, nullptr, inf) { } ~NlLemma() {} - /** The inference id for the lemma */ - Inference d_id; - /** The lemma */ - Node d_lemma; - /** Whether to preprocess the lemma */ - bool d_preprocess; + + bool process(TheoryInferenceManager* im) override; + /** secant points to add * * A member (tf, d, c) in this vector indicates that point c should be added @@ -62,8 +70,8 @@ struct NlLemma * Cimatti et al., CADE 2017. */ std::vector > d_secantPoint; - /** get lemma property (preprocess or none) */ - LemmaProperty getLemmaProperty() const; + + NonlinearExtension* d_nlext; }; /** * Writes a non-linear lemma to a stream. diff --git a/src/theory/arith/nl/nl_model.cpp b/src/theory/arith/nl/nl_model.cpp index cfa153a56..fbc38fbc2 100644 --- a/src/theory/arith/nl/nl_model.cpp +++ b/src/theory/arith/nl/nl_model.cpp @@ -326,7 +326,7 @@ bool NlModel::checkModel(const std::vector& assertions, Node v = cb.first; Node pred = nm->mkNode(AND, nm->mkNode(GEQ, v, l), nm->mkNode(GEQ, u, v)); pred = nm->mkNode(OR, mg.negate(), pred); - lemmas.push_back(pred); + lemmas.emplace_back(pred); } } return true; diff --git a/src/theory/arith/nl/nl_solver.cpp b/src/theory/arith/nl/nl_solver.cpp index 521539674..6c20eec76 100644 --- a/src/theory/arith/nl/nl_solver.cpp +++ b/src/theory/arith/nl/nl_solver.cpp @@ -843,7 +843,7 @@ std::vector NlSolver::checkMonomialMagnitude(unsigned c) std::vector nr_lemmas; for (unsigned i = 0; i < lemmas.size(); i++) { - if (r_lemmas.find(lemmas[i].d_lemma) == r_lemmas.end()) + if (r_lemmas.find(lemmas[i].d_node) == r_lemmas.end()) { nr_lemmas.push_back(lemmas[i]); } diff --git a/src/theory/arith/nl/nonlinear_extension.cpp b/src/theory/arith/nl/nonlinear_extension.cpp index 8535396e7..ada6aa11a 100644 --- a/src/theory/arith/nl/nonlinear_extension.cpp +++ b/src/theory/arith/nl/nonlinear_extension.cpp @@ -166,9 +166,9 @@ void NonlinearExtension::sendLemmas(const std::vector& out) { for (const NlLemma& nlem : out) { - Node lem = nlem.d_lemma; - LemmaProperty p = nlem.getLemmaProperty(); - Trace("nl-ext-lemma") << "NonlinearExtension::Lemma : " << nlem.d_id + Node lem = nlem.d_node; + LemmaProperty p = nlem.d_property; + Trace("nl-ext-lemma") << "NonlinearExtension::Lemma : " << nlem.d_inference << " : " << lem << std::endl; d_containing.getOutputChannel().lemma(lem, p); // process the side effect @@ -182,7 +182,7 @@ void NonlinearExtension::sendLemmas(const std::vector& out) { d_lemmas.insert(lem); } - d_stats.d_inferences << nlem.d_id; + d_stats.d_inferences << nlem.d_inference; } } @@ -210,14 +210,15 @@ void NonlinearExtension::computeRelevantAssertions( unsigned NonlinearExtension::filterLemma(NlLemma lem, std::vector& out) { Trace("nl-ext-lemma-debug") - << "NonlinearExtension::Lemma pre-rewrite : " << lem.d_lemma << std::endl; - lem.d_lemma = Rewriter::rewrite(lem.d_lemma); + << "NonlinearExtension::Lemma pre-rewrite : " << lem.d_node << std::endl; + lem.d_node = Rewriter::rewrite(lem.d_node); // get the proper cache - NodeSet& lcache = lem.d_preprocess ? d_lemmasPp : d_lemmas; - if (lcache.find(lem.d_lemma) != lcache.end()) + NodeSet& lcache = + isLemmaPropertyPreprocess(lem.d_property) ? d_lemmasPp : d_lemmas; + if (lcache.find(lem.d_node) != lcache.end()) { Trace("nl-ext-lemma-debug") - << "NonlinearExtension::Lemma duplicate : " << lem.d_lemma << std::endl; + << "NonlinearExtension::Lemma duplicate : " << lem.d_node << std::endl; return 0; } out.emplace_back(lem); @@ -232,7 +233,7 @@ unsigned NonlinearExtension::filterLemmas(std::vector& lemmas, // check if any are entailed to be false for (const NlLemma& lem : lemmas) { - Node ch_lemma = lem.d_lemma.negate(); + 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; @@ -243,7 +244,7 @@ unsigned NonlinearExtension::filterLemmas(std::vector& lemmas, if (et.first) { Trace("nl-ext-et") << "*** Lemma entailed to be in conflict : " - << lem.d_lemma << std::endl; + << lem.d_node << std::endl; // return just this lemma if (filterLemma(lem, out) > 0) { diff --git a/src/theory/arith/nl/nonlinear_extension.h b/src/theory/arith/nl/nonlinear_extension.h index ee58a9e2e..d035b1056 100644 --- a/src/theory/arith/nl/nonlinear_extension.h +++ b/src/theory/arith/nl/nonlinear_extension.h @@ -172,6 +172,9 @@ class NonlinearExtension */ void presolve(); + /** Process side effect se */ + void processSideEffect(const NlLemma& se); + private: /** Model-based refinement * @@ -274,8 +277,6 @@ class NonlinearExtension * Send lemmas in out on the output channel of theory of arithmetic. */ void sendLemmas(const std::vector& out); - /** Process side effect se */ - void processSideEffect(const NlLemma& se); /** cache of all lemmas sent on the output channel (user-context-dependent) */ NodeSet d_lemmas; diff --git a/src/theory/arith/nl/transcendental_solver.cpp b/src/theory/arith/nl/transcendental_solver.cpp index 321818b94..b2ef16459 100644 --- a/src/theory/arith/nl/transcendental_solver.cpp +++ b/src/theory/arith/nl/transcendental_solver.cpp @@ -212,8 +212,8 @@ void TranscendentalSolver::initLastCall(const std::vector& assertions, // note we must do preprocess on this lemma Trace("nl-ext-lemma") << "NonlinearExtension::Lemma : purify : " << lem << std::endl; - NlLemma nlem(lem, Inference::T_PURIFY_ARG); - nlem.d_preprocess = true; + NlLemma nlem( + lem, LemmaProperty::PREPROCESS, nullptr, Inference::T_PURIFY_ARG); lems.emplace_back(nlem); } diff --git a/src/theory/inference_manager_buffered.cpp b/src/theory/inference_manager_buffered.cpp index a1cb9c4e9..df01b4e93 100644 --- a/src/theory/inference_manager_buffered.cpp +++ b/src/theory/inference_manager_buffered.cpp @@ -121,5 +121,13 @@ void InferenceManagerBuffered::clearPendingPhaseRequirements() d_pendingReqPhase.clear(); } + + std::size_t InferenceManagerBuffered::numPendingLemmas() const { + return d_pendingLem.size(); + } + std::size_t InferenceManagerBuffered::numPendingFacts() const { + return d_pendingFact.size(); + } + } // namespace theory } // namespace CVC4 diff --git a/src/theory/inference_manager_buffered.h b/src/theory/inference_manager_buffered.h index e6e7822c5..762b7d4e0 100644 --- a/src/theory/inference_manager_buffered.h +++ b/src/theory/inference_manager_buffered.h @@ -35,7 +35,7 @@ class InferenceManagerBuffered : public TheoryInferenceManager InferenceManagerBuffered(Theory& t, TheoryState& state, ProofNodeManager* pnm); - ~InferenceManagerBuffered() {} + virtual ~InferenceManagerBuffered() {} /** * Have we processed an inference during this call to check? In particular, * this returns true if we have a pending fact or lemma, or have encountered @@ -124,6 +124,11 @@ class InferenceManagerBuffered : public TheoryInferenceManager /** Clear pending phase requirements, without processing */ void clearPendingPhaseRequirements(); + /** Returns the number of pending lemmas. */ + std::size_t numPendingLemmas() const; + /** Returns the number of pending facts. */ + std::size_t numPendingFacts() const; + protected: /** A set of pending inferences to be processed as lemmas */ std::vector> d_pendingLem;