summaryrefslogtreecommitdiff
diff options
context:
space:
mode:
Diffstat
-rw-r--r--src/expr/Makefile.am4
-rw-r--r--src/theory/uf/Makefile.am4
-rw-r--r--src/theory/uf/theory_uf.cpp109
-rw-r--r--src/theory/uf/theory_uf.h2
-rw-r--r--test/regress/regress0/uf/Makefile.am1
-rw-r--r--test/unit/Makefile.am1
-rw-r--r--test/unit/expr/kind_map_black.h109
7 files changed, 227 insertions, 3 deletions
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<TNode> workList;
+ workList.push_back(n);
+ __gnu_cxx::hash_set<TNode, TNodeHashFunction> 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 <cxxtest/TestSuite.h>
+
+#include <iostream>
+#include <string>
+#include <sstream>
+
+#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 */
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback