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
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
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<CDProof>(d_pnm, d_ctx, "nl-ext"));
+ }
}
void ExtState::init(const std::vector<Node>& 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
#include <vector>
#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"
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<Node>& 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;
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<CDProofSet<CDProof>> d_proof;
// information about monomials
std::vector<Node> d_ms;
--- /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 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<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-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
--- /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 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<Node>& children,
+ const std::vector<Node>& args) override;
+};
+
+} // namespace nl
+} // namespace arith
+} // namespace theory
+} // namespace CVC4
+
+#endif /* CVC4__THEORY__STRINGS__PROOF_CHECKER_H */
NonlinearExtension::NonlinearExtension(TheoryArith& containing,
ArithState& state,
- eq::EqualityEngine* ee)
+ eq::EqualityEngine* ee,
+ ProofNodeManager* pnm)
: d_containing(containing),
d_im(containing.getInferenceManager()),
d_needsLastCall(false),
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),
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() {}
#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"
typedef context::CDHashSet<Node, NodeHashFunction> 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.
* 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).
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();
projects / cvc5.git / commitdiff