QuantifiersInferenceManager& qim,
TermDbSygus* tds,
SynthConjecture* p)
- : Cegis(qs, qim, tds, p), d_sygus_unif(p), d_u_enum_manager(qs, qim, tds, p)
+ : Cegis(qs, qim, tds, p),
+ d_sygus_unif(qs.getEnv(), p),
+ d_u_enum_manager(qs, qim, tds, p)
{
}
for (const Node& c : candidates)
{
Assert(ei->hasExamples(c));
- d_sygus_unif[c].reset(new SygusUnifIo(d_parent));
+ d_sygus_unif[c].reset(new SygusUnifIo(d_env, d_parent));
Trace("sygus-pbe") << "Initialize unif utility for " << c << "..."
<< std::endl;
std::map<Node, std::vector<Node>> strategy_lemmas;
namespace theory {
namespace quantifiers {
-SygusUnif::SygusUnif() : d_tds(nullptr), d_enableMinimality(false) {}
+SygusUnif::SygusUnif(Env& env)
+ : EnvObj(env), d_tds(nullptr), d_enableMinimality(false)
+{
+}
+
SygusUnif::~SygusUnif() {}
void SygusUnif::initializeCandidate(
d_tds = tds;
d_candidates.push_back(f);
// initialize the strategy
- d_strategy[f].initialize(tds, f, enums);
+ d_strategy.emplace(f, SygusUnifStrategy(d_env));
+ d_strategy.at(f).initialize(tds, f, enums);
}
Node SygusUnif::getMinimalTerm(const std::vector<Node>& terms)
* Based on the above, solutions can be constructed via calls to
* constructSolution.
*/
-class SygusUnif
+class SygusUnif : protected EnvObj
{
public:
- SygusUnif();
+ SygusUnif(Env& env);
virtual ~SygusUnif();
/** initialize candidate
getLeavesInternal(vals, pol, v, 0, -2);
}
-SygusUnifIo::SygusUnifIo(SynthConjecture* p)
- : d_parent(p),
+SygusUnifIo::SygusUnifIo(Env& env, SynthConjecture* p)
+ : SygusUnif(env),
+ d_parent(p),
d_check_sol(false),
d_cond_count(0),
d_sol_term_size(0),
d_ecache.clear();
SygusUnif::initializeCandidate(tds, f, enums, strategy_lemmas);
// learn redundant operators based on the strategy
- d_strategy[f].staticLearnRedundantOps(strategy_lemmas);
+ d_strategy.at(f).staticLearnRedundantOps(strategy_lemmas);
}
void SygusUnifIo::notifyEnumeration(Node e, Node v, std::vector<Node>& lemmas)
Assert(!d_examples.empty());
Assert(d_examples.size() == d_examples_out.size());
- EnumInfo& ei = d_strategy[c].getEnumInfo(e);
+ EnumInfo& ei = d_strategy.at(c).getEnumInfo(e);
// The explanation for why the current value should be excluded in future
// iterations.
Node exp_exc;
for (const Node& xs : ei.d_enum_slave)
{
Assert(srmap.find(xs) == srmap.end());
- EnumInfo& eiv = d_strategy[c].getEnumInfo(xs);
+ EnumInfo& eiv = d_strategy.at(c).getEnumInfo(xs);
Node templ = eiv.d_template;
if (!templ.isNull())
{
for (unsigned s = 0; s < ei.d_enum_slave.size(); s++)
{
Node xs = ei.d_enum_slave[s];
- EnumInfo& eiv = d_strategy[c].getEnumInfo(xs);
+ EnumInfo& eiv = d_strategy.at(c).getEnumInfo(xs);
EnumCache& ecv = d_ecache[xs];
Trace("sygus-sui-enum") << "Process " << xs << " from " << s << std::endl;
// bool prevIsCover = false;
initializeConstructSol();
initializeConstructSolFor(c);
// call the virtual construct solution method
- Node e = d_strategy[c].getRootEnumerator();
+ Node e = d_strategy.at(c).getRootEnumerator();
Node vcc = constructSol(c, e, role_equal, 1, lemmas);
// if we constructed the solution, and we either did not previously have
// a solution, or the new solution is better (smaller).
<< "Is " << e << " is str.contains exclusion?" << std::endl;
d_use_str_contains_eexc[e] = true;
Node c = d_candidate;
- EnumInfo& ei = d_strategy[c].getEnumInfo(e);
+ EnumInfo& ei = d_strategy.at(c).getEnumInfo(e);
for (const Node& sn : ei.d_enum_slave)
{
- EnumInfo& eis = d_strategy[c].getEnumInfo(sn);
+ EnumInfo& eis = d_strategy.at(c).getEnumInfo(sn);
EnumRole er = eis.getRole();
if (er != enum_io && er != enum_concat_term)
{
<< "Check enumerator exclusion for " << e << " -> "
<< d_tds->sygusToBuiltin(v) << " based on str.contains." << std::endl;
std::vector<unsigned> cmp_indices;
- for (unsigned i = 0, size = results.size(); i < size; i++)
+ for (size_t i = 0, size = results.size(); i < size; i++)
{
// If the result is not constant, then it is worthless. It does not
// impact whether the term is excluded.
Trace("sygus-sui-cterm-debug")
<< " " << results[i] << " <> " << d_examples_out[i];
Node cont = nm->mkNode(STRING_CONTAINS, d_examples_out[i], results[i]);
- Node contr = Rewriter::rewrite(cont);
+ Node contr = rewrite(cont);
if (contr == d_false)
{
cmp_indices.push_back(i);
Trace("sygus-sui-dt-debug") << std::endl;
}
// enumerator type info
- EnumTypeInfo& tinfo = d_strategy[f].getEnumTypeInfo(etn);
+ EnumTypeInfo& tinfo = d_strategy.at(f).getEnumTypeInfo(etn);
// get the enumerator information
- EnumInfo& einfo = d_strategy[f].getEnumInfo(e);
+ EnumInfo& einfo = d_strategy.at(f).getEnumInfo(e);
EnumCache& ecache = d_ecache[e];
friend class UnifContextIo;
public:
- SygusUnifIo(SynthConjecture* p);
+ SygusUnifIo(Env& env, SynthConjecture* p);
~SygusUnifIo();
/** initialize
namespace theory {
namespace quantifiers {
-SygusUnifRl::SygusUnifRl(SynthConjecture* p)
- : d_parent(p), d_useCondPool(false), d_useCondPoolIGain(false)
+SygusUnifRl::SygusUnifRl(Env& env, SynthConjecture* p)
+ : SygusUnif(env),
+ d_parent(p),
+ d_useCondPool(false),
+ d_useCondPoolIGain(false)
{
}
SygusUnifRl::~SygusUnifRl() {}
}
// register the strategy
registerStrategy(f, enums, restrictions.d_unused_strategies);
- d_strategy[f].staticLearnRedundantOps(strategy_lemmas, restrictions);
+ d_strategy.at(f).staticLearnRedundantOps(strategy_lemmas, restrictions);
// Copy candidates and check whether CegisUnif for any of them
if (d_unif_candidates.find(f) != d_unif_candidates.end())
{
TNode cand = n[0];
Node tmp = n.substitute(cand, it1->second);
// should be concrete, can just use the rewriter
- nv = Rewriter::rewrite(tmp);
+ nv = rewrite(tmp);
Trace("sygus-unif-rl-purify")
<< "PurifyLemma : model value for " << tmp << " is " << nv << "\n";
}
Trace("sygus-unif-rl-purify")
<< "PurifyLemma : adding model eq " << model_guards.back() << "\n";
}
- nb = Rewriter::rewrite(nb);
+ nb = rewrite(nb);
// every non-top level application of function-to-synthesize must be reduced
// to a concrete constant
Assert(!ensureConst || nb.isConst());
model_guards.push_back(plem);
plem = NodeManager::currentNM()->mkNode(OR, model_guards);
}
- plem = Rewriter::rewrite(plem);
+ plem = rewrite(plem);
Trace("sygus-unif-rl-purify") << "Purified lemma : " << plem << "\n";
Trace("sygus-unif-rl-purify") << "Collect new evaluation points...\n";
}
initializeConstructSolFor(c);
Node v = constructSol(
- c, d_strategy[c].getRootEnumerator(), role_equal, 0, lemmas);
+ c, d_strategy.at(c).getRootEnumerator(), role_equal, 0, lemmas);
if (v.isNull())
{
// we continue trying to build solutions to accumulate potentitial
Trace("sygus-unif-sol") << "ConstructSol: SygusRL : " << e << std::endl;
// retrieve strategy information
TypeNode etn = e.getType();
- EnumTypeInfo& tinfo = d_strategy[f].getEnumTypeInfo(etn);
+ EnumTypeInfo& tinfo = d_strategy.at(f).getEnumTypeInfo(etn);
StrategyNode& snode = tinfo.getStrategyNode(nrole);
if (nrole != role_equal)
{
{
Trace("sygus-unif-rl-strat")
<< "Strategy for " << f << " is : " << std::endl;
- d_strategy[f].debugPrint("sygus-unif-rl-strat");
+ d_strategy.at(f).debugPrint("sygus-unif-rl-strat");
}
Trace("sygus-unif-rl-strat") << "Register..." << std::endl;
- Node e = d_strategy[f].getRootEnumerator();
+ Node e = d_strategy.at(f).getRootEnumerator();
std::map<Node, std::map<NodeRole, bool>> visited;
registerStrategyNode(f, e, role_equal, visited, enums, unused_strats);
}
}
visited[e][nrole] = true;
TypeNode etn = e.getType();
- EnumTypeInfo& tinfo = d_strategy[f].getEnumTypeInfo(etn);
+ EnumTypeInfo& tinfo = d_strategy.at(f).getEnumTypeInfo(etn);
StrategyNode& snode = tinfo.getStrategyNode(nrole);
for (unsigned j = 0, size = snode.d_strats.size(); j < size; j++)
{
d_cenum_to_stratpt[cond].clear();
}
// register that this strategy node has a decision tree construction
- d_stratpt_to_dt[e].initialize(cond, this, &d_strategy[f], strategy_index);
+ d_stratpt_to_dt[e].initialize(cond, this, &d_strategy.at(f), strategy_index);
// associate conditional enumerator with strategy node
d_cenum_to_stratpt[cond].push_back(e);
}
class SygusUnifRl : public SygusUnif
{
public:
- SygusUnifRl(SynthConjecture* p);
+ SygusUnifRl(Env& env, SynthConjecture* p);
~SygusUnifRl();
/** initialize */
#include "theory/quantifiers/sygus/sygus_unif.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;
teut = children.size() == 1
? children[0]
: nm->mkNode(eut.getKind(), children);
- teut = Rewriter::rewrite(teut);
+ teut = rewrite(teut);
}
else
{
#define CVC5__THEORY__QUANTIFIERS__SYGUS_UNIF_STRAT_H
#include <map>
+
#include "expr/node.h"
+#include "smt/env_obj.h"
namespace cvc5 {
namespace theory {
* the grammar of the function to synthesize f. This tree is represented by
* the above classes.
*/
-class SygusUnifStrategy
+class SygusUnifStrategy : protected EnvObj
{
public:
- SygusUnifStrategy() : d_tds(nullptr) {}
+ SygusUnifStrategy(Env& env) : EnvObj(env), d_tds(nullptr) {}
/** initialize
*
* This initializes this class with function-to-synthesize f. We also call
projects / cvc5.git / commitdiff