From: Hamed Date: Fri, 7 Jul 2017 17:43:32 +0000 (-0700) Subject: Fixing more bugs regarding generating constraint variables ... X-Git-Url: http://demsky.eecs.uci.edu/git/?a=commitdiff_plain;h=819528702f5a91b111a8e03a11f45458d3ed5a77;p=satune.git Fixing more bugs regarding generating constraint variables ... --- diff --git a/src/Backend/satencoder.c b/src/Backend/satencoder.c index eb33955..8607b65 100644 --- a/src/Backend/satencoder.c +++ b/src/Backend/satencoder.c @@ -23,7 +23,8 @@ void deleteSATEncoder(SATEncoder *This) { ourfree(This); } -Constraint * getElementValueConstraint(Element* This, uint64_t value) { +Constraint * getElementValueConstraint(SATEncoder* encoder,Element* This, uint64_t value) { + generateElementEncodingVariables(encoder, getElementEncoding(This)); switch(getElementEncoding(This)->type){ case ONEHOT: ASSERT(0); @@ -32,10 +33,10 @@ Constraint * getElementValueConstraint(Element* This, uint64_t value) { ASSERT(0); break; case BINARYINDEX: - ASSERT(0); + return getElementValueBinaryIndexConstraint(This, value); break; case ONEHOTBINARY: - return getElementValueBinaryIndexConstraint(This, value); + ASSERT(0); break; case BINARYVAL: ASSERT(0); @@ -66,6 +67,7 @@ void encodeAllSATEncoder(CSolver *csolver, SATEncoder * This) { Boolean *constraint=getVectorBoolean(constraints, i); Constraint* c= encodeConstraintSATEncoder(This, constraint); printConstraint(c); + model_print("\n"); } } @@ -306,7 +308,7 @@ Constraint * encodeEnumTablePredicateSATEncoder(SATEncoder * This, BooleanPredic Element* el = getArrayElement(inputs, j); if( GETELEMENTTYPE(el) == ELEMFUNCRETURN) encodeFunctionElementSATEncoder(This, (ElementFunction*) el); - carray[j] = getElementValueConstraint(el, entry->inputs[j]); + carray[j] = getElementValueConstraint(This,el, entry->inputs[j]); ASSERT(carray[j]!= NULL); } constraints[i]=allocArrayConstraint(AND, inputNum, carray); @@ -330,7 +332,7 @@ Constraint * encodeOperatorPredicateSATEncoder(SATEncoder * This, BooleanPredica } Constraint * encodeEnumOperatorPredicateSATEncoder(SATEncoder * This, BooleanPredicate * constraint){ - ASSERT(GETPREDICATETYPE(constraint)==OPERATORPRED); + ASSERT(GETPREDICATETYPE(constraint->predicate)==OPERATORPRED); PredicateOperator* predicate = (PredicateOperator*)constraint->predicate; ASSERT(predicate->op == EQUALS); //For now, we just only support equals //getting maximum size of in common elements between two sets! @@ -345,9 +347,9 @@ Constraint * encodeEnumOperatorPredicateSATEncoder(SATEncoder * This, BooleanPre if( GETELEMENTTYPE(elem2) == ELEMFUNCRETURN) 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; @@ -400,11 +404,11 @@ Constraint* encodeOperatorElementFunctionSATEncoder(SATEncoder* encoder, Element 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* and1 = getElementValueConstraint(elem1->element, elem1->encodingArray[i]); + Constraint* and1 = getElementValueConstraint(encoder, elem1->element, elem1->encodingArray[i]); ASSERT(and1 != NULL); - Constraint* and2 = getElementValueConstraint(elem2->element, elem2->encodingArray[j]); + Constraint* and2 = getElementValueConstraint(encoder, elem2->element, elem2->encodingArray[j]); ASSERT(and2 != NULL); - Constraint* imply2 = getElementValueConstraint((Element*) This, result); + Constraint* imply2 = getElementValueConstraint(encoder, (Element*) This, result); ASSERT(imply2 != NULL); Constraint* constraint = allocConstraint(IMPLIES, allocConstraint(AND, and1, and2) , imply2); @@ -413,38 +417,45 @@ Constraint* encodeOperatorElementFunctionSATEncoder(SATEncoder* encoder, Element if(!hasOverFlow){ carray[size++] = constraint; } + break; case WRAPAROUND: carray[size++] = constraint; + break; case FLAGFORCESOVERFLOW: if(hasOverFlow){ Constraint* const1 = allocConstraint(IMPLIES, overFlowConstraint, - allocConstraint(AND, getElementValueConstraint(elem1->element, elem1->encodingArray[i]), - getElementValueConstraint(elem2->element, elem2->encodingArray[j]))); + allocConstraint(AND, getElementValueConstraint(encoder, elem1->element, elem1->encodingArray[i]), + getElementValueConstraint(encoder, elem2->element, elem2->encodingArray[j]))); carray[size++] = allocConstraint(AND, const1, constraint); } + break; case OVERFLOWSETSFLAG: if(hasOverFlow){ - Constraint* const1 = allocConstraint(IMPLIES, allocConstraint(AND, getElementValueConstraint(elem1->element, elem1->encodingArray[i]), - getElementValueConstraint(elem2->element, elem2->encodingArray[j])), overFlowConstraint); + 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; + break; 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); + 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); } + break; case NOOVERFLOW: - if(hasOverFlow) + if(hasOverFlow){ ASSERT(0); - carray[size++] = constraint; + } + carray[size++] = constraint; + break; default: ASSERT(0); } @@ -468,10 +479,10 @@ Constraint* encodeEnumTableElemFunctionSATEncoder(SATEncoder* encoder, ElementFu Constraint* carray[inputNum]; for(uint j=0; jinputs[j]); + carray[j] = getElementValueConstraint(encoder, el, entry->inputs[j]); ASSERT(carray[j]!= NULL); } - Constraint* output = getElementValueConstraint((Element*)This, entry->output); + Constraint* output = getElementValueConstraint(encoder, (Element*)This, entry->output); ASSERT(output!= NULL); Constraint* row= allocConstraint(IMPLIES, allocArrayConstraint(AND, inputNum, carray), output); constraints[i]=row; diff --git a/src/Backend/satencoder.h b/src/Backend/satencoder.h index 2976314..03b238c 100644 --- a/src/Backend/satencoder.h +++ b/src/Backend/satencoder.h @@ -29,7 +29,7 @@ Constraint * encodeOperatorPredicateSATEncoder(SATEncoder * This, BooleanPredica Constraint * encodeEnumOperatorPredicateSATEncoder(SATEncoder * This, BooleanPredicate * constraint); Constraint * getElementValueBinaryIndexConstraint(Element* This, uint64_t value); -Constraint * getElementValueConstraint(Element* This, uint64_t value); +Constraint * getElementValueConstraint(SATEncoder* encoder, Element* This, uint64_t value); Constraint* encodeFunctionElementSATEncoder(SATEncoder* encoder, ElementFunction *This); Constraint* encodeEnumTableElemFunctionSATEncoder(SATEncoder* encoder, ElementFunction* This); diff --git a/src/Encoders/elementencoding.c b/src/Encoders/elementencoding.c index 08eb2e8..6ed38c2 100644 --- a/src/Encoders/elementencoding.c +++ b/src/Encoders/elementencoding.c @@ -49,7 +49,8 @@ void generateBinaryIndexEncodingVars(SATEncoder* encoder, ElementEncoding* This) void generateElementEncodingVariables(SATEncoder* encoder, ElementEncoding* This){ ASSERT(This->type!=ELEM_UNASSIGNED); - ASSERT(This->variables==NULL); + if(This->variables!=NULL) + return; switch(This->type){ case BINARYINDEX: generateBinaryIndexEncodingVars(encoder, This);