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;
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 HashTableBoolConst* boolToConsts = boolOrder->order->boolsToConstraints;
179 OrderPair pair={boolOrder->first, boolOrder->second};
180 Constraint* constraint = getPairConstraint(This, boolToConsts, & pair);
181 ASSERT(constraint != NULL);
185 void createAllTotalOrderConstraintsSATEncoder(SATEncoder* This, Order* order){
186 ASSERT(order->type == TOTAL);
187 VectorInt* mems = order->set->members;
188 HashTableBoolConst* table = order->boolsToConstraints;
189 uint size = getSizeVectorInt(mems);
190 for(uint i=0; i<size; i++){
191 uint64_t valueI = getVectorInt(mems, i);
192 for(uint j=i+1; j<size;j++){
193 uint64_t valueJ = getVectorInt(mems, j);
194 OrderPair pairIJ = {valueI, valueJ};
195 Constraint* constIJ=getPairConstraint(This, table, & pairIJ);
196 for(uint k=j+1; k<size; k++){
197 uint64_t valueK = getVectorInt(mems, k);
198 OrderPair pairJK = {valueJ, valueK};
199 OrderPair pairIK = {valueI, valueK};
200 Constraint* constIK = getPairConstraint(This, table, & pairIK);
201 Constraint* constJK = getPairConstraint(This, table, & pairJK);
202 generateTransOrderConstraintSATEncoder(This, constIJ, constJK, constIK);
208 Constraint* getOrderConstraint(HashTableBoolConst *table, OrderPair *pair){
209 ASSERT(pair->first!= pair->second);
210 Constraint* constraint= getBoolConst(table, pair);
211 ASSERT(constraint!= NULL);
212 if(pair->first > pair->second)
215 return negateConstraint(constraint);
218 Constraint * generateTransOrderConstraintSATEncoder(SATEncoder *This, Constraint *constIJ,Constraint *constJK,Constraint *constIK){
219 //FIXME: first we should add the the constraint to the satsolver!
220 ASSERT(constIJ!= NULL && constJK != NULL && constIK != NULL);
221 Constraint *carray[] = {constIJ, constJK, negateConstraint(constIK)};
222 Constraint * loop1= allocArrayConstraint(OR, 3, carray);
223 Constraint * carray2[] = {negateConstraint(constIJ), negateConstraint(constJK), constIK};
224 Constraint * loop2= allocArrayConstraint(OR, 3,carray2 );
225 return allocConstraint(AND, loop1, loop2);
228 Constraint * encodePartialOrderSATEncoder(SATEncoder *This, BooleanOrder * constraint){
229 // FIXME: we can have this implementation for partial order. Basically,
230 // we compute the transitivity between two order constraints specified by the client! (also can be used
231 // when client specify sparse constraints for the total order!)
232 ASSERT(constraint->order->type == PARTIAL);
234 HashTableBoolConst* boolToConsts = boolOrder->order->boolsToConstraints;
235 if( containsBoolConst(boolToConsts, boolOrder) ){
236 return getBoolConst(boolToConsts, boolOrder);
238 Constraint* constraint = getNewVarSATEncoder(This);
239 putBoolConst(boolToConsts,boolOrder, constraint);
240 VectorBoolean* orderConstrs = &boolOrder->order->constraints;
241 uint size= getSizeVectorBoolean(orderConstrs);
242 for(uint i=0; i<size; i++){
243 ASSERT(GETBOOLEANTYPE( getVectorBoolean(orderConstrs, i)) == ORDERCONST );
244 BooleanOrder* tmp = (BooleanOrder*)getVectorBoolean(orderConstrs, i);
245 BooleanOrder* newBool;
246 Constraint* first, *second;
247 if(tmp->second==boolOrder->first){
248 newBool = (BooleanOrder*)allocBooleanOrder(tmp->order,tmp->first,boolOrder->second);
249 first = encodeTotalOrderSATEncoder(This, tmp);
252 }else if (boolOrder->second == tmp->first){
253 newBool = (BooleanOrder*)allocBooleanOrder(tmp->order,boolOrder->first,tmp->second);
255 second = encodeTotalOrderSATEncoder(This, tmp);
258 Constraint* transConstr= encodeTotalOrderSATEncoder(This, newBool);
259 generateTransOrderConstraintSATEncoder(This, first, second, transConstr );
267 Constraint * encodePredicateSATEncoder(SATEncoder * This, BooleanPredicate * constraint) {
268 switch(GETPREDICATETYPE(constraint->predicate) ){
270 return encodeTablePredicateSATEncoder(This, constraint);
272 return encodeOperatorPredicateSATEncoder(This, constraint);
279 Constraint * encodeTablePredicateSATEncoder(SATEncoder * This, BooleanPredicate * constraint){
280 switch(constraint->encoding.type){
281 case ENUMERATEIMPLICATIONS:
282 case ENUMERATEIMPLICATIONSNEGATE:
283 return encodeEnumTablePredicateSATEncoder(This, constraint);
293 Constraint * encodeEnumTablePredicateSATEncoder(SATEncoder * This, BooleanPredicate * constraint){
294 VectorTableEntry* entries = &(((PredicateTable*)constraint->predicate)->table->entries);
295 FunctionEncodingType encType = constraint->encoding.type;
296 uint size = getSizeVectorTableEntry(entries);
297 Constraint* constraints[size];
298 for(uint i=0; i<size; i++){
299 TableEntry* entry = getVectorTableEntry(entries, i);
300 if(encType==ENUMERATEIMPLICATIONS && entry->output!= true)
302 else if(encType==ENUMERATEIMPLICATIONSNEGATE && entry->output !=false)
304 ArrayElement* inputs = &constraint->inputs;
305 uint inputNum =getSizeArrayElement(inputs);
306 Constraint* carray[inputNum];
307 for(uint j=0; j<inputNum; j++){
308 Element* el = getArrayElement(inputs, j);
309 if( GETELEMENTTYPE(el) == ELEMFUNCRETURN)
310 encodeFunctionElementSATEncoder(This, (ElementFunction*) el);
311 carray[j] = getElementValueConstraint(This,el, entry->inputs[j]);
312 ASSERT(carray[j]!= NULL);
314 constraints[i]=allocArrayConstraint(AND, inputNum, carray);
316 Constraint* result= allocArrayConstraint(OR, size, constraints);
317 //FIXME: if it didn't match with any entry
318 return encType==ENUMERATEIMPLICATIONS? result: negateConstraint(result);
321 Constraint * encodeOperatorPredicateSATEncoder(SATEncoder * This, BooleanPredicate * constraint){
322 switch(constraint->encoding.type){
323 case ENUMERATEIMPLICATIONS:
324 return encodeEnumOperatorPredicateSATEncoder(This, constraint);
334 Constraint * encodeEnumOperatorPredicateSATEncoder(SATEncoder * This, BooleanPredicate * constraint){
335 ASSERT(GETPREDICATETYPE(constraint->predicate)==OPERATORPRED);
336 PredicateOperator* predicate = (PredicateOperator*)constraint->predicate;
337 ASSERT(predicate->op == EQUALS); //For now, we just only support equals
338 //getting maximum size of in common elements between two sets!
339 uint size=getSizeVectorInt( getArraySet( &predicate->domains, 0)->members);
340 uint64_t commonElements [size];
341 getEqualitySetIntersection(predicate, &size, commonElements);
342 Constraint* carray[size];
343 Element* elem1 = getArrayElement( &constraint->inputs, 0);
344 if( GETELEMENTTYPE(elem1) == ELEMFUNCRETURN)
345 encodeFunctionElementSATEncoder(This, (ElementFunction*) elem1);
346 Element* elem2 = getArrayElement( &constraint->inputs, 1);
347 if( GETELEMENTTYPE(elem2) == ELEMFUNCRETURN)
348 encodeFunctionElementSATEncoder(This, (ElementFunction*) elem2);
349 for(uint i=0; i<size; i++){
350 Constraint* arg1 = getElementValueConstraint(This, elem1, commonElements[i]);
352 Constraint* arg2 = getElementValueConstraint(This, elem2, commonElements[i]);
353 ASSERT(arg2 != NULL);
354 carray[i] = allocConstraint(AND, arg1, arg2);
356 //FIXME: the case when there is no intersection ....
357 return allocArrayConstraint(OR, size, carray);
360 Constraint* encodeFunctionElementSATEncoder(SATEncoder* encoder, ElementFunction *This){
361 switch(GETFUNCTIONTYPE(This->function)){
363 return encodeTableElementFunctionSATEncoder(encoder, This);
365 return encodeOperatorElementFunctionSATEncoder(encoder, This);
372 Constraint* encodeTableElementFunctionSATEncoder(SATEncoder* encoder, ElementFunction* This){
373 switch(getElementFunctionEncoding(This)->type){
374 case ENUMERATEIMPLICATIONS:
375 return encodeEnumTableElemFunctionSATEncoder(encoder, This);
386 Constraint* encodeOperatorElementFunctionSATEncoder(SATEncoder* encoder, ElementFunction* This){
387 ASSERT(GETFUNCTIONTYPE(This->function) == OPERATORFUNC);
388 ASSERT(getSizeArrayElement(&This->inputs)==2 );
389 ElementEncoding* elem1 = getElementEncoding( getArrayElement(&This->inputs,0) );
390 generateElementEncodingVariables(encoder, elem1);
391 ElementEncoding* elem2 = getElementEncoding( getArrayElement(&This->inputs,1) );
392 generateElementEncodingVariables(encoder, elem2);
393 Constraint* carray[elem1->encArraySize*elem2->encArraySize];
395 Constraint* overFlowConstraint = ((BooleanVar*) This->overflowstatus)->var;
396 for(uint i=0; i<elem1->encArraySize; i++){
397 if(isinUseElement(elem1, i)){
398 for(uint j=0; j<elem2->encArraySize; j++){
399 if(isinUseElement(elem2, j)){
400 bool isInRange = false, hasOverFlow=false;
401 uint64_t result= applyFunctionOperator((FunctionOperator*)This->function,elem1->encodingArray[i],
402 elem2->encodingArray[j], &isInRange, &hasOverFlow);
404 break; // Ignoring the cases that result of operation doesn't exist in the code.
405 //FIXME: instead of getElementValueConstraint, it might be useful to have another function
406 // that doesn't iterate over encodingArray and treats more efficient ...
407 Constraint* and1 = getElementValueConstraint(encoder, elem1->element, elem1->encodingArray[i]);
408 ASSERT(and1 != NULL);
409 Constraint* and2 = getElementValueConstraint(encoder, elem2->element, elem2->encodingArray[j]);
410 ASSERT(and2 != NULL);
411 Constraint* imply2 = getElementValueConstraint(encoder, (Element*) This, result);
412 ASSERT(imply2 != NULL);
413 Constraint* constraint = allocConstraint(IMPLIES,
414 allocConstraint(AND, and1, and2) , imply2);
415 switch( ((FunctionOperator*)This->function)->overflowbehavior ){
418 carray[size++] = constraint;
422 carray[size++] = constraint;
424 case FLAGFORCESOVERFLOW:
426 Constraint* const1 = allocConstraint(IMPLIES, overFlowConstraint,
427 allocConstraint(AND, getElementValueConstraint(encoder, elem1->element, elem1->encodingArray[i]),
428 getElementValueConstraint(encoder, elem2->element, elem2->encodingArray[j])));
429 carray[size++] = allocConstraint(AND, const1, constraint);
432 case OVERFLOWSETSFLAG:
434 Constraint* const1 = allocConstraint(IMPLIES, allocConstraint(AND, getElementValueConstraint(encoder, elem1->element, elem1->encodingArray[i]),
435 getElementValueConstraint(encoder, elem2->element, elem2->encodingArray[j])), overFlowConstraint);
436 carray[size++] = allocConstraint(AND, const1, constraint);
438 carray[size++] = constraint;
440 case FLAGIFFOVERFLOW:
442 carray[size++] = constraint;
444 Constraint* const1 = allocConstraint(IMPLIES, overFlowConstraint,
445 allocConstraint(AND, getElementValueConstraint(encoder, elem1->element, elem1->encodingArray[i]),
446 getElementValueConstraint(encoder, elem2->element, elem2->encodingArray[j])));
447 Constraint* const2 = allocConstraint(IMPLIES, allocConstraint(AND, getElementValueConstraint(encoder, elem1->element, elem1->encodingArray[i]),
448 getElementValueConstraint(encoder, elem2->element, elem2->encodingArray[j])), overFlowConstraint);
449 Constraint* res [] = {const1, const2, constraint};
450 carray[size++] = allocArrayConstraint(AND, 3, res);
457 carray[size++] = constraint;
467 return allocArrayConstraint(AND, size, carray);
470 Constraint* encodeEnumTableElemFunctionSATEncoder(SATEncoder* encoder, ElementFunction* This){
471 ASSERT(GETFUNCTIONTYPE(This->function)==TABLEFUNC);
472 ArrayElement* elements= &This->inputs;
473 Table* table = ((FunctionTable*) (This->function))->table;
474 uint size = getSizeVectorTableEntry(&table->entries);
475 Constraint* constraints[size]; //FIXME: should add a space for the case that didn't match any entries
476 for(uint i=0; i<size; i++){
477 TableEntry* entry = getVectorTableEntry(&table->entries, i);
478 uint inputNum =getSizeArrayElement(elements);
479 Constraint* carray[inputNum];
480 for(uint j=0; j<inputNum; j++){
481 Element* el= getArrayElement(elements, j);
482 carray[j] = getElementValueConstraint(encoder, el, entry->inputs[j]);
483 ASSERT(carray[j]!= NULL);
485 Constraint* output = getElementValueConstraint(encoder, (Element*)This, entry->output);
486 ASSERT(output!= NULL);
487 Constraint* row= allocConstraint(IMPLIES, allocArrayConstraint(AND, inputNum, carray), output);
490 Constraint* result = allocArrayConstraint(OR, size, constraints);