diff options
Diffstat (limited to 'src')
-rw-r--r-- | src/theory/arith/nl/cad/cdcac.cpp | 75 | ||||
-rw-r--r-- | src/theory/arith/nl/cad/cdcac.h | 23 | ||||
-rw-r--r-- | src/theory/arith/nl/cad_solver.cpp | 31 | ||||
-rw-r--r-- | src/theory/arith/nl/cad_solver.h | 8 | ||||
-rw-r--r-- | src/theory/arith/nl/nonlinear_extension.cpp | 2 |
5 files changed, 122 insertions, 17 deletions
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<poly::Variable>& ordering) +CDCAC::CDCAC(context::Context* ctx, + ProofNodeManager* pnm, + const std::vector<poly::Variable>& ordering) : d_variableOrdering(ordering) { + if (pnm != nullptr) + { + d_proof.reset(new CADProofGenerator(ctx, pnm)); + } } void CDCAC::reset() @@ -120,6 +124,17 @@ std::vector<CACInterval> 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<CACInterval> 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<CACInterval> intervals = getUnsatIntervals(curVariable); @@ -373,6 +392,10 @@ std::vector<CACInterval> 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<CACInterval> 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<CACInterval> 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<Node>& 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<CACInterval>& intervals) { - cleanIntervals(intervals); + if (isProofEnabled()) + { + std::vector<CACInterval> 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<poly::Variable>& ordering); + CDCAC(context::Context* ctx, + ProofNodeManager* pnm, + const std::vector<poly::Variable>& ordering = {}); /** Reset this instance. */ void reset(); @@ -138,7 +139,20 @@ class CDCAC std::vector<CACInterval> 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<Node>& 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<poly::Value> d_initialAssignment; + + /** The proof generator */ + std::unique_ptr<CADProofGenerator> 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) |