summaryrefslogtreecommitdiff
path: root/test/unit/theory
diff options
context:
space:
mode:
Diffstat (limited to 'test/unit/theory')
-rw-r--r--test/unit/theory/shared_term_manager_black.h4
-rw-r--r--test/unit/theory/stacking_map_black.h2
-rw-r--r--test/unit/theory/theory_arith_white.h4
-rw-r--r--test/unit/theory/theory_black.h2
-rw-r--r--test/unit/theory/theory_engine_white.h6
-rw-r--r--test/unit/theory/theory_uf_tim_white.h252
-rw-r--r--test/unit/theory/union_find_black.h10
7 files changed, 14 insertions, 266 deletions
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;
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback