1 #include "satencoder.h"
5 #include "constraint.h"
9 #include "tableentry.h"
12 #include "predicate.h"
13 #include "orderpair.h"
16 SATEncoder * allocSATEncoder() {
17 SATEncoder *This=ourmalloc(sizeof (SATEncoder));
19 This->cnf=createCNF();
23 void deleteSATEncoder(SATEncoder *This) {
28 Edge getElementValueConstraint(SATEncoder* This, Element* elem, uint64_t value) {
29 generateElementEncodingVariables(This, getElementEncoding(elem));
30 switch(getElementEncoding(elem)->type){
39 return getElementValueBinaryIndexConstraint(This, elem, value);
54 Edge getElementValueBinaryIndexConstraint(SATEncoder * This, Element* elem, uint64_t value) {
55 ASTNodeType type = GETELEMENTTYPE(elem);
56 ASSERT(type == ELEMSET || type == ELEMFUNCRETURN);
57 ElementEncoding* elemEnc = getElementEncoding(elem);
58 for(uint i=0; i<elemEnc->encArraySize; i++){
59 if( isinUseElement(elemEnc, i) && elemEnc->encodingArray[i]==value){
60 return generateBinaryConstraint(This->cnf, elemEnc->numVars, elemEnc->variables, i);
66 void encodeAllSATEncoder(CSolver *csolver, SATEncoder * This) {
67 VectorBoolean *constraints=csolver->constraints;
68 uint size=getSizeVectorBoolean(constraints);
69 for(uint i=0;i<size;i++) {
70 Boolean *constraint=getVectorBoolean(constraints, i);
71 Edge c= encodeConstraintSATEncoder(This, constraint);
74 addConstraint(This->cnf, c);
78 Edge encodeConstraintSATEncoder(SATEncoder *This, Boolean *constraint) {
79 switch(GETBOOLEANTYPE(constraint)) {
81 return encodeOrderSATEncoder(This, (BooleanOrder *) constraint);
83 return encodeVarSATEncoder(This, (BooleanVar *) constraint);
85 return encodeLogicSATEncoder(This, (BooleanLogic *) constraint);
87 return encodePredicateSATEncoder(This, (BooleanPredicate *) constraint);
89 model_print("Unhandled case in encodeConstraintSATEncoder %u", GETBOOLEANTYPE(constraint));
94 void getArrayNewVarsSATEncoder(SATEncoder* encoder, uint num, Edge * carray) {
95 for(uint i=0;i<num;i++)
96 carray[i]=getNewVarSATEncoder(encoder);
99 Edge getNewVarSATEncoder(SATEncoder *This) {
100 return constraintNewVar(This->cnf);
103 Edge encodeVarSATEncoder(SATEncoder *This, BooleanVar * constraint) {
104 if (edgeIsNull(constraint->var)) {
105 constraint->var=getNewVarSATEncoder(This);
107 return constraint->var;
110 Edge encodeLogicSATEncoder(SATEncoder *This, BooleanLogic * constraint) {
111 Edge array[getSizeArrayBoolean(&constraint->inputs)];
112 for(uint i=0;i<getSizeArrayBoolean(&constraint->inputs);i++)
113 array[i]=encodeConstraintSATEncoder(This, getArrayBoolean(&constraint->inputs, i));
115 switch(constraint->op) {
117 return constraintAND(This->cnf, getSizeArrayBoolean(&constraint->inputs), array);
119 return constraintOR(This->cnf, getSizeArrayBoolean(&constraint->inputs), array);
121 ASSERT( getSizeArrayBoolean(&constraint->inputs)==1);
122 return constraintNegate(array[0]);
124 ASSERT( getSizeArrayBoolean(&constraint->inputs)==2);
125 return constraintXOR(This->cnf, array[0], array[1]);
127 ASSERT( getSizeArrayBoolean( &constraint->inputs)==2);
128 return constraintIMPLIES(This->cnf, array[0], array[1]);
130 model_print("Unhandled case in encodeLogicSATEncoder %u", constraint->op);
136 Edge encodeOrderSATEncoder(SATEncoder *This, BooleanOrder * constraint) {
137 switch( constraint->order->type){
139 return encodePartialOrderSATEncoder(This, constraint);
141 return encodeTotalOrderSATEncoder(This, constraint);
148 Edge getPairConstraint(SATEncoder *This, HashTableBoolConst * table, OrderPair * pair) {
151 if (pair->first > pair->second) {
153 flipped.first=pair->second;
154 flipped.second=pair->first;
155 pair = &flipped; //FIXME: accessing a local variable from outside of the function?
158 if (!containsBoolConst(table, pair)) {
159 constraint = getNewVarSATEncoder(This);
160 OrderPair * paircopy = allocOrderPair(pair->first, pair->second, constraint);
161 putBoolConst(table, paircopy, paircopy);
163 constraint = getBoolConst(table, pair)->constraint;
165 return constraintNegate(constraint);
171 Edge encodeTotalOrderSATEncoder(SATEncoder *This, BooleanOrder * boolOrder){
172 ASSERT(boolOrder->order->type == TOTAL);
173 if(boolOrder->order->boolsToConstraints == NULL){
174 initializeOrderHashTable(boolOrder->order);
175 createAllTotalOrderConstraintsSATEncoder(This, boolOrder->order);
177 HashTableBoolConst* boolToConsts = boolOrder->order->boolsToConstraints;
178 OrderPair pair={boolOrder->first, boolOrder->second, E_NULL};
179 Edge constraint = getPairConstraint(This, boolToConsts, & pair);
183 void createAllTotalOrderConstraintsSATEncoder(SATEncoder* This, Order* order){
184 ASSERT(order->type == TOTAL);
185 VectorInt* mems = order->set->members;
186 HashTableBoolConst* table = order->boolsToConstraints;
187 uint size = getSizeVectorInt(mems);
189 for(uint i=0; i<size; i++){
190 uint64_t valueI = getVectorInt(mems, i);
191 for(uint j=i+1; j<size;j++){
192 uint64_t valueJ = getVectorInt(mems, j);
193 OrderPair pairIJ = {valueI, valueJ};
194 Edge constIJ=getPairConstraint(This, table, & pairIJ);
195 for(uint k=j+1; k<size; k++){
196 uint64_t valueK = getVectorInt(mems, k);
197 OrderPair pairJK = {valueJ, valueK};
198 OrderPair pairIK = {valueI, valueK};
199 Edge constIK = getPairConstraint(This, table, & pairIK);
200 Edge constJK = getPairConstraint(This, table, & pairJK);
201 addConstraint(This->cnf, generateTransOrderConstraintSATEncoder(This, constIJ, constJK, constIK));
207 Edge getOrderConstraint(HashTableBoolConst *table, OrderPair *pair){
208 ASSERT(pair->first!= pair->second);
209 Edge constraint = getBoolConst(table, pair)->constraint;
210 if(pair->first > pair->second)
213 return constraintNegate(constraint);
216 Edge generateTransOrderConstraintSATEncoder(SATEncoder *This, Edge constIJ,Edge constJK,Edge constIK){
217 Edge carray[] = {constIJ, constJK, constraintNegate(constIK)};
218 Edge loop1= constraintOR(This->cnf, 3, carray);
219 Edge carray2[] = {constraintNegate(constIJ), constraintNegate(constJK), constIK};
220 Edge loop2= constraintOR(This->cnf, 3, carray2 );
221 return constraintAND2(This->cnf, loop1, loop2);
224 Edge encodePartialOrderSATEncoder(SATEncoder *This, BooleanOrder * constraint){
225 // FIXME: we can have this implementation for partial order. Basically,
226 // we compute the transitivity between two order constraints specified by the client! (also can be used
227 // when client specify sparse constraints for the total order!)
228 ASSERT(constraint->order->type == PARTIAL);
230 HashTableBoolConst* boolToConsts = boolOrder->order->boolsToConstraints;
231 if( containsBoolConst(boolToConsts, boolOrder) ){
232 return getBoolConst(boolToConsts, boolOrder);
234 Edge constraint = getNewVarSATEncoder(This);
235 putBoolConst(boolToConsts,boolOrder, constraint);
236 VectorBoolean* orderConstrs = &boolOrder->order->constraints;
237 uint size= getSizeVectorBoolean(orderConstrs);
238 for(uint i=0; i<size; i++){
239 ASSERT(GETBOOLEANTYPE( getVectorBoolean(orderConstrs, i)) == ORDERCONST );
240 BooleanOrder* tmp = (BooleanOrder*)getVectorBoolean(orderConstrs, i);
241 BooleanOrder* newBool;
243 if(tmp->second==boolOrder->first){
244 newBool = (BooleanOrder*)allocBooleanOrder(tmp->order,tmp->first,boolOrder->second);
245 first = encodeTotalOrderSATEncoder(This, tmp);
248 }else if (boolOrder->second == tmp->first){
249 newBool = (BooleanOrder*)allocBooleanOrder(tmp->order,boolOrder->first,tmp->second);
251 second = encodeTotalOrderSATEncoder(This, tmp);
254 Edge transConstr= encodeTotalOrderSATEncoder(This, newBool);
255 generateTransOrderConstraintSATEncoder(This, first, second, transConstr );
263 Edge encodePredicateSATEncoder(SATEncoder * This, BooleanPredicate * constraint) {
264 switch(GETPREDICATETYPE(constraint->predicate) ){
266 return encodeTablePredicateSATEncoder(This, constraint);
268 return encodeOperatorPredicateSATEncoder(This, constraint);
275 Edge encodeTablePredicateSATEncoder(SATEncoder * This, BooleanPredicate * constraint){
276 switch(constraint->encoding.type){
277 case ENUMERATEIMPLICATIONS:
278 case ENUMERATEIMPLICATIONSNEGATE:
279 return encodeEnumTablePredicateSATEncoder(This, constraint);
289 Edge encodeEnumTablePredicateSATEncoder(SATEncoder * This, BooleanPredicate * constraint){
290 VectorTableEntry* entries = &(((PredicateTable*)constraint->predicate)->table->entries);
291 FunctionEncodingType encType = constraint->encoding.type;
292 uint size = getSizeVectorTableEntry(entries);
293 bool generateNegation = encType == ENUMERATEIMPLICATIONSNEGATE;
295 Edge constraints[size];
296 for(uint i=0; i<size; i++){
297 TableEntry* entry = getVectorTableEntry(entries, i);
299 if(generateNegation == entry->output) {
300 //Skip the irrelevant entries
304 ArrayElement* inputs = &constraint->inputs;
305 uint inputNum =getSizeArrayElement(inputs);
306 Edge carray[inputNum];
307 for(uint j=0; j<inputNum; j++){
308 Element* el = getArrayElement(inputs, j);
309 Edge tmpc = getElementValueConstraint(This, el, entry->inputs[j]);
310 if( GETELEMENTTYPE(el) == ELEMFUNCRETURN){
311 // HAMED : THIS IS COMPLETELY BROKEN....
312 Edge func =encodeFunctionElementSATEncoder(This, (ElementFunction*) el);
313 carray[j] = constraintAND2(This->cnf, func, tmpc);
318 constraints[i]=constraintAND(This->cnf, inputNum, carray);
320 Edge result=constraintOR(This->cnf, size, constraints);
322 return generationNegation ? result: constraintNegate(result);
325 Edge encodeOperatorPredicateSATEncoder(SATEncoder * This, BooleanPredicate * constraint){
326 switch(constraint->encoding.type){
327 case ENUMERATEIMPLICATIONS:
328 return encodeEnumOperatorPredicateSATEncoder(This, constraint);
338 Edge encodeEnumOperatorPredicateSATEncoder(SATEncoder * This, BooleanPredicate * constraint){
339 ASSERT(GETPREDICATETYPE(constraint->predicate)==OPERATORPRED);
340 PredicateOperator* predicate = (PredicateOperator*)constraint->predicate;
341 ASSERT(predicate->op == EQUALS); //For now, we just only support equals
342 //getting maximum size of in common elements between two sets!
343 uint size=getSizeVectorInt( getArraySet( &predicate->domains, 0)->members);
344 uint64_t commonElements [size];
345 getEqualitySetIntersection(predicate, &size, commonElements);
347 Element* elem1 = getArrayElement( &constraint->inputs, 0);
348 Edge elemc1 = E_NULL, elemc2 = E_NULL;
349 if( GETELEMENTTYPE(elem1) == ELEMFUNCRETURN) //HAMED: THIS IS PRETTY BROKEN...
350 elemc1 = encodeFunctionElementSATEncoder(This, (ElementFunction*) elem1);
351 Element* elem2 = getArrayElement( &constraint->inputs, 1);
352 if( GETELEMENTTYPE(elem2) == ELEMFUNCRETURN) //HAMED: THIS IS PRETTY BROKEN
353 elemc2 = encodeFunctionElementSATEncoder(This, (ElementFunction*) elem2);
354 for(uint i=0; i<size; i++){
355 Edge arg1 = getElementValueConstraint(This, elem1, commonElements[i]);
356 Edge arg2 = getElementValueConstraint(This, elem2, commonElements[i]);
357 carray[i] = constraintAND2(This->cnf, arg1, arg2);
359 //FIXME: the case when there is no intersection ....
360 Edge result = constraintOR(This->cnf, size, carray);
361 if (!edgeIsNull(elemc1))
362 result = constraintAND2(This->cnf, result, elemc1);
363 if (!edgeIsNull(elemc2))
364 result = constraintAND2(This->cnf, result, elemc2);
368 Edge encodeFunctionElementSATEncoder(SATEncoder* encoder, ElementFunction *This){
369 switch(GETFUNCTIONTYPE(This->function)){
371 return encodeTableElementFunctionSATEncoder(encoder, This);
373 return encodeOperatorElementFunctionSATEncoder(encoder, This);
380 Edge encodeTableElementFunctionSATEncoder(SATEncoder* encoder, ElementFunction* This){
381 switch(getElementFunctionEncoding(This)->type){
382 case ENUMERATEIMPLICATIONS:
383 return encodeEnumTableElemFunctionSATEncoder(encoder, This);
394 Edge encodeOperatorElementFunctionSATEncoder(SATEncoder* encoder, ElementFunction* This){
395 ASSERT(GETFUNCTIONTYPE(This->function) == OPERATORFUNC);
396 ASSERT(getSizeArrayElement(&This->inputs)==2 );
397 ElementEncoding* elem1 = getElementEncoding( getArrayElement(&This->inputs,0) );
398 ElementEncoding* elem2 = getElementEncoding( getArrayElement(&This->inputs,1) );
399 Edge carray[elem1->encArraySize*elem2->encArraySize];
401 Edge overFlowConstraint = ((BooleanVar*) This->overflowstatus)->var;
402 for(uint i=0; i<elem1->encArraySize; i++){
403 if(isinUseElement(elem1, i)){
404 for( uint j=0; j<elem2->encArraySize; j++){
405 if(isinUseElement(elem2, j)){
406 bool isInRange = false;
407 uint64_t result= applyFunctionOperator((FunctionOperator*)This->function,elem1->encodingArray[i],
408 elem2->encodingArray[j], &isInRange);
409 //FIXME: instead of getElementValueConstraint, it might be useful to have another function
410 // that doesn't iterate over encodingArray and treats more efficient ...
411 Edge valConstrIn1 = getElementValueConstraint(encoder, elem1->element, elem1->encodingArray[i]);
412 Edge valConstrIn2 = getElementValueConstraint(encoder, elem2->element, elem2->encodingArray[j]);
413 Edge valConstrOut = getElementValueConstraint(encoder, (Element*) This, result);
414 if(edgeIsNull(valConstrOut))
415 continue; //FIXME:Should talk to brian about it!
416 Edge OpConstraint = constraintIMPLIES(encoder->cnf, constraintAND2(encoder->cnf, valConstrIn1, valConstrIn2), valConstrOut);
417 switch( ((FunctionOperator*)This->function)->overflowbehavior ){
420 carray[size++] = OpConstraint;
424 carray[size++] = OpConstraint;
426 case FLAGFORCESOVERFLOW:
428 Edge const1 = constraintIMPLIES(encoder->cnf, constraintAND2(encoder->cnf, valConstrIn1, valConstrIn2), constraintNegate(overFlowConstraint));
429 carray[size++] = constraintAND2(encoder->cnf, const1, OpConstraint);
432 case OVERFLOWSETSFLAG:
434 carray[size++] = OpConstraint;
436 carray[size++] = constraintIMPLIES(encoder->cnf, constraintAND2(encoder->cnf, valConstrIn1, valConstrIn2), overFlowConstraint);
439 case FLAGIFFOVERFLOW:
441 Edge const1 = constraintIMPLIES(encoder->cnf, constraintAND2(encoder->cnf, valConstrIn1, valConstrIn2), constraintNegate(overFlowConstraint));
442 carray[size++] = constraintAND2(encoder->cnf, const1, OpConstraint);
444 carray[size++] = constraintIMPLIES(encoder->cnf, constraintAND2(encoder->cnf, valConstrIn1, valConstrIn2), overFlowConstraint);
451 carray[size++] = OpConstraint;
461 return constraintAND(encoder->cnf, size, carray);
464 Edge encodeEnumTableElemFunctionSATEncoder(SATEncoder* encoder, ElementFunction* This){
465 ASSERT(GETFUNCTIONTYPE(This->function)==TABLEFUNC);
466 ArrayElement* elements= &This->inputs;
467 Table* table = ((FunctionTable*) (This->function))->table;
468 uint size = getSizeVectorTableEntry(&table->entries);
469 Edge constraints[size]; //FIXME: should add a space for the case that didn't match any entries
470 for(uint i=0; i<size; i++) {
471 TableEntry* entry = getVectorTableEntry(&table->entries, i);
472 uint inputNum = getSizeArrayElement(elements);
473 Edge carray[inputNum];
474 for(uint j=0; j<inputNum; j++){
475 Element* el= getArrayElement(elements, j);
476 carray[j] = getElementValueConstraint(encoder, el, entry->inputs[j]);
478 Edge output = getElementValueConstraint(encoder, (Element*)This, entry->output);
479 Edge row= constraintIMPLIES(encoder->cnf, constraintAND(encoder->cnf, inputNum, carray), output);
482 Edge result = constraintOR(encoder->cnf, size, constraints);