summaryrefslogtreecommitdiff
diff options
context:
space:
mode:
Diffstat
-rw-r--r--src/CMakeLists.txt2
-rw-r--r--src/theory/quantifiers/sygus/sygus_stats.cpp53
-rw-r--r--src/theory/quantifiers/sygus/sygus_stats.h52
-rw-r--r--src/theory/quantifiers/sygus/synth_conjecture.cpp11
-rw-r--r--src/theory/quantifiers/sygus/synth_conjecture.h5
-rw-r--r--src/theory/quantifiers/sygus/synth_engine.cpp32
-rw-r--r--src/theory/quantifiers/sygus/synth_engine.h18
7 files changed, 123 insertions, 50 deletions
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<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 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,
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback