Fix for sampler. (#1639)

diff --git a/src/theory/quantifiers/sygus_sampler.cpp b/src/theory/quantifiers/sygus_sampler.cpp
index 0b9254818245b433ffd8fb71941d03c78549d31a..65883502fcccd3047f4b3dc0b8a77fc8ae66a81c 100644 (file)
--- a/src/theory/quantifiers/sygus_sampler.cpp
+++ b/src/theory/quantifiers/sygus_sampler.cpp
@@ -303,7 +303,7 @@ Node SygusSampler::registerTerm(Node n, bool forceKeep)
     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());
+      Assert(d_builtin_to_sygus.find(res) != d_builtin_to_sygus.end());
       res = res != bn ? d_builtin_to_sygus[res] : n;
     }
     return res;
@@ -690,9 +690,16 @@ Node SygusSamplerExt::registerTerm(Node n, bool forceKeep)
   {
     return n;
   }
+  Node bn = n;
+  Node beq_n = eq_n;
+  if (d_use_sygus_type)
+  {
+    bn = d_tds->sygusToBuiltin(n);
+    beq_n = d_tds->sygusToBuiltin(eq_n);
+  }
   // one of eq_n or n must be ordered
-  bool eqor = isOrdered(eq_n);
-  bool nor = isOrdered(n);
+  bool eqor = isOrdered(beq_n);
+  bool nor = isOrdered(bn);
   Trace("sygus-synth-rr-debug")
       << "Ordered? : " << nor << " " << eqor << std::endl;
   bool isUnique = false;
@@ -703,11 +710,11 @@ Node SygusSamplerExt::registerTerm(Node n, bool forceKeep)
     // free variables of the other
     if (!eqor)
     {
-      isUnique = containsFreeVariables(n, eq_n);
+      isUnique = containsFreeVariables(bn, beq_n);
     }
     else if (!nor)
     {
-      isUnique = containsFreeVariables(eq_n, n);
+      isUnique = containsFreeVariables(beq_n, bn);
     }
   }
   Trace("sygus-synth-rr-debug") << "AlphaEq unique: " << isUnique << std::endl;
@@ -715,7 +722,7 @@ Node SygusSamplerExt::registerTerm(Node n, bool forceKeep)
   if (d_drewrite != nullptr)
   {
     Trace("sygus-synth-rr-debug") << "Add rewrite..." << std::endl;
-    if (!d_drewrite->addRewrite(n, eq_n))
+    if (!d_drewrite->addRewrite(bn, beq_n))
     {
       rewRedundant = isUnique;
       // must be unique according to the dynamic rewriter
@@ -731,7 +738,7 @@ Node SygusSamplerExt::registerTerm(Node n, bool forceKeep)
     // sampler database.
     if (!eqor)
     {
-      registerTerm(n, true);
+      SygusSampler::registerTerm(n, true);
     }
     return eq_n;
   }

diff --git a/src/theory/quantifiers/sygus_sampler.h b/src/theory/quantifiers/sygus_sampler.h
index 5fcfc1c93052ea35d3d61e3b30bc128311f999c2..06576d6cefc1453b578bad679ee98bb26aa9d9f7 100644 (file)
--- a/src/theory/quantifiers/sygus_sampler.h
+++ b/src/theory/quantifiers/sygus_sampler.h
@@ -207,7 +207,8 @@ class SygusSampler : public LazyTrieEvaluator
    * are those that occur in the range d_type_vars.
    */
   bool containsFreeVariables(Node a, Node b);
- private:
+
+ protected:
   /** sygus term database of d_qe */
   TermDbSygus* d_tds;
   /** samples */