Minor improvements to sygus sampler (#1598)

7 files changed, 62 insertions, 23 deletions

diff --git a/src/theory/quantifiers/ce_guided_conjecture.cpp b/src/theory/quantifiers/ce_guided_conjecture.cpp
index b6ba792df..0ce9b7c72 100644
--- a/src/theory/quantifiers/ce_guided_conjecture.cpp
+++ b/src/theory/quantifiers/ce_guided_conjecture.cpp
@@ -623,7 +623,8 @@ void CegConjecture::printSynthSolution( std::ostream& out, bool singleInvocation
         Printer::getPrinter(options::outputLanguage())->toStreamSygus(out, sol);
       }
       out << ")" << std::endl;
-      ++(d_qe->getCegInstantiation()->d_statistics.d_solutions);
+      CegInstantiation* cei = d_qe->getCegInstantiation();
+      ++(cei->d_statistics.d_solutions);
 
       if (status != 0 && options::sygusRewSynth())
       {
@@ -640,22 +641,26 @@ void CegConjecture::printSynthSolution( std::ostream& out, bool singleInvocation
         // eq_sol is a candidate solution that is equivalent to sol
         if (eq_sol != solb)
         {
-          // 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;
-          ++(d_qe->getCegInstantiation()->d_statistics.d_candidate_rewrites);
-          // debugging information
-          if (Trace.isOn("sygus-rr-debug"))
+          ++(cei->d_statistics.d_candidate_rewrites);
+          if (!eq_sol.isNull())
           {
-            ExtendedRewriter* er = sygusDb->getExtRewriter();
-            Node solbr = er->extendedRewrite(solb);
-            Node eq_solr = er->extendedRewrite(eq_sol);
-            Trace("sygus-rr-debug")
-                << "; candidate #1 ext-rewrites to: " << solbr << std::endl;
-            Trace("sygus-rr-debug")
-                << "; candidate #2 ext-rewrites to: " << eq_solr << std::endl;
+            // 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;
+            ++(cei->d_statistics.d_candidate_rewrites_print);
+            // debugging information
+            if (Trace.isOn("sygus-rr-debug"))
+            {
+              ExtendedRewriter* er = sygusDb->getExtRewriter();
+              Node solbr = er->extendedRewrite(solb);
+              Node eq_solr = er->extendedRewrite(eq_sol);
+              Trace("sygus-rr-debug")
+                  << "; candidate #1 ext-rewrites to: " << solbr << std::endl;
+              Trace("sygus-rr-debug")
+                  << "; candidate #2 ext-rewrites to: " << eq_solr << std::endl;
+            }
           }
         }
       }
diff --git a/src/theory/quantifiers/ce_guided_instantiation.cpp b/src/theory/quantifiers/ce_guided_instantiation.cpp
index fbafb8b8c..ea2a2d13a 100644
--- a/src/theory/quantifiers/ce_guided_instantiation.cpp
+++ b/src/theory/quantifiers/ce_guided_instantiation.cpp
@@ -362,6 +362,7 @@ CegInstantiation::Statistics::Statistics()
       d_cegqi_lemmas_refine("CegInstantiation::cegqi_lemmas_refine", 0),
       d_cegqi_si_lemmas("CegInstantiation::cegqi_lemmas_si", 0),
       d_solutions("CegConjecture::solutions", 0),
+      d_candidate_rewrites_print("CegConjecture::candidate_rewrites_print", 0),
       d_candidate_rewrites("CegConjecture::candidate_rewrites", 0)
 
 {
@@ -369,6 +370,7 @@ CegInstantiation::Statistics::Statistics()
   smtStatisticsRegistry()->registerStat(&d_cegqi_lemmas_refine);
   smtStatisticsRegistry()->registerStat(&d_cegqi_si_lemmas);
   smtStatisticsRegistry()->registerStat(&d_solutions);
+  smtStatisticsRegistry()->registerStat(&d_candidate_rewrites_print);
   smtStatisticsRegistry()->registerStat(&d_candidate_rewrites);
 }
 
@@ -377,6 +379,7 @@ CegInstantiation::Statistics::~Statistics(){
   smtStatisticsRegistry()->unregisterStat(&d_cegqi_lemmas_refine);
   smtStatisticsRegistry()->unregisterStat(&d_cegqi_si_lemmas);
   smtStatisticsRegistry()->unregisterStat(&d_solutions);
+  smtStatisticsRegistry()->unregisterStat(&d_candidate_rewrites_print);
   smtStatisticsRegistry()->unregisterStat(&d_candidate_rewrites);
 }
 
diff --git a/src/theory/quantifiers/ce_guided_instantiation.h b/src/theory/quantifiers/ce_guided_instantiation.h
index 644e5b3ef..2dc74dc72 100644
--- a/src/theory/quantifiers/ce_guided_instantiation.h
+++ b/src/theory/quantifiers/ce_guided_instantiation.h
@@ -75,6 +75,7 @@ public:
     IntStat d_cegqi_lemmas_refine;
     IntStat d_cegqi_si_lemmas;
     IntStat d_solutions;
+    IntStat d_candidate_rewrites_print;
     IntStat d_candidate_rewrites;
     Statistics();
     ~Statistics();
diff --git a/src/theory/quantifiers/dynamic_rewrite.cpp b/src/theory/quantifiers/dynamic_rewrite.cpp
index a19695770..3462a4d10 100644
--- a/src/theory/quantifiers/dynamic_rewrite.cpp
+++ b/src/theory/quantifiers/dynamic_rewrite.cpp
@@ -25,7 +25,8 @@ namespace quantifiers {
 
 DynamicRewriter::DynamicRewriter(const std::string& name, QuantifiersEngine* qe)
     : d_qe(qe),
-      d_equalityEngine(qe->getUserContext(), "DynamicRewriter::" + name, true)
+      d_equalityEngine(qe->getUserContext(), "DynamicRewriter::" + name, true),
+      d_rewrites(qe->getUserContext())
 {
   d_equalityEngine.addFunctionKind(kind::APPLY_UF);
 }
@@ -42,20 +43,26 @@ bool DynamicRewriter::addRewrite(Node a, Node b)
   // add to the equality engine
   Node ai = toInternal(a);
   Node bi = toInternal(b);
+  Trace("dyn-rewrite-debug") << "Internal : " << ai << " " << bi << std::endl;
   d_equalityEngine.addTerm(ai);
   d_equalityEngine.addTerm(bi);
 
+  Trace("dyn-rewrite-debug") << "get reps..." << std::endl;
   // may already be equal by congruence
   Node air = d_equalityEngine.getRepresentative(ai);
   Node bir = d_equalityEngine.getRepresentative(bi);
+  Trace("dyn-rewrite-debug") << "Reps : " << air << " " << bir << std::endl;
   if (air == bir)
   {
     Trace("dyn-rewrite") << "...fail, congruent." << std::endl;
     return false;
   }
 
+  Trace("dyn-rewrite-debug") << "assert eq..." << std::endl;
   Node eq = ai.eqNode(bi);
+  d_rewrites.push_back(eq);
   d_equalityEngine.assertEquality(eq, true, eq);
+  Trace("dyn-rewrite-debug") << "Finished" << std::endl;
   return true;
 }
 
diff --git a/src/theory/quantifiers/dynamic_rewrite.h b/src/theory/quantifiers/dynamic_rewrite.h
index be2ff4c78..2b5464151 100644
--- a/src/theory/quantifiers/dynamic_rewrite.h
+++ b/src/theory/quantifiers/dynamic_rewrite.h
@@ -19,6 +19,7 @@
 
 #include <map>
 
+#include "context/cdlist.h"
 #include "theory/quantifiers_engine.h"
 #include "theory/uf/equality_engine.h"
 
@@ -51,6 +52,8 @@ namespace quantifiers {
  */
 class DynamicRewriter
 {
+  typedef context::CDList<Node> NodeList;
+
  public:
   DynamicRewriter(const std::string& name, QuantifiersEngine* qe);
   ~DynamicRewriter() {}
@@ -105,6 +108,8 @@ class DynamicRewriter
   std::map<Node, Node> d_term_to_internal;
   /** stores congruence closure over terms given to this class. */
   eq::EqualityEngine d_equalityEngine;
+  /** list of all equalities asserted to equality engine */
+  NodeList d_rewrites;
 };
 
 } /* CVC4::theory::quantifiers namespace */
diff --git a/src/theory/quantifiers/sygus_sampler.cpp b/src/theory/quantifiers/sygus_sampler.cpp
index 757b8e44f..aa0a4b778 100644
--- a/src/theory/quantifiers/sygus_sampler.cpp
+++ b/src/theory/quantifiers/sygus_sampler.cpp
@@ -430,6 +430,7 @@ Node SygusSampler::evaluate(Node n, unsigned index)
   // just a substitution
   std::vector<Node>& pt = d_samples[index];
   Node ev = n.substitute(d_vars.begin(), d_vars.end(), pt.begin(), pt.end());
+  Trace("sygus-sample-ev-debug") << "Rewrite : " << ev << std::endl;
   ev = Rewriter::rewrite(ev);
   Trace("sygus-sample-ev") << "( " << n << ", " << index << " ) -> " << ev
                            << std::endl;
@@ -656,6 +657,8 @@ void SygusSamplerExt::initializeSygusExt(QuantifiersEngine* qe,
 Node SygusSamplerExt::registerTerm(Node n, bool forceKeep)
 {
   Node eq_n = SygusSampler::registerTerm(n, forceKeep);
+  Trace("sygus-synth-rr") << "sygusSampleExt : " << n << "..." << eq_n
+                          << std::endl;
   if (eq_n == n)
   {
     return n;
@@ -678,9 +681,11 @@ Node SygusSamplerExt::registerTerm(Node n, bool forceKeep)
       isUnique = containsFreeVariables(eq_n, n);
     }
   }
+  Trace("sygus-synth-rr-debug") << "AlphaEq unique: " << isUnique << std::endl;
   bool rewRedundant = false;
   if (d_drewrite != nullptr)
   {
+    Trace("sygus-synth-rr-debug") << "Add rewrite..." << std::endl;
     if (!d_drewrite->addRewrite(n, eq_n))
     {
       rewRedundant = isUnique;
@@ -688,6 +693,7 @@ Node SygusSamplerExt::registerTerm(Node n, bool forceKeep)
       isUnique = false;
     }
   }
+  Trace("sygus-synth-rr-debug") << "Rewrite unique: " << isUnique << std::endl;
 
   if (isUnique)
   {
@@ -709,7 +715,7 @@ Node SygusSamplerExt::registerTerm(Node n, bool forceKeep)
     }
     Trace("sygus-synth-rr") << std::endl;
   }
-  return n;
+  return Node::null();
 }
 
 } /* CVC4::theory::quantifiers namespace */
