From 6445c3dbf5fed9fa32426f041061234b5ac407f7 Mon Sep 17 00:00:00 2001 From: Andrew Reynolds Date: Wed, 25 Apr 2018 11:29:59 -0500 Subject: [PATCH] Move candidate rewrite code to own file (#1804) --- src/Makefile.am | 2 + .../candidate_rewrite_database.cpp | 216 ++++++++++++++++++ .../quantifiers/candidate_rewrite_database.h | 91 ++++++++ .../sygus/ce_guided_conjecture.cpp | 181 +-------------- .../quantifiers/sygus/ce_guided_conjecture.h | 11 +- 5 files changed, 319 insertions(+), 182 deletions(-) create mode 100644 src/theory/quantifiers/candidate_rewrite_database.cpp create mode 100644 src/theory/quantifiers/candidate_rewrite_database.h 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 fvs; + TermUtil::computeVarContains(crr, fvs); + std::map fv_index; + std::vector 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::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 vars; + d_sampler.getVariables(vars); + std::vector pt; + for (const Node& v : vars) + { + std::map::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 +#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 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::iterator its = d_sampler.find(prog); - if (its == d_sampler.end()) + std::map::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 fvs; - TermUtil::computeVarContains(crr, fvs); - std::map fv_index; - std::vector 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::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 vars; - d_sampler[prog].getVariables(vars); - std::vector pt; - for (const Node& v : vars) - { - std::map::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 +#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 d_sampler; - /** - * Cache of skolems for each free variable that appears in a synthesis check - * (for --sygus-rr-synth-check). - */ - std::map d_fv_to_skolem; + std::map d_crrdb; }; } /* namespace CVC4::theory::quantifiers */ -- 2.30.2