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.h | |
| 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.h')
| -rw-r--r-- | src/theory/quantifiers/sygus/synth_conjecture.h | 3 |
1 files changed, 3 insertions, 0 deletions
diff --git a/src/theory/quantifiers/sygus/synth_conjecture.h b/src/theory/quantifiers/sygus/synth_conjecture.h index 5572032b6..7f499b1b3 100644 --- a/src/theory/quantifiers/sygus/synth_conjecture.h +++ b/src/theory/quantifiers/sygus/synth_conjecture.h @@ -33,6 +33,7 @@ #include "theory/quantifiers/sygus/sygus_process_conj.h" #include "theory/quantifiers/sygus/sygus_repair_const.h" #include "theory/quantifiers/sygus/sygus_stats.h" +#include "theory/quantifiers/sygus/template_infer.h" namespace CVC4 { namespace theory { @@ -216,6 +217,8 @@ class SynthConjecture std::unique_ptr<DecisionStrategy> d_feasible_strategy; /** single invocation utility */ std::unique_ptr<CegSingleInv> d_ceg_si; + /** template inference utility */ + std::unique_ptr<SygusTemplateInfer> d_templInfer; /** utility for static preprocessing and analysis of conjectures */ std::unique_ptr<SynthConjectureProcess> d_ceg_proc; /** grammar utility */ |