src/theory/quantifiers/candidate_rewrite_database.cpp

   1 /******************************************************************************
   2  * Top contributors (to current version):
   3  *   Andrew Reynolds, Aina Niemetz, Andres Noetzli
   4  *
   5  * This file is part of the cvc5 project.
   6  *
   7  * Copyright (c) 2009-2021 by the authors listed in the file AUTHORS
   8  * in the top-level source directory and their institutional affiliations.
   9  * All rights reserved.  See the file COPYING in the top-level source
  10  * directory for licensing information.
  11  * ****************************************************************************
  12  *
  13  * Implementation of candidate_rewrite_database.
  14  */
  15
  16 #include "theory/quantifiers/candidate_rewrite_database.h"
  17
  18 #include "options/base_options.h"
  19 #include "printer/printer.h"
  20 #include "smt/smt_engine.h"
  21 #include "smt/smt_engine_scope.h"
  22 #include "smt/smt_statistics_registry.h"
  23 #include "theory/datatypes/sygus_datatype_utils.h"
  24 #include "theory/quantifiers/sygus/term_database_sygus.h"
  25 #include "theory/quantifiers/term_util.h"
  26 #include "theory/rewriter.h"
  27
  28 using namespace std;
  29 using namespace cvc5::kind;
  30 using namespace cvc5::context;
  31
  32 namespace cvc5 {
  33 namespace theory {
  34 namespace quantifiers {
  35
  36 CandidateRewriteDatabase::CandidateRewriteDatabase(
  37     Env& env, bool doCheck, bool rewAccel, bool silent, bool filterPairs)
  38     : ExprMiner(env),
  39       d_tds(nullptr),
  40       d_ext_rewrite(nullptr),
  41       d_doCheck(doCheck),
  42       d_rewAccel(rewAccel),
  43       d_silent(silent),
  44       d_filterPairs(filterPairs),
  45       d_using_sygus(false)
  46 {
  47 }
  48 void CandidateRewriteDatabase::initialize(const std::vector<Node>& vars,
  49                                           SygusSampler* ss)
  50 {
  51   Assert(ss != nullptr);
  52   d_candidate = Node::null();
  53   d_using_sygus = false;
  54   d_tds = nullptr;
  55   d_ext_rewrite = nullptr;
  56   if (d_filterPairs)
  57   {
  58     d_crewrite_filter.initialize(ss, nullptr, false);
  59   }
  60   ExprMiner::initialize(vars, ss);
  61 }
  62
  63 void CandidateRewriteDatabase::initializeSygus(const std::vector<Node>& vars,
  64                                                TermDbSygus* tds,
  65                                                Node f,
  66                                                SygusSampler* ss)
  67 {
  68   Assert(ss != nullptr);
  69   d_candidate = f;
  70   d_using_sygus = true;
  71   d_tds = tds;
  72   d_ext_rewrite = nullptr;
  73   if (d_filterPairs)
  74   {
  75     d_crewrite_filter.initialize(ss, d_tds, d_using_sygus);
  76   }
  77   ExprMiner::initialize(vars, ss);
  78 }
  79
  80 Node CandidateRewriteDatabase::addTerm(Node sol,
  81                                        bool rec,
  82                                        std::ostream& out,
  83                                        bool& rew_print)
  84 {
  85   // have we added this term before?
  86   std::unordered_map<Node, Node>::iterator itac = d_add_term_cache.find(sol);
  87   if (itac != d_add_term_cache.end())
  88   {
  89     return itac->second;
  90   }
  91
  92   if (rec)
  93   {
  94     // if recursive, we first add all subterms
  95     for (const Node& solc : sol)
  96     {
  97       // whether a candidate rewrite is printed for any subterm is irrelevant
  98       bool rew_printc = false;
  99       addTerm(solc, rec, out, rew_printc);
 100     }
 101   }
 102   // register the term
 103   bool is_unique_term = true;
 104   Node eq_sol = d_sampler->registerTerm(sol);
 105   // eq_sol is a candidate solution that is equivalent to sol
 106   if (eq_sol != sol)
 107   {
 108     is_unique_term = false;
 109     // should we filter the pair?
 110     if (!d_filterPairs || !d_crewrite_filter.filterPair(sol, eq_sol))
 111     {
 112       // get the actual term
 113       Node solb = sol;
 114       Node eq_solb = eq_sol;
 115       if (d_using_sygus)
 116       {
 117         Assert(d_tds != nullptr);
 118         solb = d_tds->sygusToBuiltin(sol);
 119         eq_solb = d_tds->sygusToBuiltin(eq_sol);
 120       }
 121       // get the rewritten form
 122       Node solbr;
 123       Node eq_solr;
 124       if (d_ext_rewrite != nullptr)
 125       {
 126         solbr = d_ext_rewrite->extendedRewrite(solb);
 127         eq_solr = d_ext_rewrite->extendedRewrite(eq_solb);
 128       }
 129       else
 130       {
 131         solbr = Rewriter::rewrite(solb);
 132         eq_solr = Rewriter::rewrite(eq_solb);
 133       }
 134       bool verified = false;
 135       Trace("rr-check") << "Check candidate rewrite..." << std::endl;
 136       // verify it if applicable
 137       if (d_doCheck)
 138       {
 139         Node crr = solbr.eqNode(eq_solr).negate();
 140         Trace("rr-check") << "Check candidate rewrite : " << crr << std::endl;
 141
 142         // Notice we don't set produce-models. rrChecker takes the same
 143         // options as the SmtEngine we belong to, where we ensure that
 144         // produce-models is set.
 145         std::unique_ptr<SmtEngine> rrChecker;
 146         initializeChecker(rrChecker, crr);
 147         Result r = rrChecker->checkSat();
 148         Trace("rr-check") << "...result : " << r << std::endl;
 149         if (r.asSatisfiabilityResult().isSat() == Result::SAT)
 150         {
 151           Trace("rr-check") << "...rewrite does not hold for: " << std::endl;
 152           is_unique_term = true;
 153           std::vector<Node> vars;
 154           d_sampler->getVariables(vars);
 155           std::vector<Node> pt;
 156           for (const Node& v : vars)
 157           {
 158             Node val;
 159             Node refv = v;
 160             // if a bound variable, map to the skolem we introduce before
 161             // looking up the model value
 162             if (v.getKind() == BOUND_VARIABLE)
 163             {
 164               std::map<Node, Node>::iterator itf = d_fv_to_skolem.find(v);
 165               if (itf == d_fv_to_skolem.end())
 166               {
 167                 // not in conjecture, can use arbitrary value
 168                 val = v.getType().mkGroundTerm();
 169               }
 170               else
 171               {
 172                 // get the model value of its skolem
 173                 refv = itf->second;
 174               }
 175             }
 176             if (val.isNull())
 177             {
 178               Assert(!refv.isNull() && refv.getKind() != BOUND_VARIABLE);
 179               val = rrChecker->getValue(refv);
 180             }
 181             Trace("rr-check") << "  " << v << " -> " << val << std::endl;
 182             pt.push_back(val);
 183           }
 184           d_sampler->addSamplePoint(pt);
 185           // add the solution again
 186           // by construction of the above point, we should be unique now
 187           eq_sol = d_sampler->registerTerm(sol);
 188           Assert(eq_sol == sol);
 189         }
 190         else
 191         {
 192           verified = !r.asSatisfiabilityResult().isUnknown();
 193         }
 194       }
 195       else
 196       {
 197         // just insist that constants are not relevant pairs
 198         if (solb.isConst() && eq_solb.isConst())
 199         {
 200           is_unique_term = true;
 201           eq_sol = sol;
 202         }
 203       }
 204       if (!is_unique_term)
 205       {
 206         // register this as a relevant pair (helps filtering)
 207         if (d_filterPairs)
 208         {
 209           d_crewrite_filter.registerRelevantPair(sol, eq_sol);
 210         }
 211         // The analog of terms sol and eq_sol are equivalent under
 212         // sample points but do not rewrite to the same term. Hence,
 213         // this indicates a candidate rewrite.
 214         if (!d_silent)
 215         {
 216           out << "(" << (verified ? "" : "candidate-") << "rewrite ";
 217           if (d_using_sygus)
 218           {
 219             TermDbSygus::toStreamSygus(out, sol);
 220             out << " ";
 221             TermDbSygus::toStreamSygus(out, eq_sol);
 222           }
 223           else
 224           {
 225             out << sol << " " << eq_sol;
 226           }
 227           out << ")" << std::endl;
 228         }
 229         // we count this as printed, despite not literally printing it
 230         rew_print = true;
 231         // debugging information
 232         if (Trace.isOn("sygus-rr-debug"))
 233         {
 234           Trace("sygus-rr-debug") << "; candidate #1 ext-rewrites to: " << solbr
 235                                   << std::endl;
 236           Trace("sygus-rr-debug")
 237               << "; candidate #2 ext-rewrites to: " << eq_solr << std::endl;
 238         }
 239         if (d_rewAccel && d_using_sygus)
 240         {
 241           Assert(d_tds != nullptr);
 242           // Add a symmetry breaking clause that excludes the larger
 243           // of sol and eq_sol. This effectively states that we no longer
 244           // wish to enumerate any term that contains sol (resp. eq_sol)
 245           // as a subterm.
 246           Node exc_sol = sol;
 247           unsigned sz = datatypes::utils::getSygusTermSize(sol);
 248           unsigned eqsz = datatypes::utils::getSygusTermSize(eq_sol);
 249           if (eqsz > sz)
 250           {
 251             sz = eqsz;
 252             exc_sol = eq_sol;
 253           }
 254           TypeNode ptn = d_candidate.getType();
 255           Node x = d_tds->getFreeVar(ptn, 0);
 256           Node lem = d_tds->getExplain()->getExplanationForEquality(x, exc_sol);
 257           lem = lem.negate();
 258           Trace("sygus-rr-sb") << "Symmetry breaking lemma : " << lem
 259                                << std::endl;
 260           d_tds->registerSymBreakLemma(d_candidate, lem, ptn, sz);
 261         }
 262       }
 263     }
 264     // We count this as a rewrite if we did not explicitly rule it out.
 265     // The value of is_unique_term is false iff this call resulted in a rewrite.
 266     // Notice that when --sygus-rr-synth-check is enabled,
 267     // statistics on number of candidate rewrite rules is
 268     // an accurate count of (#enumerated_terms-#unique_terms) only if
 269     // the option sygus-rr-synth-filter-order is disabled. The reason
 270     // is that the sygus sampler may reason that a candidate rewrite
 271     // rule is not useful since its variables are unordered, whereby
 272     // it discards it as a redundant candidate rewrite rule before
 273     // checking its correctness.
 274   }
 275   d_add_term_cache[sol] = eq_sol;
 276   return eq_sol;
 277 }
 278
 279 Node CandidateRewriteDatabase::addTerm(Node sol, bool rec, std::ostream& out)
 280 {
 281   bool rew_print = false;
 282   return addTerm(sol, rec, out, rew_print);
 283 }
 284 bool CandidateRewriteDatabase::addTerm(Node sol, std::ostream& out)
 285 {
 286   Node rsol = addTerm(sol, false, out);
 287   return sol == rsol;
 288 }
 289
 290 void CandidateRewriteDatabase::setSilent(bool flag) { d_silent = flag; }
 291
 292 void CandidateRewriteDatabase::setExtendedRewriter(ExtendedRewriter* er)
 293 {
 294   d_ext_rewrite = er;
 295 }
 296
 297 }  // namespace quantifiers
 298 }  // namespace theory
 299 }  // namespace cvc5