From: Dejan Jovanović <dejan.jovanovic@gmail.com>
Date: Thu, 7 Jul 2011 14:03:14 +0000 (+0000)
Subject: removing duplicate clauses in ite cnf conversion
X-Git-Tag: cvc5-1.0.0~8520
X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=86f2a3e111137fecaf942050dfd7ade0c881d6eb;p=cvc5.git

removing duplicate clauses in ite cnf conversion
---

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]);