1 #include "satencoder.h"
9 #include "orderanalysis.h"
10 #include "ordergraph.h"
11 #include "orderedge.h"
13 #include "predicate.h"
14 #include "orderelement.h"
15 #include "orderpairresolver.h"
17 Edge SATEncoder::encodeOrderSATEncoder(BooleanOrder *constraint) {
18 switch ( constraint->order->type) {
20 return encodePartialOrderSATEncoder(constraint);
22 return encodeTotalOrderSATEncoder(constraint);
29 Edge SATEncoder::inferOrderConstraintFromGraph(Order *order, uint64_t _first, uint64_t _second) {
30 if (order->graph != NULL) {
31 OrderGraph *graph = order->graph;
32 OrderNode *first = graph->lookupOrderNodeFromOrderGraph(_first);
33 OrderNode *second = graph->lookupOrderNodeFromOrderGraph(_second);
34 if ((first != NULL) && (second != NULL)) {
35 OrderEdge *edge = graph->lookupOrderEdgeFromOrderGraph(first, second);
39 else if (edge->mustNeg)
42 OrderEdge *invedge = graph->lookupOrderEdgeFromOrderGraph(second, first);
43 if (invedge != NULL) {
46 else if (invedge->mustNeg)
54 Edge SATEncoder::getPairConstraint(Order *order, OrderPair *pair) {
55 Edge gvalue = inferOrderConstraintFromGraph(order, pair->first, pair->second);
56 if (!edgeIsNull(gvalue))
59 HashtableOrderPair *table = order->orderPairTable;
62 if (pair->first < pair->second) {
64 flipped.first = pair->second;
65 flipped.second = pair->first;
69 if (!(table->contains(pair))) {
70 constraint = getNewVarSATEncoder();
71 OrderPair *paircopy = new OrderPair(pair->first, pair->second, constraint);
72 table->put(paircopy, paircopy);
74 constraint = table->get(pair)->constraint;
76 return negate ? constraintNegate(constraint) : constraint;
79 Edge SATEncoder::encodeTotalOrderSATEncoder(BooleanOrder *boolOrder) {
80 ASSERT(boolOrder->order->type == SATC_TOTAL);
81 if (boolOrder->order->orderPairTable == NULL) {
82 //This is pairwised encoding ...
83 boolOrder->order->setOrderResolver(new OrderPairResolver(solver, boolOrder->order));
84 boolOrder->order->initializeOrderHashtable();
85 bool doOptOrderStructure = GETVARTUNABLE(solver->getTuner(), boolOrder->order->type, OPTIMIZEORDERSTRUCTURE, &onoff);
86 if (doOptOrderStructure) {
87 boolOrder->order->graph = buildMustOrderGraph(boolOrder->order);
88 reachMustAnalysis(solver, boolOrder->order->graph, true);
90 createAllTotalOrderConstraintsSATEncoder(boolOrder->order);
92 OrderPair pair(boolOrder->first, boolOrder->second, E_NULL);
93 Edge constraint = getPairConstraint(boolOrder->order, &pair);
98 void SATEncoder::createAllTotalOrderConstraintsSATEncoder(Order *order) {
100 model_print("in total order ...\n");
102 ASSERT(order->type == SATC_TOTAL);
103 Set *set = order->set;
104 uint size = order->set->getSize();
105 for (uint i = 0; i < size; i++) {
106 uint64_t valueI = set->getMemberAt(i);
107 for (uint j = i + 1; j < size; j++) {
108 uint64_t valueJ = set->getMemberAt(j);
109 OrderPair pairIJ(valueI, valueJ, E_NULL);
110 Edge constIJ = getPairConstraint(order, &pairIJ);
111 for (uint k = j + 1; k < size; k++) {
112 uint64_t valueK = set->getMemberAt(k);
113 OrderPair pairJK(valueJ, valueK, E_NULL);
114 OrderPair pairIK(valueI, valueK, E_NULL);
115 Edge constIK = getPairConstraint(order, &pairIK);
116 Edge constJK = getPairConstraint(order, &pairJK);
117 addConstraintCNF(cnf, generateTransOrderConstraintSATEncoder(constIJ, constJK, constIK));
123 Edge getOrderConstraint(HashtableOrderPair *table, OrderPair *pair) {
124 ASSERT(pair->first != pair->second);
127 if (pair->first < pair->second) {
129 flipped.first = pair->second;
130 flipped.second = pair->first;
133 if (!table->contains(pair)) {
136 Edge constraint = table->get(pair)->constraint;
137 ASSERT(!edgeIsNull(constraint));
138 return negate ? constraintNegate(constraint) : constraint;
141 Edge SATEncoder::generateTransOrderConstraintSATEncoder(Edge constIJ,Edge constJK,Edge constIK) {
142 Edge carray[] = {constIJ, constJK, constraintNegate(constIK)};
143 Edge loop1 = constraintOR(cnf, 3, carray);
144 Edge carray2[] = {constraintNegate(constIJ), constraintNegate(constJK), constIK};
145 Edge loop2 = constraintOR(cnf, 3, carray2 );
146 return constraintAND2(cnf, loop1, loop2);
149 Edge SATEncoder::encodePartialOrderSATEncoder(BooleanOrder *constraint) {
150 ASSERT(constraint->order->type == SATC_PARTIAL);