Simplify sygus unif so that it is one-to-one with functions to synthesize (#1726)

1 files changed, 26 insertions, 24 deletions

diff --git a/src/theory/quantifiers/sygus/sygus_unif.h b/src/theory/quantifiers/sygus/sygus_unif.h
index d46fb9c86..518a730a5 100644
--- a/src/theory/quantifiers/sygus/sygus_unif.h
+++ b/src/theory/quantifiers/sygus/sygus_unif.h
@@ -101,8 +101,11 @@ class UnifContext
 {
  public:
   UnifContext();
-  /** this intiializes this context for function-to-synthesize c */
-  void initialize(SygusUnif* pbe, Node c);
+  /**
+   * This intiializes this context based on information in pbe regarding the
+   * kinds of examples it contains.
+   */
+  void initialize(SygusUnif* pbe);
 
   //----------for ITE strategy
   /** the value of the context conditional
@@ -408,9 +411,9 @@ class SygusUnif
   Node d_true;
   Node d_false;
   /** input of I/O examples */
-  std::map<Node, std::vector<std::vector<Node> > > d_examples;
+  std::vector<std::vector<Node> > d_examples;
   /** output of I/O examples */
-  std::map<Node, std::vector<Node> > d_examples_out;
+  std::vector<Node> d_examples_out;
 
   //------------------------------ representation of a enumeration strategy
   /**
@@ -582,7 +585,7 @@ class SygusUnif
   /** the candidate for this class */
   Node d_candidate;
   /** maps a function-to-synthesize to the above information */
-  std::map<Node, CandidateInfo> d_cinfo;
+  CandidateInfo d_cinfo;
 
   //------------------------------ representation of an enumeration strategy
   /** domain-specific enumerator exclusion techniques
@@ -590,14 +593,12 @@ class SygusUnif
    * Returns true if the value v for x can be excluded based on a
    * domain-specific exclusion technique like the ones below.
    *
-   * c : the candidate variable that x is enumerating for,
-   * results : the values of v under the input examples of c,
+   * results : the values of v under the input examples,
    * ei : the enumerator information for x,
    * exp : if this function returns true, then exp contains a (possibly
    * generalize) explanation for why v can be excluded.
    */
-  bool getExplanationForEnumeratorExclude(Node c,
-                                          Node x,
+  bool getExplanationForEnumeratorExclude(Node x,
                                           Node v,
                                           std::vector<Node>& results,
                                           EnumInfo& ei,
@@ -622,21 +623,23 @@ class SygusUnif
   /** collect enumerator types
    *
    * This builds the strategy for enumerated values of type tn for the given
-   * role of nrole, for solutions to function-to-synthesize c.
+   * role of nrole, for solutions to function-to-synthesize of this class.
    */
-  void collectEnumeratorTypes(Node c, TypeNode tn, NodeRole nrole);
+  void collectEnumeratorTypes(TypeNode tn, NodeRole nrole);
   /** register enumerator
    *
-   * This registers that et is an enumerator for function-to-synthesize c
-   * of type tn, having enumerator role enum_role.
+   * This registers that et is an enumerator of type tn, having enumerator
+   * role enum_role.
    *
    * inSearch is whether we will enumerate values based on this enumerator.
    * A strategy node is represented by a (enumerator, node role) pair. Hence,
    * we may use enumerators for which this flag is false to represent strategy
    * nodes that have child strategies.
    */
-  void registerEnumerator(
-      Node et, Node c, TypeNode tn, EnumRole enum_role, bool inSearch);
+  void registerEnumerator(Node et,
+                          TypeNode tn,
+                          EnumRole enum_role,
+                          bool inSearch);
   /** infer template */
   bool inferTemplate(unsigned k,
                      Node n,
@@ -645,9 +648,10 @@ class SygusUnif
   /** static learn redundant operators
    *
    * This learns static lemmas for pruning enumerative space based on the
-   * strategy for the function-to-synthesize c, and stores these into lemmas.
+   * strategy for the function-to-synthesize of this class, and stores these
+   * into lemmas.
    */
-  void staticLearnRedundantOps(Node c, std::vector<Node>& lemmas);
+  void staticLearnRedundantOps(std::vector<Node>& lemmas);
   /** helper for static learn redundant operators
    *
    * (e, nrole) specify the strategy node in the graph we are currently
@@ -662,7 +666,6 @@ class SygusUnif
    * conditional of an strat_ITE strategy).
    */
   void staticLearnRedundantOps(
-      Node c,
       Node e,
       NodeRole nrole,
       std::map<Node, std::map<NodeRole, bool> >& visited,
@@ -673,13 +676,12 @@ class SygusUnif
 
   /** helper function for construct solution.
    *
-   * Construct a solution based on enumerator e for function-to-synthesize c
-   * with node role nrole in context x.
+   * Construct a solution based on enumerator e for function-to-synthesize of
+   * this class with node role nrole in context x.
    *
    * ind is the term depth of the context (for debugging).
    */
-  Node constructSolution(
-      Node c, Node e, NodeRole nrole, UnifContext& x, int ind);
+  Node constructSolution(Node e, NodeRole nrole, UnifContext& x, int ind);
   /** Heuristically choose the best solved term from solved in context x,
    * currently return the first. */
   Node constructBestSolvedTerm(std::vector<Node>& solved, UnifContext& x);
@@ -712,9 +714,9 @@ class SygusUnif
    * class, we may make recursive calls to the children of the strategy,
    * given in d_cenum. If all recursive calls to constructSolution for these
    * children are successful, say:
-   *   constructSolution( c, d_cenum[1], ... ) = t1,
+   *   constructSolution( d_cenum[1], ... ) = t1,
    *    ...,
-   *   constructSolution( c, d_cenum[n], ... ) = tn,
+   *   constructSolution( d_cenum[n], ... ) = tn,
    * Then, the solution returned by this strategy is
    *   d_sol_templ * { d_sol_templ_args -> (t1,...,tn) }
    * where * is application of substitution.