Print candidate rewrites in terms of original grammar (#1635)

3 files changed, 64 insertions, 20 deletions

diff --git a/src/theory/quantifiers/sygus/ce_guided_conjecture.cpp b/src/theory/quantifiers/sygus/ce_guided_conjecture.cpp
index f2a1c334c..ac0982c4e 100644
--- a/src/theory/quantifiers/sygus/ce_guided_conjecture.cpp
+++ b/src/theory/quantifiers/sygus/ce_guided_conjecture.cpp
@@ -620,29 +620,34 @@ void CegConjecture::printSynthSolution( std::ostream& out, bool singleInvocation
         if (its == d_sampler.end())
         {
           d_sampler[prog].initializeSygusExt(
-              d_qe, prog, options::sygusSamples());
+              d_qe, prog, options::sygusSamples(), true);
           its = d_sampler.find(prog);
         }
-        Node solb = sygusDb->sygusToBuiltin(sol, prog.getType());
-        Node eq_sol = its->second.registerTerm(solb);
+        Node eq_sol = its->second.registerTerm(sol);
         // eq_sol is a candidate solution that is equivalent to sol
-        if (eq_sol != solb)
+        if (eq_sol != sol)
         {
           ++(cei->d_statistics.d_candidate_rewrites);
           if (!eq_sol.isNull())
           {
-            // Terms solb and eq_sol are equivalent under sample points but do
-            // not rewrite to the same term. Hence, this indicates a candidate
-            // rewrite.
-            out << "(candidate-rewrite " << solb << " " << eq_sol << ")"
-                << std::endl;
+            // The analog of terms sol and eq_sol are equivalent under sample
+            // points but do not rewrite to the same term. Hence, this indicates
+            // a candidate rewrite.
+            Printer* p = Printer::getPrinter(options::outputLanguage());
+            out << "(candidate-rewrite ";
+            p->toStreamSygus(out, sol);
+            out << " ";
+            p->toStreamSygus(out, eq_sol);
+            out << ")" << std::endl;
             ++(cei->d_statistics.d_candidate_rewrites_print);
             // debugging information
             if (Trace.isOn("sygus-rr-debug"))
             {
               ExtendedRewriter* er = sygusDb->getExtRewriter();
+              Node solb = sygusDb->sygusToBuiltin(sol);
               Node solbr = er->extendedRewrite(solb);
-              Node eq_solr = er->extendedRewrite(eq_sol);
+              Node eq_solb = sygusDb->sygusToBuiltin(eq_sol);
+              Node eq_solr = er->extendedRewrite(eq_solb);
               Trace("sygus-rr-debug")
                   << "; candidate #1 ext-rewrites to: " << solbr << std::endl;
               Trace("sygus-rr-debug")
diff --git a/src/theory/quantifiers/sygus_sampler.cpp b/src/theory/quantifiers/sygus_sampler.cpp
index fa0478ac7..0b9254818 100644
--- a/src/theory/quantifiers/sygus_sampler.cpp
+++ b/src/theory/quantifiers/sygus_sampler.cpp
@@ -64,13 +64,17 @@ Node LazyTrie::add(Node n,
   return Node::null();
 }
 
-SygusSampler::SygusSampler() : d_tds(nullptr), d_is_valid(false) {}
+SygusSampler::SygusSampler()
+    : d_tds(nullptr), d_use_sygus_type(false), d_is_valid(false)
+{
+}
 
 void SygusSampler::initialize(TypeNode tn,
                               std::vector<Node>& vars,
                               unsigned nsamples)
 {
   d_tds = nullptr;
+  d_use_sygus_type = false;
   d_is_valid = true;
   d_tn = tn;
   d_ftn = TypeNode::null();
@@ -105,9 +109,13 @@ void SygusSampler::initialize(TypeNode tn,
   initializeSamples(nsamples);
 }
 
-void SygusSampler::initializeSygus(TermDbSygus* tds, Node f, unsigned nsamples)
+void SygusSampler::initializeSygus(TermDbSygus* tds,
+                                   Node f,
+                                   unsigned nsamples,
+                                   bool useSygusType)
 {
   d_tds = tds;
+  d_use_sygus_type = useSygusType;
   d_is_valid = true;
   d_ftn = f.getType();
   Assert(d_ftn.isDatatype());
@@ -282,8 +290,23 @@ Node SygusSampler::registerTerm(Node n, bool forceKeep)
 {
   if (d_is_valid)
   {
-    Assert(n.getType() == d_tn);
-    return d_trie.add(n, this, 0, d_samples.size(), forceKeep);
+    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);
+      bn = Rewriter::rewrite(bn);
+      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;
   }
   return n;
 }
@@ -645,9 +668,11 @@ void SygusSampler::registerSygusType(TypeNode tn)
 
 void SygusSamplerExt::initializeSygusExt(QuantifiersEngine* qe,
                                          Node f,
-                                         unsigned nsamples)
+                                         unsigned nsamples,
+                                         bool useSygusType)
 {
-  SygusSampler::initializeSygus(qe->getTermDatabaseSygus(), f, nsamples);
+  SygusSampler::initializeSygus(
+      qe->getTermDatabaseSygus(), f, nsamples, useSygusType);
 
   // initialize the dynamic rewriter
   std::stringstream ss;
diff --git a/src/theory/quantifiers/sygus_sampler.h b/src/theory/quantifiers/sygus_sampler.h
index abc9232af..5fcfc1c93 100644
--- a/src/theory/quantifiers/sygus_sampler.h
+++ b/src/theory/quantifiers/sygus_sampler.h
@@ -148,11 +148,18 @@ class SygusSampler : public LazyTrieEvaluator
   /** initialize sygus
    *
    * tds : pointer to sygus database,
-   * f : a term of some SyGuS datatype type whose (builtin) values we will be
+   * f : a term of some SyGuS datatype type whose values we will be
    * testing under the free variables in the grammar of f,
-   * nsamples : number of sample points this class will test.
+   * nsamples : number of sample points this class will test,
+   * useSygusType : whether we will register terms with this sampler that have
+   * the same type as f. If this flag is false, then we will be registering
+   * terms of the analog of the type of f, that is, the builtin type that
+   * f's type encodes in the deep embedding.
    */
-  void initializeSygus(TermDbSygus* tds, Node f, unsigned nsamples);
+  void initializeSygus(TermDbSygus* tds,
+                       Node f,
+                       unsigned nsamples,
+                       bool useSygusType);
   /** register term n with this sampler database
    *
    * forceKeep is whether we wish to force that n is chosen as a representative
@@ -222,6 +229,10 @@ class SygusSampler : public LazyTrieEvaluator
   TypeNode d_tn;
   /** the sygus type for this sampler (if applicable). */
   TypeNode d_ftn;
+  /** whether we are registering terms of type d_ftn */
+  bool d_use_sygus_type;
+  /** map from builtin terms to the sygus term they correspond to */
+  std::map<Node, Node> d_builtin_to_sygus;
   /** all variables we are sampling values for */
   std::vector<Node> d_vars;
   /** type variables
@@ -329,7 +340,10 @@ class SygusSamplerExt : public SygusSampler
 {
  public:
   /** initialize extended */
-  void initializeSygusExt(QuantifiersEngine* qe, Node f, unsigned nsamples);
+  void initializeSygusExt(QuantifiersEngine* qe,
+                          Node f,
+                          unsigned nsamples,
+                          bool useSygusType);
   /** register term n with this sampler database
    *
    * This returns either null, or a term ret with the same guarantees as