return ret;
}
-int NonlinearExtension::flushLemma(Node lem) {
+void NonlinearExtension::sendLemmas(const std::vector<Node>& out,
+ bool preprocess)
+{
+ for (const Node& lem : out)
+ {
+ Trace("nl-ext-lemma") << "NonlinearExtension::Lemma : " << lem << std::endl;
+ d_containing.getOutputChannel().lemma(lem, false, preprocess);
+ // add to cache if not preprocess
+ if (!preprocess)
+ {
+ d_lemmas.insert(lem);
+ }
+ }
+}
+
+unsigned NonlinearExtension::filterLemma(Node lem, std::vector<Node>& out)
+{
Trace("nl-ext-lemma-debug")
<< "NonlinearExtension::Lemma pre-rewrite : " << lem << std::endl;
lem = Rewriter::rewrite(lem);
- if (Contains(d_lemmas, lem)) {
+ if (d_lemmas.find(lem) != d_lemmas.end()
+ || std::find(out.begin(), out.end(), lem) != out.end())
+ {
Trace("nl-ext-lemma-debug")
<< "NonlinearExtension::Lemma duplicate : " << lem << std::endl;
- // should not generate duplicates
- // Assert( false );
return 0;
}
- d_lemmas.insert(lem);
- Trace("nl-ext-lemma") << "NonlinearExtension::Lemma : " << lem << std::endl;
- d_containing.getOutputChannel().lemma(lem);
+ out.push_back(lem);
return 1;
}
-int NonlinearExtension::flushLemmas(std::vector<Node>& lemmas) {
- if (options::nlExtEntailConflicts()) {
+unsigned NonlinearExtension::filterLemmas(std::vector<Node>& lemmas,
+ std::vector<Node>& out)
+{
+ if (options::nlExtEntailConflicts())
+ {
// check if any are entailed to be false
- for (unsigned i = 0; i < lemmas.size(); i++) {
- Node ch_lemma = lemmas[i].negate();
+ for (const Node& lem : lemmas)
+ {
+ Node ch_lemma = lem.negate();
ch_lemma = Rewriter::rewrite(ch_lemma);
Trace("nl-ext-et-debug")
<< "Check entailment of " << ch_lemma << "..." << std::endl;
THEORY_OF_TYPE_BASED, ch_lemma);
Trace("nl-ext-et-debug") << "entailment test result : " << et.first << " "
<< et.second << std::endl;
- if (et.first) {
- Trace("nl-ext-et") << "*** Lemma entailed to be in conflict : "
- << lemmas[i] << std::endl;
+ if (et.first)
+ {
+ Trace("nl-ext-et") << "*** Lemma entailed to be in conflict : " << lem
+ << std::endl;
// return just this lemma
- if (flushLemma(lemmas[i])) {
+ if (filterLemma(lem, out) > 0)
+ {
lemmas.clear();
return 1;
}
}
}
- int sum = 0;
- for (unsigned i = 0; i < lemmas.size(); i++) {
- sum += flushLemma(lemmas[i]);
+ unsigned sum = 0;
+ for (const Node& lem : lemmas)
+ {
+ sum += filterLemma(lem, out);
}
lemmas.clear();
return sum;
}
bool NonlinearExtension::checkModel(const std::vector<Node>& assertions,
- const std::vector<Node>& false_asserts)
+ const std::vector<Node>& false_asserts,
+ std::vector<Node>& lemmas,
+ std::vector<Node>& gs)
{
Trace("nl-ext-cm") << "--- check-model ---" << std::endl;
}
}
}
- std::vector<Node> lemmas;
- std::vector<Node> gs;
bool ret = d_model.checkModel(
passertions, false_asserts, d_taylor_degree, lemmas, gs);
- for (Node& mg : gs)
- {
- mg = Rewriter::rewrite(mg);
- mg = d_containing.getValuation().ensureLiteral(mg);
- d_containing.getOutputChannel().requirePhase(mg, true);
- d_builtModel = true;
- }
- for (Node& lem : lemmas)
- {
- Trace("nl-ext-lemma-model")
- << "Lemma from check model : " << lem << std::endl;
- d_containing.getOutputChannel().lemma(lem);
- }
return ret;
}
int NonlinearExtension::checkLastCall(const std::vector<Node>& assertions,
const std::vector<Node>& false_asserts,
- const std::vector<Node>& xts)
+ const std::vector<Node>& xts,
+ std::vector<Node>& lems,
+ std::vector<Node>& lemsPp,
+ std::vector<Node>& wlems)
{
d_ms_vars.clear();
d_ms_proc.clear();
d_ci_max.clear();
d_f_map.clear();
d_tf_region.clear();
- d_waiting_lemmas.clear();
- int lemmas_proc = 0;
std::vector<Node> lemmas;
NodeManager* nm = NodeManager::currentNM();
getCurrentPiBounds(lemmas);
}
- lemmas_proc = flushLemmas(lemmas);
- if (lemmas_proc > 0) {
- Trace("nl-ext") << " ...finished with " << lemmas_proc << " new lemmas during registration." << std::endl;
- return lemmas_proc;
+ filterLemmas(lemmas, lems);
+ if (!lems.empty())
+ {
+ Trace("nl-ext") << " ...finished with " << lems.size()
+ << " new lemmas during registration." << std::endl;
+ return lems.size();
}
// process SINE phase shifting
// must do preprocess on this one
Trace("nl-ext-lemma")
<< "NonlinearExtension::Lemma : purify : " << lem << std::endl;
- d_containing.getOutputChannel().lemma(lem, false, true);
- lemmas_proc++;
+ lemsPp.push_back(lem);
}
}
- if (lemmas_proc > 0)
+ if (!lemsPp.empty())
{
- Trace("nl-ext") << " ...finished with " << lemmas_proc
+ Trace("nl-ext") << " ...finished with " << lemsPp.size()
<< " new lemmas SINE phase shifting." << std::endl;
- return lemmas_proc;
+ return lemsPp.size();
}
Trace("nl-ext") << "We have " << d_ms.size() << " monomials." << std::endl;
if (options::nlExtSplitZero()) {
Trace("nl-ext") << "Get zero split lemmas..." << std::endl;
lemmas = checkSplitZero();
- lemmas_proc = flushLemmas(lemmas);
- if (lemmas_proc > 0) {
- Trace("nl-ext") << " ...finished with " << lemmas_proc << " new lemmas." << std::endl;
- return lemmas_proc;
+ filterLemmas(lemmas, lems);
+ if (!lems.empty())
+ {
+ Trace("nl-ext") << " ...finished with " << lems.size() << " new lemmas."
+ << std::endl;
+ return lems.size();
}
}
//-----------------------------------initial lemmas for transcendental functions
lemmas = checkTranscendentalInitialRefine();
- lemmas_proc = flushLemmas(lemmas);
- if (lemmas_proc > 0) {
- Trace("nl-ext") << " ...finished with " << lemmas_proc << " new lemmas." << std::endl;
- return lemmas_proc;
+ filterLemmas(lemmas, lems);
+ if (!lems.empty())
+ {
+ Trace("nl-ext") << " ...finished with " << lems.size() << " new lemmas."
+ << std::endl;
+ return lems.size();
}
-
+
//-----------------------------------lemmas based on sign (comparison to zero)
lemmas = checkMonomialSign();
- lemmas_proc = flushLemmas(lemmas);
- if (lemmas_proc > 0) {
- Trace("nl-ext") << " ...finished with " << lemmas_proc << " new lemmas." << std::endl;
- return lemmas_proc;
+ filterLemmas(lemmas, lems);
+ if (!lems.empty())
+ {
+ Trace("nl-ext") << " ...finished with " << lems.size() << " new lemmas."
+ << std::endl;
+ return lems.size();
}
-
+
//-----------------------------------monotonicity of transdental functions
lemmas = checkTranscendentalMonotonic();
- lemmas_proc = flushLemmas(lemmas);
- if (lemmas_proc > 0) {
- Trace("nl-ext") << " ...finished with " << lemmas_proc << " new lemmas." << std::endl;
- return lemmas_proc;
+ filterLemmas(lemmas, lems);
+ if (!lems.empty())
+ {
+ Trace("nl-ext") << " ...finished with " << lems.size() << " new lemmas."
+ << std::endl;
+ return lems.size();
}
//-----------------------------------lemmas based on magnitude of non-zero monomials
// c is effort level
lemmas = checkMonomialMagnitude( c );
unsigned nlem = lemmas.size();
- lemmas_proc = flushLemmas(lemmas);
- if (lemmas_proc > 0) {
- Trace("nl-ext") << " ...finished with " << lemmas_proc
+ filterLemmas(lemmas, lems);
+ if (!lems.empty())
+ {
+ Trace("nl-ext") << " ...finished with " << lems.size()
<< " new lemmas (out of possible " << nlem << ")."
<< std::endl;
- return lemmas_proc;
+ return lems.size();
}
}
// Trace("nl-ext") << "Bound lemmas : " << lemmas.size() << ", " <<
// nt_lemmas.size() << std::endl; prioritize lemmas that do not
// introduce new monomials
- lemmas_proc = flushLemmas(lemmas);
+ filterLemmas(lemmas, lems);
if (options::nlExtTangentPlanes() && options::nlExtTangentPlanesInterleave())
{
lemmas = checkTangentPlanes();
- lemmas_proc += flushLemmas(lemmas);
+ filterLemmas(lemmas, lems);
}
- if (lemmas_proc > 0) {
- Trace("nl-ext") << " ...finished with " << lemmas_proc << " new lemmas."
+ if (!lems.empty())
+ {
+ Trace("nl-ext") << " ...finished with " << lems.size() << " new lemmas."
<< std::endl;
- return lemmas_proc;
+ return lems.size();
}
-
+
// from inferred bound inferences : now do ones that introduce new terms
- lemmas_proc = flushLemmas(nt_lemmas);
- if (lemmas_proc > 0) {
- Trace("nl-ext") << " ...finished with " << lemmas_proc
+ filterLemmas(nt_lemmas, lems);
+ if (!lems.empty())
+ {
+ Trace("nl-ext") << " ...finished with " << lems.size()
<< " new (monomial-introducing) lemmas." << std::endl;
- return lemmas_proc;
+ return lems.size();
}
-
+
//------------------------------------factoring lemmas
// x*y + x*z >= t => exists k. k = y + z ^ x*k >= t
if( options::nlExtFactor() ){
lemmas = checkFactoring(assertions, false_asserts);
- lemmas_proc = flushLemmas(lemmas);
- if (lemmas_proc > 0) {
- Trace("nl-ext") << " ...finished with " << lemmas_proc << " new lemmas." << std::endl;
- return lemmas_proc;
+ filterLemmas(lemmas, lems);
+ if (!lems.empty())
+ {
+ Trace("nl-ext") << " ...finished with " << lems.size() << " new lemmas."
+ << std::endl;
+ return lems.size();
}
}
// e.g. ( y>=0 ^ s <= x*z ^ x*y <= t ) => y*s <= z*t
if (options::nlExtResBound()) {
lemmas = checkMonomialInferResBounds();
- lemmas_proc = flushLemmas(lemmas);
- if (lemmas_proc > 0) {
- Trace("nl-ext") << " ...finished with " << lemmas_proc << " new lemmas." << std::endl;
- return lemmas_proc;
+ filterLemmas(lemmas, lems);
+ if (!lems.empty())
+ {
+ Trace("nl-ext") << " ...finished with " << lems.size() << " new lemmas."
+ << std::endl;
+ return lems.size();
}
}
if (options::nlExtTangentPlanes() && !options::nlExtTangentPlanesInterleave())
{
lemmas = checkTangentPlanes();
- d_waiting_lemmas.insert(
- d_waiting_lemmas.end(), lemmas.begin(), lemmas.end());
- lemmas.clear();
+ filterLemmas(lemmas, wlems);
}
if (options::nlExtTfTangentPlanes())
{
lemmas = checkTranscendentalTangentPlanes();
- d_waiting_lemmas.insert(
- d_waiting_lemmas.end(), lemmas.begin(), lemmas.end());
- lemmas.clear();
+ filterLemmas(lemmas, wlems);
}
- Trace("nl-ext") << " ...finished with " << d_waiting_lemmas.size()
- << " waiting lemmas." << std::endl;
+ Trace("nl-ext") << " ...finished with " << wlems.size() << " waiting lemmas."
+ << std::endl;
return 0;
}
TheoryModel* tm = d_containing.getValuation().getModel();
if (!d_builtModel.get())
{
- // run model-based refinement
- if (modelBasedRefinement())
+ // run a last call effort check
+ std::vector<Node> mlems;
+ std::vector<Node> mlemsPp;
+ if (modelBasedRefinement(mlems, mlemsPp))
{
+ sendLemmas(mlems);
+ sendLemmas(mlemsPp, true);
return;
}
}
}
}
-bool NonlinearExtension::modelBasedRefinement()
+bool NonlinearExtension::modelBasedRefinement(std::vector<Node>& mlems,
+ std::vector<Node>& mlemsPp)
{
// reset the model object
d_model.reset(d_containing.getValuation().getModel());
// complete_status:
// 1 : we may answer SAT, -1 : we may not answer SAT, 0 : unknown
int complete_status = 1;
- int num_added_lemmas = 0;
- // we require a check either if an assertion is false or a shared term has
+ // lemmas that should be sent later
+ std::vector<Node> 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;
- num_added_lemmas = checkLastCall(assertions, false_asserts, xts);
- if (num_added_lemmas > 0)
+ checkLastCall(assertions, false_asserts, xts, mlems, mlemsPp, wlems);
+ if (!mlems.empty() || !mlemsPp.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.
- if (checkModel(assertions, false_asserts))
+ std::vector<Node> lemmas;
+ std::vector<Node> gs;
+ if (checkModel(assertions, false_asserts, lemmas, gs))
{
complete_status = 1;
}
+ for (const Node& mg : gs)
+ {
+ Node mgr = Rewriter::rewrite(mg);
+ mgr = d_containing.getValuation().ensureLiteral(mgr);
+ d_containing.getOutputChannel().requirePhase(mgr, true);
+ d_builtModel = true;
+ }
+ filterLemmas(lemmas, mlems);
+ if (!mlems.empty())
+ {
+ return true;
+ }
}
// if we have not concluded SAT
if (complete_status != 1)
{
// flush the waiting lemmas
- num_added_lemmas = flushLemmas(d_waiting_lemmas);
- if (num_added_lemmas > 0)
+ if (!wlems.empty())
{
- Trace("nl-ext") << "...added " << num_added_lemmas << " waiting lemmas."
+ mlems.insert(mlems.end(), wlems.begin(), wlems.end());
+ Trace("nl-ext") << "...added " << wlems.size() << " waiting lemmas."
<< std::endl;
return true;
}
complete_status = -1;
if (!shared_term_value_splits.empty())
{
- std::vector<Node> shared_term_value_lemmas;
+ std::vector<Node> stvLemmas;
for (const Node& eq : shared_term_value_splits)
{
Node req = Rewriter::rewrite(eq);
Node literal = d_containing.getValuation().ensureLiteral(req);
d_containing.getOutputChannel().requirePhase(literal, true);
Trace("nl-ext-debug") << "Split on : " << literal << std::endl;
- shared_term_value_lemmas.push_back(
- literal.orNode(literal.negate()));
+ Node split = literal.orNode(literal.negate());
+ filterLemma(split, stvLemmas);
}
- num_added_lemmas = flushLemmas(shared_term_value_lemmas);
- if (num_added_lemmas > 0)
+ if (!stvLemmas.empty())
{
- Trace("nl-ext") << "...added " << num_added_lemmas
+ mlems.insert(mlems.end(), stvLemmas.begin(), stvLemmas.end());
+ Trace("nl-ext") << "...added " << stvLemmas.size()
<< " shared term value split lemmas." << std::endl;
return true;
}
* 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 sent out on the output
- * channel of the theory of arithmetic. 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.
+ * This function returns true if a lemma was added to the vector lems/lemsPp.
+ * 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();
+ bool modelBasedRefinement(std::vector<Node>& mlems,
+ std::vector<Node>& mlemsPp);
/** returns true if the multiset containing the
* factors of monomial a is a subset of the multiset
* containing the factors of monomial b.
*
* xts : the list of (non-reduced) extended terms in the current context.
*
- * This method returns the number of lemmas added on the output channel of
- * TheoryArith.
+ * This method adds lemmas to arguments lems, lemsPp, 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
+ * 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.
+ *
+ * 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);
+ const std::vector<Node>& xts,
+ std::vector<Node>& lems,
+ std::vector<Node>& lemsPp,
+ std::vector<Node>& wlems);
//---------------------------------------term utilities
static bool isArithKind(Kind k);
static Node mkLit(Node a, Node b, int status, bool isAbsolute = false);
*
* For details, see Section 3 of Cimatti et al CADE 2017 under the heading
* "Detecting Satisfiable Formulas".
+ *
+ * The arguments lemmas and gs store the lemmas and guard literals to be sent
+ * out on the output channel of TheoryArith as lemmas and calls to
+ * ensureLiteral respectively.
*/
bool checkModel(const std::vector<Node>& assertions,
- const std::vector<Node>& false_asserts);
+ const std::vector<Node>& false_asserts,
+ std::vector<Node>& lemmas,
+ std::vector<Node>& gs);
//---------------------------end check model
/** In the following functions, status states a relationship
/** Is n entailed with polarity pol in the current context? */
bool isEntailed(Node n, bool pol);
- /** flush lemmas
- *
- * Potentially sends lem on the output channel if lem has not been sent on the
- * output channel in this context. Returns the number of lemmas sent on the
- * output channel of TheoryArith.
+ /**
+ * Potentially adds lemmas to the set out and clears lemmas. Returns
+ * the number of lemmas added to out. We do not add lemmas that have already
+ * been sent on the output channel of TheoryArith.
*/
- int flushLemma(Node lem);
+ unsigned filterLemmas(std::vector<Node>& lemmas, std::vector<Node>& out);
+ /** singleton version of above */
+ unsigned filterLemma(Node lem, std::vector<Node>& out);
- /** Potentially sends lemmas to the output channel and clears lemmas. Returns
- * the number of lemmas sent to the output channel.
+ /**
+ * Send lemmas in out on the output channel of theory of arithmetic.
*/
- int flushLemmas(std::vector<Node>& lemmas);
+ void sendLemmas(const std::vector<Node>& out, bool preprocess = false);
// Returns the NodeMultiset for an existing monomial.
const NodeMultiset& getMonomialExponentMap(Node monomial) const;
/** Stores skolems in the range of the above map */
std::map<Node, bool> d_tr_is_base;
std::map< Node, bool > d_tf_initial_refine;
- /** the list of lemmas we are waiting to flush until after check model */
- std::vector<Node> d_waiting_lemmas;
void mkPi();
void getCurrentPiBounds( std::vector< Node >& lemmas );
projects / cvc5.git / commitdiff