diff options
Diffstat (limited to 'src')
-rw-r--r-- | src/Makefile.am | 1 | ||||
-rw-r--r-- | src/context/stacking_vector.h | 114 | ||||
-rw-r--r-- | src/util/statistics_registry.h | 39 |
3 files changed, 28 insertions, 126 deletions
diff --git a/src/Makefile.am b/src/Makefile.am index e44bd920c..157fe33d2 100644 --- a/src/Makefile.am +++ b/src/Makefile.am @@ -55,7 +55,6 @@ libcvc4_la_SOURCES = \ context/context.h \ context/context_mm.cpp \ context/context_mm.h \ - context/stacking_vector.h \ decision/decision_attributes.h \ decision/decision_engine.cpp \ decision/decision_engine.h \ diff --git a/src/context/stacking_vector.h b/src/context/stacking_vector.h deleted file mode 100644 index 5ef0404e4..000000000 --- a/src/context/stacking_vector.h +++ /dev/null @@ -1,114 +0,0 @@ -/********************* */ -/*! \file stacking_vector.h - ** \verbatim - ** Top contributors (to current version): - ** Morgan Deters, Tim King, Dejan Jovanovic - ** This file is part of the CVC4 project. - ** Copyright (c) 2009-2017 by the authors listed in the file AUTHORS - ** in the top-level source directory) and their institutional affiliations. - ** All rights reserved. See the file COPYING in the top-level source - ** directory for licensing information.\endverbatim - ** - ** \brief Backtrackable vector using an undo stack - ** - ** Backtrackable vector using an undo stack rather than storing items in - ** a CDVector<>. - **/ - -#include "cvc4_private.h" - -#ifndef __CVC4__CONTEXT__STACKING_VECTOR_H -#define __CVC4__CONTEXT__STACKING_VECTOR_H - -#include <utility> -#include <vector> - -#include "context/cdo.h" - -namespace CVC4 { -namespace context { - -template <class T> -class StackingVector : context::ContextNotifyObj { - /** Our underlying map type. */ - typedef std::vector<T> VectorType; - - /** Our map of indices to their values. */ - VectorType d_map; - - /** Our undo stack for changes made to d_map. */ - std::vector<std::pair<size_t, T> > d_trace; - - /** Our current offset in the d_trace stack (context-dependent). */ - context::CDO<size_t> d_offset; - -public: - typedef typename VectorType::const_iterator const_iterator; - - StackingVector(context::Context* ctxt) : - context::ContextNotifyObj(ctxt), - d_offset(ctxt, 0) { - } - - ~StackingVector() { } - - /** - * Return a value from the vector. If n is not a key in - * the map, this function returns a default-constructed T. - */ - T operator[](size_t n) const { - return n < d_map.size() ? d_map[n] : T(); - } - //T& operator[](ArgType n) { return d_map[n]; }// not permitted--bypasses set() logic - - /** - * Set the value in the key-value map for Node n to newValue. - */ - void set(size_t n, const T& newValue); - - /** - * Return the current size of the vector. Note that once a certain - * size is achieved, the size never goes down again, although the - * elements off the old end of the vector will be replaced with - * default-constructed T values. - */ - size_t size() const { - return d_map.size(); - } - - /** - * Called by the Context when a pop occurs. Cancels everything to the - * current context level. Overrides ContextNotifyObj::notify(). - */ - void contextNotifyPop(); - -};/* class StackingVector<> */ - -template <class T> -void StackingVector<T>::set(size_t n, const T& newValue) { - Trace("sv") << "SV setting " << n << " : " << newValue << " @ " << d_trace.size() << std::endl; - if(n >= d_map.size()) { - d_map.resize(n + 1); - } - T& ref = d_map[n]; - d_trace.push_back(std::make_pair(n, T(ref))); - d_offset = d_trace.size(); - ref = newValue; -} - -template <class T> -void StackingVector<T>::contextNotifyPop() { - Trace("sv") << "SV cancelling : " << d_offset << " < " << d_trace.size() << " ?" << std::endl; - while(d_offset < d_trace.size()) { - std::pair<size_t, T> p = d_trace.back(); - Trace("sv") << "SV cancelling: " << p.first << " back to " << p.second << std::endl; - d_map[p.first] = p.second; - d_trace.pop_back(); - } - Trace("sv") << "SV cancelling finished." << std::endl; -} - -}/* CVC4::context namespace */ -}/* CVC4 namespace */ - -#endif /*__CVC4__CONTEXT__STACKING_VECTOR_H */ diff --git a/src/util/statistics_registry.h b/src/util/statistics_registry.h index d77dceea7..30f330cd7 100644 --- a/src/util/statistics_registry.h +++ b/src/util/statistics_registry.h @@ -225,6 +225,9 @@ public: /** Get the value of the statistic. */ virtual T getData() const = 0; + /** Get a reference to the data value of the statistic. */ + virtual const T& getDataRef() const = 0; + /** Flush the value of the statistic to the given output stream. */ void flushInformation(std::ostream& out) const { if(__CVC4_USE_STATISTICS) { @@ -234,7 +237,7 @@ public: virtual void safeFlushInformation(int fd) const { if (__CVC4_USE_STATISTICS) { - safe_print<T>(fd, getData()); + safe_print<T>(fd, getDataRef()); } } @@ -320,9 +323,10 @@ public: } /** Get the value of the referenced data cell. */ - T getData() const { - return *d_data; - } + virtual T getData() const { return *d_data; } + + /** Get a reference to the value of the referenced data cell. */ + virtual const T& getDataRef() const { return *d_data; } };/* class ReferenceStat<T> */ @@ -361,9 +365,10 @@ public: } /** Get the underlying data value. */ - T getData() const { - return d_data; - } + virtual T getData() const { return d_data; } + + /** Get a reference to the underlying data value. */ + virtual const T& getDataRef() const { return d_data; } };/* class BackedStat<T> */ @@ -402,8 +407,16 @@ public: } /** Get the data of the underlying (wrapped) statistic. */ - T getData() const { - return d_stat.getData(); + virtual T getData() const { return d_stat.getData(); } + + /** Get a reference to the data of the underlying (wrapped) statistic. */ + virtual const T& getDataRef() const { return d_stat.getDataRef(); } + + virtual void safeFlushInformation(int fd) const { + // ReadOnlyDataStat uses getDataRef() to get the information to print, + // which might not be appropriate for all wrapped statistics. Delegate the + // printing to the wrapped statistic instead. + d_stat.safeFlushInformation(fd); } SExpr getValue() const { @@ -728,10 +741,14 @@ public: /** If the timer is currently running */ bool running() const; - timespec getData() const; + virtual timespec getData() const; virtual void safeFlushInformation(int fd) const { - safe_print<timespec>(fd, d_data); + // Overwrite the implementation in the superclass because we cannot use + // getDataRef(): it might return stale data if the timer is currently + // running. + ::timespec data = getData(); + safe_print<timespec>(fd, data); } SExpr getValue() const; |