From 1753106f61bca87513a84493b643e2a7e245e0f5 Mon Sep 17 00:00:00 2001 From: Gereon Kremer Date: Thu, 17 Dec 2020 17:12:15 +0100 Subject: [PATCH] (proof-new) Prepare nonlinear extension and nl-ext for proofs. (#5697) This PR prepares the nonlinear extension itself and the nl-ext part for proofs. In particular we add a proof checker for nl-ext we add a CDProofSet for nl-ext --- src/CMakeLists.txt | 2 + src/theory/arith/nl/ext/ext_state.cpp | 19 ++++++- src/theory/arith/nl/ext/ext_state.h | 27 +++++++++- src/theory/arith/nl/ext/proof_checker.cpp | 53 +++++++++++++++++++ src/theory/arith/nl/ext/proof_checker.h | 56 +++++++++++++++++++++ src/theory/arith/nl/nonlinear_extension.cpp | 11 +++- src/theory/arith/nl/nonlinear_extension.h | 8 ++- src/theory/arith/theory_arith.cpp | 2 +- 8 files changed, 170 insertions(+), 8 deletions(-) create mode 100644 src/theory/arith/nl/ext/proof_checker.cpp create mode 100644 src/theory/arith/nl/ext/proof_checker.h diff --git a/src/CMakeLists.txt b/src/CMakeLists.txt index ca124d90b..8dc30e549 100644 --- a/src/CMakeLists.txt +++ b/src/CMakeLists.txt @@ -357,6 +357,8 @@ libcvc4_add_sources( theory/arith/nl/ext/monomial_check.h theory/arith/nl/ext/ext_state.cpp theory/arith/nl/ext/ext_state.h + theory/arith/nl/ext/proof_checker.cpp + theory/arith/nl/ext/proof_checker.h theory/arith/nl/ext/split_zero_check.cpp theory/arith/nl/ext/split_zero_check.h theory/arith/nl/ext/tangent_plane_check.cpp diff --git a/src/theory/arith/nl/ext/ext_state.cpp b/src/theory/arith/nl/ext/ext_state.cpp index d850ff34e..5da5319a1 100644 --- a/src/theory/arith/nl/ext/ext_state.cpp +++ b/src/theory/arith/nl/ext/ext_state.cpp @@ -26,14 +26,21 @@ namespace theory { namespace arith { namespace nl { -ExtState::ExtState(InferenceManager& im, NlModel& model, context::Context* c) - : d_im(im), d_model(model) +ExtState::ExtState(InferenceManager& im, + NlModel& model, + ProofNodeManager* pnm, + context::UserContext* c) + : d_im(im), d_model(model), d_pnm(pnm), d_ctx(c) { d_false = NodeManager::currentNM()->mkConst(false); d_true = NodeManager::currentNM()->mkConst(true); d_zero = NodeManager::currentNM()->mkConst(Rational(0)); d_one = NodeManager::currentNM()->mkConst(Rational(1)); d_neg_one = NodeManager::currentNM()->mkConst(Rational(-1)); + if (d_pnm != nullptr) + { + d_proof.reset(new CDProofSet(d_pnm, d_ctx, "nl-ext")); + } } void ExtState::init(const std::vector& xts) @@ -89,6 +96,14 @@ void ExtState::init(const std::vector& xts) Trace("nl-ext") << "We have " << d_ms.size() << " monomials." << std::endl; } +bool ExtState::isProofEnabled() const { return d_proof.get() != nullptr; } + +CDProof* ExtState::getProof() +{ + Assert(isProofEnabled()); + return d_proof->allocateProof(d_ctx); +} + } // namespace nl } // namespace arith } // namespace theory diff --git a/src/theory/arith/nl/ext/ext_state.h b/src/theory/arith/nl/ext/ext_state.h index adf576c8b..863b3f879 100644 --- a/src/theory/arith/nl/ext/ext_state.h +++ b/src/theory/arith/nl/ext/ext_state.h @@ -18,7 +18,7 @@ #include #include "expr/node.h" -#include "expr/proof.h" +#include "expr/proof_set.h" #include "theory/arith/inference_manager.h" #include "theory/arith/nl/ext/monomial.h" #include "theory/arith/nl/nl_model.h" @@ -30,10 +30,22 @@ namespace nl { struct ExtState { - ExtState(InferenceManager& im, NlModel& model, context::Context* c); + ExtState(InferenceManager& im, + NlModel& model, + ProofNodeManager* pnm, + context::UserContext* c); void init(const std::vector& xts); + /** + * Checks whether proofs are enabled. + */ + bool isProofEnabled() const; + /** + * Creates and returns a new LazyCDProof that can be used to prove some lemma. + */ + CDProof* getProof(); + Node d_false; Node d_true; Node d_zero; @@ -44,6 +56,17 @@ struct ExtState InferenceManager& d_im; /** Reference to the non-linear model object */ NlModel& d_model; + /** + * Pointer to the current proof node manager. nullptr, if proofs are + * disabled. + */ + ProofNodeManager* d_pnm; + /** The user context. */ + context::UserContext* d_ctx; + /** + * A CDProofSet that hands out CDProof objects for lemmas. + */ + std::unique_ptr> d_proof; // information about monomials std::vector d_ms; diff --git a/src/theory/arith/nl/ext/proof_checker.cpp b/src/theory/arith/nl/ext/proof_checker.cpp new file mode 100644 index 000000000..57ef378b6 --- /dev/null +++ b/src/theory/arith/nl/ext/proof_checker.cpp @@ -0,0 +1,53 @@ +/********************* */ +/*! \file proof_checker.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 NlExt proof checker + **/ + +#include "theory/arith/nl/ext/proof_checker.h" + +#include "expr/sequence.h" +#include "theory/arith/arith_utilities.h" +#include "theory/rewriter.h" + +using namespace CVC4::kind; + +namespace CVC4 { +namespace theory { +namespace arith { +namespace nl { + +void ExtProofRuleChecker::registerTo(ProofChecker* pc) +{ +} + +Node ExtProofRuleChecker::checkInternal(PfRule id, + const std::vector& children, + const std::vector& args) +{ + NodeManager* nm = NodeManager::currentNM(); + auto zero = nm->mkConst(0); + auto one = nm->mkConst(1); + auto mone = nm->mkConst(-1); + auto pi = nm->mkNullaryOperator(nm->realType(), Kind::PI); + auto mpi = nm->mkNode(Kind::MULT, mone, pi); + Trace("nl-ext-checker") << "Checking " << id << std::endl; + for (const auto& c : children) + { + Trace("nl-ext-checker") << "\t" << c << std::endl; + } + return Node::null(); +} + +} // namespace nl +} // namespace arith +} // namespace theory +} // namespace CVC4 diff --git a/src/theory/arith/nl/ext/proof_checker.h b/src/theory/arith/nl/ext/proof_checker.h new file mode 100644 index 000000000..88df46110 --- /dev/null +++ b/src/theory/arith/nl/ext/proof_checker.h @@ -0,0 +1,56 @@ +/********************* */ +/*! \file proof_checker.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 NlExt proof checker utility + **/ + +#include "cvc4_private.h" + +#ifndef CVC4__THEORY__ARITH__NL__EXT__PROOF_CHECKER_H +#define CVC4__THEORY__ARITH__NL__EXT__PROOF_CHECKER_H + +#include "expr/node.h" +#include "expr/proof_checker.h" +#include "expr/proof_node.h" + +namespace CVC4 { +namespace theory { +namespace arith { +namespace nl { + +/** + * A checker for NlExt proofs + * + * This proof checker takes care of all proofs for lemmas from the ext + * subsolver. + */ +class ExtProofRuleChecker : public ProofRuleChecker +{ + public: + ExtProofRuleChecker() = default; + ~ExtProofRuleChecker() = default; + + /** Register all rules owned by this rule checker in pc. */ + void registerTo(ProofChecker* pc) override; + + protected: + /** Return the conclusion of the given proof step, or null if it is invalid */ + Node checkInternal(PfRule id, + const std::vector& children, + const std::vector& args) override; +}; + +} // namespace nl +} // namespace arith +} // namespace theory +} // namespace CVC4 + +#endif /* CVC4__THEORY__STRINGS__PROOF_CHECKER_H */ diff --git a/src/theory/arith/nl/nonlinear_extension.cpp b/src/theory/arith/nl/nonlinear_extension.cpp index dff43e568..e4a71b34d 100644 --- a/src/theory/arith/nl/nonlinear_extension.cpp +++ b/src/theory/arith/nl/nonlinear_extension.cpp @@ -35,7 +35,8 @@ namespace nl { NonlinearExtension::NonlinearExtension(TheoryArith& containing, ArithState& state, - eq::EqualityEngine* ee) + eq::EqualityEngine* ee, + ProofNodeManager* pnm) : d_containing(containing), d_im(containing.getInferenceManager()), d_needsLastCall(false), @@ -47,7 +48,7 @@ NonlinearExtension::NonlinearExtension(TheoryArith& containing, containing.getOutputChannel()), d_model(containing.getSatContext()), d_trSlv(d_im, d_model), - d_extState(d_im, d_model, containing.getSatContext()), + d_extState(d_im, d_model, pnm, containing.getUserContext()), d_factoringSlv(d_im, d_model), d_monomialBoundsSlv(&d_extState), d_monomialSlv(&d_extState), @@ -67,6 +68,12 @@ NonlinearExtension::NonlinearExtension(TheoryArith& containing, d_zero = NodeManager::currentNM()->mkConst(Rational(0)); d_one = NodeManager::currentNM()->mkConst(Rational(1)); d_neg_one = NodeManager::currentNM()->mkConst(Rational(-1)); + + ProofChecker* pc = pnm != nullptr ? pnm->getChecker() : nullptr; + if (pc != nullptr) + { + d_proofChecker.registerTo(pc); + } } NonlinearExtension::~NonlinearExtension() {} diff --git a/src/theory/arith/nl/nonlinear_extension.h b/src/theory/arith/nl/nonlinear_extension.h index 2de5daeb6..77031ee1c 100644 --- a/src/theory/arith/nl/nonlinear_extension.h +++ b/src/theory/arith/nl/nonlinear_extension.h @@ -29,6 +29,7 @@ #include "theory/arith/nl/ext/factoring_check.h" #include "theory/arith/nl/ext/monomial_bounds_check.h" #include "theory/arith/nl/ext/monomial_check.h" +#include "theory/arith/nl/ext/proof_checker.h" #include "theory/arith/nl/ext/split_zero_check.h" #include "theory/arith/nl/ext/tangent_plane_check.h" #include "theory/arith/nl/ext_theory_callback.h" @@ -76,7 +77,10 @@ class NonlinearExtension typedef context::CDHashSet NodeSet; public: - NonlinearExtension(TheoryArith& containing, ArithState& state, eq::EqualityEngine* ee); + NonlinearExtension(TheoryArith& containing, + ArithState& state, + eq::EqualityEngine* ee, + ProofNodeManager* pnm); ~NonlinearExtension(); /** * Does non-context dependent setup for a node connected to a theory. @@ -252,6 +256,8 @@ class NonlinearExtension * transcendental functions. */ transcendental::TranscendentalSolver d_trSlv; + /** The proof checker for proofs of the nlext. */ + ExtProofRuleChecker d_proofChecker; /** * Holds common lookup data for the checks implemented in the "nl-ext" * solvers (from Cimatti et al., TACAS 2017). diff --git a/src/theory/arith/theory_arith.cpp b/src/theory/arith/theory_arith.cpp index b8cead4fc..d1dd4bb63 100644 --- a/src/theory/arith/theory_arith.cpp +++ b/src/theory/arith/theory_arith.cpp @@ -82,7 +82,7 @@ void TheoryArith::finishInit() if (logicInfo.isTheoryEnabled(THEORY_ARITH) && !logicInfo.isLinear()) { d_nonlinearExtension.reset( - new nl::NonlinearExtension(*this, d_astate, d_equalityEngine)); + new nl::NonlinearExtension(*this, d_astate, d_equalityEngine, d_pnm)); } // finish initialize internally d_internal->finishInit(); -- 2.30.2