Fixing memory leaks

diff --git a/src/Backend/satorderencoder.c b/src/Backend/satorderencoder.c
index 4d6f639b51750f02c5e7cfc41958e8f22ea4ce7c..dee9b26f94959541ee7b9b9910f4e4d5317c7654 100644 (file)
--- a/src/Backend/satorderencoder.c
+++ b/src/Backend/satorderencoder.c
@@ -83,6 +83,9 @@ Edge getOrderConstraint(HashTableOrderPair *table, OrderPair *pair){
        if(value == NULL)
                return E_NULL;
        Edge constraint = value->constraint;
+       model_print("Constraint:\n");
+       printCNF(constraint);
+       model_print("\n***********\n");
        if(pair->first > pair->second || edgeIsNull(constraint))
                return constraint;
        else

diff --git a/src/Backend/sattranslator.c b/src/Backend/sattranslator.c
index 3bfc06b75c34d47108c96ce550178ac3df1b417d..ee228798023666ed3f3f5f48a2ea0f9efc0d1069 100644 (file)
--- a/src/Backend/sattranslator.c
+++ b/src/Backend/sattranslator.c
@@ -10,7 +10,7 @@ uint64_t getElementValueBinaryIndexSATTranslator(CSolver* This, ElementEncoding*
        uint index=0;
        for(int i=elemEnc->numVars-1;i>=0;i--) {
                index=index<<1;
-               if (This->satEncoder->cnf->solver->solution[ getEdgeVar( elemEnc->variables[i] ) ])
+               if (getValueSolver(This->satEncoder->cnf->solver, getEdgeVar( elemEnc->variables[i] )))
                        index |= 1;
        }
        ASSERT(elemEnc->encArraySize >index && isinUseElement(elemEnc, index));
@@ -22,7 +22,7 @@ uint64_t getElementValueBinaryValueSATTranslator(CSolver* This, ElementEncoding*
        uint64_t value=0;
        for(int i=elemEnc->numVars-1;i>=0;i--) {
                value=value<<1;
-               if (This->satEncoder->cnf->solver->solution[ getEdgeVar( elemEnc->variables[i] ) ])
+               if (getValueSolver(This->satEncoder->cnf->solver, getEdgeVar( elemEnc->variables[i] )) )
                        value |= 1;
        }
        return value;
@@ -31,7 +31,7 @@ uint64_t getElementValueBinaryValueSATTranslator(CSolver* This, ElementEncoding*
 uint64_t getElementValueOneHotSATTranslator(CSolver* This, ElementEncoding* elemEnc){
        uint index=0;
        for(int i=elemEnc->numVars-1;i>=0;i--) {
-               if (This->satEncoder->cnf->solver->solution[ getEdgeVar( elemEnc->variables[i] ) ])
+               if (getValueSolver(This->satEncoder->cnf->solver, getEdgeVar( elemEnc->variables[i] )))
                        index = i;
        }
        ASSERT(elemEnc->encArraySize >index && isinUseElement(elemEnc, index));
@@ -41,7 +41,7 @@ uint64_t getElementValueOneHotSATTranslator(CSolver* This, ElementEncoding* elem
 uint64_t getElementValueUnarySATTranslator(CSolver* This, ElementEncoding* elemEnc){
        uint i;
        for(i=0;i<elemEnc->numVars;i++) {
-               if (!This->satEncoder->cnf->solver->solution[ getEdgeVar( elemEnc->variables[i] ) ]) {
+               if (! getValueSolver(This->satEncoder->cnf->solver, getEdgeVar( elemEnc->variables[i] )) ) {
                        break;
                }
        }
@@ -77,16 +77,16 @@ uint64_t getElementValueSATTranslator(CSolver* This, Element* element){
 
 bool getBooleanVariableValueSATTranslator( CSolver* This , Boolean* boolean){
        int index = getEdgeVar( ((BooleanVar*) boolean)->var );
-       return This->satEncoder->cnf->solver->solution[index] == true;
+       return getValueSolver(This->satEncoder->cnf->solver, index);
 }
 
 HappenedBefore getOrderConstraintValueSATTranslator(CSolver* This, Order * order, uint64_t first, uint64_t second){
        ASSERT(order->orderPairTable!= NULL);
+       model_print("Frist:%llu\tSecond:%llu\n", first, second);
        OrderPair pair={first, second, E_NULL};
        Edge var = getOrderConstraint(order->orderPairTable, & pair);
        if(edgeIsNull(var))
                return UNORDERED;
-       int index = getEdgeVar( var );
-       return This->satEncoder->cnf->solver->solution[index] ? FIRST: SECOND;
+       return getValueCNF(This->satEncoder->cnf, var)? FIRST: SECOND;
 }