minor fixups

3 files changed, 111 insertions, 0 deletions

diff --git a/test/regress/regress0/uf/Makefile.am b/test/regress/regress0/uf/Makefile.am
index 45cf22232..01eaee999 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 cef4590a3..f98f434c1 100644
--- a/test/unit/Makefile.am
+++ b/test/unit/Makefile.am
@@ -12,6 +12,7 @@ UNIT_TESTS = \
 	expr/node_white \
 	expr/node_black \
 	expr/kind_black \
+	expr/kind_map_black \
 	expr/node_builder_black \
 	expr/node_manager_black \
 	expr/node_manager_white \
diff --git a/test/unit/expr/kind_map_black.h b/test/unit/expr/kind_map_black.h
new file mode 100644
index 000000000..e5bcdd298
--- /dev/null
+++ b/test/unit/expr/kind_map_black.h
@@ -0,0 +1,109 @@
+/*********************                                                        */
+/*! \file kind_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::KindMap
+ **
+ ** Black box testing of CVC4::KindMap.
+ **/
+
+#include <cxxtest/TestSuite.h>
+
+#include <iostream>
+#include <string>
+#include <sstream>
+
+#include "expr/kind_map.h"
+
+using namespace CVC4;
+using namespace CVC4::kind;
+using namespace std;
+
+class KindMapBlack : public CxxTest::TestSuite {
+
+public:
+
+  void testSimple() {
+    KindMap map;
+    TS_ASSERT(map.isEmpty());
+    map.set(AND);
+    TS_ASSERT(!map.isEmpty());
+    KindMap map2 = map;
+    TS_ASSERT(!map2.isEmpty());
+    TS_ASSERT_EQUALS(map, map2);
+    TS_ASSERT(map.tst(AND));
+    TS_ASSERT(map2.tst(AND));
+    TS_ASSERT(!map.tst(OR));
+    TS_ASSERT(!map2.tst(OR));
+    map2 = ~map2;
+    TS_ASSERT(map2.tst(OR));
+    TS_ASSERT(!map2.tst(AND));
+    TS_ASSERT(map != map2);
+    TS_ASSERT(map.begin() != map.end());
+    TS_ASSERT(map2.begin() != map2.end());
+    map &= ~AND;
+    TS_ASSERT(map.isEmpty());
+    map2.clear();
+    TS_ASSERT(map2.isEmpty());
+    TS_ASSERT_EQUALS(map2, map);
+    TS_ASSERT_EQUALS(map.begin(), map.end());
+    TS_ASSERT_EQUALS(map2.begin(), map2.end());
+  }
+
+  void testIteration() {
+    KindMap m = AND & OR;
+    TS_ASSERT(m.isEmpty());
+    for(KindMap::iterator i = m.begin(); i != m.end(); ++i) {
+      TS_FAIL("expected empty iterator range");
+    }
+    m = AND | OR;
+    KindMap::iterator i = m.begin();
+    TS_ASSERT(i != m.end());
+    TS_ASSERT_EQUALS(*i, AND);
+    ++i;
+    TS_ASSERT(i != m.end());
+    TS_ASSERT_EQUALS(*i, OR);
+    ++i;
+    TS_ASSERT(i == m.end());
+
+    m = ~m;
+    unsigned k = 0;
+    for(i = m.begin(); i != m.end(); ++i, ++k) {
+      while(k == AND || k == OR) {
+        ++k;
+      }
+      TS_ASSERT_DIFFERS(Kind(k), UNDEFINED_KIND);
+      TS_ASSERT_DIFFERS(Kind(k), LAST_KIND);
+      TS_ASSERT_EQUALS(*i, Kind(k));
+    }
+  }
+
+  void testConstruction() {
+    TS_ASSERT(!(AND & AND).isEmpty());
+    TS_ASSERT((AND & ~AND).isEmpty());
+    TS_ASSERT(!(AND & AND & AND).isEmpty());
+
+    TS_ASSERT(!(AND | AND).isEmpty());
+    TS_ASSERT(!(AND | ~AND).isEmpty());
+    TS_ASSERT(((AND | AND) & ~AND).isEmpty());
+    TS_ASSERT(!((AND | OR) & ~AND).isEmpty());
+
+    TS_ASSERT((AND ^ AND).isEmpty());
+    TS_ASSERT(!(AND ^ OR).isEmpty());
+    TS_ASSERT(!(AND ^ AND ^ AND).isEmpty());
+
+#ifdef CVC4_ASSERTIONS
+    TS_ASSERT_THROWS(~LAST_KIND, IllegalArgumentException);
+#endif /* CVC4_ASSERTIONS */
+  }
+
+};/* class KindMapBlack */