+++ /dev/null
-/********************* */
-/*! \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 */
+++ /dev/null
-/********************* */
-/*! \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());
- }
-};
projects / cvc5.git / commitdiff