Fixing some bugs

diff --git a/src/Backend/satencoder.c b/src/Backend/satencoder.c
index 70bfce095076c0b4d888800690936a177181f396..5a90b6c8e5d7e19200fdae0dcd6dc1bc184fe60e 100644 (file)
--- a/src/Backend/satencoder.c
+++ b/src/Backend/satencoder.c
@@ -82,21 +82,6 @@ void encodeAllSATEncoder(CSolver *csolver, SATEncoder * This) {
                Boolean *constraint=getVectorBoolean(constraints, i);
                encodeConstraintSATEncoder(This, constraint);
        }
-       
-//     FIXME: Following line for element!
-//     size = getSizeVectorElement(csolver->allElements);
-//     for(uint i=0; i<size; i++){
-//             Element* element = getVectorElement(csolver->allElements, i);
-//             switch(GETELEMENTTYPE(element)){
-//                     case ELEMFUNCRETURN: 
-//                             encodeFunctionElementSATEncoder(This, (ElementFunction*) element);
-//                             break;
-//                     default:        
-//                             continue;
-//                             //ElementSets that aren't used in any constraints/functions
-//                             //will be eliminated.
-//             }
-//     }
 }
 
 Constraint * encodeConstraintSATEncoder(SATEncoder *This, Boolean *constraint) {
@@ -330,8 +315,10 @@ Constraint * encodeEnumTablePredicateSATEncoder(SATEncoder * This, BooleanPredic
                ArrayElement* inputs = &constraint->inputs;
                uint inputNum =getSizeArrayElement(inputs);
                Constraint* carray[inputNum];
-               Element* el = getArrayElement(inputs, i);
                for(uint j=0; j<inputNum; j++){
+                       Element* el = getArrayElement(inputs, j);
+                       if( GETELEMENTTYPE(el) == ELEMFUNCRETURN)
+                               encodeFunctionElementSATEncoder(This, (ElementFunction*) el);
                        carray[j] = getElementValueConstraint(el, entry->inputs[j]);
                }
                constraints[i]=allocArrayConstraint(AND, inputNum, carray);
@@ -364,9 +351,12 @@ Constraint * encodeEnumOperatorPredicateSATEncoder(SATEncoder * This, BooleanPre
        getEqualitySetIntersection(predicate, &size, commonElements);
        Constraint*  carray[size];
        Element* elem1 = getArrayElement( &constraint->inputs, 0);
+       if( GETELEMENTTYPE(elem1) == ELEMFUNCRETURN)
+               encodeFunctionElementSATEncoder(This, (ElementFunction*) elem1);
        Element* elem2 = getArrayElement( &constraint->inputs, 1);
+       if( GETELEMENTTYPE(elem2) == ELEMFUNCRETURN)
+               encodeFunctionElementSATEncoder(This, (ElementFunction*) elem2);
        for(uint i=0; i<size; i++){
-               
                carray[i] =  allocConstraint(AND, getElementValueConstraint(elem1, commonElements[i]),
                        getElementValueConstraint(elem2, commonElements[i]) );
        }
@@ -414,10 +404,10 @@ Constraint* encodeEnumTableElemFunctionSATEncoder(SATEncoder* encoder, ElementFu
        for(uint i=0; i<size; i++){
                TableEntry* entry = getVectorTableEntry(&table->entries, i);
                uint inputNum =getSizeArrayElement(elements);
-               Element* el= getArrayElement(elements, i);
                Constraint* carray[inputNum];
                for(uint j=0; j<inputNum; j++){
-                       carray[inputNum] = getElementValueConstraint(el, entry->inputs[j]);
+                       Element* el= getArrayElement(elements, j);
+                       carray[j] = getElementValueConstraint(el, entry->inputs[j]);
                }
                Constraint* row= allocConstraint(IMPLIES, allocArrayConstraint(AND, inputNum, carray),
                        getElementValueBinaryIndexConstraint((Element*)This, entry->output));

diff --git a/src/csolver.c b/src/csolver.c
index 60240990e484371648b6e1b613d5cc8054284aca..68fb39fc3855f4ed3472b677e1daa07a5bca7f2a 100644 (file)
--- a/src/csolver.c
+++ b/src/csolver.c
@@ -174,7 +174,7 @@ Boolean * orderConstraint(CSolver *solver, Order * order, uint64_t first, uint64
 void encode(CSolver* solver){
        naiveEncodingDecision(solver);
        SATEncoder* satEncoder = allocSATEncoder();
-       initializeConstraintVars(solver, satEncoder);
+//     initializeConstraintVars(solver, satEncoder);
        encodeAllSATEncoder(solver, satEncoder);
        //For now, let's just delete it, and in future for doing queries 
        //we may need it.