diff options
Diffstat (limited to 'src/theory/arith/nl/cad_solver.cpp')
| -rw-r--r-- | src/theory/arith/nl/cad_solver.cpp | 31 |
1 files changed, 23 insertions, 8 deletions
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 " |