1 #include "satencoder.h"
9 #include "orderanalysis.h"
10 #include "ordergraph.h"
11 #include "orderedge.h"
13 #include "predicate.h"
14 #include "orderelement.h"
16 Edge SATEncoder::encodeOrderSATEncoder(BooleanOrder *constraint) {
17 switch ( constraint->order->type) {
19 return encodePartialOrderSATEncoder(constraint);
21 return encodeTotalOrderSATEncoder(constraint);
28 Edge SATEncoder::inferOrderConstraintFromGraph(Order *order, uint64_t _first, uint64_t _second) {
29 if (order->graph != NULL) {
30 OrderGraph *graph = order->graph;
31 OrderNode *first = graph->lookupOrderNodeFromOrderGraph(_first);
32 OrderNode *second = graph->lookupOrderNodeFromOrderGraph(_second);
33 if ((first != NULL) && (second != NULL)) {
34 OrderEdge *edge = graph->lookupOrderEdgeFromOrderGraph(first, second);
38 else if (edge->mustNeg)
41 OrderEdge *invedge = graph->lookupOrderEdgeFromOrderGraph(second, first);
42 if (invedge != NULL) {
45 else if (invedge->mustNeg)
53 Edge SATEncoder::getPairConstraint(Order *order, OrderPair *pair) {
54 Edge gvalue = inferOrderConstraintFromGraph(order, pair->first, pair->second);
55 if (!edgeIsNull(gvalue))
58 HashTableOrderPair *table = order->orderPairTable;
61 if (pair->first < pair->second) {
63 flipped.first = pair->second;
64 flipped.second = pair->first;
68 if (!(table->contains(pair))) {
69 constraint = getNewVarSATEncoder();
70 OrderPair *paircopy = new OrderPair(pair->first, pair->second, constraint);
71 table->put(paircopy, paircopy);
73 constraint = table->get(pair)->constraint;
75 return negate ? constraintNegate(constraint) : constraint;
78 Edge SATEncoder::encodeTotalOrderSATEncoder(BooleanOrder *boolOrder) {
79 ASSERT(boolOrder->order->type == TOTAL);
80 if (boolOrder->order->orderPairTable == NULL) {
81 boolOrder->order->initializeOrderHashTable();
82 bool doOptOrderStructure = GETVARTUNABLE(solver->getTuner(), boolOrder->order->type, OPTIMIZEORDERSTRUCTURE, &onoff);
83 if (doOptOrderStructure) {
84 boolOrder->order->graph = buildMustOrderGraph(boolOrder->order);
85 reachMustAnalysis(solver, boolOrder->order->graph, true);
87 createAllTotalOrderConstraintsSATEncoder(boolOrder->order);
89 OrderPair pair(boolOrder->first, boolOrder->second, E_NULL);
90 Edge constraint = getPairConstraint(boolOrder->order, &pair);
95 void SATEncoder::createAllTotalOrderConstraintsSATEncoder(Order *order) {
97 model_print("in total order ...\n");
99 ASSERT(order->type == TOTAL);
100 Vector<uint64_t> *mems = order->set->members;
101 uint size = mems->getSize();
102 for (uint i = 0; i < size; i++) {
103 uint64_t valueI = mems->get(i);
104 for (uint j = i + 1; j < size; j++) {
105 uint64_t valueJ = mems->get(j);
106 OrderPair pairIJ(valueI, valueJ, E_NULL);
107 Edge constIJ = getPairConstraint(order, &pairIJ);
108 for (uint k = j + 1; k < size; k++) {
109 uint64_t valueK = mems->get(k);
110 OrderPair pairJK(valueJ, valueK, E_NULL);
111 OrderPair pairIK(valueI, valueK, E_NULL);
112 Edge constIK = getPairConstraint(order, &pairIK);
113 Edge constJK = getPairConstraint(order, &pairJK);
114 addConstraintCNF(cnf, generateTransOrderConstraintSATEncoder(constIJ, constJK, constIK));
120 Edge getOrderConstraint(HashTableOrderPair *table, OrderPair *pair) {
121 ASSERT(pair->first != pair->second);
124 if (pair->first < pair->second) {
126 flipped.first = pair->second;
127 flipped.second = pair->first;
130 if (!table->contains(pair)) {
133 Edge constraint = table->get(pair)->constraint;
134 ASSERT(!edgeIsNull(constraint));
135 return negate ? constraintNegate(constraint) : constraint;
138 Edge SATEncoder::generateTransOrderConstraintSATEncoder(Edge constIJ,Edge constJK,Edge constIK) {
139 Edge carray[] = {constIJ, constJK, constraintNegate(constIK)};
140 Edge loop1 = constraintOR(cnf, 3, carray);
141 Edge carray2[] = {constraintNegate(constIJ), constraintNegate(constJK), constIK};
142 Edge loop2 = constraintOR(cnf, 3, carray2 );
143 return constraintAND2(cnf, loop1, loop2);
146 Edge SATEncoder::encodePartialOrderSATEncoder(BooleanOrder *constraint) {
147 ASSERT(constraint->order->type == PARTIAL);