src/Backend/satorderencoder.cc

   1 #include "satencoder.h"
   2 #include "structs.h"
   3 #include "common.h"
   4 #include "order.h"
   5 #include "csolver.h"
   6 #include "orderpair.h"
   7 #include "set.h"
   8 #include "tunable.h"
   9 #include "orderanalysis.h"
  10 #include "ordergraph.h"
  11 #include "orderedge.h"
  12 #include "element.h"
  13 #include "predicate.h"
  14 #include "orderelement.h"
  15 #include "orderpairresolver.h"
  16
  17 Edge SATEncoder::encodeOrderSATEncoder(BooleanOrder *constraint) {
  18         switch ( constraint->order->type) {
  19         case SATC_PARTIAL:
  20                 return encodePartialOrderSATEncoder(constraint);
  21         case SATC_TOTAL:
  22                 return encodeTotalOrderSATEncoder(constraint);
  23         default:
  24                 ASSERT(0);
  25         }
  26         return E_BOGUS;
  27 }
  28
  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);
  36                         if (edge != NULL) {
  37                                 if (edge->mustPos)
  38                                         return E_True;
  39                                 else if (edge->mustNeg)
  40                                         return E_False;
  41                         }
  42                         OrderEdge *invedge = graph->lookupOrderEdgeFromOrderGraph(second, first);
  43                         if (invedge != NULL) {
  44                                 if (invedge->mustPos)
  45                                         return E_False;
  46                                 else if (invedge->mustNeg)
  47                                         return E_True;
  48                         }
  49                 }
  50         }
  51         return E_NULL;
  52 }
  53
  54 Edge SATEncoder::getPairConstraint(Order *order, OrderPair *pair) {
  55         Edge gvalue = inferOrderConstraintFromGraph(order, pair->first, pair->second);
  56         if (!edgeIsNull(gvalue))
  57                 return gvalue;
  58
  59         HashtableOrderPair *table = order->getOrderPairTable();
  60         bool negate = false;
  61         OrderPair flipped;
  62         if (pair->first < pair->second) {
  63                 negate = true;
  64                 flipped.first = pair->second;
  65                 flipped.second = pair->first;
  66                 pair = &flipped;
  67         }
  68         OrderPair *tmp;
  69         if (!(table->contains(pair))) {
  70                 tmp = new OrderPair(pair->first, pair->second, getNewVarSATEncoder());
  71                 table->put(tmp, tmp);
  72         } else {
  73                 tmp = table->get(pair);
  74         }
  75         return negate ? tmp->getNegatedConstraint() : tmp->getConstraint();
  76 }
  77
  78 Edge SATEncoder::getPartialPairConstraint(Order *order, OrderPair *pair) {
  79         Edge gvalue = inferOrderConstraintFromGraph(order, pair->first, pair->second);
  80         if (!edgeIsNull(gvalue))
  81                 return gvalue;
  82
  83         HashtableOrderPair *table = order->getOrderPairTable();
  84
  85         OrderPair *tmp;
  86         if (!(table->contains(pair))) {
  87                 Edge constraint = getNewVarSATEncoder();
  88                 tmp = new OrderPair(pair->first, pair->second, constraint);
  89                 table->put(tmp, tmp);
  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)));
  94         } else {
  95                 tmp = table->get(pair);
  96         }
  97         return tmp->getConstraint();
  98 }
  99
 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);
 110                 }
 111                 if (GETVARTUNABLE(solver->getTuner(), order->type, DECOMPOSEORDER, &onoff) == 0)
 112                         createAllTotalOrderConstraintsSATEncoderSparse(boolOrder->order);
 113                 else
 114                         createAllTotalOrderConstraintsSATEncoder(boolOrder->order);
 115         }
 116         OrderPair pair(boolOrder->first, boolOrder->second, E_NULL);
 117         Edge constraint = getPairConstraint(boolOrder->order, &pair);
 118         return constraint;
 119 }
 120
 121
 122 void SATEncoder::createAllTotalOrderConstraintsSATEncoder(Order *order) {
 123 #ifdef CONFIG_DEBUG
 124         model_print("in total order ...\n");
 125 #endif
 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));
 142                         }
 143                 }
 144         }
 145 }
 146
 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);
 153 }
 154
 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));
 159
 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);
 172
 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);
 185
 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);
 198
 199         Edge unorder [] = {uoIJ, uoJK, uoIK};
 200         Edge cunorder = constraintAND(cnf, 3, unorder);
 201
 202
 203         Edge res[] = {ct1,ct2,ct3,ct4,ct5,ct6,
 204                                                                 cp1,cp2,cp3,cp4,cp5,cp6,
 205                                                                 co1,co2,co3,co4,co5,co6,
 206                                                                 cunorder};
 207         return constraintOR(cnf, 19, res);
 208 }
 209
 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);
 219                 }
 220                 if (GETVARTUNABLE(solver->getTuner(), order->type, DECOMPOSEORDER, &onoff) == 0)
 221                         createAllPartialOrderConstraintsSATEncoderSparse(boolOrder->order);
 222                 else
 223                         createAllPartialOrderConstraintsSATEncoder(boolOrder->order);
 224         }
 225         OrderPair pair(boolOrder->first, boolOrder->second, E_NULL);
 226         Edge constraint = getPartialPairConstraint(boolOrder->order, &pair);
 227         return constraint;
 228 }
 229
 230
 231 void SATEncoder::createAllPartialOrderConstraintsSATEncoder(Order *order) {
 232 #ifdef CONFIG_DEBUG
 233         model_print("in partial order ...\n");
 234 #endif
 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));
 258                         }
 259                 }
 260         }
 261 }
 262
 263 void SATEncoder::createAllTotalOrderConstraintsSATEncoderSparse(Order *order) {
 264 #ifdef CONFIG_DEBUG
 265         model_print("in total order ...\n");
 266 #endif
 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));
 284                         }
 285                 }
 286         }
 287 }
 288
 289 void SATEncoder::createAllPartialOrderConstraintsSATEncoderSparse(Order *order) {
 290 #ifdef CONFIG_DEBUG
 291         model_print("in partial order ...\n");
 292 #endif
 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,
 316
 317
 318                                                                                                                                                                                                                                                                                                 constJK, constKJ, constIK, constKI));
 319                         }
 320                 }
 321         }
 322 }