From: bdemsky <bdemsky@uci.edu>
Date: Mon, 10 Jul 2017 21:37:29 +0000 (-0700)
Subject: Another bug fix
X-Git-Url: http://demsky.eecs.uci.edu/git/?a=commitdiff_plain;h=6120ecdb7144ce0b55fa57352d9cc4e2411bcd08;p=satune.git

Another bug fix
---

diff --git a/src/Backend/nodeedge.c b/src/Backend/nodeedge.c
index 6349453..9e85bfc 100644
--- a/src/Backend/nodeedge.c
+++ b/src/Backend/nodeedge.c
@@ -245,7 +245,7 @@ Edge constraintIMPLIES(CNF * cnf, Edge left, Edge right) {
 }
 
 Edge constraintIFF(CNF * cnf, Edge left, Edge right) {
-	bool negate=sameSignEdge(left, right);
+	bool negate=!sameSignEdge(left, right);
 	Edge lpos=getNonNeg(left);
 	Edge rpos=getNonNeg(right);
 
@@ -314,13 +314,19 @@ Edge constraintNewVar(CNF *cnf) {
 	return e;
 }
 
-void solveCNF(CNF *cnf) {
+int solveCNF(CNF *cnf) {
 	countPass(cnf);
 	convertPass(cnf, false);
 	finishedClauses(cnf->solver);
-	solve(cnf->solver);
+	return solve(cnf->solver);
 }
 
+bool getValueCNF(CNF *cnf, Edge var) {
+	Literal l=getEdgeVar(var);
+	bool isneg=(l<0);
+	l=abs(l);
+	return isneg ^ getValueSolver(cnf->solver, l);
+}
 
 void countPass(CNF *cnf) {
 	uint numConstraints=getSizeVectorEdge(&cnf->constraints);
@@ -681,6 +687,43 @@ CNFExpr* fillArgs(CNF *cnf, Edge e, bool isNeg, Edge * largestEdge) {
 	return largest;
 }
 
+void printCNF(Edge e) {
+	if (edgeIsVarConst(e)) {
+		Literal l=getEdgeVar(e);
+		printf ("%d", l);
+		return;
+	}
+	bool isNeg=isNegEdge(e);
+	if (edgeIsConst(e)) {
+		if (isNeg)
+			printf("T");
+		else
+			printf("F");
+		return;
+	}
+	Node *n=getNodePtrFromEdge(e);
+	if (isNeg)
+		printf("!");
+	switch(getNodeType(e)) {
+	case NodeType_AND:
+		printf("and");
+		break;
+	case NodeType_ITE:
+		printf("ite");
+		break;
+	case NodeType_IFF:
+		printf("iff");
+		break;
+	}
+	printf("(");
+	for(uint i=0;i<n->numEdges;i++) {
+		Edge e=n->edges[i];
+		if (i!=0)
+			printf(" ");
+		printCNF(e);
+	}
+	printf(")");
+}
 
 CNFExpr * produceConjunction(CNF * cnf, Edge e) {
 	Edge largestEdge;
diff --git a/src/Backend/nodeedge.h b/src/Backend/nodeedge.h
index 95ee530..89ea40f 100644
--- a/src/Backend/nodeedge.h
+++ b/src/Backend/nodeedge.h
@@ -191,8 +191,9 @@ Edge constraintNewVar(CNF *cnf);
 void countPass(CNF *cnf);
 void countConstraint(CNF *cnf, VectorEdge * stack, Edge e);
 void addConstraint(CNF *cnf, Edge constraint);
-void solveCNF(CNF *cnf);
-
+int solveCNF(CNF *cnf);
+bool getValueCNF(CNF *cnf, Edge var);
+void printCNF(Edge e);
 
 void convertPass(CNF *cnf, bool backtrackLit);
 void convertConstraint(CNF *cnf, VectorEdge *stack, Edge e, bool backtrackLit);
diff --git a/src/Collections/vector.h b/src/Collections/vector.h
index 5b638e9..e0ebebd 100644
--- a/src/Collections/vector.h
+++ b/src/Collections/vector.h
@@ -35,7 +35,7 @@
 		Vector ## name * tmp = (Vector ## name *)ourmalloc(sizeof(Vector ## name));  \
 		tmp->size = 0;                                                      \
 		tmp->capacity = capacity;                                           \
-		tmp->array = (type *) ourcalloc(1, sizeof(type) * capacity);          \
+		tmp->array = (type *) ourmalloc(sizeof(type) * capacity);						\
 		return tmp;                                                         \
 	}                                                                     \
 	Vector ## name * allocVectorArray ## name(uint capacity, type * array)  { \
@@ -65,6 +65,7 @@
 		if (vector->size >= vector->capacity) {															\
 			uint newcap=vector->capacity << 1;																\
 			vector->array=(type *)ourrealloc(vector->array, newcap * sizeof(type)); \
+			vector->capacity=newcap;																					\
 		}                                                                   \
 		vector->array[vector->size++] = item;                               \
 	}                                                                     \
@@ -93,7 +94,7 @@
 	void allocInlineVector ## name(Vector ## name * vector, uint capacity) { \
 		vector->size = 0;                                                      \
 		vector->capacity = capacity;																							\
-		vector->array = (type *) ourcalloc(1, sizeof(type) * capacity);			\
+		vector->array = (type *) ourmalloc(sizeof(type) * capacity);				\
 	}																																			\
 	void allocInlineDefVector ## name(Vector ## name * vector) {					\
 		allocInlineVector ## name(vector, defcap);													\
diff --git a/src/Test/testcnf.c b/src/Test/testcnf.c
index 9405009..d5f4166 100644
--- a/src/Test/testcnf.c
+++ b/src/Test/testcnf.c
@@ -1,4 +1,5 @@
 #include "nodeedge.h"
+#include <stdio.h>
 
 int main(int numargs, char ** argv) {
 	CNF *cnf=createCNF();
@@ -6,13 +7,26 @@ int main(int numargs, char ** argv) {
 	Edge v2=constraintNewVar(cnf);
 	Edge v3=constraintNewVar(cnf);
 	Edge nv1=constraintNegate(v1);
+	printCNF(nv1);
+	printf("\n");
 	Edge nv2=constraintNegate(v2);
 	Edge iff1=constraintIFF(cnf, nv1, v2);
+	printCNF(iff1);
+	printf("\n");
 	Edge iff2=constraintIFF(cnf, nv2, v3);
-	//	Edge iff3=constraintIFF(cnf, v3, nv1);
-	//Edge cand=constraintAND(cnf, 3, (Edge[]) {iff1, iff2, iff3});
-	Edge cand=constraintAND(cnf, 2, (Edge[]) {iff1, iff2});
+	Edge iff3=constraintIFF(cnf, v3, nv1);
+	Edge cand=constraintAND(cnf, 3, (Edge[]) {iff1, iff2, iff3});
+	//Edge cand=constraintAND(cnf, 2, (Edge[]) {iff1, iff2});
+	printCNF(cand);
+	printf("\n");
 	addConstraint(cnf, cand);
-	solveCNF(cnf);
+	int value=solveCNF(cnf);
+	if (value==1) {
+		bool v1v=getValueCNF(cnf, v1);
+		bool v2v=getValueCNF(cnf, v2);
+		bool v3v=getValueCNF(cnf, v3);
+		printf("%d %u %u %u\n", value, v1v, v2v, v3v);
+	} else
+		printf("%d\n",value);
 	deleteCNF(cnf);
 }