SyGuS instantiation modes (#5228)

This PR adds three instantiation modes to the SyGuS instantiation module.

4 files changed, 78 insertions, 26 deletions

diff --git a/src/expr/node.h b/src/expr/node.h
index 7ae56d313..bb014bbaf 100644
--- a/src/expr/node.h
+++ b/src/expr/node.h
@@ -1417,7 +1417,7 @@ NodeTemplate<ref_count>::substitute(Iterator1 nodesBegin,
   Assert(std::distance(nodesBegin, nodesEnd)
          == std::distance(replacementsBegin, replacementsEnd))
       << "Substitution iterator ranges must be equal size";
-  Iterator1 j = find(nodesBegin, nodesEnd, TNode(*this));
+  Iterator1 j = std::find(nodesBegin, nodesEnd, TNode(*this));
   if(j != nodesEnd) {
     Iterator2 b = replacementsBegin;
     std::advance(b, std::distance(nodesBegin, j));
diff --git a/src/options/quantifiers_options.toml b/src/options/quantifiers_options.toml
index 2a5faf9f7..d29052042 100644
--- a/src/options/quantifiers_options.toml
+++ b/src/options/quantifiers_options.toml
@@ -2023,3 +2023,21 @@ header = "options/quantifiers_options.h"
 [[option.mode.BOTH]]
   name = "both"
   help = "combines minimal and maximal ."
+
+[[option]]
+  name       = "sygusInstMode"
+  category   = "regular"
+  long       = "sygus-inst-mode=MODE"
+  type       = "SygusInstMode"
+  default    = "PRIORITY_INST"
+  help       = "select instantiation lemma mode"
+  help_mode  = "SyGuS instantiation lemma modes."
+[[option.mode.PRIORITY_INST]]
+  name = "priority-inst"
+  help = "add instantiation lemmas first, add evaluation unfolding if instantiation fails."
+[[option.mode.PRIORITY_EVAL]]
+  name = "priority-eval"
+  help = "add evaluation unfolding lemma first, add instantiation lemma if unfolding lemmas already added."
+[[option.mode.INTERLEAVE]]
+  name = "interleave"
+  help = "add instantiation and evaluation unfolding lemmas in the same step."
diff --git a/src/theory/quantifiers/sygus_inst.cpp b/src/theory/quantifiers/sygus_inst.cpp
index e2aeee1b6..119cd925c 100644
--- a/src/theory/quantifiers/sygus_inst.cpp
+++ b/src/theory/quantifiers/sygus_inst.cpp
@@ -182,7 +182,6 @@ void addSpecialValues(
 
 SygusInst::SygusInst(QuantifiersEngine* qe)
     : QuantifiersModule(qe),
-      d_lemma_cache(qe->getUserContext()),
       d_ce_lemma_added(qe->getUserContext()),
       d_global_terms(qe->getUserContext()),
       d_notified_assertions(qe->getUserContext())
@@ -245,14 +244,20 @@ void SygusInst::check(Theory::Effort e, QEffort quant_e)
   TermDbSygus* db = d_quantEngine->getTermDatabaseSygus();
   SygusExplain syexplain(db);
   NodeManager* nm = NodeManager::currentNM();
+  options::SygusInstMode mode = options::sygusInstMode();
 
   for (const Node& q : d_active_quant)
   {
-    std::vector<Node> terms;
-    for (const Node& var : q[0])
+    const std::vector<Node>& inst_constants = d_inst_constants.at(q);
+    const std::vector<Node>& dt_evals = d_var_eval.at(q);
+    Assert(inst_constants.size() == dt_evals.size());
+    Assert(inst_constants.size() == q[0].getNumChildren());
+
+    std::vector<Node> terms, eval_unfold_lemmas;
+    for (size_t i = 0, size = q[0].getNumChildren(); i < size; ++i)
     {
-      Node dt_var = d_inst_constants[var];
-      Node dt_eval = d_var_eval[var];
+      Node dt_var = inst_constants[i];
+      Node dt_eval = dt_evals[i];
       Node value = model->getValue(dt_var);
       Node t = datatypes::utils::sygusToBuiltin(value);
       terms.push_back(t);
@@ -270,22 +275,43 @@ void SygusInst::check(Theory::Effort e, QEffort quant_e)
                          exp.size() == 1 ? exp[0] : nm->mkNode(kind::AND, exp),
                          dt_eval.eqNode(t));
       }
+      eval_unfold_lemmas.push_back(lem);
+    }
 
-      if (d_lemma_cache.find(lem) == d_lemma_cache.end())
+    if (mode == options::SygusInstMode::PRIORITY_INST)
+    {
+      if (!inst->addInstantiation(q, terms))
       {
-        Trace("sygus-inst") << "Evaluation unfolding: " << lem << std::endl;
-        d_quantEngine->addLemma(lem, false);
-        d_lemma_cache.insert(lem);
+        sendEvalUnfoldLemmas(eval_unfold_lemmas);
       }
     }
-
-    if (inst->addInstantiation(q, terms))
+    else if (mode == options::SygusInstMode::PRIORITY_EVAL)
+    {
+      if (!sendEvalUnfoldLemmas(eval_unfold_lemmas))
+      {
+        inst->addInstantiation(q, terms);
+      }
+    }
+    else
     {
-      Trace("sygus-inst") << "Instantiate " << q << std::endl;
+      Assert(mode == options::SygusInstMode::INTERLEAVE);
+      inst->addInstantiation(q, terms);
+      sendEvalUnfoldLemmas(eval_unfold_lemmas);
     }
   }
 }
 
+bool SygusInst::sendEvalUnfoldLemmas(const std::vector<Node>& lemmas)
+{
+  bool added_lemma = false;
+  for (const Node& lem : lemmas)
+  {
+    Trace("sygus-inst") << "Evaluation unfolding: " << lem << std::endl;
+    added_lemma |= d_quantEngine->addLemma(lem);
+  }
+  return added_lemma;
+}
+
 bool SygusInst::checkCompleteFor(Node q)
 {
   return d_inactive_quant.find(q) != d_inactive_quant.end();
@@ -440,6 +466,10 @@ void SygusInst::registerCeLemma(Node q, std::vector<TypeNode>& types)
 {
   Assert(q[0].getNumChildren() == types.size());
   Assert(d_ce_lemmas.find(q) == d_ce_lemmas.end());
+  Assert(d_inst_constants.find(q) == d_inst_constants.end());
+  Assert(d_var_eval.find(q) == d_var_eval.end());
+
+  Trace("sygus-inst") << "Register CE Lemma for " << q << std::endl;
 
   /* Generate counterexample lemma for 'q'. */
   NodeManager* nm = NodeManager::currentNM();
@@ -448,8 +478,8 @@ void SygusInst::registerCeLemma(Node q, std::vector<TypeNode>& types)
   /* For each variable x_i of \forall x_i . P[x_i], create a fresh datatype
    * instantiation constant ic_i with type types[i] and wrap each ic_i in
    * DT_SYGUS_EVAL(ic_i), which will be used to instantiate x_i. */
-  std::vector<Node> vars;
   std::vector<Node> evals;
+  std::vector<Node> inst_constants;
   for (size_t i = 0, size = types.size(); i < size; ++i)
   {
     TypeNode tn = types[i];
@@ -459,6 +489,7 @@ void SygusInst::registerCeLemma(Node q, std::vector<TypeNode>& types)
     Node ic = nm->mkInstConstant(tn);
     InstConstantAttribute ica;
     ic.setAttribute(ica, q);
+    Trace("sygus-inst") << "Create " << ic << " for " << var << std::endl;
 
     db->registerEnumerator(ic, ic, nullptr, ROLE_ENUM_MULTI_SOLUTION);
 
@@ -470,13 +501,13 @@ void SygusInst::registerCeLemma(Node q, std::vector<TypeNode>& types)
     }
     Node eval = nm->mkNode(kind::DT_SYGUS_EVAL, args);
 
-    d_inst_constants.emplace(std::make_pair(var, ic));
-    d_var_eval.emplace(std::make_pair(var, eval));
-
-    vars.push_back(var);
+    inst_constants.push_back(ic);
     evals.push_back(eval);
   }
 
+  d_inst_constants.emplace(q, inst_constants);
+  d_var_eval.emplace(q, evals);
+
   Node lit = getCeLiteral(q);
   d_quantEngine->addRequirePhase(lit, true);
 
@@ -496,7 +527,7 @@ void SygusInst::registerCeLemma(Node q, std::vector<TypeNode>& types)
 
   /* Add counterexample lemma (lit => ~P[x_i/eval_i]) */
   Node body =
-      q[1].substitute(vars.begin(), vars.end(), evals.begin(), evals.end());
+      q[1].substitute(q[0].begin(), q[0].end(), evals.begin(), evals.end());
   Node lem = nm->mkNode(kind::OR, lit.negate(), body.negate());
   lem = Rewriter::rewrite(lem);
 
diff --git a/src/theory/quantifiers/sygus_inst.h b/src/theory/quantifiers/sygus_inst.h
index c95c6a026..0358b4984 100644
--- a/src/theory/quantifiers/sygus_inst.h
+++ b/src/theory/quantifiers/sygus_inst.h
@@ -99,11 +99,17 @@ class SygusInst : public QuantifiersModule
    * preRegisterQuantifier() call.*/
   void addCeLemma(Node q);
 
-  /* Maps bound variables to corresponding instantiation constants. */
-  std::unordered_map<Node, Node, NodeHashFunction> d_inst_constants;
+  /* Send evaluation unfolding lemmas and cache them.
+   * Returns true if a new lemma (not cached) was added, and false otherwise.
+   */
+  bool sendEvalUnfoldLemmas(const std::vector<Node>& lemmas);
+
+  /* Maps quantifiers to a vector of instantiation constants. */
+  std::unordered_map<Node, std::vector<Node>, NodeHashFunction>
+      d_inst_constants;
 
-  /* Maps bound variables to corresponding DT_SYGUS_EVAL term. */
-  std::unordered_map<Node, Node, NodeHashFunction> d_var_eval;
+  /* Maps quantifiers to a vector of DT_SYGUS_EVAL terms. */
+  std::unordered_map<Node, std::vector<Node>, NodeHashFunction> d_var_eval;
 
   /* Maps quantified formulas to registered counterexample literals. */
   std::unordered_map<Node, Node, NodeHashFunction> d_ce_lits;
@@ -118,9 +124,6 @@ class SygusInst : public QuantifiersModule
   /* Currently inactive quantifiers. */
   std::unordered_set<Node, NodeHashFunction> d_inactive_quant;
 
-  /* Evaluation unfolding lemma. */
-  context::CDHashSet<Node, NodeHashFunction> d_lemma_cache;
-
   /* Registered counterexample lemma cache. */
   std::unordered_map<Node, Node, NodeHashFunction> d_ce_lemmas;