#include "options/smt_options.h"
#include "preprocessing/assertion_pipeline.h"
#include "preprocessing/preprocessing_pass_context.h"
-#include "theory/quantifiers/extended_rewrite.h"
namespace cvc5 {
namespace preprocessing {
PreprocessingPassResult ExtRewPre::applyInternal(
AssertionPipeline* assertionsToPreprocess)
{
- theory::quantifiers::ExtendedRewriter extr(options::extRewPrepAgg());
for (unsigned i = 0, size = assertionsToPreprocess->size(); i < size; ++i)
{
assertionsToPreprocess->replace(
- i, extr.extendedRewrite((*assertionsToPreprocess)[i]));
+ i,
+ extendedRewrite((*assertionsToPreprocess)[i],
+ options::extRewPrepAgg()));
}
return PreprocessingPassResult::NO_CONFLICT;
}
Node EnvObj::rewrite(TNode node) { return d_env.getRewriter()->rewrite(node); }
+Node EnvObj::extendedRewrite(TNode node, bool aggr)
+{
+ return d_env.getRewriter()->extendedRewrite(node, aggr);
+}
+
const LogicInfo& EnvObj::logicInfo() const { return d_env.getLogicInfo(); }
const Options& EnvObj::options() const { return d_env.getOptions(); }
* This is a wrapper around theory::Rewriter::rewrite via Env.
*/
Node rewrite(TNode node);
+ /**
+ * Extended rewrite a node.
+ * This is a wrapper around theory::Rewriter::extendedRewrite via Env.
+ */
+ Node extendedRewrite(TNode node, bool aggr = true);
/** Get the current logic information. */
const LogicInfo& logicInfo() const;
if (!proofStepProcessed)
{
// maybe its just an (extended) rewrite?
- theory::quantifiers::ExtendedRewriter extr(true);
- Node pr = extr.extendedRewrite(proven[0]);
+ Node pr = theory::Rewriter::callExtendedRewrite(proven[0]);
if (proven[1] == pr)
{
Node idr = mkMethodId(MethodId::RW_EXT_REWRITE);
#include "expr/subs.h"
#include "smt/smt_solver.h"
#include "theory/quantifiers/cegqi/nested_qe.h"
-#include "theory/quantifiers/extended_rewrite.h"
#include "theory/quantifiers_engine.h"
-#include "theory/rewriter.h"
#include "theory/theory_engine.h"
#include "util/string.h"
namespace smt {
QuantElimSolver::QuantElimSolver(Env& env, SmtSolver& sms)
- : d_env(env), d_smtSolver(sms)
+ : EnvObj(env), d_smtSolver(sms)
{
}
}
NodeManager* nm = NodeManager::currentNM();
// ensure the body is rewritten
- q = nm->mkNode(q.getKind(), q[0], Rewriter::rewrite(q[1]));
+ q = nm->mkNode(q.getKind(), q[0], rewrite(q[1]));
// do nested quantifier elimination if necessary
q = quantifiers::NestedQe::doNestedQe(d_env, q, true);
Trace("smt-qe") << "QuantElimSolver: after nested quantifier elimination : "
Trace("smt-qe") << "QuantElimSolver returned : " << ret << std::endl;
if (q.getKind() == EXISTS)
{
- ret = Rewriter::rewrite(ret.negate());
+ ret = rewrite(ret.negate());
}
}
else
ret = nm->mkConst(q.getKind() != EXISTS);
}
// do extended rewrite to minimize the size of the formula aggressively
- theory::quantifiers::ExtendedRewriter extr(true);
- ret = extr.extendedRewrite(ret);
+ ret = extendedRewrite(ret);
// if we are not an internal subsolver, convert to witness form, since
// internally generated skolems should not escape
if (!isInternalSubsolver)
#include "expr/node.h"
#include "smt/assertions.h"
+#include "smt/env_obj.h"
namespace cvc5 {
-class Env;
-
namespace smt {
class SmtSolver;
* quantifier instantiations used for unsat which are in turn used for
* constructing the solution for the quantifier elimination query.
*/
-class QuantElimSolver
+class QuantElimSolver : protected EnvObj
{
public:
QuantElimSolver(Env& env, SmtSolver& sms);
bool isInternalSubsolver);
private:
- /** Reference to the env */
- Env& d_env;
/** The SMT solver, which is used during doQuantifierElimination. */
SmtSolver& d_smtSolver;
};
#include "theory/arith/nl/cad/projections.h"
#include "theory/arith/nl/cad/variable_ordering.h"
#include "theory/arith/nl/nl_model.h"
-#include "theory/quantifiers/extended_rewrite.h"
+#include "theory/rewriter.h"
namespace std {
/** Generic streaming operator for std::vector. */
namespace cad {
CDCAC::CDCAC(Env& env, const std::vector<poly::Variable>& ordering)
- : d_env(env), d_variableOrdering(ordering)
+ : EnvObj(env), d_variableOrdering(ordering)
{
if (d_env.isTheoryProofProducing())
{
Kind::EQUAL, nl::as_cvc_polynomial(coeff, vm), zero));
}
// if phi is false (i.e. p can not vanish)
- quantifiers::ExtendedRewriter rew;
- Node rewritten =
- rew.extendedRewrite(NodeManager::currentNM()->mkAnd(conditions));
+ Node rewritten = Rewriter::callExtendedRewrite(
+ NodeManager::currentNM()->mkAnd(conditions));
if (rewritten.isConst())
{
Assert(rewritten.getKind() == Kind::CONST_BOOLEAN);
#include <vector>
#include "smt/env.h"
+#include "smt/env_obj.h"
#include "theory/arith/nl/cad/cdcac_utils.h"
#include "theory/arith/nl/cad/constraints.h"
#include "theory/arith/nl/cad/proof_generator.h"
* This class implements Cylindrical Algebraic Coverings as presented in
* https://arxiv.org/pdf/2003.05633.pdf
*/
-class CDCAC
+class CDCAC : protected EnvObj
{
public:
/** Initialize this method with the given variable ordering. */
*/
void pruneRedundantIntervals(std::vector<CACInterval>& intervals);
- /** A reference to the environment */
- Env& d_env;
-
/**
* The current assignment. When the method terminates with SAT, it contains a
* model for the input constraints.
#include "proof/method_id.h"
#include "proof/proof_checker.h"
#include "proof/proof_node.h"
-#include "theory/quantifiers/extended_rewrite.h"
namespace cvc5 {
const std::vector<Node>& children,
const std::vector<Node>& args) override;
- /** extended rewriter object */
- quantifiers::ExtendedRewriter d_ext_rewriter;
-
private:
/** Reference to the environment. */
Env& d_env;
using namespace cvc5::theory;
using namespace cvc5::theory::datatypes;
-SygusExtension::SygusExtension(TheoryState& s,
+SygusExtension::SygusExtension(Env& env,
+ TheoryState& s,
InferenceManager& im,
quantifiers::TermDbSygus* tds)
- : d_state(s),
+ : EnvObj(env),
+ d_state(s),
d_im(im),
d_tds(tds),
d_ssb(tds),
<< ", type=" << tn << std::endl;
Node bv = d_tds->sygusToBuiltin(cnv, tn);
Trace("sygus-sb-debug") << " ......builtin is " << bv << std::endl;
- Node bvr = d_tds->getExtRewriter()->extendedRewrite(bv);
+ Node bvr = extendedRewrite(bv);
Trace("sygus-sb-debug") << " ......search value rewrites to " << bvr << std::endl;
Trace("dt-sygus") << " * DT builtin : " << n << " -> " << bvr << std::endl;
unsigned sz = utils::getSygusTermSize(nv);
#include "context/cdhashset.h"
#include "context/context.h"
#include "expr/node.h"
+#include "smt/env_obj.h"
#include "theory/datatypes/sygus_simple_sym.h"
#include "theory/decision_manager.h"
#include "theory/quantifiers/sygus_sampler.h"
* We prioritize decisions of form (1) before (2). Both kinds of decision are
* critical for solution completeness, which is enforced by DecisionManager.
*/
-class SygusExtension
+class SygusExtension : protected EnvObj
{
typedef context::CDHashMap<Node, int> IntMap;
typedef context::CDHashMap<Node, Node> NodeMap;
typedef context::CDHashSet<Node> NodeSet;
public:
- SygusExtension(TheoryState& s,
+ SygusExtension(Env& env,
+ TheoryState& s,
InferenceManager& im,
quantifiers::TermDbSygus* tds);
~SygusExtension();
{
quantifiers::TermDbSygus* tds =
getQuantifiersEngine()->getTermDatabaseSygus();
- d_sygusExtension.reset(new SygusExtension(d_state, d_im, tds));
+ d_sygusExtension.reset(new SygusExtension(d_env, d_state, d_im, tds));
// do congruence on evaluation functions
d_equalityEngine->addFunctionKind(kind::DT_SYGUS_EVAL);
}
Env& env, bool doCheck, bool rewAccel, bool silent, bool filterPairs)
: ExprMiner(env),
d_tds(nullptr),
- d_ext_rewrite(nullptr),
+ d_useExtRewriter(false),
d_doCheck(doCheck),
d_rewAccel(rewAccel),
d_silent(silent),
d_candidate = Node::null();
d_using_sygus = false;
d_tds = nullptr;
- d_ext_rewrite = nullptr;
+ d_useExtRewriter = false;
if (d_filterPairs)
{
d_crewrite_filter.initialize(ss, nullptr, false);
d_candidate = f;
d_using_sygus = true;
d_tds = tds;
- d_ext_rewrite = nullptr;
+ d_useExtRewriter = false;
if (d_filterPairs)
{
d_crewrite_filter.initialize(ss, d_tds, d_using_sygus);
// get the rewritten form
Node solbr;
Node eq_solr;
- if (d_ext_rewrite != nullptr)
+ if (d_useExtRewriter)
{
- solbr = d_ext_rewrite->extendedRewrite(solb);
- eq_solr = d_ext_rewrite->extendedRewrite(eq_solb);
+ solbr = extendedRewrite(solb);
+ eq_solr = extendedRewrite(eq_solb);
}
else
{
void CandidateRewriteDatabase::setSilent(bool flag) { d_silent = flag; }
-void CandidateRewriteDatabase::setExtendedRewriter(ExtendedRewriter* er)
+void CandidateRewriteDatabase::enableExtendedRewriter()
{
- d_ext_rewrite = er;
+ d_useExtRewriter = true;
}
} // namespace quantifiers
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);
+ /** Enable the (extended) rewriter for this class */
+ void enableExtendedRewriter();
private:
/** (required) pointer to the sygus term database of d_qe */
TermDbSygus* d_tds;
- /** an extended rewriter object */
- ExtendedRewriter* d_ext_rewrite;
+ /** Whether we use the extended rewriter */
+ bool d_useExtRewriter;
/** the function-to-synthesize we are testing (if sygus) */
Node d_candidate;
/** whether we are checking equivalence using subsolver */
{
d_crd.initialize(vars, &d_sampler);
}
- d_crd.setExtendedRewriter(&d_ext_rew);
+ d_crd.enableExtendedRewriter();
d_crd.setSilent(false);
}
#include "expr/node.h"
#include "smt/env_obj.h"
#include "theory/quantifiers/candidate_rewrite_database.h"
-#include "theory/quantifiers/extended_rewrite.h"
#include "theory/quantifiers/query_generator.h"
#include "theory/quantifiers/solution_filter.h"
#include "theory/quantifiers/sygus_sampler.h"
namespace cvc5 {
-
-class Env;
-
namespace theory {
namespace quantifiers {
SolutionFilterStrength d_sols;
/** sygus sampler object */
SygusSampler d_sampler;
- /** extended rewriter object */
- ExtendedRewriter d_ext_rew;
};
} // namespace quantifiers
};
typedef expr::Attribute<ExtRewriteAggAttributeId, Node> ExtRewriteAggAttribute;
-ExtendedRewriter::ExtendedRewriter(bool aggr) : d_aggr(aggr)
+ExtendedRewriter::ExtendedRewriter(Rewriter& rew, bool aggr)
+ : d_rew(rew), d_aggr(aggr)
{
d_true = NodeManager::currentNM()->mkConst(true);
d_false = NodeManager::currentNM()->mkConst(false);
Node ExtendedRewriter::extendedRewrite(Node n) const
{
- n = Rewriter::rewrite(n);
+ n = d_rew.rewrite(n);
// has it already been computed?
Node ncache = getCache(n);
}
}
}
- ret = Rewriter::rewrite(ret);
+ ret = d_rew.rewrite(ret);
//--------------------end rewrite children
// now, do extended rewrite
t2.substitute(vars.begin(), vars.end(), subs.begin(), subs.end());
if (nn != t2)
{
- nn = Rewriter::rewrite(nn);
+ nn = d_rew.rewrite(nn);
if (nn == t1)
{
new_ret = t2;
// must use partial substitute here, to avoid substitution into witness
std::map<Kind, bool> rkinds;
nn = partialSubstitute(t1, vars, subs, rkinds);
- nn = Rewriter::rewrite(nn);
+ nn = d_rew.rewrite(nn);
if (nn != t1)
{
// If full=false, then we've duplicated a term u in the children of n.
Node nn = partialSubstitute(t2, assign, rkinds);
if (nn != t2)
{
- nn = Rewriter::rewrite(nn);
+ nn = d_rew.rewrite(nn);
if (nn == t1)
{
new_ret = nn;
{
children[ii] = n[i][j + 1];
Node pull = nm->mkNode(n.getKind(), children);
- Node pullr = Rewriter::rewrite(pull);
+ Node pullr = d_rew.rewrite(pull);
children[ii] = n[i];
ite_c[i][j] = pullr;
}
Assert(nite.getKind() == itek);
// now, simply pull the ITE and try ITE rewrites
Node pull_ite = nm->mkNode(itek, nite[0], ip.second[0], ip.second[1]);
- pull_ite = Rewriter::rewrite(pull_ite);
+ pull_ite = d_rew.rewrite(pull_ite);
if (pull_ite.getKind() == ITE)
{
Node new_pull_ite = extendedRewriteIte(itek, pull_ite, false);
ccs = cpol ? ccs : TermUtil::mkNegate(notk, ccs);
Trace("ext-rew-bcp") << "BCP: propagated " << c << " -> " << ccs
<< std::endl;
- ccs = Rewriter::rewrite(ccs);
+ ccs = d_rew.rewrite(ccs);
Trace("ext-rew-bcp") << "BCP: rewritten to " << ccs << std::endl;
to_process.push_back(ccs);
// store this as a node that propagation touched. This marks c so that
index--;
new_ret = nm->mkNode(eqk, children[index], new_ret);
}
- new_ret = Rewriter::rewrite(new_ret);
+ new_ret = d_rew.rewrite(new_ret);
if (new_ret != ret)
{
return new_ret;
namespace cvc5 {
namespace theory {
+
+class Rewriter;
+
namespace quantifiers {
/** Extended rewriter
class ExtendedRewriter
{
public:
- ExtendedRewriter(bool aggr = true);
+ ExtendedRewriter(Rewriter& rew, bool aggr = true);
~ExtendedRewriter() {}
/** return the extended rewritten form of n */
Node extendedRewrite(Node n) const;
private:
+ /** The underlying rewriter that we are extending */
+ Rewriter& d_rew;
/** cache that the extended rewritten form of n is ret */
void setCache(Node n, Node ret) const;
/** get the cache for n */
{
}
QuantifiersModules::~QuantifiersModules() {}
-void QuantifiersModules::initialize(QuantifiersState& qs,
+void QuantifiersModules::initialize(Env& env,
+ QuantifiersState& qs,
QuantifiersInferenceManager& qim,
QuantifiersRegistry& qr,
TermRegistry& tr,
}
if (options::sygus())
{
- d_synth_e.reset(new SynthEngine(qs, qim, qr, tr));
+ d_synth_e.reset(new SynthEngine(env, qs, qim, qr, tr));
modules.push_back(d_synth_e.get());
}
// bounded integer instantiation is used when the user requests it via
* This constructs the above modules based on the current options. It adds
* a pointer to each module it constructs to modules.
*/
- void initialize(QuantifiersState& qs,
+ void initialize(Env& env,
+ QuantifiersState& qs,
QuantifiersInferenceManager& qim,
QuantifiersRegistry& qr,
TermRegistry& tr,
{
Node body = q[1];
// apply extended rewriter
- ExtendedRewriter er;
- Node bodyr = er.extendedRewrite(body);
+ Node bodyr = Rewriter::callExtendedRewrite(body);
if (body != bodyr)
{
std::vector<Node> children;
}
//simplify the solution using the extended rewriter
Trace("csi-sol") << "Solution (pre-simplification): " << s << std::endl;
- s = d_treg.getTermDatabaseSygus()->getExtRewriter()->extendedRewrite(s);
+ s = extendedRewrite(s);
Trace("csi-sol") << "Solution (post-simplification): " << s << std::endl;
// wrap into lambda, as needed
return SygusUtils::wrapSolutionForSynthFun(prog, s);
{
Trace("csi-sol") << "Post-process solution..." << std::endl;
Node prev = sol;
- sol = d_treg.getTermDatabaseSygus()->getExtRewriter()->extendedRewrite(sol);
+ sol = extendedRewrite(sol);
if (prev != sol)
{
Trace("csi-sol") << "Solution (after post process) : " << sol
d_rl_vals.end());
}
// rewrite with extended rewriter
- slem = d_tds->getExtRewriter()->extendedRewrite(slem);
+ slem = extendedRewrite(slem);
// collect all variables in slem
expr::getSymbols(slem, d_refinement_lemma_vars);
std::vector<Node> waiting;
#include "theory/quantifiers/sygus/enum_stream_substitution.h"
+#include <numeric> // for std::iota
+#include <sstream>
+
#include "expr/dtype_cons.h"
#include "options/base_options.h"
#include "options/datatypes_options.h"
#include "options/quantifiers_options.h"
#include "printer/printer.h"
#include "theory/quantifiers/sygus/term_database_sygus.h"
-
-#include <numeric> // for std::iota
-#include <sstream>
+#include "theory/rewriter.h"
using namespace cvc5::kind;
namespace theory {
namespace quantifiers {
-EnumStreamPermutation::EnumStreamPermutation(quantifiers::TermDbSygus* tds)
+EnumStreamPermutation::EnumStreamPermutation(TermDbSygus* tds)
: d_tds(tds), d_first(true), d_curr_ind(0)
{
}
{
d_first = false;
Node bultin_value = d_tds->sygusToBuiltin(d_value, d_value.getType());
- d_perm_values.insert(
- d_tds->getExtRewriter()->extendedRewrite(bultin_value));
+ d_perm_values.insert(Rewriter::callExtendedRewrite(bultin_value));
return d_value;
}
unsigned n_classes = d_perm_state_class.size();
<< " ......perm builtin is " << bultin_perm_value;
if (options::sygusSymBreakDynamic())
{
- bultin_perm_value =
- d_tds->getExtRewriter()->extendedRewrite(bultin_perm_value);
+ bultin_perm_value = Rewriter::callExtendedRewrite(bultin_perm_value);
Trace("synth-stream-concrete-debug")
<< " and rewrites to " << bultin_perm_value;
}
d_tds->sygusToBuiltin(comb_value, comb_value.getType());
if (options::sygusSymBreakDynamic())
{
- builtin_comb_value =
- d_tds->getExtRewriter()->extendedRewrite(builtin_comb_value);
+ builtin_comb_value = Rewriter::callExtendedRewrite(builtin_comb_value);
}
if (Trace.isOn("synth-stream-concrete"))
{
namespace theory {
namespace quantifiers {
-EnumValueManager::EnumValueManager(Node e,
+EnumValueManager::EnumValueManager(Env& env,
QuantifiersState& qs,
QuantifiersInferenceManager& qim,
TermRegistry& tr,
SygusStatistics& s,
+ Node e,
bool hasExamples)
- : d_enum(e),
+ : EnvObj(env),
+ d_enum(e),
d_qstate(qs),
d_qim(qim),
d_treg(tr),
#define CVC5__THEORY__QUANTIFIERS__SYGUS__ENUM_VALUE_MANAGER_H
#include "expr/node.h"
+#include "smt/env_obj.h"
#include "theory/quantifiers/sygus/enum_val_generator.h"
#include "theory/quantifiers/sygus/example_eval_cache.h"
#include "theory/quantifiers/sygus/sygus_enumerator_callback.h"
* not actively generated, or may be determined by the (fast) enumerator
* when it is actively generated.
*/
-class EnumValueManager
+class EnumValueManager : protected EnvObj
{
public:
- EnumValueManager(Node e,
+ EnumValueManager(Env& env,
QuantifiersState& qs,
QuantifiersInferenceManager& qim,
TermRegistry& tr,
SygusStatistics& s,
+ Node e,
bool hasExamples);
~EnumValueManager();
/**
#include "theory/quantifiers/sygus/sygus_enumerator_basic.h"
#include "options/datatypes_options.h"
+#include "theory/rewriter.h"
using namespace cvc5::kind;
using namespace std;
if (options::sygusSymBreakDynamic())
{
Node nextb = d_tds->sygusToBuiltin(d_currTerm);
- nextb = d_tds->getExtRewriter()->extendedRewrite(nextb);
+ nextb = Rewriter::callExtendedRewrite(nextb);
if (d_cache.find(nextb) == d_cache.end())
{
d_cache.insert(nextb);
#include "theory/quantifiers/sygus/example_eval_cache.h"
#include "theory/quantifiers/sygus/sygus_stats.h"
#include "theory/quantifiers/sygus_sampler.h"
+#include "theory/rewriter.h"
namespace cvc5 {
namespace theory {
bool SygusEnumeratorCallback::addTerm(Node n, std::unordered_set<Node>& bterms)
{
Node bn = datatypes::utils::sygusToBuiltin(n);
- Node bnr = d_extr.extendedRewrite(bn);
+ Node bnr = Rewriter::callExtendedRewrite(bn);
if (d_stats != nullptr)
{
++(d_stats->d_enumTermsRewrite);
Node d_enum;
/** The type of enum */
TypeNode d_tn;
- /** extended rewriter */
- ExtendedRewriter d_extr;
/** pointer to the statistics */
SygusStatistics* d_stats;
};
#include "options/quantifiers_options.h"
#include "theory/quantifiers/sygus/term_database_sygus.h"
#include "theory/quantifiers/term_util.h"
+#include "theory/rewriter.h"
using namespace std;
using namespace cvc5::kind;
if (index == dt[c].getNumArgs())
{
Node gt = tds->mkGeneric(dt, c, pre);
- gt = tds->getExtRewriter()->extendedRewrite(gt);
+ gt = Rewriter::callExtendedRewrite(gt);
terms.push_back(gt);
return;
}
{
TypeNode tn = nvn.getType();
Node nbv = tds->sygusToBuiltin(nvn, tn);
- Node nbvr = tds->getExtRewriter()->extendedRewrite(nbv);
+ Node nbvr = Rewriter::callExtendedRewrite(nbv);
Trace("sygus-sb-mexp-debug") << " min-exp check : " << nbv << " -> " << nbvr
<< std::endl;
bool exc_arg = false;
{
TypeNode tn = nvn.getType();
Node nbv = tds->sygusToBuiltin(nvn, tn);
- Node nbvr = tds->getExtRewriter()->extendedRewrite(nbv);
+ Node nbvr = Rewriter::callExtendedRewrite(nbv);
if (tds->involvesDivByZero(nbvr))
{
Trace("sygus-sb-mexp") << "sb-min-exp : " << tds->sygusToBuiltin(nvn)
{
TypeNode tn = nvn.getType();
Node nbv = tds->sygusToBuiltin(nvn, tn);
- Node nbvr = tds->getExtRewriter()->extendedRewrite(nbv);
+ Node nbvr = Rewriter::callExtendedRewrite(nbv);
// if for any of the examples, it is not contained, then we can exclude
for (unsigned i = 0; i < d_neg_con_indices.size(); i++)
{
// Apply extended rewriting on the lemma. This helps utilities like
// SygusEnumerator more easily recognize the shape of this lemma, e.g.
// ( ~is-ite(x) or ( ~is-ite(x) ^ P ) ) --> ~is-ite(x).
- lem = d_tds->getExtRewriter()->extendedRewrite(lem);
+ lem = extendedRewrite(lem);
Trace("sygus-pbe") << " static redundant op lemma : " << lem
<< std::endl;
// Register as a symmetry breaking lemma with the term database.
std::vector<Node> base_results;
TypeNode xtn = e.getType();
Node bv = d_tds->sygusToBuiltin(v, xtn);
- bv = d_tds->getExtRewriter()->extendedRewrite(bv);
+ bv = extendedRewrite(bv);
Trace("sygus-sui-enum") << "PBE Compute Examples for " << bv << std::endl;
// compte the results (should be cached)
ExampleEvalCache* eec = d_parent->getExampleEvalCache(e);
namespace theory {
namespace quantifiers {
-SynthConjecture::SynthConjecture(QuantifiersState& qs,
+SynthConjecture::SynthConjecture(Env& env,
+ QuantifiersState& qs,
QuantifiersInferenceManager& qim,
QuantifiersRegistry& qr,
TermRegistry& tr,
SygusStatistics& s)
- : d_qstate(qs),
+ : EnvObj(env),
+ d_qstate(qs),
d_qim(qim),
d_qreg(qr),
d_treg(tr),
d_tds(tr.getTermDatabaseSygus()),
d_verify(qs.options(), qs.getLogicInfo(), d_tds),
d_hasSolution(false),
- d_ceg_si(new CegSingleInv(qs.getEnv(), tr, s)),
+ d_ceg_si(new CegSingleInv(env, tr, s)),
d_templInfer(new SygusTemplateInfer),
d_ceg_proc(new SynthConjectureProcess),
d_ceg_gc(new CegGrammarConstructor(d_tds, this)),
- d_sygus_rconst(new SygusRepairConst(qs.getEnv(), d_tds)),
+ d_sygus_rconst(new SygusRepairConst(env, d_tds)),
d_exampleInfer(new ExampleInfer(d_tds)),
d_ceg_pbe(new SygusPbe(qs, qim, d_tds, this)),
d_ceg_cegis(new Cegis(qs, qim, d_tds, this)),
}
Trace("sygus-engine") << "Check side condition..." << std::endl;
Trace("cegqi-debug") << "Check side condition : " << sc << std::endl;
- Env& env = d_qstate.getEnv();
- Result r = checkWithSubsolver(sc, env.getOptions(), env.getLogicInfo());
+ Result r = checkWithSubsolver(sc, options(), logicInfo());
Trace("cegqi-debug") << "...got side condition : " << r << std::endl;
if (r == Result::UNSAT)
{
Node f = d_tds->getSynthFunForEnumerator(e);
bool hasExamples = (d_exampleInfer->hasExamples(f)
&& d_exampleInfer->getNumExamples(f) != 0);
- d_enumManager[e].reset(
- new EnumValueManager(e, d_qstate, d_qim, d_treg, d_stats, hasExamples));
+ d_enumManager[e].reset(new EnumValueManager(
+ d_env, d_qstate, d_qim, d_treg, d_stats, e, hasExamples));
EnumValueManager* eman = d_enumManager[e].get();
// set up the examples
if (hasExamples)
d_exprm.find(prog);
if (its == d_exprm.end())
{
- d_exprm[prog].reset(new ExpressionMinerManager(d_qstate.getEnv()));
+ d_exprm[prog].reset(new ExpressionMinerManager(d_env));
ExpressionMinerManager* emm = d_exprm[prog].get();
emm->initializeSygus(
d_tds, d_candidates[i], options::sygusSamples(), true);
#include <memory>
+#include "smt/env_obj.h"
#include "theory/quantifiers/expr_miner_manager.h"
#include "theory/quantifiers/sygus/ce_guided_single_inv.h"
#include "theory/quantifiers/sygus/cegis.h"
* determines which approach and optimizations are applicable to the
* conjecture, and has interfaces for implementing them.
*/
-class SynthConjecture
+class SynthConjecture : protected EnvObj
{
public:
- SynthConjecture(QuantifiersState& qs,
+ SynthConjecture(Env& env,
+ QuantifiersState& qs,
QuantifiersInferenceManager& qim,
QuantifiersRegistry& qr,
TermRegistry& tr,
namespace theory {
namespace quantifiers {
-SynthEngine::SynthEngine(QuantifiersState& qs,
+SynthEngine::SynthEngine(Env& env,
+ QuantifiersState& qs,
QuantifiersInferenceManager& qim,
QuantifiersRegistry& qr,
TermRegistry& tr)
: QuantifiersModule(qs, qim, qr, tr), d_conj(nullptr), d_sqp(qs.getEnv())
{
d_conjs.push_back(std::unique_ptr<SynthConjecture>(
- new SynthConjecture(qs, qim, qr, tr, d_statistics)));
+ new SynthConjecture(env, qs, qim, qr, tr, d_statistics)));
d_conj = d_conjs.back().get();
}
// allocate a new synthesis conjecture if not assigned
if (d_conjs.back()->isAssigned())
{
- d_conjs.push_back(std::unique_ptr<SynthConjecture>(
- new SynthConjecture(d_qstate, d_qim, d_qreg, d_treg, d_statistics)));
+ d_conjs.push_back(std::unique_ptr<SynthConjecture>(new SynthConjecture(
+ d_env, d_qstate, d_qim, d_qreg, d_treg, d_statistics)));
}
d_conjs.back()->assign(q);
}
typedef context::CDHashMap<Node, bool> NodeBoolMap;
public:
- SynthEngine(QuantifiersState& qs,
+ SynthEngine(Env& env,
+ QuantifiersState& qs,
QuantifiersInferenceManager& qim,
QuantifiersRegistry& qr,
TermRegistry& tr);
return os;
}
-TermDbSygus::TermDbSygus(QuantifiersState& qs)
- : d_qstate(qs),
+TermDbSygus::TermDbSygus(Env& env, QuantifiersState& qs)
+ : EnvObj(env),
+ d_qstate(qs),
d_syexp(new SygusExplain(this)),
- d_ext_rw(new ExtendedRewriter(true)),
d_eval(new Evaluator),
d_funDefEval(new FunDefEvaluator),
d_eval_unfold(new SygusEvalUnfold(this))
}
if (options::sygusExtRew())
{
- ret = getExtRewriter()->extendedRewrite(ret);
+ ret = extendedRewrite(ret);
}
// use rewriting, possibly involving recursive functions
ret = rewriteNode(ret);
#include <unordered_set>
#include "expr/dtype.h"
+#include "smt/env_obj.h"
#include "theory/evaluator.h"
#include "theory/quantifiers/extended_rewrite.h"
#include "theory/quantifiers/fun_def_evaluator.h"
std::ostream& operator<<(std::ostream& os, EnumeratorRole r);
// TODO :issue #1235 split and document this class
-class TermDbSygus {
+class TermDbSygus : protected EnvObj
+{
public:
- TermDbSygus(QuantifiersState& qs);
+ TermDbSygus(Env& env, QuantifiersState& qs);
~TermDbSygus() {}
/** Finish init, which sets the inference manager */
void finishInit(QuantifiersInferenceManager* qim);
//------------------------------utilities
/** get the explanation utility */
SygusExplain* getExplain() { return d_syexp.get(); }
- /** get the extended rewrite utility */
- ExtendedRewriter* getExtRewriter() { return d_ext_rw.get(); }
/** get the evaluator */
Evaluator* getEvaluator() { return d_eval.get(); }
/** (recursive) function evaluator utility */
//------------------------------utilities
/** sygus explanation */
std::unique_ptr<SygusExplain> d_syexp;
- /** extended rewriter */
- std::unique_ptr<ExtendedRewriter> d_ext_rw;
/** evaluator */
std::unique_ptr<Evaluator> d_eval;
/** (recursive) function evaluator utility */
/** get anchor */
static Node getAnchor( Node n );
static unsigned getAnchorDepth( Node n );
-
};
} // namespace quantifiers
namespace theory {
namespace quantifiers {
-TermRegistry::TermRegistry(QuantifiersState& qs, QuantifiersRegistry& qr)
+TermRegistry::TermRegistry(Env& env,
+ QuantifiersState& qs,
+ QuantifiersRegistry& qr)
: d_presolve(qs.getUserContext(), true),
d_presolveCache(qs.getUserContext()),
d_termEnum(new TermEnumeration),
if (options::sygus() || options::sygusInst())
{
// must be constructed here since it is required for datatypes finistInit
- d_sygusTdb.reset(new TermDbSygus(qs));
+ d_sygusTdb.reset(new TermDbSygus(env, qs));
}
Trace("quant-engine-debug") << "Initialize quantifiers engine." << std::endl;
Trace("quant-engine-debug")
using NodeSet = context::CDHashSet<Node>;
public:
- TermRegistry(QuantifiersState& qs,
- QuantifiersRegistry& qr);
+ TermRegistry(Env& env, QuantifiersState& qs, QuantifiersRegistry& qr);
/** Finish init, which sets the inference manager on modules of this class */
void finishInit(FirstOrderModel* fm, QuantifiersInferenceManager* qim);
/** Presolve */
: Theory(THEORY_QUANTIFIERS, env, out, valuation),
d_qstate(env, valuation, logicInfo()),
d_qreg(),
- d_treg(d_qstate, d_qreg),
+ d_treg(env, d_qstate, d_qreg),
d_qim(env, *this, d_qstate, d_qreg, d_treg, d_pnm),
d_qengine(nullptr)
{
// construct the quantifiers engine
d_qengine.reset(
- new QuantifiersEngine(d_qstate, d_qreg, d_treg, d_qim, d_pnm));
+ new QuantifiersEngine(env, d_qstate, d_qreg, d_treg, d_qim, d_pnm));
// indicate we are using the quantifiers theory state object
d_theoryState = &d_qstate;
namespace theory {
QuantifiersEngine::QuantifiersEngine(
+ Env& env,
quantifiers::QuantifiersState& qs,
quantifiers::QuantifiersRegistry& qr,
quantifiers::TermRegistry& tr,
quantifiers::QuantifiersInferenceManager& qim,
ProofNodeManager* pnm)
- : d_qstate(qs),
+ : EnvObj(env),
+ d_qstate(qs),
d_qim(qim),
d_te(nullptr),
d_pnm(pnm),
// Initialize the modules and the utilities here.
d_qmodules.reset(new quantifiers::QuantifiersModules);
d_qmodules->initialize(
- d_qstate, d_qim, d_qreg, d_treg, d_builder.get(), d_modules);
+ d_env, d_qstate, d_qim, d_qreg, d_treg, d_builder.get(), d_modules);
if (d_qmodules->d_rel_dom.get())
{
d_util.push_back(d_qmodules->d_rel_dom.get());
#include "context/cdhashmap.h"
#include "context/cdhashset.h"
#include "context/cdlist.h"
+#include "smt/env_obj.h"
#include "theory/quantifiers/quant_util.h"
namespace cvc5 {
class TermRegistry;
}
-// TODO: organize this more/review this, github issue #1163
-class QuantifiersEngine {
+/**
+ * The main class that manages techniques for quantified formulas.
+ */
+class QuantifiersEngine : protected EnvObj
+{
friend class ::cvc5::TheoryEngine;
typedef context::CDHashMap<Node, bool> BoolMap;
typedef context::CDHashSet<Node> NodeSet;
public:
- QuantifiersEngine(quantifiers::QuantifiersState& qstate,
+ QuantifiersEngine(Env& env,
+ quantifiers::QuantifiersState& qstate,
quantifiers::QuantifiersRegistry& qr,
quantifiers::TermRegistry& tr,
quantifiers::QuantifiersInferenceManager& qim,
std::map<Node, Node> d_quants_red_lem;
/** Number of rounds we have instantiated */
uint32_t d_numInstRoundsLemma;
-};/* class QuantifiersEngine */
+}; /* class QuantifiersEngine */
} // namespace theory
} // namespace cvc5
NodeBuilder d_builder;
};
-RewriteResponse identityRewrite(RewriteEnvironment* re, TNode n)
-{
- return RewriteResponse(REWRITE_DONE, n);
-}
Node Rewriter::rewrite(TNode node) {
if (node.getNumChildren() == 0)
return getInstance()->rewriteTo(theoryOf(node), node);
}
+Node Rewriter::callExtendedRewrite(TNode node, bool aggr)
+{
+ return getInstance()->extendedRewrite(node, aggr);
+}
+
+Node Rewriter::extendedRewrite(TNode node, bool aggr)
+{
+ quantifiers::ExtendedRewriter er(*this, aggr);
+ return er.extendedRewrite(node);
+}
+
TrustNode Rewriter::rewriteWithProof(TNode node,
bool isExtEq)
{
}
if (idr == MethodId::RW_EXT_REWRITE)
{
- quantifiers::ExtendedRewriter er;
- return er.extendedRewrite(n);
+ return extendedRewrite(n);
}
if (idr == MethodId::RW_REWRITE_EQ_EXT)
{
namespace theory {
-namespace builtin {
-class BuiltinProofRuleChecker;
-}
-
-/**
- * The rewrite environment holds everything that the individual rewrites have
- * access to.
- */
-class RewriteEnvironment
-{
-};
-
-/**
- * The identity rewrite just returns the original node.
- *
- * @param re The rewrite environment
- * @param n The node to rewrite
- * @return The original node
- */
-RewriteResponse identityRewrite(RewriteEnvironment* re, TNode n);
-
/**
* The main rewriter class.
*/
class Rewriter {
- friend builtin::BuiltinProofRuleChecker;
public:
Rewriter();
/**
+ * !!! Temporary until static access to rewriter is eliminated.
+ *
* Rewrites the node using theoryOf() to determine which rewriter to
* use on the node.
*/
static Node rewrite(TNode node);
+ /**
+ * !!! Temporary until static access to rewriter is eliminated.
+ */
+ static Node callExtendedRewrite(TNode node, bool aggr = true);
/**
* Rewrites the equality node using theoryOf() to determine which rewriter to
*/
Node rewriteEqualityExt(TNode node);
+ /**
+ * Extended rewrite of the given node. This method is implemented by a
+ * custom ExtendRewriter class that wraps this class to perform custom
+ * rewrites (usually those that are not useful for solving, but e.g. useful
+ * for SyGuS symmetry breaking).
+ * @param node The node to rewrite
+ * @param aggr Whether to perform aggressive rewrites.
+ */
+ Node extendedRewrite(TNode node, bool aggr = true);
+
/**
* Rewrite with proof production, which is managed by the term conversion
* proof generator managed by this class (d_tpg). This method requires a call
/** Theory rewriters used by this rewriter instance */
TheoryRewriter* d_theoryRewriters[theory::THEORY_LAST];
- RewriteEnvironment d_re;
-
/** The proof generator */
std::unique_ptr<TConvProofGenerator> d_tpg;
#ifdef CVC5_ASSERTIONS
#include "expr/node.h"
#include "expr/node_manager.h"
#include "test_smt.h"
-#include "theory/quantifiers/extended_rewrite.h"
#include "theory/rewriter.h"
#include "theory/strings/arith_entail.h"
#include "theory/strings/sequences_rewriter.h"
namespace cvc5 {
using namespace theory;
-using namespace theory::quantifiers;
using namespace theory::strings;
namespace test {
{
TestSmt::SetUp();
Options opts;
- d_rewriter.reset(new ExtendedRewriter(true));
+ d_rewriter = d_smtEngine->getRewriter();
}
- std::unique_ptr<ExtendedRewriter> d_rewriter;
+ Rewriter* d_rewriter;
void inNormalForm(Node t)
{
Node slen_y = d_nodeManager->mkNode(kind::STRING_LENGTH, y);
Node x_plus_slen_y = d_nodeManager->mkNode(kind::PLUS, x, slen_y);
- Node x_plus_slen_y_eq_zero = Rewriter::rewrite(
+ Node x_plus_slen_y_eq_zero = d_rewriter->rewrite(
d_nodeManager->mkNode(kind::EQUAL, x_plus_slen_y, zero));
// x + (str.len y) = 0 |= 0 >= x --> true
ASSERT_FALSE(
ArithEntail::checkWithAssumption(x_plus_slen_y_eq_zero, zero, x, true));
- Node x_plus_slen_y_plus_z_eq_zero = Rewriter::rewrite(d_nodeManager->mkNode(
+ Node x_plus_slen_y_plus_z_eq_zero = d_rewriter->rewrite(d_nodeManager->mkNode(
kind::EQUAL, d_nodeManager->mkNode(kind::PLUS, x_plus_slen_y, z), zero));
// x + (str.len y) + z = 0 |= 0 > x --> false
x_plus_slen_y_plus_z_eq_zero, zero, x, true));
Node x_plus_slen_y_plus_slen_y_eq_zero =
- Rewriter::rewrite(d_nodeManager->mkNode(
+ d_rewriter->rewrite(d_nodeManager->mkNode(
kind::EQUAL,
d_nodeManager->mkNode(kind::PLUS, x_plus_slen_y, slen_y),
zero));
Node six = d_nodeManager->mkConst(Rational(6));
Node x_plus_five = d_nodeManager->mkNode(kind::PLUS, x, five);
Node x_plus_five_lt_six =
- Rewriter::rewrite(d_nodeManager->mkNode(kind::LT, x_plus_five, six));
+ d_rewriter->rewrite(d_nodeManager->mkNode(kind::LT, x_plus_five, six));
// x + 5 < 6 |= 0 >= x --> true
ASSERT_TRUE(
Node neg_x = d_nodeManager->mkNode(kind::UMINUS, x);
Node x_plus_five_lt_five =
- Rewriter::rewrite(d_nodeManager->mkNode(kind::LT, x_plus_five, five));
+ d_rewriter->rewrite(d_nodeManager->mkNode(kind::LT, x_plus_five, five));
// x + 5 < 5 |= -x >= 0 --> true
ASSERT_TRUE(ArithEntail::checkWithAssumption(
ArithEntail::checkWithAssumption(x_plus_five_lt_five, zero, x, false));
// 0 < x |= x >= (str.len (int.to.str x))
- Node assm = Rewriter::rewrite(d_nodeManager->mkNode(kind::LT, zero, x));
+ Node assm = d_rewriter->rewrite(d_nodeManager->mkNode(kind::LT, zero, x));
ASSERT_TRUE(ArithEntail::checkWithAssumption(
assm,
x,
#include "theory/arith/nl/nl_lemma_utils.h"
#include "theory/arith/nl/poly_conversion.h"
#include "theory/arith/theory_arith.h"
-#include "theory/quantifiers/extended_rewrite.h"
+#include "theory/rewriter.h"
#include "theory/theory.h"
#include "theory/theory_engine.h"
#include "util/poly_util.h"
EXPECT_NE(rewritten, d_nodeManager->mkConst(false));
}
{
- quantifiers::ExtendedRewriter extrew;
- Node rewritten = extrew.extendedRewrite(orig);
+ Node rewritten = Rewriter::callExtendedRewrite(orig);
EXPECT_EQ(rewritten, d_nodeManager->mkConst(false));
}
}
projects / cvc5.git / commitdiff