Fix symmetry breaking for multiple sygus types (#3775)

3 files changed, 9 insertions, 5 deletions

diff --git a/src/theory/quantifiers/sygus/example_eval_cache.cpp b/src/theory/quantifiers/sygus/example_eval_cache.cpp
index 2a43335d7..ee5394972 100644
--- a/src/theory/quantifiers/sygus/example_eval_cache.cpp
+++ b/src/theory/quantifiers/sygus/example_eval_cache.cpp
@@ -43,7 +43,7 @@ ExampleEvalCache::ExampleEvalCache(TermDbSygus* tds,
 
 ExampleEvalCache::~ExampleEvalCache() {}
 
-Node ExampleEvalCache::addSearchVal(Node bv)
+Node ExampleEvalCache::addSearchVal(TypeNode tn, Node bv)
 {
   if (!d_indexSearchVals)
   {
@@ -53,7 +53,7 @@ Node ExampleEvalCache::addSearchVal(Node bv)
   std::vector<Node> vals;
   evaluateVec(bv, vals, true);
   Trace("sygus-pbe-debug") << "Add to trie..." << std::endl;
-  Node ret = d_trie.addOrGetTerm(bv, vals);
+  Node ret = d_trie[tn].addOrGetTerm(bv, vals);
   Trace("sygus-pbe-debug") << "...got " << ret << std::endl;
   // Only save the cache data if necessary: if the enumerated term
   // is redundant, its cached data will not be used later and thus should
diff --git a/src/theory/quantifiers/sygus/example_eval_cache.h b/src/theory/quantifiers/sygus/example_eval_cache.h
index 6aa78851f..6c5a65e7f 100644
--- a/src/theory/quantifiers/sygus/example_eval_cache.h
+++ b/src/theory/quantifiers/sygus/example_eval_cache.h
@@ -81,6 +81,10 @@ class ExampleEvalCache
    * procedure for SyGuS datatypes or the SyGuS fast enumerator when we are
    * considering a value of enumerator e passed to the constructor of this
    * class whose analog in the signature of builtin theory is bvr.
+   * 
+   * The type tn passed to this function is the sygus type of the term whose
+   * builtin equivalent is bvr. Terms with distinct types must be cached
+   * independently since two sygus types may not generate the same terms.
    *
    * This returns either:
    * - A term that is equivalent to bvr up to examples that was passed as the
@@ -94,7 +98,7 @@ class ExampleEvalCache
    * result of the evaluation of bvr is cached by this class, and can be
    * later accessed by evaluateVec below.
    */
-  Node addSearchVal(Node bvr);
+  Node addSearchVal(TypeNode tn, Node bvr);
   //----------------------------------- evaluating terms
   /** Evaluate vector
    *
@@ -149,7 +153,7 @@ class ExampleEvalCache
    * This is used for symmetry breaking in quantifier-free reasoning
    * about SyGuS datatypes.
    */
-  NodeTrie d_trie;
+  std::map< TypeNode, NodeTrie> d_trie;
   /** cache for evaluate */
   std::map<Node, std::vector<Node>> d_exOutCache;
 };
diff --git a/src/theory/quantifiers/sygus/sygus_enumerator.cpp b/src/theory/quantifiers/sygus/sygus_enumerator.cpp
index 551a9d225..3923361b1 100644
--- a/src/theory/quantifiers/sygus/sygus_enumerator.cpp
+++ b/src/theory/quantifiers/sygus/sygus_enumerator.cpp
@@ -346,7 +346,7 @@ bool SygusEnumerator::TermCache::addTerm(Node n)
     {
       ++(d_stats->d_enumTermsExampleEval);
       // Is it equivalent under examples?
-      Node bne = d_eec->addSearchVal(bnr);
+      Node bne = d_eec->addSearchVal(d_tn, bnr);
       if (!bne.isNull())
       {
         if (bnr != bne)