Merge branch 'master' of github.com:CVC4/CVC4

5 files changed, 28 insertions, 286 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;
diff --git a/test/unit/Makefile.am b/test/unit/Makefile.am
index 129d086df..c2f2b24e2 100644
--- a/test/unit/Makefile.am
+++ b/test/unit/Makefile.am
@@ -37,7 +37,6 @@ UNIT_TESTS += \
 	context/cdmap_black \
 	context/cdmap_white \
 	context/cdvector_black \
-	context/stacking_vector_black \
 	util/array_store_all_black \
 	util/assert_white \
 	util/binary_heap_black \
diff --git a/test/unit/context/stacking_vector_black.h b/test/unit/context/stacking_vector_black.h
deleted file mode 100644
index 0dd96ea57..000000000
--- a/test/unit/context/stacking_vector_black.h
+++ /dev/null
@@ -1,159 +0,0 @@
-/*********************                                                        */
-/*! \file stacking_vector_black.h
- ** \verbatim
- ** Top contributors (to current version):
- **   Morgan Deters, Paul Meng
- ** 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 Black box testing of CVC4::context::StackingVector
- **
- ** Black box testing of CVC4::context::StackingVector.
- **/
-
-#include <cxxtest/TestSuite.h>
-
-#include "context/context.h"
-#include "expr/node.h"
-#include "context/stacking_vector.h"
-
-using namespace CVC4;
-using namespace CVC4::context;
-
-using namespace std;
-
-/**
- * Test the StackingVector.
- */
-class StackingVectorBlack : public CxxTest::TestSuite {
-  Context* d_ctxt;
-  StackingVector<TNode>* d_vectorPtr;
-  NodeManager* d_nm;
-  NodeManagerScope* d_scope;
-
-  Node a, b, c, d, e, f, g;
-
-public:
-
-  void setUp() {
-    d_ctxt = new Context();
-    d_nm = new NodeManager(NULL);
-    d_scope = new NodeManagerScope(d_nm);
-    d_vectorPtr = new StackingVector<TNode>(d_ctxt);
-
-    a = d_nm->mkSkolem("a", d_nm->realType());
-    b = d_nm->mkSkolem("b", d_nm->realType());
-    c = d_nm->mkSkolem("c", d_nm->realType());
-    d = d_nm->mkSkolem("d", d_nm->realType());
-    e = d_nm->mkSkolem("e", d_nm->realType());
-    f = d_nm->mkSkolem("f", d_nm->realType());
-    g = d_nm->mkSkolem("g", d_nm->realType());
-  }
-
-  void tearDown() {
-    g = Node::null();
-    f = Node::null();
-    e = Node::null();
-    d = Node::null();
-    c = Node::null();
-    b = Node::null();
-    a = Node::null();
-
-    delete d_vectorPtr;
-    delete d_scope;
-    delete d_nm;
-    delete d_ctxt;
-  }
-
-  void testSimpleContextual() {
-    StackingVector<TNode>& d_vector = *d_vectorPtr;
-
-    TS_ASSERT(d_vector[1].isNull());
-    TS_ASSERT(d_vector[2].isNull());
-    TS_ASSERT(d_vector[3].isNull());
-    TS_ASSERT(d_vector[4].isNull());
-    TS_ASSERT(d_vector[5].isNull());
-    TS_ASSERT(d_vector[6].isNull());
-    TS_ASSERT(d_vector[7].isNull());
-
-    d_vector.set(1, b);
-
-    TS_ASSERT(d_vector[1] == b);
-    TS_ASSERT(d_vector[2].isNull());
-    TS_ASSERT(d_vector[3].isNull());
-    TS_ASSERT(d_vector[4].isNull());
-    TS_ASSERT(d_vector[5].isNull());
-    TS_ASSERT(d_vector[6].isNull());
-    TS_ASSERT(d_vector[7].isNull());
-
-    d_ctxt->push();
-    {
-      TS_ASSERT(d_vector[1] == b);
-      TS_ASSERT(d_vector[2].isNull());
-      TS_ASSERT(d_vector[3].isNull());
-      TS_ASSERT(d_vector[4].isNull());
-      TS_ASSERT(d_vector[5].isNull());
-      TS_ASSERT(d_vector[6].isNull());
-      TS_ASSERT(d_vector[7].isNull());
-
-      d_vector.set(3, d);
-      d_vector.set(6, e);
-
-      TS_ASSERT(d_vector[1] == b);
-      TS_ASSERT(d_vector[2].isNull());
-      TS_ASSERT(d_vector[3] == d);
-      TS_ASSERT(d_vector[4].isNull());
-      TS_ASSERT(d_vector[5].isNull());
-      TS_ASSERT(d_vector[6] == e);
-      TS_ASSERT(d_vector[7].isNull());
-
-      d_ctxt->push();
-      {
-
-        TS_ASSERT(d_vector[1] == b);
-        TS_ASSERT(d_vector[2].isNull());
-        TS_ASSERT(d_vector[3] == d);
-        TS_ASSERT(d_vector[4].isNull());
-        TS_ASSERT(d_vector[5].isNull());
-        TS_ASSERT(d_vector[6] == e);
-        TS_ASSERT(d_vector[7].isNull());
-
-        d_vector.set(1, c);
-        d_vector.set(6, f);
-        d_vector.set(5, d);
-        d_vector.set(3, Node::null());
-        d_vector.set(7, a);
-
-        TS_ASSERT(d_vector[1] == c);
-        TS_ASSERT(d_vector[2].isNull());
-        TS_ASSERT(d_vector[3].isNull());
-        TS_ASSERT(d_vector[4].isNull());
-        TS_ASSERT(d_vector[5] == d);
-        TS_ASSERT(d_vector[6] == f);
-        TS_ASSERT(d_vector[7] == a);
-
-      }
-      d_ctxt->pop();
-
-      TS_ASSERT(d_vector[1] == b);
-      TS_ASSERT(d_vector[2].isNull());
-      TS_ASSERT(d_vector[3] == d);
-      TS_ASSERT(d_vector[4].isNull());
-      TS_ASSERT(d_vector[5].isNull());
-      TS_ASSERT(d_vector[6] == e);
-      TS_ASSERT(d_vector[7].isNull());
-    }
-    d_ctxt->pop();
-
-    TS_ASSERT(d_vector[1] == b);
-    TS_ASSERT(d_vector[2].isNull());
-    TS_ASSERT(d_vector[3].isNull());
-    TS_ASSERT(d_vector[4].isNull());
-    TS_ASSERT(d_vector[5].isNull());
-    TS_ASSERT(d_vector[6].isNull());
-    TS_ASSERT(d_vector[7].isNull());
-  }
-};