diff options
Diffstat (limited to 'src/theory/quantifiers/sygus/synth_conjecture.cpp')
-rw-r--r-- | src/theory/quantifiers/sygus/synth_conjecture.cpp | 11 |
1 files changed, 7 insertions, 4 deletions
diff --git a/src/theory/quantifiers/sygus/synth_conjecture.cpp b/src/theory/quantifiers/sygus/synth_conjecture.cpp index 03449589b..73fc53d86 100644 --- a/src/theory/quantifiers/sygus/synth_conjecture.cpp +++ b/src/theory/quantifiers/sygus/synth_conjecture.cpp @@ -43,9 +43,12 @@ namespace CVC4 { namespace theory { namespace quantifiers { -SynthConjecture::SynthConjecture(QuantifiersEngine* qe, SynthEngine* p) +SynthConjecture::SynthConjecture(QuantifiersEngine* qe, + SynthEngine* p, + SygusStatistics& s) : d_qe(qe), d_parent(p), + d_stats(s), d_tds(qe->getTermDatabaseSygus()), d_hasSolution(false), d_ceg_si(new CegSingleInv(qe, this)), @@ -1058,7 +1061,7 @@ void SynthConjecture::printSynthSolution(std::ostream& out) ss << prog; std::string f(ss.str()); f.erase(f.begin()); - ++(d_parent->d_statistics.d_solutions); + ++(d_stats.d_solutions); bool is_unique_term = true; @@ -1102,11 +1105,11 @@ void SynthConjecture::printSynthSolution(std::ostream& out) is_unique_term = d_exprm[prog].addTerm(sol, out, rew_print); if (rew_print) { - ++(d_parent->d_statistics.d_candidate_rewrites_print); + ++(d_stats.d_candidate_rewrites_print); } if (!is_unique_term) { - ++(d_parent->d_statistics.d_filtered_solutions); + ++(d_stats.d_filtered_solutions); } } if (is_unique_term) |