diff options
author | Dejan Jovanović <dejan.jovanovic@gmail.com> | 2010-03-12 23:41:12 +0000 |
---|---|---|
committer | Dejan Jovanović <dejan.jovanovic@gmail.com> | 2010-03-12 23:41:12 +0000 |
commit | 856567b63c56b238db8a5bb84ad0da7990c1f1eb (patch) | |
tree | ab2a453f926b56070c39b9afba02dba7ba59858d /test/unit | |
parent | 20b3dabb4823ede8147a08a47f8d909980414bee (diff) |
Fixing unnecessary construction of NOT nodes when generating conflict clauses and:
* adding the smallest test case (eq_diamond23.smt) that memouts in 50s
* adding the initial attributes black box test
Diffstat (limited to 'test/unit')
-rw-r--r-- | test/unit/Makefile.am | 1 | ||||
-rw-r--r-- | test/unit/expr/attribute_black.h | 86 |
2 files changed, 87 insertions, 0 deletions
diff --git a/test/unit/Makefile.am b/test/unit/Makefile.am index 9d1a2995b..305731f5b 100644 --- a/test/unit/Makefile.am +++ b/test/unit/Makefile.am @@ -4,6 +4,7 @@ UNIT_TESTS = \ expr/node_black \ expr/kind_black \ expr/node_builder_black \ + expr/attribute_black \ parser/parser_black \ context/context_black \ context/context_mm_black \ diff --git a/test/unit/expr/attribute_black.h b/test/unit/expr/attribute_black.h new file mode 100644 index 000000000..b5e897e89 --- /dev/null +++ b/test/unit/expr/attribute_black.h @@ -0,0 +1,86 @@ +/********************* */ +/** node_black.h + ** Original author: mdeters + ** Major contributors: taking + ** 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. + ** + ** Black box testing of CVC4::Node. + **/ + +#include <cxxtest/TestSuite.h> + +//Used in some of the tests +#include <vector> +#include <sstream> + +#include "expr/expr_manager.h" +#include "expr/node_value.h" +#include "expr/node_builder.h" +#include "expr/node_manager.h" +#include "expr/node.h" +#include "expr/attribute.h" + +using namespace CVC4; +using namespace CVC4::kind; +using namespace CVC4::context; +using namespace std; + +class AttributeBlack : public CxxTest::TestSuite { +private: + + Context* d_ctxt; + NodeManager* d_nodeManager; + NodeManagerScope* d_scope; + +public: + + void setUp() { + d_ctxt = new Context; + d_nodeManager = new NodeManager(d_ctxt); + d_scope = new NodeManagerScope(d_nodeManager); + } + + void tearDown() { + delete d_scope; + delete d_nodeManager; + delete d_ctxt; + } + + class MyData { + public: + static int count; + MyData() { count ++; } + ~MyData() { count --; } + }; + + struct MyDataAttributeId {}; + + struct MyDataCleanupFunction { + static void cleanup(MyData*& myData){ + delete myData; + } + }; + + typedef expr::Attribute<MyDataAttributeId, MyData*, MyDataCleanupFunction> MyDataAttribute; + + void testDeallocation() { + Node* node = new Node(d_nodeManager->mkVar()); + MyData* data; + MyData* data1; + MyDataAttribute attr; + TS_ASSERT(!node->hasAttribute(attr, data)); + node->setAttribute(attr, new MyData()); + TS_ASSERT(node->hasAttribute(attr, data1)); + TS_ASSERT(MyData::count == 1); + delete node; + } + +}; + +int AttributeBlack::MyData::count = 0; |