diff options
author | Andrew Reynolds <andrew.j.reynolds@gmail.com> | 2012-07-27 21:07:42 +0000 |
---|---|---|
committer | Andrew Reynolds <andrew.j.reynolds@gmail.com> | 2012-07-27 21:07:42 +0000 |
commit | 33fd76601b42599d9883889a03d59d0d85729661 (patch) | |
tree | 57072e562d7639d9fe444e18c313330f6907a5a1 /test | |
parent | 9a994c449d65e64d574a423ad9caad519f8c2148 (diff) |
removing unecessary files
Diffstat (limited to 'test')
-rw-r--r-- | test/unit/Makefile.am | 2 | ||||
-rw-r--r-- | test/unit/theory/union_find_black.h | 189 | ||||
-rw-r--r-- | test/unit/util/congruence_closure_white.h | 529 |
3 files changed, 0 insertions, 720 deletions
diff --git a/test/unit/Makefile.am b/test/unit/Makefile.am index d5b6ce5bf..1ab00bf8d 100644 --- a/test/unit/Makefile.am +++ b/test/unit/Makefile.am @@ -4,7 +4,6 @@ UNIT_TESTS = \ theory/theory_engine_white \ theory/theory_white \ theory/theory_arith_white \ - theory/union_find_black \ theory/theory_bv_white \ theory/type_enumerator_white \ expr/expr_public \ @@ -41,7 +40,6 @@ UNIT_TESTS = \ util/bitvector_black \ util/datatype_black \ util/configuration_black \ - util/congruence_closure_white \ util/output_black \ util/exception_black \ util/integer_black \ diff --git a/test/unit/theory/union_find_black.h b/test/unit/theory/union_find_black.h deleted file mode 100644 index fead619d2..000000000 --- a/test/unit/theory/union_find_black.h +++ /dev/null @@ -1,189 +0,0 @@ -/********************* */ -/*! \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, 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::datatypes::UnionFind - ** - ** Black box testing of CVC4::theory::datatypes::UnionFind. - **/ - -#include <cxxtest/TestSuite.h> - -#include "context/context.h" -#include "expr/node.h" -#include "theory/datatypes/union_find.h" - -using namespace CVC4; -using namespace CVC4::theory::datatypes; -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, NULL); - 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); - } -}; diff --git a/test/unit/util/congruence_closure_white.h b/test/unit/util/congruence_closure_white.h deleted file mode 100644 index 0c14160f7..000000000 --- a/test/unit/util/congruence_closure_white.h +++ /dev/null @@ -1,529 +0,0 @@ -/********************* */ -/*! \file congruence_closure_white.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 White box testing of CVC4::CongruenceClosure. - ** - ** White box testing of CVC4::CongruenceClosure. - **/ - -#include <cxxtest/TestSuite.h> -#include <sstream> - -#include "context/context.h" -#include "context/cdhashset.h" -#include "context/cdhashmap.h" -#include "expr/node.h" -#include "expr/kind.h" -#include "expr/node_manager.h" -#include "util/congruence_closure.h" - - -using namespace CVC4; -using namespace CVC4::context; -using namespace std; - - -struct MyOutputChannel { - CDHashSet<Node, NodeHashFunction> d_notifications; - CDHashMap<Node, Node, NodeHashFunction> d_equivalences; - NodeManager* d_nm; - - MyOutputChannel(Context* ctxt, NodeManager* nm) : - d_notifications(ctxt), - d_equivalences(ctxt), - d_nm(nm) { - } - - bool saw(TNode a, TNode b) { - return d_notifications.contains(d_nm->mkNode(kind::EQUAL, a, b)) || - d_notifications.contains(d_nm->mkNode(kind::EQUAL, b, a)); - } - - TNode find(TNode n) { - CDHashMap<Node, Node, NodeHashFunction>::iterator i = d_equivalences.find(n); - if(i == d_equivalences.end()) { - return n; - } else { - // lazy path compression - TNode p = (*i).second; // parent - TNode f = d_equivalences[n] = find(p); // compress - return f; - } - } - - bool areCongruent(TNode a, TNode b) { - Debug("cc") << "=== a is " << a << std::endl - << "=== a' is " << find(a) << std::endl - << "=== b is " << b << std::endl - << "=== b' is " << find(b) << std::endl; - - return find(a) == find(b); - } - - void notifyCongruent(TNode a, TNode b) { - Debug("cc") << "======OI! I've been notified of: " - << a << " == " << b << std::endl; - - Node eq = d_nm->mkNode(kind::EQUAL, a, b); - Node eqRev = d_nm->mkNode(kind::EQUAL, b, a); - - TS_ASSERT(!d_notifications.contains(eq)); - TS_ASSERT(!d_notifications.contains(eqRev)); - - d_notifications.insert(eq); - - d_equivalences.insert(a, b); - } -};/* class MyOutputChannel */ - - -class CongruenceClosureWhite : public CxxTest::TestSuite { - Context* d_context; - NodeManager* d_nm; - NodeManagerScope* d_scope; - MyOutputChannel* d_out; - CongruenceClosure<MyOutputChannel, CongruenceOperator<kind::APPLY_UF> >* d_cc; - CongruenceClosure<MyOutputChannel, CONGRUENCE_OPERATORS_2(kind::SELECT, kind::STORE)>* d_ccArray; - - TypeNode U; - Node a, f, fa, ffa, fffa, ffffa, b, fb, ffb, fffb, ffffb; - Node g, gab, gba, gfafb, gfbfa, gfaa, gbfb; - Node h, hab, hba, hfaa; - Node a_eq_b, fa_eq_b, a_eq_fb, fa_eq_fb, h_eq_g; - - Node ar, ar_a, ar_b; - Node arar, arar_a, arar_b; - -public: - - void setUp() { - d_context = new Context; - d_nm = new NodeManager(d_context, NULL); - d_scope = new NodeManagerScope(d_nm); - d_out = new MyOutputChannel(d_context, d_nm); - d_cc = new CongruenceClosure<MyOutputChannel, CongruenceOperator<kind::APPLY_UF> >(d_context, d_out); - d_ccArray = new CongruenceClosure<MyOutputChannel, CONGRUENCE_OPERATORS_2(kind::SELECT, kind::STORE)>(d_context, d_out); - - U = d_nm->mkSort("U"); - - f = d_nm->mkVar("f", d_nm->mkFunctionType(U, U)); - a = d_nm->mkVar("a", U); - fa = d_nm->mkNode(kind::APPLY_UF, f, a); - ffa = d_nm->mkNode(kind::APPLY_UF, f, fa); - fffa = d_nm->mkNode(kind::APPLY_UF, f, ffa); - ffffa = d_nm->mkNode(kind::APPLY_UF, f, fffa); - b = d_nm->mkVar("b", U); - fb = d_nm->mkNode(kind::APPLY_UF, f, b); - ffb = d_nm->mkNode(kind::APPLY_UF, f, fb); - fffb = d_nm->mkNode(kind::APPLY_UF, f, ffb); - ffffb = d_nm->mkNode(kind::APPLY_UF, f, fffb); - vector<TypeNode> args(2, U); - g = d_nm->mkVar("g", d_nm->mkFunctionType(args, U)); - gab = d_nm->mkNode(kind::APPLY_UF, g, a, b); - gfafb = d_nm->mkNode(kind::APPLY_UF, g, fa, fb); - gba = d_nm->mkNode(kind::APPLY_UF, g, b, a); - gfbfa = d_nm->mkNode(kind::APPLY_UF, g, fb, fa); - gfaa = d_nm->mkNode(kind::APPLY_UF, g, fa, a); - gbfb = d_nm->mkNode(kind::APPLY_UF, g, b, fb); - h = d_nm->mkVar("h", d_nm->mkFunctionType(args, U)); - hab = d_nm->mkNode(kind::APPLY_UF, h, a, b); - hba = d_nm->mkNode(kind::APPLY_UF, h, b, a); - hfaa = d_nm->mkNode(kind::APPLY_UF, h, fa, a); - - a_eq_b = d_nm->mkNode(kind::EQUAL, a, b); - fa_eq_b = d_nm->mkNode(kind::EQUAL, fa, b); - a_eq_fb = d_nm->mkNode(kind::EQUAL, a, fb); - fa_eq_fb = d_nm->mkNode(kind::EQUAL, fa, fb); - - h_eq_g = d_nm->mkNode(kind::EQUAL, h, g); - - // arrays - ar = d_nm->mkVar("ar", d_nm->mkArrayType(U, U)); - ar_a = d_nm->mkNode(kind::SELECT, ar, a); - ar_b = d_nm->mkNode(kind::SELECT, ar, b); - - arar = d_nm->mkVar("arar", d_nm->mkArrayType(U, d_nm->mkArrayType(U, U))); - arar_a = d_nm->mkNode(kind::SELECT, arar, a); - arar_b = d_nm->mkNode(kind::SELECT, arar, b); - } - - void tearDown() { - try { - arar = arar_a = arar_b = Node::null(); - ar = ar_a = ar_b = Node::null(); - - f = a = fa = ffa = fffa = ffffa = Node::null(); - b = fb = ffb = fffb = ffffb = Node::null(); - g = gab = gba = gfafb = gfbfa = gfaa = gbfb = Node::null(); - h = hab = hba = hfaa = Node::null(); - a_eq_b = fa_eq_b = a_eq_fb = fa_eq_fb = h_eq_g = Node::null(); - U = TypeNode::null(); - - delete d_ccArray; - delete d_cc; - delete d_out; - delete d_scope; - delete d_nm; - delete d_context; - } catch(Exception& e) { - cout << "\n\n" << e << "\n\n"; - throw; - } - } - - void testSimple() { - //Debug.on("cc"); - // add terms, then add equalities - - d_cc->addTerm(fa); - d_cc->addTerm(fb); - - d_cc->addEquality(a_eq_b); - - TS_ASSERT(d_out->areCongruent(fa, fb)); - TS_ASSERT(d_cc->areCongruent(fa, fb)); - - TS_ASSERT(!d_out->areCongruent(a, b)); - TS_ASSERT(d_cc->areCongruent(a, b)); - } - - void testSimpleReverse() { - // add equalities, then add terms; should get the same as - // testSimple() - - d_cc->addEquality(a_eq_b); - - d_cc->addTerm(fa); - d_cc->addTerm(fb); - - TS_ASSERT(d_out->areCongruent(fa, fb)); - TS_ASSERT(d_cc->areCongruent(fa, fb)); - - TS_ASSERT(!d_out->areCongruent(a, b)); - TS_ASSERT(d_cc->areCongruent(a, b)); - } - - void testSimpleContextual() { - TS_ASSERT(!d_out->areCongruent(fa, fb)); - TS_ASSERT(!d_cc->areCongruent(fa, fb)); - - TS_ASSERT(!d_out->areCongruent(a, b)); - TS_ASSERT(!d_cc->areCongruent(a, b)); - - { - d_context->push(); - - d_cc->addTerm(fa); - d_cc->addTerm(fb); - - TS_ASSERT(!d_out->areCongruent(fa, fb)); - TS_ASSERT(!d_cc->areCongruent(fa, fb)); - - TS_ASSERT(!d_out->areCongruent(a, b)); - TS_ASSERT(!d_cc->areCongruent(a, b)); - - { - d_context->push(); - - d_cc->addEquality(a_eq_b); - - TS_ASSERT(d_out->areCongruent(fa, fb)); - TS_ASSERT(d_cc->areCongruent(fa, fb)); - - TS_ASSERT(!d_out->areCongruent(a, b)); - TS_ASSERT(d_cc->areCongruent(a, b)); - - d_context->pop(); - } - - TS_ASSERT(!d_out->areCongruent(fa, fb)); - TS_ASSERT(!d_cc->areCongruent(fa, fb)); - - TS_ASSERT(!d_out->areCongruent(a, b)); - TS_ASSERT(!d_cc->areCongruent(a, b)); - - d_context->pop(); - } - - TS_ASSERT(!d_out->areCongruent(fa, fb)); - TS_ASSERT(!d_cc->areCongruent(fa, fb)); - - TS_ASSERT(!d_out->areCongruent(a, b)); - TS_ASSERT(!d_cc->areCongruent(a, b)); - } - - void testSimpleContextualReverse() { - TS_ASSERT(!d_out->areCongruent(fa, fb)); - TS_ASSERT(!d_cc->areCongruent(fa, fb)); - - TS_ASSERT(!d_out->areCongruent(a, b)); - TS_ASSERT(!d_cc->areCongruent(a, b)); - - { - d_context->push(); - - d_cc->addEquality(a_eq_b); - - TS_ASSERT(!d_out->areCongruent(fa, fb)); - TS_ASSERT(d_cc->areCongruent(fa, fb)); - - TS_ASSERT(!d_out->areCongruent(a, b)); - TS_ASSERT(d_cc->areCongruent(a, b)); - - { - d_context->push(); - - d_cc->addTerm(fa); - d_cc->addTerm(fb); - - TS_ASSERT(d_out->areCongruent(fa, fb)); - TS_ASSERT(d_cc->areCongruent(fa, fb)); - - TS_ASSERT(!d_out->areCongruent(a, b)); - TS_ASSERT(d_cc->areCongruent(a, b)); - - d_context->pop(); - } - - TS_ASSERT(!d_out->areCongruent(fa, fb)); - TS_ASSERT(d_cc->areCongruent(fa, fb)); - - TS_ASSERT(!d_out->areCongruent(a, b)); - TS_ASSERT(d_cc->areCongruent(a, b)); - - d_context->pop(); - } - - TS_ASSERT(!d_out->areCongruent(fa, fb)); - TS_ASSERT(!d_cc->areCongruent(fa, fb)); - - TS_ASSERT(!d_out->areCongruent(a, b)); - TS_ASSERT(!d_cc->areCongruent(a, b)); - } - - void test_f_of_f_of_something() { - d_cc->addTerm(ffa); - d_cc->addTerm(ffb); - - d_cc->addEquality(a_eq_b); - - TS_ASSERT(d_out->areCongruent(ffa, ffb)); - TS_ASSERT(d_cc->areCongruent(ffa, ffb)); - - TS_ASSERT(!d_out->areCongruent(fa, fb)); - TS_ASSERT(d_cc->areCongruent(fa, fb)); - - TS_ASSERT(!d_out->areCongruent(a, b)); - TS_ASSERT(d_cc->areCongruent(a, b)); - } - - void test_f4_of_something() { - d_cc->addTerm(ffffa); - d_cc->addTerm(ffffb); - - d_cc->addEquality(a_eq_b); - - TS_ASSERT(d_out->areCongruent(ffffa, ffffb)); - TS_ASSERT(d_cc->areCongruent(ffffa, ffffb)); - - TS_ASSERT(!d_out->areCongruent(fffa, fffb)); - TS_ASSERT(d_cc->areCongruent(fffa, fffb)); - - TS_ASSERT(!d_out->areCongruent(ffa, ffb)); - TS_ASSERT(d_cc->areCongruent(ffa, ffb)); - - TS_ASSERT(!d_out->areCongruent(fa, fb)); - TS_ASSERT(d_cc->areCongruent(fa, fb)); - - TS_ASSERT(!d_out->areCongruent(a, b)); - TS_ASSERT(d_cc->areCongruent(a, b)); - } - - void testSimpleBinaryFunction() { - d_cc->addTerm(gab); - d_cc->addTerm(gba); - - d_cc->addEquality(a_eq_b); - - TS_ASSERT(d_out->areCongruent(gab, gba)); - TS_ASSERT(d_cc->areCongruent(gab, gba)); - } - - void testSimpleBinaryFunction2() { - - //Debug.on("cc"); - try { - - d_cc->addTerm(gfafb); - d_cc->addTerm(gba); - d_cc->addTerm(gfaa); - d_cc->addTerm(hfaa); - - d_cc->addEquality(a_eq_fb); - d_cc->addEquality(fa_eq_b); - - TS_ASSERT(d_cc->areCongruent(a, fb)); - TS_ASSERT(d_cc->areCongruent(b, fa)); - TS_ASSERT(d_cc->areCongruent(fb, ffa)); - - Debug("cc") << "\n\n\n" - << "a norm: " << d_cc->normalize(a) << std::endl - << "fb norm: " << d_cc->normalize(fb) << std::endl - << "b norm: " << d_cc->normalize(b) << std::endl - << "fa norm: " << d_cc->normalize(fa) << std::endl - << "ffa norm: " << d_cc->normalize(ffa) << std::endl - << "ffffa norm " << d_cc->normalize(ffffa) << std::endl - << "ffffb norm " << d_cc->normalize(ffffb) << std::endl - << "gba norm: " << d_cc->normalize(gba) << std::endl - << "gfaa norm: " << d_cc->normalize(gfaa) << std::endl - << "gbfb norm: " << d_cc->normalize(gbfb) << std::endl - << "gfafb norm: " << d_cc->normalize(gfafb) << std::endl - << "hab norm: " << d_cc->normalize(hab) << std::endl - << "hba norm: " << d_cc->normalize(hba) << std::endl - << "hfaa norm: " << d_cc->normalize(hfaa) << std::endl; - - TS_ASSERT(d_out->areCongruent(gfafb, gba)); - TS_ASSERT(d_cc->areCongruent(b, fa)); - TS_ASSERT(d_cc->areCongruent(gfafb, gba)); - TS_ASSERT(d_cc->areCongruent(hba, hba)); - TS_ASSERT(d_cc->areCongruent(hfaa, hba)); - TS_ASSERT(d_out->areCongruent(gfaa, gba)); - TS_ASSERT(d_cc->areCongruent(gfaa, gba)); - - } catch(Exception& e) { - cout << "\n\n" << e << "\n\n"; - throw; - } - } - - void testUF() { - //Debug.on("cc"); - try{ - Node c_0 = d_nm->mkVar("c_0", U); - Node c_1 = d_nm->mkVar("c_1", U); - Node c_2 = d_nm->mkVar("c_2", U); - Node c2 = d_nm->mkVar("c2", U); - Node c3 = d_nm->mkVar("c3", U); - Node c4 = d_nm->mkVar("c4", U); - Node c5 = d_nm->mkVar("c5", U); - Node c6 = d_nm->mkVar("c6", U); - Node c7 = d_nm->mkVar("c7", U); - Node c8 = d_nm->mkVar("c8", U); - Node c9 = d_nm->mkVar("c9", U); - vector<TypeNode> args2U(2, U); - Node f1 = d_nm->mkVar("f1", d_nm->mkFunctionType(args2U, U)); - - d_cc->addEquality(d_nm->mkNode(kind::EQUAL, d_nm->mkNode(kind::APPLY_UF, f1,d_nm->mkNode(kind::APPLY_UF, f1,c_0,c_0),c_0),d_nm->mkNode(kind::APPLY_UF, f1,c_0,d_nm->mkNode(kind::APPLY_UF, f1,c_0,c_0)))); - d_cc->addEquality(d_nm->mkNode(kind::EQUAL, d_nm->mkNode(kind::APPLY_UF, f1,d_nm->mkNode(kind::APPLY_UF, f1,c_0,c_0),c_2),d_nm->mkNode(kind::APPLY_UF, f1,c_0,d_nm->mkNode(kind::APPLY_UF, f1,c_0,c_2)))); - d_cc->addEquality(d_nm->mkNode(kind::EQUAL, d_nm->mkNode(kind::APPLY_UF, f1,d_nm->mkNode(kind::APPLY_UF, f1,c_0,c_1),c_1),d_nm->mkNode(kind::APPLY_UF, f1,c_0,d_nm->mkNode(kind::APPLY_UF, f1,c_1,c_1)))); - d_cc->addEquality(d_nm->mkNode(kind::EQUAL, d_nm->mkNode(kind::APPLY_UF, f1,d_nm->mkNode(kind::APPLY_UF, f1,c_0,c_1),c_2),d_nm->mkNode(kind::APPLY_UF, f1,c_0,d_nm->mkNode(kind::APPLY_UF, f1,c_1,c_2)))); - d_cc->addEquality(d_nm->mkNode(kind::EQUAL, d_nm->mkNode(kind::APPLY_UF, f1,d_nm->mkNode(kind::APPLY_UF, f1,c_2,c_1),c_2),d_nm->mkNode(kind::APPLY_UF, f1,c_2,d_nm->mkNode(kind::APPLY_UF, f1,c_1,c_2)))); - d_cc->addEquality(d_nm->mkNode(kind::EQUAL, d_nm->mkNode(kind::APPLY_UF, f1,d_nm->mkNode(kind::APPLY_UF, f1,c_2,c_2),c_0),d_nm->mkNode(kind::APPLY_UF, f1,c_2,d_nm->mkNode(kind::APPLY_UF, f1,c_2,c_0)))); - d_cc->addEquality(d_nm->mkNode(kind::EQUAL, d_nm->mkNode(kind::APPLY_UF, f1,d_nm->mkNode(kind::APPLY_UF, f1,c_2,c_2),c_1),d_nm->mkNode(kind::APPLY_UF, f1,c_2,d_nm->mkNode(kind::APPLY_UF, f1,c_2,c_1)))); - d_cc->addEquality(d_nm->mkNode(kind::EQUAL, d_nm->mkNode(kind::APPLY_UF, f1,c_0,d_nm->mkNode(kind::APPLY_UF, f1,c_2,d_nm->mkNode(kind::APPLY_UF, f1,c_2,d_nm->mkNode(kind::APPLY_UF, f1,c_2,c_0)))),d_nm->mkNode(kind::APPLY_UF, f1,c_2,d_nm->mkNode(kind::APPLY_UF, f1,c_0,d_nm->mkNode(kind::APPLY_UF, f1,c_2,d_nm->mkNode(kind::APPLY_UF, f1,c_0,c_2)))))); - d_cc->addEquality(d_nm->mkNode(kind::EQUAL, d_nm->mkNode(kind::APPLY_UF, f1,c2,c8),d_nm->mkNode(kind::APPLY_UF, f1,c4,c9))); - d_cc->addEquality(d_nm->mkNode(kind::EQUAL, c9,c_0)); - d_cc->addEquality(d_nm->mkNode(kind::EQUAL, c8,c_0)); - d_cc->addEquality(d_nm->mkNode(kind::EQUAL, c4,c_0)); - d_cc->addEquality(d_nm->mkNode(kind::EQUAL, c2,c_0)); - d_cc->addEquality(d_nm->mkNode(kind::EQUAL, c5,c_0)); - d_cc->addEquality(d_nm->mkNode(kind::EQUAL, c7,c_0)); - d_cc->addEquality(d_nm->mkNode(kind::EQUAL, c3,c_0)); - d_cc->addEquality(d_nm->mkNode(kind::EQUAL, c6,c_1)); - d_cc->addEquality(d_nm->mkNode(kind::EQUAL, d_nm->mkNode(kind::APPLY_UF, f1,c_2,c_2),c_0)); - d_cc->addEquality(d_nm->mkNode(kind::EQUAL, d_nm->mkNode(kind::APPLY_UF, f1,c_2,c_1),c_0)); - d_cc->addEquality(d_nm->mkNode(kind::EQUAL, d_nm->mkNode(kind::APPLY_UF, f1,c_2,c_0),c_0)); - d_cc->addEquality(d_nm->mkNode(kind::EQUAL, d_nm->mkNode(kind::APPLY_UF, f1,c_1,c_2),c_0)); - d_cc->addEquality(d_nm->mkNode(kind::EQUAL, d_nm->mkNode(kind::APPLY_UF, f1,c_1,c_1),c_0)); - d_cc->addEquality(d_nm->mkNode(kind::EQUAL, d_nm->mkNode(kind::APPLY_UF, f1,c_1,c_0),c_1)); - d_cc->addEquality(d_nm->mkNode(kind::EQUAL, d_nm->mkNode(kind::APPLY_UF, f1,c_0,c_1),c_0)); - d_cc->addEquality(d_nm->mkNode(kind::EQUAL, d_nm->mkNode(kind::APPLY_UF, f1,c_0,c_0),c_0)); - } catch(Exception& e) { - cout << "\n\n" << e << "\n\n"; - throw e; - } - } - - void testUF2() { - Node f = d_nm->mkVar("f", d_nm->mkFunctionType(U, U)); - Node x = d_nm->mkVar("x", U); - Node y = d_nm->mkVar("y", U); - Node z = d_nm->mkVar("z", U); - Node ffx = d_nm->mkNode(kind::APPLY_UF, f, d_nm->mkNode(kind::APPLY_UF, f, x)); - Node fffx = d_nm->mkNode(kind::APPLY_UF, f, ffx); - Node ffffx = d_nm->mkNode(kind::APPLY_UF, f, fffx); - Node ffx_eq_fffx = ffx.eqNode(fffx); - Node ffx_eq_y = ffx.eqNode(y); - Node ffffx_eq_z = ffffx.eqNode(z); - - d_cc->addEquality(ffx_eq_fffx); - d_cc->addEquality(ffx_eq_y); - d_cc->addEquality(ffffx_eq_z); - } - - void testSimpleArray() { - //Debug.on("cc"); - // add terms, then add equalities - try { - d_ccArray->addTerm(ar_a); - d_ccArray->addTerm(ar_b); - - d_ccArray->addEquality(a_eq_b); - - TS_ASSERT(d_out->areCongruent(ar_a, ar_b)); - TS_ASSERT(d_ccArray->areCongruent(ar_a, ar_b)); - - TS_ASSERT(!d_out->areCongruent(a, b)); - TS_ASSERT(d_ccArray->areCongruent(a, b)); - } catch(Exception& e) { - cout << "\n\n" << e << "\n\n"; - throw; - } - } - - void testSimpleReverseArray() { - // add equalities, then add terms; should get the same as - // testSimple() - - d_ccArray->addEquality(a_eq_b); - - d_ccArray->addTerm(ar_a); - d_ccArray->addTerm(ar_b); - - TS_ASSERT(d_out->areCongruent(ar_a, ar_b)); - TS_ASSERT(d_ccArray->areCongruent(ar_a, ar_b)); - - TS_ASSERT(!d_out->areCongruent(a, b)); - TS_ASSERT(d_ccArray->areCongruent(a, b)); - } - - void testArray() { - Node ar_eq_arar_a = d_nm->mkNode(kind::EQUAL, ar, arar_a); - Node ar2 = d_nm->mkVar("ar2", d_nm->mkArrayType(U, U)); - Node store_arar_b_ar2 = d_nm->mkNode(kind::STORE, arar, b, ar2); - Node select__store_arar_b_ar2__a = - d_nm->mkNode(kind::SELECT, store_arar_b_ar2, a); - Node select__store_arar_b_ar2__a__eq__arar_a = - d_nm->mkNode(kind::EQUAL, select__store_arar_b_ar2__a, arar_a); - - d_ccArray->addTerm(ar); - d_ccArray->addTerm(select__store_arar_b_ar2__a); - - d_ccArray->addEquality(ar_eq_arar_a); - d_ccArray->addEquality(select__store_arar_b_ar2__a__eq__arar_a); - - TS_ASSERT(d_ccArray->areCongruent(ar, select__store_arar_b_ar2__a)); - TS_ASSERT(d_out->areCongruent(ar, select__store_arar_b_ar2__a)); - } - -};/* class CongruenceClosureWhite */ |