From: Dejan Jovanović <dejan.jovanovic@gmail.com>
Date: Sat, 13 Feb 2010 00:55:40 +0000 (+0000)
Subject: Improvements to CNF conversion when already in CNF
X-Git-Tag: cvc5-1.0.0~9255
X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=e063e5258a2a223cc0ab3aee3cb30041c4b907f8;p=cvc5.git

Improvements to CNF conversion when already in CNF
---

diff --git a/src/prop/cnf_stream.cpp b/src/prop/cnf_stream.cpp
index 011d8ba5a..a96d499b6 100644
--- a/src/prop/cnf_stream.cpp
+++ b/src/prop/cnf_stream.cpp
@@ -318,6 +318,28 @@ SatLiteral TseitinCnfStream::toCNF(const Node& node) {
 
 void TseitinCnfStream::convertAndAssert(const Node& node) {
   Debug("cnf") << "convertAndAssert(" << node << ")" << endl;
+  // If the node is a conjuntion, we handle each conjunct separatelu
+  if (node.getKind() == AND) {
+    Node::iterator conjunct = node.begin();
+    Node::iterator node_end = node.end();
+    while (conjunct != node_end) {
+      convertAndAssert(*conjunct);
+      ++ conjunct;
+    }
+    return;
+  }
+  // If the node is a disjunction, we construct a clause and assert it
+  if (node.getKind() == OR) {
+    int nChildren = node.getNumChildren();
+    SatClause clause(nChildren);
+    Node::iterator disjunct = node.begin();
+    for (int i = 0; i < nChildren; ++ disjunct, ++ i) {
+      clause[i] = toCNF(*disjunct);
+    }
+    assertClause(clause);
+    return;
+  }
+  // Otherwise, we just convert using the definitional transformation
   assertClause(toCNF(node));
 }