From 58733b382a4a956c051d06e7318afa1deed612da Mon Sep 17 00:00:00 2001 From: Gereon Kremer Date: Thu, 3 Sep 2020 16:27:56 +0200 Subject: [PATCH] Basic integration of arith::InferenceManager (#4999) This PR adds a first basic integration of the arith::InferenceManager into the arithmetic theory and the nonlinear extension in particular. While the lemma collection mechanism (in the nonlinear extension) remains unchanged, the lemmas are ultimately not directly pushed to the output channel but instead added to the inference manager. Additionally, we no longer use the cache within the nonlinear extension but instead rely on the inference manager. This PR is based on #4960. --- src/CMakeLists.txt | 4 +- src/theory/arith/arith_lemma.h | 6 +- src/theory/arith/inference_id.cpp | 57 ++++++++++++++++++ .../arith/{nl/inference.h => inference_id.h} | 58 +++++++++--------- src/theory/arith/inference_manager.cpp | 4 +- src/theory/arith/inference_manager.h | 6 +- src/theory/arith/nl/cad_solver.cpp | 8 +-- src/theory/arith/nl/iand_solver.cpp | 4 +- src/theory/arith/nl/inference.cpp | 59 ------------------- src/theory/arith/nl/nl_lemma_utils.h | 5 +- src/theory/arith/nl/nl_solver.cpp | 18 +++--- src/theory/arith/nl/nonlinear_extension.cpp | 35 ++++------- src/theory/arith/nl/nonlinear_extension.h | 6 +- src/theory/arith/nl/stats.h | 4 +- src/theory/arith/nl/transcendental_solver.cpp | 14 ++--- src/theory/arith/theory_arith.cpp | 3 +- src/theory/arith/theory_arith.h | 11 ++++ 17 files changed, 147 insertions(+), 155 deletions(-) create mode 100644 src/theory/arith/inference_id.cpp rename src/theory/arith/{nl/inference.h => inference_id.h} (78%) delete mode 100644 src/theory/arith/nl/inference.cpp diff --git a/src/CMakeLists.txt b/src/CMakeLists.txt index 9523f9600..a0fd277f8 100644 --- a/src/CMakeLists.txt +++ b/src/CMakeLists.txt @@ -291,6 +291,8 @@ libcvc4_add_sources( theory/arith/fc_simplex.h theory/arith/infer_bounds.cpp theory/arith/infer_bounds.h + theory/arith/inference_id.cpp + theory/arith/inference_id.h theory/arith/inference_manager.cpp theory/arith/inference_manager.h theory/arith/linear_equality.cpp @@ -313,8 +315,6 @@ libcvc4_add_sources( theory/arith/nl/ext_theory_callback.h theory/arith/nl/iand_solver.cpp theory/arith/nl/iand_solver.h - theory/arith/nl/inference.cpp - theory/arith/nl/inference.h theory/arith/nl/nl_constraint.cpp theory/arith/nl/nl_constraint.h theory/arith/nl/nl_lemma_utils.cpp diff --git a/src/theory/arith/arith_lemma.h b/src/theory/arith/arith_lemma.h index a06cb83f3..8af620286 100644 --- a/src/theory/arith/arith_lemma.h +++ b/src/theory/arith/arith_lemma.h @@ -19,7 +19,7 @@ #include #include "expr/node.h" -#include "theory/arith/nl/inference.h" +#include "theory/arith/inference_id.h" #include "theory/inference_manager_buffered.h" #include "theory/output_channel.h" #include "theory/theory_inference.h" @@ -40,14 +40,14 @@ class ArithLemma : public SimpleTheoryLemma ArithLemma(Node n, LemmaProperty p, ProofGenerator* pg, - nl::Inference inf = nl::Inference::UNKNOWN) + InferenceId inf = InferenceId::UNKNOWN) : SimpleTheoryLemma(n, p, pg), d_inference(inf) { } virtual ~ArithLemma() {} /** The inference id for the lemma */ - nl::Inference d_inference; + InferenceId d_inference; }; /** * Writes an arithmetic lemma to a stream. diff --git a/src/theory/arith/inference_id.cpp b/src/theory/arith/inference_id.cpp new file mode 100644 index 000000000..7ecbb364d --- /dev/null +++ b/src/theory/arith/inference_id.cpp @@ -0,0 +1,57 @@ +/********************* */ +/*! \file inference_id.cpp + ** \verbatim + ** Top contributors (to current version): + ** Andrew Reynolds + ** This file is part of the CVC4 project. + ** Copyright (c) 2009-2020 by the authors listed in the file AUTHORS + ** in the top-level source directory) and their institutional affiliations. + ** All rights reserved. See the file COPYING in the top-level source + ** directory for licensing information.\endverbatim + ** + ** \brief Implementation of inference enumeration. + **/ + +#include "theory/arith/inference_id.h" + +namespace CVC4 { +namespace theory { +namespace arith { + +const char* toString(InferenceId i) +{ + switch (i) + { + case InferenceId::NL_CONGRUENCE: return "CONGRUENCE"; + case InferenceId::NL_SHARED_TERM_VALUE_SPLIT: return "SHARED_TERM_VALUE_SPLIT"; + case InferenceId::NL_SPLIT_ZERO: return "SPLIT_ZERO"; + case InferenceId::NL_SIGN: return "SIGN"; + case InferenceId::NL_COMPARISON: return "COMPARISON"; + case InferenceId::NL_INFER_BOUNDS: return "INFER_BOUNDS"; + case InferenceId::NL_INFER_BOUNDS_NT: return "INFER_BOUNDS_NT"; + case InferenceId::NL_FACTOR: return "FACTOR"; + case InferenceId::NL_RES_INFER_BOUNDS: return "RES_INFER_BOUNDS"; + case InferenceId::NL_TANGENT_PLANE: return "TANGENT_PLANE"; + case InferenceId::NL_T_PURIFY_ARG: return "T_PURIFY_ARG"; + case InferenceId::NL_T_INIT_REFINE: return "T_INIT_REFINE"; + case InferenceId::NL_T_PI_BOUND: return "T_PI_BOUND"; + case InferenceId::NL_T_MONOTONICITY: return "T_MONOTONICITY"; + case InferenceId::NL_T_SECANT: return "T_SECANT"; + case InferenceId::NL_T_TANGENT: return "T_TANGENT"; + case InferenceId::NL_IAND_INIT_REFINE: return "IAND_INIT_REFINE"; + case InferenceId::NL_IAND_VALUE_REFINE: return "IAND_VALUE_REFINE"; + case InferenceId::NL_CAD_CONFLICT: return "CAD_CONFLICT"; + case InferenceId::NL_CAD_EXCLUDED_INTERVAL: return "CAD_EXCLUDED_INTERVAL"; + default: return "?"; + } +} + +std::ostream& operator<<(std::ostream& out, InferenceId i) +{ + out << toString(i); + return out; +} + +} // namespace arith +} // namespace theory +} // namespace CVC4 diff --git a/src/theory/arith/nl/inference.h b/src/theory/arith/inference_id.h similarity index 78% rename from src/theory/arith/nl/inference.h rename to src/theory/arith/inference_id.h index 0cf6ad3bd..56aeb3d24 100644 --- a/src/theory/arith/nl/inference.h +++ b/src/theory/arith/inference_id.h @@ -1,5 +1,5 @@ /********************* */ -/*! \file inference.h +/*! \file inference_id.h ** \verbatim ** Top contributors (to current version): ** Andrew Reynolds @@ -9,13 +9,13 @@ ** All rights reserved. See the file COPYING in the top-level source ** directory for licensing information.\endverbatim ** - ** \brief Inference enumeration for non-linear arithmetic. + ** \brief Inference enumeration for arithmetic. **/ #include "cvc4_private.h" -#ifndef CVC4__THEORY__ARITH__NL__INFER_INFO_H -#define CVC4__THEORY__ARITH__NL__INFER_INFO_H +#ifndef CVC4__THEORY__ARITH__INFERENCE_ID_H +#define CVC4__THEORY__ARITH__INFERENCE_ID_H #include #include @@ -25,58 +25,57 @@ namespace CVC4 { namespace theory { namespace arith { -namespace nl { /** * Types of inferences used in the procedure */ -enum class Inference : uint32_t +enum class InferenceId : uint32_t { //-------------------- core // simple congruence x=y => f(x)=f(y) - CONGRUENCE, + NL_CONGRUENCE, // shared term value split (for naive theory combination) - SHARED_TERM_VALUE_SPLIT, + NL_SHARED_TERM_VALUE_SPLIT, //-------------------- incremental linearization solver // splitting on zero (NlSolver::checkSplitZero) - SPLIT_ZERO, + NL_SPLIT_ZERO, // based on sign (NlSolver::checkMonomialSign) - SIGN, + NL_SIGN, // based on comparing (abs) model values (NlSolver::checkMonomialMagnitude) - COMPARISON, + NL_COMPARISON, // based on inferring bounds (NlSolver::checkMonomialInferBounds) - INFER_BOUNDS, + NL_INFER_BOUNDS, // same as above, for inferences that introduce new terms - INFER_BOUNDS_NT, + NL_INFER_BOUNDS_NT, // factoring (NlSolver::checkFactoring) - FACTOR, + NL_FACTOR, // resolution bound inferences (NlSolver::checkMonomialInferResBounds) - RES_INFER_BOUNDS, + NL_RES_INFER_BOUNDS, // tangent planes (NlSolver::checkTangentPlanes) - TANGENT_PLANE, + NL_TANGENT_PLANE, //-------------------- transcendental solver // purification of arguments to transcendental functions - T_PURIFY_ARG, + NL_T_PURIFY_ARG, // initial refinement (TranscendentalSolver::checkTranscendentalInitialRefine) - T_INIT_REFINE, + NL_T_INIT_REFINE, // pi bounds - T_PI_BOUND, + NL_T_PI_BOUND, // monotonicity (TranscendentalSolver::checkTranscendentalMonotonic) - T_MONOTONICITY, + NL_T_MONOTONICITY, // tangent refinement (TranscendentalSolver::checkTranscendentalTangentPlanes) - T_TANGENT, + NL_T_TANGENT, // secant refinement, the dual of the above inference - T_SECANT, + NL_T_SECANT, //-------------------- iand solver // initial refinements (IAndSolver::checkInitialRefine) - IAND_INIT_REFINE, + NL_IAND_INIT_REFINE, // value refinements (IAndSolver::checkFullRefine) - IAND_VALUE_REFINE, + NL_IAND_VALUE_REFINE, //-------------------- cad solver // conflict / infeasible subset obtained from cad - CAD_CONFLICT, + NL_CAD_CONFLICT, // excludes an interval for a single variable - CAD_EXCLUDED_INTERVAL, + NL_CAD_EXCLUDED_INTERVAL, //-------------------- unknown UNKNOWN, }; @@ -90,7 +89,7 @@ enum class Inference : uint32_t * @param i The inference * @return The name of the inference */ -const char* toString(Inference i); +const char* toString(InferenceId i); /** * Writes an inference name to a stream. @@ -99,11 +98,10 @@ const char* toString(Inference i); * @param i The inference to write to the stream * @return The stream */ -std::ostream& operator<<(std::ostream& out, Inference i); +std::ostream& operator<<(std::ostream& out, InferenceId i); -} // namespace nl } // namespace arith } // namespace theory } // namespace CVC4 -#endif /* CVC4__THEORY__ARITH__NL__INFER_INFO_H */ +#endif /* CVC4__THEORY__ARITH__INFERENCE_H */ diff --git a/src/theory/arith/inference_manager.cpp b/src/theory/arith/inference_manager.cpp index bb0bb494e..d03d2ba37 100644 --- a/src/theory/arith/inference_manager.cpp +++ b/src/theory/arith/inference_manager.cpp @@ -65,7 +65,7 @@ void InferenceManager::addPendingArithLemma(const ArithLemma& lemma, isWaiting); } void InferenceManager::addPendingArithLemma(const Node& lemma, - nl::Inference inftype, + InferenceId inftype, bool isWaiting) { addPendingArithLemma(std::unique_ptr(new ArithLemma( @@ -82,7 +82,7 @@ void InferenceManager::flushWaitingLemmas() d_waitingLem.clear(); } -void InferenceManager::addConflict(const Node& conf, nl::Inference inftype) +void InferenceManager::addConflict(const Node& conf, InferenceId inftype) { conflict(Rewriter::rewrite(conf)); } diff --git a/src/theory/arith/inference_manager.h b/src/theory/arith/inference_manager.h index 1c0678e60..33e4f424b 100644 --- a/src/theory/arith/inference_manager.h +++ b/src/theory/arith/inference_manager.h @@ -22,7 +22,7 @@ #include "theory/arith/arith_lemma.h" #include "theory/arith/arith_state.h" -#include "theory/arith/nl/inference.h" +#include "theory/arith/inference_id.h" #include "theory/arith/nl/nl_lemma_utils.h" #include "theory/inference_manager_buffered.h" @@ -69,7 +69,7 @@ class InferenceManager : public InferenceManagerBuffered * added as pending lemma when calling flushWaitingLemmas. */ void addPendingArithLemma(const Node& lemma, - nl::Inference inftype, + InferenceId inftype, bool isWaiting = false); /** @@ -79,7 +79,7 @@ class InferenceManager : public InferenceManagerBuffered void flushWaitingLemmas(); /** Add a conflict to the this inference manager. */ - void addConflict(const Node& conf, nl::Inference inftype); + void addConflict(const Node& conf, InferenceId inftype); /** 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 ac939c341..473e067b7 100644 --- a/src/theory/arith/nl/cad_solver.cpp +++ b/src/theory/arith/nl/cad_solver.cpp @@ -18,7 +18,7 @@ #include #endif -#include "inference.h" +#include "theory/arith/inference_id.h" #include "theory/arith/nl/cad/cdcac.h" #include "theory/arith/nl/poly_conversion.h" #include "util/poly_util.h" @@ -89,11 +89,11 @@ std::vector CadSolver::checkFull() Assert(!mis.empty()) << "Infeasible subset can not be empty"; if (mis.size() == 1) { - lems.emplace_back(mis.front(), Inference::CAD_CONFLICT); + lems.emplace_back(mis.front(), InferenceId::NL_CAD_CONFLICT); } else { - lems.emplace_back(nm->mkNode(Kind::OR, mis), Inference::CAD_CONFLICT); + lems.emplace_back(nm->mkNode(Kind::OR, mis), InferenceId::NL_CAD_CONFLICT); } Trace("nl-cad") << "UNSAT with MIS: " << lems.back().d_node << std::endl; } @@ -138,7 +138,7 @@ std::vector CadSolver::checkPartial() 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, Inference::CAD_EXCLUDED_INTERVAL); + lems.emplace_back(lemma, InferenceId::NL_CAD_EXCLUDED_INTERVAL); } } } diff --git a/src/theory/arith/nl/iand_solver.cpp b/src/theory/arith/nl/iand_solver.cpp index 3b6c3cbe4..08c85cafe 100644 --- a/src/theory/arith/nl/iand_solver.cpp +++ b/src/theory/arith/nl/iand_solver.cpp @@ -101,7 +101,7 @@ 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, Inference::IAND_INIT_REFINE); + lems.emplace_back(lem, InferenceId::NL_IAND_INIT_REFINE); } } return lems; @@ -163,7 +163,7 @@ std::vector IAndSolver::checkFullRefine() Node lem = valueBasedLemma(i); Trace("iand-lemma") << "IAndSolver::Lemma: " << lem << " ; VALUE_REFINE" << std::endl; - lems.emplace_back(lem, Inference::IAND_VALUE_REFINE); + lems.emplace_back(lem, InferenceId::NL_IAND_VALUE_REFINE); } } } diff --git a/src/theory/arith/nl/inference.cpp b/src/theory/arith/nl/inference.cpp deleted file mode 100644 index 0d8413777..000000000 --- a/src/theory/arith/nl/inference.cpp +++ /dev/null @@ -1,59 +0,0 @@ -/********************* */ -/*! \file inference.cpp - ** \verbatim - ** Top contributors (to current version): - ** Andrew Reynolds - ** This file is part of the CVC4 project. - ** Copyright (c) 2009-2020 by the authors listed in the file AUTHORS - ** in the top-level source directory) and their institutional affiliations. - ** All rights reserved. See the file COPYING in the top-level source - ** directory for licensing information.\endverbatim - ** - ** \brief Implementation of inference enumeration. - **/ - -#include "theory/arith/nl/inference.h" - -namespace CVC4 { -namespace theory { -namespace arith { -namespace nl { - -const char* toString(Inference i) -{ - switch (i) - { - case Inference::CONGRUENCE: return "CONGRUENCE"; - case Inference::SHARED_TERM_VALUE_SPLIT: return "SHARED_TERM_VALUE_SPLIT"; - case Inference::SPLIT_ZERO: return "SPLIT_ZERO"; - case Inference::SIGN: return "SIGN"; - case Inference::COMPARISON: return "COMPARISON"; - case Inference::INFER_BOUNDS: return "INFER_BOUNDS"; - case Inference::INFER_BOUNDS_NT: return "INFER_BOUNDS_NT"; - case Inference::FACTOR: return "FACTOR"; - case Inference::RES_INFER_BOUNDS: return "RES_INFER_BOUNDS"; - case Inference::TANGENT_PLANE: return "TANGENT_PLANE"; - case Inference::T_PURIFY_ARG: return "T_PURIFY_ARG"; - case Inference::T_INIT_REFINE: return "T_INIT_REFINE"; - case Inference::T_PI_BOUND: return "T_PI_BOUND"; - case Inference::T_MONOTONICITY: return "T_MONOTONICITY"; - case Inference::T_SECANT: return "T_SECANT"; - case Inference::T_TANGENT: return "T_TANGENT"; - case Inference::IAND_INIT_REFINE: return "IAND_INIT_REFINE"; - case Inference::IAND_VALUE_REFINE: return "IAND_VALUE_REFINE"; - case Inference::CAD_CONFLICT: return "CAD_CONFLICT"; - case Inference::CAD_EXCLUDED_INTERVAL: return "CAD_EXCLUDED_INTERVAL"; - default: return "?"; - } -} - -std::ostream& operator<<(std::ostream& out, Inference i) -{ - out << toString(i); - return out; -} - -} // namespace nl -} // namespace arith -} // namespace theory -} // namespace CVC4 diff --git a/src/theory/arith/nl/nl_lemma_utils.h b/src/theory/arith/nl/nl_lemma_utils.h index c6c22c3c6..1c0635f1f 100644 --- a/src/theory/arith/nl/nl_lemma_utils.h +++ b/src/theory/arith/nl/nl_lemma_utils.h @@ -20,7 +20,6 @@ #include "expr/node.h" #include "theory/arith/arith_lemma.h" -#include "theory/arith/nl/inference.h" #include "theory/output_channel.h" namespace CVC4 { @@ -48,11 +47,11 @@ class NlLemma : public ArithLemma NlLemma(Node n, LemmaProperty p, ProofGenerator* pg, - nl::Inference inf = nl::Inference::UNKNOWN) + InferenceId inf = InferenceId::UNKNOWN) : ArithLemma(n, p, pg, inf) { } - NlLemma(Node n, nl::Inference inf = nl::Inference::UNKNOWN) + NlLemma(Node n, InferenceId inf = InferenceId::UNKNOWN) : ArithLemma(n, LemmaProperty::NONE, nullptr, inf) { } diff --git a/src/theory/arith/nl/nl_solver.cpp b/src/theory/arith/nl/nl_solver.cpp index 6c20eec76..d4a7db55f 100644 --- a/src/theory/arith/nl/nl_solver.cpp +++ b/src/theory/arith/nl/nl_solver.cpp @@ -178,7 +178,7 @@ std::vector NlSolver::checkSplitZero() Node literal = d_containing.getValuation().ensureLiteral(eq); d_containing.getOutputChannel().requirePhase(literal, true); lemmas.emplace_back(literal.orNode(literal.negate()), - Inference::SPLIT_ZERO); + InferenceId::NL_SPLIT_ZERO); } } return lemmas; @@ -274,7 +274,7 @@ int NlSolver::compareSign(Node oa, { Node lemma = safeConstructNary(AND, exp).impNode(mkLit(oa, d_zero, status * 2)); - lem.emplace_back(lemma, Inference::SIGN); + lem.emplace_back(lemma, InferenceId::NL_SIGN); } return status; } @@ -291,7 +291,7 @@ int NlSolver::compareSign(Node oa, if (mvaoa.getConst().sgn() != 0) { Node lemma = av.eqNode(d_zero).impNode(oa.eqNode(d_zero)); - lem.emplace_back(lemma, Inference::SIGN); + lem.emplace_back(lemma, InferenceId::NL_SIGN); } return 0; } @@ -448,7 +448,7 @@ bool NlSolver::compareMonomial( Node clem = nm->mkNode( IMPLIES, safeConstructNary(AND, exp), mkLit(oa, ob, status, true)); Trace("nl-ext-comp-lemma") << "comparison lemma : " << clem << std::endl; - lem.emplace_back(clem, Inference::COMPARISON); + lem.emplace_back(clem, InferenceId::NL_COMPARISON); cmp_infers[status][oa][ob] = clem; } return true; @@ -1007,7 +1007,7 @@ std::vector NlSolver::checkTangentPlanes() tplaneConj.push_back(lb_reverse2); Node tlem = nm->mkNode(AND, tplaneConj); - lemmas.emplace_back(tlem, Inference::TANGENT_PLANE); + lemmas.emplace_back(tlem, InferenceId::NL_TANGENT_PLANE); } } } @@ -1262,11 +1262,11 @@ std::vector NlSolver::checkMonomialInferBounds( // monomials = " << introNewTerms << std::endl; if (!introNewTerms) { - lemmas.emplace_back(iblem, Inference::INFER_BOUNDS); + lemmas.emplace_back(iblem, InferenceId::NL_INFER_BOUNDS); } else { - nt_lemmas.emplace_back(iblem, Inference::INFER_BOUNDS_NT); + nt_lemmas.emplace_back(iblem, InferenceId::NL_INFER_BOUNDS_NT); } } } @@ -1398,7 +1398,7 @@ std::vector NlSolver::checkFactoring( lemma_disj.push_back(conc_lit); Node flem = nm->mkNode(OR, lemma_disj); Trace("nl-ext-factor") << "...lemma is " << flem << std::endl; - lemmas.emplace_back(flem, Inference::FACTOR); + lemmas.emplace_back(flem, InferenceId::NL_FACTOR); } } } @@ -1570,7 +1570,7 @@ std::vector NlSolver::checkMonomialInferResBounds() rblem = Rewriter::rewrite(rblem); Trace("nl-ext-rbound-lemma") << "Resolution bound lemma : " << rblem << std::endl; - lemmas.emplace_back(rblem, Inference::RES_INFER_BOUNDS); + lemmas.emplace_back(rblem, InferenceId::NL_RES_INFER_BOUNDS); } } exp.pop_back(); diff --git a/src/theory/arith/nl/nonlinear_extension.cpp b/src/theory/arith/nl/nonlinear_extension.cpp index 09806cbbd..537dd604c 100644 --- a/src/theory/arith/nl/nonlinear_extension.cpp +++ b/src/theory/arith/nl/nonlinear_extension.cpp @@ -33,9 +33,8 @@ namespace nl { NonlinearExtension::NonlinearExtension(TheoryArith& containing, eq::EqualityEngine* ee) - : d_lemmas(containing.getUserContext()), - d_lemmasPp(containing.getUserContext()), - d_containing(containing), + : d_containing(containing), + d_im(containing.getInferenceManager()), d_ee(ee), d_needsLastCall(false), d_checkCounter(0), @@ -75,22 +74,9 @@ void NonlinearExtension::sendLemmas(const std::vector& out) { for (const NlLemma& nlem : out) { - Node lem = nlem.d_node; - LemmaProperty p = nlem.d_property; Trace("nl-ext-lemma") << "NonlinearExtension::Lemma : " << nlem.d_inference - << " : " << lem << std::endl; - d_containing.getOutputChannel().lemma(lem, p); - // process the side effect - processSideEffect(nlem); - // add to cache based on preprocess - if (isLemmaPropertyPreprocess(p)) - { - d_lemmasPp.insert(lem); - } - else - { - d_lemmas.insert(lem); - } + << " : " << nlem.d_node << std::endl; + d_im.addPendingArithLemma(nlem); d_stats.d_inferences << nlem.d_inference; } } @@ -121,10 +107,8 @@ unsigned NonlinearExtension::filterLemma(NlLemma lem, std::vector& out) Trace("nl-ext-lemma-debug") << "NonlinearExtension::Lemma pre-rewrite : " << lem.d_node << std::endl; lem.d_node = Rewriter::rewrite(lem.d_node); - // get the proper cache - NodeSet& lcache = - isLemmaPropertyPreprocess(lem.d_property) ? d_lemmasPp : d_lemmas; - if (lcache.find(lem.d_node) != lcache.end()) + + if (d_im.hasCachedLemma(lem.d_node, lem.d_property)) { Trace("nl-ext-lemma-debug") << "NonlinearExtension::Lemma duplicate : " << lem.d_node << std::endl; @@ -620,9 +604,12 @@ void NonlinearExtension::check(Theory::Effort e) else { // If we computed lemmas during collectModelInfo, send them now. - if (!d_cmiLemmas.empty()) + if (!d_cmiLemmas.empty() || d_im.hasPendingLemma()) { sendLemmas(d_cmiLemmas); + d_im.doPendingFacts(); + d_im.doPendingLemmas(); + d_im.doPendingPhaseRequirements(); return; } // Otherwise, we will answer SAT. The values that we approximated are @@ -799,7 +786,7 @@ bool NonlinearExtension::modelBasedRefinement(std::vector& mlems) d_containing.getOutputChannel().requirePhase(literal, true); Trace("nl-ext-debug") << "Split on : " << literal << std::endl; Node split = literal.orNode(literal.negate()); - NlLemma nsplit(split, Inference::SHARED_TERM_VALUE_SPLIT); + NlLemma nsplit(split, InferenceId::NL_SHARED_TERM_VALUE_SPLIT); filterLemma(nsplit, stvLemmas); } if (!stvLemmas.empty()) diff --git a/src/theory/arith/nl/nonlinear_extension.h b/src/theory/arith/nl/nonlinear_extension.h index 41f24e769..b62b81e9c 100644 --- a/src/theory/arith/nl/nonlinear_extension.h +++ b/src/theory/arith/nl/nonlinear_extension.h @@ -26,6 +26,7 @@ #include "context/cdlist.h" #include "expr/kind.h" #include "expr/node.h" +#include "theory/arith/inference_manager.h" #include "theory/arith/nl/cad_solver.h" #include "theory/arith/nl/ext_theory_callback.h" #include "theory/arith/nl/iand_solver.h" @@ -237,10 +238,6 @@ class NonlinearExtension */ void sendLemmas(const std::vector& out); - /** cache of all lemmas sent on the output channel (user-context-dependent) */ - NodeSet d_lemmas; - /** Same as above, for preprocessed lemmas */ - NodeSet d_lemmasPp; /** commonly used terms */ Node d_zero; Node d_one; @@ -248,6 +245,7 @@ class NonlinearExtension Node d_true; // The theory of arithmetic containing this extension. TheoryArith& d_containing; + InferenceManager& d_im; // pointer to used equality engine eq::EqualityEngine* d_ee; /** The statistics class */ diff --git a/src/theory/arith/nl/stats.h b/src/theory/arith/nl/stats.h index 1a8a9419e..bc0791c4d 100644 --- a/src/theory/arith/nl/stats.h +++ b/src/theory/arith/nl/stats.h @@ -18,7 +18,7 @@ #define CVC4__THEORY__ARITH__NL__STATS_H #include "expr/kind.h" -#include "theory/arith/nl/inference.h" +#include "theory/arith/inference_id.h" #include "util/statistics_registry.h" namespace CVC4 { @@ -42,7 +42,7 @@ class NlStats /** Number of calls to NonlinearExtension::checkLastCall */ IntStat d_checkRuns; /** Counts the number of applications of each type of inference */ - HistogramStat d_inferences; + HistogramStat d_inferences; }; } // namespace nl diff --git a/src/theory/arith/nl/transcendental_solver.cpp b/src/theory/arith/nl/transcendental_solver.cpp index b2ef16459..d075d5037 100644 --- a/src/theory/arith/nl/transcendental_solver.cpp +++ b/src/theory/arith/nl/transcendental_solver.cpp @@ -136,7 +136,7 @@ void TranscendentalSolver::initLastCall(const std::vector& assertions, } Node expn = exp.size() == 1 ? exp[0] : nm->mkNode(AND, exp); Node cong_lemma = nm->mkNode(OR, expn.negate(), a.eqNode(aa)); - lems.emplace_back(cong_lemma, Inference::CONGRUENCE); + lems.emplace_back(cong_lemma, InferenceId::NL_CONGRUENCE); } } else @@ -213,7 +213,7 @@ void TranscendentalSolver::initLastCall(const std::vector& assertions, Trace("nl-ext-lemma") << "NonlinearExtension::Lemma : purify : " << lem << std::endl; NlLemma nlem( - lem, LemmaProperty::PREPROCESS, nullptr, Inference::T_PURIFY_ARG); + lem, LemmaProperty::PREPROCESS, nullptr, InferenceId::NL_T_PURIFY_ARG); lems.emplace_back(nlem); } @@ -369,7 +369,7 @@ void TranscendentalSolver::getCurrentPiBounds(std::vector& lemmas) Node pi_lem = nm->mkNode(AND, nm->mkNode(GEQ, d_pi, d_pi_bound[0]), nm->mkNode(LEQ, d_pi, d_pi_bound[1])); - lemmas.emplace_back(pi_lem, Inference::T_PI_BOUND); + lemmas.emplace_back(pi_lem, InferenceId::NL_T_PI_BOUND); } std::vector TranscendentalSolver::checkTranscendentalInitialRefine() @@ -454,7 +454,7 @@ std::vector TranscendentalSolver::checkTranscendentalInitialRefine() } if (!lem.isNull()) { - lemmas.emplace_back(lem, Inference::T_INIT_REFINE); + lemmas.emplace_back(lem, InferenceId::NL_T_INIT_REFINE); } } } @@ -630,7 +630,7 @@ std::vector TranscendentalSolver::checkTranscendentalMonotonic() } Trace("nl-ext-tf-mono") << "Monotonicity lemma : " << mono_lem << std::endl; - lemmas.emplace_back(mono_lem, Inference::T_MONOTONICITY); + lemmas.emplace_back(mono_lem, InferenceId::NL_T_MONOTONICITY); } } // store the previous values @@ -883,7 +883,7 @@ bool TranscendentalSolver::checkTfTangentPlanesFun(Node tf, << "*** Tangent plane lemma : " << lem << std::endl; Assert(d_model.computeAbstractModelValue(lem) == d_false); // Figure 3 : line 9 - lemmas.emplace_back(lem, Inference::T_TANGENT); + lemmas.emplace_back(lem, InferenceId::NL_T_TANGENT); } else if (is_secant) { @@ -1017,7 +1017,7 @@ bool TranscendentalSolver::checkTfTangentPlanesFun(Node tf, Assert(!lemmaConj.empty()); Node lem = lemmaConj.size() == 1 ? lemmaConj[0] : nm->mkNode(AND, lemmaConj); - NlLemma nlem(lem, Inference::T_SECANT); + NlLemma nlem(lem, InferenceId::NL_T_SECANT); // The side effect says that if lem is added, then we should add the // secant point c for (tf,d). nlem.d_secantPoint.push_back(std::make_tuple(tf, d, c)); diff --git a/src/theory/arith/theory_arith.cpp b/src/theory/arith/theory_arith.cpp index fbf25705c..1436198a8 100644 --- a/src/theory/arith/theory_arith.cpp +++ b/src/theory/arith/theory_arith.cpp @@ -41,7 +41,8 @@ TheoryArith::TheoryArith(context::Context* c, d_internal( new TheoryArithPrivate(*this, c, u, out, valuation, logicInfo, pnm)), d_ppRewriteTimer("theory::arith::ppRewriteTimer"), - d_astate(*d_internal, c, u, valuation) + d_astate(*d_internal, c, u, valuation), + d_inferenceManager(*this, d_astate, pnm) { smtStatisticsRegistry()->registerStat(&d_ppRewriteTimer); diff --git a/src/theory/arith/theory_arith.h b/src/theory/arith/theory_arith.h index 71a25ac12..4851f1c5d 100644 --- a/src/theory/arith/theory_arith.h +++ b/src/theory/arith/theory_arith.h @@ -19,6 +19,7 @@ #include "expr/node.h" #include "theory/arith/arith_state.h" +#include "theory/arith/inference_manager.h" #include "theory/arith/theory_arith_private_forward.h" #include "theory/theory.h" @@ -96,9 +97,19 @@ class TheoryArith : public Theory { std::pair entailmentCheck(TNode lit) override; + /** Return a reference to the arith::InferenceManager. */ + InferenceManager& getInferenceManager() + { + return d_inferenceManager; + } + private: /** The state object wrapping TheoryArithPrivate */ ArithState d_astate; + + /** The arith::InferenceManager. */ + InferenceManager d_inferenceManager; + };/* class TheoryArith */ }/* CVC4::theory::arith namespace */ -- 2.30.2