summaryrefslogtreecommitdiff
path: root/src/theory/arith/nl
diff options
context:
space:
mode:
Diffstat (limited to 'src/theory/arith/nl')
-rw-r--r--src/theory/arith/nl/cad_solver.cpp8
-rw-r--r--src/theory/arith/nl/iand_solver.cpp4
-rw-r--r--src/theory/arith/nl/inference.cpp59
-rw-r--r--src/theory/arith/nl/inference.h109
-rw-r--r--src/theory/arith/nl/nl_lemma_utils.h5
-rw-r--r--src/theory/arith/nl/nl_solver.cpp18
-rw-r--r--src/theory/arith/nl/nonlinear_extension.cpp35
-rw-r--r--src/theory/arith/nl/nonlinear_extension.h6
-rw-r--r--src/theory/arith/nl/stats.h4
-rw-r--r--src/theory/arith/nl/transcendental_solver.cpp14
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));
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback