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 "orderencoder.h"
  10 #include "ordergraph.h"
  11 #include "orderedge.h"
  12 #include "element.h"
  13 #include "predicate.h"
  14 #include "orderelement.h"
  15
  16 Edge encodeOrderSATEncoder(SATEncoder *This, BooleanOrder *constraint) {
  17         switch ( constraint->order->type) {
  18                 case PARTIAL:
  19                         return encodePartialOrderSATEncoder(This, constraint);
  20                 case TOTAL:
  21                         return encodeTotalOrderSATEncoder(This, constraint);
  22                 default:
  23                         ASSERT(0);
  24         }
  25         default:
  26                 ASSERT(0);
  27         return E_BOGUS;
  28 }
  29
  30 Edge inferOrderConstraintFromGraph(Order* order, uint64_t _first, uint64_t _second){
  31         if (order->graph != NULL) {
  32                 OrderGraph *graph=order->graph;
  33                 OrderNode *first=lookupOrderNodeFromOrderGraph(graph, _first);
  34                 OrderNode *second=lookupOrderNodeFromOrderGraph(graph, _second);
  35                 if ((first != NULL) && (second != NULL)) {
  36                         OrderEdge *edge=lookupOrderEdgeFromOrderGraph(graph, first, second);
  37                         if (edge != NULL) {
  38                                 if (edge->mustPos)
  39                                         return E_True;
  40                                 else if (edge->mustNeg)
  41                                         return E_False;
  42                         }
  43                         OrderEdge *invedge=getOrderEdgeFromOrderGraph(graph, second, first);
  44                         if (invedge != NULL) {
  45                                 if (invedge->mustPos)
  46                                         return E_False;
  47                                 else if (invedge->mustNeg)
  48                                         return E_True;
  49                         }
  50                 }
  51         }
  52         return E_NULL;
  53 }
  54
  55 Edge getPairConstraint(SATEncoder *This, Order *order, OrderPair *pair) {
  56         Edge gvalue = inferOrderConstraintFromGraph(order, pair->first, pair->second);
  57         if(!edgeIsNull(gvalue))
  58                 return gvalue;
  59
  60         HashTableOrderPair *table = order->orderPairTable;
  61         bool negate = false;
  62         OrderPair flipped;
  63         if (pair->first < pair->second) {
  64                 negate = true;
  65                 flipped.first = pair->second;
  66                 flipped.second = pair->first;
  67                 pair = &flipped;
  68         }
  69         Edge constraint;
  70         if (!(table->contains(pair))) {
  71                 constraint = getNewVarSATEncoder(This);
  72                 OrderPair *paircopy = new OrderPair(pair->first, pair->second, constraint);
  73                 table->put(paircopy, paircopy);
  74         } else
  75                 constraint = table->get(pair)->constraint;
  76
  77         return negate ? constraintNegate(constraint) : constraint;
  78 }
  79
  80 Edge encodeTotalOrderSATEncoder(SATEncoder *This, BooleanOrder *boolOrder) {
  81         ASSERT(boolOrder->order->type == TOTAL);
  82         if (boolOrder->order->orderPairTable == NULL) {
  83                 boolOrder->order->initializeOrderHashTable();
  84                 bool doOptOrderStructure=GETVARTUNABLE(This->solver->tuner, boolOrder->order->type, OPTIMIZEORDERSTRUCTURE, &onoff);
  85                 if (doOptOrderStructure) {
  86                         boolOrder->order->graph = buildMustOrderGraph(boolOrder->order);
  87                         reachMustAnalysis(This->solver, boolOrder->order->graph, true);
  88                 }
  89                 createAllTotalOrderConstraintsSATEncoder(This, boolOrder->order);
  90         }
  91         OrderPair pair(boolOrder->first, boolOrder->second, E_NULL);
  92         Edge constraint = getPairConstraint(This, boolOrder->order, &pair);
  93         return constraint;
  94 }
  95
  96
  97 void createAllTotalOrderConstraintsSATEncoder(SATEncoder *This, Order *order) {
  98 #ifdef TRACE_DEBUG
  99         model_print("in total order ...\n");
 100 #endif
 101         ASSERT(order->type == TOTAL);
 102         Vector<uint64_t> *mems = order->set->members;
 103         uint size = mems->getSize();
 104         for (uint i = 0; i < size; i++) {
 105                 uint64_t valueI = mems->get(i);
 106                 for (uint j = i + 1; j < size; j++) {
 107                         uint64_t valueJ = mems->get(j);
 108                         OrderPair pairIJ(valueI, valueJ, E_NULL);
 109                         Edge constIJ = getPairConstraint(This, order, &pairIJ);
 110                         for (uint k = j + 1; k < size; k++) {
 111                                 uint64_t valueK = mems->get(k);
 112                                 OrderPair pairJK(valueJ, valueK, E_NULL);
 113                                 OrderPair pairIK(valueI, valueK, E_NULL);
 114                                 Edge constIK = getPairConstraint(This, order, &pairIK);
 115                                 Edge constJK = getPairConstraint(This, order, &pairJK);
 116                                 addConstraintCNF(This->cnf, generateTransOrderConstraintSATEncoder(This, constIJ, constJK, constIK));
 117                         }
 118                 }
 119         }
 120 }
 121
 122 Edge getOrderConstraint(HashTableOrderPair *table, OrderPair *pair) {
 123         ASSERT(pair->first != pair->second);
 124         bool negate = false;
 125         OrderPair flipped;
 126         if (pair->first < pair->second) {
 127                 negate = true;
 128                 flipped.first = pair->second;
 129                 flipped.second = pair->first;
 130                 pair = &flipped;
 131         }
 132         if (!table->contains(pair)) {
 133                 return E_NULL;
 134         }
 135         Edge constraint = table->get(pair)->constraint;
 136         ASSERT(!edgeIsNull(constraint));
 137         return negate ? constraintNegate(constraint) : constraint;
 138 }
 139
 140 Edge generateTransOrderConstraintSATEncoder(SATEncoder *This, Edge constIJ,Edge constJK,Edge constIK) {
 141         Edge carray[] = {constIJ, constJK, constraintNegate(constIK)};
 142         Edge loop1 = constraintOR(This->cnf, 3, carray);
 143         Edge carray2[] = {constraintNegate(constIJ), constraintNegate(constJK), constIK};
 144         Edge loop2 = constraintOR(This->cnf, 3, carray2 );
 145         return constraintAND2(This->cnf, loop1, loop2);
 146 }
 147
 148 Edge encodePartialOrderSATEncoder(SATEncoder *This, BooleanOrder *constraint) {
 149         ASSERT(constraint->order->type == PARTIAL);
 150         return E_BOGUS;
 151 }