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/theory/builtin | |
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/theory/builtin')
-rw-r--r-- | src/theory/builtin/theory_builtin.cpp | 16 |
1 files changed, 9 insertions, 7 deletions
diff --git a/src/theory/builtin/theory_builtin.cpp b/src/theory/builtin/theory_builtin.cpp index 174e10d2f..ba258aafd 100644 --- a/src/theory/builtin/theory_builtin.cpp +++ b/src/theory/builtin/theory_builtin.cpp @@ -20,8 +20,6 @@ #include "expr/kind.h" using namespace std; -using namespace CVC4; -using namespace CVC4::theory::builtin; namespace CVC4 { namespace theory { @@ -33,8 +31,10 @@ Node TheoryBuiltin::blastDistinct(TNode in) { if(in.getNumChildren() == 2) { // if this is the case exactly 1 != pair will be generated so the // AND is not required - Node eq = NodeManager::currentNM()->mkNode(CVC4::kind::EQUAL, in[0], in[1]); - Node neq = NodeManager::currentNM()->mkNode(CVC4::kind::NOT, eq); + Node eq = NodeManager::currentNM()->mkNode(in[0].getType().isBoolean() ? + kind::IFF : kind::EQUAL, + in[0], in[1]); + Node neq = NodeManager::currentNM()->mkNode(kind::NOT, eq); return neq; } // assume that in.getNumChildren() > 2 => diseqs.size() > 1 @@ -42,12 +42,14 @@ Node TheoryBuiltin::blastDistinct(TNode in) { for(TNode::iterator i = in.begin(); i != in.end(); ++i) { TNode::iterator j = i; while(++j != in.end()) { - Node eq = NodeManager::currentNM()->mkNode(CVC4::kind::EQUAL, *i, *j); - Node neq = NodeManager::currentNM()->mkNode(CVC4::kind::NOT, eq); + Node eq = NodeManager::currentNM()->mkNode((*i).getType().isBoolean() ? + kind::IFF : kind::EQUAL, + *i, *j); + Node neq = NodeManager::currentNM()->mkNode(kind::NOT, eq); diseqs.push_back(neq); } } - Node out = NodeManager::currentNM()->mkNode(CVC4::kind::AND, diseqs); + Node out = NodeManager::currentNM()->mkNode(kind::AND, diseqs); return out; } |