diff options
author | Morgan Deters <mdeters@gmail.com> | 2010-11-19 01:37:55 +0000 |
---|---|---|
committer | Morgan Deters <mdeters@gmail.com> | 2010-11-19 01:37:55 +0000 |
commit | 663a6edef6b65d400e2d97dc9c8276da3d3cb0b1 (patch) | |
tree | 29c7782beaf37ea855b9bc9436d61e94f60c9393 /test/unit/theory/stacking_map_black.h | |
parent | c21ad20770c41ece116c182d97e0ef824e7b26f4 (diff) |
Merge from ufprop branch, including:
* Theory::staticLearning() for statically adding new T-stuff before
normal preprocessing. UF's staticLearning() does transitivity of
equality/iff, solving the diamonds.
* more aggressive T-propagation for UF
* new KEEP_STATISTIC macro to hide Theories from having to
register/deregister statistics (and also has the advantage of
keeping the statistic type, field name, and the 'tag' used to output
the statistic in the same place---instead of scattered in the theory
definition and constructor initializer list. See documentation for
KEEP_STATISTIC in src/util/stats.h for more of an explanation).
* more statistics for UF
* restart notifications from SAT (through TheoryEngine) via
Theory::notifyRestart()
* StackingMap and UnionFind unit tests
* build fixes/adjustments
* code cleanup; minor other improvements
Diffstat (limited to 'test/unit/theory/stacking_map_black.h')
-rw-r--r-- | test/unit/theory/stacking_map_black.h | 160 |
1 files changed, 160 insertions, 0 deletions
diff --git a/test/unit/theory/stacking_map_black.h b/test/unit/theory/stacking_map_black.h new file mode 100644 index 000000000..39dad4732 --- /dev/null +++ b/test/unit/theory/stacking_map_black.h @@ -0,0 +1,160 @@ +/********************* */ +/*! \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 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::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); + 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()); + } +}; |