Add print routine for CNFExpr

diff --git a/src/Backend/cnfexpr.c b/src/Backend/cnfexpr.c
index 6bbbbfc7cf1f5f5fd6cd554e23ad23c8101b8116..dbbd93f53d51e6143db4a1bdbda6bf1102c2f4df 100644 (file)
--- a/src/Backend/cnfexpr.c
+++ b/src/Backend/cnfexpr.c
@@ -1,5 +1,5 @@
 #include "cnfexpr.h"
-
+#include <stdio.h>
 /* 
 V2 Copyright (c) 2014 Ben Chambers, Eugene Goldberg, Pete Manolios,
 Vasilis Papavasileiou, Sudarshan Srinivasan, and Daron Vroon.
@@ -445,5 +445,21 @@ void disjoinCNFExpr(CNFExpr *This, CNFExpr *expr, bool destroy) {
                deleteCNFExpr(expr);
 }
 
-
-
+void printCNFExpr(CNFExpr *This) {
+       for(uint i=0;i<getSizeLitVector(&This->singletons);i++) {
+               if (i!=0)
+                       printf(" ^ ");
+               Literal l=getLiteralLitVector(&This->singletons,i);
+               printf ("%d",l);
+       }
+       for(uint i=0;i<getSizeVectorLitVector(&This->clauses);i++) {
+               LitVector *lv=getVectorLitVector(&This->clauses,i);
+               printf(" ^ (");
+               for(uint j=0;j<getSizeLitVector(lv);j++) {
+                       if (j!=0)
+                               printf(" v ");
+                       printf("%d", getLiteralLitVector(lv, j));
+               }
+               printf(")");
+       }
+}

diff --git a/src/Backend/cnfexpr.h b/src/Backend/cnfexpr.h
index 5f1f9077d93e21277ef13128e2d784dd539c5570..1b64528d87b787ccc5e8f1f3a0bfba9108ffd34e 100644 (file)
--- a/src/Backend/cnfexpr.h
+++ b/src/Backend/cnfexpr.h
@@ -43,6 +43,7 @@ CNFExpr * allocCNFExprBool(bool isTrue);
 CNFExpr * allocCNFExprLiteral(Literal l);
 void deleteCNFExpr(CNFExpr *This);
 void clearCNFExpr(CNFExpr *This, bool isTrue);
+void printCNFExpr(CNFExpr *This);
 
 void copyCNF(CNFExpr *This, CNFExpr *expr, bool destroy);
 static inline bool alwaysTrueCNF(CNFExpr * This) {return (This->litSize==0) && This->isTrue;}