From 8bf406cd70b5883a7894485006834ff69682dbd6 Mon Sep 17 00:00:00 2001 From: Andrew Reynolds Date: Fri, 31 Jan 2020 10:14:31 -0600 Subject: [PATCH] Refactor sygus stats (#3684) --- src/CMakeLists.txt | 2 + src/theory/quantifiers/sygus/sygus_stats.cpp | 53 +++++++++++++++++++ src/theory/quantifiers/sygus/sygus_stats.h | 52 ++++++++++++++++++ .../quantifiers/sygus/synth_conjecture.cpp | 11 ++-- .../quantifiers/sygus/synth_conjecture.h | 5 +- src/theory/quantifiers/sygus/synth_engine.cpp | 32 +---------- src/theory/quantifiers/sygus/synth_engine.h | 18 ++----- 7 files changed, 123 insertions(+), 50 deletions(-) create mode 100644 src/theory/quantifiers/sygus/sygus_stats.cpp create mode 100644 src/theory/quantifiers/sygus/sygus_stats.h diff --git a/src/CMakeLists.txt b/src/CMakeLists.txt index 271ceb045..f5f6a83c9 100644 --- a/src/CMakeLists.txt +++ b/src/CMakeLists.txt @@ -592,6 +592,8 @@ libcvc4_add_sources( theory/quantifiers/sygus/sygus_process_conj.h theory/quantifiers/sygus/sygus_repair_const.cpp theory/quantifiers/sygus/sygus_repair_const.h + theory/quantifiers/sygus/sygus_stats.cpp + theory/quantifiers/sygus/sygus_stats.h theory/quantifiers/sygus/sygus_unif.cpp theory/quantifiers/sygus/sygus_unif.h theory/quantifiers/sygus/sygus_unif_io.cpp diff --git a/src/theory/quantifiers/sygus/sygus_stats.cpp b/src/theory/quantifiers/sygus/sygus_stats.cpp new file mode 100644 index 000000000..bee2e1d56 --- /dev/null +++ b/src/theory/quantifiers/sygus/sygus_stats.cpp @@ -0,0 +1,53 @@ +/********************* */ +/*! \file sygus_stats.cpp + ** \verbatim + ** Top contributors (to current version): + ** Andrew Reynolds, Tim King, Morgan Deters + ** This file is part of the CVC4 project. + ** Copyright (c) 2009-2019 by the authors listed in the file AUTHORS + ** in the top-level source directory) and their institutional affiliations. + ** All rights reserved. See the file COPYING in the top-level source + ** directory for licensing information.\endverbatim + ** + ** \brief A shared statistics class for sygus. + ** + **/ + +#include "theory/quantifiers/sygus/sygus_stats.h" + +#include "smt/smt_statistics_registry.h" + +namespace CVC4 { +namespace theory { +namespace quantifiers { + +SygusStatistics::SygusStatistics() + : d_cegqi_lemmas_ce("SynthEngine::cegqi_lemmas_ce", 0), + d_cegqi_lemmas_refine("SynthEngine::cegqi_lemmas_refine", 0), + d_cegqi_si_lemmas("SynthEngine::cegqi_lemmas_si", 0), + d_solutions("SynthConjecture::solutions", 0), + d_filtered_solutions("SynthConjecture::filtered_solutions", 0), + d_candidate_rewrites_print("SynthConjecture::candidate_rewrites_print", 0) + +{ + smtStatisticsRegistry()->registerStat(&d_cegqi_lemmas_ce); + smtStatisticsRegistry()->registerStat(&d_cegqi_lemmas_refine); + smtStatisticsRegistry()->registerStat(&d_cegqi_si_lemmas); + smtStatisticsRegistry()->registerStat(&d_solutions); + smtStatisticsRegistry()->registerStat(&d_filtered_solutions); + smtStatisticsRegistry()->registerStat(&d_candidate_rewrites_print); +} + +SygusStatistics::~SygusStatistics() +{ + smtStatisticsRegistry()->unregisterStat(&d_cegqi_lemmas_ce); + smtStatisticsRegistry()->unregisterStat(&d_cegqi_lemmas_refine); + smtStatisticsRegistry()->unregisterStat(&d_cegqi_si_lemmas); + smtStatisticsRegistry()->unregisterStat(&d_solutions); + smtStatisticsRegistry()->unregisterStat(&d_filtered_solutions); + smtStatisticsRegistry()->unregisterStat(&d_candidate_rewrites_print); +} + +} // namespace quantifiers +} // namespace theory +} /* namespace CVC4 */ diff --git a/src/theory/quantifiers/sygus/sygus_stats.h b/src/theory/quantifiers/sygus/sygus_stats.h new file mode 100644 index 000000000..c4c7ba060 --- /dev/null +++ b/src/theory/quantifiers/sygus/sygus_stats.h @@ -0,0 +1,52 @@ +/********************* */ +/*! \file sygus_stats.h + ** \verbatim + ** Top contributors (to current version): + ** Andrew Reynolds + ** This file is part of the CVC4 project. + ** Copyright (c) 2009-2019 by the authors listed in the file AUTHORS + ** in the top-level source directory) and their institutional affiliations. + ** All rights reserved. See the file COPYING in the top-level source + ** directory for licensing information.\endverbatim + ** + ** \brief A shared statistics class for sygus. + **/ + +#include "cvc4_private.h" + +#ifndef CVC4__THEORY__QUANTIFIERS__SYGUS_STATS_H +#define CVC4__THEORY__QUANTIFIERS__SYGUS_STATS_H + +#include "util/statistics_registry.h" + +namespace CVC4 { +namespace theory { +namespace quantifiers { + +/** + * All statistics managed for the synth engine. + */ +class SygusStatistics +{ + public: + SygusStatistics(); + ~SygusStatistics(); + /** Number of counterexample lemmas */ + IntStat d_cegqi_lemmas_ce; + /** Number of refinement lemmas */ + IntStat d_cegqi_lemmas_refine; + /** Number of single invocation lemmas */ + IntStat d_cegqi_si_lemmas; + /** Number of solutions printed (could be >1 for --sygus-stream) */ + IntStat d_solutions; + /** Number of solutions filtered */ + IntStat d_filtered_solutions; + /** Number of candidate rewrites printed (for --sygus-rr) */ + IntStat d_candidate_rewrites_print; +}; + +} // namespace quantifiers +} // namespace theory +} /* namespace CVC4 */ + +#endif 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) 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. */ diff --git a/src/theory/quantifiers/sygus/synth_engine.cpp b/src/theory/quantifiers/sygus/synth_engine.cpp index 4a708e66c..2b621f6dd 100644 --- a/src/theory/quantifiers/sygus/synth_engine.cpp +++ b/src/theory/quantifiers/sygus/synth_engine.cpp @@ -18,7 +18,6 @@ #include "options/quantifiers_options.h" #include "smt/smt_engine.h" #include "smt/smt_engine_scope.h" -#include "smt/smt_statistics_registry.h" #include "theory/quantifiers/quantifiers_attributes.h" #include "theory/quantifiers/sygus/term_database_sygus.h" #include "theory/quantifiers/term_util.h" @@ -36,7 +35,7 @@ SynthEngine::SynthEngine(QuantifiersEngine* qe, context::Context* c) : QuantifiersModule(qe), d_tds(qe->getTermDatabaseSygus()) { d_conjs.push_back(std::unique_ptr( - new SynthConjecture(d_quantEngine, this))); + new SynthConjecture(d_quantEngine, this, d_statistics))); d_conj = d_conjs.back().get(); } @@ -267,7 +266,7 @@ void SynthEngine::assignConjecture(Node q) if (d_conjs.back()->isAssigned()) { d_conjs.push_back(std::unique_ptr( - new SynthConjecture(d_quantEngine, this))); + new SynthConjecture(d_quantEngine, this, d_statistics))); } d_conjs.back()->assign(q); } @@ -424,33 +423,6 @@ void SynthEngine::preregisterAssertion(Node n) } } -SynthEngine::Statistics::Statistics() - : d_cegqi_lemmas_ce("SynthEngine::cegqi_lemmas_ce", 0), - d_cegqi_lemmas_refine("SynthEngine::cegqi_lemmas_refine", 0), - d_cegqi_si_lemmas("SynthEngine::cegqi_lemmas_si", 0), - d_solutions("SynthConjecture::solutions", 0), - d_filtered_solutions("SynthConjecture::filtered_solutions", 0), - d_candidate_rewrites_print("SynthConjecture::candidate_rewrites_print", 0) - -{ - smtStatisticsRegistry()->registerStat(&d_cegqi_lemmas_ce); - smtStatisticsRegistry()->registerStat(&d_cegqi_lemmas_refine); - smtStatisticsRegistry()->registerStat(&d_cegqi_si_lemmas); - smtStatisticsRegistry()->registerStat(&d_solutions); - smtStatisticsRegistry()->registerStat(&d_filtered_solutions); - smtStatisticsRegistry()->registerStat(&d_candidate_rewrites_print); -} - -SynthEngine::Statistics::~Statistics() -{ - smtStatisticsRegistry()->unregisterStat(&d_cegqi_lemmas_ce); - smtStatisticsRegistry()->unregisterStat(&d_cegqi_lemmas_refine); - smtStatisticsRegistry()->unregisterStat(&d_cegqi_si_lemmas); - smtStatisticsRegistry()->unregisterStat(&d_solutions); - smtStatisticsRegistry()->unregisterStat(&d_filtered_solutions); - smtStatisticsRegistry()->unregisterStat(&d_candidate_rewrites_print); -} - } // namespace quantifiers } // namespace theory } /* namespace CVC4 */ diff --git a/src/theory/quantifiers/sygus/synth_engine.h b/src/theory/quantifiers/sygus/synth_engine.h index 1eca56959..4b47235da 100644 --- a/src/theory/quantifiers/sygus/synth_engine.h +++ b/src/theory/quantifiers/sygus/synth_engine.h @@ -20,6 +20,7 @@ #include "context/cdhashmap.h" #include "theory/quantifiers/quant_util.h" +#include "theory/quantifiers/sygus/sygus_stats.h" #include "theory/quantifiers/sygus/synth_conjecture.h" namespace CVC4 { @@ -72,21 +73,6 @@ class SynthEngine : public QuantifiersModule */ void preregisterAssertion(Node n); - public: - class Statistics - { - public: - IntStat d_cegqi_lemmas_ce; - IntStat d_cegqi_lemmas_refine; - IntStat d_cegqi_si_lemmas; - IntStat d_solutions; - IntStat d_filtered_solutions; - IntStat d_candidate_rewrites_print; - Statistics(); - ~Statistics(); - }; /* class SynthEngine::Statistics */ - Statistics d_statistics; - private: /** term database sygus of d_qe */ TermDbSygus* d_tds; @@ -100,6 +86,8 @@ class SynthEngine : public QuantifiersModule * preregisterAssertion. */ SynthConjecture* d_conj; + /** The statistics */ + SygusStatistics d_statistics; /** assign quantified formula q as a conjecture * * This method either assigns q to a synthesis conjecture object in d_conjs, -- 2.30.2