Make sygus pbe use sygus unif utility (#1724)

1 files changed, 6 insertions, 16 deletions

diff --git a/src/theory/quantifiers/sygus/sygus_unif.h b/src/theory/quantifiers/sygus/sygus_unif.h
index 68ed442a8..d46fb9c86 100644
--- a/src/theory/quantifiers/sygus/sygus_unif.h
+++ b/src/theory/quantifiers/sygus/sygus_unif.h
@@ -339,7 +339,7 @@ class SygusUnif
   friend class UnifContext;
 
  public:
-  SygusUnif(QuantifiersEngine* qe);
+  SygusUnif();
   ~SygusUnif();
 
   /** initialize
@@ -356,7 +356,10 @@ class SygusUnif
    * those that exclude ITE from enumerators whose role is enum_io when the
    * strategy is ITE_strat).
    */
-  void initialize(Node f, std::vector<Node>& enums, std::vector<Node>& lemmas);
+  void initialize(QuantifiersEngine* qe,
+                  Node f,
+                  std::vector<Node>& enums,
+                  std::vector<Node>& lemmas);
   /** reset examples
    *
    * Reset the specification for f.
@@ -432,7 +435,7 @@ class SygusUnif
     * role is the "role" the enumerator plays in the high-level strategy,
     *   which is one of enum_* above.
     */
-    void initialize(Node c, EnumRole role);
+    void initialize(EnumRole role);
     /** is this enumerator associated with a template? */
     bool isTemplated() { return !d_template.isNull(); }
     /** set conditional
@@ -447,10 +450,6 @@ class SygusUnif
     bool isConditional() { return d_is_conditional; }
     /** get the role of this enumerator */
     EnumRole getRole() { return d_role; }
-    /**
-    * The candidate variable that this enumerator is for (see sygus_pbe.h).
-    */
-    Node d_parent_candidate;
     /** enumerator template
     *
     * If d_template non-null, enumerated values V are immediately transformed to
@@ -586,15 +585,6 @@ class SygusUnif
   std::map<Node, CandidateInfo> d_cinfo;
 
   //------------------------------ representation of an enumeration strategy
-  /** add enumerated value
-   *
-   * We have enumerated the value v for x. This function adds x->v to the
-   * relevant data structures that are used for strategy-specific construction
-   * of solutions when necessary, and returns a set of lemmas, which are added
-   * to the input argument lems. These lemmas are used to rule out models where
-   * x = v, to force that a new value is enumerated for x.
-   */
-  void addEnumeratedValue(Node x, Node v, std::vector<Node>& lems);
   /** domain-specific enumerator exclusion techniques
    *
    * Returns true if the value v for x can be excluded based on a