diff options
| author | Andrew Reynolds <andrew.j.reynolds@gmail.com> | 2020-01-31 10:14:31 -0600 |
|---|---|---|
| committer | GitHub <noreply@github.com> | 2020-01-31 10:14:31 -0600 |
| commit | 8bf406cd70b5883a7894485006834ff69682dbd6 (patch) | |
| tree | 3612ea25a4547a231a253d28a002092401ffe236 /src/theory/quantifiers/sygus/synth_conjecture.h | |
| parent | f069ec7aee5a3433b54598defdc4af53e3573670 (diff) | |
Refactor sygus stats (#3684)
Diffstat (limited to 'src/theory/quantifiers/sygus/synth_conjecture.h')
| -rw-r--r-- | src/theory/quantifiers/sygus/synth_conjecture.h | 5 |
1 files changed, 4 insertions, 1 deletions
diff --git a/src/theory/quantifiers/sygus/synth_conjecture.h b/src/theory/quantifiers/sygus/synth_conjecture.h index db9872ec3..a001572c2 100644 --- a/src/theory/quantifiers/sygus/synth_conjecture.h +++ b/src/theory/quantifiers/sygus/synth_conjecture.h @@ -30,6 +30,7 @@ #include "theory/quantifiers/sygus/sygus_pbe.h" #include "theory/quantifiers/sygus/sygus_process_conj.h" #include "theory/quantifiers/sygus/sygus_repair_const.h" +#include "theory/quantifiers/sygus/sygus_stats.h" namespace CVC4 { namespace theory { @@ -71,7 +72,7 @@ class EnumValGenerator class SynthConjecture { public: - SynthConjecture(QuantifiersEngine* qe, SynthEngine* p); + SynthConjecture(QuantifiersEngine* qe, SynthEngine* p, SygusStatistics& s); ~SynthConjecture(); /** presolve */ void presolve(); @@ -174,6 +175,8 @@ class SynthConjecture QuantifiersEngine* d_qe; /** pointer to the synth engine that owns this */ SynthEngine* d_parent; + /** reference to the statistics of parent */ + SygusStatistics& d_stats; /** term database sygus of d_qe */ TermDbSygus* d_tds; /** The feasible guard. */ |