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.
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
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
#include <vector>
#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"
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.
--- /dev/null
+/********************* */
+/*! \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
--- /dev/null
+/********************* */
+/*! \file inference_id.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 arithmetic.
+ **/
+
+#include "cvc4_private.h"
+
+#ifndef CVC4__THEORY__ARITH__INFERENCE_ID_H
+#define CVC4__THEORY__ARITH__INFERENCE_ID_H
+
+#include <map>
+#include <vector>
+
+#include "util/safe_print.h"
+
+namespace CVC4 {
+namespace theory {
+namespace arith {
+
+/**
+ * Types of inferences used in the procedure
+ */
+enum class InferenceId : uint32_t
+{
+ //-------------------- core
+ // simple congruence x=y => f(x)=f(y)
+ NL_CONGRUENCE,
+ // shared term value split (for naive theory combination)
+ NL_SHARED_TERM_VALUE_SPLIT,
+ //-------------------- incremental linearization solver
+ // splitting on zero (NlSolver::checkSplitZero)
+ NL_SPLIT_ZERO,
+ // based on sign (NlSolver::checkMonomialSign)
+ NL_SIGN,
+ // based on comparing (abs) model values (NlSolver::checkMonomialMagnitude)
+ NL_COMPARISON,
+ // based on inferring bounds (NlSolver::checkMonomialInferBounds)
+ NL_INFER_BOUNDS,
+ // same as above, for inferences that introduce new terms
+ NL_INFER_BOUNDS_NT,
+ // factoring (NlSolver::checkFactoring)
+ NL_FACTOR,
+ // resolution bound inferences (NlSolver::checkMonomialInferResBounds)
+ NL_RES_INFER_BOUNDS,
+ // tangent planes (NlSolver::checkTangentPlanes)
+ NL_TANGENT_PLANE,
+ //-------------------- transcendental solver
+ // purification of arguments to transcendental functions
+ NL_T_PURIFY_ARG,
+ // initial refinement (TranscendentalSolver::checkTranscendentalInitialRefine)
+ NL_T_INIT_REFINE,
+ // pi bounds
+ NL_T_PI_BOUND,
+ // monotonicity (TranscendentalSolver::checkTranscendentalMonotonic)
+ NL_T_MONOTONICITY,
+ // tangent refinement (TranscendentalSolver::checkTranscendentalTangentPlanes)
+ NL_T_TANGENT,
+ // secant refinement, the dual of the above inference
+ NL_T_SECANT,
+ //-------------------- iand solver
+ // initial refinements (IAndSolver::checkInitialRefine)
+ NL_IAND_INIT_REFINE,
+ // value refinements (IAndSolver::checkFullRefine)
+ NL_IAND_VALUE_REFINE,
+ //-------------------- cad solver
+ // conflict / infeasible subset obtained from cad
+ NL_CAD_CONFLICT,
+ // excludes an interval for a single variable
+ NL_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(InferenceId 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, InferenceId i);
+
+} // namespace arith
+} // namespace theory
+} // namespace CVC4
+
+#endif /* CVC4__THEORY__ARITH__INFERENCE_H */
isWaiting);
}
void InferenceManager::addPendingArithLemma(const Node& lemma,
- nl::Inference inftype,
+ InferenceId inftype,
bool isWaiting)
{
addPendingArithLemma(std::unique_ptr<ArithLemma>(new ArithLemma(
d_waitingLem.clear();
}
-void InferenceManager::addConflict(const Node& conf, nl::Inference inftype)
+void InferenceManager::addConflict(const Node& conf, InferenceId inftype)
{
conflict(Rewriter::rewrite(conf));
}
#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"
* added as pending lemma when calling flushWaitingLemmas.
*/
void addPendingArithLemma(const Node& lemma,
- nl::Inference inftype,
+ InferenceId inftype,
bool isWaiting = false);
/**
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;
#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"
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;
}
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);
}
}
}
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;
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);
}
}
}
+++ /dev/null
-/********************* */
-/*! \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
+++ /dev/null
-/********************* */
-/*! \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 */
#include "expr/node.h"
#include "theory/arith/arith_lemma.h"
-#include "theory/arith/nl/inference.h"
#include "theory/output_channel.h"
namespace CVC4 {
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)
{
}
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;
{
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;
}
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;
}
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;
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);
}
}
}
// 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);
}
}
}
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);
}
}
}
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();
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),
{
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;
}
}
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;
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
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())
#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"
*/
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;
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 */
#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 {
/** 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
}
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
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);
}
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()
}
if (!lem.isNull())
{
- lemmas.emplace_back(lem, Inference::T_INIT_REFINE);
+ lemmas.emplace_back(lem, InferenceId::NL_T_INIT_REFINE);
}
}
}
}
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
<< "*** 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)
{
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));
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);
#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"
std::pair<bool, Node> 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 */
projects / cvc5.git / commitdiff