diff options
author | Morgan Deters <mdeters@gmail.com> | 2011-07-09 02:35:19 +0000 |
---|---|---|
committer | Morgan Deters <mdeters@gmail.com> | 2011-07-09 02:35:19 +0000 |
commit | 7e9d980e1fbaffadd0c76511e6c42e12b8039585 (patch) | |
tree | 586be147825f50f2f40b7935bd2a9a522f3530c7 /src | |
parent | 878f71272c06cf605fb3d2f4e66eaea55aa32127 (diff) |
minor fixups
Diffstat (limited to 'src')
-rw-r--r-- | src/expr/Makefile.am | 4 | ||||
-rw-r--r-- | src/theory/uf/Makefile.am | 4 | ||||
-rw-r--r-- | src/theory/uf/theory_uf.cpp | 109 | ||||
-rw-r--r-- | src/theory/uf/theory_uf.h | 2 |
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 */ |