diff options
Diffstat (limited to 'test/unit/util/congruence_closure_white.h')
-rw-r--r-- | test/unit/util/congruence_closure_white.h | 454 |
1 files changed, 454 insertions, 0 deletions
diff --git a/test/unit/util/congruence_closure_white.h b/test/unit/util/congruence_closure_white.h new file mode 100644 index 000000000..273f9cfa5 --- /dev/null +++ b/test/unit/util/congruence_closure_white.h @@ -0,0 +1,454 @@ +/********************* */ +/*! \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 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/cdset.h" +#include "context/cdmap.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 { + CDSet<Node, NodeHashFunction> d_notifications; + CDMap<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) { + CDMap<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>* d_cc; + + 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; +public: + + void setUp() { + d_context = new Context; + d_nm = new NodeManager(d_context); + d_scope = new NodeManagerScope(d_nm); + d_out = new MyOutputChannel(d_context, d_nm); + d_cc = new CongruenceClosure<MyOutputChannel>(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); + } + + void tearDown() { + try { + 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_cc; + delete d_out; + delete d_scope; + delete d_nm; + delete d_context; + + } catch(Exception& e) { + Warning() << std::endl << e << std::endl; + 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(hfaa); + + d_cc->addEquality(a_eq_fb); + d_cc->addEquality(fa_eq_b); + d_cc->addEquality(h_eq_g); + + 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, hba)); + TS_ASSERT(d_cc->areCongruent(gfafb, gba)); + TS_ASSERT(d_cc->areCongruent(hba, gba)); + TS_ASSERT(d_cc->areCongruent(hfaa, hba)); + TS_ASSERT(d_out->areCongruent(hfaa, gba));// fails due to problem with care lists + TS_ASSERT(d_cc->areCongruent(hfaa, 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 << e << "\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); + } + +};/* class CongruenceClosureWhite */ |