Pass synthesis conjecture to sygus modules (#3212)

8 files changed, 37 insertions, 15 deletions

diff --git a/src/theory/quantifiers/sygus/cegis.cpp b/src/theory/quantifiers/sygus/cegis.cpp
index 301d772bf..1e8012697 100644
--- a/src/theory/quantifiers/sygus/cegis.cpp
+++ b/src/theory/quantifiers/sygus/cegis.cpp
@@ -39,7 +39,8 @@ Cegis::Cegis(QuantifiersEngine* qe, SynthConjecture* p)
   }
 }
 
-bool Cegis::initialize(Node n,
+bool Cegis::initialize(Node conj,
+                       Node n,
                        const std::vector<Node>& candidates,
                        std::vector<Node>& lemmas)
 {
@@ -61,10 +62,11 @@ bool Cegis::initialize(Node n,
     TypeNode bt = d_base_body.getType();
     d_cegis_sampler.initialize(bt, d_base_vars, options::sygusSamples());
   }
-  return processInitialize(n, candidates, lemmas);
+  return processInitialize(conj, n, candidates, lemmas);
 }
 
-bool Cegis::processInitialize(Node n,
+bool Cegis::processInitialize(Node conj,
+                              Node n,
                               const std::vector<Node>& candidates,
                               std::vector<Node>& lemmas)
 {
diff --git a/src/theory/quantifiers/sygus/cegis.h b/src/theory/quantifiers/sygus/cegis.h
index a295f6a40..891379992 100644
--- a/src/theory/quantifiers/sygus/cegis.h
+++ b/src/theory/quantifiers/sygus/cegis.h
@@ -44,7 +44,8 @@ class Cegis : public SygusModule
   Cegis(QuantifiersEngine* qe, SynthConjecture* p);
   ~Cegis() override {}
   /** initialize */
-  virtual bool initialize(Node n,
+  virtual bool initialize(Node conj,
+                          Node n,
                           const std::vector<Node>& candidates,
                           std::vector<Node>& lemmas) override;
   /** get term list */
@@ -77,14 +78,21 @@ class Cegis : public SygusModule
    */
   Node d_base_body;
   //----------------------------------cegis-implementation-specific
-  /** do cegis-implementation-specific initialization for this class */
-  virtual bool processInitialize(Node n,
+  /**
+   * Do cegis-implementation-specific initialization for this class. The return
+   * value and behavior of this function is the same as initialize(...) above.
+   */
+  virtual bool processInitialize(Node conj,
+                                 Node n,
                                  const std::vector<Node>& candidates,
                                  std::vector<Node>& lemmas);
   /** do cegis-implementation-specific post-processing for construct candidate
    *
    * satisfiedRl is whether all refinement lemmas are satisfied under the
    * substitution { enums -> enum_values }.
+   *
+   * The return value and behavior of this function is the same as
+   * constructCandidates(...) above.
    */
   virtual bool processConstructCandidates(const std::vector<Node>& enums,
                                           const std::vector<Node>& enum_values,
diff --git a/src/theory/quantifiers/sygus/cegis_unif.cpp b/src/theory/quantifiers/sygus/cegis_unif.cpp
index 6e9467b7c..399a9576c 100644
--- a/src/theory/quantifiers/sygus/cegis_unif.cpp
+++ b/src/theory/quantifiers/sygus/cegis_unif.cpp
@@ -35,7 +35,8 @@ CegisUnif::CegisUnif(QuantifiersEngine* qe, SynthConjecture* p)
 }
 
 CegisUnif::~CegisUnif() {}
-bool CegisUnif::processInitialize(Node n,
+bool CegisUnif::processInitialize(Node conj,
+                                  Node n,
                                   const std::vector<Node>& candidates,
                                   std::vector<Node>& lemmas)
 {
diff --git a/src/theory/quantifiers/sygus/cegis_unif.h b/src/theory/quantifiers/sygus/cegis_unif.h
index a2e7be1c1..ac859750f 100644
--- a/src/theory/quantifiers/sygus/cegis_unif.h
+++ b/src/theory/quantifiers/sygus/cegis_unif.h
@@ -233,7 +233,8 @@ class CegisUnif : public Cegis
 
  private:
   /** do cegis-implementation-specific initialization for this class */
-  bool processInitialize(Node n,
+  bool processInitialize(Node conj,
+                         Node n,
                          const std::vector<Node>& candidates,
                          std::vector<Node>& lemmas) override;
   /** Tries to build new candidate solutions with new enumerated expressions
diff --git a/src/theory/quantifiers/sygus/sygus_module.h b/src/theory/quantifiers/sygus/sygus_module.h
index 10c0104bc..ac3adb36a 100644
--- a/src/theory/quantifiers/sygus/sygus_module.h
+++ b/src/theory/quantifiers/sygus/sygus_module.h
@@ -57,16 +57,23 @@ class SygusModule
   virtual ~SygusModule() {}
   /** initialize
    *
+   * This function initializes the module for solving the given conjecture. This
+   * typically involves registering enumerators (for constructing terms) via
+   * calls to TermDbSygus::registerEnumerator.
+   *
+   * This function returns true if this module will take responsibility for
+   * constructing candidates for the given conjecture.
+   *
+   * conj is the synthesis conjecture (prior to deep-embedding).
+   *
    * n is the "base instantiation" of the deep-embedding version of the
    * synthesis conjecture under candidates (see SynthConjecture::d_base_inst).
    *
    * This function may add lemmas to the argument lemmas, which should be
    * sent out on the output channel of quantifiers by the caller.
-   *
-   * This function returns true if this module will take responsibility for
-   * constructing candidates for the given conjecture.
    */
-  virtual bool initialize(Node n,
+  virtual bool initialize(Node conj,
+                          Node n,
                           const std::vector<Node>& candidates,
                           std::vector<Node>& lemmas) = 0;
   /** get term list
diff --git a/src/theory/quantifiers/sygus/sygus_pbe.cpp b/src/theory/quantifiers/sygus/sygus_pbe.cpp
index 2ab51f1fb..c76082b02 100644
--- a/src/theory/quantifiers/sygus/sygus_pbe.cpp
+++ b/src/theory/quantifiers/sygus/sygus_pbe.cpp
@@ -144,7 +144,8 @@ bool SygusPbe::collectExamples(Node n,
   return true;
 }
 
-bool SygusPbe::initialize(Node n,
+bool SygusPbe::initialize(Node conj,
+                          Node n,
                           const std::vector<Node>& candidates,
                           std::vector<Node>& lemmas)
 {
diff --git a/src/theory/quantifiers/sygus/sygus_pbe.h b/src/theory/quantifiers/sygus/sygus_pbe.h
index e82ce01da..258fe017b 100644
--- a/src/theory/quantifiers/sygus/sygus_pbe.h
+++ b/src/theory/quantifiers/sygus/sygus_pbe.h
@@ -107,7 +107,8 @@ class SygusPbe : public SygusModule
   * of an enumerator is not ITE if it is being used to construct
   * return values for decision trees.
   */
-  bool initialize(Node n,
+  bool initialize(Node conj,
+                  Node n,
                   const std::vector<Node>& candidates,
                   std::vector<Node>& lemmas) override;
   /** get term list
diff --git a/src/theory/quantifiers/sygus/synth_conjecture.cpp b/src/theory/quantifiers/sygus/synth_conjecture.cpp
index aabc2f1f3..97e5a5338 100644
--- a/src/theory/quantifiers/sygus/synth_conjecture.cpp
+++ b/src/theory/quantifiers/sygus/synth_conjecture.cpp
@@ -191,7 +191,8 @@ void SynthConjecture::assign(Node q)
     d_ceg_proc->initialize(d_base_inst, d_candidates);
     for (unsigned i = 0, size = d_modules.size(); i < size; i++)
     {
-      if (d_modules[i]->initialize(d_base_inst, d_candidates, guarded_lemmas))
+      if (d_modules[i]->initialize(
+              d_simp_quant, d_base_inst, d_candidates, guarded_lemmas))
       {
         d_master = d_modules[i];
         break;