diff options
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 */ |