Move candidate rewrite code to own file (#1804)

1 files changed, 216 insertions, 0 deletions

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 */