Pass synthesis conjecture to sygus modules (#3212)

diff --git a/src/theory/quantifiers/sygus/cegis.cpp b/src/theory/quantifiers/sygus/cegis.cpp
index 301d772bff52213dd43e2cd3252004cda6b2bda9..1e8012697e858f659a01ac5151cd3957ebd5f705 100644 (file)
--- 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 a295f6a40dc9d5603eb98de3cc9cccb759ef4a98..8913799926cd623313de9e75222a0f52a7896715 100644 (file)
--- 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 6e9467b7c67bec4357e47586f14cfa8496231105..399a9576c5def5e00098a780c7fd26dbdd740bbd 100644 (file)
--- 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 a2e7be1c1778c71231cecae56566e306eb10d642..ac859750fa97190fce8d946a6bc14f92549edc3e 100644 (file)
--- 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 10c0104bc66b5ce724512680acbcb4ab98aa3e14..ac3adb36a7b63ee439c10b846735f68a9921a92a 100644 (file)
--- a/src/theory/quantifiers/sygus/sygus_module.h
+++ b/src/theory/quantifiers/sygus/sygus_module.h
@@ -56,17 +56,24 @@ class SygusModule
   SygusModule(QuantifiersEngine* qe, SynthConjecture* p);
   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 2ab51f1fbd947807759e8ddf755a9a002e7166bc..c76082b024bde3ceeb0931456af2ecd459463867 100644 (file)
--- 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 e82ce01da3810103385b26e3c5fdf529b2832c07..258fe017b7baed3da4e92896b3372b4bcb889862 100644 (file)
--- 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 aabc2f1f3b255735a6505831a31a8853f385bdf2..97e5a53384a013e3a10216b83b68e0c42bc60ec6 100644 (file)
--- 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;