Fixing more bugs

diff --git a/src/AST/function.c b/src/AST/function.c
index 65aea05acf939ab12eb5bd5f61ede77ee6507f5f..61e413b88ebdf1ce42553288b4a1a0495bdc5c29 100644 (file)
--- a/src/AST/function.c
+++ b/src/AST/function.c
@@ -20,18 +20,14 @@ Function* allocFunctionTable (Table* table){
        return &This->base;
 }
 
-uint64_t applyFunctionOperator(FunctionOperator* func, uint64_t var1, uint64_t var2, bool* isInRange, bool* hasOverFlow){
+uint64_t applyFunctionOperator(FunctionOperator* func, uint64_t var1, uint64_t var2, bool* isInRange){
        uint64_t result = 0;
        switch( func->op){
                case ADD:
                        result = var1+ var2;
-                       if(result < var1){
-                               *hasOverFlow=true;
-                       }
                        break;
                case SUB:
                        result = var1 - var2;
-                       //FIXME: Should we consider underflow as well?
                        break;
                default:
                        ASSERT(0);

diff --git a/src/AST/function.h b/src/AST/function.h
index 5180ba1ed7b1570c1c68917085fa689f07c169cd..158a55c9059f0650b2dbab700af63434781ea844 100644 (file)
--- a/src/AST/function.h
+++ b/src/AST/function.h
@@ -26,7 +26,7 @@ struct FunctionTable {
 
 Function* allocFunctionOperator( ArithOp op, Set ** domain, uint numDomain, Set * range,OverFlowBehavior overflowbehavior);
 Function* allocFunctionTable (Table* table);
-uint64_t applyFunctionOperator(FunctionOperator* func, uint64_t var1, uint64_t var2, bool* isInrange, bool* hasOverFlow);
+uint64_t applyFunctionOperator(FunctionOperator* func, uint64_t var1, uint64_t var2, bool* isInrange);
 void deleteFunction(Function* This);
 
 #endif

diff --git a/src/AST/order.c b/src/AST/order.c
index 19b1c6e57d41529b1e7e60fd28c9bfd291ca2b38..2f3de74478ef26928919c5a53aea039aa48cdd3a 100644 (file)
--- a/src/AST/order.c
+++ b/src/AST/order.c
@@ -10,10 +10,14 @@ Order* allocOrder(OrderType type, Set * set){
        allocInlineDefVectorBoolean(& order->constraints);
        order->type=type;
        allocOrderEncoding(& order->order, order);
-       order->boolsToConstraints = allocHashTableBoolConst(HT_INITIAL_CAPACITY, HT_DEFAULT_FACTOR);
+       order->boolsToConstraints = NULL;
        return order;
 }
 
+void initializeOrderHashTable(Order* order){
+       order->boolsToConstraints= allocHashTableBoolConst(HT_INITIAL_CAPACITY, HT_DEFAULT_FACTOR);
+}
+
 void addOrderConstraint(Order* order, BooleanOrder* constraint){
        pushVectorBoolean( &order->constraints, (Boolean*) constraint);
 }

diff --git a/src/AST/order.h b/src/AST/order.h
index 933d831a3a53114cc8b3072e05cd9232055d179b..67f0d9928b5406e0df0b2bbd0fcf21e4b169f3c1 100644 (file)
--- a/src/AST/order.h
+++ b/src/AST/order.h
@@ -16,6 +16,7 @@ struct Order {
 };
 
 Order* allocOrder(OrderType type, Set * set);
+void initializeOrderHashTable(Order * order);
 void addOrderConstraint(Order* order, BooleanOrder* constraint);
 void setOrderEncodingType(Order* order, OrderEncodingType type);
 void deleteOrder(Order* order);

diff --git a/src/Backend/satencoder.c b/src/Backend/satencoder.c
index 8607b65020027e01261fd4f082010096ee1181da..e78cb3f634764c3d65fd68b971b313f087745c61 100644 (file)
--- a/src/Backend/satencoder.c
+++ b/src/Backend/satencoder.c
@@ -67,7 +67,7 @@ void encodeAllSATEncoder(CSolver *csolver, SATEncoder * This) {
                Boolean *constraint=getVectorBoolean(constraints, i);
                Constraint* c= encodeConstraintSATEncoder(This, constraint);
                printConstraint(c);
-               model_print("\n");
+               model_print("\n\n");
        }
 }
 
@@ -157,7 +157,7 @@ Constraint * getPairConstraint(SATEncoder *This, HashTableBoolConst * table, Ord
                negate=true;
                flipped.first=pair->second;
                flipped.second=pair->first;
-               pair = &flipped;
+               pair = &flipped;        //FIXME: accessing a local variable from outside of the function?
        }
        Constraint * constraint;
        if (!containsBoolConst(table, pair)) {
@@ -175,6 +175,10 @@ Constraint * getPairConstraint(SATEncoder *This, HashTableBoolConst * table, Ord
 
 Constraint * encodeTotalOrderSATEncoder(SATEncoder *This, BooleanOrder * boolOrder){
        ASSERT(boolOrder->order->type == TOTAL);
+       if(boolOrder->order->boolsToConstraints == NULL){
+               initializeOrderHashTable(boolOrder->order);
+               return createAllTotalOrderConstraintsSATEncoder(This, boolOrder->order);
+       }
        HashTableBoolConst* boolToConsts = boolOrder->order->boolsToConstraints;
        OrderPair pair={boolOrder->first, boolOrder->second};
        Constraint* constraint = getPairConstraint(This, boolToConsts, & pair);
@@ -182,11 +186,13 @@ Constraint * encodeTotalOrderSATEncoder(SATEncoder *This, BooleanOrder * boolOrd
        return constraint;
 }
 
-void createAllTotalOrderConstraintsSATEncoder(SATEncoder* This, Order* order){
+Constraint* createAllTotalOrderConstraintsSATEncoder(SATEncoder* This, Order* order){
        ASSERT(order->type == TOTAL);
        VectorInt* mems = order->set->members;
        HashTableBoolConst* table = order->boolsToConstraints;
        uint size = getSizeVectorInt(mems);
+       Constraint* constraints [size*size];
+       uint csize =0;
        for(uint i=0; i<size; i++){
                uint64_t valueI = getVectorInt(mems, i);
                for(uint j=i+1; j<size;j++){
@@ -199,10 +205,12 @@ void createAllTotalOrderConstraintsSATEncoder(SATEncoder* This, Order* order){
                                OrderPair pairIK = {valueI, valueK};
                                Constraint* constIK = getPairConstraint(This, table, & pairIK);
                                Constraint* constJK = getPairConstraint(This, table, & pairJK);
-                               generateTransOrderConstraintSATEncoder(This, constIJ, constJK, constIK); 
+                               constraints[csize++] = generateTransOrderConstraintSATEncoder(This, constIJ, constJK, constIK); 
+                               ASSERT(csize < size*size);
                        }
                }
        }
+       return allocArrayConstraint(AND, csize, constraints);
 }
 
 Constraint* getOrderConstraint(HashTableBoolConst *table, OrderPair *pair){
@@ -306,9 +314,15 @@ Constraint * encodeEnumTablePredicateSATEncoder(SATEncoder * This, BooleanPredic
                Constraint* carray[inputNum];
                for(uint j=0; j<inputNum; j++){
                        Element* el = getArrayElement(inputs, j);
-                       if( GETELEMENTTYPE(el) == ELEMFUNCRETURN)
-                               encodeFunctionElementSATEncoder(This, (ElementFunction*) el);
-                       carray[j] = getElementValueConstraint(This,el, entry->inputs[j]);
+                       Constraint* tmpc = getElementValueConstraint(This,el, entry->inputs[j]);
+                       ASSERT(tmpc!= NULL);
+                       if( GETELEMENTTYPE(el) == ELEMFUNCRETURN){
+                               Constraint* func =encodeFunctionElementSATEncoder(This, (ElementFunction*) el);
+                               ASSERT(func!=NULL);
+                               carray[j] = allocConstraint(AND, func, tmpc);
+                       } else {
+                               carray[j] = tmpc;
+                       }
                        ASSERT(carray[j]!= NULL);
                }
                constraints[i]=allocArrayConstraint(AND, inputNum, carray);
@@ -341,11 +355,12 @@ Constraint * encodeEnumOperatorPredicateSATEncoder(SATEncoder * This, BooleanPre
        getEqualitySetIntersection(predicate, &size, commonElements);
        Constraint*  carray[size];
        Element* elem1 = getArrayElement( &constraint->inputs, 0);
+       Constraint *elemc1 = NULL, *elemc2 = NULL;
        if( GETELEMENTTYPE(elem1) == ELEMFUNCRETURN)
-               encodeFunctionElementSATEncoder(This, (ElementFunction*) elem1);
+               elemc1 = encodeFunctionElementSATEncoder(This, (ElementFunction*) elem1);
        Element* elem2 = getArrayElement( &constraint->inputs, 1);
        if( GETELEMENTTYPE(elem2) == ELEMFUNCRETURN)
-               encodeFunctionElementSATEncoder(This, (ElementFunction*) elem2);
+               elemc2 = encodeFunctionElementSATEncoder(This, (ElementFunction*) elem2);
        for(uint i=0; i<size; i++){
                Constraint* arg1 = getElementValueConstraint(This, elem1, commonElements[i]);
                ASSERT(arg1!=NULL);
@@ -354,7 +369,13 @@ Constraint * encodeEnumOperatorPredicateSATEncoder(SATEncoder * This, BooleanPre
                carray[i] =  allocConstraint(AND, arg1, arg2);
        }
        //FIXME: the case when there is no intersection ....
-       return allocArrayConstraint(OR, size, carray);
+       Constraint* result = allocArrayConstraint(OR, size, carray);
+       ASSERT(result!= NULL);
+       if(elemc1!= NULL)
+               result = allocConstraint(AND, result, elemc1);
+       if(elemc2 != NULL)
+               result = allocConstraint (AND, result, elemc2);
+       return result;
 }
 
 Constraint* encodeFunctionElementSATEncoder(SATEncoder* encoder, ElementFunction *This){
@@ -387,74 +408,71 @@ Constraint* encodeOperatorElementFunctionSATEncoder(SATEncoder* encoder, Element
        ASSERT(GETFUNCTIONTYPE(This->function) == OPERATORFUNC);
        ASSERT(getSizeArrayElement(&This->inputs)==2 );
        ElementEncoding* elem1 = getElementEncoding( getArrayElement(&This->inputs,0) );
-       generateElementEncodingVariables(encoder, elem1);
        ElementEncoding* elem2 = getElementEncoding( getArrayElement(&This->inputs,1) );
-       generateElementEncodingVariables(encoder, elem2);
        Constraint* carray[elem1->encArraySize*elem2->encArraySize];
        uint size=0;
        Constraint* overFlowConstraint = ((BooleanVar*) This->overflowstatus)->var;
        for(uint i=0; i<elem1->encArraySize; i++){
                if(isinUseElement(elem1, i)){
-                       for(uint j=0; j<elem2->encArraySize; j++){
+                       for( uint j=0; j<elem2->encArraySize; j++){
                                if(isinUseElement(elem2, j)){
-                                       bool isInRange = false, hasOverFlow=false;
+                                       bool isInRange = false;
                                        uint64_t result= applyFunctionOperator((FunctionOperator*)This->function,elem1->encodingArray[i],
-                                               elem2->encodingArray[j], &isInRange, &hasOverFlow);
-                                       if(!isInRange)
-                                               break; // Ignoring the cases that result of operation doesn't exist in the code.
+                                               elem2->encodingArray[j], &isInRange);
                                        //FIXME: instead of getElementValueConstraint, it might be useful to have another function
                                        // that doesn't iterate over encodingArray and treats more efficient ...
-                                       Constraint* and1 = getElementValueConstraint(encoder, elem1->element, elem1->encodingArray[i]);
-                                       ASSERT(and1 != NULL);
-                                       Constraint* and2 = getElementValueConstraint(encoder, elem2->element, elem2->encodingArray[j]);
-                                       ASSERT(and2 != NULL);
-                                       Constraint* imply2 = getElementValueConstraint(encoder, (Element*) This, result);
-                                       ASSERT(imply2 != NULL);
-                                       Constraint* constraint = allocConstraint(IMPLIES, 
-                                               allocConstraint(AND, and1, and2) , imply2);
+                                       Constraint* valConstrIn1 = getElementValueConstraint(encoder, elem1->element, elem1->encodingArray[i]);
+                                       ASSERT(valConstrIn1 != NULL);
+                                       Constraint* valConstrIn2 = getElementValueConstraint(encoder, elem2->element, elem2->encodingArray[j]);
+                                       ASSERT(valConstrIn2 != NULL);
+                                       Constraint* valConstrOut = getElementValueConstraint(encoder, (Element*) This, result);
+                                       if(valConstrOut == NULL)
+                                               continue; //FIXME:Should talk to brian about it!
+                                       Constraint* OpConstraint = allocConstraint(IMPLIES, 
+                                               allocConstraint(AND, valConstrIn1, valConstrIn2) , valConstrOut);
                                        switch( ((FunctionOperator*)This->function)->overflowbehavior ){
                                                case IGNORE:
-                                                       if(!hasOverFlow){
-                                                               carray[size++] = constraint;
+                                                       if(isInRange){
+                                                               carray[size++] = OpConstraint;
                                                        }
                                                        break;
                                                case WRAPAROUND:
-                                                       carray[size++] = constraint;
+                                                       carray[size++] = OpConstraint;
                                                        break;
                                                case FLAGFORCESOVERFLOW:
-                                                       if(hasOverFlow){
-                                                               Constraint* const1 = allocConstraint(IMPLIES, overFlowConstraint, 
-                                                                               allocConstraint(AND, getElementValueConstraint(encoder, elem1->element, elem1->encodingArray[i]),
-                                                                               getElementValueConstraint(encoder, elem2->element, elem2->encodingArray[j])));
-                                                               carray[size++] = allocConstraint(AND, const1, constraint);
+                                                       if(isInRange){
+                                                               Constraint* const1 = allocConstraint(IMPLIES,
+                                                                       allocConstraint(AND, valConstrIn1, valConstrIn2), 
+                                                                       negateConstraint(overFlowConstraint));
+                                                               carray[size++] = allocConstraint(AND, const1, OpConstraint);
                                                        }
                                                        break;
                                                case OVERFLOWSETSFLAG:
-                                                       if(hasOverFlow){
-                                                               Constraint* const1 = allocConstraint(IMPLIES, allocConstraint(AND, getElementValueConstraint(encoder, elem1->element, elem1->encodingArray[i]),
-                                                                               getElementValueConstraint(encoder, elem2->element, elem2->encodingArray[j])), overFlowConstraint);
-                                                               carray[size++] = allocConstraint(AND, const1, constraint);
-                                                       } else
-                                                               carray[size++] = constraint;
+                                                       if(isInRange){
+                                                               carray[size++] = OpConstraint;
+                                                       } else{
+                                                               carray[size++] = allocConstraint(IMPLIES,
+                                                                       allocConstraint(AND, valConstrIn1, valConstrIn2),
+                                                                       overFlowConstraint);
+                                                       }
                                                        break;
                                                case FLAGIFFOVERFLOW:
-                                                       if(!hasOverFlow){
-                                                               carray[size++] = constraint;
+                                                       if(isInRange){
+                                                               Constraint* const1 = allocConstraint(IMPLIES,
+                                                                       allocConstraint(AND, valConstrIn1, valConstrIn2), 
+                                                                       negateConstraint(overFlowConstraint));
+                                                               carray[size++] = allocConstraint(AND, const1, OpConstraint);
                                                        }else{
-                                                               Constraint* const1 = allocConstraint(IMPLIES, overFlowConstraint, 
-                                                                               allocConstraint(AND, getElementValueConstraint(encoder, elem1->element, elem1->encodingArray[i]),
-                                                                               getElementValueConstraint(encoder, elem2->element, elem2->encodingArray[j])));
-                                                               Constraint* const2 = allocConstraint(IMPLIES, allocConstraint(AND, getElementValueConstraint(encoder, elem1->element, elem1->encodingArray[i]),
-                                                                               getElementValueConstraint(encoder, elem2->element, elem2->encodingArray[j])), overFlowConstraint);
-                                                               Constraint* res [] = {const1, const2, constraint};
-                                                               carray[size++] = allocArrayConstraint(AND, 3, res);
+                                                               carray[size++] = allocConstraint(IMPLIES,
+                                                                       allocConstraint(AND, valConstrIn1, valConstrIn2),
+                                                                       overFlowConstraint);
                                                        }
                                                        break;
                                                case NOOVERFLOW:
-                                                       if(hasOverFlow){
+                                                       if(!isInRange){
                                                                ASSERT(0);
                                                        }
-                                                       carray[size++] = constraint;
+                                                       carray[size++] = OpConstraint;
                                                        break;
                                                default:
                                                        ASSERT(0);

diff --git a/src/Backend/satencoder.h b/src/Backend/satencoder.h
index 03b238c64a9f035134c61cca716353e5a27c97b1..36cbc7727a95df9241e114217dfd9df01010ab6f 100644 (file)
--- a/src/Backend/satencoder.h
+++ b/src/Backend/satencoder.h
@@ -15,7 +15,7 @@ Constraint * getNewVarSATEncoder(SATEncoder *This);
 void getArrayNewVarsSATEncoder(SATEncoder* encoder, uint num, Constraint **carray);
 Constraint * encodeConstraintSATEncoder(SATEncoder *This, Boolean *constraint);
 Constraint * encodeOrderSATEncoder(SATEncoder *This, BooleanOrder * constraint);
-void createAllTotalOrderConstraintsSATEncoder(SATEncoder* This, Order* order);
+Constraint * createAllTotalOrderConstraintsSATEncoder(SATEncoder* This, Order* order);
 Constraint* getOrderConstraint(HashTableBoolConst *table, OrderPair *pair);
 Constraint * generateTransOrderConstraintSATEncoder(SATEncoder *This, Constraint *constIJ,Constraint *constJK,Constraint *constIK);
 Constraint * encodeTotalOrderSATEncoder(SATEncoder *This, BooleanOrder * constraint);

diff --git a/src/Encoders/elementencoding.h b/src/Encoders/elementencoding.h
index 15282456b0cb1c573f237ffbd9e7ad7791095a60..d51f5fa00a7693e31d17084cbe3fb58dd891baba 100644 (file)
--- a/src/Encoders/elementencoding.h
+++ b/src/Encoders/elementencoding.h
@@ -24,8 +24,6 @@ void setElementEncodingType(ElementEncoding* This, ElementEncodingType type);
 void deleteElementEncoding(ElementEncoding *This);
 void allocEncodingArrayElement(ElementEncoding *This, uint size);
 void allocInUseArrayElement(ElementEncoding *This, uint size);
-//FIXME
-//uint addNewVariableToEncodingArray(ElementEncoding* This, uint64_t var);
 static inline bool isinUseElement(ElementEncoding *This, uint offset) {
        return (This->inUseArray[(offset>>6)] >> (offset & 63)) &0x1;
 }

diff --git a/src/Test/buildconstraints.c b/src/Test/buildconstraints.c
index 440d1aa1def4b7a30e6f5d0d884b5fecac8b4b7d..81f01b3988c38deac8bbd87ed16560bfeb2c5f70 100644 (file)
--- a/src/Test/buildconstraints.c
+++ b/src/Test/buildconstraints.c
@@ -16,19 +16,26 @@ int main(int numargs, char ** argv) {
        addBoolean(solver, oc);
        
        uint64_t set2[] = {2, 3};
-       Set* range = createSet(solver, 1, set2, 2);
-       Function * f1 = createFunctionOperator(solver, ADD, domain, 2, range, IGNORE);
-       /*Table* table = createTable(solver, domain, 2, range);
+       Set* rangef1 = createSet(solver, 1, set2, 2);
+       Function * f1 = createFunctionOperator(solver, ADD, domain, 2, rangef1, IGNORE);
+       
+       Table* table = createTable(solver, domain, 2, s);
        uint64_t row1[] = {0, 1};
        uint64_t row2[] = {1, 1};
-       addTableEntry(solver, table, row1, 2, 2);
-       addTableEntry(solver, table, row2, 2, 3);
-       Function * f2 = completeTable(solver, table); */
+       uint64_t row3[] = {2, 1};
+       uint64_t row4[] = {1, 2};
+       addTableEntry(solver, table, row1, 2, 0);
+       addTableEntry(solver, table, row2, 2, 1);
+       addTableEntry(solver, table, row3, 2, 2);
+       addTableEntry(solver, table, row4, 2, 2);
+       Function * f2 = completeTable(solver, table); //its range would be as same as s
+       
        Boolean* overflow = getBooleanVar(solver , 2);
        Element * e3 = applyFunction(solver, f1, inputs, 2, overflow);
-       Set* domain2[] = {s,range};
+       Element * e4 = applyFunction(solver, f2, inputs, 2, overflow);
+       Set* domain2[] = {s,rangef1};
        Predicate* equal2 = createPredicateOperator(solver, EQUALS, domain2, 2);
-       Element* inputs2 [] = {e1, e3};
+       Element* inputs2 [] = {e4, e3};
        Boolean* pred = applyPredicate(solver, equal2, inputs2, 2);
        addBoolean(solver, pred);
        startEncoding(solver);