Refactor sygus stats (#3684)

diff --git a/src/CMakeLists.txt b/src/CMakeLists.txt
index 271ceb045fc26c92bf0388bddb8c07fe152cb9d0..f5f6a83c99c7ed4d234a45927b228ceacb83a81b 100644 (file)
--- 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 (file)
index 0000000..bee2e1d
--- /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 (file)
index 0000000..c4c7ba0
--- /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 03449589b92eb73bb71e1c4c770cc5b68d29d4bc..73fc53d86fc495a8e761b818a327419efa203c34 100644 (file)
--- 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 db9872ec34d374be8d123aa05dfc8a29db5c1067..a001572c2160a2cb1cf3d310f14861d74a935035 100644 (file)
--- 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 4a708e66cc8f2b49d6a3143098e60d179cdb69b4..2b621f6dd93e6733a516ae2b3f5a81d7deb29b77 100644 (file)
--- 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<SynthConjecture>(
-      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<SynthConjecture>(
-        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 1eca56959a1d0383b77eadd70216fb5046f3219a..4b47235dacfbf8c6c88b1cefe7270bce4afb9c1d 100644 (file)
--- 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,