summaryrefslogtreecommitdiff
path: root/src
diff options
context:
space:
mode:
Diffstat (limited to 'src')
-rw-r--r--src/theory/arith/nl/cad/cdcac.cpp75
-rw-r--r--src/theory/arith/nl/cad/cdcac.h23
-rw-r--r--src/theory/arith/nl/cad_solver.cpp31
-rw-r--r--src/theory/arith/nl/cad_solver.h8
-rw-r--r--src/theory/arith/nl/nonlinear_extension.cpp2
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)
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback