1 #include "satencoder.h"
8 Edge encodeOrderSATEncoder(SATEncoder *This, BooleanOrder * constraint) {
9 switch( constraint->order->type){
11 return encodePartialOrderSATEncoder(This, constraint);
13 return encodeTotalOrderSATEncoder(This, constraint);
20 Edge getPairConstraint(SATEncoder *This, HashTableOrderPair * table, OrderPair * pair) {
23 if (pair->first > pair->second) {
25 flipped.first=pair->second;
26 flipped.second=pair->first;
30 if (!containsOrderPair(table, pair)) {
31 constraint = getNewVarSATEncoder(This);
32 OrderPair * paircopy = allocOrderPair(pair->first, pair->second, constraint);
33 putOrderPair(table, paircopy, paircopy);
35 constraint = getOrderPair(table, pair)->constraint;
37 return negate ? constraintNegate(constraint) : constraint;
40 Edge encodeTotalOrderSATEncoder(SATEncoder *This, BooleanOrder * boolOrder) {
41 ASSERT(boolOrder->order->type == TOTAL);
42 if(boolOrder->order->orderPairTable == NULL) {
43 initializeOrderHashTable(boolOrder->order);
44 createAllTotalOrderConstraintsSATEncoder(This, boolOrder->order);
46 HashTableOrderPair* orderPairTable = boolOrder->order->orderPairTable;
47 OrderPair pair={boolOrder->first, boolOrder->second, E_NULL};
48 Edge constraint = getPairConstraint(This, orderPairTable, & pair);
53 void createAllTotalOrderConstraintsSATEncoder(SATEncoder* This, Order* order){
55 model_print("in total order ...\n");
57 ASSERT(order->type == TOTAL);
58 VectorInt* mems = order->set->members;
59 HashTableOrderPair* table = order->orderPairTable;
60 uint size = getSizeVectorInt(mems);
62 for(uint i=0; i<size; i++){
63 uint64_t valueI = getVectorInt(mems, i);
64 for(uint j=i+1; j<size;j++){
65 uint64_t valueJ = getVectorInt(mems, j);
66 OrderPair pairIJ = {valueI, valueJ};
67 Edge constIJ=getPairConstraint(This, table, & pairIJ);
68 for(uint k=j+1; k<size; k++){
69 uint64_t valueK = getVectorInt(mems, k);
70 OrderPair pairJK = {valueJ, valueK};
71 OrderPair pairIK = {valueI, valueK};
72 Edge constIK = getPairConstraint(This, table, & pairIK);
73 Edge constJK = getPairConstraint(This, table, & pairJK);
74 addConstraintCNF(This->cnf, generateTransOrderConstraintSATEncoder(This, constIJ, constJK, constIK));
80 Edge getOrderConstraint(HashTableOrderPair *table, OrderPair *pair){
81 ASSERT(pair->first!= pair->second);
82 OrderPair* value = getOrderPair(table, pair);
85 Edge constraint = value->constraint;
86 model_print("Constraint:\n");
88 model_print("\n***********\n");
89 if(pair->first > pair->second || edgeIsNull(constraint))
92 return constraintNegate(constraint);
95 Edge generateTransOrderConstraintSATEncoder(SATEncoder *This, Edge constIJ,Edge constJK,Edge constIK){
96 Edge carray[] = {constIJ, constJK, constraintNegate(constIK)};
97 Edge loop1= constraintOR(This->cnf, 3, carray);
98 Edge carray2[] = {constraintNegate(constIJ), constraintNegate(constJK), constIK};
99 Edge loop2= constraintOR(This->cnf, 3, carray2 );
100 return constraintAND2(This->cnf, loop1, loop2);
103 Edge encodePartialOrderSATEncoder(SATEncoder *This, BooleanOrder * constraint){
104 ASSERT(constraint->order->type == PARTIAL);