Fix purification in SygusUnifRL (#1912)

3 files changed, 30 insertions, 18 deletions

diff --git a/src/theory/quantifiers/sygus/cegis_unif.cpp b/src/theory/quantifiers/sygus/cegis_unif.cpp
index 2456839e7..def21e6cc 100644
--- a/src/theory/quantifiers/sygus/cegis_unif.cpp
+++ b/src/theory/quantifiers/sygus/cegis_unif.cpp
@@ -38,11 +38,10 @@ bool CegisUnif::initialize(Node n,
                            const std::vector<Node>& candidates,
                            std::vector<Node>& lemmas)
 {
-  Trace("cegis-unif") << "Initialize CegisUnif : " << n << std::endl;
+  Trace("cegis-unif-debug") << "Initialize CegisUnif : " << n << std::endl;
   // Init UNIF util
   std::map<Node, std::vector<Node>> strategy_lemmas;
   d_sygus_unif.initialize(d_qe, candidates, d_cond_enums, strategy_lemmas);
-  Trace("cegis-unif") << "Initializing enums for pure Cegis case\n";
   std::vector<Node> unif_candidates;
   // Initialize enumerators for non-unif functions-to-synhesize
   for (const Node& c : candidates)
@@ -148,7 +147,6 @@ bool CegisUnif::constructCandidates(const std::vector<Node>& enums,
   // evaluate on refinement lemmas
   if (addEvalLemmas(enums, enum_values))
   {
-    Trace("cegis-unif-lemma") << "Added eval lemmas\n";
     return false;
   }
   // build solutions (for unif candidates a divide-and-conquer approach is used)
@@ -179,11 +177,10 @@ void CegisUnif::registerRefinementLemma(const std::vector<Node>& vars,
   std::map<Node, std::vector<Node>> eval_pts;
   Node plem = d_sygus_unif.addRefLemma(lem, eval_pts);
   d_refinement_lemmas.push_back(plem);
-  Trace("cegis-unif") << "* Refinement lemma:\n" << plem << "\n";
+  Trace("cegis-unif-lemma") << "* Refinement lemma:\n" << plem << "\n";
   // Notify the enumeration manager if there are new evaluation points
   for (const std::pair<const Node, std::vector<Node>>& ep : eval_pts)
   {
-    Trace("cegis-unif") << "** Registering new point:\n" << plem << "\n";
     d_u_enum_manager.registerEvalPts(ep.second, ep.first);
   }
   // Make the refinement lemma and add it to lems. This lemma is guarded by the
diff --git a/src/theory/quantifiers/sygus/sygus_unif_rl.cpp b/src/theory/quantifiers/sygus/sygus_unif_rl.cpp
index 427d413c8..6f68a9871 100644
--- a/src/theory/quantifiers/sygus/sygus_unif_rl.cpp
+++ b/src/theory/quantifiers/sygus/sygus_unif_rl.cpp
@@ -111,10 +111,25 @@ Node SygusUnifRl::purifyLemma(Node n,
     // occurring under a unification function-to-synthesize
     if (ensureConst)
     {
-      nv = d_parent->getModelValue(n);
-      Assert(n != nv);
+      std::map<Node, Node>::iterator it = d_cand_to_sol.find(n[0]);
+      // if function-to-synthesize, retrieve its built solution to replace in
+      // the application before computing the model value
+      AlwaysAssert(!u_fapp || it != d_cand_to_sol.end());
+      if (it != d_cand_to_sol.end())
+      {
+        TNode cand = n[0];
+        Node tmp = n.substitute(cand, it->second);
+        nv = d_tds->evaluateWithUnfolding(tmp);
+        Trace("sygus-unif-rl-purify") << "PurifyLemma : model value for " << tmp
+                                      << " is " << nv << "\n";
+      }
+      else
+      {
+        nv = d_parent->getModelValue(n);
       Trace("sygus-unif-rl-purify") << "PurifyLemma : model value for " << n
                                     << " is " << nv << "\n";
+      }
+      Assert(n != nv);
     }
   }
   // Travese to purify
@@ -299,20 +314,18 @@ bool SygusUnifRl::constructSolution(std::vector<Node>& sols)
       Trace("sygus-unif-rl-sol") << "Adding solution " << v
                                  << " to non-unif candidate " << c << "\n";
       sols.push_back(v);
+      continue;
     }
-    else
+    initializeConstructSolFor(c);
+    Node v = constructSol(c, d_strategy[c].getRootEnumerator(), role_equal, 0);
+    if (v.isNull())
     {
-      initializeConstructSolFor(c);
-      Node v =
-          constructSol(c, d_strategy[c].getRootEnumerator(), role_equal, 0);
-      if (v.isNull())
-      {
-        return false;
-      }
-      Trace("sygus-unif-rl-sol") << "Adding solution " << v
-                                 << " to unif candidate " << c << "\n";
-      sols.push_back(v);
+      return false;
     }
+    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;
 }
diff --git a/src/theory/quantifiers/sygus/sygus_unif_rl.h b/src/theory/quantifiers/sygus/sygus_unif_rl.h
index 941bb5763..09a226ae7 100644
--- a/src/theory/quantifiers/sygus/sygus_unif_rl.h
+++ b/src/theory/quantifiers/sygus/sygus_unif_rl.h
@@ -98,6 +98,8 @@ class SygusUnifRl : public SygusUnif
   void initializeConstructSol() override;
   /** initialize construction solution for function-to-synthesize f */
   void initializeConstructSolFor(Node f) override;
+  /** maps unif functions-to~synhesize to their last built solutions */
+  std::map<Node, Node> d_cand_to_sol;
   /*
     --------------------------------------------------------------
         Purification