From 68df2d8d6c9218fe6a9bf01d22c7dfe2abdf684d Mon Sep 17 00:00:00 2001 From: Andrew Reynolds Date: Thu, 9 Jul 2020 15:21:08 -0500 Subject: [PATCH] Associate all lemmas in non-linear arithmetic with an inference identifier (#4712) 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. --- src/CMakeLists.txt | 4 + src/theory/arith/nl/inference.cpp | 55 +++++++++++ src/theory/arith/nl/inference.h | 99 +++++++++++++++++++ src/theory/arith/nl/nl_lemma_utils.h | 8 +- src/theory/arith/nl/nl_solver.cpp | 32 +++--- src/theory/arith/nl/nonlinear_extension.cpp | 14 ++- src/theory/arith/nl/nonlinear_extension.h | 3 + src/theory/arith/nl/stats.cpp | 44 +++++++++ src/theory/arith/nl/stats.h | 53 ++++++++++ src/theory/arith/nl/transcendental_solver.cpp | 18 ++-- 10 files changed, 304 insertions(+), 26 deletions(-) create mode 100644 src/theory/arith/nl/inference.cpp create mode 100644 src/theory/arith/nl/inference.h create mode 100644 src/theory/arith/nl/stats.cpp create mode 100644 src/theory/arith/nl/stats.h diff --git a/src/CMakeLists.txt b/src/CMakeLists.txt index 1b7236d3a..9331b1dc7 100644 --- a/src/CMakeLists.txt +++ b/src/CMakeLists.txt @@ -302,6 +302,8 @@ libcvc4_add_sources( 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 @@ -314,6 +316,8 @@ libcvc4_add_sources( 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 diff --git a/src/theory/arith/nl/inference.cpp b/src/theory/arith/nl/inference.cpp new file mode 100644 index 000000000..34242e746 --- /dev/null +++ b/src/theory/arith/nl/inference.cpp @@ -0,0 +1,55 @@ +/********************* */ +/*! \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 diff --git a/src/theory/arith/nl/inference.h b/src/theory/arith/nl/inference.h new file mode 100644 index 000000000..99b7e681e --- /dev/null +++ b/src/theory/arith/nl/inference.h @@ -0,0 +1,99 @@ +/********************* */ +/*! \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 +#include + +#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 "" 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 eaa9adcc3..2b5158f18 100644 --- a/src/theory/arith/nl/nl_lemma_utils.h +++ b/src/theory/arith/nl/nl_lemma_utils.h @@ -18,6 +18,7 @@ #include #include #include "expr/node.h" +#include "theory/arith/nl/inference.h" namespace CVC4 { namespace theory { @@ -39,8 +40,13 @@ class NlModel; */ 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 */ diff --git a/src/theory/arith/nl/nl_solver.cpp b/src/theory/arith/nl/nl_solver.cpp index fee89caf6..521539674 100644 --- a/src/theory/arith/nl/nl_solver.cpp +++ b/src/theory/arith/nl/nl_solver.cpp @@ -177,7 +177,8 @@ std::vector NlSolver::checkSplitZero() 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; @@ -273,7 +274,7 @@ int NlSolver::compareSign(Node oa, { Node lemma = safeConstructNary(AND, exp).impNode(mkLit(oa, d_zero, status * 2)); - lem.push_back(lemma); + lem.emplace_back(lemma, Inference::SIGN); } return status; } @@ -290,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.push_back(lemma); + lem.emplace_back(lemma, Inference::SIGN); } return 0; } @@ -447,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.push_back(clem); + lem.emplace_back(clem, Inference::COMPARISON); cmp_infers[status][oa][ob] = clem; } return true; @@ -943,6 +944,8 @@ std::vector NlSolver::checkTangentPlanes() 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 tplaneConj; for (unsigned d = 0; d < 4; d++) { Node aa = nm->mkNode(d == 0 || d == 3 ? GEQ : LEQ, a, a_v); @@ -951,7 +954,7 @@ std::vector NlSolver::checkTangentPlanes() 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 @@ -974,13 +977,13 @@ std::vector NlSolver::checkTangentPlanes() 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) ). @@ -995,13 +998,16 @@ std::vector NlSolver::checkTangentPlanes() 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); } } } @@ -1256,11 +1262,11 @@ std::vector NlSolver::checkMonomialInferBounds( // 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); } } } @@ -1392,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.push_back(flem); + lemmas.emplace_back(flem, Inference::FACTOR); } } } @@ -1564,7 +1570,7 @@ std::vector NlSolver::checkMonomialInferResBounds() 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(); diff --git a/src/theory/arith/nl/nonlinear_extension.cpp b/src/theory/arith/nl/nonlinear_extension.cpp index bd48a726a..97f0ce2c1 100644 --- a/src/theory/arith/nl/nonlinear_extension.cpp +++ b/src/theory/arith/nl/nonlinear_extension.cpp @@ -152,7 +152,8 @@ void NonlinearExtension::sendLemmas(const std::vector& out) { 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); @@ -165,6 +166,7 @@ void NonlinearExtension::sendLemmas(const std::vector& out) { d_lemmas.insert(lem); } + d_stats.d_inferences << nlem.d_id; // also indicate this is a tautology d_model.addTautology(lem); } @@ -188,7 +190,7 @@ unsigned NonlinearExtension::filterLemma(NlLemma lem, std::vector& out) << "NonlinearExtension::Lemma duplicate : " << lem.d_lemma << std::endl; return 0; } - out.push_back(lem); + out.emplace_back(lem); return 1; } @@ -405,6 +407,8 @@ int NonlinearExtension::checkLastCall(const std::vector& assertions, { std::vector lemmas; + ++(d_stats.d_checkRuns); + if (options::nlExt()) { // initialize the non-linear solver @@ -639,6 +643,8 @@ void NonlinearExtension::check(Theory::Effort e) bool NonlinearExtension::modelBasedRefinement(std::vector& mlems) { + ++(d_stats.d_mbrRuns); + // get the assertions std::vector assertions; getAssertions(assertions); @@ -647,6 +653,7 @@ bool NonlinearExtension::modelBasedRefinement(std::vector& mlems) << "Getting model values... check for [model-false]" << std::endl; // get the assertions that are false in the model const std::vector false_asserts = checkModelEval(assertions); + Trace("nl-ext") << "# false asserts = " << false_asserts.size() << std::endl; // get the extended terms belonging to this theory std::vector xts; @@ -786,7 +793,8 @@ 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()); - filterLemma(split, stvLemmas); + NlLemma nsplit(split, Inference::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 ed1838b4b..69710265c 100644 --- a/src/theory/arith/nl/nonlinear_extension.h +++ b/src/theory/arith/nl/nonlinear_extension.h @@ -29,6 +29,7 @@ #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" @@ -284,6 +285,8 @@ class NonlinearExtension 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 diff --git a/src/theory/arith/nl/stats.cpp b/src/theory/arith/nl/stats.cpp new file mode 100644 index 000000000..e189d13a8 --- /dev/null +++ b/src/theory/arith/nl/stats.cpp @@ -0,0 +1,44 @@ +/********************* */ +/*! \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 diff --git a/src/theory/arith/nl/stats.h b/src/theory/arith/nl/stats.h new file mode 100644 index 000000000..1a8a9419e --- /dev/null +++ b/src/theory/arith/nl/stats.h @@ -0,0 +1,53 @@ +/********************* */ +/*! \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 d_inferences; +}; + +} // namespace nl +} // namespace arith +} // namespace theory +} // namespace CVC4 + +#endif /* CVC4__THEORY__ARITH__NL__STATS_H */ diff --git a/src/theory/arith/nl/transcendental_solver.cpp b/src/theory/arith/nl/transcendental_solver.cpp index 1a80342bc..321818b94 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.push_back(cong_lemma); + lems.emplace_back(cong_lemma, Inference::CONGRUENCE); } } else @@ -212,9 +212,9 @@ void TranscendentalSolver::initLastCall(const std::vector& assertions, // 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")) @@ -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.push_back(pi_lem); + lemmas.emplace_back(pi_lem, Inference::T_PI_BOUND); } std::vector TranscendentalSolver::checkTranscendentalInitialRefine() @@ -454,7 +454,7 @@ std::vector TranscendentalSolver::checkTranscendentalInitialRefine() } if (!lem.isNull()) { - lemmas.push_back(lem); + lemmas.emplace_back(lem, Inference::T_INIT_REFINE); } } } @@ -630,7 +630,7 @@ std::vector TranscendentalSolver::checkTranscendentalMonotonic() } 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 @@ -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.push_back(lem); + lemmas.emplace_back(lem, Inference::T_TANGENT); } else if (is_secant) { @@ -1017,11 +1017,11 @@ bool TranscendentalSolver::checkTfTangentPlanesFun(Node tf, 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; } -- 2.30.2