1 #include "satencoder.h"
9 #include "orderencoder.h"
10 #include "ordergraph.h"
11 #include "orderedge.h"
13 Edge encodeOrderSATEncoder(SATEncoder *This, BooleanOrder *constraint) {
14 switch ( constraint->order->type) {
16 return encodePartialOrderSATEncoder(This, constraint);
18 return encodeTotalOrderSATEncoder(This, constraint);
25 Edge getPairConstraint(SATEncoder *This, Order *order, OrderPair *pair) {
26 if (order->graph != NULL) {
27 OrderGraph *graph=order->graph;
28 OrderNode *first=lookupOrderNodeFromOrderGraph(graph, pair->first);
29 OrderNode *second=lookupOrderNodeFromOrderGraph(graph, pair->second);
30 if ((first != NULL) && (second != NULL)) {
31 OrderEdge *edge=lookupOrderEdgeFromOrderGraph(graph, first, second);
35 else if (edge->mustNeg)
38 OrderEdge *invedge=getOrderEdgeFromOrderGraph(graph, first, second);
39 if (invedge != NULL) {
42 else if (invedge->mustNeg)
47 HashTableOrderPair *table = order->orderPairTable;
50 if (pair->first < pair->second) {
52 flipped.first = pair->second;
53 flipped.second = pair->first;
57 if (!containsOrderPair(table, pair)) {
58 constraint = getNewVarSATEncoder(This);
59 OrderPair *paircopy = allocOrderPair(pair->first, pair->second, constraint);
60 putOrderPair(table, paircopy, paircopy);
62 constraint = getOrderPair(table, pair)->constraint;
64 return negate ? constraintNegate(constraint) : constraint;
67 Edge encodeTotalOrderSATEncoder(SATEncoder *This, BooleanOrder *boolOrder) {
68 ASSERT(boolOrder->order->type == TOTAL);
69 if (boolOrder->order->orderPairTable == NULL) {
70 initializeOrderHashTable(boolOrder->order);
71 bool doOptOrderStructure=GETVARTUNABLE(This->solver->tuner, boolOrder->order->type, OPTIMIZEORDERSTRUCTURE, &onoff);
72 if (doOptOrderStructure) {
73 boolOrder->order->graph = buildMustOrderGraph(boolOrder->order);
74 reachMustAnalysis(This->solver, boolOrder->order->graph, true);
76 createAllTotalOrderConstraintsSATEncoder(This, boolOrder->order);
78 OrderPair pair = {boolOrder->first, boolOrder->second, E_NULL};
79 Edge constraint = getPairConstraint(This, boolOrder->order, &pair);
84 void createAllTotalOrderConstraintsSATEncoder(SATEncoder *This, Order *order) {
86 model_print("in total order ...\n");
88 ASSERT(order->type == TOTAL);
89 VectorInt *mems = order->set->members;
90 uint size = getSizeVectorInt(mems);
91 for (uint i = 0; i < size; i++) {
92 uint64_t valueI = getVectorInt(mems, i);
93 for (uint j = i + 1; j < size; j++) {
94 uint64_t valueJ = getVectorInt(mems, j);
95 OrderPair pairIJ = {valueI, valueJ};
96 Edge constIJ = getPairConstraint(This, order, &pairIJ);
97 for (uint k = j + 1; k < size; k++) {
98 uint64_t valueK = getVectorInt(mems, k);
99 OrderPair pairJK = {valueJ, valueK};
100 OrderPair pairIK = {valueI, valueK};
101 Edge constIK = getPairConstraint(This, order, &pairIK);
102 Edge constJK = getPairConstraint(This, order, &pairJK);
103 addConstraintCNF(This->cnf, generateTransOrderConstraintSATEncoder(This, constIJ, constJK, constIK));
109 Edge getOrderConstraint(HashTableOrderPair *table, OrderPair *pair) {
110 ASSERT(pair->first != pair->second);
113 if (pair->first < pair->second) {
115 flipped.first = pair->second;
116 flipped.second = pair->first;
119 if (!containsOrderPair(table, pair)) {
122 Edge constraint = getOrderPair(table, pair)->constraint;
123 ASSERT(!edgeIsNull(constraint));
124 return negate ? constraintNegate(constraint) : constraint;
127 Edge generateTransOrderConstraintSATEncoder(SATEncoder *This, Edge constIJ,Edge constJK,Edge constIK) {
128 Edge carray[] = {constIJ, constJK, constraintNegate(constIK)};
129 Edge loop1 = constraintOR(This->cnf, 3, carray);
130 Edge carray2[] = {constraintNegate(constIJ), constraintNegate(constJK), constIK};
131 Edge loop2 = constraintOR(This->cnf, 3, carray2 );
132 return constraintAND2(This->cnf, loop1, loop2);
135 Edge encodePartialOrderSATEncoder(SATEncoder *This, BooleanOrder *constraint) {
136 ASSERT(constraint->order->type == PARTIAL);