From 770d9ae622ec04bc2fbea8356ce11329ed06fa5b Mon Sep 17 00:00:00 2001 From: Gereon Kremer Date: Wed, 23 Sep 2020 20:05:06 +0200 Subject: [PATCH] Make IAND solver use inference manager. (#5126) This PR moves the iand solver (within the nonlinear extension) to use the new inference manager to send lemmas. --- src/theory/arith/nl/iand_solver.cpp | 19 ++++++---------- src/theory/arith/nl/iand_solver.h | 13 +++++------ src/theory/arith/nl/nonlinear_extension.cpp | 24 ++++++++++----------- src/theory/arith/nl/nonlinear_extension.h | 2 +- src/theory/arith/theory_arith.cpp | 2 +- 5 files changed, 28 insertions(+), 32 deletions(-) diff --git a/src/theory/arith/nl/iand_solver.cpp b/src/theory/arith/nl/iand_solver.cpp index 7e9fa13e5..a72010bf4 100644 --- a/src/theory/arith/nl/iand_solver.cpp +++ b/src/theory/arith/nl/iand_solver.cpp @@ -28,10 +28,10 @@ namespace theory { namespace arith { namespace nl { -IAndSolver::IAndSolver(TheoryArith& containing, NlModel& model) - : d_containing(containing), +IAndSolver::IAndSolver(InferenceManager& im, ArithState& state, NlModel& model) + : d_im(im), d_model(model), - d_initRefine(containing.getUserContext()) + d_initRefine(state.getUserContext()) { NodeManager* nm = NodeManager::currentNM(); d_true = nm->mkConst(true); @@ -66,10 +66,9 @@ void IAndSolver::initLastCall(const std::vector& assertions, Trace("iand") << "We have " << d_iands.size() << " IAND terms." << std::endl; } -std::vector IAndSolver::checkInitialRefine() +void IAndSolver::checkInitialRefine() { Trace("iand-check") << "IAndSolver::checkInitialRefine" << std::endl; - std::vector lems; NodeManager* nm = NodeManager::currentNM(); for (const std::pair >& is : d_iands) { @@ -101,17 +100,15 @@ std::vector IAndSolver::checkInitialRefine() Node lem = conj.size() == 1 ? conj[0] : nm->mkNode(AND, conj); Trace("iand-lemma") << "IAndSolver::Lemma: " << lem << " ; INIT_REFINE" << std::endl; - lems.emplace_back(lem, InferenceId::NL_IAND_INIT_REFINE); + d_im.addPendingArithLemma(lem, InferenceId::NL_IAND_INIT_REFINE); } } - return lems; } -std::vector IAndSolver::checkFullRefine() +void IAndSolver::checkFullRefine() { Trace("iand-check") << "IAndSolver::checkFullRefine"; Trace("iand-check") << "IAND terms: " << std::endl; - std::vector lems; for (const std::pair >& is : d_iands) { // the reference bitwidth @@ -163,12 +160,10 @@ std::vector IAndSolver::checkFullRefine() Node lem = valueBasedLemma(i); Trace("iand-lemma") << "IAndSolver::Lemma: " << lem << " ; VALUE_REFINE" << std::endl; - lems.emplace_back(lem, InferenceId::NL_IAND_VALUE_REFINE); + d_im.addPendingArithLemma(lem, InferenceId::NL_IAND_VALUE_REFINE, true); } } } - - return lems; } Node IAndSolver::convertToBvK(unsigned k, Node n) const diff --git a/src/theory/arith/nl/iand_solver.h b/src/theory/arith/nl/iand_solver.h index 216e1556b..d74365784 100644 --- a/src/theory/arith/nl/iand_solver.h +++ b/src/theory/arith/nl/iand_solver.h @@ -20,9 +20,10 @@ #include "context/cdhashset.h" #include "expr/node.h" +#include "theory/arith/arith_state.h" +#include "theory/arith/inference_manager.h" #include "theory/arith/nl/nl_lemma_utils.h" #include "theory/arith/nl/nl_model.h" -#include "theory/arith/theory_arith.h" namespace CVC4 { namespace theory { @@ -37,7 +38,7 @@ class IAndSolver typedef context::CDHashSet NodeSet; public: - IAndSolver(TheoryArith& containing, NlModel& model); + IAndSolver(InferenceManager& im, ArithState& state, NlModel& model); ~IAndSolver(); /** init last call @@ -66,18 +67,18 @@ class IAndSolver * This should be a heuristic incomplete check that only introduces a * small number of new terms in the lemmas it returns. */ - std::vector checkInitialRefine(); + void checkInitialRefine(); /** check full refine * * This should be a complete check that returns at least one lemma to * rule out the current model. */ - std::vector checkFullRefine(); + void checkFullRefine(); //-------------------------------------------- end lemma schemas private: - // The theory of arithmetic containing this extension. - TheoryArith& d_containing; + // The inference manager that we push conflicts and lemmas to. + InferenceManager& d_im; /** Reference to the non-linear model object */ NlModel& d_model; /** commonly used terms */ diff --git a/src/theory/arith/nl/nonlinear_extension.cpp b/src/theory/arith/nl/nonlinear_extension.cpp index b8f69f521..af1f536be 100644 --- a/src/theory/arith/nl/nonlinear_extension.cpp +++ b/src/theory/arith/nl/nonlinear_extension.cpp @@ -19,6 +19,7 @@ #include "options/arith_options.h" #include "options/theory_options.h" +#include "theory/arith/arith_state.h" #include "theory/arith/arith_utilities.h" #include "theory/arith/theory_arith.h" #include "theory/ext_theory.h" @@ -32,6 +33,7 @@ namespace arith { namespace nl { NonlinearExtension::NonlinearExtension(TheoryArith& containing, + ArithState& state, eq::EqualityEngine* ee) : d_containing(containing), d_im(containing.getInferenceManager()), @@ -48,7 +50,7 @@ NonlinearExtension::NonlinearExtension(TheoryArith& containing, d_nlSlv(containing, d_model), d_cadSlv(d_im, d_model), d_icpSlv(d_im), - d_iandSlv(containing, d_model), + d_iandSlv(d_im, state, d_model), d_builtModel(containing.getSatContext(), false) { d_extTheory.addFunctionKind(kind::NONLINEAR_MULT); @@ -448,13 +450,12 @@ int NonlinearExtension::checkLastCall(const std::vector& assertions, } } //-----------------------------------initial lemmas for iand - lemmas = d_iandSlv.checkInitialRefine(); - filterLemmas(lemmas, lems); - if (!lems.empty()) + d_iandSlv.checkInitialRefine(); + if (d_im.hasUsed()) { - Trace("nl-ext") << " ...finished with " << lems.size() << " new lemmas." + Trace("nl-ext") << " ...finished with " << d_im.numPendingLemmas() << " new lemmas." << std::endl; - return lems.size(); + return d_im.numPendingLemmas(); } // main calls to nlExt @@ -583,13 +584,12 @@ int NonlinearExtension::checkLastCall(const std::vector& assertions, } } // run the full refinement in the IAND solver - lemmas = d_iandSlv.checkFullRefine(); - filterLemmas(lemmas, wlems); - - Trace("nl-ext") << " ...finished with " - << (wlems.size() + d_im.numWaitingLemmas()) - << " waiting lemmas." << std::endl; + d_iandSlv.checkFullRefine(); + Trace("nl-ext") << " ...finished with " << d_im.numWaitingLemmas() << " waiting lemmas." + << std::endl; + Trace("nl-ext") << " ...finished with " << d_im.numPendingLemmas() << " lemmas." + << std::endl; return 0; } diff --git a/src/theory/arith/nl/nonlinear_extension.h b/src/theory/arith/nl/nonlinear_extension.h index 15beea32c..d09d92c9f 100644 --- a/src/theory/arith/nl/nonlinear_extension.h +++ b/src/theory/arith/nl/nonlinear_extension.h @@ -74,7 +74,7 @@ class NonlinearExtension typedef context::CDHashSet NodeSet; public: - NonlinearExtension(TheoryArith& containing, eq::EqualityEngine* ee); + NonlinearExtension(TheoryArith& containing, ArithState& state, eq::EqualityEngine* ee); ~NonlinearExtension(); /** * Does non-context dependent setup for a node connected to a theory. diff --git a/src/theory/arith/theory_arith.cpp b/src/theory/arith/theory_arith.cpp index abdf6930a..9324c94af 100644 --- a/src/theory/arith/theory_arith.cpp +++ b/src/theory/arith/theory_arith.cpp @@ -83,7 +83,7 @@ void TheoryArith::finishInit() if (logicInfo.isTheoryEnabled(THEORY_ARITH) && !logicInfo.isLinear()) { d_nonlinearExtension.reset( - new nl::NonlinearExtension(*this, d_equalityEngine)); + new nl::NonlinearExtension(*this, d_astate, d_equalityEngine)); } // finish initialize internally d_internal->finishInit(); -- 2.30.2