From: bdemsky <bdemsky@uci.edu>
Date: Wed, 21 Jun 2017 22:56:38 +0000 (-0700)
Subject: Be consistent
X-Git-Url: http://demsky.eecs.uci.edu/git/?a=commitdiff_plain;h=1ef513bcc82d5806cb1a123d968b411d28c0b019;p=satune.git

Be consistent
---

diff --git a/src/AST/boolean.c b/src/AST/boolean.c
index 39d7e10..bcfd1d4 100644
--- a/src/AST/boolean.c
+++ b/src/AST/boolean.c
@@ -26,7 +26,9 @@ Boolean * allocBooleanPredicate(Predicate * predicate, Element ** inputs, uint n
 	BooleanPredicate* This = (BooleanPredicate*) ourmalloc(sizeof(BooleanPredicate));
 	GETBOOLEANTYPE(This)= PREDICATEOP;
 	This->predicate=predicate;
-	This->inputs= allocVectorArrayElement (numInputs,inputs);
+	This->inputs=ourmalloc(sizeof(Element*)*numInputs);
+	memcpy(This->inputs, inputs, sizeof(Element*)*numInputs);
+	This->numInputs=numInputs;
 	allocInlineDefVectorBoolean(GETBOOLEANPARENTS(This));
 
 	for(uint i=0;i<numInputs;i++) {
@@ -38,7 +40,7 @@ Boolean * allocBooleanPredicate(Predicate * predicate, Element ** inputs, uint n
 Boolean * allocBooleanLogicArray(CSolver *solver, LogicOp op, Boolean ** array, uint asize){
 	BooleanLogic * This = ourmalloc(sizeof(BooleanLogic));
 	allocInlineDefVectorBoolean(GETBOOLEANPARENTS(This));
-	This->array = ourmalloc(sizeof(Boolean *)*asize);
+	This->array=ourmalloc(sizeof(Boolean *)*asize);
 	memcpy(This->array, array, sizeof(Boolean *)*asize);
 	for(uint i=0;i<asize;i++) {
 		pushVectorBoolean(GETBOOLEANPARENTS(array[i]), (Boolean *)This);
@@ -50,7 +52,7 @@ Boolean * allocBooleanLogicArray(CSolver *solver, LogicOp op, Boolean ** array,
 void deleteBoolean(Boolean * This) {
 	switch(GETBOOLEANTYPE(This)){
 		case PREDICATEOP:
-			deleteVectorArrayElement( ((BooleanPredicate*)This)->inputs );
+			ourfree(((BooleanPredicate*)This)->inputs );
 			break;
 		default:
 			break;
diff --git a/src/AST/boolean.h b/src/AST/boolean.h
index 17e29b6..4ade14a 100644
--- a/src/AST/boolean.h
+++ b/src/AST/boolean.h
@@ -41,7 +41,8 @@ struct BooleanLogic {
 struct BooleanPredicate {
 	Boolean base;
 	Predicate * predicate;
-	VectorElement* inputs;
+	Element** inputs;
+	int numInputs;
 };
 
 Boolean * allocBoolean(VarType t);
diff --git a/src/AST/element.c b/src/AST/element.c
index 3cec477..36005e6 100644
--- a/src/AST/element.c
+++ b/src/AST/element.c
@@ -15,7 +15,9 @@ Element* allocElementFunction(Function * function, Element ** array, uint numArr
 	GETELEMENTTYPE(tmp)= ELEMFUNCRETURN;
 	tmp->function=function;
 	tmp->overflowstatus = overflowstatus;
-	tmp->Elements = allocVectorArrayElement(numArrays, array);
+	tmp->inputs=ourmalloc(sizeof(Element *)*numArrays);
+	tmp->numInputs=numArrays;
+	memcpy(tmp->inputs, array, numArrays*sizeof(Element *));
 	allocInlineDefVectorASTNode(GETELEMENTPARENTS(tmp));
 	for(uint i=0;i<numArrays;i++)
 		pushVectorASTNode(GETELEMENTPARENTS(array[i]), (ASTNode *) tmp);
@@ -23,6 +25,13 @@ Element* allocElementFunction(Function * function, Element ** array, uint numArr
 }
 
 void deleteElement(Element *This) {
+	switch(GETELEMENTTYPE(This)) {
+	case ELEMFUNCRETURN:
+		ourfree(((ElementFunction *)This)->inputs);
+		break;
+	default:
+		;
+	}
 	deleteVectorArrayASTNode(GETELEMENTPARENTS(This));
 	ourfree(This);
 }
diff --git a/src/AST/element.h b/src/AST/element.h
index 56079e9..6e6fbd0 100644
--- a/src/AST/element.h
+++ b/src/AST/element.h
@@ -22,7 +22,8 @@ struct ElementSet {
 struct ElementFunction {
 	Element base;
 	Function * function;
-	VectorElement* Elements;
+	Element ** inputs;
+	uint numInputs;
 	Boolean * overflowstatus;
 };
 
diff --git a/src/Backend/satencoder.c b/src/Backend/satencoder.c
index 8dd0b54..2083d60 100644
--- a/src/Backend/satencoder.c
+++ b/src/Backend/satencoder.c
@@ -3,6 +3,7 @@
 #include "csolver.h"
 #include "boolean.h"
 #include "constraint.h"
+#include "common.h"
 
 SATEncoder * allocSATEncoder() {
 	SATEncoder *This=ourmalloc(sizeof (SATEncoder));
@@ -32,7 +33,7 @@ Constraint * encodeConstraintSATEncoder(SATEncoder *This, Boolean *constraint) {
 	case LOGICOP:
 		return encodeLogicSATEncoder(This, (BooleanLogic *) constraint);
 	default:
-		printf("Unhandled case in encodeConstraintSATEncoder %u", GETBOOLEANTYPE(constraint));
+		model_print("Unhandled case in encodeConstraintSATEncoder %u", GETBOOLEANTYPE(constraint));
 		exit(-1);
 	}
 }
@@ -78,9 +79,7 @@ Constraint * encodeLogicSATEncoder(SATEncoder *This, BooleanLogic * constraint)
 	case L_IMPLIES:
 		return allocConstraint(IMPLIES, array[0], array[1]);
 	default:
-		printf("Unhandled case in encodeLogicSATEncoder %u", constraint->op);
+		model_print("Unhandled case in encodeLogicSATEncoder %u", constraint->op);
 		exit(-1);
 	}
-	
-	return NULL;
 }