From: Andrew Reynolds Date: Tue, 23 Feb 2021 03:53:45 +0000 (-0600) Subject: Explanation of failure for instantiate, use in enumerative instantiation (#5951) X-Git-Tag: cvc5-1.0.0~2240 X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=4711be9f5f65d5ea61321bc80d31e030536de81b;p=cvc5.git Explanation of failure for instantiate, use in enumerative instantiation (#5951) This makes enumerative instantiation generalize the failures in Instantiate::addInstantiate and increment its enumeration accordingly. This leads to (+104-6) using enumerative instantiation only on SMT-LIB quantified benchmarks, 60 second timeout. This is in preparation for further improvements to enumerative instantiation. --- diff --git a/src/theory/quantifiers/inst_strategy_enumerative.cpp b/src/theory/quantifiers/inst_strategy_enumerative.cpp index d448699af..dae1c21c7 100644 --- a/src/theory/quantifiers/inst_strategy_enumerative.cpp +++ b/src/theory/quantifiers/inst_strategy_enumerative.cpp @@ -323,7 +323,8 @@ bool InstStrategyEnum::process(Node f, bool fullEffort, bool isRd) << "Incompatible type " << f << ", " << terms[i].getType() << ", " << ftypes[i] << std::endl; } - if (ie->addInstantiation(f, terms)) + std::vector failMask; + if (ie->addInstantiationExpFail(f, terms, failMask, false)) { Trace("inst-alg-rd") << "Success!" << std::endl; ++(d_quantEngine->d_statistics.d_instantiations_guess); @@ -332,6 +333,15 @@ bool InstStrategyEnum::process(Node f, bool fullEffort, bool isRd) else { index--; + // currently, we use the failmask only for backtracking, although + // more could be learned here (wishue #81). + Assert(failMask.size() == terms.size()); + while (!failMask.empty() && !failMask.back()) + { + failMask.pop_back(); + childIndex.pop_back(); + index--; + } } if (d_qstate.isInConflict()) { diff --git a/src/theory/quantifiers/instantiate.cpp b/src/theory/quantifiers/instantiate.cpp index cc7f24a12..2eb99a774 100644 --- a/src/theory/quantifiers/instantiate.cpp +++ b/src/theory/quantifiers/instantiate.cpp @@ -379,6 +379,97 @@ bool Instantiate::addInstantiation( return true; } +bool Instantiate::addInstantiationExpFail(Node q, + std::vector& terms, + std::vector& failMask, + bool mkRep, + bool modEq, + bool doVts, + bool expFull) +{ + if (addInstantiation(q, terms, mkRep, modEq, doVts)) + { + return true; + } + size_t tsize = terms.size(); + failMask.resize(tsize, true); + if (tsize == 1) + { + // will never succeed with 1 variable + return false; + } + Trace("inst-exp-fail") << "Explain inst failure..." << terms << std::endl; + // set up information for below + std::vector& vars = d_qreg.d_vars[q]; + Assert(tsize == vars.size()); + std::map subs; + for (size_t i = 0; i < tsize; i++) + { + subs[vars[i]] = terms[i]; + } + // get the instantiation body + Node ibody = getInstantiation(q, vars, terms, doVts); + ibody = Rewriter::rewrite(ibody); + for (size_t i = 0; i < tsize; i++) + { + // process consecutively in reverse order, which is important since we use + // the fail mask for incrementing in a lexicographic order + size_t ii = (tsize - 1) - i; + // replace with the identity substitution + Node prev = terms[ii]; + terms[ii] = vars[ii]; + subs.erase(vars[ii]); + if (subs.empty()) + { + // will never succeed with empty substitution + break; + } + Trace("inst-exp-fail") << "- revert " << ii << std::endl; + // check whether we are still redundant + bool success = false; + // check entailment, only if option is set + if (options::instNoEntail()) + { + Trace("inst-exp-fail") << " check entailment" << std::endl; + success = d_term_db->isEntailed(q[1], subs, false, true); + Trace("inst-exp-fail") << " entailed: " << success << std::endl; + } + // check whether the instantiation rewrites to the same thing + if (!success) + { + Node ibodyc = getInstantiation(q, vars, terms, doVts); + ibodyc = Rewriter::rewrite(ibodyc); + success = (ibodyc == ibody); + Trace("inst-exp-fail") << " rewrite invariant: " << success << std::endl; + } + if (success) + { + // if we still fail, we are not critical + failMask[ii] = false; + } + else + { + subs[vars[ii]] = prev; + terms[ii] = prev; + // not necessary to proceed if expFull is false + if (!expFull) + { + break; + } + } + } + if (Trace.isOn("inst-exp-fail")) + { + Trace("inst-exp-fail") << "Fail mask: "; + for (bool b : failMask) + { + Trace("inst-exp-fail") << (b ? 1 : 0); + } + Trace("inst-exp-fail") << std::endl; + } + return false; +} + bool Instantiate::recordInstantiation(Node q, std::vector& terms, bool modEq, @@ -418,12 +509,12 @@ Node Instantiate::getInstantiation(Node q, bool doVts, LazyCDProof* pf) { - Node body; Assert(vars.size() == terms.size()); Assert(q[0].getNumChildren() == vars.size()); // Notice that this could be optimized, but no significant performance // improvements were observed with alternative implementations (see #1386). - body = q[1].substitute(vars.begin(), vars.end(), terms.begin(), terms.end()); + Node body = + q[1].substitute(vars.begin(), vars.end(), terms.begin(), terms.end()); // store the proof of the instantiated body, with (open) assumption q if (pf != nullptr) diff --git a/src/theory/quantifiers/instantiate.h b/src/theory/quantifiers/instantiate.h index c9911785f..a0b776819 100644 --- a/src/theory/quantifiers/instantiate.h +++ b/src/theory/quantifiers/instantiate.h @@ -146,6 +146,36 @@ class Instantiate : public QuantifiersUtil bool mkRep = false, bool modEq = false, bool doVts = false); + /** + * Same as above, but we also compute a vector failMask indicating which + * values in terms led to the instantiation not being added when this method + * returns false. For example, if q is the formula + * forall xy. x>5 => P(x,y) + * If terms = { 4, 0 }, then this method will return false since + * 4>5 => P(4,0) + * is entailed true based on rewriting. This method may additionally set + * failMask to "10", indicating that x's value was critical, but y's value + * was not. In other words, all instantiations including { x -> 4 } will also + * lead to this method returning false. + * + * The bits of failMask are computed in a greedy fashion, in reverse order. + * That is, we check whether each variable is critical one at a time, starting + * from the end. + * + * The parameter expFull is whether try to set all bits of the fail mask to + * 0. If this argument is true, then we only try to set a suffix of the + * bits in failMask to false. The motivation for expFull=false is for callers + * of this method that are enumerating tuples in lexiocographic order. The + * number of false bits in the suffix of failMask tells the caller how many + * "decimal" places to increment their iterator. + */ + bool addInstantiationExpFail(Node q, + std::vector& terms, + std::vector& failMask, + bool mkRep = false, + bool modEq = false, + bool doVts = false, + bool expFull = true); /** record instantiation * * Explicitly record that q has been instantiated with terms. This is the