diff options
Diffstat (limited to 'test/unit')
| -rw-r--r-- | test/unit/Makefile.am | 9 | ||||
| -rw-r--r-- | test/unit/expr/attribute_white.h | 4 | ||||
| -rw-r--r-- | test/unit/theory/shared_term_manager_black.h | 6 | ||||
| -rw-r--r-- | test/unit/theory/theory_engine_white.h | 5 | ||||
| -rw-r--r-- | test/unit/theory/theory_uf_tim_white.h (renamed from test/unit/theory/theory_uf_white.h) | 14 | ||||
| -rw-r--r-- | test/unit/util/congruence_closure_white.h | 454 |
6 files changed, 477 insertions, 15 deletions
diff --git a/test/unit/Makefile.am b/test/unit/Makefile.am index f25862b54..eb920e6c5 100644 --- a/test/unit/Makefile.am +++ b/test/unit/Makefile.am @@ -3,7 +3,7 @@ UNIT_TESTS = \ theory/shared_term_manager_black \ theory/theory_engine_white \ theory/theory_black \ - theory/theory_uf_white \ + theory/theory_uf_tim_white \ theory/theory_arith_white \ expr/expr_public \ expr/expr_manager_public \ @@ -29,6 +29,7 @@ UNIT_TESTS = \ util/assert_white \ util/bitvector_black \ util/configuration_black \ + util/congruence_closure_white \ util/output_black \ util/exception_black \ util/integer_black \ @@ -182,13 +183,13 @@ no-cxxtest-available: else \ echo; \ echo "ERROR:"; \ - echo "ERROR: You cannot make dist in this build directory, you do not have CxxTest."; \ - echo "ERROR: The tests should be generated for the user and included in the tarball,"; \ + echo "ERROR: You cannot make dist in this build directory, you do not have CxxTest."; \ + echo "ERROR: The tests should be generated for the user and included in the tarball,"; \ echo "ERROR: otherwise they'll be required to have CxxTest just to test the standard"; \ echo "ERROR: distribution built correctly."; \ echo "ERROR: If you really want to do this, append the following to your make command."; \ echo "ERROR:"; \ - echo "ERROR: I_REALLY_WANT_TO_BUILD_CVC4_DIST_WITHOUT_TESTS=1"; \ + echo "ERROR: I_REALLY_WANT_TO_BUILD_CVC4_DIST_WITHOUT_TESTS=1"; \ echo "ERROR:"; \ echo; \ exit 1; \ diff --git a/test/unit/expr/attribute_white.h b/test/unit/expr/attribute_white.h index e18aeb975..ea1f40eac 100644 --- a/test/unit/expr/attribute_white.h +++ b/test/unit/expr/attribute_white.h @@ -104,8 +104,8 @@ public: TS_ASSERT_DIFFERS(VarNameAttr::s_id, TestStringAttr2::s_id); TS_ASSERT_DIFFERS(TestStringAttr1::s_id, TestStringAttr2::s_id); - lastId = attr::LastAttributeId<void*, false>::s_id; - TS_ASSERT_LESS_THAN(theory::uf::ECAttr::s_id, lastId); + //lastId = attr::LastAttributeId<void*, false>::s_id; + //TS_ASSERT_LESS_THAN(theory::uf::ECAttr::s_id, lastId); lastId = attr::LastAttributeId<bool, false>::s_id; TS_ASSERT_LESS_THAN(theory::Theory::PreRegisteredAttr::s_id, lastId); diff --git a/test/unit/theory/shared_term_manager_black.h b/test/unit/theory/shared_term_manager_black.h index 4393d99cd..def2f7049 100644 --- a/test/unit/theory/shared_term_manager_black.h +++ b/test/unit/theory/shared_term_manager_black.h @@ -31,6 +31,7 @@ #include "context/context.h" #include "util/rational.h" #include "util/integer.h" +#include "util/options.h" #include "util/Assert.h" using namespace CVC4; @@ -50,6 +51,7 @@ class SharedTermManagerBlack : public CxxTest::TestSuite { NodeManager* d_nm; NodeManagerScope* d_scope; TheoryEngine* d_theoryEngine; + Options d_options; public: @@ -59,11 +61,11 @@ public: d_nm = new NodeManager(d_ctxt); d_scope = new NodeManagerScope(d_nm); - d_theoryEngine = new TheoryEngine(d_ctxt); - + d_theoryEngine = new TheoryEngine(d_ctxt, &d_options); } void tearDown() { + d_theoryEngine->shutdown(); delete d_theoryEngine; delete d_scope; diff --git a/test/unit/theory/theory_engine_white.h b/test/unit/theory/theory_engine_white.h index ead879336..1ec523148 100644 --- a/test/unit/theory/theory_engine_white.h +++ b/test/unit/theory/theory_engine_white.h @@ -35,6 +35,7 @@ #include "context/context.h" #include "util/rational.h" #include "util/integer.h" +#include "util/options.h" #include "util/Assert.h" using namespace CVC4; @@ -214,6 +215,7 @@ class TheoryEngineWhite : public CxxTest::TestSuite { FakeOutputChannel *d_nullChannel; FakeTheory *d_builtin, *d_bool, *d_uf, *d_arith, *d_arrays, *d_bv; TheoryEngine* d_theoryEngine; + Options d_options; public: @@ -234,7 +236,7 @@ public: d_bv = new FakeTheory(d_ctxt, *d_nullChannel, "BV"); // create the TheoryEngine - d_theoryEngine = new TheoryEngine(d_ctxt); + d_theoryEngine = new TheoryEngine(d_ctxt, &d_options); // insert our fake versions into the TheoryEngine's theoryOf table d_theoryEngine->d_theoryOfTable. @@ -254,6 +256,7 @@ public: } void tearDown() { + d_theoryEngine->shutdown(); delete d_theoryEngine; delete d_bv; diff --git a/test/unit/theory/theory_uf_white.h b/test/unit/theory/theory_uf_tim_white.h index f273de30f..aec999293 100644 --- a/test/unit/theory/theory_uf_white.h +++ b/test/unit/theory/theory_uf_tim_white.h @@ -11,15 +11,16 @@ ** See the file COPYING in the top-level source directory for licensing ** information.\endverbatim ** - ** \brief White box testing of CVC4::theory::uf::TheoryUF. + ** \brief White box testing of CVC4::theory::uf::tim::TheoryUFTim. ** - ** White box testing of CVC4::theory::uf::TheoryUF. + ** 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" @@ -31,13 +32,14 @@ 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 TheoryUFWhite : public CxxTest::TestSuite { +class TheoryUFTimWhite : public CxxTest::TestSuite { Context* d_ctxt; NodeManager* d_nm; @@ -46,20 +48,20 @@ class TheoryUFWhite : public CxxTest::TestSuite { TestOutputChannel d_outputChannel; Theory::Effort d_level; - TheoryUF* d_euf; + TheoryUFTim* d_euf; TypeNode* d_booleanType; public: - TheoryUFWhite() : d_level(Theory::FULL_EFFORT) {} + TheoryUFTimWhite() : d_level(Theory::FULL_EFFORT) {} void setUp() { d_ctxt = new Context; d_nm = new NodeManager(d_ctxt); d_scope = new NodeManagerScope(d_nm); d_outputChannel.clear(); - d_euf = new TheoryUF(0, d_ctxt, d_outputChannel); + d_euf = new TheoryUFTim(0, d_ctxt, d_outputChannel); d_booleanType = new TypeNode(d_nm->booleanType()); } 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 */ |