Building and refining solutions with dynamic condition generation in CegisUnif (#1920)

6 files changed, 181 insertions, 70 deletions

diff --git a/src/theory/quantifiers/lazy_trie.cpp b/src/theory/quantifiers/lazy_trie.cpp
index 21a87c792..33d8adaa1 100644
--- a/src/theory/quantifiers/lazy_trie.cpp
+++ b/src/theory/quantifiers/lazy_trie.cpp
@@ -148,6 +148,12 @@ Node LazyTrieMulti::add(Node f, LazyTrieEvaluator* ev, unsigned ntotal)
   return res;
 }
 
+void LazyTrieMulti::clear()
+{
+  d_trie.clear();
+  d_rep_to_class.clear();
+}
+
 } /* CVC4::theory::quantifiers namespace */
 } /* CVC4::theory namespace */
 } /* CVC4 namespace */
diff --git a/src/theory/quantifiers/lazy_trie.h b/src/theory/quantifiers/lazy_trie.h
index 935b9bec1..3585247c6 100644
--- a/src/theory/quantifiers/lazy_trie.h
+++ b/src/theory/quantifiers/lazy_trie.h
@@ -159,6 +159,9 @@ class LazyTrieMulti
    * containing only itself.
    */
   Node add(Node f, LazyTrieEvaluator* ev, unsigned ntotal);
+  /** clear the trie */
+  void clear();
+
   /** A regular lazy trie */
   LazyTrie d_trie;
 };
diff --git a/src/theory/quantifiers/sygus/cegis_unif.cpp b/src/theory/quantifiers/sygus/cegis_unif.cpp
index 920b142bb..8db60d373 100644
--- a/src/theory/quantifiers/sygus/cegis_unif.cpp
+++ b/src/theory/quantifiers/sygus/cegis_unif.cpp
@@ -68,8 +68,8 @@ bool CegisUnif::initialize(Node n,
       {
         Node cond = d_sygus_unif.getConditionForEvaluationPoint(e);
         Assert(!cond.isNull());
-        Trace("cegis-unif")
-            << "  " << e << " with condition : " << cond << std::endl;
+        Trace("cegis-unif") << "  " << e << " with condition : " << cond
+                            << std::endl;
         pt_to_cond[e] = cond;
       }
     }
@@ -123,6 +123,8 @@ bool CegisUnif::constructCandidates(const std::vector<Node>& enums,
   // 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)
   {
     // Non-unif enums (which are the very candidates) should not be notified
@@ -144,6 +146,7 @@ bool CegisUnif::constructCandidates(const std::vector<Node>& enums,
     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);
@@ -160,8 +163,6 @@ bool CegisUnif::constructCandidates(const std::vector<Node>& enums,
     d_sygus_unif.setConditions(cs.first, cs.second);
   }
   // TODO : check symmetry breaking for enumerators
-  // TODO : check separation of evaluation heads wrt condition enumerators and
-  // add lemmas.
   // build solutions (for unif candidates a divide-and-conquer approach is used)
   std::vector<Node> sols;
   if (d_sygus_unif.constructSolution(sols))
@@ -179,6 +180,48 @@ bool CegisUnif::constructCandidates(const std::vector<Node>& enums,
     }
     return true;
   }
+  std::map<Node, std::vector<Node>> sepPairs;
+  if (d_sygus_unif.getSeparationPairs(sepPairs))
+  {
+    // 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)
+    {
+      // 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)
+      {
+        Assert(cenum_to_value.find(ce) != cenum_to_value.end());
+        cond_eqs.push_back(nm->mkNode(EQUAL, ce, cenum_to_value[ce]));
+      }
+      Assert(!cond_eqs.empty());
+      Node neg_conds_lit =
+          cond_eqs.size() > 1 ? nm->mkNode(AND, cond_eqs) : cond_eqs[0];
+      neg_conds_lit = neg_conds_lit.negate();
+      for (const Node& eq : np.second)
+      {
+        // A separation lemma is of the shape
+        //   (cost_n+1 ^ (c_1 = M(c_1) ^ ... ^ M(c_n))) => e_i = e_j
+        // in which cost_n+1 is the cost function for the size n+1, each c_k is
+        // a conditional enumerator associated with the respective decision
+        // tree, each M(c_k) its current model value, and e_i, e_j are two
+        // distinct heads that could not be separated by these condition values
+        //
+        // Such a lemma will force the ground solver, within the restrictions of
+        // the respective cost function, to make e_i and e_j equal or to come up
+        // with new values for the conditional enumerators such that we can try
+        Node sep_lemma = nm->mkNode(OR, neg_cost_lit, neg_conds_lit, eq);
+        Trace("cegis-unif")
+            << "CegisUnif::lemma, separation lemma : " << sep_lemma << "\n";
+        d_qe->getOutputChannel().lemma(sep_lemma);
+      }
+    }
+  }
   return false;
 }
 
