Repair constants using symbolic constructors (#1960)

1 files changed, 59 insertions, 10 deletions

diff --git a/src/theory/quantifiers/sygus/cegis.cpp b/src/theory/quantifiers/sygus/cegis.cpp
index fc41c7561..92ed41f3d 100644
--- a/src/theory/quantifiers/sygus/cegis.cpp
+++ b/src/theory/quantifiers/sygus/cegis.cpp
@@ -29,7 +29,7 @@ namespace theory {
 namespace quantifiers {
 
 Cegis::Cegis(QuantifiersEngine* qe, CegConjecture* p)
-    : SygusModule(qe, p), d_eval_unfold(nullptr)
+    : SygusModule(qe, p), d_eval_unfold(nullptr), d_using_gr_repair(false)
 {
   if (options::sygusEvalUnfold())
   {
@@ -66,10 +66,27 @@ bool Cegis::processInitialize(Node n,
                               const std::vector<Node>& candidates,
                               std::vector<Node>& lemmas)
 {
+  Trace("cegis") << "Initialize cegis..." << std::endl;
   // initialize an enumerator for each candidate
   for (unsigned i = 0; i < candidates.size(); i++)
   {
-    d_tds->registerEnumerator(candidates[i], candidates[i], d_parent);
+    Trace("cegis") << "...register enumerator " << candidates[i];
+    bool do_repair_const = false;
+    if (options::sygusRepairConst())
+    {
+      TypeNode ctn = candidates[i].getType();
+      d_tds->registerSygusType(ctn);
+      if (d_tds->hasSubtermSymbolicCons(ctn))
+      {
+        do_repair_const = true;
+        // remember that we are doing grammar-based repair
+        d_using_gr_repair = true;
+        Trace("cegis") << " (using repair)";
+      }
+    }
+    Trace("cegis") << std::endl;
+    d_tds->registerEnumerator(
+        candidates[i], candidates[i], d_parent, false, do_repair_const);
   }
   return true;
 }
@@ -156,6 +173,46 @@ bool Cegis::constructCandidates(const std::vector<Node>& enums,
       Trace("cegis") << ss.str() << std::endl;
     }
   }
+  // if we are using grammar-based repair
+  if (d_using_gr_repair)
+  {
+    SygusRepairConst* src = d_parent->getRepairConst();
+    Assert(src != nullptr);
+    // check if any enum_values have symbolic terms that must be repaired
+    bool mustRepair = false;
+    for (const Node& c : enum_values)
+    {
+      if (SygusRepairConst::mustRepair(c))
+      {
+        mustRepair = true;
+        break;
+      }
+    }
+    Trace("cegis") << "...must repair is: " << mustRepair << std::endl;
+    // if the solution contains a subterm that must be repaired
+    if (mustRepair)
+    {
+      std::vector<Node> fail_cvs = enum_values;
+      Assert(candidates.size() == fail_cvs.size());
+      if (src->repairSolution(candidates, fail_cvs, candidate_values))
+      {
+        return true;
+      }
+      // repair solution didn't work, exclude this solution
+      std::vector<Node> exp;
+      for (unsigned i = 0, size = enums.size(); i < size; i++)
+      {
+        d_tds->getExplain()->getExplanationForEquality(
+            enums[i], enum_values[i], exp);
+      }
+      Assert(!exp.empty());
+      Node expn =
+          exp.size() == 1 ? exp[0] : NodeManager::currentNM()->mkNode(AND, exp);
+      lems.push_back(expn.negate());
+      return false;
+    }
+  }
+
   // evaluate on refinement lemmas
   bool addedEvalLemmas = addEvalLemmas(enums, enum_values);
 
@@ -197,14 +254,6 @@ bool Cegis::processConstructCandidates(const std::vector<Node>& enums,
         candidate_values.end(), enum_values.begin(), enum_values.end());
     return true;
   }
-  SygusRepairConst* src = d_parent->getRepairConst();
-  if (src != nullptr)
-  {
-    // it may be repairable
-    std::vector<Node> fail_cvs = enum_values;
-    Assert(candidates.size() == fail_cvs.size());
-    return src->repairSolution(candidates, fail_cvs, candidate_values);
-  }
   return false;
 }