Improvements and refactoring for enumeratative strategy (#6030)

Refactoring out the code from  `inst_strategy_enumerative` into a separate
class. Some additional tricks to avoid duplicate instantiations, most
notably, before instantiation, a tuple is checked if it's not a
super-tuple of some tuple that had earlier resulted in a useless
instantiation.

Signed-off-by: mikolas <mikolas.janota@gmail.com>

1 files changed, 35 insertions, 171 deletions

diff --git a/src/theory/quantifiers/inst_strategy_enumerative.cpp b/src/theory/quantifiers/inst_strategy_enumerative.cpp
index 0f2fc0ba0..0595484fa 100644
--- a/src/theory/quantifiers/inst_strategy_enumerative.cpp
+++ b/src/theory/quantifiers/inst_strategy_enumerative.cpp
@@ -18,6 +18,7 @@
 #include "theory/quantifiers/instantiate.h"
 #include "theory/quantifiers/relevant_domain.h"
 #include "theory/quantifiers/term_database.h"
+#include "theory/quantifiers/term_tuple_enumerator.h"
 #include "theory/quantifiers/term_util.h"
 #include "theory/quantifiers_engine.h"
 
@@ -175,189 +176,52 @@ void InstStrategyEnum::check(Theory::Effort e, QEffort quant_e)
   }
 }
 
