Pass synthesis conjecture to sygus modules (#3212)

1 files changed, 11 insertions, 4 deletions

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