Be consistent

diff --git a/src/AST/boolean.c b/src/AST/boolean.c
index 39d7e107a7fce4e9ce96c379e1ae1f336a38afea..bcfd1d41bd4e406f39cb93663044d3144ebaa09d 100644 (file)
--- 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 17e29b6066fc4fcb4a85af5a77b88613d9b0106c..4ade14a0eed9707a68e10a6aef5e6bf6ee959b79 100644 (file)
--- 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 3cec4770d3601f34282bd3a74f6a62127b566012..36005e630a35366dc3cf380c99db6b5036437991 100644 (file)
--- 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 56079e9eff889db8783bf52b398a0a943eea71e4..6e6fbd06f3afbbf16eeb19c06903f445d337791e 100644 (file)
--- 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 8dd0b545ea22f4ee225959b407a799782f0412ca..2083d6074de106b87165056f92f9f839daf3386e 100644 (file)
--- 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;
 }