Move candidate rewrite code to own file (#1804)

5 files changed, 319 insertions, 182 deletions

diff --git a/src/Makefile.am b/src/Makefile.am
index 04d6e24b7..7b364129f 100644
--- a/src/Makefile.am
+++ b/src/Makefile.am
@@ -373,6 +373,8 @@ libcvc4_la_SOURCES = \
 	theory/quantifiers/anti_skolem.h \
 	theory/quantifiers/bv_inverter.cpp \
 	theory/quantifiers/bv_inverter.h \
+	theory/quantifiers/candidate_rewrite_database.cpp \
+	theory/quantifiers/candidate_rewrite_database.h \
 	theory/quantifiers/cegqi/ceg_instantiator.cpp \
 	theory/quantifiers/cegqi/ceg_instantiator.h \
 	theory/quantifiers/cegqi/ceg_t_instantiator.cpp \
diff --git a/src/theory/quantifiers/candidate_rewrite_database.cpp b/src/theory/quantifiers/candidate_rewrite_database.cpp
new file mode 100644
index 000000000..fc7ec8e52
--- /dev/null
+++ b/src/theory/quantifiers/candidate_rewrite_database.cpp
@@ -0,0 +1,216 @@
+/*********************                                                        */
+/*! \file candidate_rewrite_database.cpp
+ ** \verbatim
+ ** Top contributors (to current version):
+ **   Andrew Reynolds
+ ** This file is part of the CVC4 project.
+ ** Copyright (c) 2009-2018 by the authors listed in the file AUTHORS
+ ** in the top-level source directory) and their institutional affiliations.
+ ** All rights reserved.  See the file COPYING in the top-level source
+ ** directory for licensing information.\endverbatim
+ **
+ ** \brief Implementation of candidate_rewrite_database
+ **/
+
+#include "theory/quantifiers/candidate_rewrite_database.h"
+
+#include "options/base_options.h"
+#include "options/quantifiers_options.h"
+#include "printer/printer.h"
+#include "smt/smt_engine.h"
+#include "smt/smt_engine_scope.h"
+#include "smt/smt_statistics_registry.h"
+#include "theory/quantifiers/sygus/ce_guided_instantiation.h"
+#include "theory/quantifiers/sygus/term_database_sygus.h"
+#include "theory/quantifiers/term_util.h"
+
+using namespace std;
+using namespace CVC4::kind;
+using namespace CVC4::context;
+
+namespace CVC4 {
+namespace theory {
+namespace quantifiers {
+
+CandidateRewriteDatabase::CandidateRewriteDatabase() : d_qe(nullptr) {}
+void CandidateRewriteDatabase::initialize(QuantifiersEngine* qe,
+                                          Node f,
+                                          unsigned nsamples,
+                                          bool useSygusType)
+{
+  d_qe = qe;
+  d_candidate = f;
+  d_sampler.initializeSygusExt(d_qe, f, nsamples, useSygusType);
+}
+
+bool CandidateRewriteDatabase::addTerm(Node sol, std::ostream& out)
+{
+  bool is_unique_term = true;
+  TermDbSygus* sygusDb = d_qe->getTermDatabaseSygus();
+  Node eq_sol = d_sampler.registerTerm(sol);
+  // eq_sol is a candidate solution that is equivalent to sol
+  if (eq_sol != sol)
+  {
+    CegInstantiation* cei = d_qe->getCegInstantiation();
+    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();
+      Node solb = sygusDb->sygusToBuiltin(sol);
+      Node solbr = er->extendedRewrite(solb);
+      Node eq_solb = sygusDb->sygusToBuiltin(eq_sol);
+      Node eq_solr = er->extendedRewrite(eq_solb);
+      bool verified = false;
+      Trace("rr-check") << "Check candidate rewrite..." << std::endl;
+      // verify it if applicable
+      if (options::sygusRewSynthCheck())
+      {
+        // 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.
+        NodeManager* nm = NodeManager::currentNM();
+        SmtEngine rrChecker(nm->toExprManager());
+        rrChecker.setLogic(smt::currentSmtEngine()->getLogicInfo());
+        Node crr = solbr.eqNode(eq_solr).negate();
+        Trace("rr-check") << "Check candidate rewrite : " << crr << std::endl;
+        // quantify over the free variables in crr
+        std::vector<Node> fvs;
+        TermUtil::computeVarContains(crr, fvs);
+        std::map<Node, unsigned> fv_index;
+        std::vector<Node> sks;
+        if (!fvs.empty())
+        {
+          // map to skolems
+          for (unsigned i = 0, size = fvs.size(); i < size; i++)
+          {
+            Node v = fvs[i];
+            fv_index[v] = i;
+            std::map<Node, Node>::iterator itf = d_fv_to_skolem.find(v);
+            if (itf == d_fv_to_skolem.end())
+            {
+              Node sk = nm->mkSkolem("rrck", v.getType());
+              d_fv_to_skolem[v] = sk;
+              sks.push_back(sk);
+            }
+            else
+            {
+              sks.push_back(itf->second);
+            }
+          }
+          crr = crr.substitute(fvs.begin(), fvs.end(), sks.begin(), sks.end());
+        }
+        rrChecker.assertFormula(crr.toExpr());
+        Result r = rrChecker.checkSat();
+        Trace("rr-check") << "...result : " << r << std::endl;
+        if (r.asSatisfiabilityResult().isSat())
+        {
+          Trace("rr-check") << "...rewrite does not hold for: " << std::endl;
+          success = false;
+          is_unique_term = true;
+          std::vector<Node> vars;
+          d_sampler.getVariables(vars);
+          std::vector<Node> pt;
+          for (const Node& v : vars)
+          {
+            std::map<Node, unsigned>::iterator itf = fv_index.find(v);
+            Node val;
+            if (itf == fv_index.end())
+            {
+              // not in conjecture, can use arbitrary value
+              val = v.getType().mkGroundTerm();
+            }
+            else
+            {
+              // get the model value of its skolem
+              Node sk = sks[itf->second];
+              val = Node::fromExpr(rrChecker.getValue(sk.toExpr()));
+              Trace("rr-check") << "  " << v << " -> " << val << std::endl;
+            }
+            pt.push_back(val);
+          }
+          d_sampler.addSamplePoint(pt);
+          // add the solution again
+          // by construction of the above point, we should be unique now
+          Node eq_sol_new = d_sampler.registerTerm(sol);
+          Assert(eq_sol_new == sol);
+        }
+        else
+        {
+          verified = !r.asSatisfiabilityResult().isUnknown();
+        }
+      }
+      else
+      {
+        // just insist that constants are not relevant pairs
+        success = !solb.isConst() || !eq_solb.isConst();
+      }
+      if (success)
+      {
+        // register this as a relevant pair (helps filtering)
+        d_sampler.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);
+        out << " ";
+        p->toStreamSygus(out, eq_sol);
+        out << ")" << std::endl;
+        ++(cei->d_statistics.d_candidate_rewrites_print);
+        // debugging information
+        if (Trace.isOn("sygus-rr-debug"))
+        {
+          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;
+        }
+        if (options::sygusRewSynthAccel())
+        {
+          // Add a symmetry breaking clause that excludes the larger
+          // of sol and eq_sol. This effectively states that we no longer
+          // wish to enumerate any term that contains sol (resp. eq_sol)
+          // as a subterm.
+          Node exc_sol = sol;
+          unsigned sz = sygusDb->getSygusTermSize(sol);
+          unsigned eqsz = sygusDb->getSygusTermSize(eq_sol);
+          if (eqsz > sz)
+          {
+            sz = eqsz;
+            exc_sol = eq_sol;
+          }
+          TypeNode ptn = d_candidate.getType();
+          Node x = sygusDb->getFreeVar(ptn, 0);
+          Node lem =
+              sygusDb->getExplain()->getExplanationForEquality(x, exc_sol);
+          lem = lem.negate();
+          Trace("sygus-rr-sb") << "Symmetry breaking lemma : " << lem
+                               << std::endl;
+          sygusDb->registerSymBreakLemma(d_candidate, lem, ptn, sz);
+        }
+      }
+    }
+    // We count this as a rewrite if we did not explicitly rule it out.
+    // Notice that when --sygus-rr-synth-check is enabled,
+    // statistics on number of candidate rewrite rules is
+    // an accurate count of (#enumerated_terms-#unique_terms) only if
+    // the option sygus-rr-synth-filter-order is disabled. The reason
+    // is that the sygus sampler may reason that a candidate rewrite
+    // rule is not useful since its variables are unordered, whereby
+    // it discards it as a redundant candidate rewrite rule before
+    // checking its correctness.
+    if (success)
+    {
+      ++(cei->d_statistics.d_candidate_rewrites);
+    }
+  }
+  return is_unique_term;
+}
+
+} /* CVC4::theory::quantifiers namespace */
+} /* CVC4::theory namespace */
+} /* CVC4 namespace */
diff --git a/src/theory/quantifiers/candidate_rewrite_database.h b/src/theory/quantifiers/candidate_rewrite_database.h
new file mode 100644
index 000000000..9ca946d26
--- /dev/null
+++ b/src/theory/quantifiers/candidate_rewrite_database.h
@@ -0,0 +1,91 @@
+/*********************                                                        */
+/*! \file candidate_rewrite_database.h
+ ** \verbatim
+ ** Top contributors (to current version):
+ **   Andrew Reynolds
+ ** This file is part of the CVC4 project.
+ ** Copyright (c) 2009-2018 by the authors listed in the file AUTHORS
+ ** in the top-level source directory) and their institutional affiliations.
+ ** All rights reserved.  See the file COPYING in the top-level source
+ ** directory for licensing information.\endverbatim
+ **
+ ** \brief candidate_rewrite_database
+ **/
+
+#include "cvc4_private.h"
+
+#ifndef __CVC4__THEORY__QUANTIFIERS__CANDIDATE_REWRITE_DATABASE_H
+#define __CVC4__THEORY__QUANTIFIERS__CANDIDATE_REWRITE_DATABASE_H
+
+#include <map>
+#include "theory/quantifiers/sygus_sampler.h"
+
+namespace CVC4 {
+namespace theory {
+namespace quantifiers {
+
+/** CandidateRewriteDatabase
+ *
+ * This maintains the necessary data structures for generating a database
+ * of candidate rewrite rules (see Reynolds et al "Rewrites for SMT Solvers
+ * Using Syntax-Guided Enumeration" SMT 2018). The primary responsibilities
+ * of this class are to perform the "equivalence checking" and "congruence
+ * and matching filtering" in Figure 1. The equivalence checking is done
+ * through a combination of the sygus sampler object owned by this class
+ * and the calls made to copies of the SmtEngine in ::addTerm. The rewrite
+ * rule filtering (based on congruence, matching, variable ordering) is also
+ * managed by the sygus sampler object.
+ */
+class CandidateRewriteDatabase
+{
+ public:
+  CandidateRewriteDatabase();
+  ~CandidateRewriteDatabase() {}
+  /**  Initialize this class
+   *
+   * qe : pointer to quantifiers engine,
+   * f : a term of some SyGuS datatype type whose values we will be
+   * testing under the free variables in the grammar of f. This is the
+   * "candidate variable" CegConjecture::d_candidates,
+   * 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.
+   *
+   * These arguments are used to initialize the sygus sampler class.
+   */
+  void initialize(QuantifiersEngine* qe,
+                  Node f,
+                  unsigned nsamples,
+                  bool useSygusType);
+  /** add term
+   *
+   * Notifies this class that the solution sol was enumerated. This may
+   * cause a candidate-rewrite to be printed on the output stream out.
+   */
+  bool addTerm(Node sol, std::ostream& out);
+
+ private:
+  /** reference to quantifier engine */
+  QuantifiersEngine* d_qe;
+  /** the function-to-synthesize we are testing */
+  Node d_candidate;
+  /** sygus sampler objects for each program variable
+   *
+   * This is used for the sygusRewSynth() option to synthesize new candidate
+   * rewrite rules.
+   */
+  SygusSamplerExt d_sampler;
+  /**
+   * Cache of skolems for each free variable that appears in a synthesis check
+   * (for --sygus-rr-synth-check).
+   */
+  std::map<Node, Node> d_fv_to_skolem;
+};
+
+} /* CVC4::theory::quantifiers namespace */
+} /* CVC4::theory namespace */
+} /* CVC4 namespace */
+
+#endif /* __CVC4__THEORY__QUANTIFIERS__CANDIDATE_REWRITE_DATABASE_H */
diff --git a/src/theory/quantifiers/sygus/ce_guided_conjecture.cpp b/src/theory/quantifiers/sygus/ce_guided_conjecture.cpp
index ca1f92d89..6914fc66f 100644
--- a/src/theory/quantifiers/sygus/ce_guided_conjecture.cpp
+++ b/src/theory/quantifiers/sygus/ce_guided_conjecture.cpp
@@ -19,9 +19,6 @@
 #include "options/quantifiers_options.h"
 #include "printer/printer.h"
 #include "prop/prop_engine.h"
