Improve accuracy of stats for sygus sampler (#1755)

6 files changed, 110 insertions, 65 deletions

diff --git a/src/smt/smt_engine.cpp b/src/smt/smt_engine.cpp
index dd8a2e502..029fb84c9 100644
--- a/src/smt/smt_engine.cpp
+++ b/src/smt/smt_engine.cpp
@@ -1481,8 +1481,11 @@ void SmtEngine::setDefaults() {
     options::boolToBitvector.set(false);
   }
 
-  if(options::produceAssignments() && !options::produceModels()) {
-    Notice() << "SmtEngine: turning on produce-models to support produce-assignments" << endl;
+  // cases where we need produce models
+  if (!options::produceModels()
+      && (options::produceAssignments() || options::sygusRewSynthCheck()))
+  {
+    Notice() << "SmtEngine: turning on produce-models" << endl;
     setOption("produce-models", SExpr("true"));
   }
 
diff --git a/src/theory/quantifiers/dynamic_rewrite.cpp b/src/theory/quantifiers/dynamic_rewrite.cpp
index cb7379910..00e527aba 100644
--- a/src/theory/quantifiers/dynamic_rewrite.cpp
+++ b/src/theory/quantifiers/dynamic_rewrite.cpp
@@ -31,39 +31,26 @@ DynamicRewriter::DynamicRewriter(const std::string& name, QuantifiersEngine* qe)
   d_equalityEngine.addFunctionKind(kind::APPLY_UF);
 }
 
-bool DynamicRewriter::addRewrite(Node a, Node b)
+void DynamicRewriter::addRewrite(Node a, Node b)
 {
   Trace("dyn-rewrite") << "Dyn-Rewriter : " << a << " == " << b << std::endl;
   if (a == b)
   {
-    Trace("dyn-rewrite") << "...fail, equal." << std::endl;
-    return false;
+    Trace("dyn-rewrite") << "...equal." << std::endl;
+    return;
   }
 
   // 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);
+  Assert(d_equalityEngine.consistent());
   Trace("dyn-rewrite-debug") << "Finished" << std::endl;
-  return true;
 }
 
 bool DynamicRewriter::areEqual(Node a, Node b)
diff --git a/src/theory/quantifiers/dynamic_rewrite.h b/src/theory/quantifiers/dynamic_rewrite.h
index 388173829..56f591470 100644
--- a/src/theory/quantifiers/dynamic_rewrite.h
+++ b/src/theory/quantifiers/dynamic_rewrite.h
@@ -57,12 +57,8 @@ class DynamicRewriter
  public:
   DynamicRewriter(const std::string& name, QuantifiersEngine* qe);
   ~DynamicRewriter() {}
-  /** inform this class that the equality a = b holds.
-   *
-   * This function returns true if this class did not already know that
-   * a = b based on the previous equalities it has seen.
-   */
-  bool addRewrite(Node a, Node b);
+  /** inform this class that the equality a = b holds. */
+  void addRewrite(Node a, Node b);
   /**
    * Check whether this class knows that the equality a = b holds.
    */
diff --git a/src/theory/quantifiers/sygus/ce_guided_conjecture.cpp b/src/theory/quantifiers/sygus/ce_guided_conjecture.cpp
index 98855a7ca..046c5724e 100644
--- a/src/theory/quantifiers/sygus/ce_guided_conjecture.cpp
+++ b/src/theory/quantifiers/sygus/ce_guided_conjecture.cpp
@@ -582,22 +582,11 @@ void CegConjecture::printSynthSolution( std::ostream& out, bool singleInvocation
       ss << prog;
       std::string f(ss.str());
       f.erase(f.begin());
-      out << "(define-fun " << f << " ";
-      if( dt.getSygusVarList().isNull() ){
-        out << "() ";
-      }else{
-        out << dt.getSygusVarList() << " ";
-      }
-      out << dt.getSygusType() << " ";
-      if( status==0 ){
-        out << sol;
-      }else{
-        Printer::getPrinter(options::outputLanguage())->toStreamSygus(out, sol);
-      }
-      out << ")" << std::endl;
       CegInstantiation* cei = d_qe->getCegInstantiation();
       ++(cei->d_statistics.d_solutions);
 
+      bool is_unique_term = true;
+
       if (status != 0 && options::sygusRewSynth())
       {
         TermDbSygus* sygusDb = d_qe->getTermDatabaseSygus();
@@ -612,9 +601,10 @@ void CegConjecture::printSynthSolution( std::ostream& out, bool singleInvocation
         // eq_sol is a candidate solution that is equivalent to sol
         if (eq_sol != sol)
         {
-          ++(cei->d_statistics.d_candidate_rewrites);
+          is_unique_term = false;
           // if eq_sol is null, then we have an uninteresting candidate rewrite,
           // e.g. one that is alpha-equivalent to another.
+          bool success = true;
           if (!eq_sol.isNull())
           {
             ExtendedRewriter* er = sygusDb->getExtRewriter();
@@ -622,12 +612,11 @@ void CegConjecture::printSynthSolution( std::ostream& out, bool singleInvocation
             Node solbr = er->extendedRewrite(solb);
             Node eq_solb = sygusDb->sygusToBuiltin(eq_sol);
             Node eq_solr = er->extendedRewrite(eq_solb);
-            bool success = true;
             bool verified = false;
+            Trace("rr-check") << "Check candidate rewrite..." << std::endl;
             // verify it if applicable
             if (options::sygusRewSynthCheck())
             {
-              Trace("rr-check") << "Check candidate rewrite..." << std::endl;
               // Notice we don't set produce-models. rrChecker takes the same
               // options as the SmtEngine we belong to, where we ensure that
               // produce-models is set.
@@ -645,6 +634,7 @@ void CegConjecture::printSynthSolution( std::ostream& out, bool singleInvocation
                 Trace("rr-check")
                     << "...rewrite does not hold for: " << std::endl;
                 success = false;
+                is_unique_term = true;
                 std::vector<Node> vars;
                 d_sampler[prog].getVariables(vars);
                 std::vector<Node> pt;
@@ -665,11 +655,18 @@ void CegConjecture::printSynthSolution( std::ostream& out, bool singleInvocation
                 verified = true;
               }
             }
+            else
+            {
+              // just insist that constants are not relevant pairs
+              success = !solb.isConst() || !eq_solb.isConst();
+            }
             if (success)
             {
-              // 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.
+              // register this as a relevant pair (helps filtering)
+              d_sampler[prog].registerRelevantPair(sol, eq_sol);
+              // 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 << "(" << (verified ? "" : "candidate-") << "rewrite ";
               p->toStreamSygus(out, sol);
@@ -711,7 +708,35 @@ void CegConjecture::printSynthSolution( std::ostream& out, bool singleInvocation
               }
             }
           }
+          // we count this as a rewrite if we did not explicitly rule it out
+          if (success)
+          {
+            ++(cei->d_statistics.d_candidate_rewrites);
+          }
+        }
+      }
+      if (is_unique_term)
+      {
+        out << "(define-fun " << f << " ";
+        if (dt.getSygusVarList().isNull())
+        {
+          out << "() ";
+        }
+        else
+        {
+          out << dt.getSygusVarList() << " ";
+        }
+        out << dt.getSygusType() << " ";
+        if (status == 0)
+        {
+          out << sol;
+        }
+        else
+        {
+          Printer::getPrinter(options::outputLanguage())
+              ->toStreamSygus(out, sol);
         }
+        out << ")" << std::endl;
       }
     }
   }
diff --git a/src/theory/quantifiers/sygus_sampler.cpp b/src/theory/quantifiers/sygus_sampler.cpp
index f9ae0b553..f15c1199c 100644
--- a/src/theory/quantifiers/sygus_sampler.cpp
+++ b/src/theory/quantifiers/sygus_sampler.cpp
@@ -14,7 +14,9 @@
 
 #include "theory/quantifiers/sygus_sampler.h"
 
+#include "options/base_options.h"
 #include "options/quantifiers_options.h"
+#include "printer/printer.h"
 #include "util/bitvector.h"
 #include "util/random.h"
 
@@ -700,13 +702,13 @@ 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)
   {
     // this is a unique term
     return n;
   }
+  Trace("sygus-synth-rr") << "sygusSampleExt : " << n << "..." << eq_n
+                          << std::endl;
   Node bn = n;
   Node beq_n = eq_n;
   if (d_use_sygus_type)
@@ -727,7 +729,7 @@ Node SygusSamplerExt::registerTerm(Node n, bool forceKeep)
     if (!d_match_trie.getMatches(bn, &d_ssenm))
     {
       keep = false;
-      Trace("sygus-synth-rr-debug") << "...redundant (matchable)" << std::endl;
+      Trace("sygus-synth-rr") << "...redundant (matchable)" << std::endl;
     }
   }
 
@@ -735,39 +737,64 @@ Node SygusSamplerExt::registerTerm(Node n, bool forceKeep)
   if (d_drewrite != nullptr)
   {
     Trace("sygus-synth-rr-debug") << "Add rewrite pair..." << std::endl;
-    if (!d_drewrite->addRewrite(bn, beq_n))
+    if (d_drewrite->areEqual(bn, beq_n))
     {
       // must be unique according to the dynamic rewriter
+      Trace("sygus-synth-rr") << "...redundant (rewritable)" << std::endl;
       keep = false;
-      Trace("sygus-synth-rr-debug") << "...redundant (rewritable)" << std::endl;
     }
   }
 
   if (keep)
   {
-    // add to match information
-    for (unsigned r = 0; r < 2; r++)
-    {
-      Node t = r == 0 ? bn : beq_n;
-      Node to = r == 0 ? beq_n : bn;
-      // insert in match trie if first time
-      if (d_pairs.find(t) == d_pairs.end())
-      {
-        Trace("sse-match") << "SSE add term : " << t << std::endl;
-        d_match_trie.addTerm(t);
-      }
-      d_pairs[t].insert(to);
-    }
     return eq_n;
   }
-  else if (Trace.isOn("sygus-synth-rr"))
+  Trace("sygus-synth-rr") << "Redundant pair : " << eq_n << " " << n;
+  Trace("sygus-synth-rr") << std::endl;
+  if (Trace.isOn("sygus-rr-filter"))
   {
-    Trace("sygus-synth-rr") << "Redundant pair : " << eq_n << " " << n;
-    Trace("sygus-synth-rr") << std::endl;
+    Printer* p = Printer::getPrinter(options::outputLanguage());
+    std::stringstream ss;
+    ss << "(redundant-rewrite ";
+    p->toStreamSygus(ss, n);
+    ss << " ";
+    p->toStreamSygus(ss, eq_n);
+    Trace("sygus-rr-filter") << ss.str() << std::endl;
   }
   return Node::null();
 }
 
