1 files changed, 22 insertions, 7 deletions
diff --git a/src/theory/quantifiers/sygus_sampler.h b/src/theory/quantifiers/sygus_sampler.h
index 98f52992b..526a9e4b1 100644
--- a/src/theory/quantifiers/sygus_sampler.h
+++ b/src/theory/quantifiers/sygus_sampler.h
@@ -188,14 +188,15 @@ class SygusSampler : public LazyTrieEvaluator
   };
   /** a trie for samples */
   PtTrie d_samples_trie;
-  /** type of nodes we will be registering with this class */
-  TypeNode d_tn;
   /** the sygus type for this sampler (if applicable). */
   TypeNode d_ftn;
-  /** whether we are registering terms of type d_ftn */
+  /** whether we are registering terms of sygus types with this sampler */
   bool d_use_sygus_type;
-  /** map from builtin terms to the sygus term they correspond to */
-  std::map<Node, Node> d_builtin_to_sygus;
+  /**
+   * For each (sygus) type, a map from builtin terms to the sygus term they
+   * correspond to.
+   */
+  std::map<TypeNode, std::map<Node, Node> > d_builtin_to_sygus;
   /** all variables we are sampling values for */
   std::vector<Node> d_vars;
   /** type variables
@@ -229,8 +230,22 @@ class SygusSampler : public LazyTrieEvaluator
    * that type.
    */
   std::map<TypeNode, std::vector<Node> > d_type_consts;
-  /** the lazy trie */
-  LazyTrie d_trie;
+  /** a lazy trie for each type
+   *
+   * This stores the evaluation of all terms registered to this class.
+   *
+   * Notice if we are registering sygus terms with this class, then terms
+   * are grouped into this trie according to their sygus type, and not their
+   * builtin type. For example, for grammar:
+   *   A -> x | B+1
+   *   B -> x | 0 | 1 | B+B
+   * If we register C^B_+( C^B_x(), C^B_0() ) and C^A_x() with this class,
+   * then x+0 is registered to d_trie[B] and x is registered to d_trie[A],
+   * and no rewrite rule is reported. The reason for this is that otherwise
+   * we would end up reporting many useless rewrites since the same builtin
+   * term can be generated by multiple sygus types (e.g. C^B_x() and C^A_x()).
+   */
+  std::map<TypeNode, LazyTrie> d_trie;
   /** is this sampler valid?
    *
    * A sampler can be invalid if sample points cannot be generated for a type