diff options
| author | Andrew Reynolds <andrew.j.reynolds@gmail.com> | 2020-11-05 23:06:13 -0600 |
|---|---|---|
| committer | GitHub <noreply@github.com> | 2020-11-05 23:06:13 -0600 |
| commit | 04dc5b60462dc367fe1b99254c215957006f7b21 (patch) | |
| tree | e13c0360026bb3c6d19d5f61e0034345c98306e9 /src/theory/quantifiers/sygus/synth_conjecture.cpp | |
| parent | af18cd275f340d1896c3b635dbeecbea2e521db1 (diff) | |
Split sygus template inference to its own file (#5388)
This splits techniques for inferring templates for functions-to-synthesize to their own file.
This is work towards cleaning up the single invocation utility, which will be undergoing some additions.
Diffstat (limited to 'src/theory/quantifiers/sygus/synth_conjecture.cpp')
| -rw-r--r-- | src/theory/quantifiers/sygus/synth_conjecture.cpp | 18 |
1 files changed, 11 insertions, 7 deletions
diff --git a/src/theory/quantifiers/sygus/synth_conjecture.cpp b/src/theory/quantifiers/sygus/synth_conjecture.cpp index c65ac9e65..2b4eba3b7 100644 --- a/src/theory/quantifiers/sygus/synth_conjecture.cpp +++ b/src/theory/quantifiers/sygus/synth_conjecture.cpp @@ -50,7 +50,8 @@ SynthConjecture::SynthConjecture(QuantifiersEngine* qe, d_stats(s), d_tds(qe->getTermDatabaseSygus()), d_hasSolution(false), - d_ceg_si(new CegSingleInv(qe, this)), + d_ceg_si(new CegSingleInv(qe)), + d_templInfer(new SygusTemplateInfer), d_ceg_proc(new SynthConjectureProcess(qe)), d_ceg_gc(new CegGrammarConstructor(qe, this)), d_sygus_rconst(new SygusRepairConst(qe)), @@ -116,15 +117,18 @@ void SynthConjecture::assign(Node q) { d_ceg_si->initialize(d_simp_quant); d_simp_quant = d_ceg_si->getSimplifiedConjecture(); + if (!d_ceg_si->isSingleInvocation()) + { + d_templInfer->initialize(d_simp_quant); + } // carry the templates - for (unsigned i = 0; i < q[0].getNumChildren(); i++) + for (const Node& v : q[0]) { - Node v = q[0][i]; - Node templ = d_ceg_si->getTemplate(v); + Node templ = d_templInfer->getTemplate(v); if (!templ.isNull()) { templates[v] = templ; - templates_arg[v] = d_ceg_si->getTemplateArg(v); + templates_arg[v] = d_templInfer->getTemplateArg(v); } } } @@ -1334,7 +1338,7 @@ bool SynthConjecture::getSynthSolutionsInternal(std::vector<Node>& sols, // check if there was a template Node sf = d_quant[0][i]; - Node templ = d_ceg_si->getTemplate(sf); + Node templ = d_templInfer->getTemplate(sf); if (!templ.isNull()) { Trace("cegqi-inv-debug") @@ -1342,7 +1346,7 @@ bool SynthConjecture::getSynthSolutionsInternal(std::vector<Node>& sols, // if it was not embedded into the grammar if (!options::sygusTemplEmbedGrammar()) { - TNode templa = d_ceg_si->getTemplateArg(sf); + TNode templa = d_templInfer->getTemplateArg(sf); // make the builtin version of the full solution sol = d_tds->sygusToBuiltin(sol, sol.getType()); Trace("cegqi-inv") << "Builtin version of solution is : " << sol |