Reenable repair const (#1983)

4 files changed, 37 insertions, 0 deletions

diff --git a/src/theory/quantifiers/sygus/ce_guided_conjecture.cpp b/src/theory/quantifiers/sygus/ce_guided_conjecture.cpp
index f66a97ce8..ecb6db2fb 100644
--- a/src/theory/quantifiers/sygus/ce_guided_conjecture.cpp
+++ b/src/theory/quantifiers/sygus/ce_guided_conjecture.cpp
@@ -258,6 +258,33 @@ void CegConjecture::doCheck(std::vector<Node>& lems)
   std::vector<Node> candidate_values;
   bool constructed_cand = false;
 
+  // If a module is not trying to repair constants in solutions and the option
+  // sygusRepairConst  is true, we use a default scheme for trying to repair
+  // constants here.
+  if (options::sygusRepairConst() && !d_master->usingRepairConst())
+  {
+    Trace("cegqi-check") << "CegConjuncture : repair previous solution..."
+                         << std::endl;
+    // have we tried to repair the previous solution?
+    // if not, call the repair constant utility
+    unsigned ninst = d_cinfo[d_candidates[0]].d_inst.size();
+    if (d_repair_index < ninst)
+    {
+      std::vector<Node> fail_cvs;
+      for (const Node& cprog : d_candidates)
+      {
+        Assert(d_repair_index < d_cinfo[cprog].d_inst.size());
+        fail_cvs.push_back(d_cinfo[cprog].d_inst[d_repair_index]);
+      }
+      d_repair_index++;
+      if (d_sygus_rconst->repairSolution(
+              d_candidates, fail_cvs, candidate_values))
+      {
+        constructed_cand = true;
+      }
+    }
+  }
+
   // get the model value of the relevant terms from the master module
   std::vector<Node> enum_values;
   getModelValues(terms, enum_values);
diff --git a/src/theory/quantifiers/sygus/cegis.cpp b/src/theory/quantifiers/sygus/cegis.cpp
index 92ed41f3d..ee54c3296 100644
--- a/src/theory/quantifiers/sygus/cegis.cpp
+++ b/src/theory/quantifiers/sygus/cegis.cpp
@@ -397,6 +397,8 @@ void Cegis::registerRefinementLemma(const std::vector<Node>& vars,
   lems.push_back(rlem);
 }
 
+bool Cegis::usingRepairConst() { return d_using_gr_repair; }
+
 void Cegis::getRefinementEvalLemmas(const std::vector<Node>& vs,
                                     const std::vector<Node>& ms,
                                     std::vector<Node>& lems)
diff --git a/src/theory/quantifiers/sygus/cegis.h b/src/theory/quantifiers/sygus/cegis.h
index ca27a2281..856219b73 100644
--- a/src/theory/quantifiers/sygus/cegis.h
+++ b/src/theory/quantifiers/sygus/cegis.h
@@ -63,6 +63,8 @@ class Cegis : public SygusModule
   virtual void registerRefinementLemma(const std::vector<Node>& vars,
                                        Node lem,
                                        std::vector<Node>& lems) override;
+  /** using repair const */
+  virtual bool usingRepairConst() override;
 
  protected:
   /** the evaluation unfold utility of d_tds */
diff --git a/src/theory/quantifiers/sygus/sygus_module.h b/src/theory/quantifiers/sygus/sygus_module.h
index 75be570e6..b01f8e1d0 100644
--- a/src/theory/quantifiers/sygus/sygus_module.h
+++ b/src/theory/quantifiers/sygus/sygus_module.h
@@ -122,6 +122,12 @@ class SygusModule
   {
     return Node::null();
   }
+  /**
+   * Are we trying to repair constants in candidate solutions?
+   * If we return true for usingRepairConst is true, then this module has
+   * attmepted to repair any solutions returned by constructCandidates.
+   */
+  virtual bool usingRepairConst() { return false; }
 
  protected:
   /** reference to quantifier engine */