src/Backend/satencoder.c

   1 #include "satencoder.h"
   2 #include "structs.h"
   3 #include "csolver.h"
   4 #include "boolean.h"
   5 #include "constraint.h"
   6 #include "common.h"
   7 #include "element.h"
   8 #include "function.h"
   9 #include "tableentry.h"
  10 #include "table.h"
  11 #include "order.h"
  12 #include "predicate.h"
  13 #include "orderpair.h"
  14 #include "set.h"
  15
  16 SATEncoder * allocSATEncoder() {
  17         SATEncoder *This=ourmalloc(sizeof (SATEncoder));
  18         This->varcount=1;
  19         This->satSolver = allocIncrementalSolver();
  20         return This;
  21 }
  22
  23 void deleteSATEncoder(SATEncoder *This) {
  24         deleteIncrementalSolver(This->satSolver);
  25         ourfree(This);
  26 }
  27
  28 Constraint * getElementValueConstraint(SATEncoder* encoder,Element* This, uint64_t value) {
  29         generateElementEncodingVariables(encoder, getElementEncoding(This));
  30         switch(getElementEncoding(This)->type){
  31                 case ONEHOT:
  32                         //FIXME
  33                         ASSERT(0);
  34                         break;
  35                 case UNARY:
  36                         ASSERT(0);
  37                         break;
  38                 case BINARYINDEX:
  39                         return getElementValueBinaryIndexConstraint(This, value);
  40                         break;
  41                 case ONEHOTBINARY:
  42                         ASSERT(0);
  43                         break;
  44                 case BINARYVAL:
  45                         ASSERT(0);
  46                         break;
  47                 default:
  48                         ASSERT(0);
  49                         break;
  50         }
  51         return NULL;
  52 }
  53 Constraint * getElementValueBinaryIndexConstraint(Element* This, uint64_t value) {
  54         ASTNodeType type = GETELEMENTTYPE(This);
  55         ASSERT(type == ELEMSET || type == ELEMFUNCRETURN);
  56         ElementEncoding* elemEnc = getElementEncoding(This);
  57         for(uint i=0; i<elemEnc->encArraySize; i++){
  58                 if( isinUseElement(elemEnc, i) && elemEnc->encodingArray[i]==value){
  59                         return generateBinaryConstraint(elemEnc->numVars,
  60                                 elemEnc->variables, i);
  61                 }
  62         }
  63         return NULL;
  64 }
  65
  66 void addConstraintToSATSolver(Constraint *c, IncrementalSolver* satSolver) {
  67         VectorConstraint* simplified = simplifyConstraint(c);
  68         uint size = getSizeVectorConstraint(simplified);
  69         for(uint i=0; i<size; i++) {
  70                 Constraint *simp=getVectorConstraint(simplified, i);
  71                 if (simp->type==TRUE)
  72                         continue;
  73                 ASSERT(simp->type!=FALSE);
  74                 dumpConstraint(simp, satSolver);
  75                 freerecConstraint(simp);
  76         }
  77         deleteVectorConstraint(simplified);
  78 }
  79
  80 void encodeAllSATEncoder(CSolver *csolver, SATEncoder * This) {
  81         VectorBoolean *constraints=csolver->constraints;
  82         uint size=getSizeVectorBoolean(constraints);
  83         for(uint i=0;i<size;i++) {
  84                 Boolean *constraint=getVectorBoolean(constraints, i);
  85                 Constraint* c= encodeConstraintSATEncoder(This, constraint);
  86                 printConstraint(c);
  87                 model_print("\n\n");
  88                 addConstraintToSATSolver(c, This->satSolver);
  89         }
  90 }
  91
  92 Constraint * encodeConstraintSATEncoder(SATEncoder *This, Boolean *constraint) {
  93         switch(GETBOOLEANTYPE(constraint)) {
  94         case ORDERCONST:
  95                 return encodeOrderSATEncoder(This, (BooleanOrder *) constraint);
  96         case BOOLEANVAR:
  97                 return encodeVarSATEncoder(This, (BooleanVar *) constraint);
  98         case LOGICOP:
  99                 return encodeLogicSATEncoder(This, (BooleanLogic *) constraint);
 100         case PREDICATEOP:
 101                 return encodePredicateSATEncoder(This, (BooleanPredicate *) constraint);
 102         default:
 103                 model_print("Unhandled case in encodeConstraintSATEncoder %u", GETBOOLEANTYPE(constraint));
 104                 exit(-1);
 105         }
 106 }
 107
 108 void getArrayNewVarsSATEncoder(SATEncoder* encoder, uint num, Constraint **carray) {
 109         for(uint i=0;i<num;i++)
 110                 carray[i]=getNewVarSATEncoder(encoder);
 111 }
 112
 113 Constraint * getNewVarSATEncoder(SATEncoder *This) {
 114         Constraint * var=allocVarConstraint(VAR, This->varcount);
 115         Constraint * varneg=allocVarConstraint(NOTVAR, This->varcount++);
 116         setNegConstraint(var, varneg);
 117         setNegConstraint(varneg, var);
 118         return var;
 119 }
 120
 121 Constraint * encodeVarSATEncoder(SATEncoder *This, BooleanVar * constraint) {
 122         if (constraint->var == NULL) {
 123                 constraint->var=getNewVarSATEncoder(This);
 124         }
 125         return constraint->var;
 126 }
 127
 128 Constraint * encodeLogicSATEncoder(SATEncoder *This, BooleanLogic * constraint) {
 129         Constraint * array[getSizeArrayBoolean(&constraint->inputs)];
 130         for(uint i=0;i<getSizeArrayBoolean(&constraint->inputs);i++)
 131                 array[i]=encodeConstraintSATEncoder(This, getArrayBoolean(&constraint->inputs, i));
 132
 133         switch(constraint->op) {
 134         case L_AND:
 135                 return allocArrayConstraint(AND, getSizeArrayBoolean(&constraint->inputs), array);
 136         case L_OR:
 137                 return allocArrayConstraint(OR, getSizeArrayBoolean(&constraint->inputs), array);
 138         case L_NOT:
 139                 ASSERT( getSizeArrayBoolean(&constraint->inputs)==1);
 140                 return negateConstraint(array[0]);
 141         case L_XOR: {
 142                 ASSERT( getSizeArrayBoolean(&constraint->inputs)==2);
 143                 Constraint * nleft=negateConstraint(cloneConstraint(array[0]));
 144                 Constraint * nright=negateConstraint(cloneConstraint(array[1]));
 145                 return allocConstraint(OR,
 146                                                                                                          allocConstraint(AND, array[0], nright),
 147                                                                                                          allocConstraint(AND, nleft, array[1]));
 148         }
 149         case L_IMPLIES:
 150                 ASSERT( getSizeArrayBoolean( &constraint->inputs)==2);
 151                 return allocConstraint(IMPLIES, array[0], array[1]);
 152         default:
 153                 model_print("Unhandled case in encodeLogicSATEncoder %u", constraint->op);
 154                 exit(-1);
 155         }
 156 }
 157
 158
 159 Constraint * encodeOrderSATEncoder(SATEncoder *This, BooleanOrder * constraint) {
 160         switch( constraint->order->type){
 161                 case PARTIAL:
 162                         return encodePartialOrderSATEncoder(This, constraint);
 163                 case TOTAL:
 164                         return encodeTotalOrderSATEncoder(This, constraint);
 165                 default:
 166                         ASSERT(0);
 167         }
 168         return NULL;
 169 }
 170
 171 Constraint * getPairConstraint(SATEncoder *This, HashTableBoolConst * table, OrderPair * pair) {
 172         bool negate = false;
 173         OrderPair flipped;
 174         if (pair->first > pair->second) {
 175                 negate=true;
 176                 flipped.first=pair->second;
 177                 flipped.second=pair->first;
 178                 pair = &flipped;        //FIXME: accessing a local variable from outside of the function?
 179         }
 180         Constraint * constraint;
 181         if (!containsBoolConst(table, pair)) {
 182                 constraint = getNewVarSATEncoder(This);
 183                 OrderPair * paircopy = allocOrderPair(pair->first, pair->second, constraint);
 184                 putBoolConst(table, paircopy, paircopy);
 185         } else
 186                 constraint = getBoolConst(table, pair)->constraint;
 187         if (negate)
 188                 return negateConstraint(constraint);
 189         else
 190                 return constraint;
 191
 192 }
 193
 194 Constraint * encodeTotalOrderSATEncoder(SATEncoder *This, BooleanOrder * boolOrder){
 195         ASSERT(boolOrder->order->type == TOTAL);
 196         if(boolOrder->order->boolsToConstraints == NULL){
 197                 initializeOrderHashTable(boolOrder->order);
 198                 return createAllTotalOrderConstraintsSATEncoder(This, boolOrder->order);
 199         }
 200         HashTableBoolConst* boolToConsts = boolOrder->order->boolsToConstraints;
 201         OrderPair pair={boolOrder->first, boolOrder->second, NULL};
 202         Constraint *constraint = getPairConstraint(This, boolToConsts, & pair);
 203         return constraint;
 204 }
 205
 206 Constraint* createAllTotalOrderConstraintsSATEncoder(SATEncoder* This, Order* order){
 207         ASSERT(order->type == TOTAL);
 208         VectorInt* mems = order->set->members;
 209         HashTableBoolConst* table = order->boolsToConstraints;
 210         uint size = getSizeVectorInt(mems);
 211         Constraint* constraints [size*size];
 212         uint csize =0;
 213         for(uint i=0; i<size; i++){
 214                 uint64_t valueI = getVectorInt(mems, i);
 215                 for(uint j=i+1; j<size;j++){
 216                         uint64_t valueJ = getVectorInt(mems, j);
 217                         OrderPair pairIJ = {valueI, valueJ};
 218                         Constraint* constIJ=getPairConstraint(This, table, & pairIJ);
 219                         for(uint k=j+1; k<size; k++){
 220                                 uint64_t valueK = getVectorInt(mems, k);
 221                                 OrderPair pairJK = {valueJ, valueK};
 222                                 OrderPair pairIK = {valueI, valueK};
 223                                 Constraint* constIK = getPairConstraint(This, table, & pairIK);
 224                                 Constraint* constJK = getPairConstraint(This, table, & pairJK);
 225                                 constraints[csize++] = generateTransOrderConstraintSATEncoder(This, constIJ, constJK, constIK);
 226                                 ASSERT(csize < size*size);
 227                         }
 228                 }
 229         }
 230         return allocArrayConstraint(AND, csize, constraints);
 231 }
 232
 233 Constraint* getOrderConstraint(HashTableBoolConst *table, OrderPair *pair){
 234         ASSERT(pair->first!= pair->second);
 235         Constraint* constraint= getBoolConst(table, pair)->constraint;
 236         if(pair->first > pair->second)
 237                 return constraint;
 238         else
 239                 return negateConstraint(constraint);
 240 }
 241
 242 Constraint * generateTransOrderConstraintSATEncoder(SATEncoder *This, Constraint *constIJ,Constraint *constJK,Constraint *constIK){
 243         //FIXME: first we should add the the constraint to the satsolver!
 244         ASSERT(constIJ!= NULL && constJK != NULL && constIK != NULL);
 245         Constraint *carray[] = {constIJ, constJK, negateConstraint(constIK)};
 246         Constraint * loop1= allocArrayConstraint(OR, 3, carray);
 247         Constraint * carray2[] = {negateConstraint(constIJ), negateConstraint(constJK), constIK};
 248         Constraint * loop2= allocArrayConstraint(OR, 3,carray2 );
 249         return allocConstraint(AND, loop1, loop2);
 250 }
 251
 252 Constraint * encodePartialOrderSATEncoder(SATEncoder *This, BooleanOrder * constraint){
 253         // FIXME: we can have this implementation for partial order. Basically,
 254         // we compute the transitivity between two order constraints specified by the client! (also can be used
 255         // when client specify sparse constraints for the total order!)
 256         ASSERT(constraint->order->type == PARTIAL);
 257 /*
 258         HashTableBoolConst* boolToConsts = boolOrder->order->boolsToConstraints;
 259         if( containsBoolConst(boolToConsts, boolOrder) ){
 260                 return getBoolConst(boolToConsts, boolOrder);
 261         } else {
 262                 Constraint* constraint = getNewVarSATEncoder(This);
 263                 putBoolConst(boolToConsts,boolOrder, constraint);
 264                 VectorBoolean* orderConstrs = &boolOrder->order->constraints;
 265                 uint size= getSizeVectorBoolean(orderConstrs);
 266                 for(uint i=0; i<size; i++){
 267                         ASSERT(GETBOOLEANTYPE( getVectorBoolean(orderConstrs, i)) == ORDERCONST );
 268                         BooleanOrder* tmp = (BooleanOrder*)getVectorBoolean(orderConstrs, i);
 269                         BooleanOrder* newBool;
 270                         Constraint* first, *second;
 271                         if(tmp->second==boolOrder->first){
 272                                 newBool = (BooleanOrder*)allocBooleanOrder(tmp->order,tmp->first,boolOrder->second);
 273                                 first = encodeTotalOrderSATEncoder(This, tmp);
 274                                 second = constraint;
 275
 276                         }else if (boolOrder->second == tmp->first){
 277                                 newBool = (BooleanOrder*)allocBooleanOrder(tmp->order,boolOrder->first,tmp->second);
 278                                 first = constraint;
 279                                 second = encodeTotalOrderSATEncoder(This, tmp);
 280                         }else
 281                                 continue;
 282                         Constraint* transConstr= encodeTotalOrderSATEncoder(This, newBool);
 283                         generateTransOrderConstraintSATEncoder(This, first, second, transConstr );
 284                 }
 285                 return constraint;
 286         }
 287 */
 288         return NULL;
 289 }
 290
 291 Constraint * encodePredicateSATEncoder(SATEncoder * This, BooleanPredicate * constraint) {
 292         switch(GETPREDICATETYPE(constraint->predicate) ){
 293                 case TABLEPRED:
 294                         return encodeTablePredicateSATEncoder(This, constraint);
 295                 case OPERATORPRED:
 296                         return encodeOperatorPredicateSATEncoder(This, constraint);
 297                 default:
 298                         ASSERT(0);
 299         }
 300         return NULL;
 301 }
 302
 303 Constraint * encodeTablePredicateSATEncoder(SATEncoder * This, BooleanPredicate * constraint){
 304         switch(constraint->encoding.type){
 305                 case ENUMERATEIMPLICATIONS:
 306                 case ENUMERATEIMPLICATIONSNEGATE:
 307                         return encodeEnumTablePredicateSATEncoder(This, constraint);
 308                 case CIRCUIT:
 309                         ASSERT(0);
 310                         break;
 311                 default:
 312                         ASSERT(0);
 313         }
 314         return NULL;
 315 }
 316
 317 Constraint * encodeEnumTablePredicateSATEncoder(SATEncoder * This, BooleanPredicate * constraint){
 318         VectorTableEntry* entries = &(((PredicateTable*)constraint->predicate)->table->entries);
 319         FunctionEncodingType encType = constraint->encoding.type;
 320         uint size = getSizeVectorTableEntry(entries);
 321         Constraint* constraints[size];
 322         for(uint i=0; i<size; i++){
 323                 TableEntry* entry = getVectorTableEntry(entries, i);
 324                 if(encType==ENUMERATEIMPLICATIONS && entry->output!= true)
 325                         continue;
 326                 else if(encType==ENUMERATEIMPLICATIONSNEGATE && entry->output !=false)
 327                         continue;
 328                 ArrayElement* inputs = &constraint->inputs;
 329                 uint inputNum =getSizeArrayElement(inputs);
 330                 Constraint* carray[inputNum];
 331                 for(uint j=0; j<inputNum; j++){
 332                         Element* el = getArrayElement(inputs, j);
 333                         Constraint* tmpc = getElementValueConstraint(This,el, entry->inputs[j]);
 334                         ASSERT(tmpc!= NULL);
 335                         if( GETELEMENTTYPE(el) == ELEMFUNCRETURN){
 336                                 Constraint* func =encodeFunctionElementSATEncoder(This, (ElementFunction*) el);
 337                                 ASSERT(func!=NULL);
 338                                 carray[j] = allocConstraint(AND, func, tmpc);
 339                         } else {
 340                                 carray[j] = tmpc;
 341                         }
 342                         ASSERT(carray[j]!= NULL);
 343                 }
 344                 constraints[i]=allocArrayConstraint(AND, inputNum, carray);
 345         }
 346         Constraint* result= allocArrayConstraint(OR, size, constraints);
 347         //FIXME: if it didn't match with any entry
 348         return encType==ENUMERATEIMPLICATIONS? result: negateConstraint(result);
 349 }
 350
 351 Constraint * encodeOperatorPredicateSATEncoder(SATEncoder * This, BooleanPredicate * constraint){
 352         switch(constraint->encoding.type){
 353                 case ENUMERATEIMPLICATIONS:
 354                         return encodeEnumOperatorPredicateSATEncoder(This, constraint);
 355                 case CIRCUIT:
 356                         ASSERT(0);
 357                         break;
 358                 default:
 359                         ASSERT(0);
 360         }
 361         return NULL;
 362 }
 363
 364 Constraint * encodeEnumOperatorPredicateSATEncoder(SATEncoder * This, BooleanPredicate * constraint){
 365         ASSERT(GETPREDICATETYPE(constraint->predicate)==OPERATORPRED);
 366         PredicateOperator* predicate = (PredicateOperator*)constraint->predicate;
 367         ASSERT(predicate->op == EQUALS); //For now, we just only support equals
 368         //getting maximum size of in common elements between two sets!
 369         uint size=getSizeVectorInt( getArraySet( &predicate->domains, 0)->members);
 370         uint64_t commonElements [size];
 371         getEqualitySetIntersection(predicate, &size, commonElements);
 372         Constraint*  carray[size];
 373         Element* elem1 = getArrayElement( &constraint->inputs, 0);
 374         Constraint *elemc1 = NULL, *elemc2 = NULL;
 375         if( GETELEMENTTYPE(elem1) == ELEMFUNCRETURN)
 376                 elemc1 = encodeFunctionElementSATEncoder(This, (ElementFunction*) elem1);
 377         Element* elem2 = getArrayElement( &constraint->inputs, 1);
 378         if( GETELEMENTTYPE(elem2) == ELEMFUNCRETURN)
 379                 elemc2 = encodeFunctionElementSATEncoder(This, (ElementFunction*) elem2);
 380         for(uint i=0; i<size; i++){
 381                 Constraint* arg1 = getElementValueConstraint(This, elem1, commonElements[i]);
 382                 ASSERT(arg1!=NULL);
 383                 Constraint* arg2 = getElementValueConstraint(This, elem2, commonElements[i]);
 384                 ASSERT(arg2 != NULL);
 385                 carray[i] =  allocConstraint(AND, arg1, arg2);
 386         }
 387         //FIXME: the case when there is no intersection ....
 388         Constraint* result = allocArrayConstraint(OR, size, carray);
 389         ASSERT(result!= NULL);
 390         if(elemc1!= NULL)
 391                 result = allocConstraint(AND, result, elemc1);
 392         if(elemc2 != NULL)
 393                 result = allocConstraint (AND, result, elemc2);
 394         return result;
 395 }
 396
 397 Constraint* encodeFunctionElementSATEncoder(SATEncoder* encoder, ElementFunction *This){
 398         switch(GETFUNCTIONTYPE(This->function)){
 399                 case TABLEFUNC:
 400                         return encodeTableElementFunctionSATEncoder(encoder, This);
 401                 case OPERATORFUNC:
 402                         return encodeOperatorElementFunctionSATEncoder(encoder, This);
 403                 default:
 404                         ASSERT(0);
 405         }
 406         return NULL;
 407 }
 408
 409 Constraint* encodeTableElementFunctionSATEncoder(SATEncoder* encoder, ElementFunction* This){
 410         switch(getElementFunctionEncoding(This)->type){
 411                 case ENUMERATEIMPLICATIONS:
 412                         return encodeEnumTableElemFunctionSATEncoder(encoder, This);
 413                         break;
 414                 case CIRCUIT:
 415                         ASSERT(0);
 416                         break;
 417                 default:
 418                         ASSERT(0);
 419         }
 420         return NULL;
 421 }
 422
 423 Constraint* encodeOperatorElementFunctionSATEncoder(SATEncoder* encoder, ElementFunction* This){
 424         ASSERT(GETFUNCTIONTYPE(This->function) == OPERATORFUNC);
 425         ASSERT(getSizeArrayElement(&This->inputs)==2 );
 426         Constraint *elemc1=NULL, *elemc2 = NULL;
 427         Element* elem1 = getArrayElement(&This->inputs,0);
 428         Element* elem2 = getArrayElement(&This->inputs,1);
 429         if( GETELEMENTTYPE(elem1) == ELEMFUNCRETURN)
 430                 elemc1 = encodeFunctionElementSATEncoder(encoder, (ElementFunction*) elem1);
 431         if( GETELEMENTTYPE(elem2) == ELEMFUNCRETURN)
 432                 elemc2 = encodeFunctionElementSATEncoder(encoder , (ElementFunction*) elem2);
 433
 434         ElementEncoding* elemEnc1 = getElementEncoding( elem1 );
 435         ElementEncoding* elemEnc2 = getElementEncoding( elem2 );
 436         Constraint* carray[elemEnc1->encArraySize*elemEnc2->encArraySize];
 437         uint size=0;
 438         Constraint* overFlowConstraint = ((BooleanVar*) This->overflowstatus)->var;
 439         for(uint i=0; i<elemEnc1->encArraySize; i++){
 440                 if(isinUseElement(elemEnc1, i)){
 441                         for( uint j=0; j<elemEnc2->encArraySize; j++){
 442                                 if(isinUseElement(elemEnc2, j)){
 443                                         bool isInRange = false;
 444                                         uint64_t result= applyFunctionOperator((FunctionOperator*)This->function,elemEnc1->encodingArray[i],
 445                                                 elemEnc2->encodingArray[j], &isInRange);
 446                                         //FIXME: instead of getElementValueConstraint, it might be useful to have another function
 447                                         // that doesn't iterate over encodingArray and treats more efficient ...
 448                                         Constraint* valConstrIn1 = getElementValueConstraint(encoder, elemEnc1->element, elemEnc1->encodingArray[i]);
 449                                         ASSERT(valConstrIn1 != NULL);
 450                                         Constraint* valConstrIn2 = getElementValueConstraint(encoder, elemEnc2->element, elemEnc2->encodingArray[j]);
 451                                         ASSERT(valConstrIn2 != NULL);
 452                                         Constraint* valConstrOut = getElementValueConstraint(encoder, (Element*) This, result);
 453                                         if(valConstrOut == NULL)
 454                                                 continue; //FIXME:Should talk to brian about it!
 455                                         Constraint* OpConstraint = allocConstraint(IMPLIES,
 456                                                 allocConstraint(AND, valConstrIn1, valConstrIn2) , valConstrOut);
 457                                         switch( ((FunctionOperator*)This->function)->overflowbehavior ){
 458                                                 case IGNORE:
 459                                                         if(isInRange){
 460                                                                 carray[size++] = OpConstraint;
 461                                                         }
 462                                                         break;
 463                                                 case WRAPAROUND:
 464                                                         carray[size++] = OpConstraint;
 465                                                         break;
 466                                                 case FLAGFORCESOVERFLOW:
 467                                                         if(isInRange){
 468                                                                 Constraint* const1 = allocConstraint(IMPLIES,
 469                                                                         allocConstraint(AND, valConstrIn1, valConstrIn2),
 470                                                                         negateConstraint(overFlowConstraint));
 471                                                                 carray[size++] = allocConstraint(AND, const1, OpConstraint);
 472                                                         }
 473                                                         break;
 474                                                 case OVERFLOWSETSFLAG:
 475                                                         if(isInRange){
 476                                                                 carray[size++] = OpConstraint;
 477                                                         } else{
 478                                                                 carray[size++] = allocConstraint(IMPLIES,
 479                                                                         allocConstraint(AND, valConstrIn1, valConstrIn2),
 480                                                                         overFlowConstraint);
 481                                                         }
 482                                                         break;
 483                                                 case FLAGIFFOVERFLOW:
 484                                                         if(isInRange){
 485                                                                 Constraint* const1 = allocConstraint(IMPLIES,
 486                                                                         allocConstraint(AND, valConstrIn1, valConstrIn2),
 487                                                                         negateConstraint(overFlowConstraint));
 488                                                                 carray[size++] = allocConstraint(AND, const1, OpConstraint);
 489                                                         }else{
 490                                                                 carray[size++] = allocConstraint(IMPLIES,
 491                                                                         allocConstraint(AND, valConstrIn1, valConstrIn2),
 492                                                                         overFlowConstraint);
 493                                                         }
 494                                                         break;
 495                                                 case NOOVERFLOW:
 496                                                         if(!isInRange){
 497                                                                 ASSERT(0);
 498                                                         }
 499                                                         carray[size++] = OpConstraint;
 500                                                         break;
 501                                                 default:
 502                                                         ASSERT(0);
 503                                         }
 504
 505                                 }
 506                         }
 507                 }
 508         }
 509         Constraint* result = allocArrayConstraint(OR, size, carray);
 510         if(elemc1 != NULL)
 511                 result = allocConstraint(AND, result, elemc1);
 512         if(elemc2 != NULL)
 513                 result = allocConstraint(AND, result, elemc2);
 514         return result;
 515 }
 516
 517 Constraint* encodeEnumTableElemFunctionSATEncoder(SATEncoder* encoder, ElementFunction* This){
 518         ASSERT(GETFUNCTIONTYPE(This->function)==TABLEFUNC);
 519         ArrayElement* elements= &This->inputs;
 520         Table* table = ((FunctionTable*) (This->function))->table;
 521         uint size = getSizeVectorTableEntry(&table->entries);
 522         Constraint* constraints[size]; //FIXME: should add a space for the case that didn't match any entries
 523         for(uint i=0; i<size; i++){
 524                 TableEntry* entry = getVectorTableEntry(&table->entries, i);
 525                 uint inputNum =getSizeArrayElement(elements);
 526                 Constraint* carray[inputNum];
 527                 for(uint j=0; j<inputNum; j++){
 528                         Element* el= getArrayElement(elements, j);
 529                         carray[j] = getElementValueConstraint(encoder, el, entry->inputs[j]);
 530                         ASSERT(carray[j]!= NULL);
 531                 }
 532                 Constraint* output = getElementValueConstraint(encoder, (Element*)This, entry->output);
 533                 ASSERT(output!= NULL);
 534                 Constraint* row= allocConstraint(IMPLIES, allocArrayConstraint(AND, inputNum, carray), output);
 535                 constraints[i]=row;
 536         }
 537         Constraint* result = allocArrayConstraint(OR, size, constraints);
 538         return result;
 539 }