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 \
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
: 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,
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)
{
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)
{
// 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();
else
{
// get the model value of its skolem
- refv = sks[itf->second];
+ refv = itf->second;
}
}
if (val.isNull())
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
// 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"))
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)
{
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;
}
#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 {
* 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
* 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
* 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;
};
/**
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 */
--- /dev/null
+/********************* */
+/*! \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
--- /dev/null
+/********************* */
+/*! \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 */
--- /dev/null
+/********************* */
+/*! \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
--- /dev/null
+/********************* */
+/*! \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 */
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);
#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"
#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 {
*/
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 */
; 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)
projects / cvc5.git / commitdiff