diff options
Diffstat (limited to 'src/util/statistics.h')
-rw-r--r-- | src/util/statistics.h | 129 |
1 files changed, 0 insertions, 129 deletions
diff --git a/src/util/statistics.h b/src/util/statistics.h deleted file mode 100644 index a7088f5c5..000000000 --- a/src/util/statistics.h +++ /dev/null @@ -1,129 +0,0 @@ -/********************* */ -/*! \file statistics.h - ** \verbatim - ** Original author: Morgan Deters - ** Major contributors: none - ** Minor contributors (to current version): none - ** This file is part of the CVC4 project. - ** Copyright (c) 2009-2014 New York University and The University of Iowa - ** See the file COPYING in the top-level source directory for licensing - ** information.\endverbatim - ** - ** \brief [[ Add one-line brief description here ]] - ** - ** [[ Add lengthier description here ]] - ** \todo document this file - **/ - -#include "cvc4_public.h" - -#ifndef __CVC4__STATISTICS_H -#define __CVC4__STATISTICS_H - -#include "util/sexpr.h" - -#include <string> -#include <ostream> -#include <set> -#include <iterator> -#include <utility> - -namespace CVC4 { - -class Stat; - -class CVC4_PUBLIC StatisticsBase { -protected: - - static std::string s_regDelim; - - /** 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; - - std::string d_prefix; - - /** The set of statistics in this object */ - StatSet d_stats; - - StatisticsBase(); - StatisticsBase(const StatisticsBase& stats); - StatisticsBase& operator=(const StatisticsBase& stats); - -public: - - virtual ~StatisticsBase() { } - - class CVC4_PUBLIC 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; - - /** Set the output prefix for this set of statistics. */ - virtual void setPrefix(const std::string& prefix); - - /** Flush all statistics to the given output stream. */ - void flushInformation(std::ostream& out) 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 CVC4_PUBLIC 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 */ - -}/* CVC4 namespace */ - -#endif /* __CVC4__STATISTICS_H */ |