This makes it much easier to set custom properties of lemmas (e.g. preprocess) and also will allow proof tracking and debugging in the future.
This also enables a fix on the IAND branch related to preprocessing lemmas.
namespace arith {
namespace nl {
+std::ostream& operator<<(std::ostream& out, NlLemma& n)
+{
+ out << n.d_lemma;
+ return out;
+}
+
bool SortNlModel::operator()(Node i, Node j)
{
int cv = d_nlm->compare(i, j, d_isConcrete, d_isAbsolute);
class NlModel;
/**
- * A side effect of adding a lemma in the non-linear solver. This is used
- * to specify how the state of the non-linear solver should update. This
- * includes:
+ * The data structure for a single lemma to process by the non-linear solver,
+ * including the lemma itself and whether it should be preprocessed (see
+ * OutputChannel::lemma).
+ *
+ * This also includes data structures that encapsulate the side effect of adding
+ * this lemma in the non-linear solver. This is used to specify how the state of
+ * the non-linear solver should update. This includes:
* - A set of secant points to record (for transcendental secant plane
* inferences).
*/
-struct NlLemmaSideEffect
+struct NlLemma
{
- NlLemmaSideEffect() {}
- ~NlLemmaSideEffect() {}
+ NlLemma(Node lem) : d_lemma(lem), d_preprocess(false) {}
+ ~NlLemma() {}
+ /** The lemma */
+ Node d_lemma;
+ /** Whether to preprocess the lemma */
+ bool d_preprocess;
/** secant points to add
*
* A member (tf, d, c) in this vector indicates that point c should be added
*/
std::vector<std::tuple<Node, unsigned, Node> > d_secantPoint;
};
+/**
+ * Writes a non-linear lemma to a stream.
+ */
+std::ostream& operator<<(std::ostream& out, NlLemma& n);
struct SortNlModel
{
bool NlModel::checkModel(const std::vector<Node>& assertions,
const std::vector<Node>& false_asserts,
unsigned d,
- std::vector<Node>& lemmas,
+ std::vector<NlLemma>& lemmas,
std::vector<Node>& gs)
{
Trace("nl-ext-cm-debug") << " solve for equalities..." << std::endl;
bool NlModel::solveEqualitySimple(Node eq,
unsigned d,
- std::vector<Node>& lemmas)
+ std::vector<NlLemma>& lemmas)
{
Node seq = eq;
if (!d_check_model_vars.empty())
#include "context/context.h"
#include "expr/kind.h"
#include "expr/node.h"
+#include "theory/arith/nl/nl_lemma_utils.h"
#include "theory/theory_model.h"
namespace CVC4 {
bool checkModel(const std::vector<Node>& assertions,
const std::vector<Node>& false_asserts,
unsigned d,
- std::vector<Node>& lemmas,
+ std::vector<NlLemma>& lemmas,
std::vector<Node>& gs);
/**
* Set that we have used an approximation during this check. This flag is
* For instance, if eq reduces to a univariate quadratic equation with no
* root, we send a conflict clause of the form a*x^2 + b*x + c != 0.
*/
- bool solveEqualitySimple(Node eq, unsigned d, std::vector<Node>& lemmas);
+ bool solveEqualitySimple(Node eq, unsigned d, std::vector<NlLemma>& lemmas);
/** simple check model for transcendental functions for literal
*
}
}
-std::vector<Node> NlSolver::checkSplitZero()
+std::vector<NlLemma> NlSolver::checkSplitZero()
{
- std::vector<Node> lemmas;
+ std::vector<NlLemma> lemmas;
for (unsigned i = 0; i < d_ms_vars.size(); i++)
{
Node v = d_ms_vars[i];
unsigned a_index,
int status,
std::vector<Node>& exp,
- std::vector<Node>& lem)
+ std::vector<NlLemma>& lem)
{
Trace("nl-ext-debug") << "Process " << a << " at index " << a_index
<< ", status is " << status << std::endl;
Node b,
NodeMultiset& b_exp_proc,
std::vector<Node>& exp,
- std::vector<Node>& lem,
+ std::vector<NlLemma>& lem,
std::map<int, std::map<Node, std::map<Node, Node> > >& cmp_infers)
{
Trace("nl-ext-comp-debug")
NodeMultiset& b_exp_proc,
int status,
std::vector<Node>& exp,
- std::vector<Node>& lem,
+ std::vector<NlLemma>& lem,
std::map<int, std::map<Node, std::map<Node, Node> > >& cmp_infers)
{
Trace("nl-ext-comp-debug")
return false;
}
-std::vector<Node> NlSolver::checkMonomialSign()
+std::vector<NlLemma> NlSolver::checkMonomialSign()
{
- std::vector<Node> lemmas;
+ std::vector<NlLemma> lemmas;
std::map<Node, int> signs;
Trace("nl-ext") << "Get monomial sign lemmas..." << std::endl;
for (unsigned j = 0; j < d_ms.size(); j++)
return lemmas;
}
-std::vector<Node> NlSolver::checkMonomialMagnitude(unsigned c)
+std::vector<NlLemma> NlSolver::checkMonomialMagnitude(unsigned c)
{
// ensure information is setup
if (c == 0)
}
unsigned r = 1;
- std::vector<Node> lemmas;
+ std::vector<NlLemma> lemmas;
// if (x,y,L) in cmp_infers, then x > y inferred as conclusion of L
// in lemmas
std::map<int, std::map<Node, std::map<Node, Node> > > cmp_infers;
Trace("nl-ext-comp") << "Compute redundancies for " << lemmas.size()
<< " lemmas." << std::endl;
// naive
- std::vector<Node> r_lemmas;
+ std::unordered_set<Node, NodeHashFunction> r_lemmas;
for (std::map<int, std::map<Node, std::map<Node, Node> > >::iterator itb =
cmp_infers.begin();
itb != cmp_infers.end();
std::vector<Node> exp;
if (cmp_holds(itc3->first, itc2->first, itb->second, exp, visited))
{
- r_lemmas.push_back(itc2->second);
+ r_lemmas.insert(itc2->second);
Trace("nl-ext-comp")
<< "...inference of " << itc->first << " > " << itc2->first
<< " was redundant." << std::endl;
}
}
}
- std::vector<Node> nr_lemmas;
+ std::vector<NlLemma> nr_lemmas;
for (unsigned i = 0; i < lemmas.size(); i++)
{
- if (std::find(r_lemmas.begin(), r_lemmas.end(), lemmas[i])
- == r_lemmas.end())
+ if (r_lemmas.find(lemmas[i].d_lemma) == r_lemmas.end())
{
nr_lemmas.push_back(lemmas[i]);
}
return nr_lemmas;
}
-std::vector<Node> NlSolver::checkTangentPlanes()
+std::vector<NlLemma> NlSolver::checkTangentPlanes()
{
- std::vector<Node> lemmas;
+ std::vector<NlLemma> lemmas;
Trace("nl-ext") << "Get monomial tangent plane lemmas..." << std::endl;
NodeManager* nm = NodeManager::currentNM();
const std::map<Node, std::vector<Node> >& ccMap =
return lemmas;
}
-std::vector<Node> NlSolver::checkMonomialInferBounds(
- std::vector<Node>& nt_lemmas,
+std::vector<NlLemma> NlSolver::checkMonomialInferBounds(
+ std::vector<NlLemma>& nt_lemmas,
const std::vector<Node>& asserts,
const std::vector<Node>& false_asserts)
{
const std::map<Node, std::map<Node, ConstraintInfo> >& cim =
d_cdb.getConstraints();
- std::vector<Node> lemmas;
+ std::vector<NlLemma> lemmas;
NodeManager* nm = NodeManager::currentNM();
// register constraints
Trace("nl-ext-debug") << "Register bound constraints..." << std::endl;
return lemmas;
}
-std::vector<Node> NlSolver::checkFactoring(
+std::vector<NlLemma> NlSolver::checkFactoring(
const std::vector<Node>& asserts, const std::vector<Node>& false_asserts)
{
- std::vector<Node> lemmas;
+ std::vector<NlLemma> lemmas;
NodeManager* nm = NodeManager::currentNM();
Trace("nl-ext") << "Get factoring lemmas..." << std::endl;
for (const Node& lit : asserts)
return lemmas;
}
-Node NlSolver::getFactorSkolem(Node n, std::vector<Node>& lemmas)
+Node NlSolver::getFactorSkolem(Node n, std::vector<NlLemma>& lemmas)
{
std::map<Node, Node>::iterator itf = d_factor_skolem.find(n);
if (itf == d_factor_skolem.end())
return itf->second;
}
-std::vector<Node> NlSolver::checkMonomialInferResBounds()
+std::vector<NlLemma> NlSolver::checkMonomialInferResBounds()
{
- std::vector<Node> lemmas;
+ std::vector<NlLemma> lemmas;
NodeManager* nm = NodeManager::currentNM();
Trace("nl-ext") << "Get monomial resolution inferred bound lemmas..."
<< std::endl;
* t = 0 V t != 0
* where t is a term that exists in the current context.
*/
- std::vector<Node> checkSplitZero();
+ std::vector<NlLemma> checkSplitZero();
/** check monomial sign
*
* x < 0 => x*y*y < 0
* x = 0 => x*y*z = 0
*/
- std::vector<Node> checkMonomialSign();
+ std::vector<NlLemma> checkMonomialSign();
/** check monomial magnitude
*
* against 1, 1 : compare non-linear monomials against variables, 2 : compare
* non-linear monomials against other non-linear monomials.
*/
- std::vector<Node> checkMonomialMagnitude(unsigned c);
+ std::vector<NlLemma> checkMonomialMagnitude(unsigned c);
/** check monomial inferred bounds
*
* ...where (y > z + w) and x*y are a constraint and term
* that occur in the current context.
*/
- std::vector<Node> checkMonomialInferBounds(
- std::vector<Node>& nt_lemmas,
+ std::vector<NlLemma> checkMonomialInferBounds(
+ std::vector<NlLemma>& nt_lemmas,
const std::vector<Node>& asserts,
const std::vector<Node>& false_asserts);
* ...where k is fresh and x*z + y*z > t is a
* constraint that occurs in the current context.
*/
- std::vector<Node> checkFactoring(const std::vector<Node>& asserts,
- const std::vector<Node>& false_asserts);
+ std::vector<NlLemma> checkFactoring(const std::vector<Node>& asserts,
+ const std::vector<Node>& false_asserts);
/** check monomial infer resolution bounds
*
* ...where s <= x*z and x*y <= t are constraints
* that occur in the current context.
*/
- std::vector<Node> checkMonomialInferResBounds();
+ std::vector<NlLemma> checkMonomialInferResBounds();
/** check tangent planes
*
* ( ( x>2 ^ y>5) ^ (x<2 ^ y<5) ) => x*y > 5*x + 2*y - 10
* ( ( x>2 ^ y<5) ^ (x<2 ^ y>5) ) => x*y < 5*x + 2*y - 10
*/
- std::vector<Node> checkTangentPlanes();
+ std::vector<NlLemma> checkTangentPlanes();
//-------------------------------------------- end lemma schemas
private:
unsigned a_index,
int status,
std::vector<Node>& exp,
- std::vector<Node>& lem);
+ std::vector<NlLemma>& lem);
/** compare monomials a and b
*
* Initially, a call to this function is such that :
Node b,
NodeMultiset& b_exp_proc,
std::vector<Node>& exp,
- std::vector<Node>& lem,
+ std::vector<NlLemma>& lem,
std::map<int, std::map<Node, std::map<Node, Node> > >& cmp_infers);
/** helper function for above
*
NodeMultiset& b_exp_proc,
int status,
std::vector<Node>& exp,
- std::vector<Node>& lem,
+ std::vector<NlLemma>& lem,
std::map<int, std::map<Node, std::map<Node, Node> > >& cmp_infers);
/** Get factor skolem for n, add resulting lemmas to lemmas */
- Node getFactorSkolem(Node n, std::vector<Node>& lemmas);
+ Node getFactorSkolem(Node n, std::vector<NlLemma>& lemmas);
}; /* class NlSolver */
} // namespace nl
NonlinearExtension::NonlinearExtension(TheoryArith& containing,
eq::EqualityEngine* ee)
: d_lemmas(containing.getUserContext()),
+ d_lemmasPp(containing.getUserContext()),
d_containing(containing),
d_ee(ee),
d_needsLastCall(false),
return std::make_pair(true, Node::null());
}
-void NonlinearExtension::sendLemmas(const std::vector<Node>& out,
- bool preprocess,
- std::map<Node, NlLemmaSideEffect>& lemSE)
+void NonlinearExtension::sendLemmas(const std::vector<NlLemma>& out)
{
- std::map<Node, NlLemmaSideEffect>::iterator its;
- for (const Node& lem : out)
+ for (const NlLemma& nlem : out)
{
+ Node lem = nlem.d_lemma;
+ bool preprocess = nlem.d_preprocess;
Trace("nl-ext-lemma") << "NonlinearExtension::Lemma : " << lem << std::endl;
d_containing.getOutputChannel().lemma(lem, false, preprocess);
// process the side effect
- its = lemSE.find(lem);
- if (its != lemSE.end())
+ processSideEffect(nlem);
+ // add to cache if not preprocess
+ if (preprocess)
{
- processSideEffect(its->second);
+ d_lemmasPp.insert(lem);
}
- // add to cache if not preprocess
- if (!preprocess)
+ else
{
d_lemmas.insert(lem);
}
}
}
-void NonlinearExtension::processSideEffect(const NlLemmaSideEffect& se)
+void NonlinearExtension::processSideEffect(const NlLemma& se)
{
d_trSlv.processSideEffect(se);
}
-unsigned NonlinearExtension::filterLemma(Node lem, std::vector<Node>& out)
+unsigned NonlinearExtension::filterLemma(NlLemma lem, std::vector<NlLemma>& out)
{
Trace("nl-ext-lemma-debug")
- << "NonlinearExtension::Lemma pre-rewrite : " << lem << std::endl;
- lem = Rewriter::rewrite(lem);
- if (d_lemmas.find(lem) != d_lemmas.end()
- || std::find(out.begin(), out.end(), lem) != out.end())
+ << "NonlinearExtension::Lemma pre-rewrite : " << lem.d_lemma << std::endl;
+ lem.d_lemma = Rewriter::rewrite(lem.d_lemma);
+ // get the proper cache
+ NodeSet& lcache = lem.d_preprocess ? d_lemmasPp : d_lemmas;
+ if (lcache.find(lem.d_lemma) != lcache.end())
{
Trace("nl-ext-lemma-debug")
- << "NonlinearExtension::Lemma duplicate : " << lem << std::endl;
+ << "NonlinearExtension::Lemma duplicate : " << lem.d_lemma << std::endl;
return 0;
}
out.push_back(lem);
return 1;
}
-unsigned NonlinearExtension::filterLemmas(std::vector<Node>& lemmas,
- std::vector<Node>& out)
+unsigned NonlinearExtension::filterLemmas(std::vector<NlLemma>& lemmas,
+ std::vector<NlLemma>& out)
{
if (options::nlExtEntailConflicts())
{
// check if any are entailed to be false
- for (const Node& lem : lemmas)
+ for (const NlLemma& lem : lemmas)
{
- Node ch_lemma = lem.negate();
+ Node ch_lemma = lem.d_lemma.negate();
ch_lemma = Rewriter::rewrite(ch_lemma);
Trace("nl-ext-et-debug")
<< "Check entailment of " << ch_lemma << "..." << std::endl;
<< et.second << std::endl;
if (et.first)
{
- Trace("nl-ext-et") << "*** Lemma entailed to be in conflict : " << lem
- << std::endl;
+ Trace("nl-ext-et") << "*** Lemma entailed to be in conflict : "
+ << lem.d_lemma << std::endl;
// return just this lemma
if (filterLemma(lem, out) > 0)
{
}
unsigned sum = 0;
- for (const Node& lem : lemmas)
+ for (const NlLemma& lem : lemmas)
{
sum += filterLemma(lem, out);
}
bool NonlinearExtension::checkModel(const std::vector<Node>& assertions,
const std::vector<Node>& false_asserts,
- std::vector<Node>& lemmas,
+ std::vector<NlLemma>& lemmas,
std::vector<Node>& gs)
{
Trace("nl-ext-cm") << "--- check-model ---" << std::endl;
int NonlinearExtension::checkLastCall(const std::vector<Node>& assertions,
const std::vector<Node>& false_asserts,
const std::vector<Node>& xts,
- std::vector<Node>& lems,
- std::vector<Node>& lemsPp,
- std::vector<Node>& wlems,
- std::map<Node, NlLemmaSideEffect>& lemSE)
+ std::vector<NlLemma>& lems,
+ std::vector<NlLemma>& wlems)
{
// initialize the non-linear solver
d_nlSlv.initLastCall(assertions, false_asserts, xts);
// initialize the trancendental function solver
- std::vector<Node> lemmas;
- d_trSlv.initLastCall(assertions, false_asserts, xts, lemmas, lemsPp);
+ std::vector<NlLemma> lemmas;
+ d_trSlv.initLastCall(assertions, false_asserts, xts, lemmas);
// process lemmas that may have been generated by the transcendental solver
filterLemmas(lemmas, lems);
- if (!lems.empty() || !lemsPp.empty())
+ if (!lems.empty())
{
Trace("nl-ext") << " ...finished with " << lems.size()
<< " new lemmas during registration." << std::endl;
- return lems.size() + lemsPp.size();
+ return lems.size();
}
//----------------------------------- possibly split on zero
//-----------------------------------inferred bounds lemmas
// e.g. x >= t => y*x >= y*t
- std::vector<Node> nt_lemmas;
+ std::vector<NlLemma> nt_lemmas;
lemmas =
d_nlSlv.checkMonomialInferBounds(nt_lemmas, assertions, false_asserts);
// Trace("nl-ext") << "Bound lemmas : " << lemmas.size() << ", " <<
}
if (options::nlExtTfTangentPlanes())
{
- lemmas = d_trSlv.checkTranscendentalTangentPlanes(lemSE);
+ lemmas = d_trSlv.checkTranscendentalTangentPlanes();
filterLemmas(lemmas, wlems);
}
Trace("nl-ext") << " ...finished with " << wlems.size() << " waiting lemmas."
else
{
// If we computed lemmas during collectModelInfo, send them now.
- if (!d_cmiLemmas.empty() || !d_cmiLemmasPp.empty())
+ if (!d_cmiLemmas.empty())
{
- sendLemmas(d_cmiLemmas, false, d_cmiLemmasSE);
- sendLemmas(d_cmiLemmasPp, true, d_cmiLemmasSE);
+ sendLemmas(d_cmiLemmas);
return;
}
// Otherwise, we will answer SAT. The values that we approximated are
}
}
-bool NonlinearExtension::modelBasedRefinement(
- std::vector<Node>& mlems,
- std::vector<Node>& mlemsPp,
- std::map<Node, NlLemmaSideEffect>& lemSE)
+bool NonlinearExtension::modelBasedRefinement(std::vector<NlLemma>& mlems)
{
// get the assertions
std::vector<Node> assertions;
// 1 : we may answer SAT, -1 : we may not answer SAT, 0 : unknown
int complete_status = 1;
// lemmas that should be sent later
- std::vector<Node> wlems;
+ std::vector<NlLemma> wlems;
// We require a check either if an assertion is false or a shared term has
// a wrong value
if (!false_asserts.empty() || num_shared_wrong_value > 0)
{
complete_status = num_shared_wrong_value > 0 ? -1 : 0;
- checkLastCall(
- assertions, false_asserts, xts, mlems, mlemsPp, wlems, lemSE);
- if (!mlems.empty() || !mlemsPp.empty())
+ checkLastCall(assertions, false_asserts, xts, mlems, wlems);
+ if (!mlems.empty())
{
return true;
}
<< std::endl;
// check the model based on simple solving of equalities and using
// error bounds on the Taylor approximation of transcendental functions.
- std::vector<Node> lemmas;
+ std::vector<NlLemma> lemmas;
std::vector<Node> gs;
if (checkModel(assertions, false_asserts, lemmas, gs))
{
complete_status = -1;
if (!shared_term_value_splits.empty())
{
- std::vector<Node> stvLemmas;
+ std::vector<NlLemma> stvLemmas;
for (const Node& eq : shared_term_value_splits)
{
Node req = Rewriter::rewrite(eq);
d_model.reset(d_containing.getValuation().getModel(), arithModel);
// run a last call effort check
d_cmiLemmas.clear();
- d_cmiLemmasPp.clear();
- d_cmiLemmasSE.clear();
if (!d_builtModel.get())
{
Trace("nl-ext") << "interceptModel: do model-based refinement" << std::endl;
- modelBasedRefinement(d_cmiLemmas, d_cmiLemmasPp, d_cmiLemmasSE);
+ modelBasedRefinement(d_cmiLemmas);
}
if (d_builtModel.get())
{
* involve e.g. solving for variables in nonlinear equations.
*
* Notice that in the former case, the lemmas it constructs are not sent out
- * immediately. Instead, they are put in temporary vectors d_cmiLemmas
- * and d_cmiLemmasPp, which are then sent out (if necessary) when a last call
+ * immediately. Instead, they are put in temporary vector d_cmiLemmas, which
+ * are then sent out (if necessary) when a last call
* effort check is issued to this class.
*/
void interceptModel(std::map<Node, Node>& arithModel);
* described in Reynolds et al. FroCoS 2017 that are based on ruling out
* the current candidate model.
*
- * This function returns true if a lemma was added to the vector lems/lemsPp.
+ * This function returns true if a lemma was added to the vector lems.
* Otherwise, it returns false. In the latter case, the model object d_model
* may have information regarding how to construct a model, in the case that
* we determined the problem is satisfiable.
- *
- * The argument lemSE is the "side effect" of the lemmas in mlems and mlemsPp
- * (for details, see checkLastCall).
*/
- bool modelBasedRefinement(std::vector<Node>& mlems,
- std::vector<Node>& mlemsPp,
- std::map<Node, NlLemmaSideEffect>& lemSE);
+ bool modelBasedRefinement(std::vector<NlLemma>& mlems);
/** check last call
*
*
* xts : the list of (non-reduced) extended terms in the current context.
*
- * This method adds lemmas to arguments lems, lemsPp, and wlems, each of
+ * This method adds lemmas to arguments lems and wlems, each of
* which are intended to be sent out on the output channel of TheoryArith
* under certain conditions.
*
- * If the set lems or lemsPp is non-empty, then no further processing is
+ * If the set lems is non-empty, then no further processing is
* necessary. The last call effort check should terminate and these
- * lemmas should be sent. The set lemsPp is distinguished from lems since
- * the preprocess flag on the lemma(...) call should be set to true.
+ * lemmas should be sent.
*
* The "waiting" lemmas wlems contain lemmas that should be sent on the
* output channel as a last resort. In other words, only if we are not
* able to establish SAT via a call to checkModel(...) should wlems be
* considered. This set typically contains tangent plane lemmas.
- *
- * The argument lemSE is the "side effect" of the lemmas from the previous
- * three calls. If a lemma is mapping to a side effect, it should be
- * processed via a call to processSideEffect(...) immediately after the
- * lemma is sent (if it is indeed sent on this call to check).
*/
int checkLastCall(const std::vector<Node>& assertions,
const std::vector<Node>& false_asserts,
const std::vector<Node>& xts,
- std::vector<Node>& lems,
- std::vector<Node>& lemsPp,
- std::vector<Node>& wlems,
- std::map<Node, NlLemmaSideEffect>& lemSE);
+ std::vector<NlLemma>& lems,
+ std::vector<NlLemma>& wlems);
/** get assertions
*
*/
bool checkModel(const std::vector<Node>& assertions,
const std::vector<Node>& false_asserts,
- std::vector<Node>& lemmas,
+ std::vector<NlLemma>& lemmas,
std::vector<Node>& gs);
//---------------------------end check model
* the number of lemmas added to out. We do not add lemmas that have already
* been sent on the output channel of TheoryArith.
*/
- unsigned filterLemmas(std::vector<Node>& lemmas, std::vector<Node>& out);
+ unsigned filterLemmas(std::vector<NlLemma>& lemmas,
+ std::vector<NlLemma>& out);
/** singleton version of above */
- unsigned filterLemma(Node lem, std::vector<Node>& out);
+ unsigned filterLemma(NlLemma lem, std::vector<NlLemma>& out);
/**
* Send lemmas in out on the output channel of theory of arithmetic.
*/
- void sendLemmas(const std::vector<Node>& out,
- bool preprocess,
- std::map<Node, NlLemmaSideEffect>& lemSE);
+ void sendLemmas(const std::vector<NlLemma>& out);
/** Process side effect se */
- void processSideEffect(const NlLemmaSideEffect& se);
+ void processSideEffect(const NlLemma& se);
/** 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;
*/
NlSolver d_nlSlv;
/**
- * The lemmas we computed during collectModelInfo. We store two vectors of
- * lemmas to be sent out on the output channel of TheoryArith. The first
- * is not preprocessed, the second is.
+ * The lemmas we computed during collectModelInfo, to be sent out on the
+ * output channel of TheoryArith.
*/
- std::vector<Node> d_cmiLemmas;
- std::vector<Node> d_cmiLemmasPp;
- /** the side effects of the above lemmas */
- std::map<Node, NlLemmaSideEffect> d_cmiLemmasSE;
+ std::vector<NlLemma> d_cmiLemmas;
/**
* The approximations computed during collectModelInfo. For details, see
* NlModel::getModelValueRepair.
void TranscendentalSolver::initLastCall(const std::vector<Node>& assertions,
const std::vector<Node>& false_asserts,
const std::vector<Node>& xts,
- std::vector<Node>& lems,
- std::vector<Node>& lemsPp)
+ std::vector<NlLemma>& lems)
{
d_funcCongClass.clear();
d_funcMap.clear();
// note we must do preprocess on this lemma
Trace("nl-ext-lemma") << "NonlinearExtension::Lemma : purify : " << lem
<< std::endl;
- lemsPp.push_back(lem);
+ NlLemma nlem(lem);
+ nlem.d_preprocess = true;
+ lems.push_back(nlem);
}
if (Trace.isOn("nl-ext-mv"))
return d_taylor_degree;
}
-void TranscendentalSolver::processSideEffect(const NlLemmaSideEffect& se)
+void TranscendentalSolver::processSideEffect(const NlLemma& se)
{
for (const std::tuple<Node, unsigned, Node>& sp : se.d_secantPoint)
{
}
}
-void TranscendentalSolver::getCurrentPiBounds(std::vector<Node>& lemmas)
+void TranscendentalSolver::getCurrentPiBounds(std::vector<NlLemma>& lemmas)
{
NodeManager* nm = NodeManager::currentNM();
Node pi_lem = nm->mkNode(AND,
lemmas.push_back(pi_lem);
}
-std::vector<Node> TranscendentalSolver::checkTranscendentalInitialRefine()
+std::vector<NlLemma> TranscendentalSolver::checkTranscendentalInitialRefine()
{
NodeManager* nm = NodeManager::currentNM();
- std::vector<Node> lemmas;
+ std::vector<NlLemma> lemmas;
Trace("nl-ext")
<< "Get initial refinement lemmas for transcendental functions..."
<< std::endl;
return lemmas;
}
-std::vector<Node> TranscendentalSolver::checkTranscendentalMonotonic()
+std::vector<NlLemma> TranscendentalSolver::checkTranscendentalMonotonic()
{
- std::vector<Node> lemmas;
+ std::vector<NlLemma> lemmas;
Trace("nl-ext") << "Get monotonicity lemmas for transcendental functions..."
<< std::endl;
return lemmas;
}
-std::vector<Node> TranscendentalSolver::checkTranscendentalTangentPlanes(
- std::map<Node, NlLemmaSideEffect>& lemSE)
+std::vector<NlLemma> TranscendentalSolver::checkTranscendentalTangentPlanes()
{
- std::vector<Node> lemmas;
+ std::vector<NlLemma> lemmas;
Trace("nl-ext") << "Get tangent plane lemmas for transcendental functions..."
<< std::endl;
// this implements Figure 3 of "Satisfiaility Modulo Transcendental Functions
{
Trace("nl-ext-tftp") << "- run at degree " << d << "..." << std::endl;
unsigned prev = lemmas.size();
- if (checkTfTangentPlanesFun(tf, d, lemmas, lemSE))
+ if (checkTfTangentPlanesFun(tf, d, lemmas))
{
Trace("nl-ext-tftp")
<< "...fail, #lemmas = " << (lemmas.size() - prev) << std::endl;
return lemmas;
}
-bool TranscendentalSolver::checkTfTangentPlanesFun(
- Node tf,
- unsigned d,
- std::vector<Node>& lemmas,
- std::map<Node, NlLemmaSideEffect>& lemSE)
+bool TranscendentalSolver::checkTfTangentPlanesFun(Node tf,
+ unsigned d,
+ std::vector<NlLemma>& lemmas)
{
NodeManager* nm = NodeManager::currentNM();
Kind k = tf.getKind();
Assert(!lemmaConj.empty());
Node lem =
lemmaConj.size() == 1 ? lemmaConj[0] : nm->mkNode(AND, lemmaConj);
- lemmas.push_back(lem);
+ NlLemma nlem(lem);
// The side effect says that if lem is added, then we should add the
// secant point c for (tf,d).
- lemSE[lem].d_secantPoint.push_back(std::make_tuple(tf, d, c));
+ nlem.d_secantPoint.push_back(std::make_tuple(tf, d, c));
+ lemmas.push_back(nlem);
}
return true;
}
* model, and xts is the set of extended function terms that are active in
* the current context.
*
- * This call may add lemmas to lems/lemsPp based on registering term
+ * This call may add lemmas to lems based on registering term
* information (for example, purification of sine terms).
*/
void initLastCall(const std::vector<Node>& assertions,
const std::vector<Node>& false_asserts,
const std::vector<Node>& xts,
- std::vector<Node>& lems,
- std::vector<Node>& lemsPp);
+ std::vector<NlLemma>& lems);
/** increment taylor degree */
void incrementTaylorDegree();
/** get taylor degree */
* was conflicting.
*/
bool preprocessAssertionsCheckModel(std::vector<Node>& assertions);
- /** Process side effect se */
- void processSideEffect(const NlLemmaSideEffect& se);
+ /** Process side effects in lemma se */
+ void processSideEffect(const NlLemma& se);
//-------------------------------------------- lemma schemas
/** check transcendental initial refine
*
* exp( x )>0
* x<0 => exp( x )<1
*/
- std::vector<Node> checkTranscendentalInitialRefine();
+ std::vector<NlLemma> checkTranscendentalInitialRefine();
/** check transcendental monotonic
*
* PI/2 > x > y > 0 => sin( x ) > sin( y )
* PI > x > y > PI/2 => sin( x ) < sin( y )
*/
- std::vector<Node> checkTranscendentalMonotonic();
+ std::vector<NlLemma> checkTranscendentalMonotonic();
/** check transcendental tangent planes
*
* ( 1 < y < PI/2 ) => (sin y) >= c1*(y+c2)
* where c1, c2 are rationals (for brevity, omitted here)
* such that c1 ~= .277 and c2 ~= 2.032.
- *
- * The argument lemSE is the "side effect" of the lemmas in the return
- * value of this function (for details, see checkLastCall).
*/
- std::vector<Node> checkTranscendentalTangentPlanes(
- std::map<Node, NlLemmaSideEffect>& lemSE);
+ std::vector<NlLemma> checkTranscendentalTangentPlanes();
/** check transcendental function refinement for tf
*
* This method is called by the above method for each "master"
*
* This runs Figure 3 of Cimatti et al., CADE 2017 for transcendental
* function application tf for Taylor degree d. It may add a secant or
- * tangent plane lemma to lems and its side effect (if one exists)
- * to lemSE.
+ * tangent plane lemma to lems, which includes the side effect of the lemma
+ * (if one exists).
*
* It returns false if the bounds are not precise enough to add a
* secant or tangent plane lemma.
*/
- bool checkTfTangentPlanesFun(Node tf,
- unsigned d,
- std::vector<Node>& lems,
- std::map<Node, NlLemmaSideEffect>& lemSE);
+ bool checkTfTangentPlanesFun(Node tf, unsigned d, std::vector<NlLemma>& lems);
//-------------------------------------------- end lemma schemas
private:
/** polynomial approximation bounds
Node getDerivative(Node n, Node x);
void mkPi();
- void getCurrentPiBounds(std::vector<Node>& lemmas);
+ void getCurrentPiBounds(std::vector<NlLemma>& lemmas);
/** Make the node -pi <= a <= pi */
static Node mkValidPhase(Node a, Node pi);
projects / cvc5.git / commitdiff