summaryrefslogtreecommitdiff
path: root/test/unit/context
diff options
context:
space:
mode:
authorAndres Noetzli <andres.noetzli@gmail.com>2017-07-07 15:25:04 -0700
committerGitHub <noreply@github.com>2017-07-07 15:25:04 -0700
commit88b9d2b384f6625df3853a64b240e3cf1f3a19aa (patch)
tree9e35b462718b90beb30cd2afbfdc68ff68cff6b0 /test/unit/context
parent4f9f046557b4de30c8f2ff654ea6e172e9cd912d (diff)
Remove unused stacking_vector class (#185)
Diffstat (limited to 'test/unit/context')
-rw-r--r--test/unit/context/stacking_vector_black.h159
1 files changed, 0 insertions, 159 deletions
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());
- }
-};
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback