summaryrefslogtreecommitdiff
diff options
context:
space:
mode:
Diffstat
-rw-r--r--src/Makefile.am1
-rw-r--r--src/context/stacking_map.h162
-rw-r--r--test/unit/Makefile.am1
-rw-r--r--test/unit/context/stacking_map_black.h159
-rw-r--r--test/unit/theory/stacking_map_black.h158
5 files changed, 0 insertions, 481 deletions
diff --git a/src/Makefile.am b/src/Makefile.am
index d5223773e..f16c5408b 100644
--- a/src/Makefile.am
+++ b/src/Makefile.am
@@ -54,7 +54,6 @@ libcvc4_la_SOURCES = \
context/cdhashset_forward.h \
context/cdvector.h \
context/cdmaybe.h \
- context/stacking_map.h \
context/stacking_vector.h \
context/cddense_set.h \
decision/decision_attributes.h \
diff --git a/src/context/stacking_map.h b/src/context/stacking_map.h
deleted file mode 100644
index 4ce1b2d33..000000000
--- a/src/context/stacking_map.h
+++ /dev/null
@@ -1,162 +0,0 @@
-/********************* */
-/*! \file stacking_map.h
- ** \verbatim
- ** Original author: Morgan Deters
- ** Major contributors: none
- ** Minor contributors (to current version): Dejan Jovanovic
- ** 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 Backtrackable map using an undo stack
- **
- ** Backtrackable map using an undo stack rather than storing items in
- ** a CDMap<>.
- **/
-
-#include "cvc4_private.h"
-
-#ifndef __CVC4__CONTEXT__STACKING_MAP_H
-#define __CVC4__CONTEXT__STACKING_MAP_H
-
-#include <utility>
-#include <vector>
-#include <ext/hash_map>
-
-#include "expr/node.h"
-#include "context/cdo.h"
-
-namespace CVC4 {
-namespace context {
-
-template <class T>
-struct StackingMapArgType {
- typedef T argtype;
-};/* struct StackingMapArgType<T> */
-
-template <>
-struct StackingMapArgType<Node> {
- typedef TNode argtype;
-};/* struct StackingMapArgType<Node> */
-
-
-template <class KeyType, class ValueType, class KeyHash>
-struct StackingMapRestoreValue {
- typedef typename StackingMapArgType<KeyType>::argtype ArgType;
- static void restore(__gnu_cxx::hash_map<KeyType, ValueType, KeyHash>& map, const ArgType& k, const ValueType& v) {
- map[k] = v;
- }
-};/* struct StackingMapRestoreValue<KeyType, ValueType, KeyHash> */
-
-template <class KeyType, class KeyHash>
-struct StackingMapRestoreValue<KeyType, Node, KeyHash> {
- typedef typename StackingMapArgType<KeyType>::argtype ArgType;
- static void restore(__gnu_cxx::hash_map<KeyType, Node, KeyHash>& map, const ArgType& k, TNode v) {
- if(v.isNull()) {
- map.erase(k);
- } else {
- map[k] = v;
- }
- }
-};/* struct StackingMapRestoreValue<KeyType, Node, KeyHash> */
-
-template <class KeyType, class KeyHash>
-struct StackingMapRestoreValue<KeyType, TNode, KeyHash> {
- typedef typename StackingMapArgType<KeyType>::argtype ArgType;
- static void restore(__gnu_cxx::hash_map<KeyType, TNode, KeyHash>& map, const ArgType& k, TNode v) {
- if(v.isNull()) {
- map.erase(k);
- } else {
- map[k] = v;
- }
- }
-};/* struct StackingMapRestoreValue<KeyType, TNode, KeyHash> */
-
-
-template <class KeyType, class ValueType, class KeyHash>
-class StackingMap : context::ContextNotifyObj {
- /** Our underlying map type. */
- typedef __gnu_cxx::hash_map<KeyType, ValueType, KeyHash> MapType;
-
- /**
- * The type for arguments being passed in. It's the same as
- * KeyType, unless KeyType is Node, then it's TNode for efficiency.
- */
- typedef typename StackingMapArgType<KeyType>::argtype ArgType;
-
- /** Our map of keys to their values. */
- MapType d_map;
-
- /** Our undo stack for changes made to d_map. */
- std::vector<std::pair<ArgType, ValueType> > d_trace;
-
- /** Our current offset in the d_trace stack (context-dependent). */
- context::CDO<size_t> d_offset;
-
-protected:
-
- /**
- * Called by the Context when a pop occurs. Cancels everything to the
- * current context level. Overrides ContextNotifyObj::contextNotifyPop().
- */
- void contextNotifyPop();
-
-public:
- typedef typename MapType::const_iterator const_iterator;
-
- StackingMap(context::Context* ctxt) :
- context::ContextNotifyObj(ctxt),
- d_offset(ctxt, 0) {
- }
-
- ~StackingMap() throw() { }
-
- const_iterator find(ArgType n) const { return d_map.find(n); }
- const_iterator end() const { return d_map.end(); }
-
- /**
- * Return a key's value in the key-value map. If n is not a key in
- * the map, this function returns a default-constructed value.
- */
- ValueType operator[](ArgType n) const {
- const_iterator it = find(n);
- if(it == end()) {
- return ValueType();
- } else {
- return (*it).second;
- }
- }
- //ValueType& 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(ArgType n, const ValueType& newValue);
-
-};/* class StackingMap<> */
-
-template <class KeyType, class ValueType, class KeyHash>
-void StackingMap<KeyType, ValueType, KeyHash>::set(ArgType n, const ValueType& newValue) {
- Trace("sm") << "SM setting " << n << " : " << newValue << " @ " << d_trace.size() << std::endl;
- ValueType& ref = d_map[n];
- d_trace.push_back(std::make_pair(n, ValueType(ref)));
- d_offset = d_trace.size();
- ref = newValue;
-}
-
-template <class KeyType, class ValueType, class KeyHash>
-void StackingMap<KeyType, ValueType, KeyHash>::contextNotifyPop() {
- Trace("sm") << "SM cancelling : " << d_offset << " < " << d_trace.size() << " ?" << std::endl;
- while(d_offset < d_trace.size()) {
- std::pair<ArgType, ValueType> p = d_trace.back();
- StackingMapRestoreValue<KeyType, ValueType, KeyHash>::restore(d_map, p.first, p.second);
- d_trace.pop_back();
- }
- Trace("sm") << "SM cancelling finished." << std::endl;
-}
-
-}/* CVC4::context namespace */
-}/* CVC4 namespace */
-
-#endif /*__CVC4__CONTEXT__STACKING_MAP_H */
diff --git a/test/unit/Makefile.am b/test/unit/Makefile.am
index 98bedefbf..36203725f 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_map_black \
context/stacking_vector_black \
util/array_store_all_black \
util/assert_white \
diff --git a/test/unit/context/stacking_map_black.h b/test/unit/context/stacking_map_black.h
deleted file mode 100644
index 4daab5cce..000000000
--- a/test/unit/context/stacking_map_black.h
+++ /dev/null
@@ -1,159 +0,0 @@
-/********************* */
-/*! \file stacking_map_black.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 Black box testing of CVC4::context::StackingMap
- **
- ** Black box testing of CVC4::context::StackingMap.
- **/
-
-#include <cxxtest/TestSuite.h>
-
-#include "context/context.h"
-#include "expr/node.h"
-#include "context/stacking_map.h"
-
-using namespace CVC4;
-using namespace CVC4::context;
-
-using namespace std;
-
-/**
- * Test the StackingMap.
- */
-class StackingMapBlack : public CxxTest::TestSuite {
- Context* d_ctxt;
- StackingMap<TNode, TNode, TNodeHashFunction>* d_mapPtr;
- 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_mapPtr = new StackingMap<TNode, TNode, TNodeHashFunction>(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_mapPtr;
- delete d_scope;
- delete d_nm;
- delete d_ctxt;
- }
-
- void testSimpleContextual() {
- StackingMap<TNode, TNode, TNodeHashFunction>& d_map = *d_mapPtr;
-
- TS_ASSERT(d_map[a].isNull());
- TS_ASSERT(d_map[b].isNull());
- TS_ASSERT(d_map[c].isNull());
- TS_ASSERT(d_map[d].isNull());
- TS_ASSERT(d_map[e].isNull());
- TS_ASSERT(d_map[f].isNull());
- TS_ASSERT(d_map[g].isNull());
-
- d_map.set(a, b);
-
- TS_ASSERT(d_map[a] == b);
- TS_ASSERT(d_map[b].isNull());
- TS_ASSERT(d_map[c].isNull());
- TS_ASSERT(d_map[d].isNull());
- TS_ASSERT(d_map[e].isNull());
- TS_ASSERT(d_map[f].isNull());
- TS_ASSERT(d_map[g].isNull());
-
- d_ctxt->push();
- {
- TS_ASSERT(d_map[a] == b);
- TS_ASSERT(d_map[b].isNull());
- TS_ASSERT(d_map[c].isNull());
- TS_ASSERT(d_map[d].isNull());
- TS_ASSERT(d_map[e].isNull());
- TS_ASSERT(d_map[f].isNull());
- TS_ASSERT(d_map[g].isNull());
-
- d_map.set(c, d);
- d_map.set(f, e);
-
- TS_ASSERT(d_map[a] == b);
- TS_ASSERT(d_map[b].isNull());
- TS_ASSERT(d_map[c] == d);
- TS_ASSERT(d_map[d].isNull());
- TS_ASSERT(d_map[e].isNull());
- TS_ASSERT(d_map[f] == e);
- TS_ASSERT(d_map[g].isNull());
-
- d_ctxt->push();
- {
-
- TS_ASSERT(d_map[a] == b);
- TS_ASSERT(d_map[b].isNull());
- TS_ASSERT(d_map[c] == d);
- TS_ASSERT(d_map[d].isNull());
- TS_ASSERT(d_map[e].isNull());
- TS_ASSERT(d_map[f] == e);
- TS_ASSERT(d_map[g].isNull());
-
- d_map.set(a, c);
- d_map.set(f, f);
- d_map.set(e, d);
- d_map.set(c, Node::null());
- d_map.set(g, a);
-
- TS_ASSERT(d_map[a] == c);
- TS_ASSERT(d_map[b].isNull());
- TS_ASSERT(d_map[c].isNull());
- TS_ASSERT(d_map[d].isNull());
- TS_ASSERT(d_map[e] == d);
- TS_ASSERT(d_map[f] == f);
- TS_ASSERT(d_map[g] == a);
-
- }
- d_ctxt->pop();
-
- TS_ASSERT(d_map[a] == b);
- TS_ASSERT(d_map[b].isNull());
- TS_ASSERT(d_map[c] == d);
- TS_ASSERT(d_map[d].isNull());
- TS_ASSERT(d_map[e].isNull());
- TS_ASSERT(d_map[f] == e);
- TS_ASSERT(d_map[g].isNull());
- }
- d_ctxt->pop();
-
- TS_ASSERT(d_map[a] == b);
- TS_ASSERT(d_map[b].isNull());
- TS_ASSERT(d_map[c].isNull());
- TS_ASSERT(d_map[d].isNull());
- TS_ASSERT(d_map[e].isNull());
- TS_ASSERT(d_map[f].isNull());
- TS_ASSERT(d_map[g].isNull());
- }
-};
diff --git a/test/unit/theory/stacking_map_black.h b/test/unit/theory/stacking_map_black.h
deleted file mode 100644
index 8097220ad..000000000
--- a/test/unit/theory/stacking_map_black.h
+++ /dev/null
@@ -1,158 +0,0 @@
-/********************* */
-/*! \file stacking_map_black.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 Black box testing of CVC4::theory::uf::morgan::StackingMap
- **
- ** Black box testing of CVC4::theory::uf::morgan::StackingMap.
- **/
-
-#include <cxxtest/TestSuite.h>
-
-#include "context/context.h"
-#include "expr/node.h"
-#include "theory/uf/morgan/stacking_map.h"
-
-using namespace CVC4;
-using namespace CVC4::theory::uf::morgan;
-using namespace CVC4::context;
-
-using namespace std;
-
-/**
- * Test the StackingMap.
- */
-class StackingMapBlack : public CxxTest::TestSuite {
- Context* d_ctxt;
- StackingMap<TNode, TNodeHashFunction>* d_map;
- 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(d_ctxt, NULL);
- d_scope = new NodeManagerScope(d_nm);
- d_map = new StackingMap<TNode, TNodeHashFunction>(d_ctxt);
-
- a = d_nm->mkVar("a", d_nm->realType());
- b = d_nm->mkVar("b", d_nm->realType());
- c = d_nm->mkVar("c", d_nm->realType());
- d = d_nm->mkVar("d", d_nm->realType());
- e = d_nm->mkVar("e", d_nm->realType());
- f = d_nm->mkVar("f", d_nm->realType());
- g = d_nm->mkVar("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_map;
- delete d_scope;
- delete d_nm;
- delete d_ctxt;
- }
-
- void testSimpleContextual() {
- TS_ASSERT(d_map->find(a).isNull());
- TS_ASSERT(d_map->find(b).isNull());
- TS_ASSERT(d_map->find(c).isNull());
- TS_ASSERT(d_map->find(d).isNull());
- TS_ASSERT(d_map->find(e).isNull());
- TS_ASSERT(d_map->find(f).isNull());
- TS_ASSERT(d_map->find(g).isNull());
-
- d_map->set(a, b);
-
- TS_ASSERT(d_map->find(a) == b);
- TS_ASSERT(d_map->find(b).isNull());
- TS_ASSERT(d_map->find(c).isNull());
- TS_ASSERT(d_map->find(d).isNull());
- TS_ASSERT(d_map->find(e).isNull());
- TS_ASSERT(d_map->find(f).isNull());
- TS_ASSERT(d_map->find(g).isNull());
-
- d_ctxt->push();
- {
- TS_ASSERT(d_map->find(a) == b);
- TS_ASSERT(d_map->find(b).isNull());
- TS_ASSERT(d_map->find(c).isNull());
- TS_ASSERT(d_map->find(d).isNull());
- TS_ASSERT(d_map->find(e).isNull());
- TS_ASSERT(d_map->find(f).isNull());
- TS_ASSERT(d_map->find(g).isNull());
-
- d_map->set(c, d);
- d_map->set(f, e);
-
- TS_ASSERT(d_map->find(a) == b);
- TS_ASSERT(d_map->find(b).isNull());
- TS_ASSERT(d_map->find(c) == d);
- TS_ASSERT(d_map->find(d).isNull());
- TS_ASSERT(d_map->find(e).isNull());
- TS_ASSERT(d_map->find(f) == e);
- TS_ASSERT(d_map->find(g).isNull());
-
- d_ctxt->push();
- {
-
- TS_ASSERT(d_map->find(a) == b);
- TS_ASSERT(d_map->find(b).isNull());
- TS_ASSERT(d_map->find(c) == d);
- TS_ASSERT(d_map->find(d).isNull());
- TS_ASSERT(d_map->find(e).isNull());
- TS_ASSERT(d_map->find(f) == e);
- TS_ASSERT(d_map->find(g).isNull());
-
- d_map->set(a, c);
- d_map->set(f, f);
- d_map->set(e, d);
- d_map->set(c, Node::null());
- d_map->set(g, a);
-
- TS_ASSERT(d_map->find(a) == c);
- TS_ASSERT(d_map->find(b).isNull());
- TS_ASSERT(d_map->find(c).isNull());
- TS_ASSERT(d_map->find(d).isNull());
- TS_ASSERT(d_map->find(e) == d);
- TS_ASSERT(d_map->find(f) == f);
- TS_ASSERT(d_map->find(g) == a);
-
- }
- d_ctxt->pop();
-
- TS_ASSERT(d_map->find(a) == b);
- TS_ASSERT(d_map->find(b).isNull());
- TS_ASSERT(d_map->find(c) == d);
- TS_ASSERT(d_map->find(d).isNull());
- TS_ASSERT(d_map->find(e).isNull());
- TS_ASSERT(d_map->find(f) == e);
- TS_ASSERT(d_map->find(g).isNull());
- }
- d_ctxt->pop();
-
- TS_ASSERT(d_map->find(a) == b);
- TS_ASSERT(d_map->find(b).isNull());
- TS_ASSERT(d_map->find(c).isNull());
- TS_ASSERT(d_map->find(d).isNull());
- TS_ASSERT(d_map->find(e).isNull());
- TS_ASSERT(d_map->find(f).isNull());
- TS_ASSERT(d_map->find(g).isNull());
- }
-};
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback