From dad38b888a7e3da094ce29e0b3d69cc771d489f1 Mon Sep 17 00:00:00 2001
From: bdemsky <bdemsky@uci.edu>
Date: Sun, 9 Jul 2017 22:23:15 -0700
Subject: [PATCH] edits

---
 src/Backend/cnfexpr.c    | 10 ++++++----
 src/Backend/cnfexpr.h    |  9 ++++-----
 src/Backend/nodeedge.c   |  5 +++--
 src/Collections/vector.h |  2 +-
 4 files changed, 14 insertions(+), 12 deletions(-)

diff --git a/src/Backend/cnfexpr.c b/src/Backend/cnfexpr.c
index aebc546..07d13fa 100644
--- a/src/Backend/cnfexpr.c
+++ b/src/Backend/cnfexpr.c
@@ -38,6 +38,8 @@ C port of CNF SAT Conversion Copyright Brian Demsky 2017.
 #define LITCAPACITY 4
 #define MERGESIZE 5
 
+VectorImpl(LitVector, LitVector *, 4)
+
 static inline uint boundedSize(uint x) { return (x > MERGESIZE)?MERGESIZE:x; }
 
 LitVector * allocLitVector() {
@@ -157,7 +159,7 @@ void conjoinCNFLit(CNFExpr *This, Literal l) {
 	addLiteralLitVector(&This->singletons, l);
 	uint newsize=getSizeLitVector(&This->singletons);
 	if (newsize==0)
-		clearCNF(This, false); //We found a conflict
+		clearCNFExpr(This, false); //We found a conflict
 	else
 		This->litSize+=getSizeLitVector(&This->singletons);
 }
@@ -189,7 +191,7 @@ void copyCNF(CNFExpr *This, CNFExpr *expr, bool destroy) {
 void conjoinCNFExpr(CNFExpr *This, CNFExpr *expr, bool destroy) {
 	if (expr->litSize==0) {
 		if (!This->isTrue) {
-			clearCNF(This, false);
+			clearCNFExpr(This, false);
 		}
 		if (destroy) {
 			deleteCNFExpr(expr);
@@ -211,7 +213,7 @@ void conjoinCNFExpr(CNFExpr *This, CNFExpr *expr, bool destroy) {
 		addLiteralLitVector(&This->singletons, l);
 		if (getSizeLitVector(&This->singletons)==0) {
 			//Found conflict...
-			clearCNF(This, false);
+			clearCNFExpr(This, false);
 			if (destroy) {
 				deleteCNFExpr(expr);
 			}
@@ -341,7 +343,7 @@ void disjoinCNFExpr(CNFExpr *This, CNFExpr *expr, bool destroy) {
 	/** Handle the special cases */
 	if (expr->litSize == 0) {
 		if (expr->isTrue) {
-			clearCNF(This, true);
+			clearCNFExpr(This, true);
 		}
 		if (destroy) {
 			deleteCNFExpr(expr);
diff --git a/src/Backend/cnfexpr.h b/src/Backend/cnfexpr.h
index d76914a..5f1f907 100644
--- a/src/Backend/cnfexpr.h
+++ b/src/Backend/cnfexpr.h
@@ -45,11 +45,10 @@ void deleteCNFExpr(CNFExpr *This);
 void clearCNFExpr(CNFExpr *This, bool isTrue);
 
 void copyCNF(CNFExpr *This, CNFExpr *expr, bool destroy);
-bool alwaysTrueCNF(CNFExpr * This);
-bool alwaysFalseCNF(CNFExpr * This);
-uint getLitSizeCNF(CNFExpr * This);
-void clearCNF(CNFExpr *This, bool isTrue);
-uint getClauseSizeCNF(CNFExpr * This);
+static inline bool alwaysTrueCNF(CNFExpr * This) {return (This->litSize==0) && This->isTrue;}
+static inline bool alwaysFalseCNF(CNFExpr * This) {return (This->litSize==0) && !This->isTrue;}
+static inline uint getLitSizeCNF(CNFExpr * This) {return This->litSize;}
+static inline uint getClauseSizeCNF(CNFExpr * This) {return getSizeLitVector(&This->singletons) + getSizeVectorLitVector(&This->clauses);}
 void conjoinCNFLit(CNFExpr *This, Literal l);
 void disjoinCNFLit(CNFExpr *This, Literal l);
 void disjoinCNFExpr(CNFExpr *This, CNFExpr *expr, bool destroy);
diff --git a/src/Backend/nodeedge.c b/src/Backend/nodeedge.c
index f31a098..f836fff 100644
--- a/src/Backend/nodeedge.c
+++ b/src/Backend/nodeedge.c
@@ -136,7 +136,7 @@ Edge createNode(CNF *cnf, NodeType type, uint numEdges, Edge * edges) {
 uint hashNode(NodeType type, uint numEdges, Edge * edges) {
 	uint hashvalue=type ^ numEdges;
 	for(uint i=0;i<numEdges;i++) {
-		hashvalue ^= (uint) edges[i].node_ptr;
+		hashvalue ^= (uint) ((uintptr_t) edges[i].node_ptr);
 		hashvalue = (hashvalue << 3) | (hashvalue >> 29); //rotate left by 3 bits
 	}
 	return (uint) hashvalue;
@@ -546,7 +546,8 @@ void produceCNF(CNF * cnf, Edge e) {
 	/// propagate(solver, expPos, snPos, false) || propagate(solver, expNeg, snNeg, false)
 	
 	// propagate from positive to negative, negative to positive
-	propagate(cnf, & expPos, expNeg, true) || propagate(cnf, & expNeg, expPos, true);
+	if (!propagate(cnf, & expPos, expNeg, true))
+		propagate(cnf, & expNeg, expPos, true);
 	
 	// The polarity heuristic entails visiting the discovery polarity first
 	if (isPosEdge(e)) {
diff --git a/src/Collections/vector.h b/src/Collections/vector.h
index fdaf0f4..0538ff3 100644
--- a/src/Collections/vector.h
+++ b/src/Collections/vector.h
@@ -48,7 +48,7 @@
 		vector->size--;																											\
 	}																																			\
 	type lastVector ## name(Vector ## name *vector) {											\
-		return vector->array[vector->size];																	\
+		return vector->array[vector->size-1];																\
 	}																																			\
 	void setSizeVector ## name(Vector ## name *vector, uint size) {				\
 		if (size <= vector->size) {																					\
-- 
2.34.1