From 39df95de07a85121f5f12404afcaae48d90e0a67 Mon Sep 17 00:00:00 2001 From: Gereon Kremer Date: Fri, 18 Dec 2020 18:11:51 +0100 Subject: [PATCH] (proof-new) Setup proof infrastructure for transcendental solver (#5703) This PR introduces the infrastructure for adding proofs to the transcendental solver: a CDProofSet to easily create new proofs a proof checker --- src/CMakeLists.txt | 2 + src/theory/arith/nl/nonlinear_extension.cpp | 2 +- .../arith/nl/transcendental/proof_checker.cpp | 55 ++++++++++++++++++ .../arith/nl/transcendental/proof_checker.h | 58 +++++++++++++++++++ .../transcendental/transcendental_solver.cpp | 7 ++- .../nl/transcendental/transcendental_solver.h | 5 +- .../transcendental/transcendental_state.cpp | 24 +++++++- .../nl/transcendental/transcendental_state.h | 30 +++++++++- 8 files changed, 176 insertions(+), 7 deletions(-) create mode 100644 src/theory/arith/nl/transcendental/proof_checker.cpp create mode 100644 src/theory/arith/nl/transcendental/proof_checker.h diff --git a/src/CMakeLists.txt b/src/CMakeLists.txt index 8dc30e549..82e88f330 100644 --- a/src/CMakeLists.txt +++ b/src/CMakeLists.txt @@ -391,6 +391,8 @@ libcvc4_add_sources( theory/arith/nl/strategy.h theory/arith/nl/transcendental/exponential_solver.cpp theory/arith/nl/transcendental/exponential_solver.h + theory/arith/nl/transcendental/proof_checker.cpp + theory/arith/nl/transcendental/proof_checker.h theory/arith/nl/transcendental/sine_solver.cpp theory/arith/nl/transcendental/sine_solver.h theory/arith/nl/transcendental/taylor_generator.cpp diff --git a/src/theory/arith/nl/nonlinear_extension.cpp b/src/theory/arith/nl/nonlinear_extension.cpp index d52095e95..b97a53f95 100644 --- a/src/theory/arith/nl/nonlinear_extension.cpp +++ b/src/theory/arith/nl/nonlinear_extension.cpp @@ -47,7 +47,7 @@ NonlinearExtension::NonlinearExtension(TheoryArith& containing, containing.getUserContext(), containing.getOutputChannel()), d_model(containing.getSatContext()), - d_trSlv(d_im, d_model), + d_trSlv(d_im, d_model, pnm, containing.getUserContext()), d_extState(d_im, d_model, pnm, containing.getUserContext()), d_factoringSlv(d_im, d_model), d_monomialBoundsSlv(&d_extState), diff --git a/src/theory/arith/nl/transcendental/proof_checker.cpp b/src/theory/arith/nl/transcendental/proof_checker.cpp new file mode 100644 index 000000000..d407621e9 --- /dev/null +++ b/src/theory/arith/nl/transcendental/proof_checker.cpp @@ -0,0 +1,55 @@ +/********************* */ +/*! \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 proof checker for transcendentals + **/ + +#include "theory/arith/nl/transcendental/proof_checker.h" + +#include "expr/sequence.h" +#include "theory/arith/arith_utilities.h" +#include "theory/arith/nl/transcendental/taylor_generator.h" +#include "theory/rewriter.h" + +using namespace CVC4::kind; + +namespace CVC4 { +namespace theory { +namespace arith { +namespace nl { +namespace transcendental { + +void TranscendentalProofRuleChecker::registerTo(ProofChecker* pc) +{ +} + +Node TranscendentalProofRuleChecker::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-trans-checker") << "Checking " << id << std::endl; + for (const auto& c : children) + { + Trace("nl-trans-checker") << "\t" << c << std::endl; + } + return Node::null(); +} + +} // namespace transcendental +} // namespace nl +} // namespace arith +} // namespace theory +} // namespace CVC4 diff --git a/src/theory/arith/nl/transcendental/proof_checker.h b/src/theory/arith/nl/transcendental/proof_checker.h new file mode 100644 index 000000000..2634d70b1 --- /dev/null +++ b/src/theory/arith/nl/transcendental/proof_checker.h @@ -0,0 +1,58 @@ +/********************* */ +/*! \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 Proof checker utility for transcendental solver + **/ + +#include "cvc4_private.h" + +#ifndef CVC4__THEORY__ARITH__NL__TRANSCENDENTAL__PROOF_CHECKER_H +#define CVC4__THEORY__ARITH__NL__TRANSCENDENTAL__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 { +namespace transcendental { + +/** + * A checker for NlExt proofs + * + * This proof checker takes care of all proofs for lemmas from the + * transcendental subsolver. + */ +class TranscendentalProofRuleChecker : public ProofRuleChecker +{ + public: + TranscendentalProofRuleChecker() = default; + ~TranscendentalProofRuleChecker() = 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 transcendental +} // namespace nl +} // namespace arith +} // namespace theory +} // namespace CVC4 + +#endif /* CVC4__THEORY__STRINGS__PROOF_CHECKER_H */ diff --git a/src/theory/arith/nl/transcendental/transcendental_solver.cpp b/src/theory/arith/nl/transcendental/transcendental_solver.cpp index c2841c135..233667e5b 100644 --- a/src/theory/arith/nl/transcendental/transcendental_solver.cpp +++ b/src/theory/arith/nl/transcendental/transcendental_solver.cpp @@ -33,8 +33,11 @@ namespace arith { namespace nl { namespace transcendental { -TranscendentalSolver::TranscendentalSolver(InferenceManager& im, NlModel& m) - : d_tstate(im, m), d_expSlv(&d_tstate), d_sineSlv(&d_tstate) +TranscendentalSolver::TranscendentalSolver(InferenceManager& im, + NlModel& m, + ProofNodeManager* pnm, + context::UserContext* c) + : d_tstate(im, m, pnm, c), d_expSlv(&d_tstate), d_sineSlv(&d_tstate) { d_taylor_degree = options::nlExtTfTaylorDegree(); } diff --git a/src/theory/arith/nl/transcendental/transcendental_solver.h b/src/theory/arith/nl/transcendental/transcendental_solver.h index 64f6db163..8135ba1fb 100644 --- a/src/theory/arith/nl/transcendental/transcendental_solver.h +++ b/src/theory/arith/nl/transcendental/transcendental_solver.h @@ -65,7 +65,10 @@ namespace transcendental { class TranscendentalSolver { public: - TranscendentalSolver(InferenceManager& im, NlModel& m); + TranscendentalSolver(InferenceManager& im, + NlModel& m, + ProofNodeManager* pnm, + context::UserContext* c); ~TranscendentalSolver(); /** init last call diff --git a/src/theory/arith/nl/transcendental/transcendental_state.cpp b/src/theory/arith/nl/transcendental/transcendental_state.cpp index 6dbb847a6..67db4f2cc 100644 --- a/src/theory/arith/nl/transcendental/transcendental_state.cpp +++ b/src/theory/arith/nl/transcendental/transcendental_state.cpp @@ -23,14 +23,34 @@ namespace arith { namespace nl { namespace transcendental { -TranscendentalState::TranscendentalState(InferenceManager& im, NlModel& model) - : d_im(im), d_model(model) +TranscendentalState::TranscendentalState(InferenceManager& im, + NlModel& model, + ProofNodeManager* pnm, + context::UserContext* c) + : d_im(im), d_model(model), d_pnm(pnm), d_ctx(c) { d_true = NodeManager::currentNM()->mkConst(true); d_false = NodeManager::currentNM()->mkConst(false); 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-trans")); + d_proofChecker.reset(new TranscendentalProofRuleChecker()); + d_proofChecker->registerTo(pnm->getChecker()); + } +} + +bool TranscendentalState::isProofEnabled() const +{ + return d_proof.get() != nullptr; +} + +CDProof* TranscendentalState::getProof() +{ + Assert(isProofEnabled()); + return d_proof->allocateProof(d_ctx); } void TranscendentalState::init(const std::vector& xts, diff --git a/src/theory/arith/nl/transcendental/transcendental_state.h b/src/theory/arith/nl/transcendental/transcendental_state.h index f940ae2e3..93ac4627a 100644 --- a/src/theory/arith/nl/transcendental/transcendental_state.h +++ b/src/theory/arith/nl/transcendental/transcendental_state.h @@ -16,8 +16,10 @@ #define CVC4__THEORY__ARITH__NL__TRANSCENDENTAL__TRANSCENDENTAL_STATE_H #include "expr/node.h" +#include "expr/proof_set.h" #include "theory/arith/inference_manager.h" #include "theory/arith/nl/nl_model.h" +#include "theory/arith/nl/transcendental/proof_checker.h" #include "theory/arith/nl/transcendental/taylor_generator.h" namespace CVC4 { @@ -52,7 +54,19 @@ inline std::ostream& operator<<(std::ostream& os, Convexity c) { */ struct TranscendentalState { - TranscendentalState(InferenceManager& im, NlModel& model); + TranscendentalState(InferenceManager& im, + NlModel& model, + ProofNodeManager* pnm, + context::UserContext* c); + + /** + * Checks whether proofs are enabled. + */ + bool isProofEnabled() const; + /** + * Creates and returns a new LazyCDProof that can be used to prove some lemma. + */ + CDProof* getProof(); /** init last call * @@ -151,6 +165,20 @@ struct TranscendentalState NlModel& d_model; /** Utility to compute taylor approximations */ TaylorGenerator d_taylor; + /** + * 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; + + /** The proof checker for transcendental proofs */ + std::unique_ptr d_proofChecker; /** * Some transcendental functions f(t) are "purified", e.g. we add -- 2.30.2