diff --git a/src/theory/quantifiers/sygus_sampler.h b/src/theory/quantifiers/sygus_sampler.h
index 48ddddbc6..60c2af22a 100644
--- a/src/theory/quantifiers/sygus_sampler.h
+++ b/src/theory/quantifiers/sygus_sampler.h
@@ -332,13 +332,25 @@ class SygusSamplerExt : public SygusSampler
   void initializeSygusExt(QuantifiersEngine* qe, Node f, unsigned nsamples);
   /** register term n with this sampler database
    *
-   * This returns a term ret with the same guarantees as
-   * SygusSampler::registerTerm, with the additional guarantee
+   * This returns either null, or a term ret with the same guarantees as
+   * SygusSampler::registerTerm with the additional guarantee
    * that for all ret' returned by a previous call to registerTerm( n' ),
-   * we have that ret = n is not alpha-equivalent to ret' = n,
-   * modulo symmetry of equality. For example,
+   * we have that n = ret is not alpha-equivalent to n' = ret'
+   * modulo symmetry of equality, nor is n = ret derivable from the set of
+   * all previous input/output pairs based on the d_drewrite utility.
+   * For example,
    *   (t+0), t and (s+0), s
-   * will not be input/output pairs of this function.
+   * will not both be input/output pairs of this function since t+0=t is
+   * alpha-equivalent to s+0=s.
+   *   s, t and s+0, t+0
+   * will not both be input/output pairs of this function since s+0=t+0 is
+   * derivable from s=t.
+   *
+   * If this function returns null, then n is equivalent to a previously
+   * registered term ret, and the equality n = ret is either alpha-equivalent
+   * to a previous input/output pair n' = ret', or n = ret is derivable
+   * from the set of all previous input/output pairs based on the
+   * d_drewrite utility.
    */
   virtual Node registerTerm(Node n, bool forceKeep = false) override;