diff options
Diffstat (limited to 'src/theory/arith/nl')
-rw-r--r-- | src/theory/arith/nl/cad_solver.cpp | 8 | ||||
-rw-r--r-- | src/theory/arith/nl/iand_solver.cpp | 4 | ||||
-rw-r--r-- | src/theory/arith/nl/inference.cpp | 59 | ||||
-rw-r--r-- | src/theory/arith/nl/inference.h | 109 | ||||
-rw-r--r-- | src/theory/arith/nl/nl_lemma_utils.h | 5 | ||||
-rw-r--r-- | src/theory/arith/nl/nl_solver.cpp | 18 | ||||
-rw-r--r-- | src/theory/arith/nl/nonlinear_extension.cpp | 35 | ||||
-rw-r--r-- | src/theory/arith/nl/nonlinear_extension.h | 6 | ||||
-rw-r--r-- | src/theory/arith/nl/stats.h | 4 | ||||
-rw-r--r-- | src/theory/arith/nl/transcendental_solver.cpp | 14 |
10 files changed, 39 insertions, 223 deletions
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 <poly/polyxx.h> #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<NlLemma> 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<NlLemma> 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<NlLemma> 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<NlLemma> 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/inference.h b/src/theory/arith/nl/inference.h deleted file mode 100644 index 0cf6ad3bd..000000000 --- a/src/theory/arith/nl/inference.h +++ /dev/null @@ -1,109 +0,0 @@ -/********************* */ -/*! \file inference.h - ** \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 Inference enumeration for non-linear arithmetic. - **/ - -#include "cvc4_private.h" - -#ifndef CVC4__THEORY__ARITH__NL__INFER_INFO_H -#define CVC4__THEORY__ARITH__NL__INFER_INFO_H - -#include <map> -#include <vector> - -#include "util/safe_print.h" - -namespace CVC4 { -namespace theory { -namespace arith { -namespace nl { - -/** - * Types of inferences used in the procedure - */ -enum class Inference : uint32_t -{ - //-------------------- core - // simple congruence x=y => f(x)=f(y) - CONGRUENCE, - // shared term value split (for naive theory combination) - SHARED_TERM_VALUE_SPLIT, - //-------------------- incremental linearization solver - // splitting on zero (NlSolver::checkSplitZero) - SPLIT_ZERO, - // based on sign (NlSolver::checkMonomialSign) - SIGN, - // based on comparing (abs) model values (NlSolver::checkMonomialMagnitude) - COMPARISON, - // based on inferring bounds (NlSolver::checkMonomialInferBounds) - INFER_BOUNDS, - // same as above, for inferences that introduce new terms - INFER_BOUNDS_NT, - // factoring (NlSolver::checkFactoring) - FACTOR, - // resolution bound inferences (NlSolver::checkMonomialInferResBounds) - RES_INFER_BOUNDS, - // tangent planes (NlSolver::checkTangentPlanes) - TANGENT_PLANE, - //-------------------- transcendental solver - // purification of arguments to transcendental functions - T_PURIFY_ARG, - // initial refinement (TranscendentalSolver::checkTranscendentalInitialRefine) - T_INIT_REFINE, - // pi bounds - T_PI_BOUND, - // monotonicity (TranscendentalSolver::checkTranscendentalMonotonic) - T_MONOTONICITY, - // tangent refinement (TranscendentalSolver::checkTranscendentalTangentPlanes) - T_TANGENT, - // secant refinement, the dual of the above inference - T_SECANT, - //-------------------- iand solver - // initial refinements (IAndSolver::checkInitialRefine) - IAND_INIT_REFINE, - // value refinements (IAndSolver::checkFullRefine) - IAND_VALUE_REFINE, - //-------------------- cad solver - // conflict / infeasible subset obtained from cad - CAD_CONFLICT, - // excludes an interval for a single variable - CAD_EXCLUDED_INTERVAL, - //-------------------- unknown - UNKNOWN, -}; - -/** - * Converts an inference to a string. Note: This function is also used in - * `safe_print()`. Changing this functions name or signature will result in - * `safe_print()` printing "<unsupported>" instead of the proper strings for - * the enum values. - * - * @param i The inference - * @return The name of the inference - */ -const char* toString(Inference i); - -/** - * Writes an inference name to a stream. - * - * @param out The stream to write to - * @param i The inference to write to the stream - * @return The stream - */ -std::ostream& operator<<(std::ostream& out, Inference i); - -} // namespace nl -} // namespace arith -} // namespace theory -} // namespace CVC4 - -#endif /* CVC4__THEORY__ARITH__NL__INFER_INFO_H */ 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<NlLemma> 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<Rational>().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<NlLemma> 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<NlLemma> 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<NlLemma> 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<NlLemma> 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<NlLemma>& 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<NlLemma>& 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<NlLemma>& 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<NlLemma>& 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<Inference> d_inferences; + HistogramStat<InferenceId> 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<Node>& 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<Node>& 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<NlLemma>& 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<NlLemma> TranscendentalSolver::checkTranscendentalInitialRefine() @@ -454,7 +454,7 @@ std::vector<NlLemma> 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<NlLemma> 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)); |