-#include "smt/smt_engine.h"
-#include "smt/smt_engine_scope.h"
-#include "smt/smt_statistics_registry.h"
 #include "theory/quantifiers/first_order_model.h"
 #include "theory/quantifiers/instantiate.h"
 #include "theory/quantifiers/quantifiers_attributes.h"
@@ -589,179 +586,15 @@ void CegConjecture::printSynthSolution( std::ostream& out, bool singleInvocation
 
       if (status != 0 && options::sygusRewSynth())
       {
-        TermDbSygus* sygusDb = d_qe->getTermDatabaseSygus();
-        std::map<Node, SygusSamplerExt>::iterator its = d_sampler.find(prog);
-        if (its == d_sampler.end())
+        std::map<Node, CandidateRewriteDatabase>::iterator its =
+            d_crrdb.find(prog);
+        if (its == d_crrdb.end())
         {
-          d_sampler[prog].initializeSygusExt(
-              d_qe, prog, options::sygusSamples(), true);
-          its = d_sampler.find(prog);
-        }
-        Node eq_sol = its->second.registerTerm(sol);
-        // eq_sol is a candidate solution that is equivalent to sol
-        if (eq_sol != sol)
-        {
-          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();
-            Node solb = sygusDb->sygusToBuiltin(sol);
-            Node solbr = er->extendedRewrite(solb);
-            Node eq_solb = sygusDb->sygusToBuiltin(eq_sol);
-            Node eq_solr = er->extendedRewrite(eq_solb);
-            bool verified = false;
-            Trace("rr-check") << "Check candidate rewrite..." << std::endl;
-            // verify it if applicable
-            if (options::sygusRewSynthCheck())
-            {
-              // 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.
-              NodeManager* nm = NodeManager::currentNM();
-              SmtEngine rrChecker(nm->toExprManager());
-              rrChecker.setLogic(smt::currentSmtEngine()->getLogicInfo());
-              Node crr = solbr.eqNode(eq_solr).negate();
-              Trace("rr-check") << "Check candidate rewrite : " << crr
-                                << std::endl;
-              // quantify over the free variables in crr
-              std::vector<Node> fvs;
-              TermUtil::computeVarContains(crr, fvs);
-              std::map<Node, unsigned> fv_index;
-              std::vector<Node> sks;
-              if (!fvs.empty())
-              {
-                // map to skolems
-                for (unsigned i = 0, size = fvs.size(); i < size; i++)
-                {
-                  Node v = fvs[i];
-                  fv_index[v] = i;
-                  std::map<Node, Node>::iterator itf = d_fv_to_skolem.find(v);
-                  if (itf == d_fv_to_skolem.end())
-                  {
-                    Node sk = nm->mkSkolem("rrck", v.getType());
-                    d_fv_to_skolem[v] = sk;
-                    sks.push_back(sk);
-                  }
-                  else
-                  {
-                    sks.push_back(itf->second);
-                  }
-                }
-                crr = crr.substitute(
-                    fvs.begin(), fvs.end(), sks.begin(), sks.end());
-              }
-              rrChecker.assertFormula(crr.toExpr());
-              Result r = rrChecker.checkSat();
-              Trace("rr-check") << "...result : " << r << std::endl;
-              if (r.asSatisfiabilityResult().isSat())
-              {
-                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;
-                for (const Node& v : vars)
-                {
-                  std::map<Node, unsigned>::iterator itf = fv_index.find(v);
-                  Node val;
-                  if (itf == fv_index.end())
-                  {
-                    // not in conjecture, can use arbitrary value
-                    val = v.getType().mkGroundTerm();
-                  }
-                  else
-                  {
-                    // get the model value of its skolem
-                    Node sk = sks[itf->second];
-                    val = Node::fromExpr(rrChecker.getValue(sk.toExpr()));
-                    Trace("rr-check") << "  " << v << " -> " << val
-                                      << std::endl;
-                  }
-                  pt.push_back(val);
-                }
-                d_sampler[prog].addSamplePoint(pt);
-                // add the solution again
-                // by construction of the above point, we should be unique now
-                Node eq_sol_new = its->second.registerTerm(sol);
-                Assert(eq_sol_new == sol);
-              }
-              else
-              {
-                verified = !r.asSatisfiabilityResult().isUnknown();
-              }
-            }
-            else
-            {
-              // just insist that constants are not relevant pairs
-              success = !solb.isConst() || !eq_solb.isConst();
-            }
-            if (success)
-            {
-              // 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);
-              out << " ";
-              p->toStreamSygus(out, eq_sol);
-              out << ")" << std::endl;
-              ++(cei->d_statistics.d_candidate_rewrites_print);
-              // debugging information
-              if (Trace.isOn("sygus-rr-debug"))
-              {
-                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;
-              }
-              if (options::sygusRewSynthAccel())
-              {
-                // Add a symmetry breaking clause that excludes the larger
-                // of sol and eq_sol. This effectively states that we no longer
-                // wish to enumerate any term that contains sol (resp. eq_sol)
-                // as a subterm.
-                Node exc_sol = sol;
-                unsigned sz = sygusDb->getSygusTermSize(sol);
-                unsigned eqsz = sygusDb->getSygusTermSize(eq_sol);
-                if (eqsz > sz)
-                {
-                  sz = eqsz;
-                  exc_sol = eq_sol;
-                }
-                TypeNode ptn = prog.getType();
-                Node x = sygusDb->getFreeVar(ptn, 0);
-                Node lem = sygusDb->getExplain()->getExplanationForEquality(
-                    x, exc_sol);
-                lem = lem.negate();
-                Trace("sygus-rr-sb")
-                    << "Symmetry breaking lemma : " << lem << std::endl;
-                sygusDb->registerSymBreakLemma(d_candidates[i], lem, ptn, sz);
-              }
-            }
-          }
-          // We count this as a rewrite if we did not explicitly rule it out.
-          // Notice that when --sygus-rr-synth-check is enabled,
-          // statistics on number of candidate rewrite rules is
-          // an accurate count of (#enumerated_terms-#unique_terms) only if
-          // the option sygus-rr-synth-filter-order is disabled. The reason
-          // is that the sygus sampler may reason that a candidate rewrite
-          // rule is not useful since its variables are unordered, whereby
-          // it discards it as a redundant candidate rewrite rule before
-          // checking its correctness.
-          if (success)
-          {
-            ++(cei->d_statistics.d_candidate_rewrites);
-          }
+          d_crrdb[prog].initialize(
+              d_qe, d_candidates[i], options::sygusSamples(), true);
+          its = d_crrdb.find(prog);
         }
+        is_unique_term = d_crrdb[prog].addTerm(sol, out);
       }
       if (is_unique_term)
       {
diff --git a/src/theory/quantifiers/sygus/ce_guided_conjecture.h b/src/theory/quantifiers/sygus/ce_guided_conjecture.h
index b6812a18a..5d7f082d8 100644
--- a/src/theory/quantifiers/sygus/ce_guided_conjecture.h
+++ b/src/theory/quantifiers/sygus/ce_guided_conjecture.h
@@ -20,12 +20,12 @@
 
 #include <memory>
 
+#include "theory/quantifiers/candidate_rewrite_database.h"
 #include "theory/quantifiers/sygus/ce_guided_single_inv.h"
 #include "theory/quantifiers/sygus/cegis.h"
 #include "theory/quantifiers/sygus/sygus_grammar_cons.h"
 #include "theory/quantifiers/sygus/sygus_pbe.h"
 #include "theory/quantifiers/sygus/sygus_process_conj.h"
-#include "theory/quantifiers/sygus_sampler.h"
 #include "theory/quantifiers_engine.h"
 
 namespace CVC4 {
@@ -241,17 +241,12 @@ private:
   /** the guard for non-syntax-guided synthesis */
   Node d_nsg_guard;
   //-------------------------------- end non-syntax guided (deprecated)
-  /** sygus sampler objects for each program variable
+  /** candidate rewrite objects for each program variable
    *
    * This is used for the sygusRewSynth() option to synthesize new candidate
    * rewrite rules.
    */
-  std::map<Node, SygusSamplerExt> d_sampler;
-  /**
-   * Cache of skolems for each free variable that appears in a synthesis check
-   * (for --sygus-rr-synth-check).
-   */
-  std::map<Node, Node> d_fv_to_skolem;
+  std::map<Node, CandidateRewriteDatabase> d_crrdb;
 };
 
 } /* namespace CVC4::theory::quantifiers */