}
bool NonlinearExtension::checkModel(const std::vector<Node>& assertions,
- std::vector<NlLemma>& lemmas,
std::vector<Node>& gs)
{
Trace("nl-ext-cm") << "--- check-model ---" << std::endl;
Trace("nl-ext-cm") << "-----" << std::endl;
unsigned tdegree = d_trSlv.getTaylorDegree();
- bool ret =
- d_model.checkModel(passertions, tdegree, lemmas, gs);
+ std::vector<NlLemma> lemmas;
+ bool ret = d_model.checkModel(passertions, tdegree, lemmas, gs);
+ for (const auto& al: lemmas)
+ {
+ d_im.addPendingArithLemma(al);
+ }
return ret;
}
-int NonlinearExtension::checkLastCall(const std::vector<Node>& assertions,
- const std::vector<Node>& false_asserts,
- const std::vector<Node>& xts,
- std::vector<NlLemma>& lems,
- std::vector<NlLemma>& wlems)
+void NonlinearExtension::checkLastCall(const std::vector<Node>& assertions,
+ const std::vector<Node>& false_asserts,
+ const std::vector<Node>& xts)
{
- std::vector<NlLemma> lemmas;
-
++(d_stats.d_checkRuns);
if (Trace.isOn("nl-ext"))
Trace("nl-ext") << " ...finished with "
<< d_im.numPendingLemmas() + d_im.numSentLemmas()
<< " new lemmas from ICP." << std::endl;
- return d_im.numPendingLemmas() + d_im.numSentLemmas();
+ return;
}
Trace("nl-ext") << "Done with ICP" << std::endl;
}
// initialize the trancendental function solver
d_trSlv.initLastCall(assertions, false_asserts, xts);
}
- if (options::nlCad())
- {
- d_cadSlv.initLastCall(assertions);
- }
// init last call with IAND
d_iandSlv.initLastCall(assertions, false_asserts, xts);
- if (d_im.hasUsed() || !lems.empty())
+ if (d_im.hasUsed())
{
- unsigned count = lems.size() + d_im.numPendingLemmas() + d_im.numSentLemmas();
+ std::size_t count = d_im.numPendingLemmas() + d_im.numSentLemmas();
Trace("nl-ext") << " ...finished with " << count
<< " new lemmas during registration." << std::endl;
- return count;
+ return;
}
//----------------------------------- possibly split on zero
{
Trace("nl-ext") << " ...finished with " << d_im.numPendingLemmas() << " new lemmas."
<< std::endl;
- return d_im.numPendingLemmas();
+ return;
}
}
d_trSlv.checkTranscendentalInitialRefine();
if (d_im.hasUsed())
{
- unsigned count = lems.size() + d_im.numPendingLemmas() + d_im.numSentLemmas();
+ std::size_t count = d_im.numPendingLemmas() + d_im.numSentLemmas();
Trace("nl-ext") << " ...finished with " << count << " new lemmas."
<< std::endl;
- return count;
+ return;
}
}
//-----------------------------------initial lemmas for iand
{
Trace("nl-ext") << " ...finished with " << d_im.numPendingLemmas() << " new lemmas."
<< std::endl;
- return d_im.numPendingLemmas();
+ return;
}
// main calls to nlExt
{
Trace("nl-ext") << " ...finished with " << d_im.numPendingLemmas() << " new lemmas."
<< std::endl;
- return d_im.numPendingLemmas();
+ return;
}
//-----------------------------------monotonicity of transdental functions
d_trSlv.checkTranscendentalMonotonic();
if (d_im.hasUsed())
{
- unsigned count = lems.size() + d_im.numPendingLemmas() + d_im.numSentLemmas();
+ std::size_t count = d_im.numPendingLemmas() + d_im.numSentLemmas();
Trace("nl-ext") << " ...finished with " << count << " new lemmas."
<< std::endl;
- return count;
+ return;
}
//------------------------lemmas based on magnitude of non-zero monomials
{
Trace("nl-ext") << " ...finished with " << d_im.numPendingLemmas()
<< " new lemmas." << std::endl;
- return d_im.numPendingLemmas();
+ return;
}
}
d_nlSlv.checkMonomialInferBounds(assertions, false_asserts);
Trace("nl-ext") << "Bound lemmas : " << d_im.numPendingLemmas() << ", " << d_im.numWaitingLemmas() << std::endl;
// prioritize lemmas that do not introduce new monomials
-
if (options::nlExtTangentPlanes()
&& options::nlExtTangentPlanesInterleave())
{
{
Trace("nl-ext") << " ...finished with " << d_im.numPendingLemmas() << " new lemmas."
<< std::endl;
- return d_im.numPendingLemmas();
+ return;
}
// from inferred bound inferences : now do ones that introduce new terms
{
Trace("nl-ext") << " ...finished with " << d_im.numPendingLemmas()
<< " new (monomial-introducing) lemmas." << std::endl;
- return d_im.numPendingLemmas();
+ return;
}
//------------------------------------factoring lemmas
{
Trace("nl-ext") << " ...finished with " << d_im.numPendingLemmas()
<< " new lemmas." << std::endl;
- return d_im.numPendingLemmas();
+ return;
}
}
{
Trace("nl-ext") << " ...finished with " << d_im.numPendingLemmas()
<< " new lemmas." << std::endl;
- return d_im.numPendingLemmas();
+ return;
}
}
}
if (options::nlCad())
{
+ d_cadSlv.initLastCall(assertions);
d_cadSlv.checkFull();
if (!d_im.hasUsed())
{
else
{
// checkFull() only adds a single conflict
- return 1;
+ return;
}
}
// run the full refinement in the IAND solver
<< std::endl;
Trace("nl-ext") << " ...finished with " << d_im.numPendingLemmas() << " lemmas."
<< std::endl;
- return 0;
+ return;
}
void NonlinearExtension::check(Theory::Effort e)
else
{
// If we computed lemmas during collectModelInfo, send them now.
- if (!d_cmiLemmas.empty() || d_im.hasPendingLemma())
+ if (d_im.hasPendingLemma())
{
- sendLemmas(d_cmiLemmas);
d_im.doPendingFacts();
d_im.doPendingLemmas();
d_im.doPendingPhaseRequirements();
}
}
-bool NonlinearExtension::modelBasedRefinement(std::vector<NlLemma>& mlems)
+bool NonlinearExtension::modelBasedRefinement()
{
++(d_stats.d_mbrRuns);
d_checkCounter++;
// complete_status:
// 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<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, wlems);
- if (!mlems.empty() || d_im.hasSentLemma() || d_im.hasPendingLemma())
+ checkLastCall(assertions, false_asserts, xts);
+ if (d_im.hasSentLemma() || d_im.hasPendingLemma())
{
d_im.clearWaitingLemmas();
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<NlLemma> lemmas;
std::vector<Node> gs;
- if (checkModel(assertions, lemmas, gs))
+ if (checkModel(assertions, gs))
{
complete_status = 1;
}
d_containing.getOutputChannel().requirePhase(mgr, true);
d_builtModel = true;
}
- filterLemmas(lemmas, mlems);
- if (!mlems.empty() || d_im.hasPendingLemma())
+ if (d_im.hasUsed())
{
d_im.clearWaitingLemmas();
return true;
if (complete_status != 1)
{
// flush the waiting lemmas
- if (!wlems.empty() || d_im.hasWaitingLemma())
+ if (d_im.hasWaitingLemma())
{
- std::size_t count = wlems.size() + d_im.numWaitingLemmas();
- mlems.insert(mlems.end(), wlems.begin(), wlems.end());
+ std::size_t count = d_im.numWaitingLemmas();
d_im.flushWaitingLemmas();
Trace("nl-ext") << "...added " << count << " waiting lemmas."
<< std::endl;
complete_status = -1;
if (!shared_term_value_splits.empty())
{
- std::vector<NlLemma> stvLemmas;
for (const Node& eq : shared_term_value_splits)
{
Node req = Rewriter::rewrite(eq);
Trace("nl-ext-debug") << "Split on : " << literal << std::endl;
Node split = literal.orNode(literal.negate());
NlLemma nsplit(split, InferenceId::NL_SHARED_TERM_VALUE_SPLIT);
- filterLemma(nsplit, stvLemmas);
+ d_im.addPendingArithLemma(nsplit, true);
}
- if (!stvLemmas.empty())
+ if (d_im.hasWaitingLemma())
{
- mlems.insert(mlems.end(), stvLemmas.begin(), stvLemmas.end());
- Trace("nl-ext") << "...added " << stvLemmas.size()
+ d_im.flushWaitingLemmas();
+ Trace("nl-ext") << "...added " << d_im.numPendingLemmas()
<< " shared term value split lemmas." << std::endl;
return true;
}
Trace("nl-ext") << "NonlinearExtension::interceptModel begin" << std::endl;
d_model.reset(d_containing.getValuation().getModel(), arithModel);
// run a last call effort check
- d_cmiLemmas.clear();
if (!d_builtModel.get())
{
Trace("nl-ext") << "interceptModel: do model-based refinement" << std::endl;
- modelBasedRefinement(d_cmiLemmas);
+ modelBasedRefinement();
}
if (d_builtModel.get())
{
* constraints are satisfiable, it may "repair" the values in the argument
* arithModel so that it satisfies certain nonlinear constraints. This may
* 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 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);
/** Does this class need a call to check(...) at last call effort? */
* 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.
+ * This function returns true if a lemma was added to the inference manager.
* 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.
*/
- bool modelBasedRefinement(std::vector<NlLemma>& mlems);
+ bool modelBasedRefinement();
/** check last call
*
*
* xts : the list of (non-reduced) extended terms in the current context.
*
- * 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.
+ * This method adds lemmas to d_im directly.
*
* 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 "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.
*/
- int checkLastCall(const std::vector<Node>& assertions,
- const std::vector<Node>& false_asserts,
- const std::vector<Node>& xts,
- std::vector<NlLemma>& lems,
- std::vector<NlLemma>& wlems);
+ void checkLastCall(const std::vector<Node>& assertions,
+ const std::vector<Node>& false_asserts,
+ const std::vector<Node>& xts);
/** get assertions
*
* ensureLiteral respectively.
*/
bool checkModel(const std::vector<Node>& assertions,
- std::vector<NlLemma>& lemmas,
std::vector<Node>& gs);
//---------------------------end check model
/** compute relevant assertions */
* constraints involving integer and.
*/
IAndSolver d_iandSlv;
- /**
- * The lemmas we computed during collectModelInfo, to be sent out on the
- * output channel of TheoryArith.
- */
- std::vector<NlLemma> d_cmiLemmas;
/**
* The approximations computed during collectModelInfo. For details, see
* NlModel::getModelValueRepair.
projects / cvc5.git / commitdiff