From: bdemsky <bdemsky@uci.edu>
Date: Mon, 10 Jul 2017 02:20:49 +0000 (-0700)
Subject: Start CNF Test Case
X-Git-Url: http://demsky.eecs.uci.edu/git/?a=commitdiff_plain;h=9c99d9f2fa508e3122c9cf8d68109bd1d03f348c;p=satune.git

Start CNF Test Case
---

diff --git a/src/Backend/nodeedge.c b/src/Backend/nodeedge.c
index a1e596f..a6d9dcc 100644
--- a/src/Backend/nodeedge.c
+++ b/src/Backend/nodeedge.c
@@ -519,19 +519,19 @@ bool propagate(CNF *cnf, CNFExpr ** dest, CNFExpr * src, bool negate) {
 	if (src != NULL && !isProxy(src) && getLitSizeCNF(src) == 0) {
 		if (dest == NULL) {
 			*dest = allocCNFExprBool(negate ? alwaysFalseCNF(src) : alwaysTrueCNF(src));
-		} else if (isProxy(dest)) {
+		} else if (isProxy(*dest)) {
 			bool alwaysTrue = (negate ? alwaysFalseCNF(src) : alwaysTrueCNF(src));
 			if (alwaysTrue) {
-				Literal clause[] = {getProxy(dest)};
+				Literal clause[] = {getProxy(*dest)};
 				addArrayClauseLiteral(cnf->solver, 1, clause);
 			} else {
-				Literal clause[] = {-getProxy(dest)};
+				Literal clause[] = {-getProxy(*dest)};
 				addArrayClauseLiteral(cnf->solver, 1, clause);
 			}
 			
 			*dest = allocCNFExprBool(negate ? alwaysFalseCNF(src) : alwaysTrueCNF(src));
 		} else {
-			clearCNFExpr(dest, negate ? alwaysFalseCNF(src) : alwaysTrueCNF(src));
+			clearCNFExpr(*dest, negate ? alwaysFalseCNF(src) : alwaysTrueCNF(src));
 		}
 		return true;
 	}
diff --git a/src/Backend/nodeedge.h b/src/Backend/nodeedge.h
index ee9502b..aff2c35 100644
--- a/src/Backend/nodeedge.h
+++ b/src/Backend/nodeedge.h
@@ -173,6 +173,9 @@ static inline Literal getProxy(CNFExpr *expr) {
 	return (Literal) (((intptr_t) expr) >> 1);
 }
 
+CNF * createCNF();
+void deleteCNF(CNF * cnf);
+
 uint hashNode(NodeType type, uint numEdges, Edge * edges);
 Node * allocNode(NodeType type, uint numEdges, Edge * edges, uint hashCode);
 bool compareNodes(Node * node, NodeType type, uint numEdges, Edge *edges);
@@ -187,6 +190,10 @@ Edge constraintITE(CNF * cnf, Edge cond, Edge thenedge, Edge elseedge);
 Edge constraintNewVar(CNF *cnf);
 void countPass(CNF *cnf);
 void countConstraint(CNF *cnf, VectorEdge * stack, Edge e);
+void addConstraint(CNF *cnf, Edge constraint);
+
+
+
 void convertPass(CNF *cnf, bool backtrackLit);
 void convertConstraint(CNF *cnf, VectorEdge *stack, Edge e, bool backtrackLit);
 void constrainCNF(CNF * cnf, Literal l, CNFExpr *exp);
diff --git a/src/Test/Makefile b/src/Test/Makefile
index b3b7cb3..be27d60 100644
--- a/src/Test/Makefile
+++ b/src/Test/Makefile
@@ -6,7 +6,7 @@ include $(BASE)/common.mk
 
 DEPS := $(join $(addsuffix ., $(dir $(OBJECTS))), $(addsuffix .d, $(notdir $(OBJECTS))))
 
-CPPFLAGS += -I$(BASE) -I$(BASE)/AST -I$(BASE)/Collections
+CPPFLAGS += -I$(BASE) -I$(BASE)/AST -I$(BASE)/Collections -I$(BASE)/Backend
 
 all: $(OBJECTS) ../bin/run.sh
 
diff --git a/src/Test/testcnf.c b/src/Test/testcnf.c
new file mode 100644
index 0000000..68e2104
--- /dev/null
+++ b/src/Test/testcnf.c
@@ -0,0 +1,16 @@
+#include "nodeedge.h"
+
+int main(int numargs, char ** argv) {
+	CNF *cnf=createCNF();
+	Edge v1=constraintNewVar(cnf);
+	Edge v2=constraintNewVar(cnf);
+	Edge v3=constraintNewVar(cnf);
+	Edge nv1=constraintNegate(v1);
+	Edge nv2=constraintNegate(v2);
+	Edge iff1=constraintIFF(cnf, nv1, v2);
+	Edge iff2=constraintIFF(cnf, nv2, v3);
+	Edge iff3=constraintIFF(cnf, v3, nv1);
+	Edge cand=constraintAND(cnf, 3, (Edge[]) {iff1, iff2, iff3});
+	addConstraint(cnf, cand);
+	deleteCNF(cnf);
+}