Add option --sygus-rr-synth-rec for considering all grammar types recursively (#2270)

1 files changed, 22 insertions, 22 deletions

diff --git a/src/theory/quantifiers/sygus_sampler.cpp b/src/theory/quantifiers/sygus_sampler.cpp
index 8834fe751..27ca270cc 100644
--- a/src/theory/quantifiers/sygus_sampler.cpp
+++ b/src/theory/quantifiers/sygus_sampler.cpp
@@ -40,7 +40,6 @@ void SygusSampler::initialize(TypeNode tn,
   d_tds = nullptr;
   d_use_sygus_type = false;
   d_is_valid = true;
-  d_tn = tn;
   d_ftn = TypeNode::null();
   d_type_vars.clear();
   d_vars.clear();
@@ -95,7 +94,6 @@ void SygusSampler::initializeSygus(TermDbSygus* tds,
   Assert(d_ftn.isDatatype());
   const Datatype& dt = static_cast<DatatypeType>(d_ftn.toType()).getDatatype();
   Assert(dt.isSygus());
-  d_tn = TypeNode::fromType(dt.getSygusType());
 
   Trace("sygus-sample") << "Register sampler for " << f << std::endl;
 
@@ -264,28 +262,30 @@ bool SygusSampler::PtTrie::add(std::vector<Node>& pt)
 
 Node SygusSampler::registerTerm(Node n, bool forceKeep)
 {
-  if (d_is_valid)
+  if (!d_is_valid)
   {
-    Node bn = n;
-    // if this is a sygus type, get its builtin analog
-    if (d_use_sygus_type)
-    {
-      Assert(!d_ftn.isNull());
-      bn = d_tds->sygusToBuiltin(n);
-      Assert(d_builtin_to_sygus.find(bn) == d_builtin_to_sygus.end()
-             || d_builtin_to_sygus[bn] == n);
-      d_builtin_to_sygus[bn] = n;
-    }
-    Assert(bn.getType() == d_tn);
-    Node res = d_trie.add(bn, this, 0, d_samples.size(), forceKeep);
-    if (d_use_sygus_type)
-    {
-      Assert(d_builtin_to_sygus.find(res) != d_builtin_to_sygus.end());
-      res = res != bn ? d_builtin_to_sygus[res] : n;
-    }
-    return res;
+    // do nothing
+    return n;
+  }
+  Node bn = n;
+  TypeNode tn = n.getType();
+  // If we are using sygus types, get the builtin analog of n.
+  if (d_use_sygus_type)
+  {
+    bn = d_tds->sygusToBuiltin(n);
+    d_builtin_to_sygus[tn][bn] = n;
+  }
+  // cache based on the (original) type of n
+  Node res = d_trie[tn].add(bn, this, 0, d_samples.size(), forceKeep);
+  // If we are using sygus types, map back to an original.
+  // Notice that d_builtin_to_sygus is not necessarily bijective.
+  if (d_use_sygus_type)
+  {
+    std::map<Node, Node>& bts = d_builtin_to_sygus[tn];
+    Assert(bts.find(res) != bts.end());
+    res = res != bn ? bts[res] : n;
   }
-  return n;
+  return res;
 }
 
 bool SygusSampler::isContiguous(Node n)