-bool InstStrategyEnum::process(Node f, bool fullEffort, bool isRd)
+bool InstStrategyEnum::process(Node quantifier, bool fullEffort, bool isRd)
 {
-  // ignore if constant true (rare case of non-standard quantifier whose body is
-  // rewritten to true)
-  if (f[1].isConst() && f[1].getConst<bool>())
+  // ignore if constant true (rare case of non-standard quantifier whose body
+  // is rewritten to true)
+  if (quantifier[1].isConst() && quantifier[1].getConst<bool>())
   {
     return false;
   }
-  unsigned final_max_i = 0;
-  std::vector<unsigned> maxs;
-  std::vector<bool> max_zero;
-  bool has_zero = false;
-  std::map<TypeNode, std::vector<Node> > term_db_list;
-  std::vector<TypeNode> ftypes;
-  TermDb* tdb = d_quantEngine->getTermDatabase();
-  QuantifiersState& qs = d_quantEngine->getState();
-  // iterate over substitutions for variables
-  for (unsigned i = 0; i < f[0].getNumChildren(); i++)
+
+  TermTupleEnumeratorContext ttec;
+  ttec.d_quantEngine = d_quantEngine;
+  ttec.d_rd = d_rd;
+  ttec.d_fullEffort = fullEffort;
+  ttec.d_increaseSum = options::fullSaturateSum();
+  ttec.d_isRd = isRd;
+  std::unique_ptr<TermTupleEnumeratorInterface> enumerator(
+      mkTermTupleEnumerator(quantifier, &ttec));
+  std::vector<Node> terms;
+  std::vector<bool> failMask;
+  Instantiate* ie = d_quantEngine->getInstantiate();
+  for (enumerator->init(); enumerator->hasNext();)
   {
-    TypeNode tn = f[0][i].getType();
-    ftypes.push_back(tn);
-    unsigned ts;
-    if (isRd)
-    {
-      ts = d_rd->getRDomain(f, i)->d_terms.size();
-    }
-    else
+    if (d_qstate.isInConflict())
     {
-      ts = tdb->getNumTypeGroundTerms(tn);
-      std::map<TypeNode, std::vector<Node> >::iterator ittd =
-          term_db_list.find(tn);
-      if (ittd == term_db_list.end())
-      {
-        std::map<Node, Node> reps_found;
-        for (unsigned j = 0; j < ts; j++)
-        {
-          Node gt = tdb->getTypeGroundTerm(ftypes[i], j);
-          if (!options::cegqi() || !quantifiers::TermUtil::hasInstConstAttr(gt))
-          {
-            Node rep = qs.getRepresentative(gt);
-            if (reps_found.find(rep) == reps_found.end())
-            {
-              reps_found[rep] = gt;
-              term_db_list[tn].push_back(gt);
-            }
-          }
-        }
-        ts = term_db_list[tn].size();
-      }
-      else
-      {
-        ts = ittd->second.size();
-      }
+      // could be conflicting for an internal reason
+      return false;
     }
-    // consider a default value if at full effort
-    max_zero.push_back(fullEffort && ts == 0);
-    ts = (fullEffort && ts == 0) ? 1 : ts;
-    Trace("inst-alg-rd") << "Variable " << i << " has " << ts
-                         << " in relevant domain." << std::endl;
-    if (ts == 0)
+    enumerator->next(terms);
+    // try instantiation
+    failMask.clear();
+    /* if (ie->addInstantiation(quantifier, terms)) */
+    if (ie->addInstantiationExpFail(quantifier, terms, failMask, false))
     {
-      has_zero = true;
-      break;
+      Trace("inst-alg-rd") << "Success!" << std::endl;
+      ++(d_quantEngine->d_statistics.d_instantiations_guess);
+      return true;
     }
-    maxs.push_back(ts);
-    if (ts > final_max_i)
+    else
     {
-      final_max_i = ts;
+      enumerator->failureReason(failMask);
     }
   }
-  if (!has_zero)
-  {
-    Trace("inst-alg-rd") << "Will do " << final_max_i
-                         << " stages of instantiation." << std::endl;
-    unsigned max_i = 0;
-    bool success;
-    Instantiate* ie = d_quantEngine->getInstantiate();
-    while (max_i <= final_max_i)
-    {
-      Trace("inst-alg-rd") << "Try stage " << max_i << "..." << std::endl;
-      std::vector<unsigned> childIndex;
-      int index = 0;
-      do
-      {
-        while (index >= 0 && index < (int)f[0].getNumChildren())
-        {
-          if (index == static_cast<int>(childIndex.size()))
-          {
-            childIndex.push_back(-1);
-          }
-          else
-          {
-            Assert(index == static_cast<int>(childIndex.size()) - 1);
-            unsigned nv = childIndex[index] + 1;
-            if (nv < maxs[index] && nv <= max_i)
-            {
-              childIndex[index] = nv;
-              index++;
-            }
-            else
-            {
-              childIndex.pop_back();
-              index--;
-            }
-          }
-        }
-        success = index >= 0;
-        if (success)
-        {
-          if (Trace.isOn("inst-alg-rd"))
-          {
-            Trace("inst-alg-rd") << "Try instantiation { ";
-            for (unsigned i : childIndex)
-            {
-              Trace("inst-alg-rd") << i << " ";
-            }
-            Trace("inst-alg-rd") << "}" << std::endl;
-          }
-          // try instantiation
-          std::vector<Node> terms;
-          for (unsigned i = 0, nchild = f[0].getNumChildren(); i < nchild; i++)
-          {
-            if (max_zero[i])
-            {
-              // no terms available, will report incomplete instantiation
-              terms.push_back(Node::null());
-              Trace("inst-alg-rd") << "  null" << std::endl;
-            }
-            else if (isRd)
-            {
-              terms.push_back(d_rd->getRDomain(f, i)->d_terms[childIndex[i]]);
-              Trace("inst-alg-rd")
-                  << "  (rd) " << d_rd->getRDomain(f, i)->d_terms[childIndex[i]]
-                  << std::endl;
-            }
-            else
-            {
-              Assert(childIndex[i] < term_db_list[ftypes[i]].size());
-              terms.push_back(term_db_list[ftypes[i]][childIndex[i]]);
-              Trace("inst-alg-rd")
-                  << "  " << term_db_list[ftypes[i]][childIndex[i]]
-                  << std::endl;
-            }
-            Assert(terms[i].isNull()
-                   || terms[i].getType().isComparableTo(ftypes[i]))
-                << "Incompatible type " << f << ", " << terms[i].getType()
-                << ", " << ftypes[i] << std::endl;
-          }
-          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);
-            return true;
-          }
-          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())
-          {
-            // could be conflicting for an internal reason (such as term
-            // indices computed in above calls)
-            return false;
-          }
-        }
-      } while (success);
-      max_i++;
-    }
-  }
-  // TODO : term enumerator instantiation?
   return false;
+  // TODO : term enumerator instantiation?
 }
 
-} /* CVC4::theory::quantifiers namespace */
-} /* CVC4::theory namespace */
-} /* CVC4 namespace */
+}  // namespace quantifiers
+}  // namespace theory
+}  // namespace CVC4