+void SygusSamplerExt::registerRelevantPair(Node n, Node eq_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);
+  }
+  // ----- check rewriting redundancy
+  if (d_drewrite != nullptr)
+  {
+    Trace("sygus-synth-rr-debug") << "Add rewrite pair..." << std::endl;
+    Assert(!d_drewrite->areEqual(bn, beq_n));
+    d_drewrite->addRewrite(bn, beq_n);
+  }
+  // add to match information
+  for (unsigned r = 0; r < 2; r++)
+  {
+    Node t = r == 0 ? bn : beq_n;
+    Node to = r == 0 ? beq_n : bn;
+    // insert in match trie if first time
+    if (d_pairs.find(t) == d_pairs.end())
+    {
+      Trace("sse-match") << "SSE add term : " << t << std::endl;
+      d_match_trie.addTerm(t);
+    }
+    d_pairs[t].insert(to);
+  }
+}
+
 bool SygusSamplerExt::notify(Node s,
                              Node n,
                              std::vector<Node>& vars,
diff --git a/src/theory/quantifiers/sygus_sampler.h b/src/theory/quantifiers/sygus_sampler.h
index fa0d670d2..18b8f5511 100644
--- a/src/theory/quantifiers/sygus_sampler.h
+++ b/src/theory/quantifiers/sygus_sampler.h
@@ -431,6 +431,13 @@ class SygusSamplerExt : public SygusSampler
    */
   Node registerTerm(Node n, bool forceKeep = false) override;
 
+  /** register relevant pair
+   *
+   * This should be called after registerTerm( n ) returns eq_n.
+   * This registers ( n, eq_n ) as a relevant pair with this class.
+   */
+  void registerRelevantPair(Node n, Node eq_n);
+
  private:
   /** dynamic rewriter class */
   std::unique_ptr<DynamicRewriter> d_drewrite;