diff options
Diffstat (limited to 'src/theory/quantifiers/candidate_rewrite_database.cpp')
| -rw-r--r-- | src/theory/quantifiers/candidate_rewrite_database.cpp | 197 |
1 files changed, 154 insertions, 43 deletions
diff --git a/src/theory/quantifiers/candidate_rewrite_database.cpp b/src/theory/quantifiers/candidate_rewrite_database.cpp index 03c39f718..9bbb88699 100644 --- a/src/theory/quantifiers/candidate_rewrite_database.cpp +++ b/src/theory/quantifiers/candidate_rewrite_database.cpp @@ -32,37 +32,93 @@ namespace CVC4 { namespace theory { namespace quantifiers { -CandidateRewriteDatabase::CandidateRewriteDatabase() : d_qe(nullptr) {} -void CandidateRewriteDatabase::initialize(QuantifiersEngine* qe, - Node f, +// the number of d_drewrite objects we have allocated (to avoid name conflicts) +static unsigned drewrite_counter = 0; + +CandidateRewriteDatabase::CandidateRewriteDatabase() + : d_qe(nullptr), + d_tds(nullptr), + d_ext_rewrite(nullptr), + d_using_sygus(false) +{ + if (options::sygusRewSynthFilterCong()) + { + // initialize the dynamic rewriter + std::stringstream ss; + ss << "_dyn_rewriter_" << drewrite_counter; + drewrite_counter++; + d_drewrite = std::unique_ptr<DynamicRewriter>( + new DynamicRewriter(ss.str(), &d_fake_context)); + d_sampler.setDynamicRewriter(d_drewrite.get()); + } +} +void CandidateRewriteDatabase::initialize(ExtendedRewriter* er, + TypeNode tn, + std::vector<Node>& vars, unsigned nsamples, - bool useSygusType) + bool unique_type_ids) +{ + d_candidate = Node::null(); + d_type = tn; + d_using_sygus = false; + d_qe = nullptr; + d_tds = nullptr; + d_ext_rewrite = er; + d_sampler.initialize(tn, vars, nsamples, unique_type_ids); +} + +void CandidateRewriteDatabase::initializeSygus(QuantifiersEngine* qe, + Node f, + unsigned nsamples, + bool useSygusType) { - d_qe = qe; d_candidate = f; - d_sampler.initializeSygusExt(d_qe, f, nsamples, useSygusType); + d_type = f.getType(); + Assert(d_type.isDatatype()); + Assert(static_cast<DatatypeType>(d_type.toType()).getDatatype().isSygus()); + d_using_sygus = true; + d_qe = qe; + d_tds = d_qe->getTermDatabaseSygus(); + d_ext_rewrite = d_tds->getExtRewriter(); + d_sampler.initializeSygus(d_tds, f, nsamples, useSygusType); } -bool CandidateRewriteDatabase::addTerm(Node sol, std::ostream& out) +bool CandidateRewriteDatabase::addTerm(Node sol, + std::ostream& out, + bool& rew_print) { 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); + // get the actual term + Node solb = sol; + Node eq_solb = eq_sol; + if (d_using_sygus) + { + Assert(d_tds != nullptr); + solb = d_tds->sygusToBuiltin(sol); + eq_solb = d_tds->sygusToBuiltin(eq_sol); + } + // get the rewritten form + Node solbr; + Node eq_solr; + if (d_ext_rewrite != nullptr) + { + solbr = d_ext_rewrite->extendedRewrite(solb); + eq_solr = d_ext_rewrite->extendedRewrite(eq_solb); + } + else + { + solbr = Rewriter::rewrite(solb); + eq_solr = Rewriter::rewrite(eq_solb); + } bool verified = false; Trace("rr-check") << "Check candidate rewrite..." << std::endl; // verify it if applicable @@ -108,27 +164,36 @@ bool CandidateRewriteDatabase::addTerm(Node sol, std::ostream& out) if (r.asSatisfiabilityResult().isSat() == Result::SAT) { 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()) + Node refv = v; + // if a bound variable, map to the skolem we introduce before + // looking up the model value + if (v.getKind() == BOUND_VARIABLE) { - // not in conjecture, can use arbitrary value - val = v.getType().mkGroundTerm(); + std::map<Node, unsigned>::iterator itf = fv_index.find(v); + if (itf == fv_index.end()) + { + // not in conjecture, can use arbitrary value + val = v.getType().mkGroundTerm(); + } + else + { + // get the model value of its skolem + refv = sks[itf->second]; + } } - else + if (val.isNull()) { - // 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; + Assert(!refv.isNull() && refv.getKind() != BOUND_VARIABLE); + val = Node::fromExpr(rrChecker.getValue(refv.toExpr())); } + Trace("rr-check") << " " << v << " -> " << val << std::endl; pt.push_back(val); } d_sampler.addSamplePoint(pt); @@ -145,22 +210,29 @@ bool CandidateRewriteDatabase::addTerm(Node sol, std::ostream& out) else { // just insist that constants are not relevant pairs - success = !solb.isConst() || !eq_solb.isConst(); + is_unique_term = solb.isConst() && eq_solb.isConst(); } - if (success) + if (!is_unique_term) { // 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); + if (d_using_sygus) + { + Printer* p = Printer::getPrinter(options::outputLanguage()); + p->toStreamSygus(out, sol); + out << " "; + p->toStreamSygus(out, eq_sol); + } + else + { + out << sol << " " << eq_sol; + } out << ")" << std::endl; - ++(cei->d_statistics.d_candidate_rewrites_print); + rew_print = true; // debugging information if (Trace.isOn("sygus-rr-debug")) { @@ -169,32 +241,33 @@ bool CandidateRewriteDatabase::addTerm(Node sol, std::ostream& out) Trace("sygus-rr-debug") << "; candidate #2 ext-rewrites to: " << eq_solr << std::endl; } - if (options::sygusRewSynthAccel()) + if (options::sygusRewSynthAccel() && d_using_sygus) { + Assert(d_tds != nullptr); // 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); + unsigned sz = d_tds->getSygusTermSize(sol); + unsigned eqsz = d_tds->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); + Node x = d_tds->getFreeVar(ptn, 0); + Node lem = d_tds->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); + d_tds->registerSymBreakLemma(d_candidate, lem, ptn, sz); } } } // We count this as a rewrite if we did not explicitly rule it out. + // The value of is_unique_term is false iff this call resulted in a rewrite. // 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 @@ -203,14 +276,52 @@ bool CandidateRewriteDatabase::addTerm(Node sol, std::ostream& out) // 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; } +bool CandidateRewriteDatabase::addTerm(Node sol, std::ostream& out) +{ + bool rew_print = false; + return addTerm(sol, out, rew_print); +} + +CandidateRewriteDatabaseGen::CandidateRewriteDatabaseGen( + std::vector<Node>& vars, unsigned nsamples) + : d_vars(vars.begin(), vars.end()), d_nsamples(nsamples) +{ +} + +bool CandidateRewriteDatabaseGen::addTerm(Node n, std::ostream& out) +{ + ExtendedRewriter* er = nullptr; + if (options::synthRrPrepExtRew()) + { + er = &d_ext_rewrite; + } + Node nr; + if (er == nullptr) + { + nr = Rewriter::rewrite(n); + } + else + { + nr = er->extendedRewrite(n); + } + TypeNode tn = nr.getType(); + std::map<TypeNode, CandidateRewriteDatabase>::iterator itc = d_cdbs.find(tn); + if (itc == d_cdbs.end()) + { + Trace("synth-rr-dbg") << "Initialize database for " << tn << std::endl; + // initialize with the extended rewriter owned by this class + d_cdbs[tn].initialize(er, tn, d_vars, d_nsamples, true); + itc = d_cdbs.find(tn); + Trace("synth-rr-dbg") << "...finish." << std::endl; + } + Trace("synth-rr-dbg") << "Add term " << nr << " for " << tn << std::endl; + return itc->second.addTerm(nr, out); +} + } /* CVC4::theory::quantifiers namespace */ } /* CVC4::theory namespace */ } /* CVC4 namespace */ |