From: bdemsky <bdemsky@uci.edu>
Date: Mon, 10 Jul 2017 23:01:22 +0000 (-0700)
Subject: Add print routine for CNFExpr
X-Git-Url: http://demsky.eecs.uci.edu/git/?a=commitdiff_plain;h=d02c9c64672bf2eed2026cd626c03cafaf6324cb;p=satune.git

Add print routine for CNFExpr
---

diff --git a/src/Backend/cnfexpr.c b/src/Backend/cnfexpr.c
index 6bbbbfc..dbbd93f 100644
--- 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 5f1f907..1b64528 100644
--- 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;}