From 6478f414ad7d6dcbf597db037e81d97175757605 Mon Sep 17 00:00:00 2001 From: Gereon Kremer Date: Wed, 24 Feb 2021 16:04:59 +0100 Subject: (proof-new) Add proofs for CAD solver (#5981) This PR adds proofs for the CAD solver, based on the proof generator from the previous PR. Note that the level of detail of these CAD proofs is significantly higher than for other proofs. Making these proofs more fine-grained and maybe at some point accessible to proof checkers is probably still quite a bit of work. Thus, the CAD proof rules are both trusted rules for now. --- src/theory/arith/nl/cad/cdcac.cpp | 75 +++++++++++++++++++++++++++-- src/theory/arith/nl/cad/cdcac.h | 23 +++++++-- src/theory/arith/nl/cad_solver.cpp | 31 +++++++++--- src/theory/arith/nl/cad_solver.h | 8 ++- src/theory/arith/nl/nonlinear_extension.cpp | 2 +- 5 files changed, 122 insertions(+), 17 deletions(-) (limited to 'src/theory') diff --git a/src/theory/arith/nl/cad/cdcac.cpp b/src/theory/arith/nl/cad/cdcac.cpp index d076438f5..df3ba37f3 100644 --- a/src/theory/arith/nl/cad/cdcac.cpp +++ b/src/theory/arith/nl/cad/cdcac.cpp @@ -39,11 +39,15 @@ namespace arith { namespace nl { namespace cad { -CDCAC::CDCAC() {} - -CDCAC::CDCAC(const std::vector& ordering) +CDCAC::CDCAC(context::Context* ctx, + ProofNodeManager* pnm, + const std::vector& ordering) : d_variableOrdering(ordering) { + if (pnm != nullptr) + { + d_proof.reset(new CADProofGenerator(ctx, pnm)); + } } void CDCAC::reset() @@ -120,6 +124,17 @@ std::vector CDCAC::getUnsatIntervals(std::size_t cur_variable) if (!is_minus_infinity(get_lower(i))) l = m; if (!is_plus_infinity(get_upper(i))) u = m; res.emplace_back(CACInterval{i, l, u, m, d, {n}}); + if (isProofEnabled()) + { + d_proof->addDirect( + d_constraints.varMapper()(d_variableOrdering[cur_variable]), + d_constraints.varMapper(), + p, + d_assignment, + sc, + i, + n); + } } } pruneRedundantIntervals(res); @@ -335,6 +350,10 @@ CACInterval CDCAC::intervalFromCharacterization( std::vector CDCAC::getUnsatCover(std::size_t curVariable, bool returnFirstInterval) { + if (isProofEnabled()) + { + d_proof->startRecursive(); + } Trace("cdcac") << "Looking for unsat cover for " << d_variableOrdering[curVariable] << std::endl; std::vector intervals = getUnsatIntervals(curVariable); @@ -373,6 +392,10 @@ std::vector CDCAC::getUnsatCover(std::size_t curVariable, Trace("cdcac") << "Found full assignment: " << d_assignment << std::endl; return {}; } + if (isProofEnabled()) + { + d_proof->startScope(); + } // Recurse to next variable auto cov = getUnsatCover(curVariable + 1); if (cov.empty()) @@ -391,6 +414,16 @@ std::vector CDCAC::getUnsatCover(std::size_t curVariable, intervalFromCharacterization(characterization, curVariable, sample); newInterval.d_origins = collectConstraints(cov); intervals.emplace_back(newInterval); + if (isProofEnabled()) + { + auto cell = d_proof->constructCell( + d_constraints.varMapper()(d_variableOrdering[curVariable]), + newInterval, + d_assignment, + sample, + d_constraints.varMapper()); + d_proof->endScope(cell); + } if (returnFirstInterval) { @@ -421,9 +454,31 @@ std::vector CDCAC::getUnsatCover(std::size_t curVariable, Trace("cdcac") << "-> " << i.d_interval << std::endl; } } + if (isProofEnabled()) + { + d_proof->endRecursive(); + } return intervals; } +void CDCAC::startNewProof() +{ + if (isProofEnabled()) + { + d_proof->startNewProof(); + } +} + +ProofGenerator* CDCAC::closeProof(const std::vector& assertions) +{ + if (isProofEnabled()) + { + d_proof->endScope(assertions); + return d_proof->getProofGenerator(); + } + return nullptr; +} + bool CDCAC::checkIntegrality(std::size_t cur_variable, const poly::Value& value) { Node var = d_constraints.varMapper()(d_variableOrdering[cur_variable]); @@ -470,7 +525,19 @@ bool CDCAC::hasRootBelow(const poly::Polynomial& p, void CDCAC::pruneRedundantIntervals(std::vector& intervals) { - cleanIntervals(intervals); + if (isProofEnabled()) + { + std::vector allIntervals = intervals; + cleanIntervals(intervals); + d_proof->pruneChildren([&allIntervals, &intervals](std::size_t i) { + return std::find(intervals.begin(), intervals.end(), allIntervals[i]) + != intervals.end(); + }); + } + else + { + cleanIntervals(intervals); + } } } // namespace cad diff --git a/src/theory/arith/nl/cad/cdcac.h b/src/theory/arith/nl/cad/cdcac.h index f9294fdf1..4511d0c55 100644 --- a/src/theory/arith/nl/cad/cdcac.h +++ b/src/theory/arith/nl/cad/cdcac.h @@ -30,6 +30,7 @@ #include "theory/arith/nl/cad/cdcac_utils.h" #include "theory/arith/nl/cad/constraints.h" +#include "theory/arith/nl/cad/proof_generator.h" #include "theory/arith/nl/cad/variable_ordering.h" #include "theory/arith/nl/nl_model.h" @@ -46,10 +47,10 @@ namespace cad { class CDCAC { public: - /** Initialize without a variable ordering. */ - CDCAC(); /** Initialize this method with the given variable ordering. */ - CDCAC(const std::vector& ordering); + CDCAC(context::Context* ctx, + ProofNodeManager* pnm, + const std::vector& ordering = {}); /** Reset this instance. */ void reset(); @@ -138,7 +139,20 @@ class CDCAC std::vector getUnsatCover(std::size_t curVariable = 0, bool returnFirstInterval = false); + void startNewProof(); + /** + * Finish the generated proof (if proofs are enabled) with a scope over the + * given assertions. + */ + ProofGenerator* closeProof(const std::vector& assertions); + + /** Get the proof generator */ + CADProofGenerator* getProof() { return d_proof.get(); } + private: + /** Check whether proofs are enabled */ + bool isProofEnabled() const { return d_proof != nullptr; } + /** * Check whether the current sample satisfies the integrality condition of the * current variable. Returns true if the variable is not integral or the @@ -187,6 +201,9 @@ class CDCAC /** The linear assignment used as an initial guess. */ std::vector d_initialAssignment; + + /** The proof generator */ + std::unique_ptr d_proof; }; } // namespace cad diff --git a/src/theory/arith/nl/cad_solver.cpp b/src/theory/arith/nl/cad_solver.cpp index 83ceb1182..74c0457a8 100644 --- a/src/theory/arith/nl/cad_solver.cpp +++ b/src/theory/arith/nl/cad_solver.cpp @@ -29,14 +29,31 @@ namespace theory { namespace arith { namespace nl { -CadSolver::CadSolver(InferenceManager& im, NlModel& model) - : d_foundSatisfiability(false), d_im(im), d_model(model) +CadSolver::CadSolver(InferenceManager& im, + NlModel& model, + context::Context* ctx, + ProofNodeManager* pnm) + : +#ifdef CVC4_POLY_IMP + d_CAC(ctx, pnm), +#endif + d_foundSatisfiability(false), + d_im(im), + d_model(model) { d_ranVariable = NodeManager::currentNM()->mkSkolem("__z", NodeManager::currentNM()->realType(), "", NodeManager::SKOLEM_EXACT_NAME); +#ifdef CVC4_POLY_IMP + ProofChecker* pc = pnm != nullptr ? pnm->getChecker() : nullptr; + if (pc != nullptr) + { + // add checkers + d_proofChecker.registerTo(pc); + } +#endif } CadSolver::~CadSolver() {} @@ -75,6 +92,7 @@ void CadSolver::checkFull() Trace("nl-cad") << "No constraints. Return." << std::endl; return; } + d_CAC.startNewProof(); auto covering = d_CAC.getUnsatCover(); if (covering.empty()) { @@ -88,12 +106,9 @@ void CadSolver::checkFull() Trace("nl-cad") << "Collected MIS: " << mis << std::endl; Assert(!mis.empty()) << "Infeasible subset can not be empty"; Trace("nl-cad") << "UNSAT with MIS: " << mis << std::endl; - for (auto& n : mis) - { - n = n.negate(); - } - d_im.addPendingLemma(NodeManager::currentNM()->mkOr(mis), - InferenceId::ARITH_NL_CAD_CONFLICT); + Node lem = NodeManager::currentNM()->mkAnd(mis).negate(); + ProofGenerator* proof = d_CAC.closeProof(mis); + d_im.addPendingLemma(lem, InferenceId::ARITH_NL_CAD_CONFLICT, proof); } #else Warning() << "Tried to use CadSolver but libpoly is not available. Compile " diff --git a/src/theory/arith/nl/cad_solver.h b/src/theory/arith/nl/cad_solver.h index 4d537213f..21fbbab2e 100644 --- a/src/theory/arith/nl/cad_solver.h +++ b/src/theory/arith/nl/cad_solver.h @@ -20,6 +20,7 @@ #include "expr/node.h" #include "theory/arith/inference_manager.h" #include "theory/arith/nl/cad/cdcac.h" +#include "theory/arith/nl/cad/proof_checker.h" #include "theory/arith/nl/nl_model.h" namespace CVC4 { @@ -34,7 +35,10 @@ namespace nl { class CadSolver { public: - CadSolver(InferenceManager& im, NlModel& model); + CadSolver(InferenceManager& im, + NlModel& model, + context::Context* ctx, + ProofNodeManager* pnm); ~CadSolver(); /** @@ -81,6 +85,8 @@ class CadSolver * The object implementing the actual decision procedure. */ cad::CDCAC d_CAC; + /** The proof checker for cad proofs */ + cad::CADProofRuleChecker d_proofChecker; #endif /** * Indicates whether we found satisfiability in the last call to diff --git a/src/theory/arith/nl/nonlinear_extension.cpp b/src/theory/arith/nl/nonlinear_extension.cpp index 4d29f1955..c46781e76 100644 --- a/src/theory/arith/nl/nonlinear_extension.cpp +++ b/src/theory/arith/nl/nonlinear_extension.cpp @@ -54,7 +54,7 @@ NonlinearExtension::NonlinearExtension(TheoryArith& containing, d_monomialSlv(&d_extState), d_splitZeroSlv(&d_extState), d_tangentPlaneSlv(&d_extState), - d_cadSlv(d_im, d_model), + d_cadSlv(d_im, d_model, state.getUserContext(), pnm), d_icpSlv(d_im), d_iandSlv(d_im, state, d_model), d_builtModel(containing.getSatContext(), false) -- cgit v1.2.3