diff options
Diffstat (limited to 'src/theory/arith')
-rw-r--r-- | src/theory/arith/inference_manager.cpp | 5 | ||||
-rw-r--r-- | src/theory/arith/inference_manager.h | 6 | ||||
-rw-r--r-- | src/theory/arith/nl/cad_solver.cpp | 40 | ||||
-rw-r--r-- | src/theory/arith/nl/cad_solver.h | 12 | ||||
-rw-r--r-- | src/theory/arith/nl/nonlinear_extension.cpp | 12 |
5 files changed, 39 insertions, 36 deletions
diff --git a/src/theory/arith/inference_manager.cpp b/src/theory/arith/inference_manager.cpp index d03d2ba37..d4c5d17c5 100644 --- a/src/theory/arith/inference_manager.cpp +++ b/src/theory/arith/inference_manager.cpp @@ -87,6 +87,11 @@ void InferenceManager::addConflict(const Node& conf, InferenceId inftype) conflict(Rewriter::rewrite(conf)); } +bool InferenceManager::hasUsed() const +{ + return hasSent() || hasPending(); +} + std::size_t InferenceManager::numWaitingLemmas() const { return d_waitingLem.size(); diff --git a/src/theory/arith/inference_manager.h b/src/theory/arith/inference_manager.h index 33e4f424b..e1e386bec 100644 --- a/src/theory/arith/inference_manager.h +++ b/src/theory/arith/inference_manager.h @@ -81,6 +81,12 @@ class InferenceManager : public InferenceManagerBuffered /** Add a conflict to the this inference manager. */ void addConflict(const Node& conf, InferenceId inftype); + /** + * Checks whether we have made any progress, that is whether a conflict, lemma + * or fact was added or whether a lemma or fact is pending. + */ + bool hasUsed() const; + /** Returns the number of pending lemmas. */ std::size_t numWaitingLemmas() const; diff --git a/src/theory/arith/nl/cad_solver.cpp b/src/theory/arith/nl/cad_solver.cpp index 473e067b7..416de1c5a 100644 --- a/src/theory/arith/nl/cad_solver.cpp +++ b/src/theory/arith/nl/cad_solver.cpp @@ -28,8 +28,8 @@ namespace theory { namespace arith { namespace nl { -CadSolver::CadSolver(TheoryArith& containing, NlModel& model) - : d_foundSatisfiability(false), d_containing(containing), d_model(model) +CadSolver::CadSolver(InferenceManager& im, NlModel& model) + : d_foundSatisfiability(false), d_im(im), d_model(model) { d_ranVariable = NodeManager::currentNM()->mkSkolem("__z", @@ -66,10 +66,9 @@ void CadSolver::initLastCall(const std::vector<Node>& assertions) #endif } -std::vector<NlLemma> CadSolver::checkFull() +void CadSolver::checkFull() { #ifdef CVC4_POLY_IMP - std::vector<NlLemma> lems; auto covering = d_CAC.getUnsatCover(); if (covering.empty()) { @@ -81,23 +80,11 @@ std::vector<NlLemma> CadSolver::checkFull() d_foundSatisfiability = false; auto mis = collectConstraints(covering); Trace("nl-cad") << "Collected MIS: " << mis << std::endl; - auto* nm = NodeManager::currentNM(); - for (auto& n : mis) - { - n = n.negate(); - } Assert(!mis.empty()) << "Infeasible subset can not be empty"; - if (mis.size() == 1) - { - lems.emplace_back(mis.front(), InferenceId::NL_CAD_CONFLICT); - } - else - { - lems.emplace_back(nm->mkNode(Kind::OR, mis), InferenceId::NL_CAD_CONFLICT); - } - Trace("nl-cad") << "UNSAT with MIS: " << lems.back().d_node << std::endl; + Trace("nl-cad") << "UNSAT with MIS: " << mis << std::endl; + d_im.addConflict(NodeManager::currentNM()->mkAnd(mis), + InferenceId::NL_CAD_CONFLICT); } - return lems; #else Warning() << "Tried to use CadSolver but libpoly is not available. Compile " "with --poly." @@ -106,10 +93,9 @@ std::vector<NlLemma> CadSolver::checkFull() #endif } -std::vector<NlLemma> CadSolver::checkPartial() +void CadSolver::checkPartial() { #ifdef CVC4_POLY_IMP - std::vector<NlLemma> lems; auto covering = d_CAC.getUnsatCover(0, true); if (covering.empty()) { @@ -135,14 +121,16 @@ std::vector<NlLemma> CadSolver::checkPartial() } Node conclusion = excluding_interval_to_lemma(first_var, interval.d_interval, false); - if (!conclusion.isNull()) { + if (!conclusion.isNull()) + { Node lemma = nm->mkNode(Kind::IMPLIES, premise, conclusion); - Trace("nl-cad") << "Excluding " << first_var << " -> " << interval.d_interval << " using " << lemma << std::endl; - lems.emplace_back(lemma, InferenceId::NL_CAD_EXCLUDED_INTERVAL); - } + Trace("nl-cad") << "Excluding " << first_var << " -> " + << interval.d_interval << " using " << lemma + << std::endl; + d_im.addPendingArithLemma(lemma, InferenceId::NL_CAD_EXCLUDED_INTERVAL); + } } } - return lems; #else Warning() << "Tried to use CadSolver but libpoly is not available. Compile " "with --poly." diff --git a/src/theory/arith/nl/cad_solver.h b/src/theory/arith/nl/cad_solver.h index 6f6c0d43c..615cdb03a 100644 --- a/src/theory/arith/nl/cad_solver.h +++ b/src/theory/arith/nl/cad_solver.h @@ -18,9 +18,9 @@ #include <vector> #include "expr/node.h" +#include "theory/arith/inference_manager.h" #include "theory/arith/nl/cad/cdcac.h" #include "theory/arith/nl/nl_model.h" -#include "theory/arith/theory_arith.h" namespace CVC4 { namespace theory { @@ -34,7 +34,7 @@ namespace nl { class CadSolver { public: - CadSolver(TheoryArith& containing, NlModel& model); + CadSolver(InferenceManager& im, NlModel& model); ~CadSolver(); /** @@ -52,7 +52,7 @@ class CadSolver * for construct_model_if_available. Otherwise, the single lemma can be used * as an infeasible subset. */ - std::vector<NlLemma> checkFull(); + void checkFull(); /** * Perform a partial check, returning either {} or a list of lemmas. @@ -60,7 +60,7 @@ class CadSolver * for construct_model_if_available. Otherwise, the lemmas exclude some part * of the search space. */ - std::vector<NlLemma> checkPartial(); + void checkPartial(); /** * If a model is available (indicated by the last call to check_full() or @@ -88,8 +88,8 @@ class CadSolver */ bool d_foundSatisfiability; - /** The theory of arithmetic containing this extension.*/ - TheoryArith& d_containing; + /** The inference manager we are pushing conflicts and lemmas to. */ + InferenceManager& d_im; /** Reference to the non-linear model object */ NlModel& d_model; }; /* class CadSolver */ diff --git a/src/theory/arith/nl/nonlinear_extension.cpp b/src/theory/arith/nl/nonlinear_extension.cpp index 537dd604c..3bf547ceb 100644 --- a/src/theory/arith/nl/nonlinear_extension.cpp +++ b/src/theory/arith/nl/nonlinear_extension.cpp @@ -46,7 +46,7 @@ NonlinearExtension::NonlinearExtension(TheoryArith& containing, d_model(containing.getSatContext()), d_trSlv(d_model), d_nlSlv(containing, d_model), - d_cadSlv(containing, d_model), + d_cadSlv(d_im, d_model), d_iandSlv(containing, d_model), d_builtModel(containing.getSatContext(), false) { @@ -557,12 +557,16 @@ int NonlinearExtension::checkLastCall(const std::vector<Node>& assertions, } if (options::nlCad()) { - lemmas = d_cadSlv.checkFull(); - if (lemmas.empty()) + d_cadSlv.checkFull(); + if (!d_im.hasUsed()) { Trace("nl-cad") << "nl-cad found SAT!" << std::endl; } - filterLemmas(lemmas, wlems); + else + { + // checkFull() only adds a single conflict + return 1; + } } // run the full refinement in the IAND solver lemmas = d_iandSlv.checkFullRefine(); |