@@ -194,7 +237,12 @@ void CegisUnif::registerRefinementLemma(const std::vector<Node>& vars,
   // Notify the enumeration manager if there are new evaluation points
   for (const std::pair<const Node, std::vector<Node>>& ep : eval_pts)
   {
-    d_u_enum_manager.registerEvalPts(ep.second, ep.first);
+    Assert(d_cand_to_strat_pt.find(ep.first) != d_cand_to_strat_pt.end());
+    // Notify each startegy point of the respective candidate
+    for (const Node& n : d_cand_to_strat_pt[ep.first])
+    {
+      d_u_enum_manager.registerEvalPts(ep.second, n);
+    }
   }
   // Make the refinement lemma and add it to lems. This lemma is guarded by the
   // parent's guard, which has the semantics "this conjecture has a solution",
@@ -242,8 +290,8 @@ void CegisUnifEnumManager::initialize(
     std::map<Node, Node>::const_iterator itcc = e_to_cond.find(e);
     Assert(itcc != e_to_cond.end());
     Node cond = itcc->second;
-    Trace("cegis-unif-enum-debug")
-        << "...its condition strategy point is " << cond << "\n";
+    Trace("cegis-unif-enum-debug") << "...its condition strategy point is "
+                                   << cond << "\n";
     d_ce_info[e].d_ce_type = cond.getType();
     // initialize the symmetry breaking lemma templates
     for (unsigned index = 0; index < 2; index++)
@@ -366,9 +414,6 @@ void CegisUnifEnumManager::incrementNumEnumerators()
         {
           continue;
         }
-        // register the enumerator
-        ci.second.d_enums[index].push_back(e);
-        d_tds->registerEnumerator(e, ci.second.d_pt, d_parent);
         // instantiate template for removing redundant operators
         if (!ci.second.d_sbt_lemma_tmpl[index].first.isNull())
         {
@@ -381,21 +426,34 @@ void CegisUnifEnumManager::incrementNumEnumerators()
           d_qe->getOutputChannel().lemma(sym_break_red_ops);
         }
         // symmetry breaking between enumerators
-        Node e_prev = ci.second.d_enums[index].back();
-        Node size_e = nm->mkNode(DT_SIZE, e);
-        Node size_e_prev = nm->mkNode(DT_SIZE, e_prev);
-        Node sym_break = nm->mkNode(GEQ, size_e, size_e_prev);
-        Trace("cegis-unif-enum-lemma")
-            << "CegisUnifEnum::lemma, enum sym break:" << sym_break << "\n";
-        d_qe->getOutputChannel().lemma(sym_break);
+        if (!ci.second.d_enums[index].empty())
+        {
+          Node e_prev = ci.second.d_enums[index].back();
+          Node size_e = nm->mkNode(DT_SIZE, e);
+          Node size_e_prev = nm->mkNode(DT_SIZE, e_prev);
+          Node sym_break = nm->mkNode(GEQ, size_e, size_e_prev);
+          Trace("cegis-unif-enum-lemma")
+              << "CegisUnifEnum::lemma, enum sym break:" << sym_break << "\n";
+          d_qe->getOutputChannel().lemma(sym_break);
+        }
+        // register the enumerator
+        ci.second.d_enums[index].push_back(e);
+        Trace("cegis-unif-enum") << "* Registering new enumerator " << e
+                                 << " to strategy point " << ci.second.d_pt
+                                 << "\n";
+        d_tds->registerEnumerator(e, ci.second.d_pt, d_parent);
         // if the sygus datatype is interpreted as an infinite type
         // (this should be the case for almost all examples)
         TypeNode et = e.getType();
         if (!et.isInterpretedFinite())
         {
           // it is disequal from all previous ones
-          for (const Node ei : ci.second.d_enums[index])
+          for (const Node& ei : ci.second.d_enums[index])
           {
+            if (ei == e)
+            {
+              continue;
+            }
             Node deq = e.eqNode(ei).negate();
             Trace("cegis-unif-enum-lemma")
                 << "CegisUnifEnum::lemma, enum deq:" << deq << "\n";
diff --git a/src/theory/quantifiers/sygus/cegis_unif.h b/src/theory/quantifiers/sygus/cegis_unif.h
index 445ab5f6c..ce096b127 100644
--- a/src/theory/quantifiers/sygus/cegis_unif.h
+++ b/src/theory/quantifiers/sygus/cegis_unif.h
@@ -82,6 +82,11 @@ class CegisUnifEnumManager
    * registerEvalPtAtValue on the output channel of d_qe.
    */
   Node getNextDecisionRequest(unsigned& priority);
+  /**
+   * Get the "current" literal G_uq_n, where n is the minimal n such that G_uq_n
+   * is not asserted negatively in the current SAT context.
+   */
+  Node getCurrentLiteral() const;
 
  private:
   /** reference to quantifier engine */
@@ -138,11 +143,6 @@ class CegisUnifEnumManager
   context::CDO<unsigned> d_curr_guq_val;
   /** increment the number of enumerators */
   void incrementNumEnumerators();
-  /**
-   * Get the "current" literal G_uq_n, where n is the minimal n such that G_uq_n
-   * is not asserted negatively in the current SAT context.
-   */
-  Node getCurrentLiteral() const;
   /** get literal G_uq_n */
   Node getLiteral(unsigned n) const;
   /** register evaluation point at size
diff --git a/src/theory/quantifiers/sygus/sygus_unif_rl.cpp b/src/theory/quantifiers/sygus/sygus_unif_rl.cpp
index f59331d68..f7337a92d 100644
--- a/src/theory/quantifiers/sygus/sygus_unif_rl.cpp
+++ b/src/theory/quantifiers/sygus/sygus_unif_rl.cpp
@@ -100,8 +100,8 @@ Node SygusUnifRl::purifyLemma(Node n,
       else
       {
         nv = d_parent->getModelValue(n);
-      Trace("sygus-unif-rl-purify") << "PurifyLemma : model value for " << n
-                                    << " is " << nv << "\n";
+        Trace("sygus-unif-rl-purify") << "PurifyLemma : model value for " << n
+                                      << " is " << nv << "\n";
       }
       Assert(n != nv);
     }
@@ -263,10 +263,11 @@ Node SygusUnifRl::addRefLemma(Node lemma,
         for (const Node& stratpt : d_cenum_to_stratpt[cenum])
         {
           Assert(d_stratpt_to_dt.find(stratpt) != d_stratpt_to_dt.end());
-          Trace("sygus-unif-rl-dt") << "Add point with head " << cp.second[j]
-                                    << " to strategy point " << stratpt << "\n";
+          Trace("sygus-unif-rl-dt") << "Register point with head "
+                                    << cp.second[j] << " to strategy point "
+                                    << stratpt << "\n";
           // Register new point from new head
-          d_stratpt_to_dt[stratpt].addPoint(cp.second[j]);
+          d_stratpt_to_dt[stratpt].d_hds.push_back(cp.second[j]);
         }
       }
     }
@@ -275,18 +276,17 @@ Node SygusUnifRl::addRefLemma(Node lemma,
   return plem;
 }
 
-void SygusUnifRl::initializeConstructSol() {}
+void SygusUnifRl::initializeConstructSol() { d_sepPairs.clear(); }
 void SygusUnifRl::initializeConstructSolFor(Node f) {}
 bool SygusUnifRl::constructSolution(std::vector<Node>& sols)
 {
   initializeConstructSol();
+  bool successful = true;
   for (const Node& c : d_candidates)
   {
     if (!usingUnif(c))
     {
       Node v = d_parent->getModelValue(c);
-      Trace("sygus-unif-rl-sol") << "Adding solution " << v
-                                 << " to non-unif candidate " << c << "\n";
       sols.push_back(v);
       continue;
     }
@@ -294,14 +294,15 @@ bool SygusUnifRl::constructSolution(std::vector<Node>& sols)
     Node v = constructSol(c, d_strategy[c].getRootEnumerator(), role_equal, 0);
     if (v.isNull())
     {
-      return false;
+      // we continue trying to build solutions to accumulate potentitial
+      // separation conditions from other decision trees
+      successful = false;
+      continue;
     }
-    Trace("sygus-unif-rl-sol") << "Adding solution " << v
-                               << " to unif candidate " << c << "\n";
     sols.push_back(v);
     d_cand_to_sol[c] = v;
   }
-  return true;
+  return successful;
 }
 
 Node SygusUnifRl::constructSol(Node f, Node e, NodeRole nrole, int ind)
@@ -333,7 +334,21 @@ Node SygusUnifRl::constructSol(Node f, Node e, NodeRole nrole, int ind)
     return d_parent->getModelValue(e);
   }
   EnumTypeInfoStrat* etis = snode.d_strats[itd->second.getStrategyIndex()];
-  return itd->second.buildSol(etis->d_cons);
+  std::vector<Node> toSeparate;
+  Node sol = itd->second.buildSol(etis->d_cons, toSeparate);
+  if (sol.isNull())
+  {
+    Assert(!toSeparate.empty());
+    d_sepPairs[e] = toSeparate;
+  }
+  return sol;
+}
+
+bool SygusUnifRl::getSeparationPairs(
+    std::map<Node, std::vector<Node>>& sepPairs)
+{
+  sepPairs = d_sepPairs;
+  return !sepPairs.empty();
 }
 
 bool SygusUnifRl::usingUnif(Node f) const
@@ -352,13 +367,8 @@ void SygusUnifRl::setConditions(Node e, const std::vector<Node>& conds)
 {
   std::map<Node, DecisionTreeInfo>::iterator it = d_stratpt_to_dt.find(e);
   Assert(it != d_stratpt_to_dt.end());
-  it->second.clearCondValues();
-  /* TODO
-  for (const Node& c : conds)
-  {
-    it->second.addCondValue(c);
-  }
-  */
+  // Clear previous trie
+  it->second.resetPointSeparator(conds);
 }
 
 std::vector<Node> SygusUnifRl::getEvalPointHeads(Node c)
@@ -477,15 +487,19 @@ void SygusUnifRl::DecisionTreeInfo::initialize(Node cond_enum,
   d_pt_sep.initialize(this);
 }
 
-void SygusUnifRl::DecisionTreeInfo::addPoint(Node f)
+void SygusUnifRl::DecisionTreeInfo::resetPointSeparator(
+    const std::vector<Node>& conds)
 {
-  d_pt_sep.d_trie.add(f, &d_pt_sep, d_conds.size());
+  // clear old condition values and trie
+  d_conds.clear();
+  d_pt_sep.d_trie.clear();
+  // set new condition values
+  d_conds.insert(d_conds.end(), conds.begin(), conds.end());
 }
 
-void SygusUnifRl::DecisionTreeInfo::clearCondValues()
+void SygusUnifRl::DecisionTreeInfo::addPoint(Node f)
 {
-  // TODO
-  // d_conds.clear();
+  d_pt_sep.d_trie.add(f, &d_pt_sep, d_conds.size());
 }
 
 void SygusUnifRl::DecisionTreeInfo::addCondValue(Node condv)
@@ -501,14 +515,15 @@ unsigned SygusUnifRl::DecisionTreeInfo::getStrategyIndex() const
 
 using UNodePair = std::pair<unsigned, Node>;
 
-Node SygusUnifRl::DecisionTreeInfo::buildSol(Node cons)
+Node SygusUnifRl::DecisionTreeInfo::buildSol(Node cons,
+                                             std::vector<Node>& toSeparate)
 {
   if (!d_template.first.isNull())
   {
     Trace("sygus-unif-sol") << "...templated conditions unsupported\n";
     return Node::null();
   }
-  if (!isSeparated())
+  if (!isSeparated(toSeparate))
   {
     Trace("sygus-unif-sol") << "...separation check failed\n";
     return Node::null();
@@ -592,9 +607,16 @@ Node SygusUnifRl::DecisionTreeInfo::buildSol(Node cons)
   return cache[root];
 }
 
-bool SygusUnifRl::DecisionTreeInfo::isSeparated()
+bool SygusUnifRl::DecisionTreeInfo::isSeparated(std::vector<Node>& toSeparate)
 {
+  // build point separator
+  for (const Node& f : d_hds)
+  {
+    addPoint(f);
+  }
+  // check separation
   d_hd_values.clear();
+  NodeManager* nm = NodeManager::currentNM();
   for (const std::pair<const Node, std::vector<Node>>& rep_to_class :
        d_pt_sep.d_trie.d_rep_to_class)
   {
@@ -639,11 +661,14 @@ bool SygusUnifRl::DecisionTreeInfo::isSeparated()
         Trace("sygus-unif-rl-dt") << "...in sep class heads with diff values: "
                                   << rep_to_class.second[0] << " and "
                                   << rep_to_class.second[i] << "\n";
-        return false;
+        toSeparate.push_back(
+            nm->mkNode(EQUAL, rep_to_class.second[0], rep_to_class.second[i]));
+        // For non-separation suffices to consider one head pair per sep class
+        break;
       }
     }
   }
-  return true;
+  return toSeparate.empty();
 }
 
 void SygusUnifRl::DecisionTreeInfo::PointSeparator::initialize(
diff --git a/src/theory/quantifiers/sygus/sygus_unif_rl.h b/src/theory/quantifiers/sygus/sygus_unif_rl.h
index b5609e625..5bd6cdc1e 100644
--- a/src/theory/quantifiers/sygus/sygus_unif_rl.h
+++ b/src/theory/quantifiers/sygus/sygus_unif_rl.h
@@ -97,6 +97,15 @@ class SygusUnifRl : public SygusUnif
   /** retrieve the head of evaluation points for candidate c, if any */
   std::vector<Node> getEvalPointHeads(Node c);
 
+  /**
+   * if a separation condition is necessary after a failed solution
+   * construction, then sepCond is assigned a pair (e, fi = fj) in which e is
+   * the strategy point and fi, fj head of evaluation points of a unif
+   * function-to-synthesize, such that fi could not be separated from fj by the
+   * current condition values
+   */
+  bool getSeparationPairs(std::map<Node, std::vector<Node>>& sepPairs);
+
  protected:
   /** reference to the parent conjecture */
   CegConjecture* d_parent;
@@ -114,6 +123,12 @@ class SygusUnifRl : public SygusUnif
   void initializeConstructSolFor(Node f) override;
   /** maps unif functions-to~synhesize to their last built solutions */
   std::map<Node, Node> d_cand_to_sol;
+  /** pair of strategy point and equality between evaluation point heads
+   *
+   * this pair is set when a unif solution cannot be built because a two
+   * evaluation point heads cannot be separated
+   */
+  std::map<Node, std::vector<Node>> d_sepPairs;
   /*
     --------------------------------------------------------------
         Purification
@@ -190,12 +205,6 @@ class SygusUnifRl : public SygusUnif
                     SygusUnifRl* unif,
                     SygusUnifStrategy* strategy,
                     unsigned strategy_index);
-    /** adds the respective evaluation point of the head f  */
-    void addPoint(Node f);
-    /** clears the condition values */
-    void clearCondValues();
-    /** adds a condition value to the pool of condition values */
-    void addCondValue(Node condv);
     /** returns index of strategy information of strategy node for this DT */
     unsigned getStrategyIndex() const;
     /** builds solution stored in DT, if any, using the given constructor
@@ -203,22 +212,29 @@ class SygusUnifRl : public SygusUnif
      * The DT contains a solution when no class contains two heads of evaluation
      * points with different model values, i.e. when all points that must be
      * separated indeed are separated.
+     */
+    Node buildSol(Node cons, std::vector<Node>& toSeparate);
+    /** whether all points that must be separated are separated
      *
-     * This function tests separation of the points in the above sense and may
-     * create separation lemmas to enforce guide the synthesis of conditons that
-     * will separate points not currently separated.
+     * This function tests separation of the points in the above sense and in
+     * case two heads cannot be separated, an equality between them is created
+     * and stored in toSeparate, so that a separation lemma can be generated to
+     * guide the synthesis search to yield either conditions that will separate
+     * these heads or equal values to them.
      */
-    Node buildSol(Node cons);
-    /** whether all points that must be separated are separated **/
-    bool isSeparated();
+    bool isSeparated(std::vector<Node>& toSeparate);
     /** reference to parent unif util */
     SygusUnifRl* d_unif;
     /** enumerator template (if no templates, nodes in pair are Node::null()) */
     NodePair d_template;
     /** enumerated condition values */
     std::vector<Node> d_conds;
+    /** gathered evaluation point heads */
+    std::vector<Node> d_hds;
     /** get condition enumerator */
     Node getConditionEnumerator() const { return d_cond_enum; }
+    /** clear trie and registered condition values */
+    void resetPointSeparator(const std::vector<Node>& conds);
 
    private:
     /**
@@ -268,6 +284,10 @@ class SygusUnifRl : public SygusUnif
      * enumerated condiotion values
      */
     PointSeparator d_pt_sep;
+    /** adds the respective evaluation point of the head f to d_pt_sep */
+    void addPoint(Node f);
+    /** adds a value to the pool of condition values and to d_pt_sep */
+    void addCondValue(Node condv);
   };
   /** maps strategy points in the strategy tree to the above data */
   std::map<Node, DecisionTreeInfo> d_stratpt_to_dt;
@@ -301,11 +321,10 @@ class SygusUnifRl : public SygusUnif
    * Registers that cond is a conditional enumerator for building a (recursive)
    * decision tree at strategy node e within the strategy tree of f.
    */
-  void registerConditionalEnumerator(
-      Node f,
-      Node e,
-      Node cond,
-      unsigned strategy_index);
+  void registerConditionalEnumerator(Node f,
+                                     Node e,
+                                     Node cond,
+                                     unsigned strategy_index);
 };
 
 } /* CVC4::theory::quantifiers namespace */