1 files changed, 63 insertions, 0 deletions
diff --git a/src/theory/quantifiers/ce_guided_conjecture.cpp b/src/theory/quantifiers/ce_guided_conjecture.cpp
index 378b26eef..74d5cef47 100644
--- a/src/theory/quantifiers/ce_guided_conjecture.cpp
+++ b/src/theory/quantifiers/ce_guided_conjecture.cpp
@@ -435,6 +435,12 @@ void CegConjecture::getModelValues( std::vector< Node >& n, std::vector< Node >&
       std::stringstream ss;
       Printer::getPrinter(options::outputLanguage())->toStreamSygus(ss, nv);
       Trace("cegqi-engine") << ss.str() << " ";
+      if (Trace.isOn("cegqi-engine-rr"))
+      {
+        Node bv = d_qe->getTermDatabaseSygus()->sygusToBuiltin(nv, tn);
+        bv = Rewriter::rewrite(bv);
+        Trace("cegqi-engine-rr") << " -> " << bv << std::endl;
+      }
     }
     Assert( !nv.isNull() );
   }
@@ -628,6 +634,63 @@ void CegConjecture::printSynthSolution( std::ostream& out, bool singleInvocation
         Printer::getPrinter(options::outputLanguage())->toStreamSygus(out, sol);
       }
       out << ")" << std::endl;
+
+      if (status != 0 && options::sygusRewSynth())
+      {
+        TermDbSygus* sygusDb = d_qe->getTermDatabaseSygus();
+        std::map<Node, SygusSampler>::iterator its = d_sampler.find(prog);
+        if (its == d_sampler.end())
+        {
+          d_sampler[prog].initialize(sygusDb, prog, options::sygusSamples());
+          its = d_sampler.find(prog);
+        }
+        Node solb = sygusDb->sygusToBuiltin(sol, prog.getType());
+        Node eq_sol = its->second.registerTerm(solb);
+        // eq_sol is a candidate solution that is equivalent to sol
+        if (eq_sol != solb)
+        {
+          // one of eq_sol or solb must be ordered
+          bool eqor = its->second.isOrdered(eq_sol);
+          bool sor = its->second.isOrdered(solb);
+          bool outputRewrite = false;
+          if (eqor || sor)
+          {
+            outputRewrite = true;
+            // if only one is ordered, then the ordered one must contain the
+            // free variables of the other
+            if (!eqor)
+            {
+              outputRewrite = its->second.containsFreeVariables(solb, eq_sol);
+            }
+            else if (!sor)
+            {
+              outputRewrite = its->second.containsFreeVariables(eq_sol, solb);
+            }
+          }
+
+          if (outputRewrite)
+          {
+            // 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;
+            // if the previous value stored was unordered, but this is
+            // ordered, we prefer this one. Thus, we force its addition to the
+            // sampler database.
+            if (!eqor)
+            {
+              its->second.registerTerm(solb, true);
+            }
+          }
+          else
+          {
+            Trace("sygus-synth-rr")
+                << "Alpha equivalent candidate rewrite : " << eq_sol << " "
+                << solb << std::endl;
+          }
+        }
+      }
     }
   }
 }