diff options
Diffstat (limited to 'src/theory/quantifiers/sygus/synth_conjecture.cpp')
| -rw-r--r-- | src/theory/quantifiers/sygus/synth_conjecture.cpp | 34 |
1 files changed, 17 insertions, 17 deletions
diff --git a/src/theory/quantifiers/sygus/synth_conjecture.cpp b/src/theory/quantifiers/sygus/synth_conjecture.cpp index 3e7095c12..da021227a 100644 --- a/src/theory/quantifiers/sygus/synth_conjecture.cpp +++ b/src/theory/quantifiers/sygus/synth_conjecture.cpp @@ -45,29 +45,31 @@ namespace cvc5 { 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_stats(s), d_tds(tr.getTermDatabaseSygus()), - d_verify(qs.options(), qs.getLogicInfo(), d_tds), + d_verify(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)), - d_ceg_cegisUnif(new CegisUnif(qs, qim, d_tds, this)), - d_sygus_ccore(new CegisCoreConnective(qs, qim, d_tds, this)), + d_ceg_pbe(new SygusPbe(env, qs, qim, d_tds, this)), + d_ceg_cegis(new Cegis(env, qs, qim, d_tds, this)), + d_ceg_cegisUnif(new CegisUnif(env, qs, qim, d_tds, this)), + d_sygus_ccore(new CegisCoreConnective(env, qs, qim, d_tds, this)), d_master(nullptr), d_set_ce_sk_vars(false), d_repair_index(0), @@ -513,7 +515,7 @@ bool SynthConjecture::doCheck() { if (printDebug) { - const Options& sopts = d_qstate.options(); + const Options& sopts = options(); std::ostream& out = *sopts.base.out; out << "(sygus-candidate "; Assert(d_quant[0].getNumChildren() == candidate_values.size()); @@ -609,8 +611,7 @@ bool SynthConjecture::checkSideCondition(const std::vector<Node>& cvals) const } 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) { @@ -763,8 +764,8 @@ EnumValueManager* SynthConjecture::getEnumValueManagerFor(Node e) 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) @@ -800,8 +801,7 @@ void SynthConjecture::printAndContinueStream(const std::vector<Node>& enums, Assert(d_master != nullptr); // we have generated a solution, print it // get the current output stream - const Options& sopts = d_qstate.options(); - printSynthSolutionInternal(*sopts.base.out); + printSynthSolutionInternal(*options().base.out); excludeCurrentSolution(enums, values); } @@ -885,7 +885,7 @@ void SynthConjecture::printSynthSolutionInternal(std::ostream& out) 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); |