From 86f2a3e111137fecaf942050dfd7ade0c881d6eb Mon Sep 17 00:00:00 2001 From: =?utf8?q?Dejan=20Jovanovi=C4=87?= Date: Thu, 7 Jul 2011 14:03:14 +0000 Subject: [PATCH] removing duplicate clauses in ite cnf conversion --- src/prop/cnf_stream.cpp | 10 +--------- 1 file changed, 1 insertion(+), 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]); -- 2.30.2