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->getOrderPairTable();
62 if (pair->first < pair->second) {
64 flipped.first = pair->second;
65 flipped.second = pair->first;
69 if (!(table->contains(pair))) {
70 tmp = new OrderPair(pair->first, pair->second, getNewVarSATEncoder());
73 tmp = table->get(pair);
75 return negate ? tmp->getNegatedConstraint() : tmp->getConstraint();
78 Edge SATEncoder::getPartialPairConstraint(Order *order, OrderPair *pair) {
79 Edge gvalue = inferOrderConstraintFromGraph(order, pair->first, pair->second);
80 if (!edgeIsNull(gvalue))
83 HashtableOrderPair *table = order->getOrderPairTable();
86 if (!(table->contains(pair))) {
87 Edge constraint = getNewVarSATEncoder();
88 tmp = new OrderPair(pair->first, pair->second, constraint);
90 Edge constraint2 = getNewVarSATEncoder();
91 OrderPair *swap = new OrderPair(pair->second, pair->first, constraint2);
92 table->put(swap, swap);
93 addConstraintCNF(cnf, constraintNegate(constraintAND2(cnf, constraint, constraint2)));
95 tmp = table->get(pair);
97 return tmp->getConstraint();
100 Edge SATEncoder::encodeTotalOrderSATEncoder(BooleanOrder *boolOrder) {
101 ASSERT(boolOrder->order->type == SATC_TOTAL);
102 if (boolOrder->order->encoding.resolver == NULL) {
103 //This is pairwised encoding ...
104 boolOrder->order->setOrderResolver(new OrderPairResolver(solver, boolOrder->order));
105 bool doOptOrderStructure = GETVARTUNABLE(solver->getTuner(), boolOrder->order->type, OPTIMIZEORDERSTRUCTURE, &onoff);
106 if (doOptOrderStructure) {
107 ASSERT(boolOrder->order->graph == NULL);
108 boolOrder->order->graph = buildMustOrderGraph(boolOrder->order);
109 reachMustAnalysis(solver, boolOrder->order->graph, true);
111 if (GETVARTUNABLE(solver->getTuner(), order->type, DECOMPOSEORDER, &onoff) == 0)
112 createAllTotalOrderConstraintsSATEncoderSparse(boolOrder->order);
114 createAllTotalOrderConstraintsSATEncoder(boolOrder->order);
116 OrderPair pair(boolOrder->first, boolOrder->second, E_NULL);
117 Edge constraint = getPairConstraint(boolOrder->order, &pair);
122 void SATEncoder::createAllTotalOrderConstraintsSATEncoder(Order *order) {
124 model_print("in total order ...\n");
126 ASSERT(order->type == SATC_TOTAL);
127 Set *set = order->set;
128 uint size = order->set->getSize();
129 for (uint i = 0; i < size; i++) {
130 uint64_t valueI = set->getElement(i);
131 for (uint j = i + 1; j < size; j++) {
132 uint64_t valueJ = set->getElement(j);
133 OrderPair pairIJ(valueI, valueJ, E_NULL);
134 Edge constIJ = getPairConstraint(order, &pairIJ);
135 for (uint k = j + 1; k < size; k++) {
136 uint64_t valueK = set->getElement(k);
137 OrderPair pairJK(valueJ, valueK, E_NULL);
138 OrderPair pairIK(valueI, valueK, E_NULL);
139 Edge constIK = getPairConstraint(order, &pairIK);
140 Edge constJK = getPairConstraint(order, &pairJK);
141 addConstraintCNF(cnf, generateTransOrderConstraintSATEncoder(constIJ, constJK, constIK));
147 Edge SATEncoder::generateTransOrderConstraintSATEncoder(Edge constIJ,Edge constJK,Edge constIK) {
148 Edge carray[] = {constIJ, constJK, constraintNegate(constIK)};
149 Edge loop1 = constraintOR(cnf, 3, carray);
150 Edge carray2[] = {constraintNegate(constIJ), constraintNegate(constJK), constIK};
151 Edge loop2 = constraintOR(cnf, 3, carray2 );
152 return constraintAND2(cnf, loop1, loop2);
155 Edge SATEncoder::generatePartialOrderConstraintsSATEncoder(Edge ij,Edge ji, Edge jk, Edge kj,Edge ik, Edge ki) {
156 Edge uoIJ = constraintAND2(cnf, constraintNegate(ij), constraintNegate(ji));
157 Edge uoJK = constraintAND2(cnf, constraintNegate(jk), constraintNegate(kj));
158 Edge uoIK = constraintAND2(cnf, constraintNegate(ik), constraintNegate(ki));
160 Edge t1[] = {ij, jk, ik};
161 Edge t2[] = {ji, jk, ik};
162 Edge t3[] = {ij, kj, ki};
163 Edge t4[] = {ij, kj, ik};
164 Edge t5[] = {ji, jk, ki};
165 Edge t6[] = {ji, kj, ki};
166 Edge ct1 = constraintAND(cnf, 3, t1);
167 Edge ct2 = constraintAND(cnf, 3, t2);
168 Edge ct3 = constraintAND(cnf, 3, t3);
169 Edge ct4 = constraintAND(cnf, 3, t4);
170 Edge ct5 = constraintAND(cnf, 3, t5);
171 Edge ct6 = constraintAND(cnf, 3, t6);
173 Edge p1[] = {uoIJ, jk, ik};
174 Edge p2[] = {ij, kj, uoIK};
175 Edge p3[] = {ji, uoJK, ki};
176 Edge p4[] = {uoIJ, kj, ki};
177 Edge p5[] = {ji, jk, uoIK};
178 Edge p6[] = {ij, uoJK, ik};
179 Edge cp1 = constraintAND(cnf, 3, p1);
180 Edge cp2 = constraintAND(cnf, 3, p2);
181 Edge cp3 = constraintAND(cnf, 3, p3);
182 Edge cp4 = constraintAND(cnf, 3, p4);
183 Edge cp5 = constraintAND(cnf, 3, p5);
184 Edge cp6 = constraintAND(cnf, 3, p6);
186 Edge o1[] = {uoIJ, uoJK, ik};
187 Edge o2[] = {ij, uoJK, uoIK};
188 Edge o3[] = {uoIK, jk, uoIK};
189 Edge o4[] = {ji, uoJK, uoIK};
190 Edge o5[] = {uoIJ, uoJK, ki};
191 Edge o6[] = {uoIJ, kj, uoIK};
192 Edge co1 = constraintAND(cnf, 3, o1);
193 Edge co2 = constraintAND(cnf, 3, o2);
194 Edge co3 = constraintAND(cnf, 3, o3);
195 Edge co4 = constraintAND(cnf, 3, o4);
196 Edge co5 = constraintAND(cnf, 3, o5);
197 Edge co6 = constraintAND(cnf, 3, o6);
199 Edge unorder [] = {uoIJ, uoJK, uoIK};
200 Edge cunorder = constraintAND(cnf, 3, unorder);
203 Edge res[] = {ct1,ct2,ct3,ct4,ct5,ct6,
204 cp1,cp2,cp3,cp4,cp5,cp6,
205 co1,co2,co3,co4,co5,co6,
207 return constraintOR(cnf, 19, res);
210 Edge SATEncoder::encodePartialOrderSATEncoder(BooleanOrder *boolOrder) {
211 ASSERT(boolOrder->order->type == SATC_PARTIAL);
212 if (boolOrder->order->encoding.resolver == NULL) {
213 //This is pairwised encoding ...
214 boolOrder->order->setOrderResolver(new OrderPairResolver(solver, boolOrder->order));
215 bool doOptOrderStructure = GETVARTUNABLE(solver->getTuner(), boolOrder->order->type, OPTIMIZEORDERSTRUCTURE, &onoff);
216 if (doOptOrderStructure) {
217 boolOrder->order->graph = buildMustOrderGraph(boolOrder->order);
218 reachMustAnalysis(solver, boolOrder->order->graph, true);
220 if (GETVARTUNABLE(solver->getTuner(), order->type, DECOMPOSEORDER, &onoff) == 0)
221 createAllPartialOrderConstraintsSATEncoderSparse(boolOrder->order);
223 createAllPartialOrderConstraintsSATEncoder(boolOrder->order);
225 OrderPair pair(boolOrder->first, boolOrder->second, E_NULL);
226 Edge constraint = getPartialPairConstraint(boolOrder->order, &pair);
231 void SATEncoder::createAllPartialOrderConstraintsSATEncoder(Order *order) {
233 model_print("in partial order ...\n");
235 ASSERT(order->type == SATC_TOTAL);
236 Set *set = order->set;
237 uint size = order->set->getSize();
238 for (uint i = 0; i < size; i++) {
239 uint64_t valueI = set->getElement(i);
240 for (uint j = i + 1; j < size; j++) {
241 uint64_t valueJ = set->getElement(j);
242 OrderPair pairIJ(valueI, valueJ, E_NULL);
243 OrderPair pairJI(valueJ, valueI, E_NULL);
244 Edge constIJ = getPartialPairConstraint(order, &pairIJ);
245 Edge constJI = getPartialPairConstraint(order, &pairJI);
246 for (uint k = j + 1; k < size; k++) {
247 uint64_t valueK = set->getElement(k);
248 OrderPair pairJK(valueJ, valueK, E_NULL);
249 OrderPair pairIK(valueI, valueK, E_NULL);
250 Edge constIK = getPartialPairConstraint(order, &pairIK);
251 Edge constJK = getPartialPairConstraint(order, &pairJK);
252 OrderPair pairKJ(valueK, valueJ, E_NULL);
253 OrderPair pairKI(valueK, valueI, E_NULL);
254 Edge constKI = getPartialPairConstraint(order, &pairKI);
255 Edge constKJ = getPartialPairConstraint(order, &pairKJ);
256 addConstraintCNF(cnf, generatePartialOrderConstraintsSATEncoder(constIJ, constJI,
257 constJK, constKJ, constIK, constKI));
263 void SATEncoder::createAllTotalOrderConstraintsSATEncoderSparse(Order *order) {
265 model_print("in total order ...\n");
267 ASSERT(order->type == SATC_TOTAL);
268 SetIterator64Int *iti = order->getUsedIterator();
269 while (iti->hasNext()) {
270 uint64_t valueI = iti->next();
271 SetIterator64Int *itj = new SetIterator64Int(iti);
272 while (itj->hasNext()) {
273 uint64_t valueJ = itj->next();
274 OrderPair pairIJ(valueI, valueJ, E_NULL);
275 Edge constIJ = getPairConstraint(order, &pairIJ);
276 SetIterator64Int *itk = new SetIterator64Int(itj);
277 while (itk->hasNext()) {
278 uint64_t valueK = itk->next();
279 OrderPair pairJK(valueJ, valueK, E_NULL);
280 OrderPair pairIK(valueI, valueK, E_NULL);
281 Edge constIK = getPairConstraint(order, &pairIK);
282 Edge constJK = getPairConstraint(order, &pairJK);
283 addConstraintCNF(cnf, generateTransOrderConstraintSATEncoder(constIJ, constJK, constIK));
289 void SATEncoder::createAllPartialOrderConstraintsSATEncoderSparse(Order *order) {
291 model_print("in partial order ...\n");
293 ASSERT(order->type == SATC_TOTAL);
294 SetIterator64Int *iti = order->getUsedIterator();
295 while (iti->hasNext()) {
296 uint64_t valueI = iti->next();
297 SetIterator64Int *itj = new SetIterator64Int(iti);
298 while (itj->hasNext()) {
299 uint64_t valueJ = itj->next();
300 OrderPair pairIJ(valueI, valueJ, E_NULL);
301 OrderPair pairJI(valueJ, valueI, E_NULL);
302 Edge constIJ = getPartialPairConstraint(order, &pairIJ);
303 Edge constJI = getPartialPairConstraint(order, &pairJI);
304 SetIterator64Int *itk = new SetIterator64Int(itj);
305 while (itk->hasNext()) {
306 uint64_t valueK = itk->next();
307 OrderPair pairJK(valueJ, valueK, E_NULL);
308 OrderPair pairIK(valueI, valueK, E_NULL);
309 Edge constIK = getPartialPairConstraint(order, &pairIK);
310 Edge constJK = getPartialPairConstraint(order, &pairJK);
311 OrderPair pairKJ(valueK, valueJ, E_NULL);
312 OrderPair pairKI(valueK, valueI, E_NULL);
313 Edge constKI = getPartialPairConstraint(order, &pairKI);
314 Edge constKJ = getPartialPairConstraint(order, &pairKJ);
315 addConstraintCNF(cnf, generatePartialOrderConstraintsSATEncoder(constIJ, constJI,
318 constJK, constKJ, constIK, constKI));