minor fixups

4 files changed, 116 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 */