+Edge encodeTotalOrderSATEncoder(SATEncoder *This, BooleanOrder * boolOrder){
+ ASSERT(boolOrder->order->type == TOTAL);
+ if(boolOrder->order->boolsToConstraints == NULL){
+ initializeOrderHashTable(boolOrder->order);
+ createAllTotalOrderConstraintsSATEncoder(This, boolOrder->order);
+ }
+ HashTableBoolConst* boolToConsts = boolOrder->order->boolsToConstraints;
+ OrderPair pair={boolOrder->first, boolOrder->second, E_NULL};
+ Edge constraint = getPairConstraint(This, boolToConsts, & pair);
+ return constraint;
+}
+
+void createAllTotalOrderConstraintsSATEncoder(SATEncoder* This, Order* order){
+ ASSERT(order->type == TOTAL);
+ VectorInt* mems = order->set->members;
+ HashTableBoolConst* table = order->boolsToConstraints;
+ uint size = getSizeVectorInt(mems);
+ uint csize =0;
+ for(uint i=0; i<size; i++){
+ uint64_t valueI = getVectorInt(mems, i);
+ for(uint j=i+1; j<size;j++){
+ uint64_t valueJ = getVectorInt(mems, j);
+ OrderPair pairIJ = {valueI, valueJ};
+ Edge constIJ=getPairConstraint(This, table, & pairIJ);
+ for(uint k=j+1; k<size; k++){
+ uint64_t valueK = getVectorInt(mems, k);
+ OrderPair pairJK = {valueJ, valueK};
+ OrderPair pairIK = {valueI, valueK};
+ Edge constIK = getPairConstraint(This, table, & pairIK);
+ Edge constJK = getPairConstraint(This, table, & pairJK);
+ addConstraint(This->cnf, generateTransOrderConstraintSATEncoder(This, constIJ, constJK, constIK));
+ }
+ }
+ }
+}
+
+Edge getOrderConstraint(HashTableBoolConst *table, OrderPair *pair){
+ ASSERT(pair->first!= pair->second);
+ Edge constraint = getBoolConst(table, pair)->constraint;
+ if(pair->first > pair->second)
+ return constraint;
+ else
+ return constraintNegate(constraint);
+}
+
+Edge generateTransOrderConstraintSATEncoder(SATEncoder *This, Edge constIJ,Edge constJK,Edge constIK){
+ Edge carray[] = {constIJ, constJK, constraintNegate(constIK)};
+ Edge loop1= constraintOR(This->cnf, 3, carray);
+ Edge carray2[] = {constraintNegate(constIJ), constraintNegate(constJK), constIK};
+ Edge loop2= constraintOR(This->cnf, 3, carray2 );
+ return constraintAND2(This->cnf, loop1, loop2);
+}
+
+Edge encodePartialOrderSATEncoder(SATEncoder *This, BooleanOrder * constraint){
+ // FIXME: we can have this implementation for partial order. Basically,
+ // we compute the transitivity between two order constraints specified by the client! (also can be used
+ // when client specify sparse constraints for the total order!)
+ ASSERT(constraint->order->type == PARTIAL);
+/*
+ HashTableBoolConst* boolToConsts = boolOrder->order->boolsToConstraints;
+ if( containsBoolConst(boolToConsts, boolOrder) ){
+ return getBoolConst(boolToConsts, boolOrder);
+ } else {
+ Edge constraint = getNewVarSATEncoder(This);
+ putBoolConst(boolToConsts,boolOrder, constraint);
+ VectorBoolean* orderConstrs = &boolOrder->order->constraints;
+ uint size= getSizeVectorBoolean(orderConstrs);
+ for(uint i=0; i<size; i++){
+ ASSERT(GETBOOLEANTYPE( getVectorBoolean(orderConstrs, i)) == ORDERCONST );
+ BooleanOrder* tmp = (BooleanOrder*)getVectorBoolean(orderConstrs, i);
+ BooleanOrder* newBool;
+ Edge first, second;
+ if(tmp->second==boolOrder->first){
+ newBool = (BooleanOrder*)allocBooleanOrder(tmp->order,tmp->first,boolOrder->second);
+ first = encodeTotalOrderSATEncoder(This, tmp);
+ second = constraint;
+
+ }else if (boolOrder->second == tmp->first){
+ newBool = (BooleanOrder*)allocBooleanOrder(tmp->order,boolOrder->first,tmp->second);
+ first = constraint;
+ second = encodeTotalOrderSATEncoder(This, tmp);
+ }else
+ continue;
+ Edge transConstr= encodeTotalOrderSATEncoder(This, newBool);
+ generateTransOrderConstraintSATEncoder(This, first, second, transConstr );
+ }
+ return constraint;
+ }
+*/
+ return E_BOGUS;
+}
+
+Edge encodePredicateSATEncoder(SATEncoder * This, BooleanPredicate * constraint) {
+ switch(GETPREDICATETYPE(constraint->predicate) ){
+ case TABLEPRED:
+ return encodeTablePredicateSATEncoder(This, constraint);
+ case OPERATORPRED:
+ return encodeOperatorPredicateSATEncoder(This, constraint);
+ default:
+ ASSERT(0);
+ }
+ return E_BOGUS;
+}
+
+Edge encodeTablePredicateSATEncoder(SATEncoder * This, BooleanPredicate * constraint){
+ switch(constraint->encoding.type){
+ case ENUMERATEIMPLICATIONS:
+ case ENUMERATEIMPLICATIONSNEGATE:
+ return encodeEnumTablePredicateSATEncoder(This, constraint);
+ case CIRCUIT:
+ ASSERT(0);
+ break;
+ default:
+ ASSERT(0);
+ }
+ return E_BOGUS;
+}
+
+Edge encodeEnumTablePredicateSATEncoder(SATEncoder * This, BooleanPredicate * constraint){
+ VectorTableEntry* entries = &(((PredicateTable*)constraint->predicate)->table->entries);
+ FunctionEncodingType encType = constraint->encoding.type;
+ uint size = getSizeVectorTableEntry(entries);
+ Edge constraints[size];
+ for(uint i=0; i<size; i++){
+ TableEntry* entry = getVectorTableEntry(entries, i);
+ if(encType==ENUMERATEIMPLICATIONS && entry->output!= true)
+ continue;
+ else if(encType==ENUMERATEIMPLICATIONSNEGATE && entry->output !=false)
+ continue;
+ ArrayElement* inputs = &constraint->inputs;
+ uint inputNum =getSizeArrayElement(inputs);
+ Edge carray[inputNum];
+ for(uint j=0; j<inputNum; j++){
+ Element* el = getArrayElement(inputs, j);
+ Edge tmpc = getElementValueConstraint(This, el, entry->inputs[j]);
+ if( GETELEMENTTYPE(el) == ELEMFUNCRETURN){
+ Edge func =encodeFunctionElementSATEncoder(This, (ElementFunction*) el);
+ carray[j] = constraintAND2(This->cnf, func, tmpc);
+ } else {
+ carray[j] = tmpc;
+ }
+ }
+ constraints[i]=constraintAND(This->cnf, inputNum, carray);
+ }
+ Edge result=constraintOR(This->cnf, size, constraints);
+ //FIXME: if it didn't match with any entry
+ return encType==ENUMERATEIMPLICATIONS? result: constraintNegate(result);
+}
+
+Edge encodeOperatorPredicateSATEncoder(SATEncoder * This, BooleanPredicate * constraint){
+ switch(constraint->encoding.type){
+ case ENUMERATEIMPLICATIONS:
+ return encodeEnumOperatorPredicateSATEncoder(This, constraint);
+ case CIRCUIT:
+ ASSERT(0);
+ break;
+ default:
+ ASSERT(0);
+ }
+ return E_BOGUS;
+}
+
+Edge encodeEnumOperatorPredicateSATEncoder(SATEncoder * This, BooleanPredicate * constraint){
+ ASSERT(GETPREDICATETYPE(constraint->predicate)==OPERATORPRED);
+ PredicateOperator* predicate = (PredicateOperator*)constraint->predicate;
+ ASSERT(predicate->op == EQUALS); //For now, we just only support equals
+ //getting maximum size of in common elements between two sets!
+ uint size=getSizeVectorInt( getArraySet( &predicate->domains, 0)->members);
+ uint64_t commonElements [size];
+ getEqualitySetIntersection(predicate, &size, commonElements);
+ Edge carray[size];
+ Element* elem1 = getArrayElement( &constraint->inputs, 0);
+ Edge elemc1 = E_NULL, elemc2 = E_NULL;
+ if( GETELEMENTTYPE(elem1) == ELEMFUNCRETURN)
+ elemc1 = encodeFunctionElementSATEncoder(This, (ElementFunction*) elem1);
+ Element* elem2 = getArrayElement( &constraint->inputs, 1);
+ if( GETELEMENTTYPE(elem2) == ELEMFUNCRETURN)
+ elemc2 = encodeFunctionElementSATEncoder(This, (ElementFunction*) elem2);
+ for(uint i=0; i<size; i++){
+ Edge arg1 = getElementValueConstraint(This, elem1, commonElements[i]);
+ Edge arg2 = getElementValueConstraint(This, elem2, commonElements[i]);
+ carray[i] = constraintAND2(This->cnf, arg1, arg2);
+ }
+ //FIXME: the case when there is no intersection ....
+ Edge result = constraintOR(This->cnf, size, carray);
+ if (!edgeIsNull(elemc1))
+ result = constraintAND2(This->cnf, result, elemc1);
+ if (!edgeIsNull(elemc2))
+ result = constraintAND2(This->cnf, result, elemc2);
+ return result;
+}
+
+Edge encodeFunctionElementSATEncoder(SATEncoder* encoder, ElementFunction *This){