diff options
author | Dejan Jovanović <dejan.jovanovic@gmail.com> | 2011-07-07 14:03:14 +0000 |
---|---|---|
committer | Dejan Jovanović <dejan.jovanovic@gmail.com> | 2011-07-07 14:03:14 +0000 |
commit | 86f2a3e111137fecaf942050dfd7ade0c881d6eb (patch) | |
tree | 44354ac7485befada8d0a8f462b2f4e6f17f227c /src/prop | |
parent | c5ffeb50b60e0aaaac0b1e64a345f048def1629f (diff) |
removing duplicate clauses in ite cnf conversion
Diffstat (limited to 'src/prop')
-rw-r--r-- | src/prop/cnf_stream.cpp | 10 |
1 files changed, 1 insertions, 9 deletions
diff --git a/src/prop/cnf_stream.cpp b/src/prop/cnf_stream.cpp index 0967f54ff..36df53ca3 100644 --- a/src/prop/cnf_stream.cpp +++ b/src/prop/cnf_stream.cpp @@ -560,7 +560,7 @@ void TseitinCnfStream::convertAndAssertIte(TNode node, bool lemma, bool negated) SatLiteral q = toCNF(node[1], negated); SatLiteral r = toCNF(node[2], negated); // Construct the clauses: - // (p => q) and (!p => r) and (!q => !p) and (!r => p) + // (p => q) and (!p => r) SatClause clause1(2); clause1[0] = ~p; clause1[1] = q; @@ -569,14 +569,6 @@ void TseitinCnfStream::convertAndAssertIte(TNode node, bool lemma, bool negated) clause2[0] = p; clause2[1] = r; assertClause(node, clause2); - SatClause clause3(2); - clause3[0] = q; - clause3[1] = ~p; - assertClause(node, clause3); - SatClause clause4(2); - clause4[0] = r; - clause4[1] = p; - assertClause(node, clause4); recordTranslation(node[0]); recordTranslation(node[1]); |