From 85a1c6a1e244ce63a74d53e7c9055a6c7abdc6b8 Mon Sep 17 00:00:00 2001 From: Hamed Date: Fri, 7 Jul 2017 17:40:54 -0700 Subject: [PATCH] Fixing more bugs --- src/AST/function.c | 6 +- src/AST/function.h | 2 +- src/AST/order.c | 6 +- src/AST/order.h | 1 + src/Backend/satencoder.c | 118 +++++++++++++++++++-------------- src/Backend/satencoder.h | 2 +- src/Encoders/elementencoding.h | 2 - src/Test/buildconstraints.c | 23 ++++--- 8 files changed, 92 insertions(+), 68 deletions(-) diff --git a/src/AST/function.c b/src/AST/function.c index 65aea05..61e413b 100644 --- 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 5180ba1..158a55c 100644 --- 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 19b1c6e..2f3de74 100644 --- 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 933d831..67f0d99 100644 --- 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 8607b65..e78cb3f 100644 --- 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; iinputs[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; ifunction) == 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; iencArraySize; i++){ if(isinUseElement(elem1, i)){ - for(uint j=0; jencArraySize; j++){ + for( uint j=0; jencArraySize; 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 03b238c..36cbc77 100644 --- 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 1528245..d51f5fa 100644 --- 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 440d1aa..81f01b3 100644 --- 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); -- 2.34.1