diff options
author | Morgan Deters <mdeters@gmail.com> | 2011-09-02 20:41:08 +0000 |
---|---|---|
committer | Morgan Deters <mdeters@gmail.com> | 2011-09-02 20:41:08 +0000 |
commit | 1d18e5ebed9a5b20ed6a8fe21d11842acf6fa7ea (patch) | |
tree | 7074f04453914bc377ff6aeb307dd17b82b76ff3 /test/unit | |
parent | 74770f1071e6102795393cf65dd0c651038db6b4 (diff) |
Merge from my post-smtcomp branch. Includes:
Dumping infrastructure. Can dump preprocessed queries and clauses. Can
also dump queries (for testing with another solver) to see if any conflicts
are missed, T-propagations are missed, all lemmas are T-valid, etc. For a
full list of options see --dump=help.
CUDD building much cleaner.
Documentation and assertion fixes.
Printer improvements, printing of commands in language-defined way, etc.
Typechecker stuff in expr package now autogenerated, no need to manually
edit the expr package when adding a new theory.
CVC3 compatibility layer (builds as libcompat).
SWIG detection and language binding support (infrastructure).
Support for some Z3 extended commands (like datatypes) in SMT-LIBv2 mode
(when not in compliance mode).
Copyright and file headers regenerated.
Diffstat (limited to 'test/unit')
46 files changed, 603 insertions, 309 deletions
diff --git a/test/unit/Makefile.am b/test/unit/Makefile.am index f98f434c1..608d6335b 100644 --- a/test/unit/Makefile.am +++ b/test/unit/Makefile.am @@ -3,9 +3,7 @@ UNIT_TESTS = \ theory/shared_term_manager_black \ theory/theory_engine_white \ theory/theory_black \ - theory/theory_uf_tim_white \ theory/theory_arith_white \ - theory/stacking_map_black \ theory/union_find_black \ expr/expr_public \ expr/expr_manager_public \ @@ -30,9 +28,12 @@ UNIT_TESTS = \ context/cdo_black \ context/cdlist_black \ context/cdlist_context_memory_black \ + context/cdcirclist_white \ context/cdmap_black \ context/cdmap_white \ context/cdvector_black \ + context/stacking_map_black \ + context/stacking_vector_black \ util/assert_white \ util/bitvector_black \ util/datatype_black \ diff --git a/test/unit/context/cdcirclist_white.h b/test/unit/context/cdcirclist_white.h new file mode 100644 index 000000000..b03a850a8 --- /dev/null +++ b/test/unit/context/cdcirclist_white.h @@ -0,0 +1,223 @@ +/********************* */ +/*! \file cdcirclist_white.h + ** \verbatim + ** Original author: mdeters + ** Major contributors: none + ** Minor contributors (to current version): none + ** This file is part of the CVC4 prototype. + ** Copyright (c) 2009, 2010, 2011 The Analysis of Computer Systems Group (ACSys) + ** Courant Institute of Mathematical Sciences + ** New York University + ** See the file COPYING in the top-level source directory for licensing + ** information.\endverbatim + ** + ** \brief White box testing of CVC4::context::CDCircList<>. + ** + ** White box testing of CVC4::context::CDCircList<>. + **/ + +#include <cxxtest/TestSuite.h> + +#include <vector> +#include <iostream> + +#include <limits.h> + +#include "context/context.h" +#include "context/cdcirclist.h" + +#include "util/output.h" + +using namespace std; +using namespace CVC4::context; +using namespace CVC4; + +class CDCircListWhite : public CxxTest::TestSuite { +private: + + Context* d_context; + +public: + + void setUp() { + d_context = new Context(); + } + + void tearDown() { + delete d_context; + } + + void testSimple() { + //Debug.on("cdcirclist"); + CDCircList<int> l(d_context, ContextMemoryAllocator<int>(d_context->getCMM())); + + TS_ASSERT_THROWS_NOTHING( l.debugCheck() ); + + d_context->push(); + { + TS_ASSERT(l.empty()); + l.push_back(1); + TS_ASSERT(!l.empty()); + TS_ASSERT_EQUALS(l.front(), 1); + TS_ASSERT_EQUALS(l.back(), 1); + TS_ASSERT_THROWS_NOTHING( l.debugCheck() ); + + l.push_back(2); + TS_ASSERT(!l.empty()); + TS_ASSERT_EQUALS(l.front(), 1); + TS_ASSERT_EQUALS(l.back(), 2); + TS_ASSERT_THROWS_NOTHING( l.debugCheck() ); + + l.push_back(3); + TS_ASSERT(!l.empty()); + TS_ASSERT_EQUALS(l.front(), 1); + TS_ASSERT_EQUALS(l.back(), 3); + TS_ASSERT_THROWS_NOTHING( l.debugCheck() ); + +#ifdef CVC4_ASSERTIONS + TS_ASSERT_THROWS( l.concat(l), AssertionException ); +#endif /* CVC4_ASSERTIONS */ + + CDCircList<int> l2(d_context, ContextMemoryAllocator<int>(d_context->getCMM())); + l2.push_back(4); + l2.push_back(5); + l2.push_back(6); + TS_ASSERT_EQUALS(l2.front(), 4); + TS_ASSERT_EQUALS(l2.back(), 6); + TS_ASSERT_THROWS_NOTHING( l2.debugCheck() ); + + d_context->push(); + { + l.concat(l2); + + TS_ASSERT_EQUALS(l.front(), 1); + TS_ASSERT_EQUALS(l.back(), 6); + TS_ASSERT_THROWS_NOTHING( l.debugCheck() ); + + TS_ASSERT_EQUALS(l2.front(), 4); + TS_ASSERT_EQUALS(l2.back(), 3); + TS_ASSERT_THROWS_NOTHING( l2.debugCheck() ); + + d_context->push(); + { + CDCircList<int>::iterator i = l.begin(); + CDCircList<int>::iterator j = l.begin(); + TS_ASSERT_EQUALS(i, j); + TS_ASSERT_EQUALS(i++, j); + TS_ASSERT_EQUALS(i, ++j); + TS_ASSERT_EQUALS(l.erase(l.begin()), i); + + i = l.begin(); + TS_ASSERT_EQUALS(i, j); TS_ASSERT_DIFFERS(i, l.end()); + TS_ASSERT_EQUALS(*i, l.front()); TS_ASSERT_DIFFERS(i, l.end()); + TS_ASSERT_EQUALS(*i, 2); TS_ASSERT_DIFFERS(i, l.end()); + TS_ASSERT_EQUALS(*i++, 2); TS_ASSERT_DIFFERS(i, l.end()); TS_ASSERT_DIFFERS(i, j); + TS_ASSERT_EQUALS(*i++, 3); TS_ASSERT_DIFFERS(i, l.end()); TS_ASSERT_DIFFERS(i, j); + TS_ASSERT_EQUALS(*i++, 4); TS_ASSERT_DIFFERS(i, l.end()); TS_ASSERT_DIFFERS(i, j); + TS_ASSERT_EQUALS(*i++, 5); TS_ASSERT_DIFFERS(i, l.end()); TS_ASSERT_DIFFERS(i, j); + TS_ASSERT_EQUALS(*i++, 6); TS_ASSERT_EQUALS(i, l.end()); TS_ASSERT_DIFFERS(i, j); + TS_ASSERT_EQUALS(*--i, 6); TS_ASSERT_DIFFERS(i, l.end()); TS_ASSERT_DIFFERS(i, j); + TS_ASSERT_EQUALS(*--i, 5); TS_ASSERT_DIFFERS(i, l.end()); TS_ASSERT_DIFFERS(i, j); + TS_ASSERT_EQUALS(*--i, 4); TS_ASSERT_DIFFERS(i, l.end()); TS_ASSERT_DIFFERS(i, j); + TS_ASSERT_EQUALS(*--i, 3); TS_ASSERT_DIFFERS(i, l.end()); TS_ASSERT_DIFFERS(i, j); + TS_ASSERT_EQUALS(*--i, 2); TS_ASSERT_DIFFERS(i, l.end()); + TS_ASSERT_EQUALS(i, l.begin()); TS_ASSERT_EQUALS(i, j); + + TS_ASSERT_THROWS_NOTHING( l.debugCheck() ); + TS_ASSERT_THROWS_NOTHING( l2.debugCheck() ); + } + d_context->pop(); + + CDCircList<int>::iterator i = l.begin(); + TS_ASSERT_EQUALS(*i, l.front()); TS_ASSERT_DIFFERS(i, l.end()); + TS_ASSERT_EQUALS(*i++, 1); TS_ASSERT_DIFFERS(i, l.end()); + TS_ASSERT_EQUALS(*i++, 2); TS_ASSERT_DIFFERS(i, l.end()); + TS_ASSERT_EQUALS(*i++, 3); TS_ASSERT_DIFFERS(i, l.end()); + TS_ASSERT_EQUALS(*i++, 4); TS_ASSERT_DIFFERS(i, l.end()); + TS_ASSERT_EQUALS(*i++, 5); TS_ASSERT_DIFFERS(i, l.end()); + TS_ASSERT_EQUALS(*i++, 6); TS_ASSERT_EQUALS(i, l.end()); + TS_ASSERT_EQUALS(*--i, 6); TS_ASSERT_DIFFERS(i, l.end()); + TS_ASSERT_EQUALS(*--i, 5); TS_ASSERT_DIFFERS(i, l.end()); + TS_ASSERT_EQUALS(*--i, 4); TS_ASSERT_DIFFERS(i, l.end()); + TS_ASSERT_EQUALS(*--i, 3); TS_ASSERT_DIFFERS(i, l.end()); + TS_ASSERT_EQUALS(*--i, 2); TS_ASSERT_DIFFERS(i, l.end()); + TS_ASSERT_EQUALS(*--i, 1); TS_ASSERT_DIFFERS(i, l.end()); + TS_ASSERT_EQUALS(i, l.begin()); + + i = l2.begin(); + TS_ASSERT_EQUALS(*i, l2.front()); TS_ASSERT_DIFFERS(i, l2.end()); + TS_ASSERT_EQUALS(*i++, 4); TS_ASSERT_DIFFERS(i, l2.end()); + TS_ASSERT_EQUALS(*i++, 5); TS_ASSERT_DIFFERS(i, l2.end()); + TS_ASSERT_EQUALS(*i++, 6); TS_ASSERT_DIFFERS(i, l2.end()); + TS_ASSERT_EQUALS(*i++, 1); TS_ASSERT_DIFFERS(i, l2.end()); + TS_ASSERT_EQUALS(*i++, 2); TS_ASSERT_DIFFERS(i, l2.end()); + TS_ASSERT_EQUALS(*i++, 3); TS_ASSERT_EQUALS(i, l2.end()); + TS_ASSERT_EQUALS(*--i, 3); TS_ASSERT_DIFFERS(i, l2.end()); + TS_ASSERT_EQUALS(*--i, 2); TS_ASSERT_DIFFERS(i, l2.end()); + TS_ASSERT_EQUALS(*--i, 1); TS_ASSERT_DIFFERS(i, l2.end()); + TS_ASSERT_EQUALS(*--i, 6); TS_ASSERT_DIFFERS(i, l2.end()); + TS_ASSERT_EQUALS(*--i, 5); TS_ASSERT_DIFFERS(i, l2.end()); + TS_ASSERT_EQUALS(*--i, 4); TS_ASSERT_DIFFERS(i, l2.end()); + TS_ASSERT_EQUALS(i, l2.begin()); + + TS_ASSERT_THROWS_NOTHING( l.debugCheck() ); + TS_ASSERT_THROWS_NOTHING( l2.debugCheck() ); + } + d_context->pop(); + + TS_ASSERT(! l.empty()); + TS_ASSERT(! l2.empty()); + + CDCircList<int>::iterator i = l.begin(); + TS_ASSERT_EQUALS(*i, l.front()); TS_ASSERT_DIFFERS(i, l.end()); + TS_ASSERT_EQUALS(*i++, 1); TS_ASSERT_DIFFERS(i, l.end()); + TS_ASSERT_EQUALS(*i++, 2); TS_ASSERT_DIFFERS(i, l.end()); + TS_ASSERT_EQUALS(*i++, 3); TS_ASSERT_EQUALS(i, l.end()); + TS_ASSERT_EQUALS(*--i, 3); TS_ASSERT_DIFFERS(i, l.end()); + TS_ASSERT_EQUALS(*--i, 2); TS_ASSERT_DIFFERS(i, l.end()); + TS_ASSERT_EQUALS(*--i, 1); TS_ASSERT_DIFFERS(i, l.end()); + TS_ASSERT_EQUALS(i, l.begin()); + + i = l2.begin(); + TS_ASSERT_EQUALS(*i, l2.front()); TS_ASSERT_DIFFERS(i, l2.end()); + TS_ASSERT_EQUALS(*i++, 4); TS_ASSERT_DIFFERS(i, l2.end()); + TS_ASSERT_EQUALS(*i++, 5); TS_ASSERT_DIFFERS(i, l2.end()); + TS_ASSERT_EQUALS(*i++, 6); TS_ASSERT_EQUALS(i, l2.end()); + TS_ASSERT_EQUALS(*--i, 6); TS_ASSERT_DIFFERS(i, l2.end()); + TS_ASSERT_EQUALS(*--i, 5); TS_ASSERT_DIFFERS(i, l2.end()); + TS_ASSERT_EQUALS(*--i, 4); TS_ASSERT_DIFFERS(i, l2.end()); + TS_ASSERT_EQUALS(i, l2.begin()); + + TS_ASSERT_THROWS_NOTHING( l.debugCheck() ); + TS_ASSERT_THROWS_NOTHING( l2.debugCheck() ); + } + d_context->pop(); + + TS_ASSERT(l.empty()); + TS_ASSERT_THROWS_NOTHING( l.debugCheck() ); + } + + void testCDPtr() { + int* x = (int*)0x12345678; + int* y = (int*)0x87654321; + CDPtr<int> p(d_context, NULL); + TS_ASSERT(p == NULL); + d_context->push(); + TS_ASSERT(p == NULL); + d_context->push(); + TS_ASSERT(p == NULL); + p = x; + TS_ASSERT(p == x); + d_context->push(); + TS_ASSERT(p == x); + p = y; + TS_ASSERT(p == y); + d_context->pop(); + TS_ASSERT(p == x); + d_context->pop(); + TS_ASSERT(p == NULL); + d_context->pop(); + TS_ASSERT(p == NULL); + } + +};/* class CDCircListWhite */ diff --git a/test/unit/context/cdlist_black.h b/test/unit/context/cdlist_black.h index 6541973bf..fcc6a7e55 100644 --- a/test/unit/context/cdlist_black.h +++ b/test/unit/context/cdlist_black.h @@ -5,7 +5,7 @@ ** Major contributors: none ** Minor contributors (to current version): none ** This file is part of the CVC4 prototype. - ** Copyright (c) 2009, 2010 The Analysis of Computer Systems Group (ACSys) + ** Copyright (c) 2009, 2010, 2011 The Analysis of Computer Systems Group (ACSys) ** Courant Institute of Mathematical Sciences ** New York University ** See the file COPYING in the top-level source directory for licensing diff --git a/test/unit/context/cdlist_context_memory_black.h b/test/unit/context/cdlist_context_memory_black.h index 2f3c27ddb..a57fd131d 100644 --- a/test/unit/context/cdlist_context_memory_black.h +++ b/test/unit/context/cdlist_context_memory_black.h @@ -5,7 +5,7 @@ ** Major contributors: none ** Minor contributors (to current version): none ** This file is part of the CVC4 prototype. - ** Copyright (c) 2009, 2010 The Analysis of Computer Systems Group (ACSys) + ** Copyright (c) 2009, 2010, 2011 The Analysis of Computer Systems Group (ACSys) ** Courant Institute of Mathematical Sciences ** New York University ** See the file COPYING in the top-level source directory for licensing diff --git a/test/unit/context/cdmap_black.h b/test/unit/context/cdmap_black.h index 37beb5054..eb2caa98f 100644 --- a/test/unit/context/cdmap_black.h +++ b/test/unit/context/cdmap_black.h @@ -5,7 +5,7 @@ ** Major contributors: none ** Minor contributors (to current version): none ** This file is part of the CVC4 prototype. - ** Copyright (c) 2009, 2010 The Analysis of Computer Systems Group (ACSys) + ** Copyright (c) 2009, 2010, 2011 The Analysis of Computer Systems Group (ACSys) ** Courant Institute of Mathematical Sciences ** New York University ** See the file COPYING in the top-level source directory for licensing diff --git a/test/unit/context/cdmap_white.h b/test/unit/context/cdmap_white.h index a3abd6f25..42f9b8563 100644 --- a/test/unit/context/cdmap_white.h +++ b/test/unit/context/cdmap_white.h @@ -5,7 +5,7 @@ ** Major contributors: none ** Minor contributors (to current version): none ** This file is part of the CVC4 prototype. - ** Copyright (c) 2009, 2010 The Analysis of Computer Systems Group (ACSys) + ** Copyright (c) 2009, 2010, 2011 The Analysis of Computer Systems Group (ACSys) ** Courant Institute of Mathematical Sciences ** New York University ** See the file COPYING in the top-level source directory for licensing diff --git a/test/unit/context/cdo_black.h b/test/unit/context/cdo_black.h index f844c2ef5..6d40a0fb1 100644 --- a/test/unit/context/cdo_black.h +++ b/test/unit/context/cdo_black.h @@ -5,7 +5,7 @@ ** Major contributors: none ** Minor contributors (to current version): none ** This file is part of the CVC4 prototype. - ** Copyright (c) 2009, 2010 The Analysis of Computer Systems Group (ACSys) + ** Copyright (c) 2009, 2010, 2011 The Analysis of Computer Systems Group (ACSys) ** Courant Institute of Mathematical Sciences ** New York University ** See the file COPYING in the top-level source directory for licensing diff --git a/test/unit/context/cdvector_black.h b/test/unit/context/cdvector_black.h index 37a285abe..b49186dd0 100644 --- a/test/unit/context/cdvector_black.h +++ b/test/unit/context/cdvector_black.h @@ -5,7 +5,7 @@ ** Major contributors: mdeters ** Minor contributors (to current version): none ** This file is part of the CVC4 prototype. - ** Copyright (c) 2009, 2010 The Analysis of Computer Systems Group (ACSys) + ** Copyright (c) 2009, 2010, 2011 The Analysis of Computer Systems Group (ACSys) ** Courant Institute of Mathematical Sciences ** New York University ** See the file COPYING in the top-level source directory for licensing diff --git a/test/unit/context/context_black.h b/test/unit/context/context_black.h index e5aee4baa..33863e848 100644 --- a/test/unit/context/context_black.h +++ b/test/unit/context/context_black.h @@ -5,7 +5,7 @@ ** Major contributors: mdeters ** Minor contributors (to current version): none ** This file is part of the CVC4 prototype. - ** Copyright (c) 2009, 2010 The Analysis of Computer Systems Group (ACSys) + ** Copyright (c) 2009, 2010, 2011 The Analysis of Computer Systems Group (ACSys) ** Courant Institute of Mathematical Sciences ** New York University ** See the file COPYING in the top-level source directory for licensing diff --git a/test/unit/context/context_mm_black.h b/test/unit/context/context_mm_black.h index 126245af7..0e5de3198 100644 --- a/test/unit/context/context_mm_black.h +++ b/test/unit/context/context_mm_black.h @@ -5,7 +5,7 @@ ** Major contributors: mdeters ** Minor contributors (to current version): none ** This file is part of the CVC4 prototype. - ** Copyright (c) 2009, 2010 The Analysis of Computer Systems Group (ACSys) + ** Copyright (c) 2009, 2010, 2011 The Analysis of Computer Systems Group (ACSys) ** Courant Institute of Mathematical Sciences ** New York University ** See the file COPYING in the top-level source directory for licensing diff --git a/test/unit/context/context_white.h b/test/unit/context/context_white.h index 38649ef5b..9fb94097d 100644 --- a/test/unit/context/context_white.h +++ b/test/unit/context/context_white.h @@ -5,7 +5,7 @@ ** Major contributors: none ** Minor contributors (to current version): none ** This file is part of the CVC4 prototype. - ** Copyright (c) 2009, 2010 The Analysis of Computer Systems Group (ACSys) + ** Copyright (c) 2009, 2010, 2011 The Analysis of Computer Systems Group (ACSys) ** Courant Institute of Mathematical Sciences ** New York University ** See the file COPYING in the top-level source directory for licensing diff --git a/test/unit/context/stacking_map_black.h b/test/unit/context/stacking_map_black.h new file mode 100644 index 000000000..f0feb1293 --- /dev/null +++ b/test/unit/context/stacking_map_black.h @@ -0,0 +1,161 @@ +/********************* */ +/*! \file stacking_map_black.h + ** \verbatim + ** Original author: mdeters + ** Major contributors: none + ** Minor contributors (to current version): none + ** This file is part of the CVC4 prototype. + ** Copyright (c) 2009, 2010, 2011 The Analysis of Computer Systems Group (ACSys) + ** Courant Institute of Mathematical Sciences + ** New York University + ** 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(d_ctxt, NULL); + d_scope = new NodeManagerScope(d_nm); + d_mapPtr = new StackingMap<TNode, 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_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/context/stacking_vector_black.h b/test/unit/context/stacking_vector_black.h new file mode 100644 index 000000000..5f410881b --- /dev/null +++ b/test/unit/context/stacking_vector_black.h @@ -0,0 +1,161 @@ +/********************* */ +/*! \file stacking_vector_black.h + ** \verbatim + ** Original author: mdeters + ** Major contributors: none + ** Minor contributors (to current version): none + ** This file is part of the CVC4 prototype. + ** Copyright (c) 2009, 2010, 2011 The Analysis of Computer Systems Group (ACSys) + ** Courant Institute of Mathematical Sciences + ** New York University + ** 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(d_ctxt, NULL); + d_scope = new NodeManagerScope(d_nm); + d_vectorPtr = new StackingVector<TNode>(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_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()); + } +}; diff --git a/test/unit/expr/attribute_black.h b/test/unit/expr/attribute_black.h index a324bbbf1..8e7f89795 100644 --- a/test/unit/expr/attribute_black.h +++ b/test/unit/expr/attribute_black.h @@ -5,7 +5,7 @@ ** Major contributors: taking ** Minor contributors (to current version): cconway, mdeters ** This file is part of the CVC4 prototype. - ** Copyright (c) 2009, 2010 The Analysis of Computer Systems Group (ACSys) + ** Copyright (c) 2009, 2010, 2011 The Analysis of Computer Systems Group (ACSys) ** Courant Institute of Mathematical Sciences ** New York University ** See the file COPYING in the top-level source directory for licensing diff --git a/test/unit/expr/declaration_scope_black.h b/test/unit/expr/declaration_scope_black.h index b1e77c614..bde04157c 100644 --- a/test/unit/expr/declaration_scope_black.h +++ b/test/unit/expr/declaration_scope_black.h @@ -5,7 +5,7 @@ ** Major contributors: none ** Minor contributors (to current version): mdeters, dejan ** This file is part of the CVC4 prototype. - ** Copyright (c) 2009, 2010 The Analysis of Computer Systems Group (ACSys) + ** Copyright (c) 2009, 2010, 2011 The Analysis of Computer Systems Group (ACSys) ** Courant Institute of Mathematical Sciences ** New York University ** See the file COPYING in the top-level source directory for licensing diff --git a/test/unit/expr/expr_manager_public.h b/test/unit/expr/expr_manager_public.h index e37c197ab..e709648c9 100644 --- a/test/unit/expr/expr_manager_public.h +++ b/test/unit/expr/expr_manager_public.h @@ -5,7 +5,7 @@ ** Major contributors: none ** Minor contributors (to current version): mdeters ** This file is part of the CVC4 prototype. - ** Copyright (c) 2009, 2010 The Analysis of Computer Systems Group (ACSys) + ** Copyright (c) 2009, 2010, 2011 The Analysis of Computer Systems Group (ACSys) ** Courant Institute of Mathematical Sciences ** New York University ** See the file COPYING in the top-level source directory for licensing diff --git a/test/unit/expr/expr_public.h b/test/unit/expr/expr_public.h index 32e8da287..853d0086b 100644 --- a/test/unit/expr/expr_public.h +++ b/test/unit/expr/expr_public.h @@ -5,7 +5,7 @@ ** Major contributors: cconway, dejan ** Minor contributors (to current version): none ** This file is part of the CVC4 prototype. - ** Copyright (c) 2009, 2010 The Analysis of Computer Systems Group (ACSys) + ** Copyright (c) 2009, 2010, 2011 The Analysis of Computer Systems Group (ACSys) ** Courant Institute of Mathematical Sciences ** New York University ** See the file COPYING in the top-level source directory for licensing diff --git a/test/unit/expr/kind_black.h b/test/unit/expr/kind_black.h index 314108a5b..5cf4ba30a 100644 --- a/test/unit/expr/kind_black.h +++ b/test/unit/expr/kind_black.h @@ -5,7 +5,7 @@ ** Major contributors: none ** Minor contributors (to current version): mdeters ** This file is part of the CVC4 prototype. - ** Copyright (c) 2009, 2010 The Analysis of Computer Systems Group (ACSys) + ** Copyright (c) 2009, 2010, 2011 The Analysis of Computer Systems Group (ACSys) ** Courant Institute of Mathematical Sciences ** New York University ** See the file COPYING in the top-level source directory for licensing diff --git a/test/unit/expr/node_black.h b/test/unit/expr/node_black.h index 6bd5aa1fd..40545e5e8 100644 --- a/test/unit/expr/node_black.h +++ b/test/unit/expr/node_black.h @@ -5,7 +5,7 @@ ** Major contributors: taking ** Minor contributors (to current version): cconway, dejan ** This file is part of the CVC4 prototype. - ** Copyright (c) 2009, 2010 The Analysis of Computer Systems Group (ACSys) + ** Copyright (c) 2009, 2010, 2011 The Analysis of Computer Systems Group (ACSys) ** Courant Institute of Mathematical Sciences ** New York University ** See the file COPYING in the top-level source directory for licensing diff --git a/test/unit/expr/node_builder_black.h b/test/unit/expr/node_builder_black.h index c084c4ecb..c6d6d815e 100644 --- a/test/unit/expr/node_builder_black.h +++ b/test/unit/expr/node_builder_black.h @@ -5,7 +5,7 @@ ** Major contributors: cconway, mdeters ** Minor contributors (to current version): dejan ** This file is part of the CVC4 prototype. - ** Copyright (c) 2009, 2010 The Analysis of Computer Systems Group (ACSys) + ** Copyright (c) 2009, 2010, 2011 The Analysis of Computer Systems Group (ACSys) ** Courant Institute of Mathematical Sciences ** New York University ** See the file COPYING in the top-level source directory for licensing diff --git a/test/unit/expr/node_manager_black.h b/test/unit/expr/node_manager_black.h index e6ebc6724..c30e4badb 100644 --- a/test/unit/expr/node_manager_black.h +++ b/test/unit/expr/node_manager_black.h @@ -5,7 +5,7 @@ ** Major contributors: dejan ** Minor contributors (to current version): taking, mdeters ** This file is part of the CVC4 prototype. - ** Copyright (c) 2009, 2010 The Analysis of Computer Systems Group (ACSys) + ** Copyright (c) 2009, 2010, 2011 The Analysis of Computer Systems Group (ACSys) ** Courant Institute of Mathematical Sciences ** New York University ** See the file COPYING in the top-level source directory for licensing diff --git a/test/unit/expr/node_manager_white.h b/test/unit/expr/node_manager_white.h index 95d3271f2..735fe2ac8 100644 --- a/test/unit/expr/node_manager_white.h +++ b/test/unit/expr/node_manager_white.h @@ -5,7 +5,7 @@ ** Major contributors: none ** Minor contributors (to current version): taking ** This file is part of the CVC4 prototype. - ** Copyright (c) 2009, 2010 The Analysis of Computer Systems Group (ACSys) + ** Copyright (c) 2009, 2010, 2011 The Analysis of Computer Systems Group (ACSys) ** Courant Institute of Mathematical Sciences ** New York University ** See the file COPYING in the top-level source directory for licensing diff --git a/test/unit/expr/node_self_iterator_black.h b/test/unit/expr/node_self_iterator_black.h index e97407dfc..9cc09f884 100644 --- a/test/unit/expr/node_self_iterator_black.h +++ b/test/unit/expr/node_self_iterator_black.h @@ -5,7 +5,7 @@ ** Major contributors: none ** Minor contributors (to current version): none ** This file is part of the CVC4 prototype. - ** Copyright (c) 2009, 2010 The Analysis of Computer Systems Group (ACSys) + ** Copyright (c) 2009, 2010, 2011 The Analysis of Computer Systems Group (ACSys) ** Courant Institute of Mathematical Sciences ** New York University ** See the file COPYING in the top-level source directory for licensing diff --git a/test/unit/expr/node_white.h b/test/unit/expr/node_white.h index 9d6311acb..ce67004c6 100644 --- a/test/unit/expr/node_white.h +++ b/test/unit/expr/node_white.h @@ -5,7 +5,7 @@ ** Major contributors: none ** Minor contributors (to current version): taking, dejan ** This file is part of the CVC4 prototype. - ** Copyright (c) 2009, 2010 The Analysis of Computer Systems Group (ACSys) + ** Copyright (c) 2009, 2010, 2011 The Analysis of Computer Systems Group (ACSys) ** Courant Institute of Mathematical Sciences ** New York University ** See the file COPYING in the top-level source directory for licensing diff --git a/test/unit/main/interactive_shell_black.h b/test/unit/main/interactive_shell_black.h index e56e8de8a..7773644da 100644 --- a/test/unit/main/interactive_shell_black.h +++ b/test/unit/main/interactive_shell_black.h @@ -2,10 +2,10 @@ /*! \file interactive_shell_black.h ** \verbatim ** Original author: cconway - ** Major contributors: - ** Minor contributors (to current version): + ** Major contributors: none + ** Minor contributors (to current version): none ** This file is part of the CVC4 prototype. - ** Copyright (c) 2009, 2010 The Analysis of Computer Systems Group (ACSys) + ** Copyright (c) 2009, 2010, 2011 The Analysis of Computer Systems Group (ACSys) ** Courant Institute of Mathematical Sciences ** New York University ** See the file COPYING in the top-level source directory for licensing diff --git a/test/unit/memory.h b/test/unit/memory.h index 6da3c08b5..19b45c05d 100644 --- a/test/unit/memory.h +++ b/test/unit/memory.h @@ -5,7 +5,7 @@ ** Major contributors: none ** Minor contributors (to current version): none ** This file is part of the CVC4 prototype. - ** Copyright (c) 2009, 2010 The Analysis of Computer Systems Group (ACSys) + ** Copyright (c) 2009, 2010, 2011 The Analysis of Computer Systems Group (ACSys) ** Courant Institute of Mathematical Sciences ** New York University ** See the file COPYING in the top-level source directory for licensing diff --git a/test/unit/parser/parser_builder_black.h b/test/unit/parser/parser_builder_black.h index 06b09f2ce..0f0dc5fbd 100644 --- a/test/unit/parser/parser_builder_black.h +++ b/test/unit/parser/parser_builder_black.h @@ -5,7 +5,7 @@ ** Major contributors: none ** Minor contributors (to current version): mdeters ** This file is part of the CVC4 prototype. - ** Copyright (c) 2009, 2010 The Analysis of Computer Systems Group (ACSys) + ** Copyright (c) 2009, 2010, 2011 The Analysis of Computer Systems Group (ACSys) ** Courant Institute of Mathematical Sciences ** New York University ** See the file COPYING in the top-level source directory for licensing diff --git a/test/unit/prop/cnf_stream_black.h b/test/unit/prop/cnf_stream_black.h index c45740da9..8fb96c74a 100644 --- a/test/unit/prop/cnf_stream_black.h +++ b/test/unit/prop/cnf_stream_black.h @@ -2,10 +2,10 @@ /*! \file cnf_stream_black.h ** \verbatim ** Original author: cconway - ** Major contributors: none - ** Minor contributors (to current version): mdeters, dejan + ** Major contributors: mdeters + ** Minor contributors (to current version): taking, dejan ** This file is part of the CVC4 prototype. - ** Copyright (c) 2009, 2010 The Analysis of Computer Systems Group (ACSys) + ** Copyright (c) 2009, 2010, 2011 The Analysis of Computer Systems Group (ACSys) ** Courant Institute of Mathematical Sciences ** New York University ** See the file COPYING in the top-level source directory for licensing diff --git a/test/unit/theory/shared_term_manager_black.h b/test/unit/theory/shared_term_manager_black.h index 0e8f5addb..1be116517 100644 --- a/test/unit/theory/shared_term_manager_black.h +++ b/test/unit/theory/shared_term_manager_black.h @@ -3,9 +3,9 @@ ** \verbatim ** Original author: barrett ** Major contributors: none - ** Minor contributors (to current version): mdeters + ** Minor contributors (to current version): cconway, mdeters ** This file is part of the CVC4 prototype. - ** Copyright (c) 2009, 2010 The Analysis of Computer Systems Group (ACSys) + ** Copyright (c) 2009, 2010, 2011 The Analysis of Computer Systems Group (ACSys) ** Courant Institute of Mathematical Sciences ** New York University ** See the file COPYING in the top-level source directory for licensing diff --git a/test/unit/theory/stacking_map_black.h b/test/unit/theory/stacking_map_black.h index c60da2922..d70aa8c22 100644 --- a/test/unit/theory/stacking_map_black.h +++ b/test/unit/theory/stacking_map_black.h @@ -5,7 +5,7 @@ ** Major contributors: none ** Minor contributors (to current version): none ** This file is part of the CVC4 prototype. - ** Copyright (c) 2009, 2010 The Analysis of Computer Systems Group (ACSys) + ** Copyright (c) 2009, 2010, 2011 The Analysis of Computer Systems Group (ACSys) ** Courant Institute of Mathematical Sciences ** New York University ** See the file COPYING in the top-level source directory for licensing diff --git a/test/unit/theory/theory_arith_white.h b/test/unit/theory/theory_arith_white.h index fb82a7ac9..ded7cee97 100644 --- a/test/unit/theory/theory_arith_white.h +++ b/test/unit/theory/theory_arith_white.h @@ -3,9 +3,9 @@ ** \verbatim ** Original author: taking ** Major contributors: none - ** Minor contributors (to current version): barrett, mdeters + ** Minor contributors (to current version): mdeters ** This file is part of the CVC4 prototype. - ** Copyright (c) 2009, 2010 The Analysis of Computer Systems Group (ACSys) + ** Copyright (c) 2009, 2010, 2011 The Analysis of Computer Systems Group (ACSys) ** Courant Institute of Mathematical Sciences ** New York University ** See the file COPYING in the top-level source directory for licensing diff --git a/test/unit/theory/theory_black.h b/test/unit/theory/theory_black.h index 2d39af956..ff6b352d0 100644 --- a/test/unit/theory/theory_black.h +++ b/test/unit/theory/theory_black.h @@ -5,7 +5,7 @@ ** Major contributors: barrett, mdeters ** Minor contributors (to current version): none ** This file is part of the CVC4 prototype. - ** Copyright (c) 2009, 2010 The Analysis of Computer Systems Group (ACSys) + ** Copyright (c) 2009, 2010, 2011 The Analysis of Computer Systems Group (ACSys) ** Courant Institute of Mathematical Sciences ** New York University ** See the file COPYING in the top-level source directory for licensing diff --git a/test/unit/theory/theory_engine_white.h b/test/unit/theory/theory_engine_white.h index f1a83cd49..a1b058eeb 100644 --- a/test/unit/theory/theory_engine_white.h +++ b/test/unit/theory/theory_engine_white.h @@ -2,10 +2,10 @@ /*! \file theory_engine_white.h ** \verbatim ** Original author: mdeters - ** Major contributors: none - ** Minor contributors (to current version): barrett, cconway + ** Major contributors: dejan + ** Minor contributors (to current version): taking, cconway ** This file is part of the CVC4 prototype. - ** Copyright (c) 2009, 2010 The Analysis of Computer Systems Group (ACSys) + ** Copyright (c) 2009, 2010, 2011 The Analysis of Computer Systems Group (ACSys) ** Courant Institute of Mathematical Sciences ** New York University ** See the file COPYING in the top-level source directory for licensing diff --git a/test/unit/theory/theory_uf_tim_white.h b/test/unit/theory/theory_uf_tim_white.h deleted file mode 100644 index ae3eee369..000000000 --- a/test/unit/theory/theory_uf_tim_white.h +++ /dev/null @@ -1,252 +0,0 @@ -/********************* */ -/*! \file theory_uf_tim_white.h - ** \verbatim - ** Original author: taking - ** Major contributors: barrett - ** Minor contributors (to current version): cconway, dejan, mdeters - ** This file is part of the CVC4 prototype. - ** Copyright (c) 2009, 2010 The Analysis of Computer Systems Group (ACSys) - ** Courant Institute of Mathematical Sciences - ** New York University - ** See the file COPYING in the top-level source directory for licensing - ** information.\endverbatim - ** - ** \brief White box testing of CVC4::theory::uf::tim::TheoryUFTim. - ** - ** White box testing of CVC4::theory::uf::tim::TheoryUFTim. - **/ - -#include <cxxtest/TestSuite.h> - -#include "theory/theory.h" -#include "theory/uf/theory_uf.h" -#include "theory/uf/tim/theory_uf_tim.h" -#include "expr/node.h" -#include "expr/node_manager.h" -#include "context/context.h" - -#include "theory/theory_test_utils.h" - -#include <vector> - -using namespace CVC4; -using namespace CVC4::theory; -using namespace CVC4::theory::uf; -using namespace CVC4::theory::uf::tim; -using namespace CVC4::expr; -using namespace CVC4::context; - -using namespace std; - - -class TheoryUFTimWhite : public CxxTest::TestSuite { - - Context* d_ctxt; - NodeManager* d_nm; - NodeManagerScope* d_scope; - - TestOutputChannel d_outputChannel; - Theory::Effort d_level; - - TheoryUFTim* d_euf; - - TypeNode* d_booleanType; - -public: - - TheoryUFTimWhite() : d_level(Theory::FULL_EFFORT) {} - - void setUp() { - d_ctxt = new Context; - d_nm = new NodeManager(d_ctxt, NULL); - d_scope = new NodeManagerScope(d_nm); - d_outputChannel.clear(); - d_euf = new TheoryUFTim(d_ctxt, d_outputChannel, Valuation(NULL)); - - d_booleanType = new TypeNode(d_nm->booleanType()); - } - - void tearDown() { - delete d_booleanType; - delete d_euf; - d_outputChannel.clear(); - delete d_scope; - delete d_nm; - delete d_ctxt; - } - - void testPushPopSimple() { - TypeNode t = d_nm->mkSort(); - Node x = d_nm->mkVar(t); - Node x_eq_x = x.eqNode(x); - - d_ctxt->push(); - d_ctxt->pop(); - } - -// FIXME: This is broken because of moving registration into theory_engine @CB -// // void testPushPopChain() { -// // Node x = d_nm->mkVar(*d_booleanType); -// // Node f = d_nm->mkVar(*d_booleanType); -// // Node f_x = d_nm->mkNode(kind::APPLY_UF, f, x); -// // Node f_f_x = d_nm->mkNode(kind::APPLY_UF, f, f_x); -// // Node f_f_f_x = d_nm->mkNode(kind::APPLY_UF, f, f_f_x); -// // Node f_f_f_f_x = d_nm->mkNode(kind::APPLY_UF, f, f_f_f_x); -// // Node f_f_f_f_f_x = d_nm->mkNode(kind::APPLY_UF, f, f_f_f_f_x); - -// // Node f3_x_eq_x = f_f_f_x.eqNode(x); -// // Node f5_x_eq_x = f_f_f_f_f_x.eqNode(x); -// // Node f1_x_neq_x = f_x.eqNode(x).notNode(); - -// // Node expectedConflict = d_nm->mkNode(kind::AND, -// // f1_x_neq_x, -// // f3_x_eq_x, -// // f5_x_eq_x -// // ); - -// // d_euf->assertFact( f3_x_eq_x ); -// // d_euf->assertFact( f1_x_neq_x ); -// // d_euf->check(d_level); -// // d_ctxt->push(); - -// // d_euf->assertFact( f5_x_eq_x ); -// // d_euf->check(d_level); - -// // TS_ASSERT_EQUALS(1u, d_outputChannel.getNumCalls()); -// // TS_ASSERT_EQUALS(CONFLICT, d_outputChannel.getIthCallType(0)); -// // Node realConflict = d_outputChannel.getIthNode(0); -// // TS_ASSERT_EQUALS(expectedConflict, realConflict); - -// // d_ctxt->pop(); -// // d_euf->check(d_level); - -// // //Test that no additional calls to the output channel occurred. -// // TS_ASSERT_EQUALS(1u, d_outputChannel.getNumCalls()); - -// // d_euf->assertFact( f5_x_eq_x ); - -// // d_euf->check(d_level); - -// // TS_ASSERT_EQUALS(2u, d_outputChannel.getNumCalls()); -// // TS_ASSERT_EQUALS(CONFLICT, d_outputChannel.getIthCallType(0)); -// // TS_ASSERT_EQUALS(CONFLICT, d_outputChannel.getIthCallType(1)); -// // Node firstConflict = d_outputChannel.getIthNode(0); -// // Node secondConflict = d_outputChannel.getIthNode(1); -// // TS_ASSERT_EQUALS(expectedConflict, firstConflict); -// // TS_ASSERT_EQUALS(expectedConflict, secondConflict); - -// // } - - - -// /* test that {f(f(x)) == x, f(f(f(x))) != f(x)} is inconsistent */ -// void testSimpleChain() { -// Node x = d_nm->mkVar(*d_booleanType); -// Node f = d_nm->mkVar(*d_booleanType); -// Node f_x = d_nm->mkNode(kind::APPLY_UF, f, x); -// Node f_f_x = d_nm->mkNode(kind::APPLY_UF, f, f_x); -// Node f_f_f_x = d_nm->mkNode(kind::APPLY_UF, f, f_f_x); - -// Node f_f_x_eq_x = f_f_x.eqNode(x); -// Node f_f_f_x_neq_f_x = (f_f_f_x.eqNode(f_x)).notNode(); - -// Node expectedConflict = f_f_f_x_neq_f_x.andNode(f_f_x_eq_x); - -// d_euf->assertFact(f_f_x_eq_x); -// d_euf->assertFact(f_f_f_x_neq_f_x); -// d_euf->check(d_level); - -// TS_ASSERT_EQUALS(1u, d_outputChannel.getNumCalls()); -// TS_ASSERT_EQUALS(CONFLICT, d_outputChannel.getIthCallType(0)); - -// Node realConflict = d_outputChannel.getIthNode(0); -// TS_ASSERT_EQUALS(expectedConflict, realConflict); - -// } - - /* test that !(x == x) is inconsistent */ -// void testSelfInconsistent() { -// Node x = d_nm->mkVar(*d_booleanType); -// Node x_neq_x = (x.eqNode(x)).notNode(); - -// d_euf->assertFact(x_neq_x); -// d_euf->check(d_level); - -// TS_ASSERT_EQUALS(1u, d_outputChannel.getNumCalls()); -// TS_ASSERT_EQUALS(x_neq_x, d_outputChannel.getIthNode(0)); -// TS_ASSERT_EQUALS(CONFLICT, d_outputChannel.getIthCallType(0)); -// } - -// /* test that (x == x) is consistent */ -// void testSelfConsistent() { -// Node x = d_nm->mkVar(*d_booleanType); -// Node x_eq_x = x.eqNode(x); - -// d_euf->assertFact(x_eq_x); -// d_euf->check(d_level); - -// TS_ASSERT_EQUALS(0u, d_outputChannel.getNumCalls()); -// } - - -// /* test that -// {f(f(f(x))) == x, -// f(f(f(f(f(x))))) = x, -// f(x) != x -// } is inconsistent */ -// void testChain() { -// Node x = d_nm->mkVar(*d_booleanType); -// Node f = d_nm->mkVar(*d_booleanType); -// Node f_x = d_nm->mkNode(kind::APPLY_UF, f, x); -// Node f_f_x = d_nm->mkNode(kind::APPLY_UF, f, f_x); -// Node f_f_f_x = d_nm->mkNode(kind::APPLY_UF, f, f_f_x); -// Node f_f_f_f_x = d_nm->mkNode(kind::APPLY_UF, f, f_f_f_x); -// Node f_f_f_f_f_x = d_nm->mkNode(kind::APPLY_UF, f, f_f_f_f_x); - -// Node f3_x_eq_x = f_f_f_x.eqNode(x); -// Node f5_x_eq_x = f_f_f_f_f_x.eqNode(x); -// Node f1_x_neq_x = f_x.eqNode(x).notNode(); - -// Node expectedConflict = d_nm->mkNode(kind::AND, -// f1_x_neq_x, -// f3_x_eq_x, -// f5_x_eq_x -// ); - -// d_euf->assertFact( f3_x_eq_x ); -// d_euf->assertFact( f5_x_eq_x ); -// d_euf->assertFact( f1_x_neq_x ); -// d_euf->check(d_level); - -// TS_ASSERT_EQUALS(1u, d_outputChannel.getNumCalls()); -// TS_ASSERT_EQUALS(CONFLICT, d_outputChannel.getIthCallType(0)); -// Node realConflict = d_outputChannel.getIthNode(0); -// TS_ASSERT_EQUALS(expectedConflict, realConflict); -// } - - -// void testPushPopA() { -// Node x = d_nm->mkVar(*d_booleanType); -// Node x_eq_x = x.eqNode(x); - -// d_ctxt->push(); -// d_euf->assertFact( x_eq_x ); -// d_euf->check(d_level); -// d_ctxt->pop(); -// d_euf->check(d_level); -// } - -// void testPushPopB() { -// Node x = d_nm->mkVar(*d_booleanType); -// Node f = d_nm->mkVar(*d_booleanType); -// Node f_x = d_nm->mkNode(kind::APPLY_UF, f, x); -// Node f_x_eq_x = f_x.eqNode(x); - -// d_euf->assertFact( f_x_eq_x ); -// d_ctxt->push(); -// d_euf->check(d_level); -// d_ctxt->pop(); -// d_euf->check(d_level); -// } - -}; diff --git a/test/unit/theory/union_find_black.h b/test/unit/theory/union_find_black.h index 6ba653946..fead619d2 100644 --- a/test/unit/theory/union_find_black.h +++ b/test/unit/theory/union_find_black.h @@ -5,25 +5,25 @@ ** Major contributors: none ** Minor contributors (to current version): none ** This file is part of the CVC4 prototype. - ** Copyright (c) 2009, 2010 The Analysis of Computer Systems Group (ACSys) + ** Copyright (c) 2009, 2010, 2011 The Analysis of Computer Systems Group (ACSys) ** Courant Institute of Mathematical Sciences ** New York University ** See the file COPYING in the top-level source directory for licensing ** information.\endverbatim ** - ** \brief Black box testing of CVC4::theory::uf::morgan::UnionFind + ** \brief Black box testing of CVC4::datatypes::UnionFind ** - ** Black box testing of CVC4::theory::uf::morgan::UnionFind. + ** Black box testing of CVC4::theory::datatypes::UnionFind. **/ #include <cxxtest/TestSuite.h> #include "context/context.h" #include "expr/node.h" -#include "theory/uf/morgan/union_find.h" +#include "theory/datatypes/union_find.h" using namespace CVC4; -using namespace CVC4::theory::uf::morgan; +using namespace CVC4::theory::datatypes; using namespace CVC4::context; using namespace std; diff --git a/test/unit/util/assert_white.h b/test/unit/util/assert_white.h index 6a8438136..6d88f89bd 100644 --- a/test/unit/util/assert_white.h +++ b/test/unit/util/assert_white.h @@ -5,7 +5,7 @@ ** Major contributors: none ** Minor contributors (to current version): none ** This file is part of the CVC4 prototype. - ** Copyright (c) 2009, 2010 The Analysis of Computer Systems Group (ACSys) + ** Copyright (c) 2009, 2010, 2011 The Analysis of Computer Systems Group (ACSys) ** Courant Institute of Mathematical Sciences ** New York University ** See the file COPYING in the top-level source directory for licensing diff --git a/test/unit/util/configuration_black.h b/test/unit/util/configuration_black.h index e06fe9636..faafb28f7 100644 --- a/test/unit/util/configuration_black.h +++ b/test/unit/util/configuration_black.h @@ -5,7 +5,7 @@ ** Major contributors: none ** Minor contributors (to current version): none ** This file is part of the CVC4 prototype. - ** Copyright (c) 2009, 2010 The Analysis of Computer Systems Group (ACSys) + ** Copyright (c) 2009, 2010, 2011 The Analysis of Computer Systems Group (ACSys) ** Courant Institute of Mathematical Sciences ** New York University ** See the file COPYING in the top-level source directory for licensing diff --git a/test/unit/util/congruence_closure_white.h b/test/unit/util/congruence_closure_white.h index f5e299377..187b7dc08 100644 --- a/test/unit/util/congruence_closure_white.h +++ b/test/unit/util/congruence_closure_white.h @@ -5,7 +5,7 @@ ** Major contributors: none ** Minor contributors (to current version): none ** This file is part of the CVC4 prototype. - ** Copyright (c) 2009, 2010 The Analysis of Computer Systems Group (ACSys) + ** Copyright (c) 2009, 2010, 2011 The Analysis of Computer Systems Group (ACSys) ** Courant Institute of Mathematical Sciences ** New York University ** See the file COPYING in the top-level source directory for licensing diff --git a/test/unit/util/datatype_black.h b/test/unit/util/datatype_black.h index 485820a61..ea8d8a900 100644 --- a/test/unit/util/datatype_black.h +++ b/test/unit/util/datatype_black.h @@ -3,7 +3,7 @@ ** \verbatim ** Original author: mdeters ** Major contributors: none - ** Minor contributors (to current version): none + ** Minor contributors (to current version): ajreynol ** This file is part of the CVC4 prototype. ** Copyright (c) 2009, 2010, 2011 The Analysis of Computer Systems Group (ACSys) ** Courant Institute of Mathematical Sciences diff --git a/test/unit/util/exception_black.h b/test/unit/util/exception_black.h index 2bbd727fb..f92b6af93 100644 --- a/test/unit/util/exception_black.h +++ b/test/unit/util/exception_black.h @@ -5,7 +5,7 @@ ** Major contributors: none ** Minor contributors (to current version): none ** This file is part of the CVC4 prototype. - ** Copyright (c) 2009, 2010 The Analysis of Computer Systems Group (ACSys) + ** Copyright (c) 2009, 2010, 2011 The Analysis of Computer Systems Group (ACSys) ** Courant Institute of Mathematical Sciences ** New York University ** See the file COPYING in the top-level source directory for licensing diff --git a/test/unit/util/integer_black.h b/test/unit/util/integer_black.h index 5b8397f66..92846bdf1 100644 --- a/test/unit/util/integer_black.h +++ b/test/unit/util/integer_black.h @@ -2,10 +2,10 @@ /*! \file integer_black.h ** \verbatim ** Original author: taking - ** Major contributors: none - ** Minor contributors (to current version): cconway, mdeters + ** Major contributors: mdeters + ** Minor contributors (to current version): cconway ** This file is part of the CVC4 prototype. - ** Copyright (c) 2009, 2010 The Analysis of Computer Systems Group (ACSys) + ** Copyright (c) 2009, 2010, 2011 The Analysis of Computer Systems Group (ACSys) ** Courant Institute of Mathematical Sciences ** New York University ** See the file COPYING in the top-level source directory for licensing diff --git a/test/unit/util/integer_white.h b/test/unit/util/integer_white.h index 1c6b03cdf..284c94670 100644 --- a/test/unit/util/integer_white.h +++ b/test/unit/util/integer_white.h @@ -5,7 +5,7 @@ ** Major contributors: mdeters ** Minor contributors (to current version): none ** This file is part of the CVC4 prototype. - ** Copyright (c) 2009, 2010 The Analysis of Computer Systems Group (ACSys) + ** Copyright (c) 2009, 2010, 2011 The Analysis of Computer Systems Group (ACSys) ** Courant Institute of Mathematical Sciences ** New York University ** See the file COPYING in the top-level source directory for licensing diff --git a/test/unit/util/rational_black.h b/test/unit/util/rational_black.h index dcae800d1..66d119567 100644 --- a/test/unit/util/rational_black.h +++ b/test/unit/util/rational_black.h @@ -5,7 +5,7 @@ ** Major contributors: mdeters ** Minor contributors (to current version): none ** This file is part of the CVC4 prototype. - ** Copyright (c) 2009, 2010 The Analysis of Computer Systems Group (ACSys) + ** Copyright (c) 2009, 2010, 2011 The Analysis of Computer Systems Group (ACSys) ** Courant Institute of Mathematical Sciences ** New York University ** See the file COPYING in the top-level source directory for licensing diff --git a/test/unit/util/rational_white.h b/test/unit/util/rational_white.h index 2fcb33642..b5d120c52 100644 --- a/test/unit/util/rational_white.h +++ b/test/unit/util/rational_white.h @@ -5,7 +5,7 @@ ** Major contributors: none ** Minor contributors (to current version): mdeters ** This file is part of the CVC4 prototype. - ** Copyright (c) 2009, 2010 The Analysis of Computer Systems Group (ACSys) + ** Copyright (c) 2009, 2010, 2011 The Analysis of Computer Systems Group (ACSys) ** Courant Institute of Mathematical Sciences ** New York University ** See the file COPYING in the top-level source directory for licensing diff --git a/test/unit/util/stats_black.h b/test/unit/util/stats_black.h index d32ef828c..7ba88edc6 100644 --- a/test/unit/util/stats_black.h +++ b/test/unit/util/stats_black.h @@ -5,7 +5,7 @@ ** Major contributors: none ** Minor contributors (to current version): none ** This file is part of the CVC4 prototype. - ** Copyright (c) 2009, 2010 The Analysis of Computer Systems Group (ACSys) + ** Copyright (c) 2009, 2010, 2011 The Analysis of Computer Systems Group (ACSys) ** Courant Institute of Mathematical Sciences ** New York University ** See the file COPYING in the top-level source directory for licensing diff --git a/test/unit/util/trans_closure_black.h b/test/unit/util/trans_closure_black.h index dfa066194..251e47a17 100644 --- a/test/unit/util/trans_closure_black.h +++ b/test/unit/util/trans_closure_black.h @@ -5,7 +5,7 @@ ** Major contributors: none ** Minor contributors (to current version): none ** This file is part of the CVC4 prototype. - ** Copyright (c) 2009, 2010 The Analysis of Computer Systems Group (ACSys) + ** Copyright (c) 2009, 2010, 2011 The Analysis of Computer Systems Group (ACSys) ** Courant Institute of Mathematical Sciences ** New York University ** See the file COPYING in the top-level source directory for licensing |