This PR refactors how we collect statistics.
It splits the current statistic values into the values and a proxy object. The actual values now live inside the registry (making the ownership model way easier) while the proxy object are handed to whoever wants to collect a new statistic.
It also extends the C++ API to obtain and inspect the statistics.
To change the ownership, this PR needs to touch every single statistic in the whole codebase and change how it is registered.
#include "util/random.h"
#include "util/result.h"
#include "util/statistics_registry.h"
-#include "util/stats_histogram.h"
+#include "util/statistics_stats.h"
+#include "util/statistics_value.h"
#include "util/utility.h"
namespace cvc5 {
namespace api {
/* -------------------------------------------------------------------------- */
-/* Statistics */
+/* APIStatistics */
/* -------------------------------------------------------------------------- */
-struct Statistics
+struct APIStatistics
{
- Statistics()
- : d_consts("api::CONSTANT"), d_vars("api::VARIABLE"), d_terms("api::TERM")
- {
- }
- IntegralHistogramStat<TypeConstant> d_consts;
- IntegralHistogramStat<TypeConstant> d_vars;
- IntegralHistogramStat<Kind> d_terms;
+ HistogramStat<TypeConstant> d_consts;
+ HistogramStat<TypeConstant> d_vars;
+ HistogramStat<Kind> d_terms;
};
/* -------------------------------------------------------------------------- */
return size_t(rm);
}
+/* -------------------------------------------------------------------------- */
+/* Statistics */
+/* -------------------------------------------------------------------------- */
+
+struct Stat::StatData
+{
+ cvc5::StatExportData data;
+ template <typename T>
+ StatData(T&& t) : data(std::forward<T>(t))
+ {
+ }
+ StatData() : data() {}
+};
+
+Stat::~Stat() {}
+Stat::Stat(const Stat& s)
+ : d_expert(s.d_expert), d_data(std::make_unique<StatData>(s.d_data->data))
+{
+}
+Stat& Stat::operator=(const Stat& s)
+{
+ d_expert = s.d_expert;
+ d_data = std::make_unique<StatData>(s.d_data->data);
+ return *this;
+}
+
+bool Stat::isExpert() const { return d_expert; }
+bool Stat::isDefault() const { return d_default; }
+
+bool Stat::isInt() const
+{
+ return std::holds_alternative<int64_t>(d_data->data);
+}
+int64_t Stat::getInt() const
+{
+ CVC5_API_TRY_CATCH_BEGIN;
+ CVC5_API_CHECK(isInt()) << "Expected Stat of type int64_t.";
+ return std::get<int64_t>(d_data->data);
+ CVC5_API_TRY_CATCH_END;
+}
+bool Stat::isDouble() const
+{
+ return std::holds_alternative<double>(d_data->data);
+}
+double Stat::getDouble() const
+{
+ CVC5_API_TRY_CATCH_BEGIN;
+ CVC5_API_CHECK(isDouble()) << "Expected Stat of type double.";
+ return std::get<double>(d_data->data);
+ CVC5_API_TRY_CATCH_END;
+}
+bool Stat::isString() const
+{
+ return std::holds_alternative<std::string>(d_data->data);
+}
+const std::string& Stat::getString() const
+{
+ CVC5_API_TRY_CATCH_BEGIN;
+ CVC5_API_CHECK(isString()) << "Expected Stat of type std::string.";
+ return std::get<std::string>(d_data->data);
+ CVC5_API_TRY_CATCH_END;
+}
+bool Stat::isHistogram() const
+{
+ return std::holds_alternative<HistogramData>(d_data->data);
+}
+const Stat::HistogramData& Stat::getHistogram() const
+{
+ CVC5_API_TRY_CATCH_BEGIN;
+ CVC5_API_CHECK(isHistogram()) << "Expected Stat of type histogram.";
+ return std::get<HistogramData>(d_data->data);
+ CVC5_API_TRY_CATCH_END;
+}
+
+Stat::Stat(bool expert, bool def, StatData&& sd)
+ : d_expert(expert),
+ d_default(def),
+ d_data(std::make_unique<StatData>(std::move(sd)))
+{
+}
+
+std::ostream& operator<<(std::ostream& os, const Stat& sv)
+{
+ return cvc5::detail::print(os, sv.d_data->data);
+}
+
+Statistics::BaseType::const_reference Statistics::iterator::operator*() const
+{
+ return d_it.operator*();
+}
+Statistics::BaseType::const_pointer Statistics::iterator::operator->() const
+{
+ return d_it.operator->();
+}
+Statistics::iterator& Statistics::iterator::operator++()
+{
+ do
+ {
+ ++d_it;
+ } while (!isVisible());
+ return *this;
+}
+Statistics::iterator Statistics::iterator::operator++(int)
+{
+ iterator tmp = *this;
+ do
+ {
+ ++d_it;
+ } while (!isVisible());
+ return tmp;
+}
+Statistics::iterator& Statistics::iterator::operator--()
+{
+ do
+ {
+ --d_it;
+ } while (!isVisible());
+ return *this;
+}
+Statistics::iterator Statistics::iterator::operator--(int)
+{
+ iterator tmp = *this;
+ do
+ {
+ --d_it;
+ } while (!isVisible());
+ return tmp;
+}
+bool Statistics::iterator::operator==(const Statistics::iterator& rhs) const
+{
+ return d_it == rhs.d_it;
+}
+bool Statistics::iterator::operator!=(const Statistics::iterator& rhs) const
+{
+ return d_it != rhs.d_it;
+}
+Statistics::iterator::iterator(Statistics::BaseType::const_iterator it,
+ const Statistics::BaseType& base,
+ bool expert,
+ bool def)
+ : d_it(it), d_base(&base), d_showExpert(expert), d_showDefault(def)
+{
+ while (!isVisible())
+ {
+ ++d_it;
+ }
+}
+bool Statistics::iterator::isVisible() const
+{
+ if (d_it == d_base->end()) return true;
+ if (!d_showExpert && d_it->second.isExpert()) return false;
+ if (!d_showDefault && d_it->second.isDefault()) return false;
+ return true;
+}
+
+const Stat& Statistics::get(const std::string& name)
+{
+ CVC5_API_TRY_CATCH_BEGIN;
+ auto it = d_stats.find(name);
+ CVC5_API_CHECK(it != d_stats.end())
+ << "No stat with name \"" << name << "\" exists.";
+ return it->second;
+ CVC5_API_TRY_CATCH_END;
+}
+
+Statistics::iterator Statistics::begin(bool expert, bool def) const
+{
+ return iterator(d_stats.begin(), d_stats, expert, def);
+}
+Statistics::iterator Statistics::end() const
+{
+ return iterator(d_stats.end(), d_stats, false, false);
+}
+
+Statistics::Statistics(const StatisticsRegistry& reg)
+{
+ for (const auto& svp : reg)
+ {
+ d_stats.emplace(svp.first,
+ Stat(svp.second->d_expert,
+ svp.second->isDefault(),
+ svp.second->getViewer()));
+ }
+}
+
+std::ostream& operator<<(std::ostream& out, const Statistics& stats)
+{
+ for (const auto& stat : stats)
+ {
+ out << stat.first << " = " << stat.second << std::endl;
+ }
+ return out;
+}
+
/* -------------------------------------------------------------------------- */
/* Solver */
/* -------------------------------------------------------------------------- */
d_smtEngine.reset(new SmtEngine(d_nodeMgr.get(), d_originalOptions.get()));
d_smtEngine->setSolver(this);
d_rng.reset(new Random(d_smtEngine->getOptions()[options::seed]));
-#if CVC5_STATISTICS_ON
- d_stats.reset(new Statistics());
- d_smtEngine->getStatisticsRegistry().registerStat(&d_stats->d_consts);
- d_smtEngine->getStatisticsRegistry().registerStat(&d_stats->d_vars);
- d_smtEngine->getStatisticsRegistry().registerStat(&d_stats->d_terms);
-#endif
+ resetStatistics();
}
Solver::~Solver() {}
void Solver::increment_term_stats(Kind kind) const
{
-#ifdef CVC5_STATISTICS_ON
- d_stats->d_terms << kind;
-#endif
+ if constexpr (Configuration::isStatisticsBuild())
+ {
+ d_stats->d_terms << kind;
+ }
}
void Solver::increment_vars_consts_stats(const Sort& sort, bool is_var) const
{
-#ifdef CVC5_STATISTICS_ON
- const TypeNode tn = sort.getTypeNode();
- TypeConstant tc = tn.getKind() == cvc5::kind::TYPE_CONSTANT
- ? tn.getConst<TypeConstant>()
- : LAST_TYPE;
- if (is_var)
- {
- d_stats->d_vars << tc;
- }
- else
+ if constexpr (Configuration::isStatisticsBuild())
{
- d_stats->d_consts << tc;
+ const TypeNode tn = sort.getTypeNode();
+ TypeConstant tc = tn.getKind() == cvc5::kind::TYPE_CONSTANT
+ ? tn.getConst<TypeConstant>()
+ : LAST_TYPE;
+ if (is_var)
+ {
+ d_stats->d_vars << tc;
+ }
+ else
+ {
+ d_stats->d_consts << tc;
+ }
}
-#endif
}
/* Split out to avoid nested API calls (problematic with API tracing). */
return true;
}
+void Solver::resetStatistics()
+{
+ if constexpr (Configuration::isStatisticsBuild())
+ {
+ d_stats.reset(new APIStatistics{
+ d_smtEngine->getStatisticsRegistry().registerHistogram<TypeConstant>(
+ "api::CONSTANT"),
+ d_smtEngine->getStatisticsRegistry().registerHistogram<TypeConstant>(
+ "api::VARIABLE"),
+ d_smtEngine->getStatisticsRegistry().registerHistogram<Kind>("api::TERM"),
+ });
+ }
+}
+
/* Helpers for mkTerm checks. */
/* .......................................................................... */
*/
Options& Solver::getOptions(void) { return d_smtEngine->getOptions(); }
+Statistics Solver::getStatistics() const
+{
+ return Statistics(d_smtEngine->getStatisticsRegistry());
+}
+
} // namespace api
} // namespace cvc5
class Options;
class Random;
class Result;
+class StatisticsRegistry;
namespace api {
class Solver;
-struct Statistics;
+class Statistics;
+struct APIStatistics;
/* -------------------------------------------------------------------------- */
/* Exception */
inline size_t operator()(const RoundingMode& rm) const;
};
+/* -------------------------------------------------------------------------- */
+/* Statistics */
+/* -------------------------------------------------------------------------- */
+
+/**
+ * Represents a snapshot of a single statistic value.
+ * A value can be of type int64_t, double, std::string or a histogram
+ * (`std::map<std::string, uint64_t>`).
+ * The value type can be queried (using `isInt`, `isString`, etc.) and
+ * the stored value can be accessed (using `getInt`, `getString`, etc.).
+ */
+class CVC4_EXPORT Stat
+{
+ struct StatData;
+
+ public:
+ friend class Statistics;
+ friend std::ostream& operator<<(std::ostream& os, const Stat& sv);
+ using HistogramData = std::map<std::string, uint64_t>;
+ /** Create from the given value. */
+ Stat() = delete;
+ Stat(const Stat& s);
+ ~Stat();
+ Stat& operator=(const Stat& s);
+
+ /** Is this value intended for experts only? */
+ bool isExpert() const;
+ /** Does this value hold the default value? */
+ bool isDefault() const;
+
+ /** Is this value an integer? */
+ bool isInt() const;
+ /** Return the integer value */
+ int64_t getInt() const;
+ /** Is this value a double? */
+ bool isDouble() const;
+ /** Return the double value */
+ double getDouble() const;
+ /** Is this value an string? */
+ bool isString() const;
+ /** Return the string value */
+ const std::string& getString() const;
+ /** Is this value an histogram? */
+ bool isHistogram() const;
+ /** Return the histogram value */
+ const HistogramData& getHistogram() const;
+
+ private:
+ Stat(bool expert, bool def, StatData&& sd);
+ /** Whether this statistic is only meant for experts */
+ bool d_expert;
+ /** Whether this statistic has the default value */
+ bool d_default;
+ std::unique_ptr<StatData> d_data;
+};
+
+std::ostream& operator<<(std::ostream& os, const Stat& sv) CVC4_EXPORT;
+
+/**
+ * Represents a snapshot of the solver statistics.
+ * Once obtained, an instance of this class is independent of the `Solver`
+ * object: it will not change when the solvers internal statistics do, it
+ * will not be invalidated if the solver is destroyed.
+ * Statistics are generally categorized as public and expert statistics.
+ * Furthermore, statistics may hold the default values and thus be not of
+ * interest.
+ * Iterating on this class (via `begin()` and `end()`) shows only public
+ * statistics that have been set. By passing appropriate flags to `begin()`,
+ * statistics that are expert, unchanged, or both, can be included as well.
+ * A single statistic value is represented as `Stat`.
+ */
+class CVC4_EXPORT Statistics
+{
+ public:
+ friend Solver;
+ using BaseType = std::map<std::string, Stat>;
+
+ /** Custom iterator to hide expert statistics from regular iteration */
+ class iterator
+ {
+ public:
+ friend Statistics;
+ BaseType::const_reference operator*() const;
+ BaseType::const_pointer operator->() const;
+ iterator& operator++();
+ iterator operator++(int);
+ iterator& operator--();
+ iterator operator--(int);
+ bool operator==(const iterator& rhs) const;
+ bool operator!=(const iterator& rhs) const;
+
+ private:
+ iterator(BaseType::const_iterator it,
+ const BaseType& base,
+ bool expert,
+ bool def);
+ bool isVisible() const;
+ BaseType::const_iterator d_it;
+ const BaseType* d_base;
+ bool d_showExpert = false;
+ bool d_showDefault = false;
+ };
+
+ /** Retrieve the statistic with the given name. */
+ const Stat& get(const std::string& name);
+ /**
+ * Begin iteration over the statistics values.
+ * By default, only entries that are public (non-expert) and have been set
+ * are visible while the others are skipped.
+ * With `expert` set to true, expert statistics are shown as well.
+ * With `def` set to true, defaulted statistics are shown as well.
+ */
+ iterator begin(bool expert = false, bool def = false) const;
+ /** end iteration */
+ iterator end() const;
+
+ private:
+ Statistics() = default;
+ Statistics(const StatisticsRegistry& reg);
+ /** Internal data */
+ BaseType d_stats;
+};
+std::ostream& operator<<(std::ostream& out, const Statistics& stats) CVC4_EXPORT;
+
/* -------------------------------------------------------------------------- */
/* Solver */
/* -------------------------------------------------------------------------- */
// the driver level. !!!
Options& getOptions(void);
+ /**
+ * Returns a snapshot of the current state of the statistic values of this
+ * solver. The returned object is completely decoupled from the solver and
+ * will not change when the solver is used again.
+ */
+ Statistics getStatistics() const;
+
private:
/** @return the node manager of this solver */
NodeManager* getNodeManager(void) const;
+ /** Reset the API statistics */
+ void resetStatistics();
/** Helper to check for API misuse in mkOp functions. */
void checkMkTerm(Kind kind, uint32_t nchildren) const;
/** The node manager of this solver. */
std::unique_ptr<NodeManager> d_nodeMgr;
/** The statistics collected on the Api level. */
- std::unique_ptr<Statistics> d_stats;
+ std::unique_ptr<APIStatistics> d_stats;
/** The SMT engine of this solver. */
std::unique_ptr<SmtEngine> d_smtEngine;
/** The random number generator of this solver. */
d_exploredThreshold(c),
d_prvsIndex(c, 0),
d_threshPrvsIndex(c, 0),
- d_helpfulness("decision::jh::helpfulness", 0),
- d_giveup("decision::jh::giveup", 0),
- d_timestat("decision::jh::time"),
+ d_helpfulness(
+ smtStatisticsRegistry().registerInt("decision::jh::helpfulness")),
+ d_giveup(smtStatisticsRegistry().registerInt("decision::jh::giveup")),
+ d_timestat(smtStatisticsRegistry().registerTimer("decision::jh::time")),
d_assertions(uc),
d_skolemAssertions(uc),
d_skolemCache(uc),
d_weightCache(uc),
d_startIndexCache(c)
{
- smtStatisticsRegistry()->registerStat(&d_helpfulness);
- smtStatisticsRegistry()->registerStat(&d_giveup);
- smtStatisticsRegistry()->registerStat(&d_timestat);
Trace("decision") << "Justification heuristic enabled" << std::endl;
}
-JustificationHeuristic::~JustificationHeuristic()
-{
- smtStatisticsRegistry()->unregisterStat(&d_helpfulness);
- smtStatisticsRegistry()->unregisterStat(&d_giveup);
- smtStatisticsRegistry()->unregisterStat(&d_timestat);
-}
+JustificationHeuristic::~JustificationHeuristic() {}
cvc5::prop::SatLiteral JustificationHeuristic::getNext(bool& stopSearch)
{
#include "expr/node.h"
#include "options/decision_weight.h"
#include "prop/sat_solver_types.h"
-#include "util/statistics_registry.h"
-#include "util/stats_timer.h"
+#include "util/statistics_stats.h"
namespace cvc5 {
namespace decision {
}
ProofCheckerStatistics::ProofCheckerStatistics()
- : d_ruleChecks("ProofCheckerStatistics::ruleChecks"),
- d_totalRuleChecks("ProofCheckerStatistics::totalRuleChecks", 0)
+ : d_ruleChecks(smtStatisticsRegistry().registerHistogram<PfRule>(
+ "ProofCheckerStatistics::ruleChecks")),
+ d_totalRuleChecks(smtStatisticsRegistry().registerInt(
+ "ProofCheckerStatistics::totalRuleChecks"))
{
- smtStatisticsRegistry()->registerStat(&d_ruleChecks);
- smtStatisticsRegistry()->registerStat(&d_totalRuleChecks);
-}
-
-ProofCheckerStatistics::~ProofCheckerStatistics()
-{
- smtStatisticsRegistry()->unregisterStat(&d_ruleChecks);
- smtStatisticsRegistry()->unregisterStat(&d_totalRuleChecks);
}
Node ProofChecker::check(ProofNode* pn, Node expected)
#include "expr/node.h"
#include "expr/proof_rule.h"
-#include "util/statistics_registry.h"
-#include "util/stats_histogram.h"
+#include "util/statistics_stats.h"
namespace cvc5 {
{
public:
ProofCheckerStatistics();
- ~ProofCheckerStatistics();
/** Counts the number of checks for each kind of proof rule */
-
IntegralHistogramStat<PfRule> d_ruleChecks;
+ HistogramStat<PfRule> d_ruleChecks;
/** Total number of rule checks */
IntStat d_totalRuleChecks;
};
#endif /* ! __WIN32__ */
}
-void printStatsIncremental(std::ostream& out, const std::string& prvsStatsString, const std::string& curStatsString);
-
CommandExecutor::CommandExecutor(Options& options)
: d_solver(new api::Solver(&options)),
d_symman(new SymbolManager(d_solver.get())),
}
if((cs != nullptr || q != nullptr) && d_options.getStatsEveryQuery()) {
- std::ostringstream ossCurStats;
- printStatistics(ossCurStats);
- std::ostream& err = *d_options.getErr();
- printStatsIncremental(err, d_lastStatistics, ossCurStats.str());
- d_lastStatistics = ossCurStats.str();
+ getSmtEngine()->printStatisticsDiff(*d_options.getErr());
}
bool isResultUnsat = res.isUnsat() || res.isEntailed();
return !cmd->fail();
}
-void printStatsIncremental(std::ostream& out,
- const std::string& prvsStatsString,
- const std::string& curStatsString)
-{
- if(prvsStatsString == "") {
- out << curStatsString;
- return;
- }
-
- // read each line
- // if a number, subtract and add that to parentheses
- std::istringstream issPrvs(prvsStatsString);
- std::istringstream issCur(curStatsString);
-
- std::string prvsStatName, prvsStatValue, curStatName, curStatValue;
-
- std::getline(issPrvs, prvsStatName, ',');
- std::getline(issCur, curStatName, ',');
-
- /**
- * Stat are assumed to one-per line: "<statName>, <statValue>"
- * e.g. "sat::decisions, 100"
- * Output is of the form: "<statName>, <statValue> (<statDiffFromPrvs>)"
- * e.g. "sat::decisions, 100 (20)"
- * If the value is not numeric, no change is made.
- */
- while( !issCur.eof() ) {
-
- std::getline(issCur, curStatValue, '\n');
-
- if(curStatName == prvsStatName) {
- std::getline(issPrvs, prvsStatValue, '\n');
-
- double prvsFloat, curFloat;
- bool isFloat =
- (std::istringstream(prvsStatValue) >> prvsFloat) &&
- (std::istringstream(curStatValue) >> curFloat);
-
- if(isFloat) {
- const std::streamsize old_precision = out.precision();
- out << curStatName << ", " << curStatValue << " "
- << "(" << std::setprecision(8) << (curFloat-prvsFloat) << ")"
- << std::endl;
- out.precision(old_precision);
- } else {
- out << curStatName << ", " << curStatValue << std::endl;
- }
-
- std::getline(issPrvs, prvsStatName, ',');
- } else {
- out << curStatName << ", " << curStatValue << std::endl;
- }
-
- std::getline(issCur, curStatName, ',');
- }
-}
-
void CommandExecutor::flushOutputStreams() {
printStatistics(*(d_options.getErr()));
class CommandExecutor
{
- private:
- std::string d_lastStatistics;
-
protected:
/**
* The solver object, which is allocated by this class and is used for
help = "print expert (non-public) statistics as well"
[[option]]
- name = "statisticsUnset"
- smt_name = "stats-unset"
- long = "stats-unset"
+ name = "statisticsAll"
+ smt_name = "stats-all"
+ long = "stats-all"
category = "expert"
type = "bool"
predicates = ["statsEnabledBuild"]
read_only = true
- help = "print unset statistics as well"
+ help = "print unchanged (defaulted) statistics as well"
[[option]]
name = "statisticsEveryQuery"
read_only = true
help = "in incremental mode, print stats after every satisfiability or validity query"
-[[option]]
- name = "statsHideZeros"
- category = "regular"
- long = "stats-hide-zeros"
- type = "bool"
- default = "false"
- read_only = true
- help = "hide statistics which are zero"
-
[[option]]
name = "parseOnly"
category = "regular"
bool getSemanticChecks() const;
bool getStatistics() const;
bool getStatsEveryQuery() const;
- bool getStatsHideZeros() const;
bool getStrictParsing() const;
int getTearDownIncremental() const;
unsigned long getCumulativeTimeLimit() const;
return (*this)[options::statisticsEveryQuery];
}
-bool Options::getStatsHideZeros() const{
- return (*this)[options::statsHideZeros];
-}
-
bool Options::getStrictParsing() const{
return (*this)[options::strictParsing];
}
Debug("bool-to-bv") << "BoolToBV::visit forcing " << n
<< " =>\n"
<< fromCache(n) << std::endl;
- ++(d_statistics.d_numIntroducedItes);
+ if (d_boolToBVMode == options::BoolToBVMode::ALL)
+ {
+ // this statistic only makes sense for ALL mode
+ ++(d_statistics.d_numIntroducedItes);
+ }
return;
}
else if (safe_to_rebuild && needToRebuild(n))
Debug("bool-to-bv") << "BoolToBV::visit forcing " << n
<< " =>\n"
<< fromCache(n) << std::endl;
- ++(d_statistics.d_numIntroducedItes);
+ if (d_boolToBVMode == options::BoolToBVMode::ALL)
+ {
+ // this statistic only makes sense for ALL mode
+ ++(d_statistics.d_numIntroducedItes);
+ }
}
else
{
if ((d_boolToBVMode == options::BoolToBVMode::ALL) && (new_kind != k))
{
+ // this statistic only makes sense for ALL mode
++(d_statistics.d_numTermsLowered);
}
}
BoolToBV::Statistics::Statistics()
- : d_numIteToBvite("preprocessing::passes::BoolToBV::NumIteToBvite", 0),
- d_numTermsLowered("preprocessing::passes:BoolToBV::NumTermsLowered", 0),
- d_numIntroducedItes(
- "preprocessing::passes::BoolToBV::NumTermsForcedLowered", 0)
-{
- smtStatisticsRegistry()->registerStat(&d_numIteToBvite);
- if (options::boolToBitvector() == options::BoolToBVMode::ALL)
- {
- // these statistics wouldn't be correct in the ITE mode,
- // because it might discard rebuilt nodes if it fails to
- // convert a bool to width-one bit-vector (never forces)
- smtStatisticsRegistry()->registerStat(&d_numTermsLowered);
- smtStatisticsRegistry()->registerStat(&d_numIntroducedItes);
- }
-}
-
-BoolToBV::Statistics::~Statistics()
+ : d_numIteToBvite(smtStatisticsRegistry().registerInt(
+ "preprocessing::passes::BoolToBV::NumIteToBvite")),
+ // the following two statistics are not correct in the ITE mode, because
+ // we might discard rebuilt nodes if we fails to convert a bool to
+ // width-one bit-vector (never forces)
+ d_numTermsLowered(smtStatisticsRegistry().registerInt(
+ "preprocessing::passes:BoolToBV::NumTermsLowered")),
+ d_numIntroducedItes(smtStatisticsRegistry().registerInt(
+ "preprocessing::passes::BoolToBV::NumTermsForcedLowered"))
{
- smtStatisticsRegistry()->unregisterStat(&d_numIteToBvite);
- if (options::boolToBitvector() == options::BoolToBVMode::ALL)
- {
- smtStatisticsRegistry()->unregisterStat(&d_numTermsLowered);
- smtStatisticsRegistry()->unregisterStat(&d_numIntroducedItes);
- }
}
-
} // namespace passes
} // namespace preprocessing
} // namespace cvc5
#include "expr/node.h"
#include "options/bv_options.h"
#include "preprocessing/preprocessing_pass.h"
-#include "util/statistics_registry.h"
+#include "util/statistics_stats.h"
namespace cvc5 {
namespace preprocessing {
IntStat d_numTermsLowered;
IntStat d_numIntroducedItes;
Statistics();
- ~Statistics();
};
/** Takes an assertion and attempts to create more bit-vector structure
Kind kind = node.getKind();
if (kind == kind::CONST_BITVECTOR || kind == kind::ITE
- || kind == kind::BITVECTOR_AND
- || kind == kind::BITVECTOR_OR
- || kind == kind::BITVECTOR_NOT
- || kind == kind::BITVECTOR_XOR
+ || kind == kind::BITVECTOR_AND || kind == kind::BITVECTOR_OR
+ || kind == kind::BITVECTOR_NOT || kind == kind::BITVECTOR_XOR
|| kind == kind::BITVECTOR_COMP)
{
return true;
}
BVToBool::Statistics::Statistics()
- : d_numTermsLifted("preprocessing::passes::BVToBool::NumTermsLifted", 0),
- d_numAtomsLifted("preprocessing::passes::BVToBool::NumAtomsLifted", 0),
- d_numTermsForcedLifted(
- "preprocessing::passes::BVToBool::NumTermsForcedLifted", 0)
+ : d_numTermsLifted(smtStatisticsRegistry().registerInt(
+ "preprocessing::passes::BVToBool::NumTermsLifted")),
+ d_numAtomsLifted(smtStatisticsRegistry().registerInt(
+ "preprocessing::passes::BVToBool::NumAtomsLifted")),
+ d_numTermsForcedLifted(smtStatisticsRegistry().registerInt(
+ "preprocessing::passes::BVToBool::NumTermsForcedLifted"))
{
- smtStatisticsRegistry()->registerStat(&d_numTermsLifted);
- smtStatisticsRegistry()->registerStat(&d_numAtomsLifted);
- smtStatisticsRegistry()->registerStat(&d_numTermsForcedLifted);
}
-BVToBool::Statistics::~Statistics()
-{
- smtStatisticsRegistry()->unregisterStat(&d_numTermsLifted);
- smtStatisticsRegistry()->unregisterStat(&d_numAtomsLifted);
- smtStatisticsRegistry()->unregisterStat(&d_numTermsForcedLifted);
-}
-
-
-} // passes
-} // Preprocessing
+} // namespace passes
+} // namespace preprocessing
} // namespace cvc5
#include "expr/node.h"
#include "preprocessing/preprocessing_pass.h"
-#include "util/statistics_registry.h"
+#include "util/statistics_stats.h"
namespace cvc5 {
namespace preprocessing {
IntStat d_numAtomsLifted;
IntStat d_numTermsForcedLifted;
Statistics();
- ~Statistics();
};
void addToBoolCache(TNode term, Node new_term);
Node getBoolCache(TNode term) const;
/* -------------------------------------------------------------------------- */
ITESimp::Statistics::Statistics()
- : d_arithSubstitutionsAdded(
- "preprocessing::passes::ITESimp::ArithSubstitutionsAdded", 0)
+ : d_arithSubstitutionsAdded(smtStatisticsRegistry().registerInt(
+ "preprocessing::passes::ITESimp::ArithSubstitutionsAdded"))
{
- smtStatisticsRegistry()->registerStat(&d_arithSubstitutionsAdded);
-}
-
-ITESimp::Statistics::~Statistics()
-{
- smtStatisticsRegistry()->unregisterStat(&d_arithSubstitutionsAdded);
}
bool ITESimp::doneSimpITE(AssertionPipeline* assertionsToPreprocess)
#include "preprocessing/preprocessing_pass.h"
#include "preprocessing/util/ite_utilities.h"
-#include "util/stats_histogram.h"
+#include "util/statistics_stats.h"
namespace cvc5 {
namespace preprocessing {
{
IntStat d_arithSubstitutionsAdded;
Statistics();
- ~Statistics();
};
bool doneSimpITE(AssertionPipeline *assertionsToPreprocesss);
}
MipLibTrick::Statistics::Statistics()
- : d_numMiplibAssertionsRemoved(
- "preprocessing::passes::MipLibTrick::numMiplibAssertionsRemoved", 0)
+ : d_numMiplibAssertionsRemoved(smtStatisticsRegistry().registerInt(
+ "preprocessing::passes::MipLibTrick::numMiplibAssertionsRemoved"))
{
- smtStatisticsRegistry()->registerStat(&d_numMiplibAssertionsRemoved);
-}
-
-MipLibTrick::Statistics::~Statistics()
-{
- smtStatisticsRegistry()->unregisterStat(&d_numMiplibAssertionsRemoved);
}
/** number of assertions removed by miplib pass */
IntStat d_numMiplibAssertionsRemoved;
Statistics();
- ~Statistics();
};
Statistics d_statistics;
/* -------------------------------------------------------------------------- */
NonClausalSimp::Statistics::Statistics()
- : d_numConstantProps(
- "preprocessing::passes::NonClausalSimp::NumConstantProps", 0)
+ : d_numConstantProps(smtStatisticsRegistry().registerInt(
+ "preprocessing::passes::NonClausalSimp::NumConstantProps"))
{
- smtStatisticsRegistry()->registerStat(&d_numConstantProps);
}
-NonClausalSimp::Statistics::~Statistics()
-{
- smtStatisticsRegistry()->unregisterStat(&d_numConstantProps);
-}
/* -------------------------------------------------------------------------- */
{
IntStat d_numConstantProps;
Statistics();
- ~Statistics();
};
Statistics d_statistics;
UnconstrainedSimplifier::UnconstrainedSimplifier(
PreprocessingPassContext* preprocContext)
: PreprocessingPass(preprocContext, "unconstrained-simplifier"),
- d_numUnconstrainedElim("preprocessor::number of unconstrained elims", 0),
+ d_numUnconstrainedElim(smtStatisticsRegistry().registerInt(
+ "preprocessor::number of unconstrained elims")),
d_context(preprocContext->getDecisionContext()),
d_substitutions(preprocContext->getDecisionContext())
{
- smtStatisticsRegistry()->registerStat(&d_numUnconstrainedElim);
-}
-
-UnconstrainedSimplifier::~UnconstrainedSimplifier()
-{
- smtStatisticsRegistry()->unregisterStat(&d_numUnconstrainedElim);
}
struct unc_preprocess_stack_element
#include "expr/node.h"
#include "preprocessing/preprocessing_pass.h"
#include "theory/substitutions.h"
-#include "util/statistics_registry.h"
+#include "util/statistics_stats.h"
namespace cvc5 {
namespace context {
{
public:
UnconstrainedSimplifier(PreprocessingPassContext* preprocContext);
- ~UnconstrainedSimplifier() override;
PreprocessingPassResult applyInternal(
AssertionPipeline* assertionsToPreprocess) override;
#include "smt/output_manager.h"
#include "smt/smt_engine_scope.h"
#include "smt/smt_statistics_registry.h"
+#include "util/statistics_stats.h"
namespace cvc5 {
namespace preprocessing {
PreprocessingPass::PreprocessingPass(PreprocessingPassContext* preprocContext,
const std::string& name)
- : d_name(name), d_timer("preprocessing::" + name) {
+ : d_name(name),
+ d_timer(smtStatisticsRegistry().registerTimer("preprocessing::" + name))
+{
d_preprocContext = preprocContext;
- smtStatisticsRegistry()->registerStat(&d_timer);
}
PreprocessingPass::~PreprocessingPass() {
Assert(smt::smtEngineInScope());
- if (smtStatisticsRegistry() != nullptr) {
- smtStatisticsRegistry()->unregisterStat(&d_timer);
- }
}
} // namespace preprocessing
#include <string>
-#include "util/statistics_registry.h"
-#include "util/stats_timer.h"
+#include "util/statistics_stats.h"
namespace cvc5 {
namespace preprocessing {
void ITECompressor::garbageCollect() { reset(); }
ITECompressor::Statistics::Statistics()
- : d_compressCalls("ite-simp::compressCalls", 0),
- d_skolemsAdded("ite-simp::skolems", 0)
+ : d_compressCalls(
+ smtStatisticsRegistry().registerInt("ite-simp::compressCalls")),
+ d_skolemsAdded(smtStatisticsRegistry().registerInt("ite-simp::skolems"))
{
- smtStatisticsRegistry()->registerStat(&d_compressCalls);
- smtStatisticsRegistry()->registerStat(&d_skolemsAdded);
-}
-ITECompressor::Statistics::~Statistics()
-{
- smtStatisticsRegistry()->unregisterStat(&d_compressCalls);
- smtStatisticsRegistry()->unregisterStat(&d_skolemsAdded);
}
Node ITECompressor::push_back_boolean(Node original, Node compressed)
}
ITESimplifier::Statistics::Statistics()
- : d_maxNonConstantsFolded("ite-simp::maxNonConstantsFolded", 0),
- d_unexpected("ite-simp::unexpected", 0),
- d_unsimplified("ite-simp::unsimplified", 0),
- d_exactMatchFold("ite-simp::exactMatchFold", 0),
- d_binaryPredFold("ite-simp::binaryPredFold", 0),
- d_specialEqualityFolds("ite-simp::specialEqualityFolds", 0),
- d_simpITEVisits("ite-simp::simpITE.visits", 0),
- d_inSmaller("ite-simp::inSmaller")
-{
- smtStatisticsRegistry()->registerStat(&d_maxNonConstantsFolded);
- smtStatisticsRegistry()->registerStat(&d_unexpected);
- smtStatisticsRegistry()->registerStat(&d_unsimplified);
- smtStatisticsRegistry()->registerStat(&d_exactMatchFold);
- smtStatisticsRegistry()->registerStat(&d_binaryPredFold);
- smtStatisticsRegistry()->registerStat(&d_specialEqualityFolds);
- smtStatisticsRegistry()->registerStat(&d_simpITEVisits);
- smtStatisticsRegistry()->registerStat(&d_inSmaller);
-}
-
-ITESimplifier::Statistics::~Statistics()
+ : d_maxNonConstantsFolded(
+ smtStatisticsRegistry().registerInt("ite-simp::maxNonConstantsFolded")),
+ d_unexpected(smtStatisticsRegistry().registerInt("ite-simp::unexpected")),
+ d_unsimplified(
+ smtStatisticsRegistry().registerInt("ite-simp::unsimplified")),
+ d_exactMatchFold(
+ smtStatisticsRegistry().registerInt("ite-simp::exactMatchFold")),
+ d_binaryPredFold(
+ smtStatisticsRegistry().registerInt("ite-simp::binaryPredFold")),
+ d_specialEqualityFolds(smtStatisticsRegistry().registerInt(
+ "ite-simp::specialEqualityFolds")),
+ d_simpITEVisits(
+ smtStatisticsRegistry().registerInt("ite-simp::simpITE.visits")),
+ d_inSmaller(smtStatisticsRegistry().registerHistogram<uint32_t>(
+ "ite-simp::inSmaller"))
{
- smtStatisticsRegistry()->unregisterStat(&d_maxNonConstantsFolded);
- smtStatisticsRegistry()->unregisterStat(&d_unexpected);
- smtStatisticsRegistry()->unregisterStat(&d_unsimplified);
- smtStatisticsRegistry()->unregisterStat(&d_exactMatchFold);
- smtStatisticsRegistry()->unregisterStat(&d_binaryPredFold);
- smtStatisticsRegistry()->unregisterStat(&d_specialEqualityFolds);
- smtStatisticsRegistry()->unregisterStat(&d_simpITEVisits);
- smtStatisticsRegistry()->unregisterStat(&d_inSmaller);
}
bool ITESimplifier::isConstantIte(TNode e)
#include "expr/node.h"
#include "util/hash.h"
-#include "util/statistics_registry.h"
-#include "util/stats_histogram.h"
+#include "util/statistics_stats.h"
namespace cvc5 {
namespace preprocessing {
IntStat d_compressCalls;
IntStat d_skolemsAdded;
Statistics();
- ~Statistics();
};
Statistics d_statistics;
}; /* class ITECompressor */
IntStat d_specialEqualityFolds;
IntStat d_simpITEVisits;
- IntegralHistogramStat<uint32_t> d_inSmaller;
+ HistogramStat<uint32_t> d_inSmaller;
Statistics();
- ~Statistics();
};
Statistics d_statistics;
// Destroy old instance before initializing new one to avoid issues with
// registering stats
d_satProof.reset();
- d_satProof.reset(new CoreSatProof(solver, d_context, ""));
+ d_satProof.reset(new CoreSatProof(solver, d_context, "satproof::"));
}
void ProofManager::initCnfProof(prop::CnfStream* cnfStream,
#include "expr/node.h"
#include "proof/clause_id.h"
#include "proof/proof_manager.h"
-#include "util/statistics_registry.h"
-#include "util/stats_histogram.h"
+#include "util/statistics_stats.h"
// Forward declarations.
namespace cvc5 {
* hasResolution(id) does not hold. */
const ResolutionChain& getResolutionChain(ClauseId id) const;
- const std::string& getName() const { return d_name; }
const ClauseId& getEmptyClauseId() const { return d_emptyClauseId; }
const IdSet& getSeenLearnt() const { return d_seenLearnt; }
const IdToConflicts& getAssumptionConflicts() const
IntStat d_numLearnedInProof;
IntStat d_numLemmasInProof;
AverageStat d_avgChainLength;
- IntegralHistogramStat<uint64_t> d_resChainLengths;
- IntegralHistogramStat<uint64_t> d_usedResChainLengths;
- IntegralHistogramStat<uint64_t> d_clauseGlue;
- IntegralHistogramStat<uint64_t> d_usedClauseGlue;
+ HistogramStat<uint64_t> d_resChainLengths;
+ HistogramStat<uint64_t> d_usedResChainLengths;
+ HistogramStat<uint64_t> d_clauseGlue;
+ HistogramStat<uint64_t> d_usedClauseGlue;
Statistics(const std::string& name);
- ~Statistics();
};
- std::string d_name;
-
const ClauseId d_emptyClauseId;
IdSet d_seenLearnt;
IdToConflicts d_assumptionConflictsDebug;
/// SatProof
template <class Solver>
-TSatProof<Solver>::TSatProof(Solver* solver, context::Context* context,
- const std::string& name, bool checkRes)
- : d_name(name),
- d_emptyClauseId(ClauseIdEmpty),
+TSatProof<Solver>::TSatProof(Solver* solver,
+ context::Context* context,
+ const std::string& name,
+ bool checkRes)
+ : d_emptyClauseId(ClauseIdEmpty),
d_seenLearnt(),
d_assumptionConflictsDebug(),
d_solver(solver),
d_seenInputs(),
d_seenLemmas(),
d_satProofConstructed(false),
- d_statistics(name) {
+ d_statistics(name)
+{
}
template <class Solver>
template <class Solver>
TSatProof<Solver>::Statistics::Statistics(const std::string& prefix)
- : d_numLearnedClauses("satproof::" + prefix + "::NumLearnedClauses", 0),
- d_numLearnedInProof("satproof::" + prefix + "::NumLearnedInProof", 0),
- d_numLemmasInProof("satproof::" + prefix + "::NumLemmasInProof", 0),
- d_avgChainLength("satproof::" + prefix + "::AvgResChainLength"),
- d_resChainLengths("satproof::" + prefix + "::ResChainLengthsHist"),
- d_usedResChainLengths("satproof::" + prefix +
- "::UsedResChainLengthsHist"),
- d_clauseGlue("satproof::" + prefix + "::ClauseGlueHist"),
- d_usedClauseGlue("satproof::" + prefix + "::UsedClauseGlueHist") {
- smtStatisticsRegistry()->registerStat(&d_numLearnedClauses);
- smtStatisticsRegistry()->registerStat(&d_numLearnedInProof);
- smtStatisticsRegistry()->registerStat(&d_numLemmasInProof);
- smtStatisticsRegistry()->registerStat(&d_avgChainLength);
- smtStatisticsRegistry()->registerStat(&d_resChainLengths);
- smtStatisticsRegistry()->registerStat(&d_usedResChainLengths);
- smtStatisticsRegistry()->registerStat(&d_clauseGlue);
- smtStatisticsRegistry()->registerStat(&d_usedClauseGlue);
-}
-
-template <class Solver>
-TSatProof<Solver>::Statistics::~Statistics() {
- smtStatisticsRegistry()->unregisterStat(&d_numLearnedClauses);
- smtStatisticsRegistry()->unregisterStat(&d_numLearnedInProof);
- smtStatisticsRegistry()->unregisterStat(&d_numLemmasInProof);
- smtStatisticsRegistry()->unregisterStat(&d_avgChainLength);
- smtStatisticsRegistry()->unregisterStat(&d_resChainLengths);
- smtStatisticsRegistry()->unregisterStat(&d_usedResChainLengths);
- smtStatisticsRegistry()->unregisterStat(&d_clauseGlue);
- smtStatisticsRegistry()->unregisterStat(&d_usedClauseGlue);
+ : d_numLearnedClauses(
+ smtStatisticsRegistry().registerInt(prefix + "NumLearnedClauses")),
+ d_numLearnedInProof(
+ smtStatisticsRegistry().registerInt(prefix + "NumLearnedInProof")),
+ d_numLemmasInProof(
+ smtStatisticsRegistry().registerInt(prefix + "NumLemmasInProof")),
+ d_avgChainLength(smtStatisticsRegistry().registerAverage(
+ prefix + "AvgResChainLength")),
+ d_resChainLengths(smtStatisticsRegistry().registerHistogram<uint64_t>(
+ prefix + "ResChainLengthsHist")),
+ d_usedResChainLengths(smtStatisticsRegistry().registerHistogram<uint64_t>(
+ prefix + "UsedResChainLengthsHist")),
+ d_clauseGlue(smtStatisticsRegistry().registerHistogram<uint64_t>(
+ prefix + "ClauseGlueHist")),
+ d_usedClauseGlue(smtStatisticsRegistry().registerHistogram<uint64_t>(
+ prefix + "UsedClauseGlueHist"))
+{
}
inline std::ostream& operator<<(std::ostream& out, cvc5::ClauseKind k)
namespace cvc5 {
namespace prop {
-BVMinisatSatSolver::BVMinisatSatSolver(StatisticsRegistry* registry, context::Context* mainSatContext, const std::string& name)
-: context::ContextNotifyObj(mainSatContext, false),
- d_minisat(new BVMinisat::SimpSolver(mainSatContext)),
- d_minisatNotify(nullptr),
- d_assertionsCount(0),
- d_assertionsRealCount(mainSatContext, 0),
- d_lastPropagation(mainSatContext, 0),
- d_statistics(registry, name)
+BVMinisatSatSolver::BVMinisatSatSolver(StatisticsRegistry& registry,
+ context::Context* mainSatContext,
+ const std::string& name)
+ : context::ContextNotifyObj(mainSatContext, false),
+ d_minisat(new BVMinisat::SimpSolver(mainSatContext)),
+ d_minisatNotify(nullptr),
+ d_assertionsCount(0),
+ d_assertionsRealCount(mainSatContext, 0),
+ d_lastPropagation(mainSatContext, 0),
+ d_statistics(registry, name)
{
d_statistics.init(d_minisat.get());
}
// Satistics for BVMinisatSatSolver
-BVMinisatSatSolver::Statistics::Statistics(StatisticsRegistry* registry,
+BVMinisatSatSolver::Statistics::Statistics(StatisticsRegistry& registry,
const std::string& prefix)
- : d_registry(registry),
- d_statStarts(prefix + "::bvminisat::starts"),
- d_statDecisions(prefix + "::bvminisat::decisions"),
- d_statRndDecisions(prefix + "::bvminisat::rnd_decisions"),
- d_statPropagations(prefix + "::bvminisat::propagations"),
- d_statConflicts(prefix + "::bvminisat::conflicts"),
- d_statClausesLiterals(prefix + "::bvminisat::clauses_literals"),
- d_statLearntsLiterals(prefix + "::bvminisat::learnts_literals"),
- d_statMaxLiterals(prefix + "::bvminisat::max_literals"),
- d_statTotLiterals(prefix + "::bvminisat::tot_literals"),
- d_statEliminatedVars(prefix + "::bvminisat::eliminated_vars"),
- d_statCallsToSolve(prefix + "::bvminisat::calls_to_solve", 0),
- d_statSolveTime(prefix + "::bvminisat::solve_time"),
- d_registerStats(!prefix.empty())
+ : d_statStarts(
+ registry.registerReference<int64_t>(prefix + "bvminisat::starts")),
+ d_statDecisions(
+ registry.registerReference<int64_t>(prefix + "bvminisat::decisions")),
+ d_statRndDecisions(registry.registerReference<int64_t>(
+ prefix + "bvminisat::rnd_decisions")),
+ d_statPropagations(registry.registerReference<int64_t>(
+ prefix + "bvminisat::propagations")),
+ d_statConflicts(
+ registry.registerReference<int64_t>(prefix + "bvminisat::conflicts")),
+ d_statClausesLiterals(registry.registerReference<int64_t>(
+ prefix + "bvminisat::clauses_literals")),
+ d_statLearntsLiterals(registry.registerReference<int64_t>(
+ prefix + "bvminisat::learnts_literals")),
+ d_statMaxLiterals(registry.registerReference<int64_t>(
+ prefix + "bvminisat::max_literals")),
+ d_statTotLiterals(registry.registerReference<int64_t>(
+ prefix + "bvminisat::tot_literals")),
+ d_statEliminatedVars(registry.registerReference<int64_t>(
+ prefix + "bvminisat::eliminated_vars")),
+ d_statCallsToSolve(
+ registry.registerInt(prefix + "bvminisat::calls_to_solve")),
+ d_statSolveTime(registry.registerTimer(prefix + "bvminisat::solve_time"))
{
if (!d_registerStats)
{
return;
}
-
- d_registry->registerStat(&d_statStarts);
- d_registry->registerStat(&d_statDecisions);
- d_registry->registerStat(&d_statRndDecisions);
- d_registry->registerStat(&d_statPropagations);
- d_registry->registerStat(&d_statConflicts);
- d_registry->registerStat(&d_statClausesLiterals);
- d_registry->registerStat(&d_statLearntsLiterals);
- d_registry->registerStat(&d_statMaxLiterals);
- d_registry->registerStat(&d_statTotLiterals);
- d_registry->registerStat(&d_statEliminatedVars);
- d_registry->registerStat(&d_statCallsToSolve);
- d_registry->registerStat(&d_statSolveTime);
-}
-
-BVMinisatSatSolver::Statistics::~Statistics() {
- if (!d_registerStats){
- return;
- }
- d_registry->unregisterStat(&d_statStarts);
- d_registry->unregisterStat(&d_statDecisions);
- d_registry->unregisterStat(&d_statRndDecisions);
- d_registry->unregisterStat(&d_statPropagations);
- d_registry->unregisterStat(&d_statConflicts);
- d_registry->unregisterStat(&d_statClausesLiterals);
- d_registry->unregisterStat(&d_statLearntsLiterals);
- d_registry->unregisterStat(&d_statMaxLiterals);
- d_registry->unregisterStat(&d_statTotLiterals);
- d_registry->unregisterStat(&d_statEliminatedVars);
- d_registry->unregisterStat(&d_statCallsToSolve);
- d_registry->unregisterStat(&d_statSolveTime);
}
void BVMinisatSatSolver::Statistics::init(BVMinisat::SimpSolver* minisat){
#include "prop/bvminisat/simp/SimpSolver.h"
#include "prop/sat_solver.h"
#include "util/resource_manager.h"
-#include "util/statistics_registry.h"
-#include "util/stats_timer.h"
+#include "util/statistics_stats.h"
namespace cvc5 {
namespace prop {
void contextNotifyPop() override;
public:
+ BVMinisatSatSolver(StatisticsRegistry& registry,
+ context::Context* mainSatContext,
+ const std::string& name = "");
+ virtual ~BVMinisatSatSolver();
- BVMinisatSatSolver(StatisticsRegistry* registry, context::Context* mainSatContext, const std::string& name = "");
- virtual ~BVMinisatSatSolver();
+ void setNotify(BVSatSolverNotify* notify) override;
- void setNotify(BVSatSolverNotify* notify) override;
+ ClauseId addClause(SatClause& clause, bool removable) override;
- ClauseId addClause(SatClause& clause, bool removable) override;
-
- ClauseId addXorClause(SatClause& clause, bool rhs, bool removable) override
- {
- Unreachable() << "Minisat does not support native XOR reasoning";
- return ClauseIdError;
- }
+ ClauseId addXorClause(SatClause& clause, bool rhs, bool removable) override
+ {
+ Unreachable() << "Minisat does not support native XOR reasoning";
+ return ClauseIdError;
+ }
SatValue propagate() override;
class Statistics {
public:
- StatisticsRegistry* d_registry;
- ReferenceStat<uint64_t> d_statStarts, d_statDecisions;
- ReferenceStat<uint64_t> d_statRndDecisions, d_statPropagations;
- ReferenceStat<uint64_t> d_statConflicts, d_statClausesLiterals;
- ReferenceStat<uint64_t> d_statLearntsLiterals, d_statMaxLiterals;
- ReferenceStat<uint64_t> d_statTotLiterals;
- ReferenceStat<int> d_statEliminatedVars;
- IntStat d_statCallsToSolve;
- TimerStat d_statSolveTime;
- bool d_registerStats;
- Statistics(StatisticsRegistry* registry, const std::string& prefix);
- ~Statistics();
- void init(BVMinisat::SimpSolver* minisat);
+ ReferenceStat<int64_t> d_statStarts, d_statDecisions;
+ ReferenceStat<int64_t> d_statRndDecisions, d_statPropagations;
+ ReferenceStat<int64_t> d_statConflicts, d_statClausesLiterals;
+ ReferenceStat<int64_t> d_statLearntsLiterals, d_statMaxLiterals;
+ ReferenceStat<int64_t> d_statTotLiterals;
+ ReferenceStat<int64_t> d_statEliminatedVars;
+ IntStat d_statCallsToSolve;
+ TimerStat d_statSolveTime;
+ bool d_registerStats;
+ Statistics(StatisticsRegistry& registry, const std::string& prefix);
+ void init(BVMinisat::SimpSolver* minisat);
};
Statistics d_statistics;
#ifdef CVC5_USE_CADICAL
#include "base/check.h"
+#include "util/statistics_registry.h"
namespace cvc5 {
namespace prop {
} // namespace helper functions
-CadicalSolver::CadicalSolver(StatisticsRegistry* registry,
+CadicalSolver::CadicalSolver(StatisticsRegistry& registry,
const std::string& name)
: d_solver(new CaDiCaL::Solver()),
// Note: CaDiCaL variables start with index 1 rather than 0 since negated
bool CadicalSolver::ok() const { return d_inSatMode; }
-CadicalSolver::Statistics::Statistics(StatisticsRegistry* registry,
+CadicalSolver::Statistics::Statistics(StatisticsRegistry& registry,
const std::string& prefix)
- : d_registry(registry),
- d_numSatCalls("theory::bv::" + prefix + "::cadical::calls_to_solve", 0),
- d_numVariables("theory::bv::" + prefix + "::cadical::variables", 0),
- d_numClauses("theory::bv::" + prefix + "::cadical::clauses", 0),
- d_solveTime("theory::bv::" + prefix + "::cadical::solve_time")
-{
- d_registry->registerStat(&d_numSatCalls);
- d_registry->registerStat(&d_numVariables);
- d_registry->registerStat(&d_numClauses);
- d_registry->registerStat(&d_solveTime);
-}
-
-CadicalSolver::Statistics::~Statistics() {
- d_registry->unregisterStat(&d_numSatCalls);
- d_registry->unregisterStat(&d_numVariables);
- d_registry->unregisterStat(&d_numClauses);
- d_registry->unregisterStat(&d_solveTime);
+ : d_numSatCalls(registry.registerInt(prefix + "cadical::calls_to_solve", 0)),
+ d_numVariables(registry.registerInt(prefix + "cadical::variables", 0)),
+ d_numClauses(registry.registerInt(prefix + "cadical::clauses", 0)),
+ d_solveTime(registry.registerTimer(prefix + "cadical::solve_time"))
+ {
}
} // namespace prop
#ifdef CVC5_USE_CADICAL
#include "prop/sat_solver.h"
-#include "util/stats_timer.h"
#include <cadical.hpp>
* Private to disallow creation outside of SatSolverFactory.
* Function init() must be called after creation.
*/
- CadicalSolver(StatisticsRegistry* registry, const std::string& name = "");
+ CadicalSolver(StatisticsRegistry& registry, const std::string& name = "");
/**
* Initialize SAT solver instance.
* Note: Split out to not call virtual functions in constructor.
struct Statistics
{
- StatisticsRegistry* d_registry;
IntStat d_numSatCalls;
IntStat d_numVariables;
IntStat d_numClauses;
TimerStat d_solveTime;
- Statistics(StatisticsRegistry* registry, const std::string& prefix);
- ~Statistics();
+ Statistics(StatisticsRegistry& registry, const std::string& prefix);
};
Statistics d_statistics;
* Implementation of the cryptominisat for cvc4 (bit-vectors).
*/
-#ifdef CVC5_USE_CRYPTOMINISAT
-
#include "prop/cryptominisat.h"
+#ifdef CVC5_USE_CRYPTOMINISAT
+
#include "base/check.h"
+#include "util/statistics_registry.h"
#include <cryptominisat5/cryptominisat.h>
} // helper functions
-CryptoMinisatSolver::CryptoMinisatSolver(StatisticsRegistry* registry,
+CryptoMinisatSolver::CryptoMinisatSolver(StatisticsRegistry& registry,
const std::string& name)
: d_solver(new CMSat::SATSolver()),
d_numVariables(0),
// Satistics for CryptoMinisatSolver
-CryptoMinisatSolver::Statistics::Statistics(StatisticsRegistry* registry,
- const std::string& prefix) :
- d_registry(registry),
- d_statCallsToSolve("theory::bv::"+prefix+"::cryptominisat::calls_to_solve", 0),
- d_xorClausesAdded("theory::bv::"+prefix+"::cryptominisat::xor_clauses", 0),
- d_clausesAdded("theory::bv::"+prefix+"::cryptominisat::clauses", 0),
- d_solveTime("theory::bv::"+prefix+"::cryptominisat::solve_time"),
- d_registerStats(!prefix.empty())
+CryptoMinisatSolver::Statistics::Statistics(StatisticsRegistry& registry,
+ const std::string& prefix)
+ : d_statCallsToSolve(registry.registerInt(prefix + "cryptominisat::calls_to_solve")),
+ d_xorClausesAdded(registry.registerInt(prefix + "cryptominisat::xor_clauses")),
+ d_clausesAdded(registry.registerInt(prefix + "cryptominisat::clauses")),
+ d_solveTime(registry.registerTimer(prefix + "cryptominisat::solve_time"))
{
- if (!d_registerStats)
- return;
-
- d_registry->registerStat(&d_statCallsToSolve);
- d_registry->registerStat(&d_xorClausesAdded);
- d_registry->registerStat(&d_clausesAdded);
- d_registry->registerStat(&d_solveTime);
-}
-
-CryptoMinisatSolver::Statistics::~Statistics() {
- if (!d_registerStats)
- return;
- d_registry->unregisterStat(&d_statCallsToSolve);
- d_registry->unregisterStat(&d_xorClausesAdded);
- d_registry->unregisterStat(&d_clausesAdded);
- d_registry->unregisterStat(&d_solveTime);
}
} // namespace prop
#ifdef CVC5_USE_CRYPTOMINISAT
#include "prop/sat_solver.h"
-#include "util/stats_timer.h"
// Cryptominisat has name clashes with the other Minisat implementations since
// the Minisat implementations export var_Undef, l_True, ... as macro whereas
class Statistics
{
public:
- StatisticsRegistry* d_registry;
IntStat d_statCallsToSolve;
IntStat d_xorClausesAdded;
IntStat d_clausesAdded;
TimerStat d_solveTime;
- bool d_registerStats;
- Statistics(StatisticsRegistry* registry, const std::string& prefix);
- ~Statistics();
+ Statistics(StatisticsRegistry& registry, const std::string& prefix);
};
/**
* Private to disallow creation outside of SatSolverFactory.
* Function init() must be called after creation.
*/
- CryptoMinisatSolver(StatisticsRegistry* registry,
+ CryptoMinisatSolver(StatisticsRegistry& registry,
const std::string& name = "");
/**
* Initialize SAT solver instance.
#ifdef CVC5_USE_KISSAT
#include "base/check.h"
+#include "util/statistics_registry.h"
namespace cvc5 {
namespace prop {
} // namespace
-KissatSolver::KissatSolver(StatisticsRegistry* registry,
+KissatSolver::KissatSolver(StatisticsRegistry& registry,
const std::string& name)
: d_solver(kissat_init()),
// Note: Kissat variables start with index 1 rather than 0 since negated
bool KissatSolver::ok() const { return d_okay; }
-KissatSolver::Statistics::Statistics(StatisticsRegistry* registry,
+KissatSolver::Statistics::Statistics(StatisticsRegistry& registry,
const std::string& prefix)
- : d_registry(registry),
- d_numSatCalls("theory::bv::" + prefix + "::Kissat::calls_to_solve", 0),
- d_numVariables("theory::bv::" + prefix + "::Kissat::variables", 0),
- d_numClauses("theory::bv::" + prefix + "::Kissat::clauses", 0),
- d_solveTime("theory::bv::" + prefix + "::Kissat::solve_time")
+ : d_numSatCalls(registry.registerInt(prefix + "Kissat::calls_to_solve")),
+ d_numVariables(registry.registerInt(prefix + "Kissat::variables")),
+ d_numClauses(registry.registerInt(prefix + "Kissat::clauses")),
+ d_solveTime(registry.registerTimer(prefix + "Kissat::solve_time"))
{
- d_registry->registerStat(&d_numSatCalls);
- d_registry->registerStat(&d_numVariables);
- d_registry->registerStat(&d_numClauses);
- d_registry->registerStat(&d_solveTime);
-}
-
-KissatSolver::Statistics::~Statistics()
-{
- d_registry->unregisterStat(&d_numSatCalls);
- d_registry->unregisterStat(&d_numVariables);
- d_registry->unregisterStat(&d_numClauses);
- d_registry->unregisterStat(&d_solveTime);
}
} // namespace prop
#ifdef CVC5_USE_KISSAT
#include "prop/sat_solver.h"
-#include "util/stats_timer.h"
extern "C" {
#include <kissat/kissat.h>
private:
struct Statistics
{
- StatisticsRegistry* d_registry;
IntStat d_numSatCalls;
IntStat d_numVariables;
IntStat d_numClauses;
TimerStat d_solveTime;
- Statistics(StatisticsRegistry* registry, const std::string& prefix);
- ~Statistics();
+ Statistics(StatisticsRegistry& registry, const std::string& prefix);
};
/**
* Private to disallow creation outside of SatSolverFactory.
* Function init() must be called after creation.
*/
- KissatSolver(StatisticsRegistry* registry, const std::string& name = "");
+ KissatSolver(StatisticsRegistry& registry, const std::string& name = "");
/**
* Initialize SAT solver instance.
* Note: Split out to not call virtual functions in constructor.
#include "options/decision_options.h"
#include "options/prop_options.h"
#include "options/smt_options.h"
-#include "prop/minisat/simp/SimpSolver.h"
#include "proof/clause_id.h"
#include "proof/sat_proof.h"
-#include "util/statistics_registry.h"
+#include "prop/minisat/simp/SimpSolver.h"
+#include "util/statistics_stats.h"
namespace cvc5 {
namespace prop {
//// DPllMinisatSatSolver
-MinisatSatSolver::MinisatSatSolver(StatisticsRegistry* registry) :
- d_minisat(NULL),
- d_context(NULL),
- d_statistics(registry)
+MinisatSatSolver::MinisatSatSolver(StatisticsRegistry& registry)
+ : d_minisat(NULL), d_context(NULL), d_statistics(registry)
{}
MinisatSatSolver::~MinisatSatSolver()
/// Statistics for MinisatSatSolver
-MinisatSatSolver::Statistics::Statistics(StatisticsRegistry* registry) :
- d_registry(registry),
- d_statStarts("sat::starts"),
- d_statDecisions("sat::decisions"),
- d_statRndDecisions("sat::rnd_decisions"),
- d_statPropagations("sat::propagations"),
- d_statConflicts("sat::conflicts"),
- d_statClausesLiterals("sat::clauses_literals"),
- d_statLearntsLiterals("sat::learnts_literals"),
- d_statMaxLiterals("sat::max_literals"),
- d_statTotLiterals("sat::tot_literals")
+MinisatSatSolver::Statistics::Statistics(StatisticsRegistry& registry)
+ : d_statStarts(registry.registerReference<int64_t>("sat::starts")),
+ d_statDecisions(registry.registerReference<int64_t>("sat::decisions")),
+ d_statRndDecisions(
+ registry.registerReference<int64_t>("sat::rnd_decisions")),
+ d_statPropagations(
+ registry.registerReference<int64_t>("sat::propagations")),
+ d_statConflicts(registry.registerReference<int64_t>("sat::conflicts")),
+ d_statClausesLiterals(
+ registry.registerReference<int64_t>("sat::clauses_literals")),
+ d_statLearntsLiterals(
+ registry.registerReference<int64_t>("sat::learnts_literals")),
+ d_statMaxLiterals(
+ registry.registerReference<int64_t>("sat::max_literals")),
+ d_statTotLiterals(
+ registry.registerReference<int64_t>("sat::tot_literals"))
{
- d_registry->registerStat(&d_statStarts);
- d_registry->registerStat(&d_statDecisions);
- d_registry->registerStat(&d_statRndDecisions);
- d_registry->registerStat(&d_statPropagations);
- d_registry->registerStat(&d_statConflicts);
- d_registry->registerStat(&d_statClausesLiterals);
- d_registry->registerStat(&d_statLearntsLiterals);
- d_registry->registerStat(&d_statMaxLiterals);
- d_registry->registerStat(&d_statTotLiterals);
-}
-
-MinisatSatSolver::Statistics::~Statistics() {
- d_registry->unregisterStat(&d_statStarts);
- d_registry->unregisterStat(&d_statDecisions);
- d_registry->unregisterStat(&d_statRndDecisions);
- d_registry->unregisterStat(&d_statPropagations);
- d_registry->unregisterStat(&d_statConflicts);
- d_registry->unregisterStat(&d_statClausesLiterals);
- d_registry->unregisterStat(&d_statLearntsLiterals);
- d_registry->unregisterStat(&d_statMaxLiterals);
- d_registry->unregisterStat(&d_statTotLiterals);
}
void MinisatSatSolver::Statistics::init(Minisat::SimpSolver* minisat){
class MinisatSatSolver : public CDCLTSatSolverInterface
{
public:
- MinisatSatSolver(StatisticsRegistry* registry);
+ MinisatSatSolver(StatisticsRegistry& registry);
~MinisatSatSolver() override;
static SatVariable toSatVariable(Minisat::Var var);
class Statistics {
private:
- StatisticsRegistry* d_registry;
- ReferenceStat<uint64_t> d_statStarts, d_statDecisions;
- ReferenceStat<uint64_t> d_statRndDecisions, d_statPropagations;
- ReferenceStat<uint64_t> d_statConflicts, d_statClausesLiterals;
- ReferenceStat<uint64_t> d_statLearntsLiterals, d_statMaxLiterals;
- ReferenceStat<uint64_t> d_statTotLiterals;
+ ReferenceStat<int64_t> d_statStarts, d_statDecisions;
+ ReferenceStat<int64_t> d_statRndDecisions, d_statPropagations;
+ ReferenceStat<int64_t> d_statConflicts, d_statClausesLiterals;
+ ReferenceStat<int64_t> d_statLearntsLiterals, d_statMaxLiterals;
+ ReferenceStat<int64_t> d_statTotLiterals;
+
public:
- Statistics(StatisticsRegistry* registry);
- ~Statistics();
- void init(Minisat::SimpSolver* d_minisat);
+ Statistics(StatisticsRegistry& registry);
+ void init(Minisat::SimpSolver* d_minisat);
};/* class MinisatSatSolver::Statistics */
Statistics d_statistics;
#include "proof/clause_id.h"
#include "prop/bv_sat_solver_notify.h"
#include "prop/sat_solver_types.h"
-#include "util/statistics_registry.h"
+#include "util/statistics_stats.h"
namespace cvc5 {
BVSatSolverInterface* SatSolverFactory::createMinisat(
context::Context* mainSatContext,
- StatisticsRegistry* registry,
+ StatisticsRegistry& registry,
const std::string& name)
{
return new BVMinisatSatSolver(registry, mainSatContext, name);
}
MinisatSatSolver* SatSolverFactory::createCDCLTMinisat(
- StatisticsRegistry* registry)
+ StatisticsRegistry& registry)
{
return new MinisatSatSolver(registry);
}
-SatSolver* SatSolverFactory::createCryptoMinisat(StatisticsRegistry* registry,
+SatSolver* SatSolverFactory::createCryptoMinisat(StatisticsRegistry& registry,
const std::string& name)
{
#ifdef CVC5_USE_CRYPTOMINISAT
#endif
}
-SatSolver* SatSolverFactory::createCadical(StatisticsRegistry* registry,
+SatSolver* SatSolverFactory::createCadical(StatisticsRegistry& registry,
const std::string& name)
{
#ifdef CVC5_USE_CADICAL
#endif
}
-SatSolver* SatSolverFactory::createKissat(StatisticsRegistry* registry,
+SatSolver* SatSolverFactory::createKissat(StatisticsRegistry& registry,
const std::string& name)
{
#ifdef CVC5_USE_KISSAT
#include "context/context.h"
#include "prop/minisat/minisat.h"
#include "prop/sat_solver.h"
-#include "util/statistics_registry.h"
+#include "util/statistics_stats.h"
namespace cvc5 {
namespace prop {
{
public:
static BVSatSolverInterface* createMinisat(context::Context* mainSatContext,
- StatisticsRegistry* registry,
+ StatisticsRegistry& registry,
const std::string& name = "");
- static MinisatSatSolver* createCDCLTMinisat(StatisticsRegistry* registry);
+ static MinisatSatSolver* createCDCLTMinisat(StatisticsRegistry& registry);
- static SatSolver* createCryptoMinisat(StatisticsRegistry* registry,
+ static SatSolver* createCryptoMinisat(StatisticsRegistry& registry,
const std::string& name = "");
- static SatSolver* createCadical(StatisticsRegistry* registry,
+ static SatSolver* createCadical(StatisticsRegistry& registry,
const std::string& name = "");
- static SatSolver* createKissat(StatisticsRegistry* registry,
+ static SatSolver* createKissat(StatisticsRegistry& registry,
const std::string& name = "");
}; /* class SatSolverFactory */
#include "smt/smt_statistics_registry.h"
#include "theory/rewriter.h"
#include "theory/theory_engine.h"
-#include "util/statistics_registry.h"
+#include "util/statistics_stats.h"
namespace cvc5 {
namespace prop {
#include "smt/smt_engine_stats.h"
#include "theory/rewriter.h"
#include "util/resource_manager.h"
+#include "util/statistics_registry.h"
using namespace cvc5::smt;
#include "options/options.h"
#include "theory/logic_info.h"
-#include "util/statistics.h"
#include "util/statistics_registry.h"
namespace cvc5 {
ProofPostprocessFinalCallback::ProofPostprocessFinalCallback(
ProofNodeManager* pnm)
- : d_ruleCount("finalProof::ruleCount"),
- d_totalRuleCount("finalProof::totalRuleCount", 0),
- d_minPedanticLevel("finalProof::minPedanticLevel", 10),
- d_numFinalProofs("finalProofs::numFinalProofs", 0),
+ : d_ruleCount(smtStatisticsRegistry().registerHistogram<PfRule>(
+ "finalProof::ruleCount")),
+ d_totalRuleCount(
+ smtStatisticsRegistry().registerInt("finalProof::totalRuleCount")),
+ d_minPedanticLevel(
+ smtStatisticsRegistry().registerInt("finalProof::minPedanticLevel")),
+ d_numFinalProofs(
+ smtStatisticsRegistry().registerInt("finalProofs::numFinalProofs")),
d_pnm(pnm),
d_pedanticFailure(false)
{
- smtStatisticsRegistry()->registerStat(&d_ruleCount);
- smtStatisticsRegistry()->registerStat(&d_totalRuleCount);
- smtStatisticsRegistry()->registerStat(&d_minPedanticLevel);
- smtStatisticsRegistry()->registerStat(&d_numFinalProofs);
-}
-
-ProofPostprocessFinalCallback::~ProofPostprocessFinalCallback()
-{
- smtStatisticsRegistry()->unregisterStat(&d_ruleCount);
- smtStatisticsRegistry()->unregisterStat(&d_totalRuleCount);
- smtStatisticsRegistry()->unregisterStat(&d_minPedanticLevel);
- smtStatisticsRegistry()->unregisterStat(&d_numFinalProofs);
+ d_minPedanticLevel += 10;
}
void ProofPostprocessFinalCallback::initializeUpdate()
#define CVC5__SMT__PROOF_POST_PROCESSOR_H
#include <map>
+#include <sstream>
#include <unordered_set>
#include "expr/proof_node_updater.h"
#include "smt/witness_form.h"
-#include "util/statistics_registry.h"
-#include "util/stats_histogram.h"
+#include "util/statistics_stats.h"
namespace cvc5 {
{
public:
ProofPostprocessFinalCallback(ProofNodeManager* pnm);
- ~ProofPostprocessFinalCallback();
/**
* Initialize, called once for each new ProofNode to process. This initializes
* static information to be used by successive calls to update.
private:
/** Counts number of postprocessed proof nodes for each kind of proof rule */
-
IntegralHistogramStat<PfRule> d_ruleCount;
+ HistogramStat<PfRule> d_ruleCount;
/** Total number of postprocessed rule applications */
IntStat d_totalRuleCount;
/** The minimum pedantic level of any rule encountered */
#include "theory/theory_engine.h"
#include "util/random.h"
#include "util/resource_manager.h"
+#include "util/statistics_registry.h"
// required for hacks related to old proofs for unsat cores
#include "base/configuration.h"
void SmtEngine::notifyStartParsing(const std::string& filename)
{
d_state->setFilename(filename);
- d_stats->d_driverFilename.set(filename);
+ d_env->getStatisticsRegistry().registerValue<std::string>("driver::filename",
+ filename);
// Copy the original options. This is called prior to beginning parsing.
// Hence reset should revert to these options, which note is after reading
// the command line.
}
void SmtEngine::setResultStatistic(const std::string& result) {
- d_stats->d_driverResult.set(result);
+ d_env->getStatisticsRegistry().registerValue<std::string>("driver::sat/unsat",
+ result);
}
-
void SmtEngine::setTotalTimeStatistic(double seconds) {
- d_stats->d_driverTotalTime.set(seconds);
+ d_env->getStatisticsRegistry().registerValue<double>("driver::totalTime",
+ seconds);
}
void SmtEngine::setLogicInternal()
if (key == "all-statistics")
{
vector<SExpr> stats;
- for (const auto& s: d_env->getStatisticsRegistry())
+ for (const auto& s : d_env->getStatisticsRegistry())
{
+ std::stringstream ss;
+ ss << *s.second;
vector<SExpr> v;
v.push_back(s.first);
- v.push_back(s.second);
+ v.push_back(ss.str());
stats.push_back(v);
}
return SExpr(stats);
return d_env->getNodeManager();
}
-Statistics SmtEngine::getStatistics() const
-{
- return Statistics(d_env->getStatisticsRegistry());
-}
-
SExpr SmtEngine::getStatistic(std::string name) const
{
- return d_env->getStatisticsRegistry().getStatistic(name);
+ const auto* val = d_env->getStatisticsRegistry().get(name);
+ std::stringstream ss;
+ ss << *val;
+ return SExpr({SExpr(name), SExpr(ss.str())});
}
void SmtEngine::printStatistics(std::ostream& out) const
{
- d_env->getStatisticsRegistry().flushInformation(out);
+ d_env->getStatisticsRegistry().print(out);
}
void SmtEngine::printStatisticsSafe(int fd) const
{
- d_env->getStatisticsRegistry().safeFlushInformation(fd);
+ d_env->getStatisticsRegistry().printSafe(fd);
+}
+
+void SmtEngine::printStatisticsDiff(std::ostream& out) const
+{
+ d_env->getStatisticsRegistry().printDiff(out);
+ d_env->getStatisticsRegistry().storeSnapshot();
}
void SmtEngine::setUserAttribute(const std::string& attr,
#include "theory/logic_info.h"
#include "util/result.h"
#include "util/sexpr.h"
-#include "util/statistics.h"
namespace cvc5 {
/** Permit access to the underlying NodeManager. */
NodeManager* getNodeManager() const;
- /** Export statistics from this SmtEngine. */
- Statistics getStatistics() const;
-
/** Get the value of one named statistic from this SmtEngine. */
SExpr getStatistic(std::string name) const;
- /** Flush statistics from this SmtEngine and the NodeManager it uses. */
+ /**
+ * Print statistics from the statistics registry in the env object owned by
+ * this SmtEngine.
+ */
void printStatistics(std::ostream& out) const;
/**
- * Flush statistics from this SmtEngine and the NodeManager it uses. Safe to
- * use in a signal handler.
+ * Print statistics from the statistics registry in the env object owned by
+ * this SmtEngine. Safe to use in a signal handler.
*/
void printStatisticsSafe(int fd) const;
+ /**
+ * Print the changes to the statistics from the statistics registry in the
+ * env object owned by this SmtEngine since this method was called the last
+ * time. Internally prints the diff and then stores a snapshot for the next
+ * call.
+ */
+ void printStatisticsDiff(std::ostream&) const;
+
/**
* Set user attribute.
* This function is called when an attribute is set by a user.
<< std::endl;
}
-StatisticsRegistry* SmtScope::currentStatisticsRegistry() {
+StatisticsRegistry& SmtScope::currentStatisticsRegistry()
+{
Assert(smtEngineInScope());
- return &(s_smtEngine_current->getStatisticsRegistry());
+ return s_smtEngine_current->getStatisticsRegistry();
}
} // namespace smt
* This returns the StatisticsRegistry attached to the currently in scope
* SmtEngine.
*/
- static StatisticsRegistry* currentStatisticsRegistry();
+ static StatisticsRegistry& currentStatisticsRegistry();
private:
/** The old SmtEngine, to be restored on destruction. */
namespace cvc5 {
namespace smt {
-SmtEngineStatistics::SmtEngineStatistics()
- : d_definitionExpansionTime("smt::SmtEngine::definitionExpansionTime"),
- d_numConstantProps("smt::SmtEngine::numConstantProps", 0),
- d_cnfConversionTime("smt::SmtEngine::cnfConversionTime"),
- d_numAssertionsPre("smt::SmtEngine::numAssertionsPreITERemoval", 0),
- d_numAssertionsPost("smt::SmtEngine::numAssertionsPostITERemoval", 0),
- d_checkModelTime("smt::SmtEngine::checkModelTime"),
- d_checkUnsatCoreTime("smt::SmtEngine::checkUnsatCoreTime"),
- d_solveTime("smt::SmtEngine::solveTime"),
- d_pushPopTime("smt::SmtEngine::pushPopTime"),
- d_processAssertionsTime("smt::SmtEngine::processAssertionsTime"),
- d_simplifiedToFalse("smt::SmtEngine::simplifiedToFalse", 0),
- d_driverFilename("driver::filename", ""),
- d_driverResult("driver::sat/unsat", ""),
- d_driverTotalTime("driver::totalTime", 0.0)
+SmtEngineStatistics::SmtEngineStatistics(const std::string& name)
+ : d_definitionExpansionTime(smtStatisticsRegistry().registerTimer(
+ name + "definitionExpansionTime")),
+ d_numConstantProps(
+ smtStatisticsRegistry().registerInt(name + "numConstantProps")),
+ d_cnfConversionTime(
+ smtStatisticsRegistry().registerTimer(name + "cnfConversionTime")),
+ d_numAssertionsPre(smtStatisticsRegistry().registerInt(
+ name + "numAssertionsPreITERemoval")),
+ d_numAssertionsPost(smtStatisticsRegistry().registerInt(
+ name + "numAssertionsPostITERemoval")),
+ d_checkModelTime(
+ smtStatisticsRegistry().registerTimer(name + "checkModelTime")),
+ d_checkUnsatCoreTime(
+ smtStatisticsRegistry().registerTimer(name + "checkUnsatCoreTime")),
+ d_solveTime(smtStatisticsRegistry().registerTimer(name + "solveTime")),
+ d_pushPopTime(
+ smtStatisticsRegistry().registerTimer(name + "pushPopTime")),
+ d_processAssertionsTime(smtStatisticsRegistry().registerTimer(
+ name + "processAssertionsTime")),
+ d_simplifiedToFalse(
+ smtStatisticsRegistry().registerInt(name + "simplifiedToFalse"))
{
- smtStatisticsRegistry()->registerStat(&d_definitionExpansionTime);
- smtStatisticsRegistry()->registerStat(&d_numConstantProps);
- smtStatisticsRegistry()->registerStat(&d_cnfConversionTime);
- smtStatisticsRegistry()->registerStat(&d_numAssertionsPre);
- smtStatisticsRegistry()->registerStat(&d_numAssertionsPost);
- smtStatisticsRegistry()->registerStat(&d_checkModelTime);
- smtStatisticsRegistry()->registerStat(&d_checkUnsatCoreTime);
- smtStatisticsRegistry()->registerStat(&d_solveTime);
- smtStatisticsRegistry()->registerStat(&d_pushPopTime);
- smtStatisticsRegistry()->registerStat(&d_processAssertionsTime);
- smtStatisticsRegistry()->registerStat(&d_simplifiedToFalse);
- smtStatisticsRegistry()->registerStat(&d_driverFilename);
- smtStatisticsRegistry()->registerStat(&d_driverResult);
- smtStatisticsRegistry()->registerStat(&d_driverTotalTime);
-}
-
-SmtEngineStatistics::~SmtEngineStatistics()
-{
- smtStatisticsRegistry()->unregisterStat(&d_definitionExpansionTime);
- smtStatisticsRegistry()->unregisterStat(&d_numConstantProps);
- smtStatisticsRegistry()->unregisterStat(&d_cnfConversionTime);
- smtStatisticsRegistry()->unregisterStat(&d_numAssertionsPre);
- smtStatisticsRegistry()->unregisterStat(&d_numAssertionsPost);
- smtStatisticsRegistry()->unregisterStat(&d_checkModelTime);
- smtStatisticsRegistry()->unregisterStat(&d_checkUnsatCoreTime);
- smtStatisticsRegistry()->unregisterStat(&d_solveTime);
- smtStatisticsRegistry()->unregisterStat(&d_pushPopTime);
- smtStatisticsRegistry()->unregisterStat(&d_processAssertionsTime);
- smtStatisticsRegistry()->unregisterStat(&d_simplifiedToFalse);
- smtStatisticsRegistry()->unregisterStat(&d_driverFilename);
- smtStatisticsRegistry()->unregisterStat(&d_driverResult);
- smtStatisticsRegistry()->unregisterStat(&d_driverTotalTime);
}
} // namespace smt
#ifndef CVC5__SMT__SMT_ENGINE_STATS_H
#define CVC5__SMT__SMT_ENGINE_STATS_H
-#include "util/statistics_registry.h"
-#include "util/stats_timer.h"
+#include "util/statistics_stats.h"
namespace cvc5 {
namespace smt {
struct SmtEngineStatistics
{
- SmtEngineStatistics();
- ~SmtEngineStatistics();
+ SmtEngineStatistics(const std::string& name = "smt::SmtEngine::");
/** time spent in definition-expansion */
TimerStat d_definitionExpansionTime;
/** number of constant propagations found during nonclausal simp */
/** Has something simplified to false? */
IntStat d_simplifiedToFalse;
-
- /** Name of the input file */
- BackedStat<std::string> d_driverFilename;
- /** Result of the last check */
- BackedStat<std::string> d_driverResult;
- /** Total time of the current run */
- BackedStat<double> d_driverTotalTime;
}; /* struct SmtEngineStatistics */
} // namespace smt
#include "smt/smt_statistics_registry.h"
#include "smt/smt_engine_scope.h"
-#include "util/statistics_registry.h"
+#include "util/statistics_stats.h"
namespace cvc5 {
-StatisticsRegistry* smtStatisticsRegistry() {
+StatisticsRegistry& smtStatisticsRegistry()
+{
return smt::SmtScope::currentStatisticsRegistry();
}
#pragma once
#include "util/statistics_registry.h"
+#include "util/statistics_stats.h"
namespace cvc5 {
* This returns the StatisticsRegistry attached to the currently in scope
* SmtEngine. This is a synonym for smt::SmtScope::currentStatisticsRegistry().
*/
-StatisticsRegistry* smtStatisticsRegistry();
+StatisticsRegistry& smtStatisticsRegistry();
} // namespace cvc5
};
ApproximateStatistics::ApproximateStatistics()
- : d_branchMaxDepth("z::approx::branchMaxDepth",0)
- , d_branchesMaxOnAVar("z::approx::branchesMaxOnAVar",0)
- , d_gaussianElimConstructTime("z::approx::gaussianElimConstruct::time")
- , d_gaussianElimConstruct("z::approx::gaussianElimConstruct::calls",0)
- , d_averageGuesses("z::approx::averageGuesses")
+ : d_branchMaxDepth(
+ smtStatisticsRegistry().registerInt("z::approx::branchMaxDepth")),
+ d_branchesMaxOnAVar(
+ smtStatisticsRegistry().registerInt("z::approx::branchesMaxOnAVar")),
+ d_gaussianElimConstructTime(smtStatisticsRegistry().registerTimer(
+ "z::approx::gaussianElimConstruct::time")),
+ d_gaussianElimConstruct(smtStatisticsRegistry().registerInt(
+ "z::approx::gaussianElimConstruct::calls")),
+ d_averageGuesses(
+ smtStatisticsRegistry().registerAverage("z::approx::averageGuesses"))
{
- smtStatisticsRegistry()->registerStat(&d_branchMaxDepth);
- smtStatisticsRegistry()->registerStat(&d_branchesMaxOnAVar);
-
- smtStatisticsRegistry()->registerStat(&d_gaussianElimConstructTime);
- smtStatisticsRegistry()->registerStat(&d_gaussianElimConstruct);
-
- smtStatisticsRegistry()->registerStat(&d_averageGuesses);
-}
-
-ApproximateStatistics::~ApproximateStatistics(){
- smtStatisticsRegistry()->unregisterStat(&d_branchMaxDepth);
- smtStatisticsRegistry()->unregisterStat(&d_branchesMaxOnAVar);
-
- smtStatisticsRegistry()->unregisterStat(&d_gaussianElimConstructTime);
- smtStatisticsRegistry()->unregisterStat(&d_gaussianElimConstruct);
-
- smtStatisticsRegistry()->unregisterStat(&d_averageGuesses);
}
Integer ApproximateSimplex::s_defaultMaxDenom(1<<26);
#include "util/dense_map.h"
#include "util/maybe.h"
#include "util/rational.h"
-#include "util/statistics_registry.h"
-#include "util/stats_timer.h"
+#include "util/statistics_stats.h"
namespace cvc5 {
namespace theory {
class ApproximateStatistics {
public:
ApproximateStatistics();
- ~ApproximateStatistics();
IntStat d_branchMaxDepth;
IntStat d_branchesMaxOnAVar;
ArithStaticLearner::~ArithStaticLearner(){
}
-ArithStaticLearner::Statistics::Statistics():
- d_iteMinMaxApplications("theory::arith::iteMinMaxApplications", 0),
- d_iteConstantApplications("theory::arith::iteConstantApplications", 0)
+ArithStaticLearner::Statistics::Statistics()
+ : d_iteMinMaxApplications(smtStatisticsRegistry().registerInt(
+ "theory::arith::iteMinMaxApplications")),
+ d_iteConstantApplications(smtStatisticsRegistry().registerInt(
+ "theory::arith::iteConstantApplications"))
{
- smtStatisticsRegistry()->registerStat(&d_iteMinMaxApplications);
- smtStatisticsRegistry()->registerStat(&d_iteConstantApplications);
-}
-
-ArithStaticLearner::Statistics::~Statistics(){
- smtStatisticsRegistry()->unregisterStat(&d_iteMinMaxApplications);
- smtStatisticsRegistry()->unregisterStat(&d_iteConstantApplications);
}
void ArithStaticLearner::staticLearning(TNode n, NodeBuilder& learned)
#include "context/cdhashmap.h"
#include "theory/arith/arith_utilities.h"
#include "theory/arith/delta_rational.h"
-#include "util/statistics_registry.h"
+#include "util/statistics_stats.h"
namespace cvc5 {
namespace context {
IntStat d_iteConstantApplications;
Statistics();
- ~Statistics();
};
Statistics d_statistics;
, d_statistics()
{ }
-AttemptSolutionSDP::Statistics::Statistics():
- d_searchTime("theory::arith::attempt::searchTime"),
- d_queueTime("theory::arith::attempt::queueTime"),
- d_conflicts("theory::arith::attempt::conflicts", 0)
+AttemptSolutionSDP::Statistics::Statistics()
+ : d_searchTime(smtStatisticsRegistry().registerTimer(
+ "theory::arith::attempt::searchTime")),
+ d_queueTime(smtStatisticsRegistry().registerTimer(
+ "theory::arith::attempt::queueTime")),
+ d_conflicts(smtStatisticsRegistry().registerInt(
+ "theory::arith::attempt::conflicts"))
{
- smtStatisticsRegistry()->registerStat(&d_searchTime);
- smtStatisticsRegistry()->registerStat(&d_queueTime);
- smtStatisticsRegistry()->registerStat(&d_conflicts);
-}
-
-AttemptSolutionSDP::Statistics::~Statistics(){
- smtStatisticsRegistry()->unregisterStat(&d_searchTime);
- smtStatisticsRegistry()->unregisterStat(&d_queueTime);
- smtStatisticsRegistry()->unregisterStat(&d_conflicts);
}
bool AttemptSolutionSDP::matchesNewValue(const DenseMap<DeltaRational>& nv, ArithVar v) const{
#pragma once
-#include "theory/arith/simplex.h"
#include "theory/arith/approx_simplex.h"
-#include "util/statistics_registry.h"
+#include "theory/arith/simplex.h"
+#include "util/statistics_stats.h"
namespace cvc5 {
namespace theory {
IntStat d_conflicts;
Statistics();
- ~Statistics();
} d_statistics;
};/* class AttemptSolutionSDP */
d_pfee = pfee;
}
-ArithCongruenceManager::Statistics::Statistics():
- d_watchedVariables("theory::arith::congruence::watchedVariables", 0),
- d_watchedVariableIsZero("theory::arith::congruence::watchedVariableIsZero", 0),
- d_watchedVariableIsNotZero("theory::arith::congruence::watchedVariableIsNotZero", 0),
- d_equalsConstantCalls("theory::arith::congruence::equalsConstantCalls", 0),
- d_propagations("theory::arith::congruence::propagations", 0),
- d_propagateConstraints("theory::arith::congruence::propagateConstraints", 0),
- d_conflicts("theory::arith::congruence::conflicts", 0)
+ArithCongruenceManager::Statistics::Statistics()
+ : d_watchedVariables(smtStatisticsRegistry().registerInt(
+ "theory::arith::congruence::watchedVariables")),
+ d_watchedVariableIsZero(smtStatisticsRegistry().registerInt(
+ "theory::arith::congruence::watchedVariableIsZero")),
+ d_watchedVariableIsNotZero(smtStatisticsRegistry().registerInt(
+ "theory::arith::congruence::watchedVariableIsNotZero")),
+ d_equalsConstantCalls(smtStatisticsRegistry().registerInt(
+ "theory::arith::congruence::equalsConstantCalls")),
+ d_propagations(smtStatisticsRegistry().registerInt(
+ "theory::arith::congruence::propagations")),
+ d_propagateConstraints(smtStatisticsRegistry().registerInt(
+ "theory::arith::congruence::propagateConstraints")),
+ d_conflicts(smtStatisticsRegistry().registerInt(
+ "theory::arith::congruence::conflicts"))
{
- smtStatisticsRegistry()->registerStat(&d_watchedVariables);
- smtStatisticsRegistry()->registerStat(&d_watchedVariableIsZero);
- smtStatisticsRegistry()->registerStat(&d_watchedVariableIsNotZero);
- smtStatisticsRegistry()->registerStat(&d_equalsConstantCalls);
- smtStatisticsRegistry()->registerStat(&d_propagations);
- smtStatisticsRegistry()->registerStat(&d_propagateConstraints);
- smtStatisticsRegistry()->registerStat(&d_conflicts);
-}
-
-ArithCongruenceManager::Statistics::~Statistics(){
- smtStatisticsRegistry()->unregisterStat(&d_watchedVariables);
- smtStatisticsRegistry()->unregisterStat(&d_watchedVariableIsZero);
- smtStatisticsRegistry()->unregisterStat(&d_watchedVariableIsNotZero);
- smtStatisticsRegistry()->unregisterStat(&d_equalsConstantCalls);
- smtStatisticsRegistry()->unregisterStat(&d_propagations);
- smtStatisticsRegistry()->unregisterStat(&d_propagateConstraints);
- smtStatisticsRegistry()->unregisterStat(&d_conflicts);
}
ArithCongruenceManager::ArithCongruenceNotify::ArithCongruenceNotify(ArithCongruenceManager& acm)
#include "context/cdlist.h"
#include "context/cdmaybe.h"
#include "context/cdtrail_queue.h"
-#include "theory/arith/arithvar.h"
#include "theory/arith/arith_utilities.h"
+#include "theory/arith/arithvar.h"
#include "theory/arith/callbacks.h"
#include "theory/arith/constraint_forward.h"
#include "theory/trust_node.h"
#include "theory/uf/equality_engine_notify.h"
#include "util/dense_map.h"
-#include "util/statistics_registry.h"
+#include "util/statistics_stats.h"
namespace cvc5 {
IntStat d_conflicts;
Statistics();
- ~Statistics();
} d_statistics;
};/* class ArithCongruenceManager */
Assert(d_nodetoConstraintMap.empty());
}
-ConstraintDatabase::Statistics::Statistics():
- d_unatePropagateCalls("theory::arith::cd::unatePropagateCalls", 0),
- d_unatePropagateImplications("theory::arith::cd::unatePropagateImplications", 0)
+ConstraintDatabase::Statistics::Statistics()
+ : d_unatePropagateCalls(smtStatisticsRegistry().registerInt(
+ "theory::arith::cd::unatePropagateCalls")),
+ d_unatePropagateImplications(smtStatisticsRegistry().registerInt(
+ "theory::arith::cd::unatePropagateImplications"))
{
- smtStatisticsRegistry()->registerStat(&d_unatePropagateCalls);
- smtStatisticsRegistry()->registerStat(&d_unatePropagateImplications);
-
-}
-
-ConstraintDatabase::Statistics::~Statistics(){
- smtStatisticsRegistry()->unregisterStat(&d_unatePropagateCalls);
- smtStatisticsRegistry()->unregisterStat(&d_unatePropagateImplications);
}
void ConstraintDatabase::deleteConstraintAndNegation(ConstraintP c){
#include "theory/arith/delta_rational.h"
#include "theory/arith/proof_macros.h"
#include "theory/trust_node.h"
-#include "util/statistics_registry.h"
+#include "util/statistics_stats.h"
namespace cvc5 {
IntStat d_unatePropagateImplications;
Statistics();
- ~Statistics();
} d_statistics;
}; /* ConstraintDatabase */
d_pureSubstitionIter(ctxt, 0),
d_decompositionLemmaQueue(ctxt) {}
-DioSolver::Statistics::Statistics() :
- d_conflictCalls("theory::arith::dio::conflictCalls",0),
- d_cutCalls("theory::arith::dio::cutCalls",0),
- d_cuts("theory::arith::dio::cuts",0),
- d_conflicts("theory::arith::dio::conflicts",0),
- d_conflictTimer("theory::arith::dio::conflictTimer"),
- d_cutTimer("theory::arith::dio::cutTimer")
+DioSolver::Statistics::Statistics()
+ : d_conflictCalls(smtStatisticsRegistry().registerInt(
+ "theory::arith::dio::conflictCalls")),
+ d_cutCalls(
+ smtStatisticsRegistry().registerInt("theory::arith::dio::cutCalls")),
+ d_cuts(smtStatisticsRegistry().registerInt("theory::arith::dio::cuts")),
+ d_conflicts(
+ smtStatisticsRegistry().registerInt("theory::arith::dio::conflicts")),
+ d_conflictTimer(smtStatisticsRegistry().registerTimer(
+ "theory::arith::dio::conflictTimer")),
+ d_cutTimer(
+ smtStatisticsRegistry().registerTimer("theory::arith::dio::cutTimer"))
{
- smtStatisticsRegistry()->registerStat(&d_conflictCalls);
- smtStatisticsRegistry()->registerStat(&d_cutCalls);
-
- smtStatisticsRegistry()->registerStat(&d_cuts);
- smtStatisticsRegistry()->registerStat(&d_conflicts);
-
- smtStatisticsRegistry()->registerStat(&d_conflictTimer);
- smtStatisticsRegistry()->registerStat(&d_cutTimer);
-}
-
-DioSolver::Statistics::~Statistics(){
- smtStatisticsRegistry()->unregisterStat(&d_conflictCalls);
- smtStatisticsRegistry()->unregisterStat(&d_cutCalls);
-
- smtStatisticsRegistry()->unregisterStat(&d_cuts);
- smtStatisticsRegistry()->unregisterStat(&d_conflicts);
-
- smtStatisticsRegistry()->unregisterStat(&d_conflictTimer);
- smtStatisticsRegistry()->unregisterStat(&d_cutTimer);
}
bool DioSolver::queueConditions(TrailIndex t){
#include "context/cdqueue.h"
#include "theory/arith/normal_form.h"
#include "util/rational.h"
-#include "util/statistics_registry.h"
-#include "util/stats_timer.h"
+#include "util/statistics_stats.h"
namespace cvc5 {
namespace context {
TimerStat d_cutTimer;
Statistics();
- ~Statistics();
};
Statistics d_statistics;
, d_statistics(d_pivots)
{ }
-DualSimplexDecisionProcedure::Statistics::Statistics(uint32_t& pivots):
- d_statUpdateConflicts("theory::arith::dual::UpdateConflicts", 0),
- d_processSignalsTime("theory::arith::dual::findConflictOnTheQueueTime"),
- d_simplexConflicts("theory::arith::dual::simplexConflicts",0),
- d_recentViolationCatches("theory::arith::dual::recentViolationCatches",0),
- d_searchTime("theory::arith::dual::searchTime"),
- d_finalCheckPivotCounter("theory::arith::dual::lastPivots", pivots)
+DualSimplexDecisionProcedure::Statistics::Statistics(uint32_t& pivots)
+ : d_statUpdateConflicts(smtStatisticsRegistry().registerInt(
+ "theory::arith::dual::UpdateConflicts")),
+ d_processSignalsTime(smtStatisticsRegistry().registerTimer(
+ "theory::arith::dual::findConflictOnTheQueueTime")),
+ d_simplexConflicts(smtStatisticsRegistry().registerInt(
+ "theory::arith::dual::simplexConflicts")),
+ d_recentViolationCatches(smtStatisticsRegistry().registerInt(
+ "theory::arith::dual::recentViolationCatches")),
+ d_searchTime(smtStatisticsRegistry().registerTimer(
+ "theory::arith::dual::searchTime")),
+ d_finalCheckPivotCounter(
+ smtStatisticsRegistry().registerReference<uint32_t>(
+ "theory::arith::dual::lastPivots", pivots))
{
- smtStatisticsRegistry()->registerStat(&d_statUpdateConflicts);
- smtStatisticsRegistry()->registerStat(&d_processSignalsTime);
- smtStatisticsRegistry()->registerStat(&d_simplexConflicts);
- smtStatisticsRegistry()->registerStat(&d_recentViolationCatches);
- smtStatisticsRegistry()->registerStat(&d_searchTime);
- smtStatisticsRegistry()->registerStat(&d_finalCheckPivotCounter);
-}
-
-DualSimplexDecisionProcedure::Statistics::~Statistics(){
- smtStatisticsRegistry()->unregisterStat(&d_statUpdateConflicts);
- smtStatisticsRegistry()->unregisterStat(&d_processSignalsTime);
- smtStatisticsRegistry()->unregisterStat(&d_simplexConflicts);
- smtStatisticsRegistry()->unregisterStat(&d_recentViolationCatches);
- smtStatisticsRegistry()->unregisterStat(&d_searchTime);
- smtStatisticsRegistry()->unregisterStat(&d_finalCheckPivotCounter);
}
Result::Sat DualSimplexDecisionProcedure::dualFindModel(bool exactResult){
#pragma once
#include "theory/arith/simplex.h"
-#include "util/statistics_registry.h"
+#include "util/statistics_stats.h"
namespace cvc5 {
namespace theory {
ReferenceStat<uint32_t> d_finalCheckPivotCounter;
Statistics(uint32_t& pivots);
- ~Statistics();
} d_statistics;
};/* class DualSimplexDecisionProcedure */
(*d_amount) = am;
}
-ErrorSet::Statistics::Statistics():
- d_enqueues("theory::arith::pqueue::enqueues", 0),
- d_enqueuesCollection("theory::arith::pqueue::enqueuesCollection", 0),
- d_enqueuesDiffMode("theory::arith::pqueue::enqueuesDiffMode", 0),
- d_enqueuesVarOrderMode("theory::arith::pqueue::enqueuesVarOrderMode", 0),
- d_enqueuesCollectionDuplicates("theory::arith::pqueue::enqueuesCollectionDuplicates", 0),
- d_enqueuesVarOrderModeDuplicates("theory::arith::pqueue::enqueuesVarOrderModeDuplicates", 0)
+ErrorSet::Statistics::Statistics()
+ : d_enqueues(
+ smtStatisticsRegistry().registerInt("theory::arith::pqueue::enqueues")),
+ d_enqueuesCollection(smtStatisticsRegistry().registerInt(
+ "theory::arith::pqueue::enqueuesCollection")),
+ d_enqueuesDiffMode(smtStatisticsRegistry().registerInt(
+ "theory::arith::pqueue::enqueuesDiffMode")),
+ d_enqueuesVarOrderMode(smtStatisticsRegistry().registerInt(
+ "theory::arith::pqueue::enqueuesVarOrderMode")),
+ d_enqueuesCollectionDuplicates(smtStatisticsRegistry().registerInt(
+ "theory::arith::pqueue::enqueuesCollectionDuplicates")),
+ d_enqueuesVarOrderModeDuplicates(smtStatisticsRegistry().registerInt(
+ "theory::arith::pqueue::enqueuesVarOrderModeDuplicates"))
{
- smtStatisticsRegistry()->registerStat(&d_enqueues);
- smtStatisticsRegistry()->registerStat(&d_enqueuesCollection);
- smtStatisticsRegistry()->registerStat(&d_enqueuesDiffMode);
- smtStatisticsRegistry()->registerStat(&d_enqueuesVarOrderMode);
- smtStatisticsRegistry()->registerStat(&d_enqueuesCollectionDuplicates);
- smtStatisticsRegistry()->registerStat(&d_enqueuesVarOrderModeDuplicates);
-}
-
-ErrorSet::Statistics::~Statistics(){
- smtStatisticsRegistry()->unregisterStat(&d_enqueues);
- smtStatisticsRegistry()->unregisterStat(&d_enqueuesCollection);
- smtStatisticsRegistry()->unregisterStat(&d_enqueuesDiffMode);
- smtStatisticsRegistry()->unregisterStat(&d_enqueuesVarOrderMode);
- smtStatisticsRegistry()->unregisterStat(&d_enqueuesCollectionDuplicates);
- smtStatisticsRegistry()->unregisterStat(&d_enqueuesVarOrderModeDuplicates);
}
ErrorSet::ErrorSet(ArithVariables& vars,
#include "theory/arith/partial_model.h"
#include "theory/arith/tableau_sizes.h"
#include "util/bin_heap.h"
-#include "util/statistics_registry.h"
+#include "util/statistics_stats.h"
namespace cvc5 {
namespace theory {
IntStat d_enqueuesVarOrderModeDuplicates;
Statistics();
- ~Statistics();
};
Statistics d_statistics;
#include "smt/smt_statistics_registry.h"
#include "theory/arith/constraint.h"
#include "theory/arith/error_set.h"
-#include "util/statistics_registry.h"
+#include "util/statistics_stats.h"
using namespace std;
namespace theory {
namespace arith {
-
-FCSimplexDecisionProcedure::FCSimplexDecisionProcedure(LinearEqualityModule& linEq, ErrorSet& errors, RaiseConflict conflictChannel, TempVarMalloc tvmalloc)
- : SimplexDecisionProcedure(linEq, errors, conflictChannel, tvmalloc)
- , d_focusSize(0)
- , d_focusErrorVar(ARITHVAR_SENTINEL)
- , d_focusCoefficients()
- , d_pivotBudget(0)
- , d_prevWitnessImprovement(AntiProductive)
- , d_witnessImprovementInARow(0)
- , d_sgnDisagreements()
- , d_statistics(d_pivots)
+FCSimplexDecisionProcedure::FCSimplexDecisionProcedure(
+ LinearEqualityModule& linEq,
+ ErrorSet& errors,
+ RaiseConflict conflictChannel,
+ TempVarMalloc tvmalloc)
+ : SimplexDecisionProcedure(linEq, errors, conflictChannel, tvmalloc),
+ d_focusSize(0),
+ d_focusErrorVar(ARITHVAR_SENTINEL),
+ d_focusCoefficients(),
+ d_pivotBudget(0),
+ d_prevWitnessImprovement(AntiProductive),
+ d_witnessImprovementInARow(0),
+ d_sgnDisagreements(),
+ d_statistics("theory::arith::FC::", d_pivots)
{ }
-FCSimplexDecisionProcedure::Statistics::Statistics(uint32_t& pivots):
- d_initialSignalsTime("theory::arith::FC::initialProcessTime"),
- d_initialConflicts("theory::arith::FC::UpdateConflicts", 0),
- d_fcFoundUnsat("theory::arith::FC::FoundUnsat", 0),
- d_fcFoundSat("theory::arith::FC::FoundSat", 0),
- d_fcMissed("theory::arith::FC::Missed", 0),
- d_fcTimer("theory::arith::FC::Timer"),
- d_fcFocusConstructionTimer("theory::arith::FC::Construction"),
- d_selectUpdateForDualLike("theory::arith::FC::selectUpdateForDualLike"),
- d_selectUpdateForPrimal("theory::arith::FC::selectUpdateForPrimal"),
- d_finalCheckPivotCounter("theory::arith::FC::lastPivots", pivots)
+FCSimplexDecisionProcedure::Statistics::Statistics(const std::string& name,
+ uint32_t& pivots)
+ : d_initialSignalsTime(
+ smtStatisticsRegistry().registerTimer(name + "initialProcessTime")),
+ d_initialConflicts(
+ smtStatisticsRegistry().registerInt(name + "UpdateConflicts")),
+ d_fcFoundUnsat(smtStatisticsRegistry().registerInt(name + "FoundUnsat")),
+ d_fcFoundSat(smtStatisticsRegistry().registerInt(name + "FoundSat")),
+ d_fcMissed(smtStatisticsRegistry().registerInt(name + "Missed")),
+ d_fcTimer(smtStatisticsRegistry().registerTimer(name + "Timer")),
+ d_fcFocusConstructionTimer(
+ smtStatisticsRegistry().registerTimer(name + "Construction")),
+ d_selectUpdateForDualLike(smtStatisticsRegistry().registerTimer(
+ name + "selectUpdateForDualLike")),
+ d_selectUpdateForPrimal(smtStatisticsRegistry().registerTimer(
+ name + "selectUpdateForPrimal")),
+ d_finalCheckPivotCounter(
+ smtStatisticsRegistry().registerReference<uint32_t>(
+ name + "lastPivots", pivots))
{
- smtStatisticsRegistry()->registerStat(&d_initialSignalsTime);
- smtStatisticsRegistry()->registerStat(&d_initialConflicts);
-
- smtStatisticsRegistry()->registerStat(&d_fcFoundUnsat);
- smtStatisticsRegistry()->registerStat(&d_fcFoundSat);
- smtStatisticsRegistry()->registerStat(&d_fcMissed);
-
- smtStatisticsRegistry()->registerStat(&d_fcTimer);
- smtStatisticsRegistry()->registerStat(&d_fcFocusConstructionTimer);
-
- smtStatisticsRegistry()->registerStat(&d_selectUpdateForDualLike);
- smtStatisticsRegistry()->registerStat(&d_selectUpdateForPrimal);
-
- smtStatisticsRegistry()->registerStat(&d_finalCheckPivotCounter);
-}
-
-FCSimplexDecisionProcedure::Statistics::~Statistics(){
- smtStatisticsRegistry()->unregisterStat(&d_initialSignalsTime);
- smtStatisticsRegistry()->unregisterStat(&d_initialConflicts);
-
- smtStatisticsRegistry()->unregisterStat(&d_fcFoundUnsat);
- smtStatisticsRegistry()->unregisterStat(&d_fcFoundSat);
- smtStatisticsRegistry()->unregisterStat(&d_fcMissed);
-
- smtStatisticsRegistry()->unregisterStat(&d_fcTimer);
- smtStatisticsRegistry()->unregisterStat(&d_fcFocusConstructionTimer);
-
- smtStatisticsRegistry()->unregisterStat(&d_selectUpdateForDualLike);
- smtStatisticsRegistry()->unregisterStat(&d_selectUpdateForPrimal);
-
- smtStatisticsRegistry()->unregisterStat(&d_finalCheckPivotCounter);
}
Result::Sat FCSimplexDecisionProcedure::findModel(bool exactResult){
#include "theory/arith/simplex.h"
#include "theory/arith/simplex_update.h"
#include "util/dense_map.h"
-#include "util/statistics_registry.h"
+#include "util/statistics_stats.h"
namespace cvc5 {
namespace theory {
ReferenceStat<uint32_t> d_finalCheckPivotCounter;
- Statistics(uint32_t& pivots);
- ~Statistics();
+ Statistics(const std::string& name, uint32_t& pivots);
} d_statistics;
};/* class FCSimplexDecisionProcedure */
InferenceManager::InferenceManager(TheoryArith& ta,
ArithState& astate,
ProofNodeManager* pnm)
- : InferenceManagerBuffered(ta, astate, pnm, "theory::arith")
+ : InferenceManagerBuffered(ta, astate, pnm, "theory::arith::")
{
}
d_trackCallback(this)
{}
-LinearEqualityModule::Statistics::Statistics():
- d_statPivots("theory::arith::pivots",0),
- d_statUpdates("theory::arith::updates",0),
- d_pivotTime("theory::arith::pivotTime"),
- d_adjTime("theory::arith::adjTime"),
- d_weakeningAttempts("theory::arith::weakening::attempts",0),
- d_weakeningSuccesses("theory::arith::weakening::success",0),
- d_weakenings("theory::arith::weakening::total",0),
- d_weakenTime("theory::arith::weakening::time"),
- d_forceTime("theory::arith::forcing::time")
+LinearEqualityModule::Statistics::Statistics()
+ : d_statPivots(
+ smtStatisticsRegistry().registerInt("theory::arith::pivots")),
+ d_statUpdates(
+ smtStatisticsRegistry().registerInt("theory::arith::updates")),
+ d_pivotTime(
+ smtStatisticsRegistry().registerTimer("theory::arith::pivotTime")),
+ d_adjTime(
+ smtStatisticsRegistry().registerTimer("theory::arith::adjTime")),
+ d_weakeningAttempts(smtStatisticsRegistry().registerInt(
+ "theory::arith::weakening::attempts")),
+ d_weakeningSuccesses(smtStatisticsRegistry().registerInt(
+ "theory::arith::weakening::success")),
+ d_weakenings(smtStatisticsRegistry().registerInt(
+ "theory::arith::weakening::total")),
+ d_weakenTime(smtStatisticsRegistry().registerTimer(
+ "theory::arith::weakening::time")),
+ d_forceTime(
+ smtStatisticsRegistry().registerTimer("theory::arith::forcing::time"))
{
- smtStatisticsRegistry()->registerStat(&d_statPivots);
- smtStatisticsRegistry()->registerStat(&d_statUpdates);
-
- smtStatisticsRegistry()->registerStat(&d_pivotTime);
- smtStatisticsRegistry()->registerStat(&d_adjTime);
-
- smtStatisticsRegistry()->registerStat(&d_weakeningAttempts);
- smtStatisticsRegistry()->registerStat(&d_weakeningSuccesses);
- smtStatisticsRegistry()->registerStat(&d_weakenings);
- smtStatisticsRegistry()->registerStat(&d_weakenTime);
- smtStatisticsRegistry()->registerStat(&d_forceTime);
-}
-
-LinearEqualityModule::Statistics::~Statistics(){
- smtStatisticsRegistry()->unregisterStat(&d_statPivots);
- smtStatisticsRegistry()->unregisterStat(&d_statUpdates);
- smtStatisticsRegistry()->unregisterStat(&d_pivotTime);
- smtStatisticsRegistry()->unregisterStat(&d_adjTime);
-
-
- smtStatisticsRegistry()->unregisterStat(&d_weakeningAttempts);
- smtStatisticsRegistry()->unregisterStat(&d_weakeningSuccesses);
- smtStatisticsRegistry()->unregisterStat(&d_weakenings);
- smtStatisticsRegistry()->unregisterStat(&d_weakenTime);
- smtStatisticsRegistry()->unregisterStat(&d_forceTime);
}
void LinearEqualityModule::includeBoundUpdate(ArithVar v, const BoundsInfo& prev){
#include "theory/arith/simplex_update.h"
#include "theory/arith/tableau.h"
#include "util/maybe.h"
-#include "util/statistics_registry.h"
-#include "util/stats_timer.h"
+#include "util/statistics_stats.h"
namespace cvc5 {
namespace theory {
TimerStat d_forceTime;
Statistics();
- ~Statistics();
};
mutable Statistics d_statistics;
namespace nl {
NlStats::NlStats()
- : d_mbrRuns("nl::mbrRuns", 0),
- d_checkRuns("nl::checkRuns", 0)
+ : d_mbrRuns(smtStatisticsRegistry().registerInt("nl::mbrRuns")),
+ d_checkRuns(smtStatisticsRegistry().registerInt("nl::checkRuns"))
{
- smtStatisticsRegistry()->registerStat(&d_mbrRuns);
- smtStatisticsRegistry()->registerStat(&d_checkRuns);
-}
-
-NlStats::~NlStats()
-{
- smtStatisticsRegistry()->unregisterStat(&d_mbrRuns);
- smtStatisticsRegistry()->unregisterStat(&d_checkRuns);
}
} // namespace nl
#ifndef CVC5__THEORY__ARITH__NL__STATS_H
#define CVC5__THEORY__ARITH__NL__STATS_H
-#include "util/statistics_registry.h"
+#include "util/statistics_stats.h"
namespace cvc5 {
namespace theory {
{
public:
NlStats();
- ~NlStats();
/**
* Number of calls to NonlinearExtension::modelBasedRefinement. Notice this
* may make multiple calls to NonlinearExtension::checkLastCall.
#include "theory/arith/error_set.h"
#include "theory/arith/linear_equality.h"
#include "theory/arith/tableau.h"
+#include "util/statistics_value.h"
using namespace std;
#include "theory/arith/partial_model.h"
#include "util/dense_map.h"
#include "util/result.h"
-#include "util/statistics_registry.h"
-#include "util/stats_timer.h"
+#include "util/statistics_stats.h"
namespace cvc5 {
namespace theory {
#include "theory/arith/constraint.h"
#include "theory/arith/error_set.h"
#include "theory/arith/tableau.h"
-#include "util/statistics_registry.h"
+#include "util/statistics_stats.h"
using namespace std;
namespace theory {
namespace arith {
-
-SumOfInfeasibilitiesSPD::SumOfInfeasibilitiesSPD(LinearEqualityModule& linEq, ErrorSet& errors, RaiseConflict conflictChannel, TempVarMalloc tvmalloc)
- : SimplexDecisionProcedure(linEq, errors, conflictChannel, tvmalloc)
- , d_soiVar(ARITHVAR_SENTINEL)
- , d_pivotBudget(0)
- , d_prevWitnessImprovement(AntiProductive)
- , d_witnessImprovementInARow(0)
- , d_sgnDisagreements()
- , d_statistics(d_pivots)
+SumOfInfeasibilitiesSPD::SumOfInfeasibilitiesSPD(LinearEqualityModule& linEq,
+ ErrorSet& errors,
+ RaiseConflict conflictChannel,
+ TempVarMalloc tvmalloc)
+ : SimplexDecisionProcedure(linEq, errors, conflictChannel, tvmalloc),
+ d_soiVar(ARITHVAR_SENTINEL),
+ d_pivotBudget(0),
+ d_prevWitnessImprovement(AntiProductive),
+ d_witnessImprovementInARow(0),
+ d_sgnDisagreements(),
+ d_statistics("theory::arith::SOI", d_pivots)
{ }
-SumOfInfeasibilitiesSPD::Statistics::Statistics(uint32_t& pivots):
- d_initialSignalsTime("theory::arith::SOI::initialProcessTime"),
- d_initialConflicts("theory::arith::SOI::UpdateConflicts", 0),
- d_soiFoundUnsat("theory::arith::SOI::FoundUnsat", 0),
- d_soiFoundSat("theory::arith::SOI::FoundSat", 0),
- d_soiMissed("theory::arith::SOI::Missed", 0),
- d_soiConflicts("theory::arith::SOI::ConfMin::num", 0),
- d_hasToBeMinimal("theory::arith::SOI::HasToBeMin", 0),
- d_maybeNotMinimal("theory::arith::SOI::MaybeNotMin", 0),
- d_soiTimer("theory::arith::SOI::Time"),
- d_soiFocusConstructionTimer("theory::arith::SOI::Construction"),
- d_soiConflictMinimization("theory::arith::SOI::Conflict::Minimization"),
- d_selectUpdateForSOI("theory::arith::SOI::selectSOI"),
- d_finalCheckPivotCounter("theory::arith::SOI::lastPivots", pivots)
+SumOfInfeasibilitiesSPD::Statistics::Statistics(const std::string& name,
+ uint32_t& pivots)
+ : d_initialSignalsTime(
+ smtStatisticsRegistry().registerTimer(name + "initialProcessTime")),
+ d_initialConflicts(
+ smtStatisticsRegistry().registerInt(name + "UpdateConflicts")),
+ d_soiFoundUnsat(smtStatisticsRegistry().registerInt(name + "FoundUnsat")),
+ d_soiFoundSat(smtStatisticsRegistry().registerInt(name + "FoundSat")),
+ d_soiMissed(smtStatisticsRegistry().registerInt(name + "Missed")),
+ d_soiConflicts(
+ smtStatisticsRegistry().registerInt(name + "ConfMin::num")),
+ d_hasToBeMinimal(
+ smtStatisticsRegistry().registerInt(name + "HasToBeMin")),
+ d_maybeNotMinimal(
+ smtStatisticsRegistry().registerInt(name + "MaybeNotMin")),
+ d_soiTimer(smtStatisticsRegistry().registerTimer(name + "Time")),
+ d_soiFocusConstructionTimer(
+ smtStatisticsRegistry().registerTimer(name + "Construction")),
+ d_soiConflictMinimization(smtStatisticsRegistry().registerTimer(
+ name + "Conflict::Minimization")),
+ d_selectUpdateForSOI(
+ smtStatisticsRegistry().registerTimer(name + "selectSOI")),
+ d_finalCheckPivotCounter(
+ smtStatisticsRegistry().registerReference<uint32_t>(
+ name + "lastPivots", pivots))
{
- smtStatisticsRegistry()->registerStat(&d_initialSignalsTime);
- smtStatisticsRegistry()->registerStat(&d_initialConflicts);
-
- smtStatisticsRegistry()->registerStat(&d_soiFoundUnsat);
- smtStatisticsRegistry()->registerStat(&d_soiFoundSat);
- smtStatisticsRegistry()->registerStat(&d_soiMissed);
-
- smtStatisticsRegistry()->registerStat(&d_soiConflicts);
- smtStatisticsRegistry()->registerStat(&d_hasToBeMinimal);
- smtStatisticsRegistry()->registerStat(&d_maybeNotMinimal);
-
- smtStatisticsRegistry()->registerStat(&d_soiTimer);
- smtStatisticsRegistry()->registerStat(&d_soiFocusConstructionTimer);
-
- smtStatisticsRegistry()->registerStat(&d_soiConflictMinimization);
-
- smtStatisticsRegistry()->registerStat(&d_selectUpdateForSOI);
-
- smtStatisticsRegistry()->registerStat(&d_finalCheckPivotCounter);
-}
-
-SumOfInfeasibilitiesSPD::Statistics::~Statistics(){
- smtStatisticsRegistry()->unregisterStat(&d_initialSignalsTime);
- smtStatisticsRegistry()->unregisterStat(&d_initialConflicts);
-
- smtStatisticsRegistry()->unregisterStat(&d_soiFoundUnsat);
- smtStatisticsRegistry()->unregisterStat(&d_soiFoundSat);
- smtStatisticsRegistry()->unregisterStat(&d_soiMissed);
-
- smtStatisticsRegistry()->unregisterStat(&d_soiConflicts);
- smtStatisticsRegistry()->unregisterStat(&d_hasToBeMinimal);
- smtStatisticsRegistry()->unregisterStat(&d_maybeNotMinimal);
-
- smtStatisticsRegistry()->unregisterStat(&d_soiTimer);
- smtStatisticsRegistry()->unregisterStat(&d_soiFocusConstructionTimer);
-
- smtStatisticsRegistry()->unregisterStat(&d_soiConflictMinimization);
-
- smtStatisticsRegistry()->unregisterStat(&d_selectUpdateForSOI);
- smtStatisticsRegistry()->unregisterStat(&d_finalCheckPivotCounter);
}
Result::Sat SumOfInfeasibilitiesSPD::findModel(bool exactResult){
#include "theory/arith/simplex.h"
#include "theory/arith/simplex_update.h"
#include "util/dense_map.h"
-#include "util/statistics_registry.h"
+#include "util/statistics_stats.h"
namespace cvc5 {
namespace theory {
ReferenceStat<uint32_t> d_finalCheckPivotCounter;
- Statistics(uint32_t& pivots);
- ~Statistics();
+ Statistics(const std::string& name, uint32_t& pivots);
} d_statistics;
};/* class FCSimplexDecisionProcedure */
: Theory(THEORY_ARITH, c, u, out, valuation, logicInfo, pnm),
d_internal(
new TheoryArithPrivate(*this, c, u, out, valuation, logicInfo, pnm)),
- d_ppRewriteTimer("theory::arith::ppRewriteTimer"),
+ d_ppRewriteTimer(smtStatisticsRegistry().registerTimer(
+ "theory::arith::ppRewriteTimer")),
d_ppPfGen(pnm, c, "Arith::ppRewrite"),
d_astate(*d_internal, c, u, valuation),
d_im(*this, d_astate, pnm),
d_nonlinearExtension(nullptr),
d_arithPreproc(d_astate, d_im, pnm, logicInfo)
{
- smtStatisticsRegistry()->registerStat(&d_ppRewriteTimer);
-
// indicate we are using the theory state object and inference manager
d_theoryState = &d_astate;
d_inferManager = &d_im;
}
TheoryArith::~TheoryArith(){
- smtStatisticsRegistry()->unregisterStat(&d_ppRewriteTimer);
delete d_internal;
}
#include "util/random.h"
#include "util/rational.h"
#include "util/result.h"
-#include "util/statistics_registry.h"
+#include "util/statistics_stats.h"
using namespace std;
using namespace cvc5::kind;
d_solveIntAttempts(0u),
d_newFacts(false),
d_previousStatus(Result::SAT_UNKNOWN),
- d_statistics()
+ d_statistics("theory::arith::")
{
}
}
TheoryArithPrivate::ModelException::~ModelException() {}
-TheoryArithPrivate::Statistics::Statistics()
- : d_statAssertUpperConflicts("theory::arith::AssertUpperConflicts", 0)
- , d_statAssertLowerConflicts("theory::arith::AssertLowerConflicts", 0)
- , d_statUserVariables("theory::arith::UserVariables", 0)
- , d_statAuxiliaryVariables("theory::arith::AuxiliaryVariables", 0)
- , d_statDisequalitySplits("theory::arith::DisequalitySplits", 0)
- , d_statDisequalityConflicts("theory::arith::DisequalityConflicts", 0)
- , d_simplifyTimer("theory::arith::simplifyTimer")
- , d_staticLearningTimer("theory::arith::staticLearningTimer")
- , d_presolveTime("theory::arith::presolveTime")
- , d_newPropTime("theory::arith::newPropTimer")
- , d_externalBranchAndBounds("theory::arith::externalBranchAndBounds",0)
- , d_initialTableauSize("theory::arith::initialTableauSize", 0)
- , d_currSetToSmaller("theory::arith::currSetToSmaller", 0)
- , d_smallerSetToCurr("theory::arith::smallerSetToCurr", 0)
- , d_restartTimer("theory::arith::restartTimer")
- , d_boundComputationTime("theory::arith::bound::time")
- , d_boundComputations("theory::arith::bound::boundComputations",0)
- , d_boundPropagations("theory::arith::bound::boundPropagations",0)
- , d_unknownChecks("theory::arith::status::unknowns", 0)
- , d_maxUnknownsInARow("theory::arith::status::maxUnknownsInARow", 0)
- , d_avgUnknownsInARow("theory::arith::status::avgUnknownsInARow")
- , d_revertsOnConflicts("theory::arith::status::revertsOnConflicts",0)
- , d_commitsOnConflicts("theory::arith::status::commitsOnConflicts",0)
- , d_nontrivialSatChecks("theory::arith::status::nontrivialSatChecks",0)
- , d_replayLogRecCount("theory::arith::z::approx::replay::rec",0)
- , d_replayLogRecConflictEscalation("theory::arith::z::approx::replay::rec::escalation",0)
- , d_replayLogRecEarlyExit("theory::arith::z::approx::replay::rec::earlyexit",0)
- , d_replayBranchCloseFailures("theory::arith::z::approx::replay::rec::branch::closefailures",0)
- , d_replayLeafCloseFailures("theory::arith::z::approx::replay::rec::leaf::closefailures",0)
- , d_replayBranchSkips("theory::arith::z::approx::replay::rec::branch::skips",0)
- , d_mirCutsAttempted("theory::arith::z::approx::cuts::mir::attempted",0)
- , d_gmiCutsAttempted("theory::arith::z::approx::cuts::gmi::attempted",0)
- , d_branchCutsAttempted("theory::arith::z::approx::cuts::branch::attempted",0)
- , d_cutsReconstructed("theory::arith::z::approx::cuts::reconstructed",0)
- , d_cutsReconstructionFailed("theory::arith::z::approx::cuts::reconstructed::failed",0)
- , d_cutsProven("theory::arith::z::approx::cuts::proofs",0)
- , d_cutsProofFailed("theory::arith::z::approx::cuts::proofs::failed",0)
- , d_mipReplayLemmaCalls("theory::arith::z::approx::external::calls",0)
- , d_mipExternalCuts("theory::arith::z::approx::external::cuts",0)
- , d_mipExternalBranch("theory::arith::z::approx::external::branches",0)
- , d_inSolveInteger("theory::arith::z::approx::inSolverInteger",0)
- , d_branchesExhausted("theory::arith::z::approx::exhausted::branches",0)
- , d_execExhausted("theory::arith::z::approx::exhausted::exec",0)
- , d_pivotsExhausted("theory::arith::z::approx::exhausted::pivots",0)
- , d_panicBranches("theory::arith::z::arith::paniclemmas",0)
- , d_relaxCalls("theory::arith::z::arith::relax::calls",0)
- , d_relaxLinFeas("theory::arith::z::arith::relax::feasible::res",0)
- , d_relaxLinFeasFailures("theory::arith::z::arith::relax::feasible::failures",0)
- , d_relaxLinInfeas("theory::arith::z::arith::relax::infeasible",0)
- , d_relaxLinInfeasFailures("theory::arith::z::arith::relax::infeasible::failures",0)
- , d_relaxLinExhausted("theory::arith::z::arith::relax::exhausted",0)
- , d_relaxOthers("theory::arith::z::arith::relax::other",0)
- , d_applyRowsDeleted("theory::arith::z::arith::cuts::applyRowsDeleted",0)
- , d_replaySimplexTimer("theory::arith::z::approx::replay::simplex::timer")
- , d_replayLogTimer("theory::arith::z::approx::replay::log::timer")
- , d_solveIntTimer("theory::arith::z::solveInt::timer")
- , d_solveRealRelaxTimer("theory::arith::z::solveRealRelax::timer")
- , d_solveIntCalls("theory::arith::z::solveInt::calls", 0)
- , d_solveStandardEffort("theory::arith::z::solveInt::calls::standardEffort", 0)
- , d_approxDisabled("theory::arith::z::approxDisabled", 0)
- , d_replayAttemptFailed("theory::arith::z::replayAttemptFailed",0)
- , d_cutsRejectedDuringReplay("theory::arith::z::approx::replay::cuts::rejected", 0)
- , d_cutsRejectedDuringLemmas("theory::arith::z::approx::external::cuts::rejected", 0)
- , d_satPivots("theory::arith::pivots::sat")
- , d_unsatPivots("theory::arith::pivots::unsat")
- , d_unknownPivots("theory::arith::pivots::unknown")
- , d_solveIntModelsAttempts("theory::arith::z::solveInt::models::attempts", 0)
- , d_solveIntModelsSuccessful("theory::arith::zzz::solveInt::models::successful", 0)
- , d_mipTimer("theory::arith::z::approx::mip::timer")
- , d_lpTimer("theory::arith::z::approx::lp::timer")
- , d_mipProofsAttempted("theory::arith::z::mip::proofs::attempted", 0)
- , d_mipProofsSuccessful("theory::arith::z::mip::proofs::successful", 0)
- , d_numBranchesFailed("theory::arith::z::mip::branch::proof::failed", 0)
+TheoryArithPrivate::Statistics::Statistics(const std::string& name)
+ : d_statAssertUpperConflicts(
+ smtStatisticsRegistry().registerInt(name + "AssertUpperConflicts")),
+ d_statAssertLowerConflicts(
+ smtStatisticsRegistry().registerInt(name + "AssertLowerConflicts")),
+ d_statUserVariables(
+ smtStatisticsRegistry().registerInt(name + "UserVariables")),
+ d_statAuxiliaryVariables(
+ smtStatisticsRegistry().registerInt(name + "AuxiliaryVariables")),
+ d_statDisequalitySplits(
+ smtStatisticsRegistry().registerInt(name + "DisequalitySplits")),
+ d_statDisequalityConflicts(
+ smtStatisticsRegistry().registerInt(name + "DisequalityConflicts")),
+ d_simplifyTimer(
+ smtStatisticsRegistry().registerTimer(name + "simplifyTimer")),
+ d_staticLearningTimer(
+ smtStatisticsRegistry().registerTimer(name + "staticLearningTimer")),
+ d_presolveTime(
+ smtStatisticsRegistry().registerTimer(name + "presolveTime")),
+ d_newPropTime(
+ smtStatisticsRegistry().registerTimer(name + "newPropTimer")),
+ d_externalBranchAndBounds(smtStatisticsRegistry().registerInt(
+ name + "externalBranchAndBounds")),
+ d_initialTableauSize(
+ smtStatisticsRegistry().registerInt(name + "initialTableauSize")),
+ d_currSetToSmaller(
+ smtStatisticsRegistry().registerInt(name + "currSetToSmaller")),
+ d_smallerSetToCurr(
+ smtStatisticsRegistry().registerInt(name + "smallerSetToCurr")),
+ d_restartTimer(
+ smtStatisticsRegistry().registerTimer(name + "restartTimer")),
+ d_boundComputationTime(
+ smtStatisticsRegistry().registerTimer(name + "bound::time")),
+ d_boundComputations(smtStatisticsRegistry().registerInt(
+ name + "bound::boundComputations")),
+ d_boundPropagations(smtStatisticsRegistry().registerInt(
+ name + "bound::boundPropagations")),
+ d_unknownChecks(
+ smtStatisticsRegistry().registerInt(name + "status::unknowns")),
+ d_maxUnknownsInARow(smtStatisticsRegistry().registerInt(
+ name + "status::maxUnknownsInARow")),
+ d_avgUnknownsInARow(smtStatisticsRegistry().registerAverage(
+ name + "status::avgUnknownsInARow")),
+ d_revertsOnConflicts(smtStatisticsRegistry().registerInt(
+ name + "status::revertsOnConflicts")),
+ d_commitsOnConflicts(smtStatisticsRegistry().registerInt(
+ name + "status::commitsOnConflicts")),
+ d_nontrivialSatChecks(smtStatisticsRegistry().registerInt(
+ name + "status::nontrivialSatChecks")),
+ d_replayLogRecCount(
+ smtStatisticsRegistry().registerInt(name + "z::approx::replay::rec")),
+ d_replayLogRecConflictEscalation(smtStatisticsRegistry().registerInt(
+ name + "z::approx::replay::rec::escalation")),
+ d_replayLogRecEarlyExit(smtStatisticsRegistry().registerInt(
+ name + "z::approx::replay::rec::earlyexit")),
+ d_replayBranchCloseFailures(smtStatisticsRegistry().registerInt(
+ name + "z::approx::replay::rec::branch::closefailures")),
+ d_replayLeafCloseFailures(smtStatisticsRegistry().registerInt(
+ name + "z::approx::replay::rec::leaf::closefailures")),
+ d_replayBranchSkips(smtStatisticsRegistry().registerInt(
+ name + "z::approx::replay::rec::branch::skips")),
+ d_mirCutsAttempted(smtStatisticsRegistry().registerInt(
+ name + "z::approx::cuts::mir::attempted")),
+ d_gmiCutsAttempted(smtStatisticsRegistry().registerInt(
+ name + "z::approx::cuts::gmi::attempted")),
+ d_branchCutsAttempted(smtStatisticsRegistry().registerInt(
+ name + "z::approx::cuts::branch::attempted")),
+ d_cutsReconstructed(smtStatisticsRegistry().registerInt(
+ name + "z::approx::cuts::reconstructed")),
+ d_cutsReconstructionFailed(smtStatisticsRegistry().registerInt(
+ name + "z::approx::cuts::reconstructed::failed")),
+ d_cutsProven(smtStatisticsRegistry().registerInt(
+ name + "z::approx::cuts::proofs")),
+ d_cutsProofFailed(smtStatisticsRegistry().registerInt(
+ name + "z::approx::cuts::proofs::failed")),
+ d_mipReplayLemmaCalls(smtStatisticsRegistry().registerInt(
+ name + "z::approx::external::calls")),
+ d_mipExternalCuts(smtStatisticsRegistry().registerInt(
+ name + "z::approx::external::cuts")),
+ d_mipExternalBranch(smtStatisticsRegistry().registerInt(
+ name + "z::approx::external::branches")),
+ d_inSolveInteger(smtStatisticsRegistry().registerInt(
+ name + "z::approx::inSolverInteger")),
+ d_branchesExhausted(smtStatisticsRegistry().registerInt(
+ name + "z::approx::exhausted::branches")),
+ d_execExhausted(smtStatisticsRegistry().registerInt(
+ name + "z::approx::exhausted::exec")),
+ d_pivotsExhausted(smtStatisticsRegistry().registerInt(
+ name + "z::approx::exhausted::pivots")),
+ d_panicBranches(
+ smtStatisticsRegistry().registerInt(name + "z::arith::paniclemmas")),
+ d_relaxCalls(
+ smtStatisticsRegistry().registerInt(name + "z::arith::relax::calls")),
+ d_relaxLinFeas(smtStatisticsRegistry().registerInt(
+ name + "z::arith::relax::feasible::res")),
+ d_relaxLinFeasFailures(smtStatisticsRegistry().registerInt(
+ name + "z::arith::relax::feasible::failures")),
+ d_relaxLinInfeas(smtStatisticsRegistry().registerInt(
+ name + "z::arith::relax::infeasible")),
+ d_relaxLinInfeasFailures(smtStatisticsRegistry().registerInt(
+ name + "z::arith::relax::infeasible::failures")),
+ d_relaxLinExhausted(smtStatisticsRegistry().registerInt(
+ name + "z::arith::relax::exhausted")),
+ d_relaxOthers(
+ smtStatisticsRegistry().registerInt(name + "z::arith::relax::other")),
+ d_applyRowsDeleted(smtStatisticsRegistry().registerInt(
+ name + "z::arith::cuts::applyRowsDeleted")),
+ d_replaySimplexTimer(smtStatisticsRegistry().registerTimer(
+ name + "z::approx::replay::simplex::timer")),
+ d_replayLogTimer(smtStatisticsRegistry().registerTimer(
+ name + "z::approx::replay::log::timer")),
+ d_solveIntTimer(
+ smtStatisticsRegistry().registerTimer(name + "z::solveInt::timer")),
+ d_solveRealRelaxTimer(smtStatisticsRegistry().registerTimer(
+ name + "z::solveRealRelax::timer")),
+ d_solveIntCalls(
+ smtStatisticsRegistry().registerInt(name + "z::solveInt::calls")),
+ d_solveStandardEffort(smtStatisticsRegistry().registerInt(
+ name + "z::solveInt::calls::standardEffort")),
+ d_approxDisabled(
+ smtStatisticsRegistry().registerInt(name + "z::approxDisabled")),
+ d_replayAttemptFailed(
+ smtStatisticsRegistry().registerInt(name + "z::replayAttemptFailed")),
+ d_cutsRejectedDuringReplay(smtStatisticsRegistry().registerInt(
+ name + "z::approx::replay::cuts::rejected")),
+ d_cutsRejectedDuringLemmas(smtStatisticsRegistry().registerInt(
+ name + "z::approx::external::cuts::rejected")),
+ d_satPivots(smtStatisticsRegistry().registerHistogram<uint32_t>(
+ name + "pivots::sat")),
+ d_unsatPivots(smtStatisticsRegistry().registerHistogram<uint32_t>(
+ name + "pivots::unsat")),
+ d_unknownPivots(smtStatisticsRegistry().registerHistogram<uint32_t>(
+ name + "pivots::unknown")),
+ d_solveIntModelsAttempts(smtStatisticsRegistry().registerInt(
+ name + "z::solveInt::models::attempts")),
+ d_solveIntModelsSuccessful(smtStatisticsRegistry().registerInt(
+ name + "zzz::solveInt::models::successful")),
+ d_mipTimer(smtStatisticsRegistry().registerTimer(
+ name + "z::approx::mip::timer")),
+ d_lpTimer(
+ smtStatisticsRegistry().registerTimer(name + "z::approx::lp::timer")),
+ d_mipProofsAttempted(smtStatisticsRegistry().registerInt(
+ name + "z::mip::proofs::attempted")),
+ d_mipProofsSuccessful(smtStatisticsRegistry().registerInt(
+ name + "z::mip::proofs::successful")),
+ d_numBranchesFailed(smtStatisticsRegistry().registerInt(
+ name + "z::mip::branch::proof::failed"))
{
- smtStatisticsRegistry()->registerStat(&d_statAssertUpperConflicts);
- smtStatisticsRegistry()->registerStat(&d_statAssertLowerConflicts);
-
- smtStatisticsRegistry()->registerStat(&d_statUserVariables);
- smtStatisticsRegistry()->registerStat(&d_statAuxiliaryVariables);
- smtStatisticsRegistry()->registerStat(&d_statDisequalitySplits);
- smtStatisticsRegistry()->registerStat(&d_statDisequalityConflicts);
- smtStatisticsRegistry()->registerStat(&d_simplifyTimer);
- smtStatisticsRegistry()->registerStat(&d_staticLearningTimer);
-
- smtStatisticsRegistry()->registerStat(&d_presolveTime);
- smtStatisticsRegistry()->registerStat(&d_newPropTime);
-
- smtStatisticsRegistry()->registerStat(&d_externalBranchAndBounds);
-
- smtStatisticsRegistry()->registerStat(&d_initialTableauSize);
- smtStatisticsRegistry()->registerStat(&d_currSetToSmaller);
- smtStatisticsRegistry()->registerStat(&d_smallerSetToCurr);
- smtStatisticsRegistry()->registerStat(&d_restartTimer);
-
- smtStatisticsRegistry()->registerStat(&d_boundComputationTime);
- smtStatisticsRegistry()->registerStat(&d_boundComputations);
- smtStatisticsRegistry()->registerStat(&d_boundPropagations);
-
- smtStatisticsRegistry()->registerStat(&d_unknownChecks);
- smtStatisticsRegistry()->registerStat(&d_maxUnknownsInARow);
- smtStatisticsRegistry()->registerStat(&d_avgUnknownsInARow);
- smtStatisticsRegistry()->registerStat(&d_revertsOnConflicts);
- smtStatisticsRegistry()->registerStat(&d_commitsOnConflicts);
- smtStatisticsRegistry()->registerStat(&d_nontrivialSatChecks);
-
-
- smtStatisticsRegistry()->registerStat(&d_satPivots);
- smtStatisticsRegistry()->registerStat(&d_unsatPivots);
- smtStatisticsRegistry()->registerStat(&d_unknownPivots);
-
- smtStatisticsRegistry()->registerStat(&d_replayLogRecCount);
- smtStatisticsRegistry()->registerStat(&d_replayLogRecConflictEscalation);
- smtStatisticsRegistry()->registerStat(&d_replayLogRecEarlyExit);
- smtStatisticsRegistry()->registerStat(&d_replayBranchCloseFailures);
- smtStatisticsRegistry()->registerStat(&d_replayLeafCloseFailures);
- smtStatisticsRegistry()->registerStat(&d_replayBranchSkips);
- smtStatisticsRegistry()->registerStat(&d_mirCutsAttempted);
- smtStatisticsRegistry()->registerStat(&d_gmiCutsAttempted);
- smtStatisticsRegistry()->registerStat(&d_branchCutsAttempted);
- smtStatisticsRegistry()->registerStat(&d_cutsReconstructed);
- smtStatisticsRegistry()->registerStat(&d_cutsProven);
- smtStatisticsRegistry()->registerStat(&d_cutsProofFailed);
- smtStatisticsRegistry()->registerStat(&d_cutsReconstructionFailed);
- smtStatisticsRegistry()->registerStat(&d_mipReplayLemmaCalls);
- smtStatisticsRegistry()->registerStat(&d_mipExternalCuts);
- smtStatisticsRegistry()->registerStat(&d_mipExternalBranch);
-
- smtStatisticsRegistry()->registerStat(&d_inSolveInteger);
- smtStatisticsRegistry()->registerStat(&d_branchesExhausted);
- smtStatisticsRegistry()->registerStat(&d_execExhausted);
- smtStatisticsRegistry()->registerStat(&d_pivotsExhausted);
- smtStatisticsRegistry()->registerStat(&d_panicBranches);
- smtStatisticsRegistry()->registerStat(&d_relaxCalls);
- smtStatisticsRegistry()->registerStat(&d_relaxLinFeas);
- smtStatisticsRegistry()->registerStat(&d_relaxLinFeasFailures);
- smtStatisticsRegistry()->registerStat(&d_relaxLinInfeas);
- smtStatisticsRegistry()->registerStat(&d_relaxLinInfeasFailures);
- smtStatisticsRegistry()->registerStat(&d_relaxLinExhausted);
- smtStatisticsRegistry()->registerStat(&d_relaxOthers);
-
- smtStatisticsRegistry()->registerStat(&d_applyRowsDeleted);
-
- smtStatisticsRegistry()->registerStat(&d_replaySimplexTimer);
- smtStatisticsRegistry()->registerStat(&d_replayLogTimer);
- smtStatisticsRegistry()->registerStat(&d_solveIntTimer);
- smtStatisticsRegistry()->registerStat(&d_solveRealRelaxTimer);
-
- smtStatisticsRegistry()->registerStat(&d_solveIntCalls);
- smtStatisticsRegistry()->registerStat(&d_solveStandardEffort);
-
- smtStatisticsRegistry()->registerStat(&d_approxDisabled);
-
- smtStatisticsRegistry()->registerStat(&d_replayAttemptFailed);
-
- smtStatisticsRegistry()->registerStat(&d_cutsRejectedDuringReplay);
- smtStatisticsRegistry()->registerStat(&d_cutsRejectedDuringLemmas);
-
- smtStatisticsRegistry()->registerStat(&d_solveIntModelsAttempts);
- smtStatisticsRegistry()->registerStat(&d_solveIntModelsSuccessful);
- smtStatisticsRegistry()->registerStat(&d_mipTimer);
- smtStatisticsRegistry()->registerStat(&d_lpTimer);
- smtStatisticsRegistry()->registerStat(&d_mipProofsAttempted);
- smtStatisticsRegistry()->registerStat(&d_mipProofsSuccessful);
- smtStatisticsRegistry()->registerStat(&d_numBranchesFailed);
-}
-
-TheoryArithPrivate::Statistics::~Statistics(){
- smtStatisticsRegistry()->unregisterStat(&d_statAssertUpperConflicts);
- smtStatisticsRegistry()->unregisterStat(&d_statAssertLowerConflicts);
-
- smtStatisticsRegistry()->unregisterStat(&d_statUserVariables);
- smtStatisticsRegistry()->unregisterStat(&d_statAuxiliaryVariables);
- smtStatisticsRegistry()->unregisterStat(&d_statDisequalitySplits);
- smtStatisticsRegistry()->unregisterStat(&d_statDisequalityConflicts);
- smtStatisticsRegistry()->unregisterStat(&d_simplifyTimer);
- smtStatisticsRegistry()->unregisterStat(&d_staticLearningTimer);
-
- smtStatisticsRegistry()->unregisterStat(&d_presolveTime);
- smtStatisticsRegistry()->unregisterStat(&d_newPropTime);
-
- smtStatisticsRegistry()->unregisterStat(&d_externalBranchAndBounds);
-
- smtStatisticsRegistry()->unregisterStat(&d_initialTableauSize);
- smtStatisticsRegistry()->unregisterStat(&d_currSetToSmaller);
- smtStatisticsRegistry()->unregisterStat(&d_smallerSetToCurr);
- smtStatisticsRegistry()->unregisterStat(&d_restartTimer);
-
- smtStatisticsRegistry()->unregisterStat(&d_boundComputationTime);
- smtStatisticsRegistry()->unregisterStat(&d_boundComputations);
- smtStatisticsRegistry()->unregisterStat(&d_boundPropagations);
-
- smtStatisticsRegistry()->unregisterStat(&d_unknownChecks);
- smtStatisticsRegistry()->unregisterStat(&d_maxUnknownsInARow);
- smtStatisticsRegistry()->unregisterStat(&d_avgUnknownsInARow);
- smtStatisticsRegistry()->unregisterStat(&d_revertsOnConflicts);
- smtStatisticsRegistry()->unregisterStat(&d_commitsOnConflicts);
- smtStatisticsRegistry()->unregisterStat(&d_nontrivialSatChecks);
-
- smtStatisticsRegistry()->unregisterStat(&d_satPivots);
- smtStatisticsRegistry()->unregisterStat(&d_unsatPivots);
- smtStatisticsRegistry()->unregisterStat(&d_unknownPivots);
-
- smtStatisticsRegistry()->unregisterStat(&d_replayLogRecCount);
- smtStatisticsRegistry()->unregisterStat(&d_replayLogRecConflictEscalation);
- smtStatisticsRegistry()->unregisterStat(&d_replayLogRecEarlyExit);
- smtStatisticsRegistry()->unregisterStat(&d_replayBranchCloseFailures);
- smtStatisticsRegistry()->unregisterStat(&d_replayLeafCloseFailures);
- smtStatisticsRegistry()->unregisterStat(&d_replayBranchSkips);
- smtStatisticsRegistry()->unregisterStat(&d_mirCutsAttempted);
- smtStatisticsRegistry()->unregisterStat(&d_gmiCutsAttempted);
- smtStatisticsRegistry()->unregisterStat(&d_branchCutsAttempted);
- smtStatisticsRegistry()->unregisterStat(&d_cutsReconstructed);
- smtStatisticsRegistry()->unregisterStat(&d_cutsProven);
- smtStatisticsRegistry()->unregisterStat(&d_cutsProofFailed);
- smtStatisticsRegistry()->unregisterStat(&d_cutsReconstructionFailed);
- smtStatisticsRegistry()->unregisterStat(&d_mipReplayLemmaCalls);
- smtStatisticsRegistry()->unregisterStat(&d_mipExternalCuts);
- smtStatisticsRegistry()->unregisterStat(&d_mipExternalBranch);
-
-
- smtStatisticsRegistry()->unregisterStat(&d_inSolveInteger);
- smtStatisticsRegistry()->unregisterStat(&d_branchesExhausted);
- smtStatisticsRegistry()->unregisterStat(&d_execExhausted);
- smtStatisticsRegistry()->unregisterStat(&d_pivotsExhausted);
- smtStatisticsRegistry()->unregisterStat(&d_panicBranches);
- smtStatisticsRegistry()->unregisterStat(&d_relaxCalls);
- smtStatisticsRegistry()->unregisterStat(&d_relaxLinFeas);
- smtStatisticsRegistry()->unregisterStat(&d_relaxLinFeasFailures);
- smtStatisticsRegistry()->unregisterStat(&d_relaxLinInfeas);
- smtStatisticsRegistry()->unregisterStat(&d_relaxLinInfeasFailures);
- smtStatisticsRegistry()->unregisterStat(&d_relaxLinExhausted);
- smtStatisticsRegistry()->unregisterStat(&d_relaxOthers);
-
- smtStatisticsRegistry()->unregisterStat(&d_applyRowsDeleted);
-
- smtStatisticsRegistry()->unregisterStat(&d_replaySimplexTimer);
- smtStatisticsRegistry()->unregisterStat(&d_replayLogTimer);
- smtStatisticsRegistry()->unregisterStat(&d_solveIntTimer);
- smtStatisticsRegistry()->unregisterStat(&d_solveRealRelaxTimer);
-
- smtStatisticsRegistry()->unregisterStat(&d_solveIntCalls);
- smtStatisticsRegistry()->unregisterStat(&d_solveStandardEffort);
-
- smtStatisticsRegistry()->unregisterStat(&d_approxDisabled);
-
- smtStatisticsRegistry()->unregisterStat(&d_replayAttemptFailed);
-
- smtStatisticsRegistry()->unregisterStat(&d_cutsRejectedDuringReplay);
- smtStatisticsRegistry()->unregisterStat(&d_cutsRejectedDuringLemmas);
-
-
- smtStatisticsRegistry()->unregisterStat(&d_solveIntModelsAttempts);
- smtStatisticsRegistry()->unregisterStat(&d_solveIntModelsSuccessful);
- smtStatisticsRegistry()->unregisterStat(&d_mipTimer);
- smtStatisticsRegistry()->unregisterStat(&d_lpTimer);
- smtStatisticsRegistry()->unregisterStat(&d_mipProofsAttempted);
- smtStatisticsRegistry()->unregisterStat(&d_mipProofsSuccessful);
- smtStatisticsRegistry()->unregisterStat(&d_numBranchesFailed);
}
bool complexityBelow(const DenseMap<Rational>& row, uint32_t cap){
std::vector<ConstraintCPVec> TheoryArithPrivate::replayLogRec(ApproximateSimplex* approx, int nid, ConstraintP bc, int depth){
++(d_statistics.d_replayLogRecCount);
- Debug("approx::replayLogRec") << "replayLogRec()"
- << d_statistics.d_replayLogRecCount.get() << std::endl;
+ Debug("approx::replayLogRec") << "replayLogRec()" << std::endl;
size_t rpvars_size = d_replayVariables.size();
size_t rpcons_size = d_replayConstraints.size();
TimerStat::CodeTimer codeTimer0(d_statistics.d_solveIntTimer);
++(d_statistics.d_solveIntCalls);
- d_statistics.d_inSolveInteger.set(1);
+ d_statistics.d_inSolveInteger = 1;
if(!Theory::fullEffort(effortLevel)){
d_solveIntAttempts++;
}
}
- d_statistics.d_inSolveInteger.set(0);
+ d_statistics.d_inSolveInteger = 0;
}
SimplexDecisionProcedure& TheoryArithPrivate::selectSimplex(bool pass1){
void TheoryArithPrivate::presolve(){
TimerStat::CodeTimer codeTimer(d_statistics.d_presolveTime);
- d_statistics.d_initialTableauSize.set(d_tableau.size());
+ d_statistics.d_initialTableauSize = d_tableau.size();
if(Debug.isOn("paranoid:check_tableau")){ d_linEq.debugCheckTableau(); }
#include "util/integer.h"
#include "util/rational.h"
#include "util/result.h"
-#include "util/statistics_registry.h"
+#include "util/statistics_stats.h"
namespace cvc5 {
namespace theory {
IntStat d_cutsRejectedDuringReplay;
IntStat d_cutsRejectedDuringLemmas;
- IntegralHistogramStat<uint32_t> d_satPivots;
- IntegralHistogramStat<uint32_t> d_unsatPivots;
- IntegralHistogramStat<uint32_t> d_unknownPivots;
-
+ HistogramStat<uint32_t> d_satPivots;
+ HistogramStat<uint32_t> d_unsatPivots;
+ HistogramStat<uint32_t> d_unknownPivots;
IntStat d_solveIntModelsAttempts;
IntStat d_solveIntModelsSuccessful;
IntStat d_numBranchesFailed;
-
-
- Statistics();
- ~Statistics();
+ Statistics(const std::string& name);
};
in_stores->deleteSelf();
}
-ArrayInfo::ArrayInfo(context::Context* c, Backtracker<TNode>* b, std::string statisticsPrefix)
- : ct(c), bck(b), info_map(),
- d_mergeInfoTimer(statisticsPrefix + "theory::arrays::mergeInfoTimer"),
- d_avgIndexListLength(statisticsPrefix + "theory::arrays::avgIndexListLength"),
- d_avgStoresListLength(statisticsPrefix + "theory::arrays::avgStoresListLength"),
- d_avgInStoresListLength(statisticsPrefix + "theory::arrays::avgInStoresListLength"),
- d_listsCount(statisticsPrefix + "theory::arrays::listsCount",0),
- d_callsMergeInfo(statisticsPrefix + "theory::arrays::callsMergeInfo",0),
- d_maxList(statisticsPrefix + "theory::arrays::maxList",0),
- d_tableSize(statisticsPrefix + "theory::arrays::infoTableSize", info_map) {
+ArrayInfo::ArrayInfo(context::Context* c,
+ Backtracker<TNode>* b,
+ std::string statisticsPrefix)
+ : ct(c),
+ bck(b),
+ info_map(),
+ d_mergeInfoTimer(smtStatisticsRegistry().registerTimer(
+ statisticsPrefix + "mergeInfoTimer")),
+ d_avgIndexListLength(smtStatisticsRegistry().registerAverage(
+ statisticsPrefix + "avgIndexListLength")),
+ d_avgStoresListLength(smtStatisticsRegistry().registerAverage(
+ statisticsPrefix + "avgStoresListLength")),
+ d_avgInStoresListLength(smtStatisticsRegistry().registerAverage(
+ statisticsPrefix + "avgInStoresListLength")),
+ d_listsCount(
+ smtStatisticsRegistry().registerInt(statisticsPrefix + "listsCount")),
+ d_callsMergeInfo(smtStatisticsRegistry().registerInt(statisticsPrefix
+ + "callsMergeInfo")),
+ d_maxList(
+ smtStatisticsRegistry().registerInt(statisticsPrefix + "maxList")),
+ d_tableSize(smtStatisticsRegistry().registerSize<CNodeInfoMap>(
+ statisticsPrefix + "infoTableSize", info_map))
+{
emptyList = new(true) CTNodeList(ct);
emptyInfo = new Info(ct, bck);
- smtStatisticsRegistry()->registerStat(&d_mergeInfoTimer);
- smtStatisticsRegistry()->registerStat(&d_avgIndexListLength);
- smtStatisticsRegistry()->registerStat(&d_avgStoresListLength);
- smtStatisticsRegistry()->registerStat(&d_avgInStoresListLength);
- smtStatisticsRegistry()->registerStat(&d_listsCount);
- smtStatisticsRegistry()->registerStat(&d_callsMergeInfo);
- smtStatisticsRegistry()->registerStat(&d_maxList);
- smtStatisticsRegistry()->registerStat(&d_tableSize);
}
ArrayInfo::~ArrayInfo() {
}
emptyList->deleteSelf();
delete emptyInfo;
- smtStatisticsRegistry()->unregisterStat(&d_mergeInfoTimer);
- smtStatisticsRegistry()->unregisterStat(&d_avgIndexListLength);
- smtStatisticsRegistry()->unregisterStat(&d_avgStoresListLength);
- smtStatisticsRegistry()->unregisterStat(&d_avgInStoresListLength);
- smtStatisticsRegistry()->unregisterStat(&d_listsCount);
- smtStatisticsRegistry()->unregisterStat(&d_callsMergeInfo);
- smtStatisticsRegistry()->unregisterStat(&d_maxList);
- smtStatisticsRegistry()->unregisterStat(&d_tableSize);
}
bool inList(const CTNodeList* l, const TNode el) {
#include "context/backtrackable.h"
#include "context/cdlist.h"
#include "expr/node.h"
-#include "util/statistics_registry.h"
-#include "util/stats_timer.h"
+#include "util/statistics_stats.h"
namespace cvc5 {
namespace theory {
IntStat d_listsCount;
IntStat d_callsMergeInfo;
IntStat d_maxList;
- SizeStat<CNodeInfoMap > d_tableSize;
+ SizeStat<CNodeInfoMap> d_tableSize;
/**
* checks if a certain element is in the list l
InferenceManager::InferenceManager(Theory& t,
TheoryState& state,
ProofNodeManager* pnm)
- : TheoryInferenceManager(t, state, pnm, "theory::arrays", false),
- d_lemmaPg(pnm ? new EagerProofGenerator(pnm,
- state.getUserContext(),
- "ArrayLemmaProofGenerator")
+ : TheoryInferenceManager(t, state, pnm, "theory::arrays::", false),
+ d_lemmaPg(pnm ? new EagerProofGenerator(
+ pnm, state.getUserContext(), "ArrayLemmaProofGenerator")
: nullptr)
{
}
ProofNodeManager* pnm,
std::string name)
: Theory(THEORY_ARRAYS, c, u, out, valuation, logicInfo, pnm, name),
- d_numRow(name + "theory::arrays::number of Row lemmas", 0),
- d_numExt(name + "theory::arrays::number of Ext lemmas", 0),
- d_numProp(name + "theory::arrays::number of propagations", 0),
- d_numExplain(name + "theory::arrays::number of explanations", 0),
- d_numNonLinear(name + "theory::arrays::number of calls to setNonLinear",
- 0),
- d_numSharedArrayVarSplits(
- name + "theory::arrays::number of shared array var splits", 0),
- d_numGetModelValSplits(
- name + "theory::arrays::number of getModelVal splits", 0),
- d_numGetModelValConflicts(
- name + "theory::arrays::number of getModelVal conflicts", 0),
- d_numSetModelValSplits(
- name + "theory::arrays::number of setModelVal splits", 0),
- d_numSetModelValConflicts(
- name + "theory::arrays::number of setModelVal conflicts", 0),
- d_ppEqualityEngine(u, name + "theory::arrays::pp", true),
+ d_numRow(
+ smtStatisticsRegistry().registerInt(name + "number of Row lemmas")),
+ d_numExt(
+ smtStatisticsRegistry().registerInt(name + "number of Ext lemmas")),
+ d_numProp(
+ smtStatisticsRegistry().registerInt(name + "number of propagations")),
+ d_numExplain(
+ smtStatisticsRegistry().registerInt(name + "number of explanations")),
+ d_numNonLinear(smtStatisticsRegistry().registerInt(
+ name + "number of calls to setNonLinear")),
+ d_numSharedArrayVarSplits(smtStatisticsRegistry().registerInt(
+ name + "number of shared array var splits")),
+ d_numGetModelValSplits(smtStatisticsRegistry().registerInt(
+ name + "number of getModelVal splits")),
+ d_numGetModelValConflicts(smtStatisticsRegistry().registerInt(
+ name + "number of getModelVal conflicts")),
+ d_numSetModelValSplits(smtStatisticsRegistry().registerInt(
+ name + "number of setModelVal splits")),
+ d_numSetModelValConflicts(smtStatisticsRegistry().registerInt(
+ name + "number of setModelVal conflicts")),
+ d_ppEqualityEngine(u, name + "pp", true),
d_ppFacts(u),
d_state(c, u, valuation),
d_im(*this, d_state, pnm),
d_literalsToPropagate(c),
d_literalsToPropagateIndex(c, 0),
d_isPreRegistered(c),
- d_mayEqualEqualityEngine(c, name + "theory::arrays::mayEqual", true),
+ d_mayEqualEqualityEngine(c, name + "mayEqual", true),
d_notify(*this),
d_backtracker(c),
d_infoMap(c, &d_backtracker, name),
d_dstrat(new TheoryArraysDecisionStrategy(this)),
d_dstratInit(false)
{
- smtStatisticsRegistry()->registerStat(&d_numRow);
- smtStatisticsRegistry()->registerStat(&d_numExt);
- smtStatisticsRegistry()->registerStat(&d_numProp);
- smtStatisticsRegistry()->registerStat(&d_numExplain);
- smtStatisticsRegistry()->registerStat(&d_numNonLinear);
- smtStatisticsRegistry()->registerStat(&d_numSharedArrayVarSplits);
- smtStatisticsRegistry()->registerStat(&d_numGetModelValSplits);
- smtStatisticsRegistry()->registerStat(&d_numGetModelValConflicts);
- smtStatisticsRegistry()->registerStat(&d_numSetModelValSplits);
- smtStatisticsRegistry()->registerStat(&d_numSetModelValConflicts);
-
d_true = NodeManager::currentNM()->mkConst<bool>(true);
d_false = NodeManager::currentNM()->mkConst<bool>(false);
it2->second->deleteSelf();
}
delete d_constReadsContext;
- smtStatisticsRegistry()->unregisterStat(&d_numRow);
- smtStatisticsRegistry()->unregisterStat(&d_numExt);
- smtStatisticsRegistry()->unregisterStat(&d_numProp);
- smtStatisticsRegistry()->unregisterStat(&d_numExplain);
- smtStatisticsRegistry()->unregisterStat(&d_numNonLinear);
- smtStatisticsRegistry()->unregisterStat(&d_numSharedArrayVarSplits);
- smtStatisticsRegistry()->unregisterStat(&d_numGetModelValSplits);
- smtStatisticsRegistry()->unregisterStat(&d_numGetModelValConflicts);
- smtStatisticsRegistry()->unregisterStat(&d_numSetModelValSplits);
- smtStatisticsRegistry()->unregisterStat(&d_numSetModelValConflicts);
}
TheoryRewriter* TheoryArrays::getTheoryRewriter() { return &d_rewriter; }
bool TheoryArrays::needsEqualityEngine(EeSetupInfo& esi)
{
esi.d_notify = &d_notify;
- esi.d_name = d_instanceName + "theory::arrays::ee";
+ esi.d_name = d_instanceName + "ee";
return true;
}
#include "theory/theory.h"
#include "theory/theory_state.h"
#include "theory/uf/equality_engine.h"
-#include "util/statistics_registry.h"
+#include "util/statistics_stats.h"
namespace cvc5 {
namespace theory {
Valuation valuation,
const LogicInfo& logicInfo,
ProofNodeManager* pnm = nullptr,
- std::string name = "");
+ std::string name = "theory::arrays::");
~TheoryArrays();
//--------------------------------- initialization
#include "theory/bags/bags_rewriter.h"
#include "theory/bags/normal_form.h"
+#include "util/statistics_registry.h"
using namespace cvc5::kind;
{
}
-BagsRewriter::BagsRewriter(IntegralHistogramStat<Rewrite>* statistics)
+BagsRewriter::BagsRewriter(HistogramStat<Rewrite>* statistics)
: d_statistics(statistics)
{
d_nm = NodeManager::currentNM();
#include "theory/bags/rewrites.h"
#include "theory/theory_rewriter.h"
-#include "util/statistics_registry.h"
-#include "util/stats_histogram.h"
+#include "util/statistics_stats.h"
namespace cvc5 {
namespace theory {
class BagsRewriter : public TheoryRewriter
{
public:
- BagsRewriter(IntegralHistogramStat<Rewrite>* statistics = nullptr);
+ BagsRewriter(HistogramStat<Rewrite>* statistics = nullptr);
/**
* postRewrite nodes with kinds: MK_BAG, BAG_COUNT, UNION_MAX, UNION_DISJOINT,
Node d_zero;
Node d_one;
/** Reference to the rewriter statistics. */
- IntegralHistogramStat<Rewrite>* d_statistics;
+ HistogramStat<Rewrite>* d_statistics;
}; /* class TheoryBagsRewriter */
} // namespace bags
namespace theory {
namespace bags {
-BagsStatistics::BagsStatistics() : d_rewrites("theory::bags::rewrites")
+BagsStatistics::BagsStatistics()
+ : d_rewrites(smtStatisticsRegistry().registerHistogram<Rewrite>(
+ "theory::bags::rewrites"))
{
- smtStatisticsRegistry()->registerStat(&d_rewrites);
-}
-
-BagsStatistics::~BagsStatistics()
-{
- smtStatisticsRegistry()->unregisterStat(&d_rewrites);
}
} // namespace bags
#define CVC5__THEORY__BAGS_STATISTICS_H
#include "theory/bags/rewrites.h"
-#include "util/statistics_registry.h"
-#include "util/stats_histogram.h"
+#include "util/statistics_stats.h"
namespace cvc5 {
namespace theory {
{
public:
BagsStatistics();
- ~BagsStatistics();
/** Counts the number of applications of each type of rewrite rule */
- IntegralHistogramStat<Rewrite> d_rewrites;
+ HistogramStat<Rewrite> d_rewrites;
};
} // namespace bags
InferenceManager::InferenceManager(Theory& t,
SolverState& s,
ProofNodeManager* pnm)
- : InferenceManagerBuffered(t, s, pnm, "theory::bags"), d_state(s)
+ : InferenceManagerBuffered(t, s, pnm, "theory::bags::"), d_state(s)
{
d_true = NodeManager::currentNM()->mkConst(true);
d_false = NodeManager::currentNM()->mkConst(false);
d_funcToSignature[abs_func] = signature;
}
- d_statistics.d_numFunctionsAbstracted.set(d_signatureToFunc.size());
-
Debug("bv-abstraction") << "AbstractionModule::finalizeSignatures abstracted "
<< d_signatureToFunc.size() << " signatures. \n";
}
return d_data.find(signature)->second;
}
-AbstractionModule::Statistics::Statistics(const std::string& name)
- : d_numFunctionsAbstracted(name + "::abstraction::NumFunctionsAbstracted",
- 0),
- d_numArgsSkolemized(name + "::abstraction::NumArgsSkolemized", 0),
- d_abstractionTime(name + "::abstraction::AbstractionTime")
+AbstractionModule::Statistics::Statistics(
+ const std::string& name, const NodeNodeMap& functionsAbstracted)
+ : d_numFunctionsAbstracted(
+ smtStatisticsRegistry().registerSize<NodeNodeMap>(
+ name + "NumFunctionsAbstracted", functionsAbstracted)),
+ d_numArgsSkolemized(
+ smtStatisticsRegistry().registerInt(name + "NumArgsSkolemized")),
+ d_abstractionTime(
+ smtStatisticsRegistry().registerTimer(name + "AbstractionTime"))
{
- smtStatisticsRegistry()->registerStat(&d_numFunctionsAbstracted);
- smtStatisticsRegistry()->registerStat(&d_numArgsSkolemized);
- smtStatisticsRegistry()->registerStat(&d_abstractionTime);
-}
-
-AbstractionModule::Statistics::~Statistics() {
- smtStatisticsRegistry()->unregisterStat(&d_numFunctionsAbstracted);
- smtStatisticsRegistry()->unregisterStat(&d_numArgsSkolemized);
- smtStatisticsRegistry()->unregisterStat(&d_abstractionTime);
}
#include "expr/node.h"
#include "theory/substitutions.h"
-#include "util/statistics_registry.h"
-#include "util/stats_timer.h"
+#include "util/statistics_stats.h"
namespace cvc5 {
namespace theory {
typedef std::vector<TNode> ArgsVec;
class AbstractionModule {
+ using NodeVecMap =
+ std::unordered_map<Node, std::vector<Node>, NodeHashFunction>;
+ using NodeTNodeMap = std::unordered_map<Node, TNode, NodeHashFunction>;
+ using TNodeTNodeMap = std::unordered_map<TNode, TNode, TNodeHashFunction>;
+ using NodeNodeMap = std::unordered_map<Node, Node, NodeHashFunction>;
+ using TNodeNodeMap = std::unordered_map<Node, TNode, NodeHashFunction>;
+ using TNodeSet = std::unordered_set<TNode, TNodeHashFunction>;
+ using IntNodeMap = std::unordered_map<unsigned, Node>;
+ using IndexMap = std::unordered_map<unsigned, unsigned>;
+ using SkolemMap = std::unordered_map<unsigned, std::vector<Node> >;
+ using SignatureMap = std::unordered_map<TNode, unsigned, TNodeHashFunction>;
struct Statistics {
- IntStat d_numFunctionsAbstracted;
+ SizeStat<NodeNodeMap> d_numFunctionsAbstracted;
IntStat d_numArgsSkolemized;
TimerStat d_abstractionTime;
- Statistics(const std::string& name);
- ~Statistics();
+ Statistics(const std::string& name, const NodeNodeMap& functionsAbstracted);
};
};
- typedef std::unordered_map<Node, std::vector<Node>, NodeHashFunction> NodeVecMap;
- typedef std::unordered_map<Node, TNode, NodeHashFunction> NodeTNodeMap;
- typedef std::unordered_map<TNode, TNode, TNodeHashFunction> TNodeTNodeMap;
- typedef std::unordered_map<Node, Node, NodeHashFunction> NodeNodeMap;
- typedef std::unordered_map<Node, TNode, NodeHashFunction> TNodeNodeMap;
- typedef std::unordered_set<TNode, TNodeHashFunction> TNodeSet;
- typedef std::unordered_map<unsigned, Node> IntNodeMap;
- typedef std::unordered_map<unsigned, unsigned> IndexMap;
- typedef std::unordered_map<unsigned, std::vector<Node> > SkolemMap;
- typedef std::unordered_map<TNode, unsigned, TNodeHashFunction > SignatureMap;
-
ArgsTable d_argsTable;
// mapping between signature and uninterpreted function symbol used to
Statistics d_statistics;
public:
- AbstractionModule(const std::string& name)
- : d_argsTable()
- , d_signatureToFunc()
- , d_funcToSignature()
- , d_assertionToSignature()
- , d_signatures()
- , d_sigToGeneralization()
- , d_skolems()
- , d_signatureIndices()
- , d_signatureSkolems()
- , d_addedLemmas()
- , d_lemmaAtoms()
- , d_inputAtoms()
- , d_statistics(name)
- {}
+ AbstractionModule(const std::string& name)
+ : d_argsTable(),
+ d_signatureToFunc(),
+ d_funcToSignature(),
+ d_assertionToSignature(),
+ d_signatures(),
+ d_sigToGeneralization(),
+ d_skolems(),
+ d_signatureIndices(),
+ d_signatureSkolems(),
+ d_addedLemmas(),
+ d_lemmaAtoms(),
+ d_inputAtoms(),
+ d_statistics(name + "abstraction::", d_signatureToFunc)
+ {
+ }
/**
* returns true if there are new uninterepreted functions symbols in the output
*
case options::SatSolverMode::MINISAT:
{
prop::BVSatSolverInterface* minisat =
- prop::SatSolverFactory::createMinisat(
- d_nullContext.get(), smtStatisticsRegistry(), "AigBitblaster");
+ prop::SatSolverFactory::createMinisat(d_nullContext.get(),
+ smtStatisticsRegistry(),
+ "theory::bv::AigBitblaster::");
d_notify.reset(new MinisatEmptyNotify());
minisat->setNotify(d_notify.get());
solver = minisat;
break;
}
case options::SatSolverMode::CADICAL:
- solver = prop::SatSolverFactory::createCadical(smtStatisticsRegistry(),
- "AigBitblaster");
+ solver = prop::SatSolverFactory::createCadical(
+ smtStatisticsRegistry(), "theory::bv::AigBitblaster::");
break;
case options::SatSolverMode::CRYPTOMINISAT:
solver = prop::SatSolverFactory::createCryptoMinisat(
- smtStatisticsRegistry(), "AigBitblaster");
+ smtStatisticsRegistry(), "theory::bv::AigBitblaster::");
break;
case options::SatSolverMode::KISSAT:
- solver = prop::SatSolverFactory::createKissat(smtStatisticsRegistry(),
- "AigBitblaster");
+ solver = prop::SatSolverFactory::createKissat(
+ smtStatisticsRegistry(), "theory::bv::AigBitblaster::");
break;
default: CVC5_FATAL() << "Unknown SAT solver type";
}
{
prop::BVSatSolverInterface* minisat =
prop::SatSolverFactory::createMinisat(
- d_nullContext.get(), smtStatisticsRegistry(), "EagerBitblaster");
+ d_nullContext.get(),
+ smtStatisticsRegistry(),
+ "theory::bv::EagerBitblaster::");
d_notify.reset(new MinisatEmptyNotify());
minisat->setNotify(d_notify.get());
solver = minisat;
break;
}
case options::SatSolverMode::CADICAL:
- solver = prop::SatSolverFactory::createCadical(smtStatisticsRegistry(),
- "EagerBitblaster");
+ solver = prop::SatSolverFactory::createCadical(
+ smtStatisticsRegistry(), "theory::bv::EagerBitblaster::");
break;
case options::SatSolverMode::CRYPTOMINISAT:
solver = prop::SatSolverFactory::createCryptoMinisat(
- smtStatisticsRegistry(), "EagerBitblaster");
+ smtStatisticsRegistry(), "theory::bv::EagerBitblaster::");
break;
case options::SatSolverMode::KISSAT:
- solver = prop::SatSolverFactory::createKissat(smtStatisticsRegistry(),
- "EagerBitblaster");
+ solver = prop::SatSolverFactory::createKissat(
+ smtStatisticsRegistry(), "theory::bv::EagerBitblaster::");
break;
default: Unreachable() << "Unknown SAT solver type";
}
d_emptyNotify(emptyNotify),
d_fullModelAssertionLevel(c, 0),
d_name(name),
- d_statistics(name)
+ d_statistics(name + "::")
{
- d_satSolver.reset(
- prop::SatSolverFactory::createMinisat(c, smtStatisticsRegistry(), name));
+ d_satSolver.reset(prop::SatSolverFactory::createMinisat(
+ c, smtStatisticsRegistry(), name + "::"));
ResourceManager* rm = smt::currentResourceManager();
d_cnfStream.reset(new prop::CnfStream(d_satSolver.get(),
}
}
-TLazyBitblaster::Statistics::Statistics(const std::string& prefix) :
- d_numTermClauses(prefix + "::NumTermSatClauses", 0),
- d_numAtomClauses(prefix + "::NumAtomSatClauses", 0),
- d_numTerms(prefix + "::NumBitblastedTerms", 0),
- d_numAtoms(prefix + "::NumBitblastedAtoms", 0),
- d_numExplainedPropagations(prefix + "::NumExplainedPropagations", 0),
- d_numBitblastingPropagations(prefix + "::NumBitblastingPropagations", 0),
- d_bitblastTimer(prefix + "::BitblastTimer")
+TLazyBitblaster::Statistics::Statistics(const std::string& prefix)
+ : d_numTermClauses(
+ smtStatisticsRegistry().registerInt(prefix + "NumTermSatClauses")),
+ d_numAtomClauses(
+ smtStatisticsRegistry().registerInt(prefix + "NumAtomSatClauses")),
+ d_numTerms(
+ smtStatisticsRegistry().registerInt(prefix + "NumBitblastedTerms")),
+ d_numAtoms(
+ smtStatisticsRegistry().registerInt(prefix + "NumBitblastedAtoms")),
+ d_numExplainedPropagations(smtStatisticsRegistry().registerInt(
+ prefix + "NumExplainedPropagations")),
+ d_numBitblastingPropagations(smtStatisticsRegistry().registerInt(
+ prefix + "NumBitblastingPropagations")),
+ d_bitblastTimer(
+ smtStatisticsRegistry().registerTimer(prefix + "BitblastTimer"))
{
- smtStatisticsRegistry()->registerStat(&d_numTermClauses);
- smtStatisticsRegistry()->registerStat(&d_numAtomClauses);
- smtStatisticsRegistry()->registerStat(&d_numTerms);
- smtStatisticsRegistry()->registerStat(&d_numAtoms);
- smtStatisticsRegistry()->registerStat(&d_numExplainedPropagations);
- smtStatisticsRegistry()->registerStat(&d_numBitblastingPropagations);
- smtStatisticsRegistry()->registerStat(&d_bitblastTimer);
-}
-
-
-TLazyBitblaster::Statistics::~Statistics() {
- smtStatisticsRegistry()->unregisterStat(&d_numTermClauses);
- smtStatisticsRegistry()->unregisterStat(&d_numAtomClauses);
- smtStatisticsRegistry()->unregisterStat(&d_numTerms);
- smtStatisticsRegistry()->unregisterStat(&d_numAtoms);
- smtStatisticsRegistry()->unregisterStat(&d_numExplainedPropagations);
- smtStatisticsRegistry()->unregisterStat(&d_numBitblastingPropagations);
- smtStatisticsRegistry()->unregisterStat(&d_bitblastTimer);
}
bool TLazyBitblaster::MinisatNotify::notify(prop::SatLiteral lit) {
IntStat d_numBitblastingPropagations;
TimerStat d_bitblastTimer;
Statistics(const std::string& name);
- ~Statistics();
};
std::string d_name;
}
QuickXPlain::Statistics::Statistics(const std::string& name)
- : d_xplainTime(name + "::QuickXplain::Time")
- , d_numSolved(name + "::QuickXplain::NumSolved", 0)
- , d_numUnknown(name + "::QuickXplain::NumUnknown", 0)
- , d_numUnknownWasUnsat(name + "::QuickXplain::NumUnknownWasUnsat", 0)
- , d_numConflictsMinimized(name + "::QuickXplain::NumConflictsMinimized", 0)
- , d_finalPeriod(name + "::QuickXplain::FinalPeriod", 0)
- , d_avgMinimizationRatio(name + "::QuickXplain::AvgMinRatio")
+ : d_xplainTime(
+ smtStatisticsRegistry().registerTimer(name + "QuickXplain::Time")),
+ d_numSolved(
+ smtStatisticsRegistry().registerInt(name + "QuickXplain::NumSolved")),
+ d_numUnknown(smtStatisticsRegistry().registerInt(
+ name + "QuickXplain::NumUnknown")),
+ d_numUnknownWasUnsat(smtStatisticsRegistry().registerInt(
+ name + "QuickXplain::NumUnknownWasUnsat")),
+ d_numConflictsMinimized(smtStatisticsRegistry().registerInt(
+ name + "QuickXplain::NumConflictsMinimized")),
+ d_finalPeriod(smtStatisticsRegistry().registerInt(
+ name + "QuickXplain::FinalPeriod")),
+ d_avgMinimizationRatio(smtStatisticsRegistry().registerAverage(
+ name + "QuickXplain::AvgMinRatio"))
{
- smtStatisticsRegistry()->registerStat(&d_xplainTime);
- smtStatisticsRegistry()->registerStat(&d_numSolved);
- smtStatisticsRegistry()->registerStat(&d_numUnknown);
- smtStatisticsRegistry()->registerStat(&d_numUnknownWasUnsat);
- smtStatisticsRegistry()->registerStat(&d_numConflictsMinimized);
- smtStatisticsRegistry()->registerStat(&d_finalPeriod);
- smtStatisticsRegistry()->registerStat(&d_avgMinimizationRatio);
-}
-
-QuickXPlain::Statistics::~Statistics() {
- smtStatisticsRegistry()->unregisterStat(&d_xplainTime);
- smtStatisticsRegistry()->unregisterStat(&d_numSolved);
- smtStatisticsRegistry()->unregisterStat(&d_numUnknown);
- smtStatisticsRegistry()->unregisterStat(&d_numUnknownWasUnsat);
- smtStatisticsRegistry()->unregisterStat(&d_numConflictsMinimized);
- smtStatisticsRegistry()->unregisterStat(&d_finalPeriod);
- smtStatisticsRegistry()->unregisterStat(&d_avgMinimizationRatio);
}
} // namespace bv
#include "expr/node.h"
#include "prop/sat_solver_types.h"
#include "theory/bv/theory_bv_utils.h"
-#include "util/statistics_registry.h"
-#include "util/stats_timer.h"
+#include "util/statistics_stats.h"
namespace cvc5 {
namespace theory {
IntStat d_finalPeriod;
AverageStat d_avgMinimizationRatio;
Statistics(const std::string& name);
- ~Statistics();
};
BVQuickCheck* d_solver;
unsigned long d_budget;
{
case options::SatSolverMode::CRYPTOMINISAT:
d_satSolver.reset(prop::SatSolverFactory::createCryptoMinisat(
- smtStatisticsRegistry(), "BVSolverBitblast"));
+ smtStatisticsRegistry(), "theory::bv::BVSolverBitblast"));
break;
default:
d_satSolver.reset(prop::SatSolverFactory::createCadical(
- smtStatisticsRegistry(), "BVSolverBitblast"));
+ smtStatisticsRegistry(), "theory::bv::BVSolverBitblast"));
}
d_cnfStream.reset(new prop::CnfStream(d_satSolver.get(),
d_nullRegistrar.get(),
}
BVSolverLazy::Statistics::Statistics()
- : d_avgConflictSize("theory::bv::lazy::AvgBVConflictSize"),
- d_solveSubstitutions("theory::bv::lazy::NumSolveSubstitutions", 0),
- d_solveTimer("theory::bv::lazy::solveTimer"),
- d_numCallsToCheckFullEffort("theory::bv::lazy::NumFullCheckCalls", 0),
- d_numCallsToCheckStandardEffort("theory::bv::lazy::NumStandardCheckCalls",
- 0),
- d_weightComputationTimer("theory::bv::lazy::weightComputationTimer"),
- d_numMultSlice("theory::bv::lazy::NumMultSliceApplied", 0)
+ : d_avgConflictSize(smtStatisticsRegistry().registerAverage(
+ "theory::bv::lazy::AvgBVConflictSize")),
+ d_solveSubstitutions(smtStatisticsRegistry().registerInt(
+ "theory::bv::lazy::NumSolveSubstitutions")),
+ d_solveTimer(smtStatisticsRegistry().registerTimer(
+ "theory::bv::lazy::solveTimer")),
+ d_numCallsToCheckFullEffort(smtStatisticsRegistry().registerInt(
+ "theory::bv::lazy::NumFullCheckCalls")),
+ d_numCallsToCheckStandardEffort(smtStatisticsRegistry().registerInt(
+ "theory::bv::lazy::NumStandardCheckCalls")),
+ d_weightComputationTimer(smtStatisticsRegistry().registerTimer(
+ "theory::bv::lazy::weightComputationTimer")),
+ d_numMultSlice(smtStatisticsRegistry().registerInt(
+ "theory::bv::lazy::NumMultSliceApplied"))
{
- smtStatisticsRegistry()->registerStat(&d_avgConflictSize);
- smtStatisticsRegistry()->registerStat(&d_solveSubstitutions);
- smtStatisticsRegistry()->registerStat(&d_solveTimer);
- smtStatisticsRegistry()->registerStat(&d_numCallsToCheckFullEffort);
- smtStatisticsRegistry()->registerStat(&d_numCallsToCheckStandardEffort);
- smtStatisticsRegistry()->registerStat(&d_weightComputationTimer);
- smtStatisticsRegistry()->registerStat(&d_numMultSlice);
-}
-
-BVSolverLazy::Statistics::~Statistics()
-{
- smtStatisticsRegistry()->unregisterStat(&d_avgConflictSize);
- smtStatisticsRegistry()->unregisterStat(&d_solveSubstitutions);
- smtStatisticsRegistry()->unregisterStat(&d_solveTimer);
- smtStatisticsRegistry()->unregisterStat(&d_numCallsToCheckFullEffort);
- smtStatisticsRegistry()->unregisterStat(&d_numCallsToCheckStandardEffort);
- smtStatisticsRegistry()->unregisterStat(&d_weightComputationTimer);
- smtStatisticsRegistry()->unregisterStat(&d_numMultSlice);
}
void BVSolverLazy::preRegisterTerm(TNode node)
TimerStat d_weightComputationTimer;
IntStat d_numMultSlice;
Statistics();
- ~Statistics();
};
Statistics d_statistics;
}
AlgebraicSolver::Statistics::Statistics()
- : d_numCallstoCheck("theory::bv::algebraic::NumCallsToCheck", 0)
- , d_numSimplifiesToTrue("theory::bv::algebraic::NumSimplifiesToTrue", 0)
- , d_numSimplifiesToFalse("theory::bv::algebraic::NumSimplifiesToFalse", 0)
- , d_numUnsat("theory::bv::algebraic::NumUnsat", 0)
- , d_numSat("theory::bv::algebraic::NumSat", 0)
- , d_numUnknown("theory::bv::algebraic::NumUnknown", 0)
- , d_solveTime("theory::bv::algebraic::SolveTime")
- , d_useHeuristic("theory::bv::algebraic::UseHeuristic", 0.2)
+ : d_numCallstoCheck(smtStatisticsRegistry().registerInt(
+ "theory::bv::algebraic::NumCallsToCheck")),
+ d_numSimplifiesToTrue(smtStatisticsRegistry().registerInt(
+ "theory::bv::algebraic::NumSimplifiesToTrue")),
+ d_numSimplifiesToFalse(smtStatisticsRegistry().registerInt(
+ "theory::bv::algebraic::NumSimplifiesToFalse")),
+ d_numUnsat(smtStatisticsRegistry().registerInt(
+ "theory::bv::algebraic::NumUnsat")),
+ d_numSat(
+ smtStatisticsRegistry().registerInt("theory::bv::algebraic::NumSat")),
+ d_numUnknown(smtStatisticsRegistry().registerInt(
+ "theory::bv::algebraic::NumUnknown")),
+ d_solveTime(smtStatisticsRegistry().registerTimer(
+ "theory::bv::algebraic::SolveTime")),
+ d_useHeuristic(smtStatisticsRegistry().registerValue<double>(
+ "theory::bv::algebraic::UseHeuristic", 0.2))
{
- smtStatisticsRegistry()->registerStat(&d_numCallstoCheck);
- smtStatisticsRegistry()->registerStat(&d_numSimplifiesToTrue);
- smtStatisticsRegistry()->registerStat(&d_numSimplifiesToFalse);
- smtStatisticsRegistry()->registerStat(&d_numUnsat);
- smtStatisticsRegistry()->registerStat(&d_numSat);
- smtStatisticsRegistry()->registerStat(&d_numUnknown);
- smtStatisticsRegistry()->registerStat(&d_solveTime);
- smtStatisticsRegistry()->registerStat(&d_useHeuristic);
-}
-
-AlgebraicSolver::Statistics::~Statistics() {
- smtStatisticsRegistry()->unregisterStat(&d_numCallstoCheck);
- smtStatisticsRegistry()->unregisterStat(&d_numSimplifiesToTrue);
- smtStatisticsRegistry()->unregisterStat(&d_numSimplifiesToFalse);
- smtStatisticsRegistry()->unregisterStat(&d_numUnsat);
- smtStatisticsRegistry()->unregisterStat(&d_numSat);
- smtStatisticsRegistry()->unregisterStat(&d_numUnknown);
- smtStatisticsRegistry()->unregisterStat(&d_solveTime);
- smtStatisticsRegistry()->unregisterStat(&d_useHeuristic);
}
bool hasExpensiveBVOperatorsRec(TNode fact, TNodeSet& seen) {
IntStat d_numSat;
IntStat d_numUnknown;
TimerStat d_solveTime;
- BackedStat<double> d_useHeuristic;
+ ValueStat<double> d_useHeuristic;
Statistics();
- ~Statistics();
};
std::unique_ptr<SubstitutionMap> d_modelMap;
BitblastSolver::~BitblastSolver() {}
BitblastSolver::Statistics::Statistics()
- : d_numCallstoCheck("theory::bv::BitblastSolver::NumCallsToCheck", 0)
- , d_numBBLemmas("theory::bv::BitblastSolver::NumTimesLemmasBB", 0)
+ : d_numCallstoCheck(smtStatisticsRegistry().registerInt(
+ "theory::bv::BitblastSolver::NumCallsToCheck")),
+ d_numBBLemmas(smtStatisticsRegistry().registerInt(
+ "theory::bv::BitblastSolver::NumTimesLemmasBB"))
{
- smtStatisticsRegistry()->registerStat(&d_numCallstoCheck);
- smtStatisticsRegistry()->registerStat(&d_numBBLemmas);
-}
-BitblastSolver::Statistics::~Statistics() {
- smtStatisticsRegistry()->unregisterStat(&d_numCallstoCheck);
- smtStatisticsRegistry()->unregisterStat(&d_numBBLemmas);
}
void BitblastSolver::setAbstraction(AbstractionModule* abs) {
IntStat d_numCallstoCheck;
IntStat d_numBBLemmas;
Statistics();
- ~Statistics();
};
/** Bitblaster */
std::unique_ptr<TLazyBitblaster> d_bitblaster;
}
CoreSolver::Statistics::Statistics()
- : d_numCallstoCheck("theory::bv::CoreSolver::NumCallsToCheck", 0)
+ : d_numCallstoCheck(smtStatisticsRegistry().registerInt(
+ "theory::bv::CoreSolver::NumCallsToCheck"))
{
- smtStatisticsRegistry()->registerStat(&d_numCallstoCheck);
-}
-CoreSolver::Statistics::~Statistics() {
- smtStatisticsRegistry()->unregisterStat(&d_numCallstoCheck);
}
void CoreSolver::checkExtf(Theory::Effort e)
struct Statistics {
IntStat d_numCallstoCheck;
Statistics();
- ~Statistics();
};
// NotifyClass: handles call-back from congruence closure module
}
InequalitySolver::Statistics::Statistics()
- : d_numCallstoCheck("theory::bv::inequality::NumCallsToCheck", 0),
- d_solveTime("theory::bv::inequality::SolveTime")
+ : d_numCallstoCheck(smtStatisticsRegistry().registerInt(
+ "theory::bv::inequality::NumCallsToCheck")),
+ d_solveTime(smtStatisticsRegistry().registerTimer(
+ "theory::bv::inequality::SolveTime"))
{
- smtStatisticsRegistry()->registerStat(&d_numCallstoCheck);
- smtStatisticsRegistry()->registerStat(&d_solveTime);
-}
-
-InequalitySolver::Statistics::~Statistics()
-{
- smtStatisticsRegistry()->unregisterStat(&d_numCallstoCheck);
- smtStatisticsRegistry()->unregisterStat(&d_solveTime);
}
IntStat d_numCallstoCheck;
TimerStat d_solveTime;
Statistics();
- ~Statistics();
};
context::CDHashSet<Node, NodeHashFunction> d_assertionSet;
d_internal(nullptr),
d_rewriter(),
d_state(c, u, valuation),
- d_im(*this, d_state, nullptr, "theory::bv"),
+ d_im(*this, d_state, nullptr, "theory::bv::"),
d_notify(d_im)
{
switch (options::bvSolver())
#include "smt/smt_engine_scope.h"
#include "theory/bv/theory_bv_utils.h"
#include "theory/theory.h"
-#include "util/statistics_registry.h"
+#include "util/statistics_stats.h"
namespace cvc5 {
namespace theory {
InferenceManager::InferenceManager(Theory& t,
TheoryState& state,
ProofNodeManager* pnm)
- : InferenceManagerBuffered(t, state, pnm, "theory::datatypes"),
+ : InferenceManagerBuffered(t, state, pnm, "theory::datatypes::"),
d_pnm(pnm),
d_ipc(pnm == nullptr ? nullptr
: new InferProofCons(state.getSatContext(), pnm)),
namespace theory {
EngineOutputChannel::Statistics::Statistics(theory::TheoryId theory)
- : conflicts(getStatsPrefix(theory) + "::conflicts", 0),
- propagations(getStatsPrefix(theory) + "::propagations", 0),
- lemmas(getStatsPrefix(theory) + "::lemmas", 0),
- requirePhase(getStatsPrefix(theory) + "::requirePhase", 0),
- restartDemands(getStatsPrefix(theory) + "::restartDemands", 0),
- trustedConflicts(getStatsPrefix(theory) + "::trustedConflicts", 0),
- trustedLemmas(getStatsPrefix(theory) + "::trustedLemmas", 0)
+ : conflicts(smtStatisticsRegistry().registerInt(getStatsPrefix(theory)
+ + "conflicts")),
+ propagations(smtStatisticsRegistry().registerInt(getStatsPrefix(theory)
+ + "propagations")),
+ lemmas(smtStatisticsRegistry().registerInt(getStatsPrefix(theory)
+ + "lemmas")),
+ requirePhase(smtStatisticsRegistry().registerInt(getStatsPrefix(theory)
+ + "requirePhase")),
+ restartDemands(smtStatisticsRegistry().registerInt(getStatsPrefix(theory)
+ + "restartDemands")),
+ trustedConflicts(smtStatisticsRegistry().registerInt(
+ getStatsPrefix(theory) + "trustedConflicts")),
+ trustedLemmas(smtStatisticsRegistry().registerInt(getStatsPrefix(theory)
+ + "trustedLemmas"))
{
- smtStatisticsRegistry()->registerStat(&conflicts);
- smtStatisticsRegistry()->registerStat(&propagations);
- smtStatisticsRegistry()->registerStat(&lemmas);
- smtStatisticsRegistry()->registerStat(&requirePhase);
- smtStatisticsRegistry()->registerStat(&restartDemands);
- smtStatisticsRegistry()->registerStat(&trustedConflicts);
- smtStatisticsRegistry()->registerStat(&trustedLemmas);
-}
-
-EngineOutputChannel::Statistics::~Statistics()
-{
- smtStatisticsRegistry()->unregisterStat(&conflicts);
- smtStatisticsRegistry()->unregisterStat(&propagations);
- smtStatisticsRegistry()->unregisterStat(&lemmas);
- smtStatisticsRegistry()->unregisterStat(&requirePhase);
- smtStatisticsRegistry()->unregisterStat(&restartDemands);
- smtStatisticsRegistry()->unregisterStat(&trustedConflicts);
- smtStatisticsRegistry()->unregisterStat(&trustedLemmas);
}
EngineOutputChannel::EngineOutputChannel(TheoryEngine* engine,
#include "expr/node.h"
#include "theory/output_channel.h"
#include "theory/theory_id.h"
-#include "util/statistics_registry.h"
+#include "util/statistics_stats.h"
namespace cvc5 {
{
public:
Statistics(theory::TheoryId theory);
- ~Statistics();
/** Number of calls to conflict, propagate, lemma, requirePhase,
* restartDemands */
IntStat conflicts, propagations, lemmas, requirePhase, restartDemands,
d_floatToRealMap(u),
d_abstractionMap(u),
d_state(c, u, valuation),
- d_im(*this, d_state, pnm, "theory::fp", false)
+ d_im(*this, d_state, pnm, "theory::fp::", false)
{
// indicate we are using the default theory state and inference manager
d_theoryState = &d_state;
InferenceManagerBuffered::InferenceManagerBuffered(Theory& t,
TheoryState& state,
ProofNodeManager* pnm,
- const std::string& name,
+ const std::string& statsName,
bool cacheLemmas)
- : TheoryInferenceManager(t, state, pnm, name, cacheLemmas),
+ : TheoryInferenceManager(t, state, pnm, statsName, cacheLemmas),
d_processingPendingLemmas(false)
{
}
InferenceManagerBuffered(Theory& t,
TheoryState& state,
ProofNodeManager* pnm,
- const std::string& name,
+ const std::string& statsName,
bool cacheLemmas = true);
virtual ~InferenceManagerBuffered() {}
/**
#include "expr/node.h"
#include "theory/inference_id.h"
-#include "util/statistics_registry.h"
+#include "util/statistics_stats.h"
namespace cvc5 {
namespace theory {
#include "theory/quantifiers/cegqi/vts_term_cache.h"
#include "theory/quantifiers/instantiate.h"
#include "theory/quantifiers/quant_module.h"
-#include "util/statistics_registry.h"
+#include "util/statistics_stats.h"
namespace cvc5 {
namespace theory {
}
Instantiate::Statistics::Statistics()
- : d_instantiations("Instantiate::Instantiations_Total", 0),
- d_inst_duplicate("Instantiate::Duplicate_Inst", 0),
- d_inst_duplicate_eq("Instantiate::Duplicate_Inst_Eq", 0),
- d_inst_duplicate_ent("Instantiate::Duplicate_Inst_Entailed", 0)
+ : d_instantiations(smtStatisticsRegistry().registerInt(
+ "Instantiate::Instantiations_Total")),
+ d_inst_duplicate(
+ smtStatisticsRegistry().registerInt("Instantiate::Duplicate_Inst")),
+ d_inst_duplicate_eq(smtStatisticsRegistry().registerInt(
+ "Instantiate::Duplicate_Inst_Eq")),
+ d_inst_duplicate_ent(smtStatisticsRegistry().registerInt(
+ "Instantiate::Duplicate_Inst_Entailed"))
{
- smtStatisticsRegistry()->registerStat(&d_instantiations);
- smtStatisticsRegistry()->registerStat(&d_inst_duplicate);
- smtStatisticsRegistry()->registerStat(&d_inst_duplicate_eq);
- smtStatisticsRegistry()->registerStat(&d_inst_duplicate_ent);
-}
-
-Instantiate::Statistics::~Statistics()
-{
- smtStatisticsRegistry()->unregisterStat(&d_instantiations);
- smtStatisticsRegistry()->unregisterStat(&d_inst_duplicate);
- smtStatisticsRegistry()->unregisterStat(&d_inst_duplicate_eq);
- smtStatisticsRegistry()->unregisterStat(&d_inst_duplicate_ent);
}
} // namespace quantifiers
#include "theory/inference_id.h"
#include "theory/quantifiers/inst_match_trie.h"
#include "theory/quantifiers/quant_util.h"
-#include "util/statistics_registry.h"
+#include "util/statistics_stats.h"
namespace cvc5 {
IntStat d_inst_duplicate_eq;
IntStat d_inst_duplicate_ent;
Statistics();
- ~Statistics();
}; /* class Instantiate::Statistics */
Statistics d_statistics;
}
}
-QuantConflictFind::Statistics::Statistics():
- d_inst_rounds("QuantConflictFind::Inst_Rounds", 0),
- d_entailment_checks("QuantConflictFind::Entailment_Checks",0)
+QuantConflictFind::Statistics::Statistics()
+ : d_inst_rounds(
+ smtStatisticsRegistry().registerInt("QuantConflictFind::Inst_Rounds")),
+ d_entailment_checks(smtStatisticsRegistry().registerInt(
+ "QuantConflictFind::Entailment_Checks"))
{
- smtStatisticsRegistry()->registerStat(&d_inst_rounds);
- smtStatisticsRegistry()->registerStat(&d_entailment_checks);
-}
-
-QuantConflictFind::Statistics::~Statistics(){
- smtStatisticsRegistry()->unregisterStat(&d_inst_rounds);
- smtStatisticsRegistry()->unregisterStat(&d_entailment_checks);
}
TNode QuantConflictFind::getZero( Kind k ) {
IntStat d_inst_rounds;
IntStat d_entailment_checks;
Statistics();
- ~Statistics();
};
Statistics d_statistics;
/** Identify this module */
QuantifiersRegistry& qr,
TermRegistry& tr,
ProofNodeManager* pnm)
- : InferenceManagerBuffered(t, state, pnm, "theory::quantifiers"),
+ : InferenceManagerBuffered(t, state, pnm, "theory::quantifiers::"),
d_instantiate(new Instantiate(state, *this, qr, tr, pnm)),
d_skolemize(new Skolemize(state, tr, pnm))
{
namespace quantifiers {
QuantifiersStatistics::QuantifiersStatistics()
- : d_time("theory::QuantifiersEngine::time"),
- d_qcf_time("theory::QuantifiersEngine::time_qcf"),
- d_ematching_time("theory::QuantifiersEngine::time_ematching"),
- d_num_quant("QuantifiersEngine::Num_Quantifiers", 0),
- d_instantiation_rounds("QuantifiersEngine::Rounds_Instantiation_Full", 0),
- d_instantiation_rounds_lc(
- "QuantifiersEngine::Rounds_Instantiation_Last_Call", 0),
- d_triggers("QuantifiersEngine::Triggers", 0),
- d_simple_triggers("QuantifiersEngine::Triggers_Simple", 0),
- d_multi_triggers("QuantifiersEngine::Triggers_Multi", 0),
- d_red_alpha_equiv("QuantifiersEngine::Reductions_Alpha_Equivalence", 0)
+ : d_time(smtStatisticsRegistry().registerTimer(
+ "theory::QuantifiersEngine::time")),
+ d_qcf_time(smtStatisticsRegistry().registerTimer(
+ "theory::QuantifiersEngine::time_qcf")),
+ d_ematching_time(smtStatisticsRegistry().registerTimer(
+ "theory::QuantifiersEngine::time_ematching")),
+ d_num_quant(smtStatisticsRegistry().registerInt(
+ "QuantifiersEngine::Num_Quantifiers")),
+ d_instantiation_rounds(smtStatisticsRegistry().registerInt(
+ "QuantifiersEngine::Rounds_Instantiation_Full")),
+ d_instantiation_rounds_lc(smtStatisticsRegistry().registerInt(
+ "QuantifiersEngine::Rounds_Instantiation_Last_Call")),
+ d_triggers(
+ smtStatisticsRegistry().registerInt("QuantifiersEngine::Triggers")),
+ d_simple_triggers(smtStatisticsRegistry().registerInt(
+ "QuantifiersEngine::Triggers_Simple")),
+ d_multi_triggers(smtStatisticsRegistry().registerInt(
+ "QuantifiersEngine::Triggers_Multi")),
+ d_red_alpha_equiv(smtStatisticsRegistry().registerInt(
+ "QuantifiersEngine::Reductions_Alpha_Equivalence"))
{
- smtStatisticsRegistry()->registerStat(&d_time);
- smtStatisticsRegistry()->registerStat(&d_qcf_time);
- smtStatisticsRegistry()->registerStat(&d_ematching_time);
- smtStatisticsRegistry()->registerStat(&d_num_quant);
- smtStatisticsRegistry()->registerStat(&d_instantiation_rounds);
- smtStatisticsRegistry()->registerStat(&d_instantiation_rounds_lc);
- smtStatisticsRegistry()->registerStat(&d_triggers);
- smtStatisticsRegistry()->registerStat(&d_simple_triggers);
- smtStatisticsRegistry()->registerStat(&d_multi_triggers);
- smtStatisticsRegistry()->registerStat(&d_red_alpha_equiv);
-}
-
-QuantifiersStatistics::~QuantifiersStatistics()
-{
- smtStatisticsRegistry()->unregisterStat(&d_time);
- smtStatisticsRegistry()->unregisterStat(&d_qcf_time);
- smtStatisticsRegistry()->unregisterStat(&d_ematching_time);
- smtStatisticsRegistry()->unregisterStat(&d_num_quant);
- smtStatisticsRegistry()->unregisterStat(&d_instantiation_rounds);
- smtStatisticsRegistry()->unregisterStat(&d_instantiation_rounds_lc);
- smtStatisticsRegistry()->unregisterStat(&d_triggers);
- smtStatisticsRegistry()->unregisterStat(&d_simple_triggers);
- smtStatisticsRegistry()->unregisterStat(&d_multi_triggers);
- smtStatisticsRegistry()->unregisterStat(&d_red_alpha_equiv);
}
} // namespace quantifiers
#ifndef CVC5__THEORY__QUANTIFIERS__QUANTIFIERS_STATISTICS_H
#define CVC5__THEORY__QUANTIFIERS__QUANTIFIERS_STATISTICS_H
-#include "util/statistics_registry.h"
-#include "util/stats_timer.h"
+#include "util/statistics_stats.h"
namespace cvc5 {
namespace theory {
{
public:
QuantifiersStatistics();
- ~QuantifiersStatistics();
TimerStat d_time;
TimerStat d_qcf_time;
TimerStat d_ematching_time;
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),
- d_enumTermsRewrite("SygusEnumerator::enumTermsRewrite", 0),
- d_enumTermsExampleEval("SygusEnumerator::enumTermsEvalExamples", 0),
- d_enumTerms("SygusEnumerator::enumTerms", 0)
+ : d_cegqi_lemmas_ce(
+ smtStatisticsRegistry().registerInt("SynthEngine::cegqi_lemmas_ce")),
+ d_cegqi_lemmas_refine(smtStatisticsRegistry().registerInt(
+ "SynthEngine::cegqi_lemmas_refine")),
+ d_cegqi_si_lemmas(
+ smtStatisticsRegistry().registerInt("SynthEngine::cegqi_lemmas_si")),
+ d_solutions(
+ smtStatisticsRegistry().registerInt("SynthConjecture::solutions")),
+ d_filtered_solutions(smtStatisticsRegistry().registerInt(
+ "SynthConjecture::filtered_solutions")),
+ d_candidate_rewrites_print(smtStatisticsRegistry().registerInt(
+ "SynthConjecture::candidate_rewrites_print")),
+ d_enumTermsRewrite(smtStatisticsRegistry().registerInt(
+ "SygusEnumerator::enumTermsRewrite")),
+ d_enumTermsExampleEval(smtStatisticsRegistry().registerInt(
+ "SygusEnumerator::enumTermsEvalExamples")),
+ d_enumTerms(
+ smtStatisticsRegistry().registerInt("SygusEnumerator::enumTerms"))
{
- 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);
- smtStatisticsRegistry()->registerStat(&d_enumTermsRewrite);
- smtStatisticsRegistry()->registerStat(&d_enumTermsExampleEval);
- smtStatisticsRegistry()->registerStat(&d_enumTerms);
-}
-
-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);
- smtStatisticsRegistry()->unregisterStat(&d_enumTermsRewrite);
- smtStatisticsRegistry()->unregisterStat(&d_enumTermsExampleEval);
- smtStatisticsRegistry()->unregisterStat(&d_enumTerms);
}
} // namespace quantifiers
#ifndef CVC5__THEORY__QUANTIFIERS__SYGUS_STATS_H
#define CVC5__THEORY__QUANTIFIERS__SYGUS_STATS_H
-#include "util/statistics_registry.h"
+#include "util/statistics_stats.h"
namespace cvc5 {
namespace theory {
{
public:
SygusStatistics();
- ~SygusStatistics();
/** Number of counterexample lemmas */
IntStat d_cegqi_lemmas_ce;
/** Number of refinement lemmas */
#include "theory/quantifiers/term_pools.h"
#include "theory/quantifiers/term_registry.h"
#include "theory/quantifiers/term_util.h"
-#include "util/statistics_registry.h"
+#include "util/statistics_stats.h"
namespace cvc5 {
d_lemmas_produced_c(u),
d_bounds_init(false),
d_state(c, u, valuation),
- d_im(*this, d_state, nullptr, "theory::sep"),
+ d_im(*this, d_state, nullptr, "theory::sep::"),
d_notify(*this),
d_reduce(u),
d_spatial_assertions(c)
#include "theory/theory.h"
#include "theory/theory_state.h"
#include "theory/uf/equality_engine.h"
-#include "util/statistics_registry.h"
+#include "util/statistics_stats.h"
namespace cvc5 {
namespace theory {
InferenceManager::InferenceManager(Theory& t,
SolverState& s,
ProofNodeManager* pnm)
- : InferenceManagerBuffered(t, s, pnm, "theory::sets"), d_state(s)
+ : InferenceManagerBuffered(t, s, pnm, "theory::sets::"), d_state(s)
{
d_true = NodeManager::currentNM()->mkConst(true);
d_false = NodeManager::currentNM()->mkConst(false);
context::UserContext* userContext,
ProofNodeManager* pnm)
: ContextNotifyObj(context),
- d_statSharedTerms("theory::shared_terms", 0),
+ d_statSharedTerms(
+ smtStatisticsRegistry().registerInt("theory::shared_terms")),
d_addedSharedTermsSize(context, 0),
d_termsToTheories(context),
d_alreadyNotifiedMap(context),
d_pfee(nullptr),
d_pnm(pnm)
{
- smtStatisticsRegistry()->registerStat(&d_statSharedTerms);
-}
-
-SharedTermsDatabase::~SharedTermsDatabase()
-{
- smtStatisticsRegistry()->unregisterStat(&d_statSharedTerms);
}
void SharedTermsDatabase::setEqualityEngine(eq::EqualityEngine* ee)
#include "theory/trust_node.h"
#include "theory/uf/equality_engine.h"
#include "theory/uf/proof_equality_engine.h"
-#include "util/statistics_registry.h"
+#include "util/statistics_stats.h"
namespace cvc5 {
context::Context* context,
context::UserContext* userContext,
ProofNodeManager* pnm);
- ~SharedTermsDatabase();
//-------------------------------------------- initialization
/** Called to set the equality engine. */
#include "theory/strings/sequences_rewriter.h"
#include "theory/strings/theory_strings_preprocess.h"
#include "theory/strings/theory_strings_utils.h"
+#include "util/statistics_registry.h"
using namespace std;
using namespace cvc5::context;
#include "theory/rewriter.h"
#include "theory/strings/regexp_operation.h"
#include "theory/strings/theory_strings_utils.h"
+#include "util/statistics_registry.h"
using namespace cvc5::kind;
ExtTheory& e,
SequencesStatistics& statistics,
ProofNodeManager* pnm)
- : InferenceManagerBuffered(t, s, pnm, "theory::strings", false),
+ : InferenceManagerBuffered(t, s, pnm, "theory::strings::", false),
d_state(s),
d_termReg(tr),
d_extt(e),
#include "theory/ext_theory.h"
#include "theory/strings/theory_strings_utils.h"
#include "theory/theory_model.h"
+#include "util/statistics_value.h"
using namespace std;
using namespace cvc5::context;
#include "theory/strings/strings_rewriter.h"
#include "theory/strings/theory_strings_utils.h"
#include "theory/strings/word.h"
+#include "util/statistics_registry.h"
using namespace std;
using namespace cvc5::kind;
namespace theory {
namespace strings {
-SequencesRewriter::SequencesRewriter(IntegralHistogramStat<Rewrite>* statistics)
+SequencesRewriter::SequencesRewriter(HistogramStat<Rewrite>* statistics)
: d_statistics(statistics), d_stringsEntail(*this)
{
}
class SequencesRewriter : public TheoryRewriter
{
public:
- SequencesRewriter(IntegralHistogramStat<Rewrite>* statistics);
+ SequencesRewriter(HistogramStat<Rewrite>* statistics);
protected:
/** rewrite regular expression concatenation
static Node canonicalStrForSymbolicLength(Node n, TypeNode stype);
/** Reference to the rewriter statistics. */
- IntegralHistogramStat<Rewrite>* d_statistics;
+ HistogramStat<Rewrite>* d_statistics;
/** Instance of the entailment checker for strings. */
StringsEntail d_stringsEntail;
namespace strings {
SequencesStatistics::SequencesStatistics()
- : d_checkRuns("theory::strings::checkRuns", 0),
- d_strategyRuns("theory::strings::strategyRuns", 0),
- d_inferencesNoPf("theory::strings::inferencesNoPf"),
- d_cdSimplifications("theory::strings::cdSimplifications"),
- d_reductions("theory::strings::reductions"),
- d_regexpUnfoldingsPos("theory::strings::regexpUnfoldingsPos"),
- d_regexpUnfoldingsNeg("theory::strings::regexpUnfoldingsNeg"),
- d_rewrites("theory::strings::rewrites"),
- d_conflictsEqEngine("theory::strings::conflictsEqEngine", 0),
- d_conflictsEager("theory::strings::conflictsEager", 0),
- d_conflictsInfer("theory::strings::conflictsInfer", 0)
+ : d_checkRuns(
+ smtStatisticsRegistry().registerInt("theory::strings::checkRuns")),
+ d_strategyRuns(
+ smtStatisticsRegistry().registerInt("theory::strings::strategyRuns")),
+ d_inferencesNoPf(smtStatisticsRegistry().registerHistogram<InferenceId>(
+ "theory::strings::inferencesNoPf")),
+ d_cdSimplifications(smtStatisticsRegistry().registerHistogram<Kind>(
+ "theory::strings::cdSimplifications")),
+ d_reductions(smtStatisticsRegistry().registerHistogram<Kind>(
+ "theory::strings::reductions")),
+ d_regexpUnfoldingsPos(smtStatisticsRegistry().registerHistogram<Kind>(
+ "theory::strings::regexpUnfoldingsPos")),
+ d_regexpUnfoldingsNeg(smtStatisticsRegistry().registerHistogram<Kind>(
+ "theory::strings::regexpUnfoldingsNeg")),
+ d_rewrites(smtStatisticsRegistry().registerHistogram<Rewrite>(
+ "theory::strings::rewrites")),
+ d_conflictsEqEngine(smtStatisticsRegistry().registerInt(
+ "theory::strings::conflictsEqEngine")),
+ d_conflictsEager(smtStatisticsRegistry().registerInt(
+ "theory::strings::conflictsEager")),
+ d_conflictsInfer(smtStatisticsRegistry().registerInt(
+ "theory::strings::conflictsInfer"))
{
- smtStatisticsRegistry()->registerStat(&d_checkRuns);
- smtStatisticsRegistry()->registerStat(&d_strategyRuns);
- smtStatisticsRegistry()->registerStat(&d_inferencesNoPf);
- smtStatisticsRegistry()->registerStat(&d_cdSimplifications);
- smtStatisticsRegistry()->registerStat(&d_reductions);
- smtStatisticsRegistry()->registerStat(&d_regexpUnfoldingsPos);
- smtStatisticsRegistry()->registerStat(&d_regexpUnfoldingsNeg);
- smtStatisticsRegistry()->registerStat(&d_rewrites);
- smtStatisticsRegistry()->registerStat(&d_conflictsEqEngine);
- smtStatisticsRegistry()->registerStat(&d_conflictsEager);
- smtStatisticsRegistry()->registerStat(&d_conflictsInfer);
-}
-
-SequencesStatistics::~SequencesStatistics()
-{
- smtStatisticsRegistry()->unregisterStat(&d_checkRuns);
- smtStatisticsRegistry()->unregisterStat(&d_strategyRuns);
- smtStatisticsRegistry()->unregisterStat(&d_inferencesNoPf);
- smtStatisticsRegistry()->unregisterStat(&d_cdSimplifications);
- smtStatisticsRegistry()->unregisterStat(&d_reductions);
- smtStatisticsRegistry()->unregisterStat(&d_regexpUnfoldingsPos);
- smtStatisticsRegistry()->unregisterStat(&d_regexpUnfoldingsNeg);
- smtStatisticsRegistry()->unregisterStat(&d_rewrites);
- smtStatisticsRegistry()->unregisterStat(&d_conflictsEqEngine);
- smtStatisticsRegistry()->unregisterStat(&d_conflictsEager);
- smtStatisticsRegistry()->unregisterStat(&d_conflictsInfer);
}
}
#include "expr/kind.h"
#include "theory/strings/infer_info.h"
#include "theory/strings/rewrites.h"
-#include "util/statistics_registry.h"
-#include "util/stats_histogram.h"
+#include "util/statistics_stats.h"
namespace cvc5 {
namespace theory {
{
public:
SequencesStatistics();
- ~SequencesStatistics();
/** Number of calls to run a check where strategy is present */
IntStat d_checkRuns;
/** Number of calls to run the strategy */
* TheoryInferenceManager, i.e.
* (theory::strings::inferences{Facts,Lemmas,Conflicts}).
*/
- IntegralHistogramStat<InferenceId> d_inferencesNoPf;
+ HistogramStat<InferenceId> d_inferencesNoPf;
/**
* Counts the number of applications of each type of context-dependent
* simplification. The sum of this map is equal to the number of EXTF or
* EXTF_N inferences.
*/
- IntegralHistogramStat<Kind> d_cdSimplifications;
+ HistogramStat<Kind> d_cdSimplifications;
/**
* Counts the number of applications of each type of reduction. The sum of
* this map is equal to the number of REDUCTION inferences (when
* options::stringLazyPreproc is true).
*/
- IntegralHistogramStat<Kind> d_reductions;
+ HistogramStat<Kind> d_reductions;
/**
* Counts the number of applications of each type of regular expression
* positive (resp. negative) unfoldings. The sum of this map is equal to the
* number of RE_UNFOLD_POS (resp. RE_UNFOLD_NEG) inferences.
*/
- IntegralHistogramStat<Kind> d_regexpUnfoldingsPos;
- IntegralHistogramStat<Kind> d_regexpUnfoldingsNeg;
+ HistogramStat<Kind> d_regexpUnfoldingsPos;
+ HistogramStat<Kind> d_regexpUnfoldingsNeg;
//--------------- end of inferences
/** Counts the number of applications of each type of rewrite rule */
- IntegralHistogramStat<Rewrite> d_rewrites;
+ HistogramStat<Rewrite> d_rewrites;
//--------------- conflicts, partition of calls to OutputChannel::conflict
/** Number of equality engine conflicts */
IntStat d_conflictsEqEngine;
namespace theory {
namespace strings {
-StringsRewriter::StringsRewriter(IntegralHistogramStat<Rewrite>* statistics)
+StringsRewriter::StringsRewriter(HistogramStat<Rewrite>* statistics)
: SequencesRewriter(statistics)
{
}
class StringsRewriter : public SequencesRewriter
{
public:
- StringsRewriter(IntegralHistogramStat<Rewrite>* statistics);
+ StringsRewriter(HistogramStat<Rewrite>* statistics);
RewriteResponse postRewrite(TNode node) override;
#include "theory/strings/arith_entail.h"
#include "theory/strings/sequences_rewriter.h"
#include "theory/strings/word.h"
+#include "util/statistics_registry.h"
using namespace cvc5;
using namespace cvc5::kind;
typedef expr::Attribute<QInternalVarAttributeId, Node> QInternalVarAttribute;
StringsPreprocess::StringsPreprocess(SkolemCache* sc,
- IntegralHistogramStat<Kind>* statReductions)
+ HistogramStat<Kind>* statReductions)
: d_sc(sc), d_statReductions(statReductions)
{
}
class StringsPreprocess {
public:
StringsPreprocess(SkolemCache* sc,
- IntegralHistogramStat<Kind>* statReductions = nullptr);
+ HistogramStat<Kind>* statReductions = nullptr);
~StringsPreprocess();
/** The reduce routine
*
/** pointer to the skolem cache used by this class */
SkolemCache* d_sc;
/** Reference to the statistics for the theory of strings/sequences. */
- IntegralHistogramStat<Kind>* d_statReductions;
+ HistogramStat<Kind>* d_statReductions;
/** visited cache */
std::map<Node, Node> d_visited;
/**
d_sharedTermsIndex(satContext, 0),
d_careGraph(nullptr),
d_instanceName(name),
- d_checkTime(getStatsPrefix(id) + name + "::checkTime"),
- d_computeCareGraphTime(getStatsPrefix(id) + name
- + "::computeCareGraphTime"),
+ d_checkTime(smtStatisticsRegistry().registerTimer(getStatsPrefix(id)
+ + name + "checkTime")),
+ d_computeCareGraphTime(smtStatisticsRegistry().registerTimer(
+ getStatsPrefix(id) + name + "computeCareGraphTime")),
d_sharedTerms(satContext),
d_out(&out),
d_valuation(valuation),
d_quantEngine(nullptr),
d_pnm(pnm)
{
- smtStatisticsRegistry()->registerStat(&d_checkTime);
- smtStatisticsRegistry()->registerStat(&d_computeCareGraphTime);
}
Theory::~Theory() {
- smtStatisticsRegistry()->unregisterStat(&d_checkTime);
- smtStatisticsRegistry()->unregisterStat(&d_computeCareGraphTime);
}
bool Theory::needsEqualityEngine(EeSetupInfo& esi)
#include "theory/theory_id.h"
#include "theory/trust_node.h"
#include "theory/valuation.h"
-#include "util/statistics_registry.h"
-#include "util/stats_timer.h"
+#include "util/statistics_stats.h"
namespace cvc5 {
d_outMgr(outMgr),
d_pnm(pnm),
d_lazyProof(
- d_pnm != nullptr
- ? new LazyCDProof(
- d_pnm, nullptr, d_userContext, "TheoryEngine::LazyCDProof")
- : nullptr),
+ d_pnm != nullptr ? new LazyCDProof(
+ d_pnm, nullptr, d_userContext, "TheoryEngine::LazyCDProof")
+ : nullptr),
d_tepg(new TheoryEngineProofGenerator(d_pnm, d_userContext)),
d_tc(nullptr),
d_sharedSolver(nullptr),
d_propagatedLiterals(context),
d_propagatedLiteralsIndex(context, 0),
d_atomRequests(context),
- d_combineTheoriesTime("TheoryEngine::combineTheoriesTime"),
+ d_combineTheoriesTime(smtStatisticsRegistry().registerTimer(
+ "TheoryEngine::combineTheoriesTime")),
d_true(),
d_false(),
d_interrupted(false),
d_sortInfer.reset(new SortInference);
}
- smtStatisticsRegistry()->registerStat(&d_combineTheoriesTime);
d_true = NodeManager::currentNM()->mkConst<bool>(true);
d_false = NodeManager::currentNM()->mkConst<bool>(false);
}
delete d_theoryOut[theoryId];
}
}
-
- smtStatisticsRegistry()->unregisterStat(&d_combineTheoriesTime);
}
void TheoryEngine::interrupt() { d_interrupted = true; }
#include "theory/uf/equality_engine.h"
#include "theory/valuation.h"
#include "util/hash.h"
-#include "util/statistics_registry.h"
+#include "util/statistics_stats.h"
#include "util/unsafe_interrupt_exception.h"
namespace cvc5 {
{
switch (theoryId)
{
- case THEORY_BUILTIN: return "theory::builtin"; break;
- case THEORY_BOOL: return "theory::bool"; break;
- case THEORY_UF: return "theory::uf"; break;
- case THEORY_ARITH: return "theory::arith"; break;
- case THEORY_BV: return "theory::bv"; break;
- case THEORY_FP: return "theory::fp"; break;
- case THEORY_ARRAYS: return "theory::arrays"; break;
- case THEORY_DATATYPES: return "theory::datatypes"; break;
- case THEORY_SEP: return "theory::sep"; break;
- case THEORY_SETS: return "theory::sets"; break;
- case THEORY_BAGS: return "theory::bags"; break;
- case THEORY_STRINGS: return "theory::strings"; break;
- case THEORY_QUANTIFIERS: return "theory::quantifiers"; break;
+ case THEORY_BUILTIN: return "theory::builtin::"; break;
+ case THEORY_BOOL: return "theory::bool::"; break;
+ case THEORY_UF: return "theory::uf::"; break;
+ case THEORY_ARITH: return "theory::arith::"; break;
+ case THEORY_BV: return "theory::bv::"; break;
+ case THEORY_FP: return "theory::fp::"; break;
+ case THEORY_ARRAYS: return "theory::arrays::"; break;
+ case THEORY_DATATYPES: return "theory::datatypes::"; break;
+ case THEORY_SEP: return "theory::sep::"; break;
+ case THEORY_SETS: return "theory::sets::"; break;
+ case THEORY_BAGS: return "theory::bags::"; break;
+ case THEORY_STRINGS: return "theory::strings::"; break;
+ case THEORY_QUANTIFIERS: return "theory::quantifiers::"; break;
default: break;
}
- return "unknown";
+ return "unknown::";
}
TheoryId TheoryIdSetUtil::setPop(TheoryIdSet& set)
TheoryInferenceManager::TheoryInferenceManager(Theory& t,
TheoryState& state,
ProofNodeManager* pnm,
- const std::string& name,
+ const std::string& statsName,
bool cacheLemmas)
: d_theory(t),
d_theoryState(state),
d_numConflicts(0),
d_numCurrentLemmas(0),
d_numCurrentFacts(0),
- d_conflictIdStats(name + "::inferencesConflict"),
- d_factIdStats(name + "::inferencesFact"),
- d_lemmaIdStats(name + "::inferencesLemma")
+ d_conflictIdStats(smtStatisticsRegistry().registerHistogram<InferenceId>(
+ statsName + "inferencesConflict")),
+ d_factIdStats(smtStatisticsRegistry().registerHistogram<InferenceId>(
+ statsName + "inferencesFact")),
+ d_lemmaIdStats(smtStatisticsRegistry().registerHistogram<InferenceId>(
+ statsName + "inferencesLemma"))
{
// don't add true lemma
Node truen = NodeManager::currentNM()->mkConst(true);
d_lemmasSent.insert(truen);
- smtStatisticsRegistry()->registerStat(&d_conflictIdStats);
- smtStatisticsRegistry()->registerStat(&d_factIdStats);
- smtStatisticsRegistry()->registerStat(&d_lemmaIdStats);
}
TheoryInferenceManager::~TheoryInferenceManager()
{
- smtStatisticsRegistry()->unregisterStat(&d_conflictIdStats);
- smtStatisticsRegistry()->unregisterStat(&d_factIdStats);
- smtStatisticsRegistry()->unregisterStat(&d_lemmaIdStats);
}
void TheoryInferenceManager::setEqualityEngine(eq::EqualityEngine* ee)
#include "theory/inference_id.h"
#include "theory/output_channel.h"
#include "theory/trust_node.h"
-#include "util/statistics_registry.h"
-#include "util/stats_histogram.h"
+#include "util/statistics_stats.h"
namespace cvc5 {
* @param state The state of the theory
* @param pnm The proof node manager, which if non-null, enables proofs for
* this inference manager
- * @param name The name of the inference manager, which is used for giving
- * unique names for statistics,
+ * @param statsName The name of the inference manager, which is used for
+ * giving unique names for statistics,
* @param cacheLemmas Whether all lemmas sent using this theory inference
* manager are added to a user-context dependent cache. This means that
* only lemmas that are unique after rewriting are sent to the theory engine
TheoryInferenceManager(Theory& t,
TheoryState& state,
ProofNodeManager* pnm,
- const std::string& name,
+ const std::string& statsName,
bool cacheLemmas = true);
virtual ~TheoryInferenceManager();
//--------------------------------------- initialization
/** The number of internal facts added since the last call to reset. */
uint32_t d_numCurrentFacts;
/** Statistics for conflicts sent via this inference manager. */
- IntegralHistogramStat<InferenceId> d_conflictIdStats;
+ HistogramStat<InferenceId> d_conflictIdStats;
/** Statistics for facts sent via this inference manager. */
- IntegralHistogramStat<InferenceId> d_factIdStats;
+ HistogramStat<InferenceId> d_factIdStats;
/** Statistics for lemmas sent via this inference manager. */
- IntegralHistogramStat<InferenceId> d_lemmaIdStats;
+ HistogramStat<InferenceId> d_lemmaIdStats;
};
} // namespace theory
}
CardinalityExtension::Statistics::Statistics()
- : d_clique_conflicts("CardinalityExtension::Clique_Conflicts", 0),
- d_clique_lemmas("CardinalityExtension::Clique_Lemmas", 0),
- d_split_lemmas("CardinalityExtension::Split_Lemmas", 0),
- d_max_model_size("CardinalityExtension::Max_Model_Size", 1)
+ : d_clique_conflicts(smtStatisticsRegistry().registerInt(
+ "CardinalityExtension::Clique_Conflicts")),
+ d_clique_lemmas(smtStatisticsRegistry().registerInt(
+ "CardinalityExtension::Clique_Lemmas")),
+ d_split_lemmas(smtStatisticsRegistry().registerInt(
+ "CardinalityExtension::Split_Lemmas")),
+ d_max_model_size(smtStatisticsRegistry().registerInt(
+ "CardinalityExtension::Max_Model_Size"))
{
- smtStatisticsRegistry()->registerStat(&d_clique_conflicts);
- smtStatisticsRegistry()->registerStat(&d_clique_lemmas);
- smtStatisticsRegistry()->registerStat(&d_split_lemmas);
- smtStatisticsRegistry()->registerStat(&d_max_model_size);
-}
-
-CardinalityExtension::Statistics::~Statistics()
-{
- smtStatisticsRegistry()->unregisterStat(&d_clique_conflicts);
- smtStatisticsRegistry()->unregisterStat(&d_clique_lemmas);
- smtStatisticsRegistry()->unregisterStat(&d_split_lemmas);
- smtStatisticsRegistry()->unregisterStat(&d_max_model_size);
+ d_max_model_size.maxAssign(1);
}
} // namespace uf
#include "context/context.h"
#include "theory/decision_strategy.h"
#include "theory/theory.h"
-#include "util/statistics_registry.h"
+#include "util/statistics_stats.h"
namespace cvc5 {
namespace theory {
IntStat d_split_lemmas;
IntStat d_max_model_size;
Statistics();
- ~Statistics();
};
/** statistics class */
Statistics d_statistics;
namespace theory {
namespace eq {
-EqualityEngine::Statistics::Statistics(std::string name)
- : d_mergesCount(name + "::mergesCount", 0),
- d_termsCount(name + "::termsCount", 0),
- d_functionTermsCount(name + "::functionTermsCount", 0),
- d_constantTermsCount(name + "::constantTermsCount", 0)
+EqualityEngine::Statistics::Statistics(const std::string& name)
+ : d_mergesCount(smtStatisticsRegistry().registerInt(name + "mergesCount")),
+ d_termsCount(smtStatisticsRegistry().registerInt(name + "termsCount")),
+ d_functionTermsCount(
+ smtStatisticsRegistry().registerInt(name + "functionTermsCount")),
+ d_constantTermsCount(
+ smtStatisticsRegistry().registerInt(name + "constantTermsCount"))
{
- smtStatisticsRegistry()->registerStat(&d_mergesCount);
- smtStatisticsRegistry()->registerStat(&d_termsCount);
- smtStatisticsRegistry()->registerStat(&d_functionTermsCount);
- smtStatisticsRegistry()->registerStat(&d_constantTermsCount);
-}
-
-EqualityEngine::Statistics::~Statistics() {
- smtStatisticsRegistry()->unregisterStat(&d_mergesCount);
- smtStatisticsRegistry()->unregisterStat(&d_termsCount);
- smtStatisticsRegistry()->unregisterStat(&d_functionTermsCount);
- smtStatisticsRegistry()->unregisterStat(&d_constantTermsCount);
}
/**
d_assertedEqualitiesCount(context, 0),
d_equalityTriggersCount(context, 0),
d_subtermEvaluatesSize(context, 0),
- d_stats(name),
+ d_stats(name + "::"),
d_inPropagate(false),
d_constantsAreTriggers(constantsAreTriggers),
d_anyTermsAreTriggers(anyTermTriggers),
d_assertedEqualitiesCount(context, 0),
d_equalityTriggersCount(context, 0),
d_subtermEvaluatesSize(context, 0),
- d_stats(name),
+ d_stats(name + "::"),
d_inPropagate(false),
d_constantsAreTriggers(constantsAreTriggers),
d_anyTermsAreTriggers(anyTermTriggers),
#include "theory/uf/equality_engine_iterator.h"
#include "theory/uf/equality_engine_notify.h"
#include "theory/uf/equality_engine_types.h"
-#include "util/statistics_registry.h"
+#include "util/statistics_stats.h"
namespace cvc5 {
namespace theory {
/** Number of constant terms managed by the system */
IntStat d_constantTermsCount;
- Statistics(std::string name);
-
- ~Statistics();
+ Statistics(const std::string& name);
};/* struct EqualityEngine::statistics */
private:
d_reps.clear();
}
-SymmetryBreaker::SymmetryBreaker(context::Context* context,
- std::string name) :
- ContextNotifyObj(context),
- d_assertionsToRerun(context),
- d_rerunningAssertions(false),
- d_phi(),
- d_phiSet(),
- d_permutations(),
- d_terms(),
- d_template(),
- d_normalizationCache(),
- d_termEqs(),
- d_termEqsOnly(),
- d_name(name),
- d_stats(d_name)
+SymmetryBreaker::SymmetryBreaker(context::Context* context, std::string name)
+ : ContextNotifyObj(context),
+ d_assertionsToRerun(context),
+ d_rerunningAssertions(false),
+ d_phi(),
+ d_phiSet(),
+ d_permutations(),
+ d_terms(),
+ d_template(),
+ d_normalizationCache(),
+ d_termEqs(),
+ d_termEqsOnly(),
+ d_name(name),
+ d_stats(d_name + "theory::uf::symmetry_breaker::")
{
}
}
}
-SymmetryBreaker::Statistics::Statistics(std::string name)
- : d_clauses(name + "theory::uf::symmetry_breaker::clauses", 0)
- , d_units(name + "theory::uf::symmetry_breaker::units", 0)
- , d_permutationSetsConsidered(name + "theory::uf::symmetry_breaker::permutationSetsConsidered", 0)
- , d_permutationSetsInvariant(name + "theory::uf::symmetry_breaker::permutationSetsInvariant", 0)
- , d_invariantByPermutationsTimer(name + "theory::uf::symmetry_breaker::timers::invariantByPermutations")
- , d_selectTermsTimer(name + "theory::uf::symmetry_breaker::timers::selectTerms")
- , d_initNormalizationTimer(name + "theory::uf::symmetry_breaker::timers::initNormalization")
-{
- smtStatisticsRegistry()->registerStat(&d_clauses);
- smtStatisticsRegistry()->registerStat(&d_units);
- smtStatisticsRegistry()->registerStat(&d_permutationSetsConsidered);
- smtStatisticsRegistry()->registerStat(&d_permutationSetsInvariant);
- smtStatisticsRegistry()->registerStat(&d_invariantByPermutationsTimer);
- smtStatisticsRegistry()->registerStat(&d_selectTermsTimer);
- smtStatisticsRegistry()->registerStat(&d_initNormalizationTimer);
-}
-
-SymmetryBreaker::Statistics::~Statistics()
+SymmetryBreaker::Statistics::Statistics(const std::string& name)
+ : d_clauses(smtStatisticsRegistry().registerInt(name + "clauses")),
+ d_units(smtStatisticsRegistry().registerInt(name + "units")),
+ d_permutationSetsConsidered(smtStatisticsRegistry().registerInt(
+ name + "permutationSetsConsidered")),
+ d_permutationSetsInvariant(smtStatisticsRegistry().registerInt(
+ name + "permutationSetsInvariant")),
+ d_invariantByPermutationsTimer(smtStatisticsRegistry().registerTimer(
+ name + "timers::invariantByPermutations")),
+ d_selectTermsTimer(
+ smtStatisticsRegistry().registerTimer(name + "timers::selectTerms")),
+ d_initNormalizationTimer(smtStatisticsRegistry().registerTimer(
+ name + "timers::initNormalization"))
{
- smtStatisticsRegistry()->unregisterStat(&d_clauses);
- smtStatisticsRegistry()->unregisterStat(&d_units);
- smtStatisticsRegistry()->unregisterStat(&d_permutationSetsConsidered);
- smtStatisticsRegistry()->unregisterStat(&d_permutationSetsInvariant);
- smtStatisticsRegistry()->unregisterStat(&d_invariantByPermutationsTimer);
- smtStatisticsRegistry()->unregisterStat(&d_selectTermsTimer);
- smtStatisticsRegistry()->unregisterStat(&d_initNormalizationTimer);
}
SymmetryBreaker::Terms::iterator
#include "expr/node.h"
#include "expr/node_builder.h"
#include "smt/smt_statistics_registry.h"
-#include "util/statistics_registry.h"
-#include "util/stats_timer.h"
+#include "util/statistics_stats.h"
namespace cvc5 {
namespace theory {
/** time spent in initial round of normalization */
TimerStat d_initNormalizationTimer;
- Statistics(std::string name);
- ~Statistics();
+ Statistics(const std::string& name);
};
Statistics d_stats;
d_functionsTerms(c),
d_symb(u, instanceName),
d_state(c, u, valuation),
- d_im(*this, d_state, pnm, "theory::uf", false),
+ d_im(*this, d_state, pnm, "theory::uf::" + instanceName, false),
d_notify(d_im, *this)
{
d_true = NodeManager::currentNM()->mkConst( true );
sexpr.h
smt2_quote_string.cpp
smt2_quote_string.h
- statistics.cpp
- statistics.h
statistics_public.cpp
statistics_public.h
- statistics_reg.cpp
- statistics_reg.h
statistics_registry.cpp
statistics_registry.h
+ statistics_stats.cpp
+ statistics_stats.h
statistics_value.cpp
statistics_value.h
- stats_base.cpp
- stats_base.h
- stats_histogram.h
- stats_timer.cpp
- stats_timer.h
- stats_utils.cpp
- stats_utils.h
string.cpp
string.h
tuple.h
struct ResourceManager::Statistics
{
- ReferenceStat<std::uint64_t> d_resourceUnitsUsed;
+ ReferenceStat<uint64_t> d_resourceUnitsUsed;
IntStat d_spendResourceCalls;
std::vector<IntStat> d_resourceSteps;
Statistics(StatisticsRegistry& stats);
- ~Statistics();
void bump(Resource r, uint64_t amount)
{
Assert(stats.size() > id);
stats[id] += amount;
}
-
- StatisticsRegistry& d_statisticsRegistry;
};
ResourceManager::Statistics::Statistics(StatisticsRegistry& stats)
- : d_resourceUnitsUsed("resource::resourceUnitsUsed"),
- d_spendResourceCalls("resource::spendResourceCalls", 0),
- d_statisticsRegistry(stats)
+ : d_resourceUnitsUsed(
+ stats.registerReference<uint64_t>("resource::resourceUnitsUsed")),
+ d_spendResourceCalls(stats.registerInt("resource::spendResourceCalls"))
{
- d_statisticsRegistry.registerStat(&d_resourceUnitsUsed);
- d_statisticsRegistry.registerStat(&d_spendResourceCalls);
-
- // Make sure we don't reallocate the vector
- d_resourceSteps.reserve(resman_detail::ResourceMax + 1);
for (std::size_t id = 0; id <= resman_detail::ResourceMax; ++id)
{
Resource r = static_cast<Resource>(id);
- d_resourceSteps.emplace_back("resource::res::" + std::string(toString(r)),
- 0);
- d_statisticsRegistry.registerStat(&d_resourceSteps[id]);
- }
-}
-
-ResourceManager::Statistics::~Statistics()
-{
- d_statisticsRegistry.unregisterStat(&d_resourceUnitsUsed);
- d_statisticsRegistry.unregisterStat(&d_spendResourceCalls);
-
- for (auto& stat : d_resourceSteps)
- {
- d_statisticsRegistry.unregisterStat(&stat);
+ d_resourceSteps.emplace_back(
+ stats.registerInt("resource::res::" + std::string(toString(r))));
}
}
+++ /dev/null
-/******************************************************************************
- * Top contributors (to current version):
- * Morgan Deters, Gereon Kremer, Tim King
- *
- * This file is part of the cvc5 project.
- *
- * Copyright (c) 2009-2021 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.
- * ****************************************************************************
- *
- * [[ Add one-line brief description here ]]
- *
- * [[ Add lengthier description here ]]
- * \todo document this file
- */
-
-#include "util/statistics.h"
-
-#include "util/safe_print.h"
-#include "util/statistics_registry.h" // for details about class Stat
-
-namespace cvc5 {
-
-bool StatisticsBase::StatCmp::operator()(const Stat* s1, const Stat* s2) const {
- return s1->getName() < s2->getName();
-}
-
-StatisticsBase::iterator::value_type StatisticsBase::iterator::operator*() const {
- return std::make_pair((*d_it)->getName(), (*d_it)->getValue());
-}
-
-StatisticsBase::StatisticsBase() :
- d_stats() {
-}
-
-StatisticsBase::StatisticsBase(const StatisticsBase& stats) :
- d_stats() {
-}
-
-StatisticsBase& StatisticsBase::operator=(const StatisticsBase& stats) {
- return *this;
-}
-
-void Statistics::copyFrom(const StatisticsBase& stats) {
- // This is ugly, but otherwise we have to introduce a "friend" relation for
- // Base to its derived class (really obnoxious).
- const StatisticsBase::const_iterator i_begin = stats.begin();
- const StatisticsBase::const_iterator i_end = stats.end();
- for(StatisticsBase::const_iterator i = i_begin; i != i_end; ++i) {
- SExprStat* p = new SExprStat((*i).first, (*i).second);
- d_stats.insert(p);
- }
-}
-
-void Statistics::clear() {
- for(StatSet::iterator i = d_stats.begin(); i != d_stats.end(); ++i) {
- delete *i;
- }
- d_stats.clear();
-}
-
-Statistics::Statistics(const StatisticsBase& stats) :
- StatisticsBase(stats) {
- copyFrom(stats);
-}
-
-Statistics::Statistics(const Statistics& stats) :
- StatisticsBase(stats) {
- copyFrom(stats);
-}
-
-Statistics::~Statistics() {
- clear();
-}
-
-Statistics& Statistics::operator=(const StatisticsBase& stats) {
- clear();
- this->StatisticsBase::operator=(stats);
- copyFrom(stats);
-
- return *this;
-}
-
-Statistics& Statistics::operator=(const Statistics& stats) {
- return this->operator=((const StatisticsBase&)stats);
-}
-
-StatisticsBase::const_iterator StatisticsBase::begin() const {
- return iterator(d_stats.begin());
-}
-
-StatisticsBase::const_iterator StatisticsBase::end() const {
- return iterator(d_stats.end());
-}
-
-void StatisticsBase::flushInformation(std::ostream &out) const {
-#ifdef CVC5_STATISTICS_ON
- for(StatSet::iterator i = d_stats.begin();
- i != d_stats.end();
- ++i) {
- Stat* s = *i;
- out << s->getName() << ", ";
- s->flushInformation(out);
- out << std::endl;
- }
-#endif /* CVC5_STATISTICS_ON */
-}
-
-void StatisticsBase::safeFlushInformation(int fd) const {
-#ifdef CVC5_STATISTICS_ON
- for (StatSet::iterator i = d_stats.begin(); i != d_stats.end(); ++i) {
- Stat* s = *i;
- safe_print(fd, s->getName());
- safe_print(fd, ", ");
- s->safeFlushInformation(fd);
- safe_print(fd, "\n");
- }
-#endif /* CVC5_STATISTICS_ON */
-}
-
-SExpr StatisticsBase::getStatistic(std::string name) const {
- SExpr value;
- IntStat s(name, 0);
- StatSet::iterator i = d_stats.find(&s);
- if(i != d_stats.end()) {
- return (*i)->getValue();
- } else {
- return SExpr();
- }
-}
-
-} // namespace cvc5
+++ /dev/null
-/******************************************************************************
- * Top contributors (to current version):
- * Morgan Deters, Mathias Preiner, Andres Noetzli
- *
- * This file is part of the cvc5 project.
- *
- * Copyright (c) 2009-2021 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.
- * ****************************************************************************
- *
- * [[ Add one-line brief description here ]]
- *
- * [[ Add lengthier description here ]]
- * \todo document this file
- */
-
-#include "cvc5_public.h"
-
-#ifndef CVC5__STATISTICS_H
-#define CVC5__STATISTICS_H
-
-#include <iterator>
-#include <ostream>
-#include <set>
-#include <string>
-#include <utility>
-
-#include "cvc4_export.h"
-#include "util/sexpr.h"
-
-namespace cvc5 {
-
-class Stat;
-
-class CVC4_EXPORT StatisticsBase
-{
- protected:
- /** A helper class for comparing two statistics */
- struct StatCmp {
- bool operator()(const Stat* s1, const Stat* s2) const;
- };/* struct StatisticsRegistry::StatCmp */
-
- /** A type for a set of statistics */
- typedef std::set< Stat*, StatCmp > StatSet;
-
- /** The set of statistics in this object */
- StatSet d_stats;
-
- StatisticsBase();
- StatisticsBase(const StatisticsBase& stats);
- StatisticsBase& operator=(const StatisticsBase& stats);
-
-public:
-
- virtual ~StatisticsBase() { }
-
- class iterator : public std::iterator<std::input_iterator_tag,
- std::pair<std::string, SExpr> >
- {
- StatSet::iterator d_it;
-
- iterator(StatSet::iterator it) : d_it(it) { }
-
- friend class StatisticsBase;
-
- public:
- iterator() : d_it() { }
- iterator(const iterator& it) : d_it(it.d_it) { }
- value_type operator*() const;
- iterator& operator++() { ++d_it; return *this; }
- iterator operator++(int) { iterator old = *this; ++d_it; return old; }
- bool operator==(const iterator& i) const { return d_it == i.d_it; }
- bool operator!=(const iterator& i) const { return d_it != i.d_it; }
- }; /* class StatisticsBase::iterator */
-
- /** An iterator type over a set of statistics. */
- typedef iterator const_iterator;
-
- /** Flush all statistics to the given output stream. */
- void flushInformation(std::ostream& out) const;
-
- /**
- * Flush all statistics to the given file descriptor. Safe to use in a signal
- * handler.
- */
- void safeFlushInformation(int fd) const;
-
- /** Get the value of a named statistic. */
- SExpr getStatistic(std::string name) const;
-
- /**
- * Get an iterator to the beginning of the range of the set of
- * statistics.
- */
- const_iterator begin() const;
-
- /**
- * Get an iterator to the end of the range of the set of statistics.
- */
- const_iterator end() const;
-
-}; /* class StatisticsBase */
-
-class Statistics : public StatisticsBase
-{
- void clear();
- void copyFrom(const StatisticsBase&);
-
-public:
-
- /**
- * Override the copy constructor to do a "deep" copy of statistics
- * values.
- */
- Statistics(const StatisticsBase& stats);
- Statistics(const Statistics& stats);
-
- ~Statistics();
-
- /**
- * Override the assignment operator to do a "deep" copy of statistics
- * values.
- */
- Statistics& operator=(const StatisticsBase& stats);
- Statistics& operator=(const Statistics& stats);
-
-}; /* class Statistics */
-
-} // namespace cvc5
-
-#endif /* CVC5__STATISTICS_H */
#include "util/statistics_public.h"
+#include "api/cpp/cvc5_kind.h"
+#include "expr/kind.h"
+#include "theory/inference_id.h"
+#include "theory/theory_id.h"
#include "util/statistics_registry.h"
namespace cvc5 {
void registerPublicStatistics(StatisticsRegistry& reg)
{
+ reg.registerHistogram<TypeConstant>("api::CONSTANT", false);
+ reg.registerHistogram<TypeConstant>("api::VARIABLE", false);
+ reg.registerHistogram<api::Kind>("api::TERM", false);
+ reg.registerValue<std::string>("driver::filename", false);
+ reg.registerValue<std::string>("driver::sat/unsat", false);
+ reg.registerValue<double>("driver::totalTime", false);
+
+ for (theory::TheoryId id = theory::THEORY_FIRST; id != theory::THEORY_LAST;
+ ++id)
+ {
+ std::string prefix = theory::getStatsPrefix(id);
+ reg.registerHistogram<theory::InferenceId>(prefix + "inferencesConflict",
+ false);
+ reg.registerHistogram<theory::InferenceId>(prefix + "inferencesFact",
+ false);
+ reg.registerHistogram<theory::InferenceId>(prefix + "inferencesLemma",
+ false);
+ }
}
} // namespace cvc5
+++ /dev/null
-/******************************************************************************
- * Top contributors (to current version):
- * Gereon Kremer
- *
- * This file is part of the cvc5 project.
- *
- * Copyright (c) 2009-2021 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.
- * ****************************************************************************
- *
- * Central statistics registry.
- *
- * The StatisticsRegistry that issues statistic proxy objects.
- */
-
-#include "util/statistics_reg.h"
-
-#include "options/base_options.h"
-#include "util/statistics_public.h"
-
-namespace cvc5 {
-
-StatisticsRegistry::StatisticsRegistry(bool registerPublic)
-{
- if (registerPublic)
- {
- registerPublicStatistics(*this);
- }
-}
-
-AverageStat StatisticsRegistry::registerAverage(const std::string& name,
- bool expert)
-{
- return registerStat<AverageStat>(name, expert);
-}
-IntStat StatisticsRegistry::registerInt(const std::string& name, bool expert)
-{
- return registerStat<IntStat>(name, expert);
-}
-TimerStat StatisticsRegistry::registerTimer(const std::string& name,
- bool expert)
-{
- return registerStat<TimerStat>(name, expert);
-}
-
-void StatisticsRegistry::storeSnapshot()
-{
- if constexpr (Configuration::isStatisticsBuild())
- {
- d_lastSnapshot = std::make_unique<Snapshot>();
- for (const auto& s : d_stats)
- {
- if (!options::statisticsExpert() && s.second->d_expert) continue;
- if (!options::statisticsUnset() && !s.second->hasValue()) continue;
- d_lastSnapshot->emplace(
- s.first,
- s.second->hasValue() ? s.second->getViewer() : StatExportData{});
- }
- }
-}
-
-StatisticBaseValue* StatisticsRegistry::get(const std::string& name) const
-{
- if constexpr (Configuration::isStatisticsBuild())
- {
- auto it = d_stats.find(name);
- if (it == d_stats.end()) return nullptr;
- return it->second.get();
- }
- return nullptr;
-}
-
-void StatisticsRegistry::print(std::ostream& os) const
-{
- if constexpr (Configuration::isStatisticsBuild())
- {
- for (const auto& s : d_stats)
- {
- if (!options::statisticsExpert() && s.second->d_expert) continue;
- if (!options::statisticsUnset() && !s.second->hasValue()) continue;
- os << s.first << " = " << *s.second << std::endl;
- }
- }
-}
-
-void StatisticsRegistry::printSafe(int fd) const
-{
- if constexpr (Configuration::isStatisticsBuild())
- {
- for (const auto& s : d_stats)
- {
- if (!options::statisticsExpert() && s.second->d_expert) continue;
- if (!options::statisticsUnset() && !s.second->hasValue()) continue;
-
- safe_print(fd, s.first);
- safe_print(fd, " = ");
- if (s.second->hasValue())
- s.second->printSafe(fd);
- else
- safe_print(fd, "<unset>");
- safe_print(fd, '\n');
- }
- }
-}
-void StatisticsRegistry::printDiff(std::ostream& os) const
-{
- if constexpr (Configuration::isStatisticsBuild())
- {
- if (!d_lastSnapshot)
- {
- // we have no snapshot, print as usual
- print(os);
- return;
- }
- for (const auto& s : d_stats)
- {
- if (!options::statisticsExpert() && s.second->d_expert) continue;
- if (!options::statisticsUnset() && !s.second->hasValue()) continue;
- auto oldit = d_lastSnapshot->find(s.first);
- if (oldit == d_lastSnapshot->end())
- {
- // not present in the snapshot
- os << s.first << " = " << *s.second << " (was <unset>)" << std::endl;
- }
- else if (oldit->second != s.second->getViewer())
- {
- // present in the snapshow, print old value
- os << s.first << " = " << *s.second << " (was ";
- detail::print(os, oldit->second);
- os << ")" << std::endl;
- }
- }
- }
-}
-
-std::ostream& operator<<(std::ostream& os, const StatisticsRegistry& sr)
-{
- sr.print(os);
- return os;
-}
-
-} // namespace cvc5
+++ /dev/null
-/******************************************************************************
- * Top contributors (to current version):
- * Gereon Kremer
- *
- * This file is part of the cvc5 project.
- *
- * Copyright (c) 2009-2021 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.
- * ****************************************************************************
- *
- * Central statistics registry.
- *
- * The StatisticsRegistry that issues statistic proxy objects.
- */
-
-#include "cvc5_private_library.h"
-
-#ifndef CVC5__UTIL__STATISTICS_REG_H
-#define CVC5__UTIL__STATISTICS_REG_H
-
-#include <iostream>
-#include <map>
-#include <memory>
-#include <typeinfo>
-
-#include "base/check.h"
-#include "util/statistics_stats.h"
-#include "util/statistics_value.h"
-
-namespace cvc5 {
-
-struct StatisticBaseValue;
-
-/**
- * The central registry for statistics.
- * Internally stores statistic data objects and issues corresponding proxy
- * objects to modules that want to expose statistics.
- * Provides registration methods (e.g. `registerAverage` or
- * `registerHistogram<T>`) that return the proxy object.
- * The different statistics are explained in more detail in statistics_stats.h
- *
- * Every statistic is identified by a name. If a statistic with the given
- * name is already registered, the registry issues another proxy object
- * for that name using the same data it already holds for this name.
- * While this makes perfect sense for most statistic types, it may lead to
- * unexpected (though not undefined) behaviour for others. For a reference
- * statistic, for example, the internal data will simply point to the object
- * registered last.
- * Note that the type of the re-registered statistic must always match
- * the type of the previously registered statistic with the same name.
- *
- * We generally distinguish between public (non-expert) and private (expert)
- * statistics. By default, `--stats` only shows public statistics. Private
- * ones are printed as well if `--all-statistics` is set.
- * All registration methods have a trailing argument `expert`, defaulting to
- * true.
- *
- * If statistics are disabled entirely (i.e. the cmake option
- * `ENABLE_STATISTICS` is not set), the registry still issues proxy objects
- * that can be used normally.
- * However, no data is stored in the registry and the modification functions
- * of the proxy objects do nothing.
- */
-class StatisticsRegistry
-{
- public:
- friend std::ostream& operator<<(std::ostream& os,
- const StatisticsRegistry& sr);
-
- using Snapshot = std::map<std::string, StatExportData>;
-
- /**
- * If `registerPublic` is true, all statistics that are public are
- * pre-registered as such. This argument mostly exists so that unit tests
- * can disable this pre-registration.
- */
- StatisticsRegistry(bool registerPublic = true);
-
- /** Register a new running average statistic for `name` */
-
- AverageStat registerAverage(const std::string& name, bool expert = true);
- /** Register a new histogram statistic for `name` */
- template <typename T>
- HistogramStat<T> registerHistogram(const std::string& name,
- bool expert = true)
- {
- return registerStat<HistogramStat<T>>(name, expert);
- }
-
- /** Register a new integer statistic for `name` */
- IntStat registerInt(const std::string& name, bool expert = true);
-
- /** Register a new reference statistic for `name` */
- template <typename T>
- ReferenceStat<T> registerReference(const std::string& name,
- bool expert = true)
- {
- return registerStat<ReferenceStat<T>>(name, expert);
- }
- /**
- * Register a new reference statistic for `name` and initialize it to
- * refer to `t`.
- */
- template <typename T>
- ReferenceStat<T> registerReference(const std::string& name,
- const T& t,
- bool expert = true)
- {
- ReferenceStat<T> res = registerStat<ReferenceStat<T>>(name, expert);
- res.set(t);
- return res;
- }
-
- /**
- * Register a new container size statistic for `name` and initialize it
- * to refer to `t`.
- */
- template <typename T>
- SizeStat<T> registerSize(const std::string& name,
- const T& t,
- bool expert = true)
- {
- SizeStat<T> res = registerStat<SizeStat<T>>(name, expert);
- res.set(t);
- return res;
- }
-
- /** Register a new timer statistic for `name` */
- TimerStat registerTimer(const std::string& name, bool expert = true);
-
- /** Register a new value statistic for `name`. */
- template <typename T>
- ValueStat<T> registerValue(const std::string& name, bool expert = true)
- {
- return registerStat<ValueStat<T>>(name, expert);
- }
-
- /** Register a new value statistic for `name` and set it to `init`. */
- template <typename T>
- ValueStat<T> registerValue(const std::string& name,
- const T& init,
- bool expert = true)
- {
- ValueStat<T> res = registerStat<ValueStat<T>>(name, expert);
- res.set(init);
- return res;
- }
-
- /** begin iteration */
- auto begin() const { return d_stats.begin(); }
- /** end iteration */
- auto end() const { return d_stats.end(); }
-
- /**
- * Store the current state of the statistics to allow for printing a diff
- * using `printDiff`.
- */
- void storeSnapshot();
-
- /**
- * Obtain a single statistic by name. Returns nullptr if no statistic has
- * been registered for this name.
- */
- StatisticBaseValue* get(const std::string& name) const;
-
- /**
- * Print all statistics to the given output stream.
- */
- void print(std::ostream& os) const;
- /**
- * Print all statistics in a safe manner to the given file descriptor.
- */
- void printSafe(int fd) const;
- /**
- * Print all statistics as a diff to the last snapshot that was stored by
- * calling `storeSnapshot`.
- */
- void printDiff(std::ostream& os) const;
-
- private:
- /**
- * Helper method to register a new statistic.
- * If the name was already used, a new proxy object is created.
- * We check whether the type matches the type of the originally registered
- * statistic using `typeid`.
- */
- template <typename Stat>
- Stat registerStat(const std::string& name, bool expert)
- {
- if constexpr (Configuration::isStatisticsBuild())
- {
- auto it = d_stats.find(name);
- if (it == d_stats.end())
- {
- it = d_stats.emplace(name, std::make_unique<typename Stat::stat_type>())
- .first;
- it->second->d_expert = expert;
- }
- auto* ptr = it->second.get();
- Assert(typeid(*ptr) == typeid(typename Stat::stat_type))
- << "Statistic value " << name
- << " was registered again with a different type.";
- it->second->d_expert = it->second->d_expert && expert;
- return Stat(static_cast<typename Stat::stat_type*>(ptr));
- }
- return Stat(nullptr);
- }
-
- /**
- * Holds (and owns) all statistic values, indexed by the name they were
- * registered for.
- */
- std::map<std::string, std::unique_ptr<StatisticBaseValue>> d_stats;
-
- /**
- * Holds a snapshot of the statistic values as StatExportData.
- * The current state can be saved to this snapshot using `storeSnapshot`,
- * which is then used in the next call to `printDiff`, but the data is not
- * exposed otherwise.
- * As this snapshot is only used by `printDiff`, which honors the relevant
- * options `--stats-expert` and `--stats-unset`, the snapshot is populated
- * by `storeSnapshot` to contain only those values that would be printed.
- */
- std::unique_ptr<Snapshot> d_lastSnapshot;
-};
-
-/** Calls `sr.print(os)`. */
-std::ostream& operator<<(std::ostream& os, const StatisticsRegistry& sr);
-
-} // namespace cvc5
-
-#endif
/******************************************************************************
* Top contributors (to current version):
- * Tim King, Morgan Deters, Mathias Preiner
+ * Gereon Kremer
*
* This file is part of the cvc5 project.
*
* directory for licensing information.
* ****************************************************************************
*
- * Statistics utility classes
+ * Central statistics registry.
+ *
+ * The StatisticsRegistry that issues statistic proxy objects.
*/
#include "util/statistics_registry.h"
-#include <cstdlib>
-#include <iostream>
-
-#include "base/check.h"
-#include "lib/clock_gettime.h"
-#include "util/ostream_util.h"
-
-#ifdef CVC5_STATISTICS_ON
-#define CVC5_USE_STATISTICS true
-#else
-#define CVC5_USE_STATISTICS false
-#endif
+#include "options/base_options.h"
+#include "util/statistics_public.h"
-
-/****************************************************************************/
-/* Some utility functions for timespec */
-/****************************************************************************/
namespace cvc5 {
-void StatisticsRegistry::registerStat(Stat* s)
+StatisticsRegistry::StatisticsRegistry(bool registerPublic)
{
-#ifdef CVC5_STATISTICS_ON
- PrettyCheckArgument(
- d_stats.find(s) == d_stats.end(),
- s,
- "Statistic `%s' is already registered with this registry.",
- s->getName().c_str());
- d_stats.insert(s);
-#endif /* CVC5_STATISTICS_ON */
-}/* StatisticsRegistry::registerStat_() */
+ if (registerPublic)
+ {
+ registerPublicStatistics(*this);
+ }
+}
-void StatisticsRegistry::unregisterStat(Stat* s)
+AverageStat StatisticsRegistry::registerAverage(const std::string& name,
+ bool expert)
+{
+ return registerStat<AverageStat>(name, expert);
+}
+IntStat StatisticsRegistry::registerInt(const std::string& name, bool expert)
+{
+ return registerStat<IntStat>(name, expert);
+}
+TimerStat StatisticsRegistry::registerTimer(const std::string& name,
+ bool expert)
{
-#ifdef CVC5_STATISTICS_ON
- AlwaysAssert(s != nullptr);
- AlwaysAssert(d_stats.erase(s) > 0)
- << "Statistic `" << s->getName()
- << "' was not registered with this registry.";
-#endif /* CVC5_STATISTICS_ON */
-} /* StatisticsRegistry::unregisterStat() */
+ return registerStat<TimerStat>(name, expert);
+}
-void StatisticsRegistry::flushStat(std::ostream &out) const {
-#ifdef CVC5_STATISTICS_ON
- flushInformation(out);
-#endif /* CVC5_STATISTICS_ON */
+void StatisticsRegistry::storeSnapshot()
+{
+ if constexpr (Configuration::isStatisticsBuild())
+ {
+ d_lastSnapshot = std::make_unique<Snapshot>();
+ for (const auto& s : d_stats)
+ {
+ if (!options::statisticsExpert() && s.second->d_expert) continue;
+ if (!options::statisticsAll() && s.second->isDefault()) continue;
+ d_lastSnapshot->emplace(
+ s.first,
+ s.second->getViewer());
+ }
+ }
}
-void StatisticsRegistry::flushInformation(std::ostream &out) const {
-#ifdef CVC5_STATISTICS_ON
- this->StatisticsBase::flushInformation(out);
-#endif /* CVC5_STATISTICS_ON */
+StatisticBaseValue* StatisticsRegistry::get(const std::string& name) const
+{
+ if constexpr (Configuration::isStatisticsBuild())
+ {
+ auto it = d_stats.find(name);
+ if (it == d_stats.end()) return nullptr;
+ return it->second.get();
+ }
+ return nullptr;
}
-void StatisticsRegistry::safeFlushInformation(int fd) const {
-#ifdef CVC5_STATISTICS_ON
- this->StatisticsBase::safeFlushInformation(fd);
-#endif /* CVC5_STATISTICS_ON */
+void StatisticsRegistry::print(std::ostream& os) const
+{
+ if constexpr (Configuration::isStatisticsBuild())
+ {
+ for (const auto& s : d_stats)
+ {
+ if (!options::statisticsExpert() && s.second->d_expert) continue;
+ if (!options::statisticsAll() && s.second->isDefault()) continue;
+ os << s.first << " = " << *s.second << std::endl;
+ }
+ }
}
-RegisterStatistic::RegisterStatistic(StatisticsRegistry* reg, Stat* stat)
- : d_reg(reg),
- d_stat(stat) {
- CheckArgument(reg != NULL, reg,
- "You need to specify a statistics registry"
- "on which to set the statistic");
- d_reg->registerStat(d_stat);
+void StatisticsRegistry::printSafe(int fd) const
+{
+ if constexpr (Configuration::isStatisticsBuild())
+ {
+ for (const auto& s : d_stats)
+ {
+ if (!options::statisticsExpert() && s.second->d_expert) continue;
+ if (!options::statisticsAll() && s.second->isDefault()) continue;
+
+ safe_print(fd, s.first);
+ safe_print(fd, " = ");
+ s.second->printSafe(fd);
+ safe_print(fd, '\n');
+ }
+ }
+}
+void StatisticsRegistry::printDiff(std::ostream& os) const
+{
+ if constexpr (Configuration::isStatisticsBuild())
+ {
+ if (!d_lastSnapshot)
+ {
+ // we have no snapshot, print as usual
+ print(os);
+ return;
+ }
+ for (const auto& s : d_stats)
+ {
+ if (!options::statisticsExpert() && s.second->d_expert) continue;
+ if (!options::statisticsAll() && s.second->isDefault())
+ {
+ auto oldit = d_lastSnapshot->find(s.first);
+ if (oldit != d_lastSnapshot->end() && oldit->second != s.second->getViewer())
+ {
+ // present in the snapshot, now defaulted
+ os << s.first << " = " << *s.second << " (was ";
+ detail::print(os, oldit->second);
+ os << ")" << std::endl;
+ }
+ }
+ else
+ {
+ auto oldit = d_lastSnapshot->find(s.first);
+ if (oldit == d_lastSnapshot->end())
+ {
+ // not present in the snapshot
+ os << s.first << " = " << *s.second << " (was <default>)"
+ << std::endl;
+ }
+ else if (oldit->second != s.second->getViewer())
+ {
+ // present in the snapshot, print old value
+ os << s.first << " = " << *s.second << " (was ";
+ detail::print(os, oldit->second);
+ os << ")" << std::endl;
+ }
+ }
+ }
+ }
}
-RegisterStatistic::~RegisterStatistic() {
- d_reg->unregisterStat(d_stat);
+std::ostream& operator<<(std::ostream& os, const StatisticsRegistry& sr)
+{
+ sr.print(os);
+ return os;
}
} // namespace cvc5
/******************************************************************************
* Top contributors (to current version):
- * Morgan Deters, Gereon Kremer, Tim King
+ * Gereon Kremer
*
* This file is part of the cvc5 project.
*
* directory for licensing information.
* ****************************************************************************
*
- * Statistics utility classes
- *
- * Statistics utility classes, including classes for holding (and referring
- * to) statistics, the statistics registry, and some other associated
- * classes.
- *
- * This file is somewhat unique in that it is a "cvc5_private_library.h"
- * header. Because of this, most classes need to be marked as CVC4_EXPORT.
- * This is because CVC4_EXPORT is connected to the visibility of the linkage
- * in the object files for the class. It does not dictate what headers are
- * installed.
- * Because the StatisticsRegistry and associated classes are built into
- * libutil, which is used by libcvc4, and then later used by the libmain
- * without referring to libutil as well. Thus the without marking these as
- * CVC4_EXPORT the symbols would be external in libutil, internal in libcvc4,
- * and not be visible to libmain and linking would fail.
- * You can debug this using "nm" on the .so and .o files in the builds/
- * directory. See
- * http://eli.thegreenplace.net/2013/07/09/library-order-in-static-linking
- * for a longer discussion on symbol visibility.
+ * Central statistics registry.
+ *
+ * The StatisticsRegistry that issues statistic proxy objects.
*/
/**
#ifndef CVC5__STATISTICS_REGISTRY_H
#define CVC5__STATISTICS_REGISTRY_H
-#include <ctime>
-#include <iomanip>
+#include <iostream>
#include <map>
-#include <sstream>
-#include <vector>
-
-#ifdef CVC5_STATISTICS_ON
-#define CVC5_USE_STATISTICS true
-#else
-#define CVC5_USE_STATISTICS false
-#endif
+#include <memory>
+#include <typeinfo>
-#include "base/exception.h"
-#include "cvc4_export.h"
-#include "util/safe_print.h"
-#include "util/statistics.h"
-#include "util/stats_base.h"
+#include "base/check.h"
+#include "util/statistics_stats.h"
+#include "util/statistics_value.h"
namespace cvc5 {
-/** A statistic that contains a SExpr. */
-class SExprStat : public Stat {
-private:
- SExpr d_data;
+struct StatisticBaseValue;
-public:
+/**
+ * The central registry for statistics.
+ * Internally stores statistic data objects and issues corresponding proxy
+ * objects to modules that want to expose statistics.
+ * Provides registration methods (e.g. `registerAverage` or
+ * `registerHistogram<T>`) that return the proxy object.
+ * The different statistics are explained in more detail in statistics_stats.h
+ *
+ * Every statistic is identified by a name. If a statistic with the given
+ * name is already registered, the registry issues another proxy object
+ * for that name using the same data it already holds for this name.
+ * While this makes perfect sense for most statistic types, it may lead to
+ * unexpected (though not undefined) behaviour for others. For a reference
+ * statistic, for example, the internal data will simply point to the object
+ * registered last.
+ * Note that the type of the re-registered statistic must always match
+ * the type of the previously registered statistic with the same name.
+ *
+ * We generally distinguish between public (non-expert) and private (expert)
+ * statistics. By default, `--stats` only shows public statistics. Private
+ * ones are printed as well if `--all-statistics` is set.
+ * All registration methods have a trailing argument `expert`, defaulting to
+ * true.
+ *
+ * If statistics are disabled entirely (i.e. the cmake option
+ * `ENABLE_STATISTICS` is not set), the registry still issues proxy objects
+ * that can be used normally.
+ * However, no data is stored in the registry and the modification functions
+ * of the proxy objects do nothing.
+ */
+class StatisticsRegistry
+{
+ public:
+ friend std::ostream& operator<<(std::ostream& os,
+ const StatisticsRegistry& sr);
+
+ using Snapshot = std::map<std::string, StatExportData>;
/**
- * Construct a SExpr-valued statistic with the given name and
- * initial value.
+ * If `registerPublic` is true, all statistics that are public are
+ * pre-registered as such. This argument mostly exists so that unit tests
+ * can disable this pre-registration.
*/
- SExprStat(const std::string& name, const SExpr& init) :
- Stat(name), d_data(init){}
+ StatisticsRegistry(bool registerPublic = true);
- void flushInformation(std::ostream& out) const override
+ /** Register a new running average statistic for `name` */
+
+ AverageStat registerAverage(const std::string& name, bool expert = true);
+ /** Register a new histogram statistic for `name` */
+ template <typename T>
+ HistogramStat<T> registerHistogram(const std::string& name,
+ bool expert = true)
{
- out << d_data;
+ return registerStat<HistogramStat<T>>(name, expert);
}
- void safeFlushInformation(int fd) const override
+ /** Register a new integer statistic for `name` */
+ IntStat registerInt(const std::string& name, bool expert = true);
+
+ /** Register a new reference statistic for `name` */
+ template <typename T>
+ ReferenceStat<T> registerReference(const std::string& name,
+ bool expert = true)
{
- // SExprStat is only used in statistics.cpp in copyFrom, which we cannot
- // do in a signal handler anyway.
- safe_print(fd, "<unsupported>");
+ return registerStat<ReferenceStat<T>>(name, expert);
+ }
+ /**
+ * Register a new reference statistic for `name` and initialize it to
+ * refer to `t`.
+ */
+ template <typename T>
+ ReferenceStat<T> registerReference(const std::string& name,
+ const T& t,
+ bool expert = true)
+ {
+ ReferenceStat<T> res = registerStat<ReferenceStat<T>>(name, expert);
+ res.set(t);
+ return res;
}
- SExpr getValue() const override { return d_data; }
-
-};/* class SExprStat */
+ /**
+ * Register a new container size statistic for `name` and initialize it
+ * to refer to `t`.
+ */
+ template <typename T>
+ SizeStat<T> registerSize(const std::string& name,
+ const T& t,
+ bool expert = true)
+ {
+ SizeStat<T> res = registerStat<SizeStat<T>>(name, expert);
+ res.set(t);
+ return res;
+ }
-/****************************************************************************/
-/* Statistics Registry */
-/****************************************************************************/
+ /** Register a new timer statistic for `name` */
+ TimerStat registerTimer(const std::string& name, bool expert = true);
-/**
- * The main statistics registry. This registry maintains the list of
- * currently active statistics and is able to "flush" them all.
- */
-class CVC4_EXPORT StatisticsRegistry : public StatisticsBase
-{
- private:
- /** Private copy constructor undefined (no copy permitted). */
- StatisticsRegistry(const StatisticsRegistry&) = delete;
+ /** Register a new value statistic for `name`. */
+ template <typename T>
+ ValueStat<T> registerValue(const std::string& name, bool expert = true)
+ {
+ return registerStat<ValueStat<T>>(name, expert);
+ }
-public:
+ /** Register a new value statistic for `name` and set it to `init`. */
+ template <typename T>
+ ValueStat<T> registerValue(const std::string& name,
+ const T& init,
+ bool expert = true)
+ {
+ ValueStat<T> res = registerStat<ValueStat<T>>(name, expert);
+ res.set(init);
+ return res;
+ }
- /** Construct an nameless statistics registry */
- StatisticsRegistry() {}
+ /** begin iteration */
+ auto begin() const { return d_stats.begin(); }
+ /** end iteration */
+ auto end() const { return d_stats.end(); }
- void flushStat(std::ostream& out) const;
+ /**
+ * Obtain the current state of all statistics.
+ */
+ void storeSnapshot();
- void flushInformation(std::ostream& out) const;
+ /**
+ * Obtain a single statistic by name. Returns nullptr if no statistic has
+ * been registered for this name.
+ */
+ StatisticBaseValue* get(const std::string& name) const;
- void safeFlushInformation(int fd) const;
+ /**
+ * Print all statistics to the given output stream.
+ */
+ void print(std::ostream& os) const;
+ /**
+ * Print all statistics in a safe manner to the given file descriptor.
+ */
+ void printSafe(int fd) const;
+ /**
+ * Print all statistics as a diff to the last stored snapshot.
+ */
+ void printDiff(std::ostream& os) const;
- SExpr getValue() const
+ private:
+ /**
+ * Helper method to register a new statistic.
+ * If the name was already used, a new proxy object is created.
+ * We check whether the type matches the type of the originally registered
+ * statistic using `typeid`.
+ */
+ template <typename Stat>
+ Stat registerStat(const std::string& name, bool expert)
{
- std::vector<SExpr> v;
- for(StatSet::iterator i = d_stats.begin(); i != d_stats.end(); ++i) {
- std::vector<SExpr> w;
- w.push_back(SExpr((*i)->getName()));
- w.push_back((*i)->getValue());
- v.push_back(SExpr(w));
+ if constexpr (Configuration::isStatisticsBuild())
+ {
+ auto it = d_stats.find(name);
+ if (it == d_stats.end())
+ {
+ it = d_stats.emplace(name, std::make_unique<typename Stat::stat_type>())
+ .first;
+ it->second->d_expert = expert;
+ }
+ auto* ptr = it->second.get();
+ Assert(typeid(*ptr) == typeid(typename Stat::stat_type))
+ << "Statistic value " << name
+ << " was registered again with a different type.";
+ it->second->d_expert = it->second->d_expert && expert;
+ return Stat(static_cast<typename Stat::stat_type*>(ptr));
}
- return SExpr(v);
+ return Stat(nullptr);
}
- /** Register a new statistic */
- void registerStat(Stat* s);
-
- /** Unregister a new statistic */
- void unregisterStat(Stat* s);
-
-}; /* class StatisticsRegistry */
-
-/**
- * Resource-acquisition-is-initialization idiom for statistics
- * registry. Useful for stack-based statistics (like in the driver).
- * This RAII class only does registration and unregistration.
- */
-class CVC4_EXPORT RegisterStatistic
-{
- public:
- RegisterStatistic(StatisticsRegistry* reg, Stat* stat);
- ~RegisterStatistic();
+ /**
+ * Holds (and owns) all statistic values, indexed by the name they were
+ * registered for.
+ */
+ std::map<std::string, std::unique_ptr<StatisticBaseValue>> d_stats;
-private:
- StatisticsRegistry* d_reg;
- Stat* d_stat;
+ std::unique_ptr<Snapshot> d_lastSnapshot;
+};
-}; /* class RegisterStatistic */
+/** Calls `sr.print(os)`. */
+std::ostream& operator<<(std::ostream& os, const StatisticsRegistry& sr);
} // namespace cvc5
std::ostream& print(std::ostream& out, const StatExportData& sed)
{
std::visit(overloaded{
- [&out](std::monostate v) { out << "<unset>"; },
[&out](int64_t v) { out << v; },
[&out](uint64_t v) { out << v; },
[&out](double v) { out << v; },
std::ostream& operator<<(std::ostream& out, const StatisticBaseValue& sbv)
{
- return detail::print(out, sbv.hasValue() ? sbv.getViewer() : StatExportData{});
+ return detail::print(out, sbv.getViewer());
}
StatExportData StatisticAverageValue::getViewer() const { return get(); }
-bool StatisticAverageValue::hasValue() const { return d_count > 0; }
-
-void StatisticAverageValue::print(std::ostream& out) const { out << get(); }
+bool StatisticAverageValue::isDefault() const { return d_count == 0; }
void StatisticAverageValue::printSafe(int fd) const
{
StatExportData StatisticTimerValue::getViewer() const
{
- return static_cast<int64_t>(get() / std::chrono::milliseconds(1));
+ return std::to_string(get()) + "ms";
}
-bool StatisticTimerValue::hasValue() const
+bool StatisticTimerValue::isDefault() const
{
- return d_running || d_duration.count() > 0;
-}
-
-void StatisticTimerValue::print(std::ostream& out) const
-{
- StreamFormatScope format_scope(out);
- duration dur = get();
-
- out << (dur / std::chrono::seconds(1)) << "." << std::setfill('0')
- << std::setw(9) << std::right << (dur % std::chrono::seconds(1)).count();
+ return !d_running && d_duration.count() == 0;
}
void StatisticTimerValue::printSafe(int fd) const
{
- duration dur = get();
- safe_print<uint64_t>(fd, dur / std::chrono::seconds(1));
- safe_print(fd, ".");
- safe_print_right_aligned(fd, (dur % std::chrono::seconds(1)).count(), 9);
+ safe_print<uint64_t>(fd, get());
+ safe_print<std::string>(fd, "ms");
}
/** Make sure that we include the time of a currently running timer */
-StatisticTimerValue::duration StatisticTimerValue::get() const
+uint64_t StatisticTimerValue::get() const
{
auto data = d_duration;
if (d_running)
{
data += clock::now() - d_start;
}
- return data;
+ return static_cast<int64_t>(data / std::chrono::milliseconds(1));
}
} // namespace cvc5
class StatisticsRegistry;
-using StatExportData = std::variant<std::monostate,
- int64_t,
- double,
- std::string,
- std::map<std::string, uint64_t>>;
+using StatExportData =
+ std::variant<int64_t, double, std::string, std::map<std::string, uint64_t>>;
namespace detail {
std::ostream& print(std::ostream& out, const StatExportData& sed);
}
struct StatisticBaseValue
{
virtual ~StatisticBaseValue();
- /** Checks whether the data holds a non-default value. */
- virtual bool hasValue() const = 0;
+ /** Checks whether the data holds the default value. */
+ virtual bool isDefault() const = 0;
/**
* Converts the internal data to an instance of `StatExportData` that is
* suitable for printing and exporting to the API.
- * Assumes that `hasValue` returns true. Otherwise, the return value should
- * assumed to be `std::monostate`.
*/
virtual StatExportData getViewer() const = 0;
- /**
- * Writes the data to a regular `std::ostream`.
- * Assumes that `hasValue` returns true. Otherwise, the user should write
- * `<undef>` to the stream.
- */
- virtual void print(std::ostream&) const = 0;
/**
* Safely writes the data to a file descriptor. Is suitable to be used
* within a signal handler.
- * Assumes that `hasValue` returns true. Otherwise, the user should write
- * `<undef>` to the file descriptor.
*/
virtual void printSafe(int fd) const = 0;
struct StatisticAverageValue : StatisticBaseValue
{
StatExportData getViewer() const override;
- bool hasValue() const override;
- void print(std::ostream& out) const override;
+ bool isDefault() const override;
void printSafe(int fd) const override;
double get() const;
struct StatisticBackedValue : StatisticBaseValue
{
StatExportData getViewer() const override { return d_value; }
- bool hasValue() const override { return d_value != T(); }
- void print(std::ostream& out) const override { out << d_value; }
+ bool isDefault() const override { return d_value == T(); }
void printSafe(int fd) const override { safe_print<T>(fd, d_value); }
T d_value;
}
return res;
}
- bool hasValue() const override { return d_hist.size() > 0; }
- void print(std::ostream& out) const override
- {
- out << "[";
- bool first = true;
- for (size_t i = 0, n = d_hist.size(); i < n; ++i)
- {
- if (d_hist[i] > 0)
- {
- if (first)
- {
- first = false;
- }
- else
- {
- out << ", ";
- }
- out << "(" << static_cast<Integral>(i + d_offset) << " : " << d_hist[i]
- << ")";
- }
- }
- out << "]";
- }
+ bool isDefault() const override { return d_hist.size() == 0; }
void printSafe(int fd) const override
{
- safe_print(fd, "[");
+ safe_print(fd, "{ ");
bool first = true;
for (size_t i = 0, n = d_hist.size(); i < n; ++i)
{
}
safe_print(fd, "(");
safe_print<Integral>(fd, static_cast<Integral>(i + d_offset));
- safe_print(fd, " : ");
+ safe_print(fd, ": ");
safe_print<uint64_t>(fd, d_hist[i]);
safe_print(fd, ")");
}
}
- safe_print(fd, "]");
+ safe_print(fd, " }");
}
/**
return *d_value;
}
}
- return {};
+ if constexpr (std::is_integral_v<T>)
+ {
+ return static_cast<int64_t>(0);
+ }
+ else
+ {
+ // this else branch is required to ensure compilation.
+ // if T is unsigned int, this return statement triggers a compiler error
+ return T();
+ }
}
- bool hasValue() const override { return d_committed || d_value != nullptr; }
- void print(std::ostream& out) const override
+ bool isDefault() const override
{
if (d_committed)
{
- out << *d_committed;
- }
- else if (d_value != nullptr)
- {
- out << *d_value;
+ return *d_committed == T();
}
+ return d_value == nullptr || *d_value == T();
}
void printSafe(int fd) const override
{
{
safe_print<T>(fd, *d_value);
}
+ else
+ {
+ safe_print<T>(fd, T());
+ }
}
void commit()
{
{
return static_cast<int64_t>(d_value->size());
}
- return {};
+ return static_cast<int64_t>(0);
}
- bool hasValue() const override { return d_committed || d_value != nullptr; }
- void print(std::ostream& out) const override
+ bool isDefault() const override
{
if (d_committed)
{
- out << *d_committed;
- }
- else if (d_value != nullptr)
- {
- out << d_value->size();
+ return *d_committed == 0;
}
+ return d_value == nullptr || d_value->size() == 0;
}
void printSafe(int fd) const override
{
{
safe_print(fd, d_value->size());
}
+ else
+ {
+ safe_print(fd, 0);
+ }
}
void commit()
{
};
/** Returns the number of milliseconds */
StatExportData getViewer() const override;
- bool hasValue() const override;
- /** Prints seconds in fixed-point format */
- void print(std::ostream& out) const override;
+ bool isDefault() const override;
/** Prints seconds in fixed-point format */
void printSafe(int fd) const override;
- /** Make sure that we include the time of a currently running timer */
- duration get() const;
+ /**
+ * Returns the elapsed time in milliseconds.
+ * Make sure that we include the time of a currently running timer
+ */
+ uint64_t get() const;
/**
* The cumulative duration of the timer so far.
+++ /dev/null
-/******************************************************************************
- * Top contributors (to current version):
- * Gereon Kremer, Tim King, Morgan Deters
- *
- * This file is part of the cvc5 project.
- *
- * Copyright (c) 2009-2021 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.
- * ****************************************************************************
- *
- * Base statistic classes.
- */
-
-#include "util/stats_base.h"
-
-#include "util/statistics_registry.h"
-
-namespace cvc5 {
-
-Stat::Stat(const std::string& name) : d_name(name)
-{
- if (CVC5_USE_STATISTICS)
- {
- CheckArgument(d_name.find(", ") == std::string::npos,
- name,
- "Statistics names cannot include a comma (',')");
- }
-}
-
-IntStat::IntStat(const std::string& name, int64_t init)
- : BackedStat<int64_t>(name, init)
-{
-}
-
-/** Increment the underlying integer statistic. */
-IntStat& IntStat::operator++()
-{
- if (CVC5_USE_STATISTICS)
- {
- ++d_data;
- }
- return *this;
-}
-/** Increment the underlying integer statistic. */
-IntStat& IntStat::operator++(int)
-{
- if (CVC5_USE_STATISTICS)
- {
- ++d_data;
- }
- return *this;
-}
-
-/** Increment the underlying integer statistic by the given amount. */
-IntStat& IntStat::operator+=(int64_t val)
-{
- if (CVC5_USE_STATISTICS)
- {
- d_data += val;
- }
- return *this;
-}
-
-/** Keep the maximum of the current statistic value and the given one. */
-void IntStat::maxAssign(int64_t val)
-{
- if (CVC5_USE_STATISTICS)
- {
- if (d_data < val)
- {
- d_data = val;
- }
- }
-}
-
-/** Keep the minimum of the current statistic value and the given one. */
-void IntStat::minAssign(int64_t val)
-{
- if (CVC5_USE_STATISTICS)
- {
- if (d_data > val)
- {
- d_data = val;
- }
- }
-}
-
-AverageStat::AverageStat(const std::string& name)
- : BackedStat<double>(name, 0.0)
-{
-}
-
-/** Add an entry to the running-average calculation. */
-AverageStat& AverageStat::operator<<(double e)
-{
- if (CVC5_USE_STATISTICS)
- {
- ++d_count;
- d_sum += e;
- set(d_sum / d_count);
- }
- return *this;
-}
-
-SExpr AverageStat::getValue() const
-{
- std::stringstream ss;
- ss << std::fixed << std::setprecision(8) << d_data;
- return SExpr(Rational::fromDecimal(ss.str()));
-}
-
-} // namespace cvc5
+++ /dev/null
-/******************************************************************************
- * Top contributors (to current version):
- * Gereon Kremer, Morgan Deters, Tim King
- *
- * This file is part of the cvc5 project.
- *
- * Copyright (c) 2009-2021 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.
- * ****************************************************************************
- *
- * Base statistic classes.
- */
-
-#include "cvc5_private_library.h"
-
-#ifndef CVC5__UTIL__STATS_BASE_H
-#define CVC5__UTIL__STATS_BASE_H
-
-#include <iomanip>
-#include <sstream>
-#include <string>
-
-#include "cvc4_export.h"
-#include "util/safe_print.h"
-#include "util/sexpr.h"
-#include "util/stats_utils.h"
-
-#ifdef CVC5_STATISTICS_ON
-#define CVC5_USE_STATISTICS true
-#else
-#define CVC5_USE_STATISTICS false
-#endif
-
-namespace cvc5 {
-
-/**
- * The base class for all statistics.
- *
- * This base class keeps the name of the statistic and declares the (pure)
- * virtual functions flushInformation() and safeFlushInformation().
- * Derived classes must implement these function and pass their name to
- * the base class constructor.
- */
-class CVC4_EXPORT Stat
-{
- public:
- /**
- * Construct a statistic with the given name. Debug builds of CVC4
- * will throw an assertion exception if the given name contains the
- * statistic delimiter string.
- */
- Stat(const std::string& name);
-
- /** Destruct a statistic. This base-class version does nothing. */
- virtual ~Stat() = default;
-
- /**
- * Flush the value of this statistic to an output stream. Should
- * finish the output with an end-of-line character.
- */
- virtual void flushInformation(std::ostream& out) const = 0;
-
- /**
- * Flush the value of this statistic to a file descriptor. Should finish the
- * output with an end-of-line character. Should be safe to use in a signal
- * handler.
- */
- virtual void safeFlushInformation(int fd) const = 0;
-
- /** Get the name of this statistic. */
- const std::string& getName() const { return d_name; }
-
- /** Get the value of this statistic as a string. */
- virtual SExpr getValue() const
- {
- std::stringstream ss;
- flushInformation(ss);
- return SExpr(ss.str());
- }
-
- protected:
- /** The name of this statistic */
- std::string d_name;
-}; /* class Stat */
-
-/**
- * A data statistic that keeps a T and sets it with setData().
- *
- * Template class T must have an operator=() and a copy constructor.
- */
-template <class T>
-class BackedStat : public Stat
-{
- public:
- /** Construct a backed statistic with the given name and initial value. */
- BackedStat(const std::string& name, const T& init) : Stat(name), d_data(init)
- {
- }
-
- /** Set the underlying data value to the given value. */
- void set(const T& t)
- {
- if (CVC5_USE_STATISTICS)
- {
- d_data = t;
- }
- }
-
- const T& get() const { return d_data; }
-
- /** Flush the value of the statistic to the given output stream. */
- virtual void flushInformation(std::ostream& out) const override
- {
- out << d_data;
- }
-
- virtual void safeFlushInformation(int fd) const override
- {
- safe_print<T>(fd, d_data);
- }
-
- protected:
- /** The internally-kept statistic value */
- T d_data;
-}; /* class BackedStat<T> */
-
-/**
- * A data statistic that references a data cell of type T,
- * implementing get() by referencing that memory cell, and
- * setData() by reassigning the statistic to point to the new
- * data cell. The referenced data cell is kept as a const
- * reference, meaning the referenced data is never actually
- * modified by this class (it must be externally modified for
- * a reference statistic to make sense). A common use for
- * this type of statistic is to output a statistic that is kept
- * outside the statistics package (for example, one that's kept
- * by a theory implementation for internal heuristic purposes,
- * which is important to keep even if statistics are turned off).
- *
- * Template class T must have an assignment operator=().
- */
-template <class T>
-class ReferenceStat : public Stat
-{
- public:
- /**
- * Construct a reference stat with the given name and a reference
- * to nullptr.
- */
- ReferenceStat(const std::string& name) : Stat(name) {}
-
- /**
- * Construct a reference stat with the given name and a reference to
- * the given data.
- */
- ReferenceStat(const std::string& name, const T& data) : Stat(name)
- {
- set(data);
- }
-
- /** Set this reference statistic to refer to the given data cell. */
- void set(const T& t)
- {
- if (CVC5_USE_STATISTICS)
- {
- d_data = &t;
- }
- }
- const T& get() const { return *d_data; }
-
- /** Flush the value of the statistic to the given output stream. */
- virtual void flushInformation(std::ostream& out) const override
- {
- out << *d_data;
- }
-
- virtual void safeFlushInformation(int fd) const override
- {
- safe_print<T>(fd, *d_data);
- }
-
- private:
- /** The referenced data cell */
- const T* d_data = nullptr;
-}; /* class ReferenceStat<T> */
-
-/**
- * A backed integer-valued (64-bit signed) statistic.
- * This doesn't functionally differ from its base class BackedStat<int64_t>,
- * except for adding convenience functions for dealing with integers.
- */
-class IntStat : public BackedStat<int64_t>
-{
- public:
- /**
- * Construct an integer-valued statistic with the given name and
- * initial value.
- */
- IntStat(const std::string& name, int64_t init);
-
- /** Increment the underlying integer statistic. */
- IntStat& operator++();
- /** Increment the underlying integer statistic. */
- IntStat& operator++(int);
-
- /** Increment the underlying integer statistic by the given amount. */
- IntStat& operator+=(int64_t val);
-
- /** Keep the maximum of the current statistic value and the given one. */
- void maxAssign(int64_t val);
-
- /** Keep the minimum of the current statistic value and the given one. */
- void minAssign(int64_t val);
-
- SExpr getValue() const override { return SExpr(Integer(d_data)); }
-
-}; /* class IntStat */
-
-/**
- * The value for an AverageStat is the running average of (e1, e_2, ..., e_n),
- * (e1 + e_2 + ... + e_n)/n,
- * where e_i is an entry added by an addEntry(e_i) call.
- * The value is initially always 0.
- * (This is to avoid making parsers confused.)
- *
- * A call to setData() will change the running average but not reset the
- * running count, so should generally be avoided. Call addEntry() to add
- * an entry to the average calculation.
- */
-class AverageStat : public BackedStat<double>
-{
- public:
- /** Construct an average statistic with the given name. */
- AverageStat(const std::string& name);
-
- /** Add an entry to the running-average calculation. */
- AverageStat& operator<<(double e);
-
- SExpr getValue() const override;
-
- private:
- /**
- * The number of accumulations of the running average that we
- * have seen so far.
- */
- uint32_t d_count = 0;
- double d_sum = 0;
-}; /* class AverageStat */
-
-template <class T>
-class SizeStat : public Stat
-{
- public:
- SizeStat(const std::string& name, const T& sized) : Stat(name), d_sized(sized)
- {
- }
- ~SizeStat() {}
-
- /** Flush the value of the statistic to the given output stream. */
- void flushInformation(std::ostream& out) const override
- {
- out << d_sized.size();
- }
-
- void safeFlushInformation(int fd) const override
- {
- safe_print(fd, d_sized.size());
- }
-
- private:
- const T& d_sized;
-}; /* class SizeStat */
-
-} // namespace cvc5
-
-#endif
+++ /dev/null
-/******************************************************************************
- * Top contributors (to current version):
- * Gereon Kremer, Mathias Preiner, Tim King
- *
- * This file is part of the cvc5 project.
- *
- * Copyright (c) 2009-2021 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.
- * ****************************************************************************
- *
- * Histogram statistics.
- *
- * Stat classes that represent histograms.
- */
-
-#include "cvc5_private_library.h"
-
-#ifndef CVC5__UTIL__STATS_HISTOGRAM_H
-#define CVC5__UTIL__STATS_HISTOGRAM_H
-
-#include <map>
-#include <vector>
-
-#include "util/stats_base.h"
-
-namespace cvc5 {
-
-/**
- * A histogram statistic class for integral types.
- * Avoids using an std::map (like we would do for generic types) in favor of a
- * faster std::vector by casting the integral values to indices into the
- * vector. Requires the type to be an integral type that is convertible to
- * int64_t, also supporting appropriate enum types.
- * The vector is resized on demand to grow as necessary and supports negative
- * values as well.
- */
-template <typename Integral>
-class IntegralHistogramStat : public Stat
-{
- static_assert(std::is_integral<Integral>::value
- || std::is_enum<Integral>::value,
- "Type should be a fundamental integral type.");
-
- public:
- /** Construct a histogram of a stream of entries. */
- IntegralHistogramStat(const std::string& name) : Stat(name) {}
-
- void flushInformation(std::ostream& out) const override
- {
- out << "[";
- bool first = true;
- for (size_t i = 0, n = d_hist.size(); i < n; ++i)
- {
- if (d_hist[i] > 0)
- {
- if (first)
- {
- first = false;
- }
- else
- {
- out << ", ";
- }
- out << "(" << static_cast<Integral>(i + d_offset) << " : "
- << d_hist[i] << ")";
- }
- }
- out << "]";
- }
-
- void safeFlushInformation(int fd) const override
- {
- safe_print(fd, "[");
- bool first = true;
- for (size_t i = 0, n = d_hist.size(); i < n; ++i)
- {
- if (d_hist[i] > 0)
- {
- if (first)
- {
- first = false;
- }
- else
- {
- safe_print(fd, ", ");
- }
- safe_print(fd, "(");
- safe_print<Integral>(fd, static_cast<Integral>(i + d_offset));
- safe_print(fd, " : ");
- safe_print<uint64_t>(fd, d_hist[i]);
- safe_print(fd, ")");
- }
- }
- safe_print(fd, "]");
- }
-
- IntegralHistogramStat& operator<<(Integral val)
- {
- if (CVC5_USE_STATISTICS)
- {
- int64_t v = static_cast<int64_t>(val);
- if (d_hist.empty())
- {
- d_offset = v;
- }
- if (v < d_offset)
- {
- d_hist.insert(d_hist.begin(), d_offset - v, 0);
- d_offset = v;
- }
- if (static_cast<size_t>(v - d_offset) >= d_hist.size())
- {
- d_hist.resize(v - d_offset + 1);
- }
- d_hist[v - d_offset]++;
- }
- return (*this);
- }
-
- private:
- std::vector<uint64_t> d_hist;
- int64_t d_offset;
-}; /* class IntegralHistogramStat */
-
-} // namespace cvc5
-
-#endif
+++ /dev/null
-/******************************************************************************
- * Top contributors (to current version):
- * Gereon Kremer, Morgan Deters, Andres Noetzli
- *
- * This file is part of the cvc5 project.
- *
- * Copyright (c) 2009-2021 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.
- * ****************************************************************************
- *
- * Timer statistics.
- *
- * Stat classes that hold timers.
- */
-
-#include "util/stats_timer.h"
-
-#include <iostream>
-
-#include "base/check.h"
-#include "util/ostream_util.h"
-
-namespace cvc5 {
-
-template <>
-void safe_print(int fd, const timer_stat_detail::duration& t)
-{
- safe_print<uint64_t>(fd, t / std::chrono::seconds(1));
- safe_print(fd, ".");
- safe_print_right_aligned(fd, (t % std::chrono::seconds(1)).count(), 9);
-}
-
-void TimerStat::start()
-{
- if (CVC5_USE_STATISTICS)
- {
- PrettyCheckArgument(!d_running, *this, "timer already running");
- d_start = timer_stat_detail::clock::now();
- d_running = true;
- }
-}
-
-void TimerStat::stop()
-{
- if (CVC5_USE_STATISTICS)
- {
- AlwaysAssert(d_running) << "timer not running";
- d_data += timer_stat_detail::clock::now() - d_start;
- d_running = false;
- }
-}
-
-bool TimerStat::running() const { return d_running; }
-
-timer_stat_detail::duration TimerStat::get() const
-{
- auto data = d_data;
- if (CVC5_USE_STATISTICS && d_running)
- {
- data += timer_stat_detail::clock::now() - d_start;
- }
- return data;
-}
-
-SExpr TimerStat::getValue() const
-{
- auto data = d_data;
- if (CVC5_USE_STATISTICS && d_running)
- {
- data += timer_stat_detail::clock::now() - d_start;
- }
- std::stringstream ss;
- ss << std::fixed << std::setprecision(8) << data;
- return SExpr(Rational::fromDecimal(ss.str()));
-}
-
-void TimerStat::flushInformation(std::ostream& out) const { out << get(); }
-
-void TimerStat::safeFlushInformation(int fd) const
-{
- // Overwrite the implementation in the superclass because we cannot use
- // getDataRef(): it might return stale data if the timer is currently
- // running.
- safe_print<timer_stat_detail::duration>(fd, get());
-}
-
-CodeTimer::CodeTimer(TimerStat& timer, bool allow_reentrant)
- : d_timer(timer), d_reentrant(false)
-{
- if (!allow_reentrant || !(d_reentrant = d_timer.running()))
- {
- d_timer.start();
- }
-}
-CodeTimer::~CodeTimer()
-{
- if (!d_reentrant)
- {
- d_timer.stop();
- }
-}
-
-} // namespace cvc5
+++ /dev/null
-/******************************************************************************
- * Top contributors (to current version):
- * Morgan Deters, Gereon Kremer, Mathias Preiner
- *
- * This file is part of the cvc5 project.
- *
- * Copyright (c) 2009-2021 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.
- * ****************************************************************************
- *
- * Timer statistics.
- *
- * Stat classes that hold timers.
- */
-
-#include "cvc5_private_library.h"
-
-#ifndef CVC5__UTIL__STATS_TIMER_H
-#define CVC5__UTIL__STATS_TIMER_H
-
-#include <chrono>
-
-#include "cvc4_export.h"
-#include "util/stats_base.h"
-
-namespace cvc5 {
-namespace timer_stat_detail {
-using clock = std::chrono::steady_clock;
-using time_point = clock::time_point;
-struct duration : public std::chrono::nanoseconds
-{
-};
-} // namespace timer_stat_detail
-
-template <>
-void CVC4_EXPORT safe_print(int fd, const timer_stat_detail::duration& t);
-
-class CodeTimer;
-
-/**
- * A timer statistic. The timer can be started and stopped
- * arbitrarily, like a stopwatch; the value of the statistic at the
- * end is the accumulated time over all (start,stop) pairs.
- */
-class CVC4_EXPORT TimerStat : public BackedStat<timer_stat_detail::duration>
-{
- public:
- typedef cvc5::CodeTimer CodeTimer;
-
- /**
- * Construct a timer statistic with the given name. Newly-constructed
- * timers have a 0.0 value and are not running.
- */
- TimerStat(const std::string& name)
- : BackedStat<timer_stat_detail::duration>(name,
- timer_stat_detail::duration()),
- d_start(),
- d_running(false)
- {
- }
-
- /** Start the timer. */
- void start();
-
- /**
- * Stop the timer and update the statistic value with the
- * accumulated time.
- */
- void stop();
-
- /** If the timer is currently running */
- bool running() const;
-
- timer_stat_detail::duration get() const;
-
- void flushInformation(std::ostream& out) const override;
- void safeFlushInformation(int fd) const override;
-
- SExpr getValue() const override;
-
- private:
- /** The last start time of this timer */
- timer_stat_detail::time_point d_start;
-
- /** Whether this timer is currently running */
- bool d_running;
-}; /* class TimerStat */
-
-/**
- * Utility class to make it easier to call stop() at the end of a
- * code block. When constructed, it starts the timer. When
- * destructed, it stops the timer.
- */
-class CodeTimer
-{
- public:
- CodeTimer(TimerStat& timer, bool allow_reentrant = false);
- ~CodeTimer();
-
-private:
- TimerStat& d_timer;
- bool d_reentrant;
-
- /** Private copy constructor undefined (no copy permitted). */
- CodeTimer(const CodeTimer& timer) = delete;
- /** Private assignment operator undefined (no copy permitted). */
- CodeTimer& operator=(const CodeTimer& timer) = delete;
-}; /* class CodeTimer */
-
-} // namespace cvc5
-
-#endif
+++ /dev/null
-/******************************************************************************
- * Top contributors (to current version):
- * Gereon Kremer
- *
- * This file is part of the cvc5 project.
- *
- * Copyright (c) 2009-2021 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.
- * ****************************************************************************
- *
- * Statistic utilities.
- */
-
-#include "util/stats_utils.h"
-
-#include <chrono>
-#include <iomanip>
-#include <iostream>
-
-#include "util/ostream_util.h"
-#include "util/stats_timer.h"
-
-namespace cvc5 {
-
-std::ostream& operator<<(std::ostream& os,
- const timer_stat_detail::duration& dur)
-{
- StreamFormatScope format_scope(os);
-
- return os << (dur / std::chrono::seconds(1)) << "." << std::setfill('0')
- << std::setw(9) << std::right
- << (dur % std::chrono::seconds(1)).count();
-}
-
-} // namespace cvc5
+++ /dev/null
-/******************************************************************************
- * Top contributors (to current version):
- * Gereon Kremer, Mathias Preiner
- *
- * This file is part of the cvc5 project.
- *
- * Copyright (c) 2009-2021 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.
- * ****************************************************************************
- *
- * Statistic utilities.
- */
-
-#include "cvc5_private_library.h"
-
-#ifndef CVC5__UTIL__STATS_UTILS_H
-#define CVC5__UTIL__STATS_UTILS_H
-
-#include <iosfwd>
-
-#include "cvc4_export.h"
-
-namespace cvc5 {
-
-namespace timer_stat_detail {
-struct duration;
-}
-
-std::ostream& operator<<(std::ostream& os,
- const timer_stat_detail::duration& dur) CVC4_EXPORT;
-
-} // namespace cvc5
-
-#endif
#include <ctime>
#include <sstream>
#include <string>
+#include <thread>
#include "expr/proof_rule.h"
#include "lib/clock_gettime.h"
#include "test.h"
#include "util/statistics_registry.h"
-#include "util/stats_histogram.h"
-#include "util/stats_timer.h"
+#include "util/statistics_stats.h"
namespace cvc5 {
+
+std::ostream& operator<<(std::ostream& os, const StatisticBaseValue* sbv)
+{
+ return os << *sbv;
+}
+bool operator==(const StatisticBaseValue* sbv, const std::string& s)
+{
+ std::stringstream ss;
+ ss << sbv;
+ return ss.str() == s;
+}
+
namespace test {
class TestUtilBlackStats : public TestInternal
TEST_F(TestUtilBlackStats, stats)
{
#ifdef CVC5_STATISTICS_ON
+ StatisticsRegistry reg(false);
std::string empty, bar = "bar", baz = "baz";
- ReferenceStat<std::string> refStr("stat #1", empty);
- ReferenceStat<std::string> refStr2("refStr2", bar);
- BackedStat<std::string> backedStr("backed", baz);
-
- BackedStat<double> backedDouble("backedDouble", 16.5);
- BackedStat<double> backedNegDouble("backedNegDouble", -16.5);
- BackedStat<double> backedDoubleNoDec("backedDoubleNoDec", 2.0);
- BackedStat<bool> backedBool("backedBool", true);
- BackedStat<void*> backedAddr("backedDouble", (void*)0xDEADBEEF);
- IntegralHistogramStat<std::int64_t> histIntStat("hist-int");
- histIntStat << 15 << 16 << 15 << 14 << 16;
- IntegralHistogramStat<cvc5::PfRule> histPfRuleStat("hist-pfrule");
- histPfRuleStat << PfRule::ASSUME << PfRule::SCOPE << PfRule::ASSUME;
-
- // A statistic with no safe_print support
- BackedStat<std::string*> backedUnsupported("backedUnsupported", &bar);
-
- IntStat sInt("my int", 10);
- TimerStat sTimer("a timer ! for measuring time");
-
- ASSERT_EQ(refStr.getName(), "stat #1");
- ASSERT_EQ(refStr2.getName(), "refStr2");
- ASSERT_EQ(backedStr.getName(), "backed");
- ASSERT_EQ(sInt.getName(), "my int");
- ASSERT_EQ(sTimer.getName(), "a timer ! for measuring time");
- ASSERT_EQ(histIntStat.getName(), "hist-int");
- ASSERT_EQ(histPfRuleStat.getName(), "hist-pfrule");
-
- ASSERT_EQ(refStr.get(), empty);
- ASSERT_EQ(refStr2.get(), bar);
- empty = "a different string";
- bar += " and with an addition";
- ASSERT_EQ(refStr.get(), empty);
- ASSERT_EQ(refStr2.get(), bar);
-
- ASSERT_EQ(backedStr.get(), "baz");
- baz = "something else";
- ASSERT_EQ(backedStr.get(), "baz");
-
- ASSERT_EQ(sInt.get(), 10);
- sInt.set(100);
- ASSERT_EQ(sInt.get(), 100);
-
- ASSERT_TRUE(sTimer.get() == std::chrono::nanoseconds());
-
- std::stringstream sstr;
-
- refStr.flushInformation(sstr);
- ASSERT_EQ(sstr.str(), empty);
- sstr.str("");
- refStr2.flushInformation(sstr);
- ASSERT_EQ(sstr.str(), bar);
- sstr.str("");
- backedStr.flushInformation(sstr);
- ASSERT_EQ(sstr.str(), "baz");
- sstr.str("");
- sInt.flushInformation(sstr);
- ASSERT_EQ(sstr.str(), "100");
- sstr.str("");
- sTimer.flushInformation(sstr);
- ASSERT_EQ(sstr.str(), "0.000000000");
-
- // Test safeFlushInformation (and safe_print functions)
- char tmp_filename[] = "testXXXXXX";
- int fd = mkstemp(tmp_filename);
- ASSERT_NE(fd, -1);
- refStr.safeFlushInformation(fd);
- safe_print(fd, "\n");
- refStr2.safeFlushInformation(fd);
- safe_print(fd, "\n");
- backedStr.safeFlushInformation(fd);
- safe_print(fd, "\n");
- sInt.safeFlushInformation(fd);
- safe_print(fd, "\n");
- sTimer.safeFlushInformation(fd);
- safe_print(fd, "\n");
- backedDouble.safeFlushInformation(fd);
- safe_print(fd, "\n");
- backedNegDouble.safeFlushInformation(fd);
- safe_print(fd, "\n");
- backedDoubleNoDec.safeFlushInformation(fd);
- safe_print(fd, "\n");
- backedAddr.safeFlushInformation(fd);
- safe_print(fd, "\n");
- backedBool.safeFlushInformation(fd);
- safe_print(fd, "\n");
- histIntStat.safeFlushInformation(fd);
- safe_print(fd, "\n");
- histPfRuleStat.safeFlushInformation(fd);
- safe_print(fd, "\n");
- backedUnsupported.safeFlushInformation(fd);
- off_t file_size = lseek(fd, 0, SEEK_CUR);
- close(fd);
-
- char* buf = new char[file_size];
- fd = open(tmp_filename, O_RDONLY);
- ASSERT_NE(fd, -1);
- ssize_t n_read = pread(fd, buf, file_size, 0);
- ASSERT_EQ(n_read, file_size);
- close(fd);
-
- const char* expected =
- "a different string\n"
- "bar and with an addition\n"
- "baz\n"
- "100\n"
- "0.000000000\n"
- "16.5\n"
- "-16.5\n"
- "2.0\n"
- "0xdeadbeef\n"
- "true\n"
- "[(14 : 1), (15 : 2), (16 : 2)]\n"
- "[(ASSUME : 2), (SCOPE : 1)]\n"
- "<unsupported>";
- ASSERT_EQ(strncmp(expected, buf, file_size), 0);
- delete[] buf;
-
- int ret = remove(tmp_filename);
- ASSERT_EQ(ret, 0);
+
+ AverageStat avg = reg.registerAverage("avg");
+ avg << 1.0 << 2.0;
+
+ HistogramStat<int64_t> histInt = reg.registerHistogram<int64_t>("hist-int");
+ histInt << 15 << 16 << 15 << 14 << 16;
+
+ HistogramStat<PfRule> histPfRule =
+ reg.registerHistogram<PfRule>("hist-pfrule");
+ histPfRule << PfRule::ASSUME << PfRule::SCOPE << PfRule::ASSUME;
+
+ IntStat intstat = reg.registerInt("int");
+ intstat = 5;
+ intstat++;
+
+ ReferenceStat<std::string> refStr =
+ reg.registerReference<std::string>("strref1", empty);
+ ReferenceStat<std::string> refStr2 =
+ reg.registerReference<std::string>("strref2", bar);
+
+ TimerStat timer = reg.registerTimer("timer");
+ {
+ CodeTimer ct(timer);
+ std::this_thread::sleep_for(std::chrono::milliseconds(50));
+ }
+
+ ValueStat<std::string> valStr = reg.registerValue("backed", baz);
+ valStr.set("barz");
+ ValueStat<double> valD1 = reg.registerValue("backedDouble", 16.5);
+ valD1.set(3.5);
+ ValueStat<double> valD2 = reg.registerValue("backedNegDouble", -16.5);
+ valD2.set(-3.5);
+ ValueStat<double> valD3 = reg.registerValue("backedDoubleNoDec", 2.0);
+ valD3.set(17);
+
+ ASSERT_EQ(reg.get("avg"), std::string("1.5"));
+ ASSERT_EQ(reg.get("hist-int"), std::string("{ 14: 1, 15: 2, 16: 2 }"));
+ ASSERT_EQ(reg.get("hist-pfrule"), std::string("{ ASSUME: 2, SCOPE: 1 }"));
+ ASSERT_EQ(reg.get("int"), std::string("6"));
+ ASSERT_EQ(reg.get("strref1"), std::string(""));
+ ASSERT_EQ(reg.get("strref2"), std::string("bar"));
+ ASSERT_EQ(reg.get("backed"), std::string("barz"));
+ ASSERT_EQ(reg.get("backedDouble"), std::string("3.5"));
+ ASSERT_EQ(reg.get("backedNegDouble"), std::string("-3.5"));
+ ASSERT_EQ(reg.get("backedDoubleNoDec"), std::string("17"));
#endif
}
} // namespace test
projects / cvc5.git / commitdiff