This PR introduces the infrastructure for adding proofs to the transcendental solver:
a CDProofSet to easily create new proofs
a proof checker
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
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),
--- /dev/null
+/********************* */
+/*! \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<Node>& children, const std::vector<Node>& args)
+{
+ NodeManager* nm = NodeManager::currentNM();
+ auto zero = nm->mkConst<Rational>(0);
+ auto one = nm->mkConst<Rational>(1);
+ auto mone = nm->mkConst<Rational>(-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
--- /dev/null
+/********************* */
+/*! \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<Node>& children,
+ const std::vector<Node>& args) override;
+};
+
+} // namespace transcendental
+} // namespace nl
+} // namespace arith
+} // namespace theory
+} // namespace CVC4
+
+#endif /* CVC4__THEORY__STRINGS__PROOF_CHECKER_H */
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();
}
class TranscendentalSolver
{
public:
- TranscendentalSolver(InferenceManager& im, NlModel& m);
+ TranscendentalSolver(InferenceManager& im,
+ NlModel& m,
+ ProofNodeManager* pnm,
+ context::UserContext* c);
~TranscendentalSolver();
/** init last call
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<CDProof>(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<Node>& xts,
#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 {
*/
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
*
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<CDProofSet<CDProof>> d_proof;
+
+ /** The proof checker for transcendental proofs */
+ std::unique_ptr<TranscendentalProofRuleChecker> d_proofChecker;
/**
* Some transcendental functions f(t) are "purified", e.g. we add
projects / cvc5.git / commitdiff