Adding function operator handler+ omitting some redundant codes

diff --git a/src/AST/function.c b/src/AST/function.c
index 43adc256e699690af4c0088800ba89a86a741cc9..65aea05acf939ab12eb5bd5f61ede77ee6507f5f 100644 (file)
--- a/src/AST/function.c
+++ b/src/AST/function.c
@@ -20,6 +20,26 @@ Function* allocFunctionTable (Table* table){
        return &This->base;
 }
 
+uint64_t applyFunctionOperator(FunctionOperator* func, uint64_t var1, uint64_t var2, bool* isInRange, bool* hasOverFlow){
+       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);
+       }
+       *isInRange = existsInSet(func->range, result);
+       return result;
+}
+
 void deleteFunction(Function* This){
        switch(GETFUNCTIONTYPE(This)){
        case TABLEFUNC:

diff --git a/src/AST/function.h b/src/AST/function.h
index 2e043203ec6ab9a6b93ce972731483cb8700fca0..5180ba1ed7b1570c1c68917085fa689f07c169cd 100644 (file)
--- a/src/AST/function.h
+++ b/src/AST/function.h
@@ -26,6 +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);
 void deleteFunction(Function* This);
 
 #endif

diff --git a/src/AST/set.c b/src/AST/set.c
index afe26ec7a5477e0fbfac0a10b11ffbfe3b7896a2..f72bbc33fbce11e11d9b1f317bc3c001e794614f 100644 (file)
--- a/src/AST/set.c
+++ b/src/AST/set.c
@@ -21,6 +21,19 @@ Set * allocSetRange(VarType t, uint64_t lowrange, uint64_t highrange) {
        return tmp;
 }
 
+bool existsInSet(Set* set, uint64_t element){
+       if(set->isRange){
+               return element >= set->low && element <= set->high;
+       }else {
+               uint size = getSizeVectorInt(set->members);
+               for(uint i=0; i< size; i++){
+                       if(element == getVectorInt(set->members, i))
+                               return true;
+               }
+               return false;
+       }
+}
+
 uint getSetSize(Set* set){
        if(set->isRange){
                return set->high- set->low+1;

diff --git a/src/AST/set.h b/src/AST/set.h
index 55fb57cb9900b6d7f5b93f38f8fe921c2b34ffe5..badb28c4b6a165ce2e048fd7b4618ad41a3a4e5c 100644 (file)
--- a/src/AST/set.h
+++ b/src/AST/set.h
@@ -23,6 +23,7 @@ struct Set {
 
 Set *allocSet(VarType t, uint64_t * elements, uint num);
 Set * allocSetRange(VarType t, uint64_t lowrange, uint64_t highrange);
+bool existsInSet(Set* set, uint64_t element);
 uint getSetSize(Set* set);
 void deleteSet(Set *set);
 #endif/* SET_H */

diff --git a/src/Backend/satencoder.c b/src/Backend/satencoder.c
index 5a90b6c8e5d7e19200fdae0dcd6dc1bc184fe60e..d6c24e9c08f1c120376d433d63947093f2b992ff 100644 (file)
--- a/src/Backend/satencoder.c
+++ b/src/Backend/satencoder.c
@@ -23,22 +23,6 @@ void deleteSATEncoder(SATEncoder *This) {
        ourfree(This);
 }
 
-void initializeConstraintVars(CSolver* csolver, SATEncoder* This){
-       /** We really should not walk the free list to generate constraint
-                       variables...walk the constraint tree instead.  Or even better
-                       yet, just do this as you need to during the encodeAllSATEncoder
-                       walk.  */
-
-//     FIXME!!!!(); // Make sure Hamed sees comment above
-
-       uint size = getSizeVectorElement(csolver->allElements);
-       for(uint i=0; i<size; i++){
-               Element* element = getVectorElement(csolver->allElements, i);
-               generateElementEncodingVariables(This,getElementEncoding(element));
-       }
-}
-
-
 Constraint * getElementValueConstraint(Element* This, uint64_t value) {
        switch(getElementEncoding(This)->type){
                case ONEHOT:
@@ -391,8 +375,74 @@ Constraint* encodeTableElementFunctionSATEncoder(SATEncoder* encoder, ElementFun
 }
 
 Constraint* encodeOperatorElementFunctionSATEncoder(SATEncoder* encoder, ElementFunction* This){
-       //FIXME: for now it just adds/substracts inputs exhustively
-       return NULL;
+       ASSERT(GETFUNCTIONTYPE(This->function) == OPERATORFUNC);
+       ASSERT(getSizeArrayElement(&This->inputs)=2 );
+       ElementEncoding* elem1 = getElementEncoding( getArrayElement(&This->inputs,0) );
+       ElementEncoding* elem2 = getElementEncoding( getArrayElement(&This->inputs,1) );
+       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++){
+                               if(isinUseElement(elem2, j)){
+                                       bool isInRange = false, hasOverFlow=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.
+                                       //FIXME: instead of getElementValueConstraint, it might be useful to have another function
+                                       // that doesn't iterate over encodingArray and treats more efficient ...
+                                       Constraint* constraint = allocConstraint(IMPLIES, 
+                                               allocConstraint(AND, getElementValueConstraint(elem1->element, elem1->encodingArray[i]),
+                                                       getElementValueConstraint(elem2->element, elem2->encodingArray[j])) ,
+                                               getElementValueConstraint((Element*) This, result) );
+                                       switch( ((FunctionOperator*)This->function)->overflowbehavior ){
+                                               case IGNORE:
+                                                       if(!hasOverFlow){
+                                                               carray[size++] = constraint;
+                                                       }
+                                               case WRAPAROUND:
+                                                       carray[size++] = constraint;
+                                               case FLAGFORCESOVERFLOW:
+                                                       if(hasOverFlow){
+                                                               Constraint* const1 = allocConstraint(IMPLIES, overFlowConstraint, 
+                                                                               allocConstraint(AND, getElementValueConstraint(elem1->element, elem1->encodingArray[i]),
+                                                                               getElementValueConstraint(elem2->element, elem2->encodingArray[j])));
+                                                               carray[size++] = allocConstraint(AND, const1, constraint);
+                                                       }
+                                               case OVERFLOWSETSFLAG:
+                                                       if(hasOverFlow){
+                                                               Constraint* const1 = allocConstraint(IMPLIES, allocConstraint(AND, getElementValueConstraint(elem1->element, elem1->encodingArray[i]),
+                                                                               getElementValueConstraint(elem2->element, elem2->encodingArray[j])), overFlowConstraint);
+                                                               carray[size++] = allocConstraint(AND, const1, constraint);
+                                                       } else
+                                                               carray[size++] = constraint;
+                                               case FLAGIFFOVERFLOW:
+                                                       if(!hasOverFlow){
+                                                               carray[size++] = constraint;
+                                                       }else{
+                                                               Constraint* const1 = allocConstraint(IMPLIES, overFlowConstraint, 
+                                                                               allocConstraint(AND, getElementValueConstraint(elem1->element, elem1->encodingArray[i]),
+                                                                               getElementValueConstraint(elem2->element, elem2->encodingArray[j])));
+                                                               Constraint* const2 = allocConstraint(IMPLIES, allocConstraint(AND, getElementValueConstraint(elem1->element, elem1->encodingArray[i]),
+                                                                               getElementValueConstraint(elem2->element, elem2->encodingArray[j])), overFlowConstraint);
+                                                               Constraint* res [] = {const1, const2, constraint};
+                                                               carray[size++] = allocArrayConstraint(AND, 3, res);
+                                                       }
+                                               case NOOVERFLOW:
+                                                       if(hasOverFlow)
+                                                               ASSERT(0);
+                                                               carray[size++] = constraint;
+                                               default:
+                                                       ASSERT(0);
+                                       }
+                                       
+                               }
+                       }
+               }
+       }
+       return allocArrayConstraint(AND, size, carray);
 }
 
 Constraint* encodeEnumTableElemFunctionSATEncoder(SATEncoder* encoder, ElementFunction* This){

diff --git a/src/Backend/satencoder.h b/src/Backend/satencoder.h
index 6963feefcfe83da08bd6e75c08e475887d3c15bd..2976314799bc7cce10d0c6129a131b2822942797 100644 (file)
--- a/src/Backend/satencoder.h
+++ b/src/Backend/satencoder.h
@@ -10,7 +10,6 @@ struct SATEncoder {
 
 SATEncoder * allocSATEncoder();
 void deleteSATEncoder(SATEncoder *This);
-void initializeConstraintVars(CSolver* csolver, SATEncoder* This);
 void encodeAllSATEncoder(CSolver *csolver, SATEncoder *This);
 Constraint * getNewVarSATEncoder(SATEncoder *This);
 void getArrayNewVarsSATEncoder(SATEncoder* encoder, uint num, Constraint **carray);