Refactoring get enumerator values in construct candidate for cegis unif (#1926)

3 files changed, 112 insertions, 54 deletions

diff --git a/src/theory/quantifiers/sygus/cegis_unif.cpp b/src/theory/quantifiers/sygus/cegis_unif.cpp
index 8db60d373..ac70a97b2 100644
--- a/src/theory/quantifiers/sygus/cegis_unif.cpp
+++ b/src/theory/quantifiers/sygus/cegis_unif.cpp
@@ -97,20 +97,6 @@ void CegisUnif::getTermList(const std::vector<Node>& candidates,
                                      << hd << "\n";
       enums.push_back(hd);
     }
-    // for each decision tree strategy allocated for c (these are referenced
-    // by strategy points in d_cand_to_strat_pt[c])
-    for (const Node& e : d_cand_to_strat_pt[c])
-    {
-      std::vector<Node> cenums;
-      // also get the current conditional enumerators
-      d_u_enum_manager.getCondEnumeratorsForStrategyPt(e, cenums);
-      for (const Node& ce : cenums)
-      {
-        d_cenum_to_strat_pt[ce] = e;
-      }
-      // conditional enumerators are also part of list
-      enums.insert(enums.end(), cenums.begin(), cenums.end());
-    }
   }
 }
 
@@ -120,49 +106,109 @@ bool CegisUnif::constructCandidates(const std::vector<Node>& enums,
                                     std::vector<Node>& candidate_values,
                                     std::vector<Node>& lems)
 {
-  // build the values of the condition enumerators for each strategy point
-  std::map<Node, std::vector<Node>> condition_map;
-  Trace("cegis-unif-enum") << "Register new enumerated values :\n";
-  // keep track of the relation between conditional enums and their values
-  NodePairMap cenum_to_value;
-  for (unsigned i = 0, size = enums.size(); i < size; ++i)
+  if (Trace.isOn("cegis-unif-enum"))
   {
-    // Non-unif enums (which are the very candidates) should not be notified
-    if (enums[i] == candidates[i] && !d_sygus_unif.usingUnif(enums[i]))
+    Trace("cegis-unif-enum") << "  Evaluation heads :\n";
+    for (unsigned i = 0, size = enums.size(); i < size; ++i)
     {
-      Trace("cegis-unif-enum") << "  Ignoring non-unif candidate " << enums[i]
-                               << std::endl;
-      continue;
-    }
-    if (Trace.isOn("cegis-unif-enum"))
-    {
-      Trace("cegis-unif-enum") << "  " << enums[i] << " -> ";
+      Trace("cegis-unif-enum") << "    " << enums[i] << " -> ";
       std::stringstream ss;
       Printer::getPrinter(options::outputLanguage())
           ->toStreamSygus(ss, enum_values[i]);
       Trace("cegis-unif-enum") << ss.str() << std::endl;
     }
-    Node e = enums[i], v = enum_values[i];
-    std::map<Node, Node>::iterator itc = d_cenum_to_strat_pt.find(e);
-    if (itc != d_cenum_to_strat_pt.end())
-    {
-      cenum_to_value[e] = v;
-      Trace("cegis-unif-enum") << "   ...this is a condition for " << e << "\n";
-      // it is the value of a current condition
-      condition_map[itc->second].push_back(v);
-    }
   }
   // evaluate on refinement lemmas
   if (addEvalLemmas(enums, enum_values))
   {
     return false;
   }
-  // inform the unif utility that we are using these conditions
-  for (const std::pair<const Node, std::vector<Node>> cs : condition_map)
+  // the unification enumerators (return values, conditions) and their model
+  // values
+  NodeManager* nm = NodeManager::currentNM();
+  bool addedUnifEnumSymBreakLemma = false;
+  std::map<Node, std::vector<Node>> unif_enums[2];
+  std::map<Node, std::vector<Node>> unif_values[2];
+  for (const Node& c : candidates)
+  {
+    // for each decision tree strategy allocated for c (these are referenced
+    // by strategy points in d_cand_to_strat_pt[c])
+    for (const Node& e : d_cand_to_strat_pt[c])
+    {
+      for (unsigned index = 0; index < 2; index++)
+      {
+        Trace("cegis-unif-enum")
+            << "  " << (index == 0 ? "Return values" : "Conditions") << " for "
+            << e << ":\n";
+        // get the current unification enumerators
+        d_u_enum_manager.getEnumeratorsForStrategyPt(
+            e, unif_enums[index][e], index);
+        // get the model value of each enumerator
+        for (const Node& eu : unif_enums[index][e])
+        {
+          Node m_eu = d_parent->getModelValue(eu);
+          if (Trace.isOn("cegis-unif-enum"))
+          {
+            Trace("cegis-unif-enum") << "    " << eu << " -> ";
+            std::stringstream ss;
+            Printer::getPrinter(options::outputLanguage())
+                ->toStreamSygus(ss, m_eu);
+            Trace("cegis-unif-enum") << ss.str() << std::endl;
+          }
+          unif_values[index][e].push_back(m_eu);
+        }
+        // inter-enumerator symmetry breaking
+        // given a pool of unification enumerators eu_1, ..., eu_n,
+        // CegisUnifEnumManager insists that size(eu_1) <= ... <= size(eu_n).
+        // We additionally insist that M(eu_i) < M(eu_{i+1}) when
+        // size(eu_i) = size(eu_{i+1}), where < is pointer comparison.
+        // We enforce this below by adding symmetry breaking lemmas of the form
+        //  ~( eu_i = M(eu_i) ^ eu_{i+1} = M(eu_{i+1} ) )
+        // when applicable.
+        for (unsigned j = 1, nenum = unif_values[index][e].size(); j < nenum;
+             j++)
+        {
+          Node prev_val = unif_values[index][e][j - 1];
+          Node curr_val = unif_values[index][e][j];
+          // compare the node values
+          if (curr_val < prev_val)
+          {
+            // must have the same size
+            unsigned prev_size = d_tds->getSygusTermSize(prev_val);
+            unsigned curr_size = d_tds->getSygusTermSize(curr_val);
+            Assert(prev_size <= curr_size);
+            if (curr_size == prev_size)
+            {
+              Node slem = nm->mkNode(AND,
+                                     unif_enums[index][e][j - 1].eqNode(
+                                         unif_values[index][e][j - 1]),
+                                     unif_enums[index][e][j].eqNode(
+                                         unif_values[index][e][j]))
+                              .negate();
+              Trace("cegis-unif") << "CegisUnif::lemma, inter-unif-enumerator "
+                                     "symmetry breaking lemma : "
+                                  << slem << "\n";
+              d_qe->getOutputChannel().lemma(slem);
+              addedUnifEnumSymBreakLemma = true;
+              break;
+            }
+          }
+        }
+      }
+    }
+  }
+  if (addedUnifEnumSymBreakLemma)
+  {
+    return false;
+  }
+  // set the conditions
+  for (const Node& c : candidates)
   {
-    d_sygus_unif.setConditions(cs.first, cs.second);
+    for (const Node& e : d_cand_to_strat_pt[c])
+    {
+      d_sygus_unif.setConditions(e, unif_values[1][e]);
+    }
   }
-  // TODO : check symmetry breaking for enumerators
   // build solutions (for unif candidates a divide-and-conquer approach is used)
   std::vector<Node> sols;
   if (d_sygus_unif.constructSolution(sols))
@@ -186,18 +232,22 @@ bool CegisUnif::constructCandidates(const std::vector<Node>& enums,
     // Build separation lemma based on current size, and for each heads that
     // could not be separated, the condition values currently enumerated for its
     // decision tree
-    NodeManager* nm = NodeManager::currentNM();
     Node neg_cost_lit = d_u_enum_manager.getCurrentLiteral().negate();
     std::vector<Node> cenums, cond_eqs;
     for (std::pair<const Node, std::vector<Node>>& np : sepPairs)
     {
+      Node e = np.first;
       // Build equalities between condition enumerators associated with the
       // strategy point whose decision tree could not separate the given heads
-      d_u_enum_manager.getCondEnumeratorsForStrategyPt(np.first, cenums);
-      for (const Node& ce : cenums)
+      std::vector<Node> cond_eqs;
+      std::map<Node, std::vector<Node>>::iterator itue = unif_enums[1].find(e);
+      Assert(itue != unif_enums[1].end());
+      std::map<Node, std::vector<Node>>::iterator ituv = unif_values[1].find(e);
+      Assert(ituv != unif_values[1].end());
+      Assert(itue->second.size() == ituv->second.size());
+      for (unsigned i = 0, size = itue->second.size(); i < size; i++)
       {
-        Assert(cenum_to_value.find(ce) != cenum_to_value.end());
-        cond_eqs.push_back(nm->mkNode(EQUAL, ce, cenum_to_value[ce]));
+        cond_eqs.push_back(itue->second[i].eqNode(ituv->second[i]));
       }
       Assert(!cond_eqs.empty());
       Node neg_conds_lit =
@@ -318,13 +368,15 @@ void CegisUnifEnumManager::initialize(
   incrementNumEnumerators();
 }
 
-void CegisUnifEnumManager::getCondEnumeratorsForStrategyPt(
-    Node e, std::vector<Node>& ces) const
+void CegisUnifEnumManager::getEnumeratorsForStrategyPt(Node e,
+                                                       std::vector<Node>& es,
+                                                       unsigned index) const
 {
   std::map<Node, StrategyPtInfo>::const_iterator itc = d_ce_info.find(e);
   Assert(itc != d_ce_info.end());
-  ces.insert(
-      ces.end(), itc->second.d_enums[1].begin(), itc->second.d_enums[1].end());
+  es.insert(es.end(),
+            itc->second.d_enums[index].begin(),
+            itc->second.d_enums[index].end());
 }
 
 void CegisUnifEnumManager::registerEvalPts(const std::vector<Node>& eis, Node e)
diff --git a/src/theory/quantifiers/sygus/cegis_unif.h b/src/theory/quantifiers/sygus/cegis_unif.h
index ce096b127..735477821 100644
--- a/src/theory/quantifiers/sygus/cegis_unif.h
+++ b/src/theory/quantifiers/sygus/cegis_unif.h
@@ -59,8 +59,14 @@ class CegisUnifEnumManager
   void initialize(const std::vector<Node>& es,
                   const std::map<Node, Node>& e_to_cond,
                   const std::map<Node, std::vector<Node>>& strategy_lemmas);
-  /** get the current set of conditional enumerators for strategy point e */
-  void getCondEnumeratorsForStrategyPt(Node e, std::vector<Node>& ces) const;
+  /** get the current set of enumerators for strategy point e
+   *
+   * Index 0 adds the set of return value enumerators to es, index 1 adds the
+   * set of condition enumerators to es.
+   */
+  void getEnumeratorsForStrategyPt(Node e,
+                                   std::vector<Node>& es,
+                                   unsigned index) const;
   /** register evaluation point for candidate
    *
    * This notifies this class that eis is a set of heads of evaluation points
diff --git a/src/theory/quantifiers/sygus/term_database_sygus.cpp b/src/theory/quantifiers/sygus/term_database_sygus.cpp
index 774ba2180..3d88cbe5d 100644
--- a/src/theory/quantifiers/sygus/term_database_sygus.cpp
+++ b/src/theory/quantifiers/sygus/term_database_sygus.cpp
@@ -112,7 +112,7 @@ Node TermDbSygus::getProxyVariable(TypeNode tn, Node c)
   Assert(
       TypeNode::fromType(
           static_cast<DatatypeType>(tn.toType()).getDatatype().getSygusType())
-      == c.getType());
+          .isComparableTo(c.getType()));
 
   std::map<Node, Node>::iterator it = d_proxy_vars[tn].find(c);
   if (it == d_proxy_vars[tn].end())