This marks all lemmas in non-linear arithmetic with an identifier, which indicates informally the kind of justification that was used for them. The main motivation for this is for debugging the behavior of the non-linear solver.
The number of inferences can then be seen with --stats:
nl::inferences, [(SPLIT_ZERO : 19), (SIGN : 4), (COMPARISON : 29)]
The same design was used in strings and has been quite helpful.
This also adds a few high level stats to the new statistics class for non-linear.
theory/arith/matrix.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
theory/arith/nl/nl_solver.h
theory/arith/nl/nonlinear_extension.cpp
theory/arith/nl/nonlinear_extension.h
+ theory/arith/nl/stats.cpp
+ theory/arith/nl/stats.h
theory/arith/nl/transcendental_solver.cpp
theory/arith/nl/transcendental_solver.h
theory/arith/normal_form.cpp
--- /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";
+ 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,
+ //-------------------- 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 <tuple>
#include <vector>
#include "expr/node.h"
+#include "theory/arith/nl/inference.h"
namespace CVC4 {
namespace theory {
*/
struct NlLemma
{
- NlLemma(Node lem) : d_lemma(lem), d_preprocess(false) {}
+ NlLemma(Node lem, Inference id = Inference::UNKNOWN)
+ : d_id(id), d_lemma(lem), d_preprocess(false)
+ {
+ }
~NlLemma() {}
+ /** The inference id for the lemma */
+ Inference d_id;
/** The lemma */
Node d_lemma;
/** Whether to preprocess the lemma */
eq = Rewriter::rewrite(eq);
Node literal = d_containing.getValuation().ensureLiteral(eq);
d_containing.getOutputChannel().requirePhase(literal, true);
- lemmas.push_back(literal.orNode(literal.negate()));
+ lemmas.emplace_back(literal.orNode(literal.negate()),
+ Inference::SPLIT_ZERO);
}
}
return lemmas;
{
Node lemma =
safeConstructNary(AND, exp).impNode(mkLit(oa, d_zero, status * 2));
- lem.push_back(lemma);
+ lem.emplace_back(lemma, Inference::SIGN);
}
return status;
}
if (mvaoa.getConst<Rational>().sgn() != 0)
{
Node lemma = av.eqNode(d_zero).impNode(oa.eqNode(d_zero));
- lem.push_back(lemma);
+ lem.emplace_back(lemma, Inference::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.push_back(clem);
+ lem.emplace_back(clem, Inference::COMPARISON);
cmp_infers[status][oa][ob] = clem;
}
return true;
nm->mkNode(
PLUS, nm->mkNode(MULT, b_v, a), nm->mkNode(MULT, a_v, b)),
nm->mkNode(MULT, a_v, b_v));
+ // conjuncts of the tangent plane lemma
+ std::vector<Node> tplaneConj;
for (unsigned d = 0; d < 4; d++)
{
Node aa = nm->mkNode(d == 0 || d == 3 ? GEQ : LEQ, a, a_v);
Node tlem = nm->mkNode(OR, aa.negate(), ab.negate(), conc);
Trace("nl-ext-tplanes")
<< "Tangent plane lemma : " << tlem << std::endl;
- lemmas.push_back(tlem);
+ tplaneConj.push_back(tlem);
}
// tangent plane reverse implication
Trace("nl-ext-tplanes")
<< "Tangent plane lemma (reverse) : " << ub_reverse1
<< std::endl;
- lemmas.push_back(ub_reverse1);
+ tplaneConj.push_back(ub_reverse1);
Node ub_reverse2 =
nm->mkNode(OR, t_leq_tplane.negate(), b_geq_bv_or_a_geq_av);
Trace("nl-ext-tplanes")
<< "Tangent plane lemma (reverse) : " << ub_reverse2
<< std::endl;
- lemmas.push_back(ub_reverse2);
+ tplaneConj.push_back(ub_reverse2);
// t >= tplane -> ( (a <= a_v ^ b <= b_v) v
// (a >= a_v ^ b >= b_v) ).
Trace("nl-ext-tplanes")
<< "Tangent plane lemma (reverse) : " << lb_reverse1
<< std::endl;
- lemmas.push_back(lb_reverse1);
+ tplaneConj.push_back(lb_reverse1);
Node lb_reverse2 =
nm->mkNode(OR, t_geq_tplane.negate(), a_geq_av_or_b_leq_bv);
Trace("nl-ext-tplanes")
<< "Tangent plane lemma (reverse) : " << lb_reverse2
<< std::endl;
- lemmas.push_back(lb_reverse2);
+ tplaneConj.push_back(lb_reverse2);
+
+ Node tlem = nm->mkNode(AND, tplaneConj);
+ lemmas.emplace_back(tlem, Inference::TANGENT_PLANE);
}
}
}
// monomials = " << introNewTerms << std::endl;
if (!introNewTerms)
{
- lemmas.push_back(iblem);
+ lemmas.emplace_back(iblem, Inference::INFER_BOUNDS);
}
else
{
- nt_lemmas.push_back(iblem);
+ nt_lemmas.emplace_back(iblem, Inference::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.push_back(flem);
+ lemmas.emplace_back(flem, Inference::FACTOR);
}
}
}
rblem = Rewriter::rewrite(rblem);
Trace("nl-ext-rbound-lemma")
<< "Resolution bound lemma : " << rblem << std::endl;
- lemmas.push_back(rblem);
+ lemmas.emplace_back(rblem, Inference::RES_INFER_BOUNDS);
}
}
exp.pop_back();
{
Node lem = nlem.d_lemma;
bool preprocess = nlem.d_preprocess;
- Trace("nl-ext-lemma") << "NonlinearExtension::Lemma : " << lem << std::endl;
+ Trace("nl-ext-lemma") << "NonlinearExtension::Lemma : " << nlem.d_id
+ << " : " << lem << std::endl;
d_containing.getOutputChannel().lemma(lem, false, preprocess);
// process the side effect
processSideEffect(nlem);
{
d_lemmas.insert(lem);
}
+ d_stats.d_inferences << nlem.d_id;
// also indicate this is a tautology
d_model.addTautology(lem);
}
<< "NonlinearExtension::Lemma duplicate : " << lem.d_lemma << std::endl;
return 0;
}
- out.push_back(lem);
+ out.emplace_back(lem);
return 1;
}
{
std::vector<NlLemma> lemmas;
+ ++(d_stats.d_checkRuns);
+
if (options::nlExt())
{
// initialize the non-linear solver
bool NonlinearExtension::modelBasedRefinement(std::vector<NlLemma>& mlems)
{
+ ++(d_stats.d_mbrRuns);
+
// get the assertions
std::vector<Node> assertions;
getAssertions(assertions);
<< "Getting model values... check for [model-false]" << std::endl;
// get the assertions that are false in the model
const std::vector<Node> false_asserts = checkModelEval(assertions);
+ Trace("nl-ext") << "# false asserts = " << false_asserts.size() << std::endl;
// get the extended terms belonging to this theory
std::vector<Node> xts;
d_containing.getOutputChannel().requirePhase(literal, true);
Trace("nl-ext-debug") << "Split on : " << literal << std::endl;
Node split = literal.orNode(literal.negate());
- filterLemma(split, stvLemmas);
+ NlLemma nsplit(split, Inference::SHARED_TERM_VALUE_SPLIT);
+ filterLemma(nsplit, stvLemmas);
}
if (!stvLemmas.empty())
{
#include "theory/arith/nl/nl_lemma_utils.h"
#include "theory/arith/nl/nl_model.h"
#include "theory/arith/nl/nl_solver.h"
+#include "theory/arith/nl/stats.h"
#include "theory/arith/nl/transcendental_solver.h"
#include "theory/arith/theory_arith.h"
#include "theory/uf/equality_engine.h"
TheoryArith& d_containing;
// pointer to used equality engine
eq::EqualityEngine* d_ee;
+ /** The statistics class */
+ NlStats d_stats;
// needs last call effort
bool d_needsLastCall;
/** The non-linear model object
--- /dev/null
+/********************* */
+/*! \file stats.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 Statistics for non-linear arithmetic
+ **/
+
+#include "theory/arith/nl/stats.h"
+
+#include "smt/smt_statistics_registry.h"
+
+namespace CVC4 {
+namespace theory {
+namespace arith {
+namespace nl {
+
+NlStats::NlStats()
+ : d_mbrRuns("nl::mbrRuns", 0),
+ d_checkRuns("nl::checkRuns", 0),
+ d_inferences("nl::inferences")
+{
+ smtStatisticsRegistry()->registerStat(&d_mbrRuns);
+ smtStatisticsRegistry()->registerStat(&d_checkRuns);
+ smtStatisticsRegistry()->registerStat(&d_inferences);
+}
+
+NlStats::~NlStats()
+{
+ smtStatisticsRegistry()->unregisterStat(&d_mbrRuns);
+ smtStatisticsRegistry()->unregisterStat(&d_checkRuns);
+ smtStatisticsRegistry()->unregisterStat(&d_inferences);
+}
+
+} // namespace nl
+} // namespace arith
+} // namespace theory
+} // namespace CVC4
--- /dev/null
+/********************* */
+/*! \file stats.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 Statistics for non-linear arithmetic
+ **/
+
+#include "cvc4_private.h"
+
+#ifndef CVC4__THEORY__ARITH__NL__STATS_H
+#define CVC4__THEORY__ARITH__NL__STATS_H
+
+#include "expr/kind.h"
+#include "theory/arith/nl/inference.h"
+#include "util/statistics_registry.h"
+
+namespace CVC4 {
+namespace theory {
+namespace arith {
+namespace nl {
+
+/**
+ * Statistics for non-linear arithmetic
+ */
+class NlStats
+{
+ public:
+ NlStats();
+ ~NlStats();
+ /**
+ * Number of calls to NonlinearExtension::modelBasedRefinement. Notice this
+ * may make multiple calls to NonlinearExtension::checkLastCall.
+ */
+ IntStat d_mbrRuns;
+ /** Number of calls to NonlinearExtension::checkLastCall */
+ IntStat d_checkRuns;
+ /** Counts the number of applications of each type of inference */
+ HistogramStat<Inference> d_inferences;
+};
+
+} // namespace nl
+} // namespace arith
+} // namespace theory
+} // namespace CVC4
+
+#endif /* CVC4__THEORY__ARITH__NL__STATS_H */
}
Node expn = exp.size() == 1 ? exp[0] : nm->mkNode(AND, exp);
Node cong_lemma = nm->mkNode(OR, expn.negate(), a.eqNode(aa));
- lems.push_back(cong_lemma);
+ lems.emplace_back(cong_lemma, Inference::CONGRUENCE);
}
}
else
// note we must do preprocess on this lemma
Trace("nl-ext-lemma") << "NonlinearExtension::Lemma : purify : " << lem
<< std::endl;
- NlLemma nlem(lem);
+ NlLemma nlem(lem, Inference::T_PURIFY_ARG);
nlem.d_preprocess = true;
- lems.push_back(nlem);
+ lems.emplace_back(nlem);
}
if (Trace.isOn("nl-ext-mv"))
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.push_back(pi_lem);
+ lemmas.emplace_back(pi_lem, Inference::T_PI_BOUND);
}
std::vector<NlLemma> TranscendentalSolver::checkTranscendentalInitialRefine()
}
if (!lem.isNull())
{
- lemmas.push_back(lem);
+ lemmas.emplace_back(lem, Inference::T_INIT_REFINE);
}
}
}
}
Trace("nl-ext-tf-mono")
<< "Monotonicity lemma : " << mono_lem << std::endl;
- lemmas.push_back(mono_lem);
+ lemmas.emplace_back(mono_lem, Inference::T_MONOTONICITY);
}
}
// store the previous values
<< "*** Tangent plane lemma : " << lem << std::endl;
Assert(d_model.computeAbstractModelValue(lem) == d_false);
// Figure 3 : line 9
- lemmas.push_back(lem);
+ lemmas.emplace_back(lem, Inference::T_TANGENT);
}
else if (is_secant)
{
Assert(!lemmaConj.empty());
Node lem =
lemmaConj.size() == 1 ? lemmaConj[0] : nm->mkNode(AND, lemmaConj);
- NlLemma nlem(lem);
+ NlLemma nlem(lem, Inference::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));
- lemmas.push_back(nlem);
+ lemmas.emplace_back(nlem);
}
return true;
}
projects / cvc5.git / commitdiff