From 7e9d980e1fbaffadd0c76511e6c42e12b8039585 Mon Sep 17 00:00:00 2001 From: Morgan Deters Date: Sat, 9 Jul 2011 02:35:19 +0000 Subject: [PATCH] minor fixups --- src/expr/Makefile.am | 4 +- src/theory/uf/Makefile.am | 4 +- src/theory/uf/theory_uf.cpp | 109 +++++++++++++++++++++++++++ src/theory/uf/theory_uf.h | 2 + test/regress/regress0/uf/Makefile.am | 1 + test/unit/Makefile.am | 1 + test/unit/expr/kind_map_black.h | 109 +++++++++++++++++++++++++++ 7 files changed, 227 insertions(+), 3 deletions(-) create mode 100644 test/unit/expr/kind_map_black.h diff --git a/src/expr/Makefile.am b/src/expr/Makefile.am index ced34b8be..352647642 100644 --- a/src/expr/Makefile.am +++ b/src/expr/Makefile.am @@ -11,7 +11,7 @@ libexpr_la_SOURCES = \ type_node.h \ type_node.cpp \ node_builder.h \ - convenience_node_builders.h \ + convenience_node_builders.h \ type.h \ type.cpp \ node_value.h \ @@ -29,7 +29,7 @@ libexpr_la_SOURCES = \ node_self_iterator.h \ expr_stream.h \ kind_map.h - + nodist_libexpr_la_SOURCES = \ kind.h \ metakind.h \ diff --git a/src/theory/uf/Makefile.am b/src/theory/uf/Makefile.am index 3cf53960a..8527924da 100644 --- a/src/theory/uf/Makefile.am +++ b/src/theory/uf/Makefile.am @@ -13,7 +13,9 @@ libuf_la_SOURCES = \ theory_uf.h \ theory_uf.cpp \ theory_uf_type_rules.h \ - theory_uf_rewriter.h + theory_uf_rewriter.h \ + equality_engine.h \ + equality_engine_impl.h libuf_la_LIBADD = \ @builddir@/tim/libuftim.la \ diff --git a/src/theory/uf/theory_uf.cpp b/src/theory/uf/theory_uf.cpp index 0571126e6..8caac6fb7 100644 --- a/src/theory/uf/theory_uf.cpp +++ b/src/theory/uf/theory_uf.cpp @@ -212,3 +212,112 @@ void TheoryUF::explain(TNode literal) { explain(literal, assumptions); d_out->explanation(mkAnd(assumptions)); } + +void TheoryUF::staticLearning(TNode n, NodeBuilder<>& learned) { + //TimerStat::CodeTimer codeTimer(d_staticLearningTimer); + + vector workList; + workList.push_back(n); + __gnu_cxx::hash_set processed; + + while(!workList.empty()) { + n = workList.back(); + + bool unprocessedChildren = false; + for(TNode::iterator i = n.begin(), iend = n.end(); i != iend; ++i) { + if(processed.find(*i) == processed.end()) { + // unprocessed child + workList.push_back(*i); + unprocessedChildren = true; + } + } + + if(unprocessedChildren) { + continue; + } + + workList.pop_back(); + // has node n been processed in the meantime ? + if(processed.find(n) != processed.end()) { + continue; + } + processed.insert(n); + + // == DIAMONDS == + + Debug("diamonds") << "===================== looking at" << endl + << n << endl; + + // binary OR of binary ANDs of EQUALities + if(n.getKind() == kind::OR && n.getNumChildren() == 2 && + n[0].getKind() == kind::AND && n[0].getNumChildren() == 2 && + n[1].getKind() == kind::AND && n[1].getNumChildren() == 2 && + (n[0][0].getKind() == kind::EQUAL || n[0][0].getKind() == kind::IFF) && + (n[0][1].getKind() == kind::EQUAL || n[0][1].getKind() == kind::IFF) && + (n[1][0].getKind() == kind::EQUAL || n[1][0].getKind() == kind::IFF) && + (n[1][1].getKind() == kind::EQUAL || n[1][1].getKind() == kind::IFF)) { + // now we have (a = b && c = d) || (e = f && g = h) + + Debug("diamonds") << "has form of a diamond!" << endl; + + TNode + a = n[0][0][0], b = n[0][0][1], + c = n[0][1][0], d = n[0][1][1], + e = n[1][0][0], f = n[1][0][1], + g = n[1][1][0], h = n[1][1][1]; + + // test that one of {a, b} = one of {c, d}, and make "b" the + // shared node (i.e. put in the form (a = b && b = d)) + // note we don't actually care about the shared ones, so the + // "swaps" below are one-sided, ignoring b and c + if(a == c) { + a = b; + } else if(a == d) { + a = b; + d = c; + } else if(b == c) { + // nothing to do + } else if(b == d) { + d = c; + } else { + // condition not satisfied + Debug("diamonds") << "+ A fails" << endl; + continue; + } + + Debug("diamonds") << "+ A holds" << endl; + + // same: one of {e, f} = one of {g, h}, and make "f" the + // shared node (i.e. put in the form (e = f && f = h)) + if(e == g) { + e = f; + } else if(e == h) { + e = f; + h = g; + } else if(f == g) { + // nothing to do + } else if(f == h) { + h = g; + } else { + // condition not satisfied + Debug("diamonds") << "+ B fails" << endl; + continue; + } + + Debug("diamonds") << "+ B holds" << endl; + + // now we have (a = b && b = d) || (e = f && f = h) + // test that {a, d} == {e, h} + if( (a == e && d == h) || + (a == h && d == e) ) { + // learn: n implies a == d + Debug("diamonds") << "+ C holds" << endl; + Node newEquality = a.getType().isBoolean() ? a.iffNode(d) : a.eqNode(d); + Debug("diamonds") << " ==> " << newEquality << endl; + learned << n.impNode(newEquality); + } else { + Debug("diamonds") << "+ C fails" << endl; + } + } + } +} diff --git a/src/theory/uf/theory_uf.h b/src/theory/uf/theory_uf.h index 266a1b7b4..c77d5a810 100644 --- a/src/theory/uf/theory_uf.h +++ b/src/theory/uf/theory_uf.h @@ -118,6 +118,8 @@ public: return "THEORY_UF"; } + void staticLearning(TNode in, NodeBuilder<>& learned); + };/* class TheoryUF */ }/* CVC4::theory::uf namespace */ diff --git a/test/regress/regress0/uf/Makefile.am b/test/regress/regress0/uf/Makefile.am index 45cf22232..01eaee999 100644 --- a/test/regress/regress0/uf/Makefile.am +++ b/test/regress/regress0/uf/Makefile.am @@ -19,6 +19,7 @@ TESTS = \ eq_diamond1.smt \ eq_diamond14.reduced.smt \ eq_diamond14.reduced2.smt \ + eq_diamond23.smt \ NEQ016_size5_reduced2a.smt \ NEQ016_size5_reduced2b.smt \ dead_dnd002.smt \ diff --git a/test/unit/Makefile.am b/test/unit/Makefile.am index cef4590a3..f98f434c1 100644 --- a/test/unit/Makefile.am +++ b/test/unit/Makefile.am @@ -12,6 +12,7 @@ UNIT_TESTS = \ expr/node_white \ expr/node_black \ expr/kind_black \ + expr/kind_map_black \ expr/node_builder_black \ expr/node_manager_black \ expr/node_manager_white \ diff --git a/test/unit/expr/kind_map_black.h b/test/unit/expr/kind_map_black.h new file mode 100644 index 000000000..e5bcdd298 --- /dev/null +++ b/test/unit/expr/kind_map_black.h @@ -0,0 +1,109 @@ +/********************* */ +/*! \file kind_map_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::KindMap + ** + ** Black box testing of CVC4::KindMap. + **/ + +#include + +#include +#include +#include + +#include "expr/kind_map.h" + +using namespace CVC4; +using namespace CVC4::kind; +using namespace std; + +class KindMapBlack : public CxxTest::TestSuite { + +public: + + void testSimple() { + KindMap map; + TS_ASSERT(map.isEmpty()); + map.set(AND); + TS_ASSERT(!map.isEmpty()); + KindMap map2 = map; + TS_ASSERT(!map2.isEmpty()); + TS_ASSERT_EQUALS(map, map2); + TS_ASSERT(map.tst(AND)); + TS_ASSERT(map2.tst(AND)); + TS_ASSERT(!map.tst(OR)); + TS_ASSERT(!map2.tst(OR)); + map2 = ~map2; + TS_ASSERT(map2.tst(OR)); + TS_ASSERT(!map2.tst(AND)); + TS_ASSERT(map != map2); + TS_ASSERT(map.begin() != map.end()); + TS_ASSERT(map2.begin() != map2.end()); + map &= ~AND; + TS_ASSERT(map.isEmpty()); + map2.clear(); + TS_ASSERT(map2.isEmpty()); + TS_ASSERT_EQUALS(map2, map); + TS_ASSERT_EQUALS(map.begin(), map.end()); + TS_ASSERT_EQUALS(map2.begin(), map2.end()); + } + + void testIteration() { + KindMap m = AND & OR; + TS_ASSERT(m.isEmpty()); + for(KindMap::iterator i = m.begin(); i != m.end(); ++i) { + TS_FAIL("expected empty iterator range"); + } + m = AND | OR; + KindMap::iterator i = m.begin(); + TS_ASSERT(i != m.end()); + TS_ASSERT_EQUALS(*i, AND); + ++i; + TS_ASSERT(i != m.end()); + TS_ASSERT_EQUALS(*i, OR); + ++i; + TS_ASSERT(i == m.end()); + + m = ~m; + unsigned k = 0; + for(i = m.begin(); i != m.end(); ++i, ++k) { + while(k == AND || k == OR) { + ++k; + } + TS_ASSERT_DIFFERS(Kind(k), UNDEFINED_KIND); + TS_ASSERT_DIFFERS(Kind(k), LAST_KIND); + TS_ASSERT_EQUALS(*i, Kind(k)); + } + } + + void testConstruction() { + TS_ASSERT(!(AND & AND).isEmpty()); + TS_ASSERT((AND & ~AND).isEmpty()); + TS_ASSERT(!(AND & AND & AND).isEmpty()); + + TS_ASSERT(!(AND | AND).isEmpty()); + TS_ASSERT(!(AND | ~AND).isEmpty()); + TS_ASSERT(((AND | AND) & ~AND).isEmpty()); + TS_ASSERT(!((AND | OR) & ~AND).isEmpty()); + + TS_ASSERT((AND ^ AND).isEmpty()); + TS_ASSERT(!(AND ^ OR).isEmpty()); + TS_ASSERT(!(AND ^ AND ^ AND).isEmpty()); + +#ifdef CVC4_ASSERTIONS + TS_ASSERT_THROWS(~LAST_KIND, IllegalArgumentException); +#endif /* CVC4_ASSERTIONS */ + } + +};/* class KindMapBlack */ -- 2.30.2