diff options
| -rw-r--r-- | src/Makefile.am | 4 | ||||
| -rw-r--r-- | src/options/quantifiers_options.toml | 6 | ||||
| -rw-r--r-- | src/theory/quantifiers/candidate_rewrite_database.cpp | 148 | ||||
| -rw-r--r-- | src/theory/quantifiers/candidate_rewrite_database.h | 68 | ||||
| -rw-r--r-- | src/theory/quantifiers/expr_miner.cpp | 115 | ||||
| -rw-r--r-- | src/theory/quantifiers/expr_miner.h | 101 | ||||
| -rw-r--r-- | src/theory/quantifiers/expr_miner_manager.cpp | 96 | ||||
| -rw-r--r-- | src/theory/quantifiers/expr_miner_manager.h | 107 | ||||
| -rw-r--r-- | src/theory/quantifiers/sygus/ce_guided_conjecture.cpp | 16 | ||||
| -rw-r--r-- | src/theory/quantifiers/sygus/ce_guided_conjecture.h | 11 | ||||
| -rw-r--r-- | test/regress/regress1/rr-verify/bv-term.sy | 3 |
11 files changed, 514 insertions, 161 deletions
diff --git a/src/Makefile.am b/src/Makefile.am index 77fd455bb..a8edbf1fd 100644 --- a/src/Makefile.am +++ b/src/Makefile.am @@ -470,6 +470,10 @@ libcvc4_la_SOURCES = \ theory/quantifiers/equality_query.h \ theory/quantifiers/equality_infer.cpp \ theory/quantifiers/equality_infer.h \ + theory/quantifiers/expr_miner.cpp \ + theory/quantifiers/expr_miner.h \ + theory/quantifiers/expr_miner_manager.cpp \ + theory/quantifiers/expr_miner_manager.h \ theory/quantifiers/extended_rewrite.cpp \ theory/quantifiers/extended_rewrite.h \ theory/quantifiers/first_order_model.cpp \ diff --git a/src/options/quantifiers_options.toml b/src/options/quantifiers_options.toml index a4fca6d3c..7b58f955a 100644 --- a/src/options/quantifiers_options.toml +++ b/src/options/quantifiers_options.toml @@ -1306,11 +1306,11 @@ header = "options/quantifiers_options.h" help = "use satisfiability check to verify correctness of candidate rewrites" [[option]] - name = "sygusRewSynthCheckTimeout" + name = "sygusExprMinerCheckTimeout" category = "regular" - long = "sygus-rr-synth-check-timeout=N" + long = "sygus-expr-miner-check-timeout=N" type = "unsigned long" - help = "timeout (in milliseconds) for the satisfiability check to verify correctness of candidate rewrites" + help = "timeout (in milliseconds) for satisfiability checks in expression miners" # CEGQI applied to general quantified formulas diff --git a/src/theory/quantifiers/candidate_rewrite_database.cpp b/src/theory/quantifiers/candidate_rewrite_database.cpp index e5df8db8a..3b7aab0b2 100644 --- a/src/theory/quantifiers/candidate_rewrite_database.cpp +++ b/src/theory/quantifiers/candidate_rewrite_database.cpp @@ -36,40 +36,36 @@ CandidateRewriteDatabase::CandidateRewriteDatabase() : d_qe(nullptr), d_tds(nullptr), d_ext_rewrite(nullptr), - d_using_sygus(false) + d_using_sygus(false), + d_silent(false) { } -void CandidateRewriteDatabase::initialize(ExtendedRewriter* er, - TypeNode tn, - std::vector<Node>& vars, - unsigned nsamples, - bool unique_type_ids) +void CandidateRewriteDatabase::initialize(const std::vector<Node>& vars, + SygusSampler* ss) { + Assert(ss != nullptr); 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); - d_crewrite_filter.initialize(&d_sampler, nullptr, false); + d_ext_rewrite = nullptr; + d_crewrite_filter.initialize(ss, nullptr, false); + ExprMiner::initialize(vars, ss); } -void CandidateRewriteDatabase::initializeSygus(QuantifiersEngine* qe, +void CandidateRewriteDatabase::initializeSygus(const std::vector<Node>& vars, + QuantifiersEngine* qe, Node f, - unsigned nsamples, - bool useSygusType) + SygusSampler* ss) { + Assert(ss != nullptr); d_candidate = f; - 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); - d_crewrite_filter.initialize(&d_sampler, d_tds, true); + d_ext_rewrite = nullptr; + d_crewrite_filter.initialize(ss, d_tds, false); + ExprMiner::initialize(vars, ss); } bool CandidateRewriteDatabase::addTerm(Node sol, @@ -77,7 +73,7 @@ bool CandidateRewriteDatabase::addTerm(Node sol, bool& rew_print) { bool is_unique_term = true; - Node eq_sol = d_sampler.registerTerm(sol); + Node eq_sol = d_sampler->registerTerm(sol); // eq_sol is a candidate solution that is equivalent to sol if (eq_sol != sol) { @@ -116,81 +112,23 @@ bool CandidateRewriteDatabase::addTerm(Node sol, 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()); - } // 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. - bool needExport = true; + bool needExport = false; ExprManagerMapCollection varMap; ExprManager em(nm->getOptions()); std::unique_ptr<SmtEngine> rrChecker; - Result r; - if (options::sygusRewSynthCheckTimeout.wasSetByUser()) - { - // To support a separate timeout for the subsolver, we need to create - // a separate ExprManager with its own options. This requires that - // the expressions sent to the subsolver can be exported from on - // ExprManager to another. If the export fails, we throw an - // OptionException. - try - { - rrChecker.reset(new SmtEngine(&em)); - rrChecker->setTimeLimit(options::sygusRewSynthCheckTimeout(), true); - rrChecker->setLogic(smt::currentSmtEngine()->getLogicInfo()); - Expr eccr = crr.toExpr().exportTo(&em, varMap); - rrChecker->assertFormula(eccr); - r = rrChecker->checkSat(); - } - catch (const CVC4::ExportUnsupportedException& e) - { - std::stringstream msg; - msg << "Unable to export " << crr - << " but exporting expressions is required for " - "--sygus-rr-synth-check-timeout."; - throw OptionException(msg.str()); - } - } - else - { - needExport = false; - rrChecker.reset(new SmtEngine(nm->toExprManager())); - rrChecker->assertFormula(crr.toExpr()); - r = rrChecker->checkSat(); - } - + initializeChecker(rrChecker, em, varMap, crr, needExport); + Result r = rrChecker->checkSat(); Trace("rr-check") << "...result : " << r << std::endl; if (r.asSatisfiabilityResult().isSat() == Result::SAT) { Trace("rr-check") << "...rewrite does not hold for: " << std::endl; is_unique_term = true; std::vector<Node> vars; - d_sampler.getVariables(vars); + d_sampler->getVariables(vars); std::vector<Node> pt; for (const Node& v : vars) { @@ -200,8 +138,8 @@ bool CandidateRewriteDatabase::addTerm(Node sol, // looking up the model value if (v.getKind() == BOUND_VARIABLE) { - std::map<Node, unsigned>::iterator itf = fv_index.find(v); - if (itf == fv_index.end()) + std::map<Node, Node>::iterator itf = d_fv_to_skolem.find(v); + if (itf == d_fv_to_skolem.end()) { // not in conjecture, can use arbitrary value val = v.getType().mkGroundTerm(); @@ -209,7 +147,7 @@ bool CandidateRewriteDatabase::addTerm(Node sol, else { // get the model value of its skolem - refv = sks[itf->second]; + refv = itf->second; } } if (val.isNull()) @@ -229,10 +167,10 @@ bool CandidateRewriteDatabase::addTerm(Node sol, Trace("rr-check") << " " << v << " -> " << val << std::endl; pt.push_back(val); } - d_sampler.addSamplePoint(pt); + 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); + Node eq_sol_new = d_sampler->registerTerm(sol); Assert(eq_sol_new == sol); } else @@ -252,19 +190,23 @@ bool CandidateRewriteDatabase::addTerm(Node 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. - out << "(" << (verified ? "" : "candidate-") << "rewrite "; - if (d_using_sygus) - { - Printer* p = Printer::getPrinter(options::outputLanguage()); - p->toStreamSygus(out, sol); - out << " "; - p->toStreamSygus(out, eq_sol); - } - else + if (!d_silent) { - out << sol << " " << eq_sol; + out << "(" << (verified ? "" : "candidate-") << "rewrite "; + 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; } - out << ")" << std::endl; + // we count this as printed, despite not literally printing it rew_print = true; // debugging information if (Trace.isOn("sygus-rr-debug")) @@ -319,6 +261,13 @@ bool CandidateRewriteDatabase::addTerm(Node sol, std::ostream& out) return addTerm(sol, out, rew_print); } +void CandidateRewriteDatabase::setSilent(bool flag) { d_silent = flag; } + +void CandidateRewriteDatabase::setExtendedRewriter(ExtendedRewriter* er) +{ + d_ext_rewrite = er; +} + CandidateRewriteDatabaseGen::CandidateRewriteDatabaseGen( std::vector<Node>& vars, unsigned nsamples) : d_qe(nullptr), d_vars(vars.begin(), vars.end()), d_nsamples(nsamples) @@ -347,7 +296,8 @@ bool CandidateRewriteDatabaseGen::addTerm(Node n, std::ostream& out) { 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); + d_cdbs[tn].initialize(d_vars, &d_sampler[tn]); + d_cdbs[tn].setExtendedRewriter(er); itc = d_cdbs.find(tn); Trace("synth-rr-dbg") << "...finish." << std::endl; } diff --git a/src/theory/quantifiers/candidate_rewrite_database.h b/src/theory/quantifiers/candidate_rewrite_database.h index 7f51043e2..5b8ffbd94 100644 --- a/src/theory/quantifiers/candidate_rewrite_database.h +++ b/src/theory/quantifiers/candidate_rewrite_database.h @@ -22,6 +22,7 @@ #include <unordered_set> #include <vector> #include "theory/quantifiers/candidate_rewrite_filter.h" +#include "theory/quantifiers/expr_miner.h" #include "theory/quantifiers/sygus_sampler.h" namespace CVC4 { @@ -40,31 +41,14 @@ namespace quantifiers { * rule filtering (based on congruence, matching, variable ordering) is also * managed by the sygus sampler object. */ -class CandidateRewriteDatabase +class CandidateRewriteDatabase : public ExprMiner { public: CandidateRewriteDatabase(); ~CandidateRewriteDatabase() {} - /** Initialize this class - * - * er : pointer to the extended rewriter (if any) we are using to compute - * candidate rewrites, - * tn : the return type of terms we will be testing with this class, - * vars : the variables we are testing substitutions for, - * nsamples : number of sample points this class will test, - * unique_type_ids : if this is set to true, then each variable is treated - * as unique. This affects whether or not a rewrite rule is considered - * redundant or not. For example the rewrite f(y)=y is redundant if - * f(x)=x has also been printed as a rewrite and x and y have the same type - * id (see SygusSampler for details). On the other hand, when a candidate - * rewrite database is initialized with sygus below, the type ids of the - * (sygus formal argument list) variables are always computed and used. - */ - void initialize(ExtendedRewriter* er, - TypeNode tn, - std::vector<Node>& vars, - unsigned nsamples, - bool unique_type_ids = false); + /** Initialize this class */ + void initialize(const std::vector<Node>& var, + SygusSampler* ss = nullptr) override; /** Initialize this class * * Serves the same purpose as the above function, but we will be using @@ -75,19 +59,12 @@ class CandidateRewriteDatabase * database when computing candidate rewrites, * 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. + * "candidate variable" CegConjecture::d_candidates. */ - void initializeSygus(QuantifiersEngine* qe, + void initializeSygus(const std::vector<Node>& vars, + QuantifiersEngine* qe, Node f, - unsigned nsamples, - bool useSygusType); + SygusSampler* ss = nullptr); /** add term * * Notifies this class that the solution sol was enumerated. This may @@ -97,34 +74,27 @@ class CandidateRewriteDatabase * true if this class printed a rewrite. */ bool addTerm(Node sol, std::ostream& out, bool& rew_print); - bool addTerm(Node sol, std::ostream& out); + bool addTerm(Node sol, std::ostream& out) override; + /** sets whether this class should output candidate rewrites it finds */ + void setSilent(bool flag); + /** set the (extended) rewriter used by this class */ + void setExtendedRewriter(ExtendedRewriter* er); private: /** reference to quantifier engine */ QuantifiersEngine* d_qe; - /** pointer to the sygus term database of d_qe */ + /** (required) pointer to the sygus term database of d_qe */ TermDbSygus* d_tds; - /** pointer to the extended rewriter object we are using */ + /** an extended rewriter object */ ExtendedRewriter* d_ext_rewrite; - /** the (sygus or builtin) type of terms we are testing */ - TypeNode d_type; /** the function-to-synthesize we are testing (if sygus) */ Node d_candidate; /** whether we are using sygus */ bool d_using_sygus; - /** sygus sampler objects for each program variable - * - * This is used for the sygusRewSynth() option to synthesize new candidate - * rewrite rules. - */ - SygusSampler d_sampler; /** candidate rewrite filter */ CandidateRewriteFilter d_crewrite_filter; - /** - * 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; + /** if true, we silence the output of candidate rewrites */ + bool d_silent; }; /** @@ -154,6 +124,8 @@ class CandidateRewriteDatabaseGen QuantifiersEngine* d_qe; /** the variables */ std::vector<Node> d_vars; + /** sygus sampler object for each type */ + std::map<TypeNode, SygusSampler> d_sampler; /** the number of samples */ unsigned d_nsamples; /** candidate rewrite databases for each type */ diff --git a/src/theory/quantifiers/expr_miner.cpp b/src/theory/quantifiers/expr_miner.cpp new file mode 100644 index 000000000..0e8542826 --- /dev/null +++ b/src/theory/quantifiers/expr_miner.cpp @@ -0,0 +1,115 @@ +/********************* */ +/*! \file expr_miner.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 expr_miner + **/ + +#include "theory/quantifiers/expr_miner.h" + +#include "options/quantifiers_options.h" +#include "smt/smt_engine.h" +#include "smt/smt_engine_scope.h" +#include "theory/quantifiers/term_util.h" + +using namespace std; +using namespace CVC4::kind; + +namespace CVC4 { +namespace theory { +namespace quantifiers { + +void ExprMiner::initialize(const std::vector<Node>& vars, SygusSampler* ss) +{ + d_sampler = ss; + d_vars.insert(d_vars.end(), vars.begin(), vars.end()); +} + +Node ExprMiner::convertToSkolem(Node n) +{ + std::vector<Node> fvs; + TermUtil::computeVarContains(n, fvs); + if (fvs.empty()) + { + return n; + } + std::vector<Node> sfvs; + std::vector<Node> sks; + // map to skolems + NodeManager* nm = NodeManager::currentNM(); + for (unsigned i = 0, size = fvs.size(); i < size; i++) + { + Node v = fvs[i]; + // only look at the sampler variables + if (std::find(d_vars.begin(), d_vars.end(), v) != d_vars.end()) + { + sfvs.push_back(v); + 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); + } + } + } + return n.substitute(sfvs.begin(), sfvs.end(), sks.begin(), sks.end()); +} + +void ExprMiner::initializeChecker(std::unique_ptr<SmtEngine>& checker, + ExprManager& em, + ExprManagerMapCollection& varMap, + Node query, + bool& needExport) +{ + // Convert bound variables to skolems. This ensures the satisfiability + // check is ground. + Node squery = convertToSkolem(query); + NodeManager* nm = NodeManager::currentNM(); + if (options::sygusExprMinerCheckTimeout.wasSetByUser()) + { + // To support a separate timeout for the subsolver, we need to create + // a separate ExprManager with its own options. This requires that + // the expressions sent to the subsolver can be exported from on + // ExprManager to another. If the export fails, we throw an + // OptionException. + try + { + checker.reset(new SmtEngine(&em)); + checker->setTimeLimit(options::sygusExprMinerCheckTimeout(), true); + checker->setLogic(smt::currentSmtEngine()->getLogicInfo()); + Expr equery = squery.toExpr().exportTo(&em, varMap); + checker->assertFormula(equery); + } + catch (const CVC4::ExportUnsupportedException& e) + { + std::stringstream msg; + msg << "Unable to export " << squery + << " but exporting expressions is required for " + "--sygus-rr-synth-check-timeout."; + throw OptionException(msg.str()); + } + needExport = true; + } + else + { + needExport = false; + checker.reset(new SmtEngine(nm->toExprManager())); + checker->assertFormula(squery.toExpr()); + } +} + +} // namespace quantifiers +} // namespace theory +} // namespace CVC4 diff --git a/src/theory/quantifiers/expr_miner.h b/src/theory/quantifiers/expr_miner.h new file mode 100644 index 000000000..c09f40d0e --- /dev/null +++ b/src/theory/quantifiers/expr_miner.h @@ -0,0 +1,101 @@ +/********************* */ +/*! \file expr_miner.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 expr_miner + **/ + +#include "cvc4_private.h" + +#ifndef __CVC4__THEORY__QUANTIFIERS__EXPRESSION_MINER_H +#define __CVC4__THEORY__QUANTIFIERS__EXPRESSION_MINER_H + +#include <map> +#include <memory> +#include <vector> +#include "expr/expr_manager.h" +#include "expr/node.h" +#include "smt/smt_engine.h" +#include "theory/quantifiers/sygus_sampler.h" + +namespace CVC4 { +namespace theory { +namespace quantifiers { + +/** Expression miner + * + * This is a virtual base class for modules that "mines" certain information + * from (enumerated) expressions. This includes: + * - candidate rewrite rules (--sygus-rr-synth) + */ +class ExprMiner +{ + public: + ExprMiner() : d_sampler(nullptr) {} + virtual ~ExprMiner() {} + /** initialize + * + * This initializes this expression miner. The argument vars indicates the + * free variables of terms that will be added to this class. The argument + * sampler gives an (optional) pointer to a sampler, which is used to + * sample tuples of valuations of these variables. + */ + virtual void initialize(const std::vector<Node>& vars, + SygusSampler* ss = nullptr); + /** add term + * + * This registers term n with this expression miner. The output stream out + * is provided as an argument for the purposes of outputting the result of + * the expression mining done by this class. For example, candidate-rewrite + * output is printed on out by the candidate rewrite generator miner. + */ + virtual bool addTerm(Node n, std::ostream& out) = 0; + + protected: + /** the set of variables used by this class */ + std::vector<Node> d_vars; + /** pointer to the sygus sampler object we are using */ + SygusSampler* d_sampler; + /** + * Maps to skolems for each free variable that appears in a check. This is + * used during initializeChecker so that query (which may contain free + * variables) is converted to a formula without free variables. + */ + std::map<Node, Node> d_fv_to_skolem; + /** convert */ + Node convertToSkolem(Node n); + /** initialize checker + * + * This function initializes the smt engine smte to check the satisfiability + * of the argument "query", which is a formula whose free variables (of + * kind BOUND_VARIABLE) are a subset of d_vars. + * + * The arguments em and varMap are used for supporting cases where we + * want smte to use a different expression manager instead of the current + * expression manager. The motivation for this so that different options can + * be set for the subcall. + * + * We update the flag needExport to true if smte is using the expression + * manager em. In this case, subsequent expressions extracted from smte + * (for instance, model values) must be exported to the current expression + * manager. + */ + void initializeChecker(std::unique_ptr<SmtEngine>& smte, + ExprManager& em, + ExprManagerMapCollection& varMap, + Node query, + bool& needExport); +}; + +} // namespace quantifiers +} // namespace theory +} // namespace CVC4 + +#endif /* __CVC4__THEORY__QUANTIFIERS__EXPRESSION_MINER_H */ diff --git a/src/theory/quantifiers/expr_miner_manager.cpp b/src/theory/quantifiers/expr_miner_manager.cpp new file mode 100644 index 000000000..8c116781d --- /dev/null +++ b/src/theory/quantifiers/expr_miner_manager.cpp @@ -0,0 +1,96 @@ +/********************* */ +/*! \file expr_miner_manager.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 expression miner manager. + **/ + +#include "theory/quantifiers/expr_miner_manager.h" + +namespace CVC4 { +namespace theory { +namespace quantifiers { + +ExpressionMinerManager::ExpressionMinerManager() + : d_doRewSynth(false), + d_use_sygus_type(false), + d_qe(nullptr), + d_tds(nullptr) +{ +} + +void ExpressionMinerManager::initialize(const std::vector<Node>& vars, + TypeNode tn, + unsigned nsamples, + bool unique_type_ids) +{ + d_doRewSynth = false; + d_sygus_fun = Node::null(); + d_use_sygus_type = false; + d_qe = nullptr; + d_tds = nullptr; + // initialize the sampler + d_sampler.initialize(tn, vars, nsamples, unique_type_ids); +} + +void ExpressionMinerManager::initializeSygus(QuantifiersEngine* qe, + Node f, + unsigned nsamples, + bool useSygusType) +{ + d_doRewSynth = false; + d_sygus_fun = f; + d_use_sygus_type = useSygusType; + d_qe = qe; + d_tds = qe->getTermDatabaseSygus(); + // initialize the sampler + d_sampler.initializeSygus(d_tds, f, nsamples, useSygusType); +} + +void ExpressionMinerManager::enableRewriteRuleSynth() +{ + if (d_doRewSynth) + { + // already enabled + return; + } + d_doRewSynth = true; + std::vector<Node> vars; + d_sampler.getVariables(vars); + // initialize the candidate rewrite database + if (!d_sygus_fun.isNull()) + { + Assert(d_qe != nullptr); + d_crd.initializeSygus(vars, d_qe, d_sygus_fun, &d_sampler); + } + else + { + d_crd.initialize(vars, &d_sampler); + } + d_crd.setExtendedRewriter(&d_ext_rew); + d_crd.setSilent(false); +} + +bool ExpressionMinerManager::addTerm(Node sol, + std::ostream& out, + bool& rew_print) +{ + return d_crd.addTerm(sol, out, rew_print); +} + +bool ExpressionMinerManager::addTerm(Node sol, std::ostream& out) +{ + bool rew_print = false; + return addTerm(sol, out, rew_print); +} + +} // namespace quantifiers +} // namespace theory +} // namespace CVC4 diff --git a/src/theory/quantifiers/expr_miner_manager.h b/src/theory/quantifiers/expr_miner_manager.h new file mode 100644 index 000000000..668d04beb --- /dev/null +++ b/src/theory/quantifiers/expr_miner_manager.h @@ -0,0 +1,107 @@ +/********************* */ +/*! \file expr_miner_manager.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 Expression miner manager, which manages individual expression miners. + **/ + +#include "cvc4_private.h" + +#ifndef __CVC4__THEORY__QUANTIFIERS__EXPR_MINER_MANAGER_H +#define __CVC4__THEORY__QUANTIFIERS__EXPR_MINER_MANAGER_H + +#include "expr/node.h" +#include "theory/quantifiers/candidate_rewrite_database.h" +#include "theory/quantifiers/extended_rewrite.h" +#include "theory/quantifiers/sygus_sampler.h" +#include "theory/quantifiers_engine.h" + +namespace CVC4 { +namespace theory { +namespace quantifiers { + +/** ExpressionMinerManager + * + * This class manages a set of expression miners. It provides a common place + * to register expressions so that multiple mining algorithms can be run in + * coordination, possibly sharing information and utilities like a common + * sampling object. + */ +class ExpressionMinerManager +{ + public: + ExpressionMinerManager(); + ~ExpressionMinerManager() {} + /** Initialize this class + * + * Initializes this class, informing it that the free variables of terms + * added to this class via addTerm will have free variables that are a subset + * of vars, and have type tn. All expression miners in this class with be + * initialized with this variable list. The arguments nsamples and + * unique_type_ids are used for initializing the sampler class of this manager + * (see SygusSampler::initialize for details). + */ + void initialize(const std::vector<Node>& vars, + TypeNode tn, + unsigned nsamples, + bool unique_type_ids = false); + /** Initialize this class, sygus version + * + * Initializes this class, informing it that the terms added to this class + * via calls to addTerm will be generated by the grammar of f. The method + * takes a pointer to the quantifiers engine qe. If the argument useSygusType + * is true, the terms added to this class are the sygus datatype terms. + * If useSygusType is false, the terms are the builtin equivalent of these + * terms. The argument nsamples is used to initialize the sampler. + */ + void initializeSygus(QuantifiersEngine* qe, + Node f, + unsigned nsamples, + bool useSygusType); + /** enable rewrite rule synthesis (--sygus-rr-synth) */ + void enableRewriteRuleSynth(); + /** add term + * + * Expression miners may print information on the output stream out, for + * instance, candidate-rewrites. The method returns true if the term sol is + * distinct (up to T-equivalence) with all previous terms added to this class, + * which is computed based on the miners that this manager enables. + */ + bool addTerm(Node sol, std::ostream& out); + /** + * Same as above, but the argument rew_print is set to true if a rewrite rule + * was printed on the output stream out. + */ + bool addTerm(Node sol, std::ostream& out, bool& rew_print); + + private: + /** whether we are doing rewrite synthesis */ + bool d_doRewSynth; + /** the sygus function passed to initializeSygus, if any */ + Node d_sygus_fun; + /** whether we are using sygus types */ + bool d_use_sygus_type; + /** pointer to the quantifiers engine, used if d_use_sygus is true */ + QuantifiersEngine* d_qe; + /** the sygus term database of d_qe */ + TermDbSygus* d_tds; + /** candidate rewrite database */ + CandidateRewriteDatabase d_crd; + /** sygus sampler object */ + SygusSampler d_sampler; + /** extended rewriter object */ + ExtendedRewriter d_ext_rew; +}; + +} // namespace quantifiers +} // namespace theory +} // namespace CVC4 + +#endif /* __CVC4__THEORY__QUANTIFIERS__EXPR_MINER_MANAGER_H */ diff --git a/src/theory/quantifiers/sygus/ce_guided_conjecture.cpp b/src/theory/quantifiers/sygus/ce_guided_conjecture.cpp index 0a212598b..d8329395d 100644 --- a/src/theory/quantifiers/sygus/ce_guided_conjecture.cpp +++ b/src/theory/quantifiers/sygus/ce_guided_conjecture.cpp @@ -723,16 +723,20 @@ void CegConjecture::printSynthSolution( std::ostream& out, bool singleInvocation if (status != 0 && options::sygusRewSynth()) { - std::map<Node, CandidateRewriteDatabase>::iterator its = - d_crrdb.find(prog); - if (its == d_crrdb.end()) + std::map<Node, ExpressionMinerManager>::iterator its = + d_exprm.find(prog); + if (its == d_exprm.end()) { - d_crrdb[prog].initializeSygus( + d_exprm[prog].initializeSygus( d_qe, d_candidates[i], options::sygusSamples(), true); - its = d_crrdb.find(prog); + if (options::sygusRewSynth()) + { + d_exprm[prog].enableRewriteRuleSynth(); + } + its = d_exprm.find(prog); } bool rew_print = false; - is_unique_term = d_crrdb[prog].addTerm(sol, out, rew_print); + is_unique_term = d_exprm[prog].addTerm(sol, out, rew_print); if (rew_print) { ++(cei->d_statistics.d_candidate_rewrites_print); diff --git a/src/theory/quantifiers/sygus/ce_guided_conjecture.h b/src/theory/quantifiers/sygus/ce_guided_conjecture.h index 612a2b4ce..88902e721 100644 --- a/src/theory/quantifiers/sygus/ce_guided_conjecture.h +++ b/src/theory/quantifiers/sygus/ce_guided_conjecture.h @@ -20,7 +20,7 @@ #include <memory> -#include "theory/quantifiers/candidate_rewrite_database.h" +#include "theory/quantifiers/expr_miner_manager.h" #include "theory/quantifiers/sygus/ce_guided_single_inv.h" #include "theory/quantifiers/sygus/cegis.h" #include "theory/quantifiers/sygus/cegis_unif.h" @@ -28,7 +28,6 @@ #include "theory/quantifiers/sygus/sygus_pbe.h" #include "theory/quantifiers/sygus/sygus_process_conj.h" #include "theory/quantifiers/sygus/sygus_repair_const.h" -#include "theory/quantifiers/sygus_sampler.h" #include "theory/quantifiers_engine.h" namespace CVC4 { @@ -262,12 +261,16 @@ private: */ void printAndContinueStream(); //-------------------------------- end sygus stream - /** candidate rewrite objects for each program variable + /** expression miner managers for each function-to-synthesize + * + * Notice that for each function-to-synthesize, we enumerate a stream of + * candidate solutions, where each of these streams is independent. Thus, + * we maintain separate expression miner managers for each of them. * * This is used for the sygusRewSynth() option to synthesize new candidate * rewrite rules. */ - std::map<Node, CandidateRewriteDatabase> d_crrdb; + std::map<Node, ExpressionMinerManager> d_exprm; }; } /* namespace CVC4::theory::quantifiers */ diff --git a/test/regress/regress1/rr-verify/bv-term.sy b/test/regress/regress1/rr-verify/bv-term.sy index 025479f24..f310396d2 100644 --- a/test/regress/regress1/rr-verify/bv-term.sy +++ b/test/regress/regress1/rr-verify/bv-term.sy @@ -1,6 +1,7 @@ ; COMMAND-LINE: --sygus-rr --sygus-samples=1000 --sygus-abort-size=2 --sygus-rr-verify-abort --no-sygus-sym-break +; COMMAND-LINE: --sygus-rr-synth --sygus-samples=1000 --sygus-abort-size=2 --sygus-rr-verify-abort --sygus-rr-synth-check ; EXPECT: (error "Maximum term size (2) for enumerative SyGuS exceeded.") -; SCRUBBER: grep -v -E '(\(define-fun|\(candidate-rewrite)' +; SCRUBBER: grep -v -E '(\(define-fun|\(candidate-rewrite|\(rewrite)' ; EXIT: 1 (set-logic BV) |