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