From ccbff8107785c22e85395de2ed0478ebc57c1921 Mon Sep 17 00:00:00 2001 From: Hamed Date: Wed, 5 Jul 2017 18:37:07 -0700 Subject: [PATCH] Adding function operator handler+ omitting some redundant codes --- src/AST/function.c | 20 ++++++++++ src/AST/function.h | 1 + src/AST/set.c | 13 ++++++ src/AST/set.h | 1 + src/Backend/satencoder.c | 86 +++++++++++++++++++++++++++++++--------- src/Backend/satencoder.h | 1 - 6 files changed, 103 insertions(+), 19 deletions(-) diff --git a/src/AST/function.c b/src/AST/function.c index 43adc25..65aea05 100644 --- 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 2e04320..5180ba1 100644 --- 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 afe26ec..f72bbc3 100644 --- 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 55fb57c..badb28c 100644 --- 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 5a90b6c..d6c24e9 100644 --- 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; iallElements, 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; iencArraySize; i++){ + if(isinUseElement(elem1, i)){ + for(uint j=0; jencArraySize; 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 6963fee..2976314 100644 --- 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); -- 2.34.1