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->orderPairTable;
  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         Edge constraint;
  69         if (!(table->contains(pair))) {
  70                 constraint = getNewVarSATEncoder();
  71                 OrderPair *paircopy = new OrderPair(pair->first, pair->second, constraint);
  72                 table->put(paircopy, paircopy);
  73         } else
  74                 constraint = table->get(pair)->constraint;
  75
  76         return negate ? constraintNegate(constraint) : constraint;
  77 }
  78
  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);
  89                 }
  90                 createAllTotalOrderConstraintsSATEncoder(boolOrder->order);
  91         }
  92         OrderPair pair(boolOrder->first, boolOrder->second, E_NULL);
  93         Edge constraint = getPairConstraint(boolOrder->order, &pair);
  94         return constraint;
  95 }
  96
  97
  98 void SATEncoder::createAllTotalOrderConstraintsSATEncoder(Order *order) {
  99 #ifdef CONFIG_DEBUG
 100         model_print("in total order ...\n");
 101 #endif
 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));
 118                         }
 119                 }
 120         }
 121 }
 122
 123 Edge getOrderConstraint(HashtableOrderPair *table, OrderPair *pair) {
 124         ASSERT(pair->first != pair->second);
 125         bool negate = false;
 126         OrderPair flipped;
 127         if (pair->first < pair->second) {
 128                 negate = true;
 129                 flipped.first = pair->second;
 130                 flipped.second = pair->first;
 131                 pair = &flipped;
 132         }
 133         if (!table->contains(pair)) {
 134                 return E_NULL;
 135         }
 136         Edge constraint = table->get(pair)->constraint;
 137         ASSERT(!edgeIsNull(constraint));
 138         return negate ? constraintNegate(constraint) : constraint;
 139 }
 140
 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);
 147 }
 148
 149 Edge SATEncoder::encodePartialOrderSATEncoder(BooleanOrder *constraint) {
 150         ASSERT(constraint->order->type == SATC_PARTIAL);
 151         return E_BOGUS;
 152 }