diff options
| author | ajreynol <andrew.j.reynolds@gmail.com> | 2017-03-02 14:45:21 -0600 |
|---|---|---|
| committer | ajreynol <andrew.j.reynolds@gmail.com> | 2017-03-02 14:45:21 -0600 |
| commit | 1f4b954a2cc7667a56a3007fa75c125fba93ed23 (patch) | |
| tree | ea8734e89aa5fba170781c7148d3fd886c597d4e /src/prop/cnf_stream.cpp | |
| parent | 21b0cedd7dadd96e5d256885e3b65a926a7e4a81 (diff) | |
Eliminate Boolean term conversion. Generalizes removeITE pass to remove Boolean terms, treats distinguished BOOLEAN_TERM_VARIABLE kind as theory literal. Fixes bugs 597, 604, 651, 652, 691, 694. Add regressions.
Diffstat (limited to 'src/prop/cnf_stream.cpp')
| -rw-r--r-- | src/prop/cnf_stream.cpp | 18 |
1 files changed, 8 insertions, 10 deletions
diff --git a/src/prop/cnf_stream.cpp b/src/prop/cnf_stream.cpp index f2401041e..bc819801b 100644 --- a/src/prop/cnf_stream.cpp +++ b/src/prop/cnf_stream.cpp @@ -242,7 +242,7 @@ SatLiteral CnfStream::convertAtom(TNode node, bool noPreregistration) { bool preRegister = false; // Is this a variable add it to the list - if (node.isVar()) { + if (node.isVar() && node.getKind()!=BOOLEAN_TERM_VARIABLE) { d_booleanVariables.push_back(node); } else { theoryLiteral = true; @@ -389,7 +389,7 @@ SatLiteral TseitinCnfStream::handleImplies(TNode impliesNode) { SatLiteral TseitinCnfStream::handleIff(TNode iffNode) { Assert(!hasLiteral(iffNode), "Atom already mapped!"); - Assert(iffNode.getKind() == IFF, "Expecting an IFF expression!"); + Assert(iffNode.getKind() == EQUAL, "Expecting an EQUAL expression!"); Assert(iffNode.getNumChildren() == 2, "Expecting exactly 2 children!"); Debug("cnf") << "handleIff(" << iffNode << ")" << endl; @@ -488,9 +488,6 @@ SatLiteral TseitinCnfStream::toCNF(TNode node, bool negated) { case ITE: nodeLit = handleIte(node); break; - case IFF: - nodeLit = handleIff(node); - break; case IMPLIES: nodeLit = handleImplies(node); break; @@ -502,8 +499,7 @@ SatLiteral TseitinCnfStream::toCNF(TNode node, bool negated) { break; case EQUAL: if(node[0].getType().isBoolean()) { - // normally this is an IFF, but EQUAL is possible with pseudobooleans - nodeLit = handleIff(node[0].iffNode(node[1])); + nodeLit = handleIff(node); } else { nodeLit = convertAtom(node); } @@ -722,9 +718,6 @@ void TseitinCnfStream::convertAndAssert(TNode node, bool negated) { case OR: convertAndAssertOr(node, negated); break; - case IFF: - convertAndAssertIff(node, negated); - break; case XOR: convertAndAssertXor(node, negated); break; @@ -737,6 +730,11 @@ void TseitinCnfStream::convertAndAssert(TNode node, bool negated) { case NOT: convertAndAssert(node[0], !negated); break; + case EQUAL: + if( node[0].getType().isBoolean() ){ + convertAndAssertIff(node, negated); + break; + } default: { Node nnode = node; |