diff options
author | Gereon Kremer <gereon.kremer@cs.rwth-aachen.de> | 2020-09-04 16:59:49 +0200 |
---|---|---|
committer | GitHub <noreply@github.com> | 2020-09-04 09:59:49 -0500 |
commit | 0d0c1cdbce4fb46ad5c7d4bc620b712ea014722e (patch) | |
tree | 5fa7c5d06cbf0a67541c5bdbc82bf692f5d1dd48 /src/theory/arith/nl/cad_solver.cpp | |
parent | bfb744af4f932f095640d97be8f0bfa9ff60e981 (diff) |
Use arith::InferenceManager for CAD lemmas (#5015)
This makes the CAD solver use the new arith::InferenceManager instead of the previously used lemma collection scheme.
Diffstat (limited to 'src/theory/arith/nl/cad_solver.cpp')
-rw-r--r-- | src/theory/arith/nl/cad_solver.cpp | 40 |
1 files changed, 14 insertions, 26 deletions
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." |