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 | |
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')
-rw-r--r-- | test/regress/regress0/uf/Makefile.am | 1 | ||||
-rw-r--r-- | test/unit/Makefile.am | 2 | ||||
-rw-r--r-- | test/unit/theory/stacking_map_black.h | 160 | ||||
-rw-r--r-- | test/unit/theory/union_find_black.h | 189 |
4 files changed, 352 insertions, 0 deletions
diff --git a/test/regress/regress0/uf/Makefile.am b/test/regress/regress0/uf/Makefile.am index 1471d8814..2e05386e0 100644 --- a/test/regress/regress0/uf/Makefile.am +++ b/test/regress/regress0/uf/Makefile.am @@ -19,6 +19,7 @@ TESTS = \ eq_diamond1.smt \ eq_diamond14.reduced.smt \ eq_diamond14.reduced2.smt \ + eq_diamond23.smt \ NEQ016_size5_reduced2a.smt \ NEQ016_size5_reduced2b.smt \ dead_dnd002.smt \ diff --git a/test/unit/Makefile.am b/test/unit/Makefile.am index 3583770b6..725d4a4bb 100644 --- a/test/unit/Makefile.am +++ b/test/unit/Makefile.am @@ -5,6 +5,8 @@ UNIT_TESTS = \ 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 \ expr/node_white \ 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()); + } +}; diff --git a/test/unit/theory/union_find_black.h b/test/unit/theory/union_find_black.h new file mode 100644 index 000000000..b9b4e58ce --- /dev/null +++ b/test/unit/theory/union_find_black.h @@ -0,0 +1,189 @@ +/********************* */ +/*! \file union_find_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::UnionFind + ** + ** Black box testing of CVC4::theory::uf::morgan::UnionFind. + **/ + +#include <cxxtest/TestSuite.h> + +#include "context/context.h" +#include "expr/node.h" +#include "theory/uf/morgan/union_find.h" + +using namespace CVC4; +using namespace CVC4::theory::uf::morgan; +using namespace CVC4::context; + +using namespace std; + +/** + * Test the UnionFind. + */ +class UnionFindBlack : public CxxTest::TestSuite { + Context* d_ctxt; + UnionFind<TNode, TNodeHashFunction>* d_uf; + 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_uf = new UnionFind<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_uf; + delete d_scope; + delete d_nm; + delete d_ctxt; + } + + void testSimpleContextual() { + TS_ASSERT(d_uf->find(a) == a); + TS_ASSERT(d_uf->find(b) == b); + TS_ASSERT(d_uf->find(c) == c); + TS_ASSERT(d_uf->find(d) == d); + TS_ASSERT(d_uf->find(e) == e); + TS_ASSERT(d_uf->find(f) == f); + TS_ASSERT(d_uf->find(g) == g); + + d_ctxt->push(); + + d_uf->setCanon(a, b); + + TS_ASSERT(d_uf->find(a) == b); + TS_ASSERT(d_uf->find(b) == b); + TS_ASSERT(d_uf->find(c) == c); + TS_ASSERT(d_uf->find(d) == d); + TS_ASSERT(d_uf->find(e) == e); + TS_ASSERT(d_uf->find(f) == f); + TS_ASSERT(d_uf->find(g) == g); + + d_ctxt->push(); + { + TS_ASSERT(d_uf->find(a) == b); + TS_ASSERT(d_uf->find(b) == b); + TS_ASSERT(d_uf->find(c) == c); + TS_ASSERT(d_uf->find(d) == d); + TS_ASSERT(d_uf->find(e) == e); + TS_ASSERT(d_uf->find(f) == f); + TS_ASSERT(d_uf->find(g) == g); + + d_uf->setCanon(c, d); + d_uf->setCanon(f, e); + + TS_ASSERT(d_uf->find(a) == b); + TS_ASSERT(d_uf->find(b) == b); + TS_ASSERT(d_uf->find(c) == d); + TS_ASSERT(d_uf->find(d) == d); + TS_ASSERT(d_uf->find(e) == e); + TS_ASSERT(d_uf->find(f) == e); + TS_ASSERT(d_uf->find(g) == g); + + d_ctxt->push(); + { + + TS_ASSERT(d_uf->find(a) == b); + TS_ASSERT(d_uf->find(b) == b); + TS_ASSERT(d_uf->find(c) == d); + TS_ASSERT(d_uf->find(d) == d); + TS_ASSERT(d_uf->find(e) == e); + TS_ASSERT(d_uf->find(f) == e); + TS_ASSERT(d_uf->find(g) == g); + +#ifdef CVC4_ASSERTIONS + TS_ASSERT_THROWS(d_uf->setCanon(a, c), AssertionException); + TS_ASSERT_THROWS(d_uf->setCanon(d_uf->find(a), c), AssertionException); + TS_ASSERT_THROWS(d_uf->setCanon(a, d_uf->find(c)), AssertionException); +#endif /* CVC4_ASSERTIONS */ + d_uf->setCanon(d_uf->find(a), d_uf->find(c)); + d_uf->setCanon(d_uf->find(f), g); + d_uf->setCanon(d_uf->find(e), d); +#ifdef CVC4_ASSERTIONS + TS_ASSERT_THROWS(d_uf->setCanon(d_uf->find(c), f), AssertionException); +#endif /* CVC4_ASSERTIONS */ + d_uf->setCanon(d_uf->find(c), d_uf->find(f)); + + TS_ASSERT(d_uf->find(a) == d); + TS_ASSERT(d_uf->find(b) == d); + TS_ASSERT(d_uf->find(c) == d); + TS_ASSERT(d_uf->find(d) == d); + TS_ASSERT(d_uf->find(e) == d); + TS_ASSERT(d_uf->find(f) == d); + TS_ASSERT(d_uf->find(g) == d); + + d_uf->setCanon(d_uf->find(g), d_uf->find(a)); + + TS_ASSERT(d_uf->find(a) == d); + TS_ASSERT(d_uf->find(b) == d); + TS_ASSERT(d_uf->find(c) == d); + TS_ASSERT(d_uf->find(d) == d); + TS_ASSERT(d_uf->find(e) == d); + TS_ASSERT(d_uf->find(f) == d); + TS_ASSERT(d_uf->find(g) == d); + + } + d_ctxt->pop(); + + TS_ASSERT(d_uf->find(a) == b); + TS_ASSERT(d_uf->find(b) == b); + TS_ASSERT(d_uf->find(c) == d); + TS_ASSERT(d_uf->find(d) == d); + TS_ASSERT(d_uf->find(e) == e); + TS_ASSERT(d_uf->find(f) == e); + TS_ASSERT(d_uf->find(g) == g); + } + d_ctxt->pop(); + + TS_ASSERT(d_uf->find(a) == b); + TS_ASSERT(d_uf->find(b) == b); + TS_ASSERT(d_uf->find(c) == c); + TS_ASSERT(d_uf->find(d) == d); + TS_ASSERT(d_uf->find(e) == e); + TS_ASSERT(d_uf->find(f) == f); + TS_ASSERT(d_uf->find(g) == g); + + d_ctxt->pop(); + + TS_ASSERT(d_uf->find(a) == a); + TS_ASSERT(d_uf->find(b) == b); + TS_ASSERT(d_uf->find(c) == c); + TS_ASSERT(d_uf->find(d) == d); + TS_ASSERT(d_uf->find(e) == e); + TS_ASSERT(d_uf->find(f) == f); + TS_ASSERT(d_uf->find(g) == g); + } +}; |