diff options
author | Morgan Deters <mdeters@gmail.com> | 2010-08-19 23:49:58 +0000 |
---|---|---|
committer | Morgan Deters <mdeters@gmail.com> | 2010-08-19 23:49:58 +0000 |
commit | ad24cbdb3462b2b2dd312aab2f1f33d9bbcac00e (patch) | |
tree | b783098b4d72422826890c46870436cbeae0788d /src/util/congruence_closure.h | |
parent | 29c72e0fd6d0161de275060bbd05370394f1f708 (diff) |
UF theory bug fixes, code cleanup, and extra debugging output.
Enabled new UF theory by default.
Added some UF regressions.
Some work on the whole equality-over-bool-removed-in-favor-of-IFF
thing. (Congruence closure module and other things have to handle
IFF as a special case of equality, etc..)
Added pre-rewriting to TheoryBool which rewrites:
* (IFF true x) => x
* (IFF false x) => (NOT x)
* (IFF x true) => x
* (IFF x false) => (NOT x)
* (IFF x x) => true
* (IFF x (NOT x)) => false
* (IFF (NOT x) x) => false
* (ITE true x y) => x
* (ITE false x y) => y
* (ITE cond x x) => x
Added post-rewriting that does all of the above, plus normalize IFF and ITE:
* (IFF x y) => (IFF y x), if y < x
* (ITE (NOT cond) x y) => (ITE cond y x)
(Note: ITEs survive the removal-of-ITEs pass only if they are Boolean-valued.)
A little more debugging output from CNF stream, context pushes/pops,
ITE removal.
Some more documentation.
Fixed some typos.
Diffstat (limited to 'src/util/congruence_closure.h')
-rw-r--r-- | src/util/congruence_closure.h | 45 |
1 files changed, 31 insertions, 14 deletions
diff --git a/src/util/congruence_closure.h b/src/util/congruence_closure.h index 058f9c193..7d7e26bbe 100644 --- a/src/util/congruence_closure.h +++ b/src/util/congruence_closure.h @@ -159,8 +159,9 @@ public: */ void addEquality(TNode inputEq) { Debug("cc") << "CC addEquality[" << d_context->getLevel() << "]: " << inputEq << std::endl; - Assert(inputEq.getKind() == kind::EQUAL); - NodeBuilder<> eqb(kind::EQUAL); + Assert(inputEq.getKind() == kind::EQUAL || + inputEq.getKind() == kind::IFF); + NodeBuilder<> eqb(inputEq.getKind()); if(inputEq[1].getKind() == kind::APPLY_UF && inputEq[0].getKind() != kind::APPLY_UF) { eqb << flatten(inputEq[1]) << inputEq[0]; @@ -190,7 +191,7 @@ public: EqMap::iterator i = d_eqMap.find(t); if(i == d_eqMap.end()) { Node v = NodeManager::currentNM()->mkSkolem(t.getType()); - addEq(NodeManager::currentNM()->mkNode(kind::EQUAL, t, v), TNode::null()); + addEq(NodeManager::currentNM()->mkNode(t.getType().isBoolean() ? kind::IFF : kind::EQUAL, t, v), TNode::null()); d_eqMap.insert(t, v); return v; } else { @@ -272,7 +273,8 @@ public: */ inline Node explain(TNode eq) throw(CongruenceClosureException, AssertionException) { - Assert(eq.getKind() == kind::EQUAL); + Assert(eq.getKind() == kind::EQUAL || + eq.getKind() == kind::IFF); return explain(eq[0], eq[1]); } @@ -299,7 +301,8 @@ private: return TNode::null(); } else { TNode l = (*i).second; - Assert(l.getKind() == kind::EQUAL); + Assert(l.getKind() == kind::EQUAL || + l.getKind() == kind::IFF); return l; } } @@ -309,7 +312,8 @@ private: */ inline void setLookup(TNode a, TNode b) { Assert(a.getKind() == kind::TUPLE); - Assert(b.getKind() == kind::EQUAL); + Assert(b.getKind() == kind::EQUAL || + b.getKind() == kind::IFF); d_lookup[a] = b; } @@ -325,7 +329,8 @@ private: */ inline void appendToUseList(TNode of, TNode eq) { Debug("cc") << "adding " << eq << " to use list of " << of << std::endl; - Assert(eq.getKind() == kind::EQUAL); + Assert(eq.getKind() == kind::EQUAL || + eq.getKind() == kind::IFF); Assert(of == find(of)); UseLists::iterator usei = d_useList.find(of); UseList* ul; @@ -389,7 +394,8 @@ void CongruenceClosure<OutputChannel>::addEq(TNode eq, TNode inputEq) { d_proofRewrite[eq] = inputEq; Debug("cc") << "CC addEq[" << d_context->getLevel() << "]: " << eq << std::endl; - Assert(eq.getKind() == kind::EQUAL); + Assert(eq.getKind() == kind::EQUAL || + eq.getKind() == kind::IFF); Assert(eq[1].getKind() != kind::APPLY_UF); if(areCongruent(eq[0], eq[1])) { Debug("cc") << "CC -- redundant, ignoring...\n"; @@ -466,7 +472,8 @@ void CongruenceClosure<OutputChannel>::propagate(TNode seed) { Debug("cc") << "=== e is " << e << " ===" << std::endl; TNode a, b; - if(e.getKind() == kind::EQUAL) { + if(e.getKind() == kind::EQUAL || + e.getKind() == kind::IFF) { // e is an equality a = b (a, b are constants) a = e[0]; @@ -481,8 +488,10 @@ void CongruenceClosure<OutputChannel>::propagate(TNode seed) { Assert(e.getKind() == kind::TUPLE); Assert(e.getNumChildren() == 2); - Assert(e[0].getKind() == kind::EQUAL); - Assert(e[1].getKind() == kind::EQUAL); + Assert(e[0].getKind() == kind::EQUAL || + e[0].getKind() == kind::IFF); + Assert(e[1].getKind() == kind::EQUAL || + e[1].getKind() == kind::IFF); // tuple is (eq, lookup) a = e[0][1]; @@ -576,7 +585,8 @@ void CongruenceClosure<OutputChannel>::propagate(TNode seed) { ++i) { TNode eq = *i; Debug("cc") << "CC -- useList: " << eq << std::endl; - Assert(eq.getKind() == kind::EQUAL); + Assert(eq.getKind() == kind::EQUAL || + eq.getKind() == kind::IFF); // change from paper // use list elts can have form (apply c..) = x OR x = (apply c..) Assert(eq[0].getKind() == kind::APPLY_UF || eq[1].getKind() == kind::APPLY_UF); @@ -730,7 +740,8 @@ Node CongruenceClosure<OutputChannel>::normalize(TNode t) const Node theLookup = lookup(ap); if(allConstants && !theLookup.isNull()) { - Assert(theLookup.getKind() == kind::EQUAL); + Assert(theLookup.getKind() == kind::EQUAL || + theLookup.getKind() == kind::IFF); Assert(theLookup[0].getKind() == kind::APPLY_UF); Assert(theLookup[1].getKind() != kind::APPLY_UF); return find(theLookup[1]); @@ -769,7 +780,8 @@ void CongruenceClosure<OutputChannel>::explainAlongPath(TNode a, TNode c, std::l while(a != c) { Node b = d_proof[a]; Node e = d_proofLabel[a]; - if(e.getKind() == kind::EQUAL) { + if(e.getKind() == kind::EQUAL || + e.getKind() == kind::IFF) { pf.push_back(e); } else { Assert(e.getKind() == kind::TUPLE); @@ -900,6 +912,11 @@ std::ostream& operator<<(std::ostream& out, out << " " << (*i).first << " => " << n << std::endl; } + out << "Care set:" << std::endl; + for(typename CongruenceClosure<OutputChannel>::CareSet::const_iterator i = cc.d_careSet.begin(); i != cc.d_careSet.end(); ++i) { + out << " " << *i << std::endl; + } + out << "==============================================" << std::endl; return out; |