Trace("dt-sygus") << " * DT builtin : " << n << " -> " << bvr << std::endl;
unsigned sz = utils::getSygusTermSize(nv);
if( d_tds->involvesDivByZero( bvr ) ){
- quantifiers::DivByZeroSygusInvarianceTest dbzet;
+ quantifiers::DivByZeroSygusInvarianceTest dbzet(d_env.getRewriter());
Trace("sygus-sb-mexp-debug") << "Minimize explanation for div-by-zero in "
<< bv << std::endl;
registerSymBreakLemmaForValue(a, nv, dbzet, Node::null(), var_count);
// generalize the explanation for why the analog of bad_val
// is equivalent to bvr
- quantifiers::EquivSygusInvarianceTest eset;
+ quantifiers::EquivSygusInvarianceTest eset(d_env.getRewriter());
eset.init(d_tds, tn, aconj, a, bvr);
Trace("sygus-sb-mexp-debug") << "Minimize explanation for eval[" << d_tds->sygusToBuiltin( bad_val ) << "] = " << bvr << std::endl;
namespace theory {
namespace quantifiers {
+BvInverter::BvInverter(Rewriter* r) : d_rewriter(r) {}
+
/*---------------------------------------------------------------------------*/
Node BvInverter::getSolveVariable(TypeNode tn)
TNode solve_var = getSolveVariable(tn);
// condition should be rewritten
- Node new_cond = Rewriter::rewrite(cond);
- if (new_cond != cond)
+ Node new_cond = cond;
+ if (d_rewriter != nullptr)
{
- Trace("cegqi-bv-skvinv-debug")
- << "Condition " << cond << " was rewritten to " << new_cond
- << std::endl;
+ new_cond = d_rewriter->rewrite(cond);
+ if (new_cond != cond)
+ {
+ Trace("cegqi-bv-skvinv-debug")
+ << "Condition " << cond << " was rewritten to " << new_cond
+ << std::endl;
+ }
}
// optimization : if condition is ( x = solve_var ) should just return
// solve_var and not introduce a Skolem this can happen when we ask for
namespace cvc5 {
namespace theory {
+
+class Rewriter;
+
namespace quantifiers {
/** BvInverterQuery
class BvInverter
{
public:
- BvInverter() {}
+ BvInverter(Rewriter* r = nullptr);
~BvInverter() {}
/** get dummy fresh variable of type tn, used as argument for sv */
Node getSolveVariable(TypeNode tn);
BvInverterQuery* m);
private:
- /** Dummy variables for each type */
- std::map<TypeNode, Node> d_solve_var;
-
/** Helper function for getPathToPv */
Node getPathToPv(Node lit,
Node pv,
* to this call is null.
*/
Node getInversionNode(Node cond, TypeNode tn, BvInverterQuery* m);
+ /** (Optional) rewriter used as helper in getInversionNode */
+ Rewriter* d_rewriter;
+ /** Dummy variables for each type */
+ std::map<TypeNode, Node> d_solve_var;
};
} // namespace quantifiers
if (options().quantifiers.cegqiBv)
{
// if doing instantiation for BV, need the inverter class
- d_bv_invert.reset(new BvInverter);
+ d_bv_invert.reset(new BvInverter(env.getRewriter()));
}
if (options().quantifiers.cegqiNestedQE)
{
#include "theory/quantifiers/quant_bound_inference.h"
#include "theory/quantifiers/fmf/bounded_integers.h"
-#include "theory/rewriter.h"
#include "util/rational.h"
using namespace cvc5::kind;
Cardinality c = tn.getCardinality();
if (!c.isLargeFinite())
{
- NodeManager* nm = NodeManager::currentNM();
- Node card = nm->mkConstInt(Rational(c.getFiniteCardinality()));
// check if less than fixed upper bound
- Node oth = nm->mkConstInt(Rational(maxCard));
- Node eq = nm->mkNode(LEQ, card, oth);
- eq = Rewriter::rewrite(eq);
- mc = eq.isConst() && eq.getConst<bool>();
+ mc = (c.getFiniteCardinality() < Integer(maxCard));
}
}
return mc;
{
// check if it rewrites to a constant
Node nn = nm->mkNode(EQUAL, no, ret[i][j]);
- nn = Rewriter::rewrite(nn);
childrenIte.push_back(nn);
- if (nn.isConst())
+ // check if it will rewrite to a constant
+ if (no == ret[i][j] || (no.isConst() && ret[i][j].isConst()))
{
doRewrite = true;
}
namespace theory {
namespace quantifiers {
+SingleInvocationPartition::SingleInvocationPartition(Env& env)
+ : EnvObj(env), d_has_input_funcs(false)
+{
+}
+
bool SingleInvocationPartition::init(Node n)
{
// first, get types of arguments for functions
d_input_funcs.end(),
d_input_func_sks.begin(),
d_input_func_sks.end());
- cr = TermUtil::getQuantSimplify(cr);
+ cr = getQuantSimplify(cr);
cr = cr.substitute(d_input_func_sks.begin(),
d_input_func_sks.end(),
d_input_funcs.begin(),
Trace(c) << std::endl;
}
+Node SingleInvocationPartition::getQuantSimplify(TNode n) const
+{
+ std::unordered_set<Node> fvs;
+ expr::getFreeVariables(n, fvs);
+ if (fvs.empty())
+ {
+ return rewrite(n);
+ }
+ std::vector<Node> bvs(fvs.begin(), fvs.end());
+ NodeManager* nm = NodeManager::currentNM();
+ Node q = nm->mkNode(FORALL, nm->mkNode(BOUND_VAR_LIST, bvs), n);
+ q = rewrite(q);
+ return TermUtil::getRemoveQuantifiers(q);
+}
+
} // namespace quantifiers
} // namespace theory
} // namespace cvc5
#include "expr/node.h"
#include "expr/subs.h"
#include "expr/type_node.h"
+#include "smt/env_obj.h"
namespace cvc5 {
namespace theory {
* see Example 5 of Reynolds et al. SYNT 2017.
*
*/
-class SingleInvocationPartition
+class SingleInvocationPartition : protected EnvObj
{
public:
- SingleInvocationPartition() : d_has_input_funcs(false) {}
+ SingleInvocationPartition(Env& env);
~SingleInvocationPartition() {}
/** initialize this partition for formula n, with input functions funcs
*
/** get the and node corresponding to d_conjuncts[index] */
Node getConjunct(int index);
+ /** Quantified simplify (treat free variables in n as quantified and run
+ * rewriter) */
+ Node getQuantSimplify(TNode n) const;
};
} // namespace quantifiers
CegSingleInv::CegSingleInv(Env& env, TermRegistry& tr, SygusStatistics& s)
: EnvObj(env),
d_isSolved(false),
- d_sip(new SingleInvocationPartition),
+ d_sip(new SingleInvocationPartition(env)),
d_srcons(new SygusReconstruct(env, tr.getTermDatabaseSygus(), s)),
d_single_invocation(false),
d_treg(tr)
Assert(!lem.isNull());
std::map<Node, Node> visited;
std::map<Node, std::vector<Node> > exp;
- EvalSygusInvarianceTest vsit;
+ EvalSygusInvarianceTest vsit(d_env.getRewriter());
Trace("sygus-cref-eval") << "Check refinement lemma conjunct " << lem
<< " against current model." << std::endl;
Trace("sygus-cref-eval2") << "Check refinement lemma conjunct " << lem
namespace theory {
namespace quantifiers {
-EnumStreamPermutation::EnumStreamPermutation(TermDbSygus* tds)
- : d_tds(tds), d_first(true), d_curr_ind(0)
+EnumStreamPermutation::EnumStreamPermutation(Env& env, TermDbSygus* tds)
+ : EnvObj(env), 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(Rewriter::callExtendedRewrite(bultin_value));
+ d_perm_values.insert(extendedRewrite(bultin_value));
return d_value;
}
unsigned n_classes = d_perm_state_class.size();
bultin_perm_value = d_tds->sygusToBuiltin(perm_value, perm_value.getType());
Trace("synth-stream-concrete-debug")
<< " ......perm builtin is " << bultin_perm_value;
- if (options::sygusSymBreakDynamic())
+ if (options().datatypes.sygusSymBreakDynamic)
{
- bultin_perm_value = Rewriter::callExtendedRewrite(bultin_perm_value);
+ bultin_perm_value = extendedRewrite(bultin_perm_value);
Trace("synth-stream-concrete-debug")
<< " and rewrites to " << bultin_perm_value;
}
return true;
}
-EnumStreamSubstitution::EnumStreamSubstitution(quantifiers::TermDbSygus* tds)
- : d_tds(tds), d_stream_permutations(tds), d_curr_ind(0)
+EnumStreamSubstitution::EnumStreamSubstitution(Env& env, TermDbSygus* tds)
+ : EnvObj(env), d_tds(tds), d_stream_permutations(env, tds), d_curr_ind(0)
{
}
// construction (unless it's equiv to a constant, e.g. true / false)
Node builtin_comb_value =
d_tds->sygusToBuiltin(comb_value, comb_value.getType());
- if (options::sygusSymBreakDynamic())
+ if (options().datatypes.sygusSymBreakDynamic)
{
- builtin_comb_value = Rewriter::callExtendedRewrite(builtin_comb_value);
+ builtin_comb_value = extendedRewrite(builtin_comb_value);
}
if (Trace.isOn("synth-stream-concrete"))
{
return new_comb;
}
+EnumStreamConcrete::EnumStreamConcrete(Env& env, TermDbSygus* tds)
+ : EnumValGenerator(env), d_ess(env, tds)
+{
+}
+
void EnumStreamConcrete::initialize(Node e) { d_ess.initialize(e.getType()); }
void EnumStreamConcrete::addValue(Node v)
{
#define CVC5__THEORY__QUANTIFIERS__SYGUS__ENUM_STREAM_SUBSTITUTION_H
#include "expr/node.h"
+#include "smt/env_obj.h"
#include "theory/quantifiers/sygus/enum_val_generator.h"
namespace cvc5 {
* Generates a new value (modulo rewriting) when queried in which its variables
* are permuted (see EnumStreamSubstitution for more details).
*/
-class EnumStreamPermutation
+class EnumStreamPermutation : protected EnvObj
{
public:
- EnumStreamPermutation(TermDbSygus* tds);
+ EnumStreamPermutation(Env& env, TermDbSygus* tds);
~EnumStreamPermutation() {}
/** resets utility
*
* Therefore when streaming concrete values, permutations and combinations are
* generated by the product of the permutations and combinations of each class.
*/
-class EnumStreamSubstitution
+class EnumStreamSubstitution : protected EnvObj
{
public:
- EnumStreamSubstitution(TermDbSygus* tds);
+ EnumStreamSubstitution(Env& env, TermDbSygus* tds);
~EnumStreamSubstitution() {}
/** initializes utility
*
class EnumStreamConcrete : public EnumValGenerator
{
public:
- EnumStreamConcrete(TermDbSygus* tds) : d_ess(tds) {}
+ EnumStreamConcrete(Env& env, TermDbSygus* tds);
/** initialize this class with enumerator e */
void initialize(Node e) override;
/** get that value v was enumerated */
#define CVC5__THEORY__QUANTIFIERS__SYGUS__ENUM_VAL_GENERATOR_H
#include "expr/node.h"
+#include "smt/env_obj.h"
namespace cvc5 {
namespace theory {
* values" a1, ..., an, ..., and generate a (possibly larger) stream of
* "concrete values" c11, ..., c1{m_1}, ..., cn1, ... cn{m_n}, ....
*/
-class EnumValGenerator
+class EnumValGenerator : protected EnvObj
{
public:
+ EnumValGenerator(Env& env) : EnvObj(env) {}
virtual ~EnumValGenerator() {}
/** initialize this class with enumerator e */
virtual void initialize(Node e) = 0;
{
if (d_tds->isVariableAgnosticEnumerator(e))
{
- d_evg.reset(new EnumStreamConcrete(d_tds));
+ d_evg = std::make_unique<EnumStreamConcrete>(d_env, d_tds);
}
else
{
if (options().quantifiers.sygusActiveGenMode
== options::SygusActiveGenMode::ENUM_BASIC)
{
- d_evg.reset(new EnumValGeneratorBasic(d_tds, e.getType()));
+ d_evg =
+ std::make_unique<EnumValGeneratorBasic>(d_env, d_tds, e.getType());
}
else if (options().quantifiers.sygusActiveGenMode
== options::SygusActiveGenMode::RANDOM)
{
- d_evg.reset(new SygusRandomEnumerator(d_tds));
+ d_evg = std::make_unique<SygusRandomEnumerator>(d_env, d_tds);
}
else
{
// use the default output for the output of sygusRewVerify
out = options().base.out;
}
- d_secd.reset(new SygusEnumeratorCallbackDefault(
- e, &d_stats, d_eec.get(), d_samplerRrV.get(), out));
+ d_secd = std::make_unique<SygusEnumeratorCallbackDefault>(
+ d_env, e, &d_stats, d_eec.get(), d_samplerRrV.get(), out);
}
// if sygus repair const is enabled, we enumerate terms with free
// variables as arguments to any-constant constructors
- d_evg.reset(
- new SygusEnumerator(d_tds,
- d_secd.get(),
- &d_stats,
- false,
- options().quantifiers.sygusRepairConst));
+ d_evg = std::make_unique<SygusEnumerator>(
+ d_env,
+ d_tds,
+ d_secd.get(),
+ &d_stats,
+ false,
+ options().quantifiers.sygusRepairConst);
}
}
Trace("sygus-active-gen")
NodeManager* nm = NodeManager::currentNM();
SkolemManager* sm = nm->getSkolemManager();
- d_enumerator.reset(new SygusEnumerator(tds, nullptr, &s, true));
+ d_enumerator = std::make_unique<SygusEnumerator>(env, tds, nullptr, &s, true);
d_enumerator->initialize(sm->mkDummySkolem("sygus_rcons", stn));
d_crd.reset(new CandidateRewriteDatabase(env, true, false, true, false));
// since initial samples are not always useful for equivalence checks, set
namespace theory {
namespace quantifiers {
-SygusEnumerator::SygusEnumerator(TermDbSygus* tds,
+SygusEnumerator::SygusEnumerator(Env& env,
+ TermDbSygus* tds,
SygusEnumeratorCallback* sec,
SygusStatistics* s,
bool enumShapes,
bool enumAnyConstHoles)
- : d_tds(tds),
+ : EnumValGenerator(env),
+ d_tds(tds),
d_sec(sec),
d_stats(s),
d_enumShapes(enumShapes),
// allocate the default callback
if (d_sec == nullptr && options::sygusSymBreakDynamic())
{
- d_secd.reset(new SygusEnumeratorCallbackDefault(e, d_stats));
+ d_secd =
+ std::make_unique<SygusEnumeratorCallbackDefault>(d_env, e, d_stats);
d_sec = d_secd.get();
}
d_etype = d_enum.getType();
{
// substitute its active guard by true and rewrite
Node slem = lem.substitute(agt, truent);
- slem = Rewriter::rewrite(slem);
+ slem = rewrite(slem);
// break into conjuncts
std::vector<Node> sblc;
if (slem.getKind() == AND)
{
public:
/**
+ * @param env Reference to the environment
* @param tds Pointer to the term database, required if enumShapes or
* enumAnyConstHoles is true, or if we want to include symmetry breaking from
* lemmas stored in the sygus term database,
* @param enumAnyConstHoles If true, this enumerator will generate terms where
* free variables are the arguments to any-constant constructors.
*/
- SygusEnumerator(TermDbSygus* tds = nullptr,
+ SygusEnumerator(Env& env,
+ TermDbSygus* tds = nullptr,
SygusEnumeratorCallback* sec = nullptr,
SygusStatistics* s = nullptr,
bool enumShapes = false,
namespace theory {
namespace quantifiers {
-EnumValGeneratorBasic::EnumValGeneratorBasic(TermDbSygus* tds, TypeNode tn)
- : d_tds(tds), d_te(tn)
+EnumValGeneratorBasic::EnumValGeneratorBasic(Env& env,
+ TermDbSygus* tds,
+ TypeNode tn)
+ : EnumValGenerator(env), d_tds(tds), d_te(tn)
{
}
return false;
}
d_currTerm = *d_te;
- if (options::sygusSymBreakDynamic())
+ if (options().datatypes.sygusSymBreakDynamic)
{
Node nextb = d_tds->sygusToBuiltin(d_currTerm);
- nextb = Rewriter::callExtendedRewrite(nextb);
+ nextb = extendedRewrite(nextb);
if (d_cache.find(nextb) == d_cache.end())
{
d_cache.insert(nextb);
class EnumValGeneratorBasic : public EnumValGenerator
{
public:
- EnumValGeneratorBasic(TermDbSygus* tds, TypeNode tn);
+ EnumValGeneratorBasic(Env& env, TermDbSygus* tds, TypeNode tn);
~EnumValGeneratorBasic() {}
/** initialize (do nothing) */
void initialize(Node e) override {}
namespace theory {
namespace quantifiers {
-SygusEnumeratorCallback::SygusEnumeratorCallback(Node e, SygusStatistics* s)
- : d_enum(e), d_stats(s)
+SygusEnumeratorCallback::SygusEnumeratorCallback(Env& env,
+ Node e,
+ SygusStatistics* s)
+ : EnvObj(env), d_enum(e), d_stats(s)
{
d_tn = e.getType();
}
bool SygusEnumeratorCallback::addTerm(Node n, std::unordered_set<Node>& bterms)
{
Node bn = datatypes::utils::sygusToBuiltin(n);
- Node bnr = Rewriter::callExtendedRewrite(bn);
+ Node bnr = extendedRewrite(bn);
if (d_stats != nullptr)
{
++(d_stats->d_enumTermsRewrite);
}
SygusEnumeratorCallbackDefault::SygusEnumeratorCallbackDefault(
+ Env& env,
Node e,
SygusStatistics* s,
ExampleEvalCache* eec,
SygusSampler* ssrv,
std::ostream* out)
- : SygusEnumeratorCallback(e, s), d_eec(eec), d_samplerRrV(ssrv), d_out(out)
+ : SygusEnumeratorCallback(env, e, s),
+ d_eec(eec),
+ d_samplerRrV(ssrv),
+ d_out(out)
{
}
void SygusEnumeratorCallbackDefault::notifyTermInternal(Node n,
#include <unordered_set>
#include "expr/node.h"
+#include "smt/env_obj.h"
#include "theory/quantifiers/extended_rewrite.h"
namespace cvc5 {
* provide custom criteria for whether or not enumerated values should be
* considered.
*/
-class SygusEnumeratorCallback
+class SygusEnumeratorCallback : protected EnvObj
{
public:
- SygusEnumeratorCallback(Node e, SygusStatistics* s = nullptr);
+ SygusEnumeratorCallback(Env& env, Node e, SygusStatistics* s = nullptr);
virtual ~SygusEnumeratorCallback() {}
/**
* Add term, return true if the term should be considered in the enumeration.
class SygusEnumeratorCallbackDefault : public SygusEnumeratorCallback
{
public:
- SygusEnumeratorCallbackDefault(Node e,
+ SygusEnumeratorCallbackDefault(Env& env,
+ Node e,
SygusStatistics* s = nullptr,
ExampleEvalCache* eec = nullptr,
SygusSampler* ssrv = nullptr,
}
else
{
- EvalSygusInvarianceTest esit;
+ EvalSygusInvarianceTest esit(d_env.getRewriter());
eval_children.insert(
eval_children.end(), it->second[i].begin(), it->second[i].end());
Node conj = nm->mkNode(DT_SYGUS_EVAL, eval_children);
sfvl = preGrammarType.getDType().getSygusVarList();
tn = preGrammarType;
// normalize type, if user-provided
- SygusGrammarNorm sygus_norm(d_tds);
+ SygusGrammarNorm sygus_norm(d_env, d_tds);
tn = sygus_norm.normalizeSygusType(tn, sfvl);
}else{
sfvl = SygusUtils::getSygusArgumentListForSynthFun(sf);
// Do beta reduction on the operator so that its arguments match the
// fresh variables of the lambda (op) we are constructing below.
sop = datatypes::utils::mkSygusTerm(sop, opLArgs);
- sop = Rewriter::rewrite(sop);
}
opCArgs.push_back(unresAnyConst);
Node coeff = nm->mkBoundVar(types[i]);
return d_children[op_pos[ind]].getOrMakeType(tn, unres_tn, op_pos, ind + 1);
}
-SygusGrammarNorm::SygusGrammarNorm(TermDbSygus* tds) : d_tds(tds) {}
+SygusGrammarNorm::SygusGrammarNorm(Env& env, TermDbSygus* tds)
+ : EnvObj(env), d_tds(tds)
+{
+}
SygusGrammarNorm::TypeObject::TypeObject(TypeNode src_tn, TypeNode unres_tn)
: d_tn(src_tn),
Trace("sygus-gnorm") << " #cons = " << op_pos.size() << " / "
<< dt.getNumConstructors() << std::endl;
// look for redundant constructors to drop
- if (options::sygusMinGrammar() && dt.getNumConstructors() == op_pos.size())
+ if (options().quantifiers.sygusMinGrammar
+ && dt.getNumConstructors() == op_pos.size())
{
- SygusRedundantCons src;
+ SygusRedundantCons src(d_env);
src.initialize(d_tds, tn);
std::vector<unsigned> rindices;
src.getRedundant(rindices);
#include "expr/node.h"
#include "expr/sygus_datatype.h"
#include "expr/type_node.h"
+#include "smt/env_obj.h"
namespace cvc5 {
namespace theory {
* These lighweight transformations are always applied, independently of the
* normalization option being enabled.
*/
-class SygusGrammarNorm
+class SygusGrammarNorm : protected EnvObj
{
public:
- SygusGrammarNorm(TermDbSygus* tds);
+ SygusGrammarNorm(Env& env, TermDbSygus* tds);
~SygusGrammarNorm() {}
/** creates a normalized typenode from a given one.
*
if (index == dt[c].getNumArgs())
{
Node gt = tds->mkGeneric(dt, c, pre);
- gt = Rewriter::callExtendedRewrite(gt);
+ gt = extendedRewrite(gt);
terms.push_back(gt);
return;
}
#include <vector>
#include "expr/node.h"
+#include "smt/env_obj.h"
namespace cvc5 {
namespace theory {
* where tn is a sygus tn. Then, use getRedundant and/or isRedundant to get the
* indicies of the constructors of tn that are redundant.
*/
-class SygusRedundantCons
+class SygusRedundantCons : protected EnvObj
{
public:
- SygusRedundantCons() {}
+ SygusRedundantCons(Env& env) : EnvObj(env) {}
~SygusRedundantCons() {}
/** register type tn
*
{
TypeNode tn = nvn.getType();
Node nbv = tds->sygusToBuiltin(nvn, tn);
- Node nbvr = Rewriter::callExtendedRewrite(nbv);
+ Node nbvr = d_rewriter->extendedRewrite(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 = Rewriter::callExtendedRewrite(nbv);
+ Node nbvr = d_rewriter->extendedRewrite(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 = Rewriter::callExtendedRewrite(nbv);
+ Node nbvr = d_rewriter->extendedRewrite(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++)
{
Node cont =
NodeManager::currentNM()->mkNode(kind::STRING_CONTAINS, out, nbvre);
Trace("sygus-pbe-cterm-debug") << "Check: " << cont << std::endl;
- Node contr = Rewriter::rewrite(cont);
+ Node contr = d_rewriter->extendedRewrite(cont);
if (!contr.isConst())
{
if (d_isUniversal)
namespace cvc5 {
namespace theory {
+
+class Rewriter;
+
namespace quantifiers {
class TermDbSygus;
class SygusInvarianceTest
{
public:
+ SygusInvarianceTest(Rewriter* r) : d_rewriter(r) {}
virtual ~SygusInvarianceTest() {}
/** Is nvn invariant with respect to this test ?
/** set updated term */
void setUpdatedTerm(Node n) { d_update_nvn = n; }
protected:
+ /** Pointer to the rewriter */
+ Rewriter* d_rewriter;
/** result of the node that satisfies this invariant */
Node d_update_nvn;
/** check whether nvn[ x ] is invariant */
class EvalSygusInvarianceTest : public SygusInvarianceTest
{
public:
- EvalSygusInvarianceTest()
- : d_kind(kind::UNDEFINED_KIND), d_is_conjunctive(false)
+ EvalSygusInvarianceTest(Rewriter* r)
+ : SygusInvarianceTest(r),
+ d_kind(kind::UNDEFINED_KIND),
+ d_is_conjunctive(false)
{
}
class EquivSygusInvarianceTest : public SygusInvarianceTest
{
public:
- EquivSygusInvarianceTest() : d_conj(nullptr) {}
+ EquivSygusInvarianceTest(Rewriter* r)
+ : SygusInvarianceTest(r), d_conj(nullptr)
+ {
+ }
/** initialize this invariance test
* tn is the sygus type for e
class DivByZeroSygusInvarianceTest : public SygusInvarianceTest
{
public:
- DivByZeroSygusInvarianceTest() {}
+ DivByZeroSygusInvarianceTest(Rewriter* r) : SygusInvarianceTest(r) {}
protected:
/** checks whether nvn involves division by zero. */
class NegContainsSygusInvarianceTest : public SygusInvarianceTest
{
public:
- NegContainsSygusInvarianceTest() : d_isUniversal(false) {}
+ NegContainsSygusInvarianceTest(Rewriter* r)
+ : SygusInvarianceTest(r), d_isUniversal(false)
+ {
+ }
/** initialize this invariance test
* e is the enumerator which we are reasoning about (associated with a synth
}
Node cn_subs =
cn.substitute(vars.begin(), vars.end(), subs.begin(), subs.end());
- cn_subs = Rewriter::rewrite(cn_subs);
- n = Rewriter::rewrite(n);
+ cn_subs = rewrite(cn_subs);
+ n = rewrite(n);
return cn_subs == n;
}
SkolemManager* sm = nm->getSkolemManager();
Trace("cegqi-qep") << "Compute single invocation for " << q << "..."
<< std::endl;
- quantifiers::SingleInvocationPartition sip;
+ quantifiers::SingleInvocationPartition sip(d_env);
std::vector<Node> funcs0;
funcs0.insert(funcs0.end(), q[0].begin(), q[0].end());
sip.init(funcs0, body);
// Generate the next sygus term.
n = incrementH();
bn = d_tds->sygusToBuiltin(n);
- bn = Rewriter::callExtendedRewrite(bn);
+ bn = extendedRewrite(bn);
// Ensure that the builtin counterpart is unique (up to rewriting).
} while (d_cache.find(bn) != d_cache.cend());
d_cache.insert(bn);
{
TypeNode tn = n.getType();
Node bn = d_tds->sygusToBuiltin(n);
- bn = Rewriter::callExtendedRewrite(bn);
+ bn = extendedRewrite(bn);
// Did we calculate the size of `n` before?
if (d_size.find(n) == d_size.cend())
{
*
* @param tds pointer to term database sygus.
*/
- SygusRandomEnumerator(TermDbSygus* tds) : d_tds(tds){};
+ SygusRandomEnumerator(Env& env, TermDbSygus* tds)
+ : EnumValGenerator(env), d_tds(tds)
+ {
+ }
/** Initialize this class with enumerator `e`. */
void initialize(Node e) override;
if (!cmp_indices.empty())
{
// we check invariance with respect to a negative contains test
- NegContainsSygusInvarianceTest ncset;
+ NegContainsSygusInvarianceTest ncset(d_env.getRewriter());
if (isConditional)
{
ncset.setUniversal();
return getRemoveQuantifiers2( n, visited );
}
-//quantified simplify
-Node TermUtil::getQuantSimplify( Node n ) {
- std::unordered_set<Node> fvs;
- expr::getFreeVariables(n, fvs);
- if (fvs.empty())
- {
- return Rewriter::rewrite( n );
- }
- std::vector<Node> bvs;
- bvs.insert(bvs.end(), fvs.begin(), fvs.end());
- NodeManager* nm = NodeManager::currentNM();
- Node q = nm->mkNode(FORALL, nm->mkNode(BOUND_VAR_LIST, bvs), n);
- q = Rewriter::rewrite(q);
- return getRemoveQuantifiers(q);
-}
-
void TermUtil::computeInstConstContains(Node n, std::vector<Node>& ics)
{
computeVarContainsInternal(n, INST_CONSTANT, ics);
int32_t offset,
int32_t& status)
{
+ Assert(val.isConst() && val.getType() == tn);
Node val_o;
- Node offset_val = mkTypeValue(tn, offset);
status = -1;
- if (!offset_val.isNull())
+ if (tn.isRealOrInt())
{
- if (tn.isRealOrInt())
- {
- val_o = Rewriter::rewrite(
- NodeManager::currentNM()->mkNode(PLUS, val, offset_val));
- status = 0;
- }
- else if (tn.isBitVector())
- {
- val_o = Rewriter::rewrite(
- NodeManager::currentNM()->mkNode(BITVECTOR_ADD, val, offset_val));
- }
+ Rational vval = val.getConst<Rational>();
+ Rational oval(offset);
+ status = 0;
+ return NodeManager::currentNM()->mkConstRealOrInt(tn, vval + oval);
+ }
+ else if (tn.isBitVector())
+ {
+ BitVector vval = val.getConst<BitVector>();
+ uint32_t uv = static_cast<uint32_t>(offset);
+ BitVector oval(tn.getConst<BitVectorSize>(), uv);
+ return NodeManager::currentNM()->mkConst(vval + oval);
}
return val_o;
}
public:
//remove quantifiers
static Node getRemoveQuantifiers( Node n );
- //quantified simplify (treat free variables in n as quantified and run rewriter)
- static Node getQuantSimplify( Node n );
private:
/** adds the set of nodes of kind k in n to vars */
projects / cvc5.git / commitdiff