diff options
author | Morgan Deters <mdeters@gmail.com> | 2010-07-10 21:52:59 +0000 |
---|---|---|
committer | Morgan Deters <mdeters@gmail.com> | 2010-07-10 21:52:59 +0000 |
commit | fc7bebbc12a38260b35442d7f9fe2da83d2525f1 (patch) | |
tree | 470b1abdc0df3dc42aec708ed6820a4a335e4e33 | |
parent | 8da0767634cb225da59af947328d6f5d8d24ad29 (diff) |
cnf bugfix for SMT2 ???
-rw-r--r-- | src/prop/cnf_stream.cpp | 7 |
1 files changed, 7 insertions, 0 deletions
diff --git a/src/prop/cnf_stream.cpp b/src/prop/cnf_stream.cpp index 9136a73c3..e95322348 100644 --- a/src/prop/cnf_stream.cpp +++ b/src/prop/cnf_stream.cpp @@ -364,6 +364,13 @@ SatLiteral TseitinCnfStream::toCNF(TNode node, bool negated) { case AND: nodeLit = handleAnd(node); break; + case EQUAL: + if(node[0].getType().isBoolean() && node[1].getType().isBoolean()) { + nodeLit = handleIff(node[0].iffNode(node[1])); + } else { + nodeLit = convertAtom(node); + } + break; default: { //TODO make sure this does not contain any boolean substructure |