From: Gereon Kremer Date: Fri, 4 Sep 2020 14:59:49 +0000 (+0200) Subject: Use arith::InferenceManager for CAD lemmas (#5015) X-Git-Tag: cvc5-1.0.0~2895 X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=0d0c1cdbce4fb46ad5c7d4bc620b712ea014722e;p=cvc5.git 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. --- 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& assertions) #endif } -std::vector CadSolver::checkFull() +void CadSolver::checkFull() { #ifdef CVC4_POLY_IMP - std::vector lems; auto covering = d_CAC.getUnsatCover(); if (covering.empty()) { @@ -81,23 +80,11 @@ std::vector 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 CadSolver::checkFull() #endif } -std::vector CadSolver::checkPartial() +void CadSolver::checkPartial() { #ifdef CVC4_POLY_IMP - std::vector lems; auto covering = d_CAC.getUnsatCover(0, true); if (covering.empty()) { @@ -135,14 +121,16 @@ std::vector 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 #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 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 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& 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(); diff --git a/src/theory/sets/cardinality_extension.cpp b/src/theory/sets/cardinality_extension.cpp index a51cee2c3..321559f5a 100644 --- a/src/theory/sets/cardinality_extension.cpp +++ b/src/theory/sets/cardinality_extension.cpp @@ -183,17 +183,17 @@ void CardinalityExtension::check() { checkCardinalityExtended(); checkRegister(); - if (d_im.hasProcessed()) + if (d_im.hasSent()) { return; } checkMinCard(); - if (d_im.hasProcessed()) + if (d_im.hasSent()) { return; } checkCardCycles(); - if (d_im.hasProcessed()) + if (d_im.hasSent()) { return; } @@ -300,7 +300,7 @@ void CardinalityExtension::checkCardCycles() std::vector curr; std::vector exp; checkCardCyclesRec(s, curr, exp); - if (d_im.hasProcessed()) + if (d_im.hasSent()) { return; } @@ -414,7 +414,7 @@ void CardinalityExtension::checkCardCyclesRec(Node eqc, } d_im.assertInference(conc, n.eqNode(emp_set), "cg_emp"); d_im.doPendingLemmas(); - if (d_im.hasProcessed()) + if (d_im.hasSent()) { return; } @@ -446,7 +446,7 @@ void CardinalityExtension::checkCardCyclesRec(Node eqc, Assert(!d_state.areEqual(n, emp_set)); d_im.assertInference(n.eqNode(emp_set), p.eqNode(emp_set), "cg_emppar"); d_im.doPendingLemmas(); - if (d_im.hasProcessed()) + if (d_im.hasSent()) { return; } @@ -493,7 +493,7 @@ void CardinalityExtension::checkCardCyclesRec(Node eqc, << "...derived " << conc.size() << " conclusions" << std::endl; d_im.assertInference(conc, n.eqNode(p), "cg_eqpar"); d_im.doPendingLemmas(); - if (d_im.hasProcessed()) + if (d_im.hasSent()) { return; } @@ -552,7 +552,7 @@ void CardinalityExtension::checkCardCyclesRec(Node eqc, Trace("sets-nf") << "Split empty : " << n << std::endl; d_im.split(n.eqNode(emp_set), 1); } - Assert(d_im.hasProcessed()); + Assert(d_im.hasSent()); return; } else @@ -600,7 +600,7 @@ void CardinalityExtension::checkCardCyclesRec(Node eqc, } d_im.assertInference(conc, cpk.eqNode(cpnl), "cg_pareq"); d_im.doPendingLemmas(); - if (d_im.hasProcessed()) + if (d_im.hasSent()) { return; } @@ -619,7 +619,7 @@ void CardinalityExtension::checkCardCyclesRec(Node eqc, Trace("sets-cycle-debug") << "Traverse card parent " << eqc << " -> " << cpnc << std::endl; checkCardCyclesRec(cpnc, curr, exp); - if (d_im.hasProcessed()) + if (d_im.hasSent()) { return; } @@ -642,7 +642,7 @@ void CardinalityExtension::checkNormalForms(std::vector& intro_sets) for (int i = (int)(d_oSetEqc.size() - 1); i >= 0; i--) { checkNormalForm(d_oSetEqc[i], intro_sets); - if (d_im.hasProcessed() || !intro_sets.empty()) + if (d_im.hasSent() || !intro_sets.empty()) { return; } @@ -783,7 +783,7 @@ void CardinalityExtension::checkNormalForm(Node eqc, d_state.debugPrintSet(r, "sets-nf"); Trace("sets-nf") << std::endl; d_im.split(r.eqNode(emp_set), 1); - Assert(d_im.hasProcessed()); + Assert(d_im.hasSent()); return; } } @@ -867,7 +867,7 @@ void CardinalityExtension::checkNormalForm(Node eqc, } if (!success) { - Assert(d_im.hasProcessed()); + Assert(d_im.hasSent()); return; } // Send to parents (a parent is a set that contains a term in this equivalence diff --git a/src/theory/sets/theory_sets_private.cpp b/src/theory/sets/theory_sets_private.cpp index 7d498a798..5e78e7ed5 100644 --- a/src/theory/sets/theory_sets_private.cpp +++ b/src/theory/sets/theory_sets_private.cpp @@ -286,7 +286,7 @@ void TheorySetsPrivate::fullEffortCheck() Trace("sets") << "----- Full effort check ------" << std::endl; do { - Assert(!d_im.hasPendingLemma() || d_im.hasProcessed()); + Assert(!d_im.hasPendingLemma() || d_im.hasSent()); Trace("sets") << "...iterate full effort check..." << std::endl; fullEffortReset(); @@ -391,7 +391,7 @@ void TheorySetsPrivate::fullEffortCheck() // We may have sent lemmas while registering the terms in the loop above, // e.g. the cardinality solver. - if (d_im.hasProcessed()) + if (d_im.hasSent()) { continue; } @@ -421,35 +421,35 @@ void TheorySetsPrivate::fullEffortCheck() // check subtypes checkSubtypes(); d_im.doPendingLemmas(); - if (d_im.hasProcessed()) + if (d_im.hasSent()) { continue; } // check downwards closure checkDownwardsClosure(); d_im.doPendingLemmas(); - if (d_im.hasProcessed()) + if (d_im.hasSent()) { continue; } // check upwards closure checkUpwardsClosure(); d_im.doPendingLemmas(); - if (d_im.hasProcessed()) + if (d_im.hasSent()) { continue; } // check disequalities checkDisequalities(); d_im.doPendingLemmas(); - if (d_im.hasProcessed()) + if (d_im.hasSent()) { continue; } // check reduce comprehensions checkReduceComprehensions(); d_im.doPendingLemmas(); - if (d_im.hasProcessed()) + if (d_im.hasSent()) { continue; } @@ -457,7 +457,7 @@ void TheorySetsPrivate::fullEffortCheck() { // call the check method of the cardinality solver d_cardSolver->check(); - if (d_im.hasProcessed()) + if (d_im.hasSent()) { continue; } @@ -469,7 +469,7 @@ void TheorySetsPrivate::fullEffortCheck() } } while (!d_im.hasSentLemma() && !d_state.isInConflict() && d_im.hasSentFact()); - Assert(!d_im.hasPendingLemma() || d_im.hasProcessed()); + Assert(!d_im.hasPendingLemma() || d_im.hasSent()); Trace("sets") << "----- End full effort check, conflict=" << d_state.isInConflict() << ", lemma=" << d_im.hasSentLemma() << std::endl; @@ -720,7 +720,7 @@ void TheorySetsPrivate::checkUpwardsClosure() } } } - if (!d_im.hasProcessed()) + if (!d_im.hasSent()) { if (options::setsExt()) { @@ -827,7 +827,7 @@ void TheorySetsPrivate::checkDisequalities() lem = Rewriter::rewrite(lem); d_im.assertInference(lem, d_true, "diseq", 1); d_im.doPendingLemmas(); - if (d_im.hasProcessed()) + if (d_im.hasSent()) { return; } diff --git a/src/theory/theory_inference_manager.cpp b/src/theory/theory_inference_manager.cpp index 570b878b4..801d6a266 100644 --- a/src/theory/theory_inference_manager.cpp +++ b/src/theory/theory_inference_manager.cpp @@ -58,7 +58,7 @@ void TheoryInferenceManager::reset() d_numCurrentFacts = 0; } -bool TheoryInferenceManager::hasProcessed() const +bool TheoryInferenceManager::hasSent() const { return d_theoryState.isInConflict() || d_numCurrentLemmas > 0 || d_numCurrentFacts > 0; diff --git a/src/theory/theory_inference_manager.h b/src/theory/theory_inference_manager.h index 7fecacf82..97baeaa40 100644 --- a/src/theory/theory_inference_manager.h +++ b/src/theory/theory_inference_manager.h @@ -96,7 +96,7 @@ class TheoryInferenceManager * Returns true if we are in conflict, or if we have sent a lemma or fact * since the last call to reset. */ - bool hasProcessed() const; + bool hasSent() const; //--------------------------------------- propagations /** * T-propagate literal lit, possibly encountered by equality engine,