Repair constants using symbolic constructors (#1960)

1 files changed, 11 insertions, 1 deletions

diff --git a/src/theory/quantifiers/sygus/cegis.h b/src/theory/quantifiers/sygus/cegis.h
index 70f3ce8b6..ca27a2281 100644
--- a/src/theory/quantifiers/sygus/cegis.h
+++ b/src/theory/quantifiers/sygus/cegis.h
@@ -79,7 +79,7 @@ class Cegis : public SygusModule
   virtual bool processInitialize(Node n,
                                  const std::vector<Node>& candidates,
                                  std::vector<Node>& lemmas);
-  /** do cegis-implementation-specific construct candidate
+  /** do cegis-implementation-specific post-processing for construct candidate
    *
    * satisfiedRl is whether all refinement lemmas are satisfied under the
    * substitution { enums -> enum_values }.
@@ -164,6 +164,16 @@ class Cegis : public SygusModule
    * added as refinement lemmas.
    */
   std::unordered_set<unsigned> d_cegis_sample_refine;
+
+  //---------------------------------for sygus repair
+  /** are we using grammar-based repair?
+   *
+   * This flag is set ot true if at least one of the enumerators allocated
+   * by this class has been configured to allow model values with symbolic
+   * constructors, such as the "any constant" constructor.
+   */
+  bool d_using_gr_repair;
+  //---------------------------------end for sygus repair
 };
 
 } /* CVC4::theory::quantifiers namespace */