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.

3 files changed, 134 insertions, 3 deletions

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<bool> 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<Node>& terms,
+                                          std::vector<bool>& 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<Node>& vars = d_qreg.d_vars[q];
+  Assert(tsize == vars.size());
+  std::map<TNode, TNode> 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<Node>& 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<Node>& terms,
+                               std::vector<bool>& 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