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));
22 void deleteSATEncoder(SATEncoder *This) {
26 Constraint * getElementValueConstraint(SATEncoder* encoder,Element* This, uint64_t value) {
27 generateElementEncodingVariables(encoder, getElementEncoding(This));
28 switch(getElementEncoding(This)->type){
36 return getElementValueBinaryIndexConstraint(This, value);
50 Constraint * getElementValueBinaryIndexConstraint(Element* This, uint64_t value) {
51 ASTNodeType type = GETELEMENTTYPE(This);
52 ASSERT(type == ELEMSET || type == ELEMFUNCRETURN);
53 ElementEncoding* elemEnc = getElementEncoding(This);
54 for(uint i=0; i<elemEnc->encArraySize; i++){
55 if( isinUseElement(elemEnc, i) && elemEnc->encodingArray[i]==value){
56 return generateBinaryConstraint(elemEnc->numVars,
57 elemEnc->variables, i);
63 void encodeAllSATEncoder(CSolver *csolver, SATEncoder * This) {
64 VectorBoolean *constraints=csolver->constraints;
65 uint size=getSizeVectorBoolean(constraints);
66 for(uint i=0;i<size;i++) {
67 Boolean *constraint=getVectorBoolean(constraints, i);
68 Constraint* c= encodeConstraintSATEncoder(This, constraint);
74 Constraint * encodeConstraintSATEncoder(SATEncoder *This, Boolean *constraint) {
75 switch(GETBOOLEANTYPE(constraint)) {
77 return encodeOrderSATEncoder(This, (BooleanOrder *) constraint);
79 return encodeVarSATEncoder(This, (BooleanVar *) constraint);
81 return encodeLogicSATEncoder(This, (BooleanLogic *) constraint);
83 return encodePredicateSATEncoder(This, (BooleanPredicate *) constraint);
85 model_print("Unhandled case in encodeConstraintSATEncoder %u", GETBOOLEANTYPE(constraint));
90 void getArrayNewVarsSATEncoder(SATEncoder* encoder, uint num, Constraint **carray) {
91 for(uint i=0;i<num;i++)
92 carray[i]=getNewVarSATEncoder(encoder);
95 Constraint * getNewVarSATEncoder(SATEncoder *This) {
96 Constraint * var=allocVarConstraint(VAR, This->varcount);
97 Constraint * varneg=allocVarConstraint(NOTVAR, This->varcount++);
98 setNegConstraint(var, varneg);
99 setNegConstraint(varneg, var);
103 Constraint * encodeVarSATEncoder(SATEncoder *This, BooleanVar * constraint) {
104 if (constraint->var == NULL) {
105 constraint->var=getNewVarSATEncoder(This);
107 return constraint->var;
110 Constraint * encodeLogicSATEncoder(SATEncoder *This, BooleanLogic * constraint) {
111 Constraint * 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 allocArrayConstraint(AND, getSizeArrayBoolean(&constraint->inputs), array);
119 return allocArrayConstraint(OR, getSizeArrayBoolean(&constraint->inputs), array);
121 ASSERT( getSizeArrayBoolean(&constraint->inputs)==1);
122 return negateConstraint(array[0]);
124 ASSERT( getSizeArrayBoolean(&constraint->inputs)==2);
125 Constraint * nleft=negateConstraint(cloneConstraint(array[0]));
126 Constraint * nright=negateConstraint(cloneConstraint(array[1]));
127 return allocConstraint(OR,
128 allocConstraint(AND, array[0], nright),
129 allocConstraint(AND, nleft, array[1]));
132 ASSERT( getSizeArrayBoolean( &constraint->inputs)==2);
133 return allocConstraint(IMPLIES, array[0], array[1]);
135 model_print("Unhandled case in encodeLogicSATEncoder %u", constraint->op);
141 Constraint * encodeOrderSATEncoder(SATEncoder *This, BooleanOrder * constraint) {
142 switch( constraint->order->type){
144 return encodePartialOrderSATEncoder(This, constraint);
146 return encodeTotalOrderSATEncoder(This, constraint);
153 Constraint * getPairConstraint(SATEncoder *This, HashTableBoolConst * table, OrderPair * pair) {
156 if (pair->first > pair->second) {
158 flipped.first=pair->second;
159 flipped.second=pair->first;
160 pair = &flipped; //FIXME: accessing a local variable from outside of the function?
162 Constraint * constraint;
163 if (!containsBoolConst(table, pair)) {
164 constraint = getNewVarSATEncoder(This);
165 OrderPair * paircopy = allocOrderPair(pair->first, pair->second);
166 putBoolConst(table, paircopy, constraint);
168 constraint = getBoolConst(table, pair);
170 return negateConstraint(constraint);
176 Constraint * encodeTotalOrderSATEncoder(SATEncoder *This, BooleanOrder * boolOrder){
177 ASSERT(boolOrder->order->type == TOTAL);
178 if(boolOrder->order->boolsToConstraints == NULL){
179 initializeOrderHashTable(boolOrder->order);
180 return createAllTotalOrderConstraintsSATEncoder(This, boolOrder->order);
182 HashTableBoolConst* boolToConsts = boolOrder->order->boolsToConstraints;
183 OrderPair pair={boolOrder->first, boolOrder->second};
184 Constraint* constraint = getPairConstraint(This, boolToConsts, & pair);
185 ASSERT(constraint != NULL);
189 Constraint* createAllTotalOrderConstraintsSATEncoder(SATEncoder* This, Order* order){
190 ASSERT(order->type == TOTAL);
191 VectorInt* mems = order->set->members;
192 HashTableBoolConst* table = order->boolsToConstraints;
193 uint size = getSizeVectorInt(mems);
194 Constraint* constraints [size*size];
196 for(uint i=0; i<size; i++){
197 uint64_t valueI = getVectorInt(mems, i);
198 for(uint j=i+1; j<size;j++){
199 uint64_t valueJ = getVectorInt(mems, j);
200 OrderPair pairIJ = {valueI, valueJ};
201 Constraint* constIJ=getPairConstraint(This, table, & pairIJ);
202 for(uint k=j+1; k<size; k++){
203 uint64_t valueK = getVectorInt(mems, k);
204 OrderPair pairJK = {valueJ, valueK};
205 OrderPair pairIK = {valueI, valueK};
206 Constraint* constIK = getPairConstraint(This, table, & pairIK);
207 Constraint* constJK = getPairConstraint(This, table, & pairJK);
208 constraints[csize++] = generateTransOrderConstraintSATEncoder(This, constIJ, constJK, constIK);
209 ASSERT(csize < size*size);
213 return allocArrayConstraint(AND, csize, constraints);
216 Constraint* getOrderConstraint(HashTableBoolConst *table, OrderPair *pair){
217 ASSERT(pair->first!= pair->second);
218 Constraint* constraint= getBoolConst(table, pair);
219 ASSERT(constraint!= NULL);
220 if(pair->first > pair->second)
223 return negateConstraint(constraint);
226 Constraint * generateTransOrderConstraintSATEncoder(SATEncoder *This, Constraint *constIJ,Constraint *constJK,Constraint *constIK){
227 //FIXME: first we should add the the constraint to the satsolver!
228 ASSERT(constIJ!= NULL && constJK != NULL && constIK != NULL);
229 Constraint *carray[] = {constIJ, constJK, negateConstraint(constIK)};
230 Constraint * loop1= allocArrayConstraint(OR, 3, carray);
231 Constraint * carray2[] = {negateConstraint(constIJ), negateConstraint(constJK), constIK};
232 Constraint * loop2= allocArrayConstraint(OR, 3,carray2 );
233 return allocConstraint(AND, loop1, loop2);
236 Constraint * encodePartialOrderSATEncoder(SATEncoder *This, BooleanOrder * constraint){
237 // FIXME: we can have this implementation for partial order. Basically,
238 // we compute the transitivity between two order constraints specified by the client! (also can be used
239 // when client specify sparse constraints for the total order!)
240 ASSERT(constraint->order->type == PARTIAL);
242 HashTableBoolConst* boolToConsts = boolOrder->order->boolsToConstraints;
243 if( containsBoolConst(boolToConsts, boolOrder) ){
244 return getBoolConst(boolToConsts, boolOrder);
246 Constraint* constraint = getNewVarSATEncoder(This);
247 putBoolConst(boolToConsts,boolOrder, constraint);
248 VectorBoolean* orderConstrs = &boolOrder->order->constraints;
249 uint size= getSizeVectorBoolean(orderConstrs);
250 for(uint i=0; i<size; i++){
251 ASSERT(GETBOOLEANTYPE( getVectorBoolean(orderConstrs, i)) == ORDERCONST );
252 BooleanOrder* tmp = (BooleanOrder*)getVectorBoolean(orderConstrs, i);
253 BooleanOrder* newBool;
254 Constraint* first, *second;
255 if(tmp->second==boolOrder->first){
256 newBool = (BooleanOrder*)allocBooleanOrder(tmp->order,tmp->first,boolOrder->second);
257 first = encodeTotalOrderSATEncoder(This, tmp);
260 }else if (boolOrder->second == tmp->first){
261 newBool = (BooleanOrder*)allocBooleanOrder(tmp->order,boolOrder->first,tmp->second);
263 second = encodeTotalOrderSATEncoder(This, tmp);
266 Constraint* transConstr= encodeTotalOrderSATEncoder(This, newBool);
267 generateTransOrderConstraintSATEncoder(This, first, second, transConstr );
275 Constraint * encodePredicateSATEncoder(SATEncoder * This, BooleanPredicate * constraint) {
276 switch(GETPREDICATETYPE(constraint->predicate) ){
278 return encodeTablePredicateSATEncoder(This, constraint);
280 return encodeOperatorPredicateSATEncoder(This, constraint);
287 Constraint * encodeTablePredicateSATEncoder(SATEncoder * This, BooleanPredicate * constraint){
288 switch(constraint->encoding.type){
289 case ENUMERATEIMPLICATIONS:
290 case ENUMERATEIMPLICATIONSNEGATE:
291 return encodeEnumTablePredicateSATEncoder(This, constraint);
301 Constraint * encodeEnumTablePredicateSATEncoder(SATEncoder * This, BooleanPredicate * constraint){
302 VectorTableEntry* entries = &(((PredicateTable*)constraint->predicate)->table->entries);
303 FunctionEncodingType encType = constraint->encoding.type;
304 uint size = getSizeVectorTableEntry(entries);
305 Constraint* constraints[size];
306 for(uint i=0; i<size; i++){
307 TableEntry* entry = getVectorTableEntry(entries, i);
308 if(encType==ENUMERATEIMPLICATIONS && entry->output!= true)
310 else if(encType==ENUMERATEIMPLICATIONSNEGATE && entry->output !=false)
312 ArrayElement* inputs = &constraint->inputs;
313 uint inputNum =getSizeArrayElement(inputs);
314 Constraint* carray[inputNum];
315 for(uint j=0; j<inputNum; j++){
316 Element* el = getArrayElement(inputs, j);
317 Constraint* tmpc = getElementValueConstraint(This,el, entry->inputs[j]);
319 if( GETELEMENTTYPE(el) == ELEMFUNCRETURN){
320 Constraint* func =encodeFunctionElementSATEncoder(This, (ElementFunction*) el);
322 carray[j] = allocConstraint(AND, func, tmpc);
326 ASSERT(carray[j]!= NULL);
328 constraints[i]=allocArrayConstraint(AND, inputNum, carray);
330 Constraint* result= allocArrayConstraint(OR, size, constraints);
331 //FIXME: if it didn't match with any entry
332 return encType==ENUMERATEIMPLICATIONS? result: negateConstraint(result);
335 Constraint * encodeOperatorPredicateSATEncoder(SATEncoder * This, BooleanPredicate * constraint){
336 switch(constraint->encoding.type){
337 case ENUMERATEIMPLICATIONS:
338 return encodeEnumOperatorPredicateSATEncoder(This, constraint);
348 Constraint * encodeEnumOperatorPredicateSATEncoder(SATEncoder * This, BooleanPredicate * constraint){
349 ASSERT(GETPREDICATETYPE(constraint->predicate)==OPERATORPRED);
350 PredicateOperator* predicate = (PredicateOperator*)constraint->predicate;
351 ASSERT(predicate->op == EQUALS); //For now, we just only support equals
352 //getting maximum size of in common elements between two sets!
353 uint size=getSizeVectorInt( getArraySet( &predicate->domains, 0)->members);
354 uint64_t commonElements [size];
355 getEqualitySetIntersection(predicate, &size, commonElements);
356 Constraint* carray[size];
357 Element* elem1 = getArrayElement( &constraint->inputs, 0);
358 Constraint *elemc1 = NULL, *elemc2 = NULL;
359 if( GETELEMENTTYPE(elem1) == ELEMFUNCRETURN)
360 elemc1 = encodeFunctionElementSATEncoder(This, (ElementFunction*) elem1);
361 Element* elem2 = getArrayElement( &constraint->inputs, 1);
362 if( GETELEMENTTYPE(elem2) == ELEMFUNCRETURN)
363 elemc2 = encodeFunctionElementSATEncoder(This, (ElementFunction*) elem2);
364 for(uint i=0; i<size; i++){
365 Constraint* arg1 = getElementValueConstraint(This, elem1, commonElements[i]);
367 Constraint* arg2 = getElementValueConstraint(This, elem2, commonElements[i]);
368 ASSERT(arg2 != NULL);
369 carray[i] = allocConstraint(AND, arg1, arg2);
371 //FIXME: the case when there is no intersection ....
372 Constraint* result = allocArrayConstraint(OR, size, carray);
373 ASSERT(result!= NULL);
375 result = allocConstraint(AND, result, elemc1);
377 result = allocConstraint (AND, result, elemc2);
381 Constraint* encodeFunctionElementSATEncoder(SATEncoder* encoder, ElementFunction *This){
382 switch(GETFUNCTIONTYPE(This->function)){
384 return encodeTableElementFunctionSATEncoder(encoder, This);
386 return encodeOperatorElementFunctionSATEncoder(encoder, This);
393 Constraint* encodeTableElementFunctionSATEncoder(SATEncoder* encoder, ElementFunction* This){
394 switch(getElementFunctionEncoding(This)->type){
395 case ENUMERATEIMPLICATIONS:
396 return encodeEnumTableElemFunctionSATEncoder(encoder, This);
407 Constraint* encodeOperatorElementFunctionSATEncoder(SATEncoder* encoder, ElementFunction* This){
408 ASSERT(GETFUNCTIONTYPE(This->function) == OPERATORFUNC);
409 ASSERT(getSizeArrayElement(&This->inputs)==2 );
410 ElementEncoding* elem1 = getElementEncoding( getArrayElement(&This->inputs,0) );
411 ElementEncoding* elem2 = getElementEncoding( getArrayElement(&This->inputs,1) );
412 Constraint* carray[elem1->encArraySize*elem2->encArraySize];
414 Constraint* overFlowConstraint = ((BooleanVar*) This->overflowstatus)->var;
415 for(uint i=0; i<elem1->encArraySize; i++){
416 if(isinUseElement(elem1, i)){
417 for( uint j=0; j<elem2->encArraySize; j++){
418 if(isinUseElement(elem2, j)){
419 bool isInRange = false;
420 uint64_t result= applyFunctionOperator((FunctionOperator*)This->function,elem1->encodingArray[i],
421 elem2->encodingArray[j], &isInRange);
422 //FIXME: instead of getElementValueConstraint, it might be useful to have another function
423 // that doesn't iterate over encodingArray and treats more efficient ...
424 Constraint* valConstrIn1 = getElementValueConstraint(encoder, elem1->element, elem1->encodingArray[i]);
425 ASSERT(valConstrIn1 != NULL);
426 Constraint* valConstrIn2 = getElementValueConstraint(encoder, elem2->element, elem2->encodingArray[j]);
427 ASSERT(valConstrIn2 != NULL);
428 Constraint* valConstrOut = getElementValueConstraint(encoder, (Element*) This, result);
429 if(valConstrOut == NULL)
430 continue; //FIXME:Should talk to brian about it!
431 Constraint* OpConstraint = allocConstraint(IMPLIES,
432 allocConstraint(AND, valConstrIn1, valConstrIn2) , valConstrOut);
433 switch( ((FunctionOperator*)This->function)->overflowbehavior ){
436 carray[size++] = OpConstraint;
440 carray[size++] = OpConstraint;
442 case FLAGFORCESOVERFLOW:
444 Constraint* const1 = allocConstraint(IMPLIES,
445 allocConstraint(AND, valConstrIn1, valConstrIn2),
446 negateConstraint(overFlowConstraint));
447 carray[size++] = allocConstraint(AND, const1, OpConstraint);
450 case OVERFLOWSETSFLAG:
452 carray[size++] = OpConstraint;
454 carray[size++] = allocConstraint(IMPLIES,
455 allocConstraint(AND, valConstrIn1, valConstrIn2),
459 case FLAGIFFOVERFLOW:
461 Constraint* const1 = allocConstraint(IMPLIES,
462 allocConstraint(AND, valConstrIn1, valConstrIn2),
463 negateConstraint(overFlowConstraint));
464 carray[size++] = allocConstraint(AND, const1, OpConstraint);
466 carray[size++] = allocConstraint(IMPLIES,
467 allocConstraint(AND, valConstrIn1, valConstrIn2),
475 carray[size++] = OpConstraint;
485 return allocArrayConstraint(AND, size, carray);
488 Constraint* encodeEnumTableElemFunctionSATEncoder(SATEncoder* encoder, ElementFunction* This){
489 ASSERT(GETFUNCTIONTYPE(This->function)==TABLEFUNC);
490 ArrayElement* elements= &This->inputs;
491 Table* table = ((FunctionTable*) (This->function))->table;
492 uint size = getSizeVectorTableEntry(&table->entries);
493 Constraint* constraints[size]; //FIXME: should add a space for the case that didn't match any entries
494 for(uint i=0; i<size; i++){
495 TableEntry* entry = getVectorTableEntry(&table->entries, i);
496 uint inputNum =getSizeArrayElement(elements);
497 Constraint* carray[inputNum];
498 for(uint j=0; j<inputNum; j++){
499 Element* el= getArrayElement(elements, j);
500 carray[j] = getElementValueConstraint(encoder, el, entry->inputs[j]);
501 ASSERT(carray[j]!= NULL);
503 Constraint* output = getElementValueConstraint(encoder, (Element*)This, entry->output);
504 ASSERT(output!= NULL);
505 Constraint* row= allocConstraint(IMPLIES, allocArrayConstraint(AND, inputNum, carray), output);
508 Constraint* result = allocArrayConstraint(OR, size, constraints);