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 addConstraintCNF(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, HashTableOrderPair * table, OrderPair * pair) {
151 if (pair->first > pair->second) {
153 flipped.first=pair->second;
154 flipped.second=pair->first;
158 if (!containsOrderPair(table, pair)) {
159 constraint = getNewVarSATEncoder(This);
160 OrderPair * paircopy = allocOrderPair(pair->first, pair->second, constraint);
161 putOrderPair(table, paircopy, paircopy);
163 constraint = getOrderPair(table, pair)->constraint;
165 return constraintNegate(constraint);
171 Edge encodeTotalOrderSATEncoder(SATEncoder *This, BooleanOrder * boolOrder){
172 ASSERT(boolOrder->order->type == TOTAL);
173 if(boolOrder->order->orderPairTable == NULL){
174 initializeOrderHashTable(boolOrder->order);
175 createAllTotalOrderConstraintsSATEncoder(This, boolOrder->order);
177 HashTableOrderPair* orderPairTable = boolOrder->order->orderPairTable;
178 OrderPair pair={boolOrder->first, boolOrder->second, E_NULL};
179 Edge constraint = getPairConstraint(This, orderPairTable, & pair);
183 void createAllTotalOrderConstraintsSATEncoder(SATEncoder* This, Order* order){
184 ASSERT(order->type == TOTAL);
185 VectorInt* mems = order->set->members;
186 HashTableOrderPair* table = order->orderPairTable;
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 addConstraintCNF(This->cnf, generateTransOrderConstraintSATEncoder(This, constIJ, constJK, constIK));
207 Edge getOrderConstraint(HashTableOrderPair *table, OrderPair *pair){
208 ASSERT(pair->first!= pair->second);
209 Edge constraint = getOrderPair(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 HashTableOrderPair* boolToConsts = boolOrder->order->boolsToConstraints;
231 if( containsOrderPair(boolToConsts, boolOrder) ){
232 return getOrderPair(boolToConsts, boolOrder);
234 Edge constraint = getNewVarSATEncoder(This);
235 putOrderPair(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 ArrayElement* inputs = &constraint->inputs;
293 uint inputNum =getSizeArrayElement(inputs);
294 //Encode all the inputs first ...
295 for(uint i=0; i<inputNum; i++){
296 encodeElementSATEncoder(This, getArrayElement(inputs, i));
299 uint size = getSizeVectorTableEntry(entries);
300 bool generateNegation = encType == ENUMERATEIMPLICATIONSNEGATE;
301 Edge constraints[size];
302 for(uint i=0; i<size; i++){
303 TableEntry* entry = getVectorTableEntry(entries, i);
304 if(generateNegation == entry->output) {
305 //Skip the irrelevant entries
308 Edge carray[inputNum];
309 for(uint j=0; j<inputNum; j++){
310 Element* el = getArrayElement(inputs, j);
311 carray[j] = getElementValueConstraint(This, el, entry->inputs[j]);
313 constraints[i]=constraintAND(This->cnf, inputNum, carray);
315 Edge result=constraintOR(This->cnf, size, constraints);
317 return generateNegation ? result: constraintNegate(result);
320 Edge encodeOperatorPredicateSATEncoder(SATEncoder * This, BooleanPredicate * constraint){
321 switch(constraint->encoding.type){
322 case ENUMERATEIMPLICATIONS:
323 return encodeEnumOperatorPredicateSATEncoder(This, constraint);
333 Edge encodeEnumOperatorPredicateSATEncoder(SATEncoder * This, BooleanPredicate * constraint){
334 ASSERT(GETPREDICATETYPE(constraint->predicate)==OPERATORPRED);
335 PredicateOperator* predicate = (PredicateOperator*)constraint->predicate;
336 ASSERT(predicate->op == EQUALS); //For now, we just only support equals
337 //getting maximum size of in common elements between two sets!
338 uint size=getSizeVectorInt( getArraySet( &predicate->domains, 0)->members);
339 uint64_t commonElements [size];
340 getEqualitySetIntersection(predicate, &size, commonElements);
342 Element* elem1 = getArrayElement( &constraint->inputs, 0);
343 Element* elem2 = getArrayElement( &constraint->inputs, 1);
344 encodeElementSATEncoder(This,elem1);
345 encodeElementSATEncoder(This, elem2);
347 for(uint i=0; i<size; i++){
348 Edge arg1 = getElementValueConstraint(This, elem1, commonElements[i]);
349 Edge arg2 = getElementValueConstraint(This, elem2, commonElements[i]);
350 carray[i] = constraintAND2(This->cnf, arg1, arg2);
352 //FIXME: the case when there is no intersection ....
353 return constraintOR(This->cnf, size, carray);
356 void encodeElementSATEncoder(SATEncoder* encoder, Element *This){
357 switch( GETELEMENTTYPE(This) ){
359 Edge c = encodeFunctionElementSATEncoder(This, (ElementFunction*) This);
360 addConstraint(encoder->cnf, c);
369 Edge encodeFunctionElementSATEncoder(SATEncoder* encoder, ElementFunction *This){
370 switch(GETFUNCTIONTYPE(This->function)){
372 return encodeTableElementFunctionSATEncoder(encoder, This);
374 return encodeOperatorElementFunctionSATEncoder(encoder, This);
381 Edge encodeTableElementFunctionSATEncoder(SATEncoder* encoder, ElementFunction* This){
382 switch(getElementFunctionEncoding(This)->type){
383 case ENUMERATEIMPLICATIONS:
384 return encodeEnumTableElemFunctionSATEncoder(encoder, This);
395 Edge encodeOperatorElementFunctionSATEncoder(SATEncoder* encoder, ElementFunction* This){
396 ASSERT(GETFUNCTIONTYPE(This->function) == OPERATORFUNC);
397 ASSERT(getSizeArrayElement(&This->inputs)==2 );
398 Element* elem1 = getArrayElement(&This->inputs,0);
399 Element* elem2 = getArrayElement(&This->inputs,1);
400 encodeElementSATEncoder(encoder, elem1);
401 encodeElementSATEncoder(encoder , elem2);
403 ElementEncoding* elemEnc1 = getElementEncoding( getArrayElement(&This->inputs,0) );
404 ElementEncoding* elemEnc2 = getElementEncoding( getArrayElement(&This->inputs,1) );
405 Edge carray[elemEnc1->encArraySize*elemEnc2->encArraySize];
407 Edge overFlowConstraint = ((BooleanVar*) This->overflowstatus)->var;
408 for(uint i=0; i<elemEnc1->encArraySize; i++){
409 if(isinUseElement(elemEnc1, i)){
410 for( uint j=0; j<elemEnc2->encArraySize; j++){
411 if(isinUseElement(elemEnc2, j)){
412 uint64_t result= applyFunctionOperator((FunctionOperator*)This->function,elemEnc1->encodingArray[i],
413 elemEnc2->encodingArray[j]);
414 bool isInRange = isInRangeFunction((FunctionOperator*)This->function, result);
416 //FIXME: instead of getElementValueConstraint, it might be useful to have another function
417 // that doesn't iterate over encodingArray and treats more efficient ...
418 Edge valConstrIn1 = getElementValueConstraint(encoder, elemEnc1->element, elemEnc1->encodingArray[i]);
419 Edge valConstrIn2 = getElementValueConstraint(encoder, elemEnc2->element, elemEnc2->encodingArray[j]);
420 Edge valConstrOut = getElementValueConstraint(encoder, (Element*) This, result);
421 if(edgeIsNull(valConstrOut))
422 continue; //FIXME:Should talk to brian about it!
423 Edge OpConstraint = constraintIMPLIES(encoder->cnf, constraintAND2(encoder->cnf, valConstrIn1, valConstrIn2), valConstrOut);
424 switch( ((FunctionOperator*)This->function)->overflowbehavior ){
427 carray[size++] = OpConstraint;
431 carray[size++] = OpConstraint;
433 case FLAGFORCESOVERFLOW:
435 Edge const1 = constraintIMPLIES(encoder->cnf, constraintAND2(encoder->cnf, valConstrIn1, valConstrIn2), constraintNegate(overFlowConstraint));
436 carray[size++] = constraintAND2(encoder->cnf, const1, OpConstraint);
439 case OVERFLOWSETSFLAG:
441 carray[size++] = OpConstraint;
443 carray[size++] = constraintIMPLIES(encoder->cnf, constraintAND2(encoder->cnf, valConstrIn1, valConstrIn2), overFlowConstraint);
446 case FLAGIFFOVERFLOW:
448 Edge const1 = constraintIMPLIES(encoder->cnf, constraintAND2(encoder->cnf, valConstrIn1, valConstrIn2), constraintNegate(overFlowConstraint));
449 carray[size++] = constraintAND2(encoder->cnf, const1, OpConstraint);
451 carray[size++] = constraintIMPLIES(encoder->cnf, constraintAND2(encoder->cnf, valConstrIn1, valConstrIn2), overFlowConstraint);
458 carray[size++] = OpConstraint;
468 Edge result = constraintAND(encoder->cnf, size, carray);
469 if (!edgeIsNull(elemc1))
470 result = constraintAND2(encoder->cnf, result, elemc1);
471 if (!edgeIsNull(elemc2))
472 result = constraintAND2(encoder->cnf, result, elemc2);
476 Edge encodeEnumTableElemFunctionSATEncoder(SATEncoder* encoder, ElementFunction* This){
477 ASSERT(GETFUNCTIONTYPE(This->function)==TABLEFUNC);
478 ArrayElement* elements= &This->inputs;
479 Table* table = ((FunctionTable*) (This->function))->table;
480 uint size = getSizeVectorTableEntry(&table->entries);
481 Edge constraints[size]; //FIXME: should add a space for the case that didn't match any entries
482 for(uint i=0; i<size; i++) {
483 TableEntry* entry = getVectorTableEntry(&table->entries, i);
484 uint inputNum = getSizeArrayElement(elements);
485 Edge carray[inputNum];
486 for(uint j=0; j<inputNum; j++){
487 Element* el= getArrayElement(elements, j);
488 carray[j] = getElementValueConstraint(encoder, el, entry->inputs[j]);
490 Edge output = getElementValueConstraint(encoder, (Element*)This, entry->output);
491 Edge row= constraintIMPLIES(encoder->cnf, constraintAND(encoder->cnf, inputNum, carray), output);
494 return constraintOR(encoder->cnf, size, constraints);