src/Backend/satorderencoder.c

   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         if(constraint->order->order.type == INTEGERENCODING){
  18                 return orderIntegerEncodingSATEncoder(This, constraint);
  19         }
  20         switch ( constraint->order->type) {
  21         case PARTIAL:
  22                 return encodePartialOrderSATEncoder(This, constraint);
  23         case TOTAL:
  24                 return encodeTotalOrderSATEncoder(This, constraint);
  25         default:
  26                 ASSERT(0);
  27         }
  28         return E_BOGUS;
  29 }
  30
  31 Edge orderIntegerEncodingSATEncoder(SATEncoder *This, BooleanOrder *boolOrder){
  32         if(boolOrder->order->graph == NULL){
  33                 bool doOptOrderStructure=GETVARTUNABLE(This->solver->tuner, boolOrder->order->type,
  34                         OPTIMIZEORDERSTRUCTURE, &onoff);
  35                 if (doOptOrderStructure ) {
  36                         boolOrder->order->graph = buildMustOrderGraph(boolOrder->order);
  37                         reachMustAnalysis(This->solver, boolOrder->order->graph, true);
  38                 }
  39         }
  40         Order* order = boolOrder->order;
  41         Edge gvalue = inferOrderConstraintFromGraph(order, boolOrder->first, boolOrder->second);
  42         if(!edgeIsNull(gvalue))
  43                 return gvalue;
  44
  45         if (boolOrder->order->elementTable == NULL) {
  46                 initializeOrderElementsHashTable(boolOrder->order);
  47         }
  48         //getting two elements and using LT predicate ...
  49         Element* elem1 = getOrderIntegerElement(This, order, boolOrder->first);
  50         ElementEncoding *encoding = getElementEncoding(elem1);
  51         if (getElementEncodingType(encoding) == ELEM_UNASSIGNED) {
  52                 setElementEncodingType(encoding, BINARYINDEX);
  53                 encodingArrayInitialization(encoding);
  54         }
  55         Element* elem2 = getOrderIntegerElement(This, order, boolOrder->second);
  56         encoding = getElementEncoding(elem2);
  57         if (getElementEncodingType(encoding) == ELEM_UNASSIGNED) {
  58                 setElementEncodingType(encoding, BINARYINDEX);
  59                 encodingArrayInitialization(encoding);
  60         }
  61         Predicate *predicate =allocPredicateOperator(LT, (Set*[]){order->set, order->set}, 2);
  62         Boolean * boolean=allocBooleanPredicate(predicate, (Element *[]){elem1,elem2}, 2, NULL);
  63         setFunctionEncodingType(getPredicateFunctionEncoding((BooleanPredicate*)boolean), CIRCUIT);
  64         {//Adding new elements and boolean/predicate to solver regarding memory management
  65                 pushVectorBoolean(This->solver->allBooleans, boolean);
  66                 pushVectorPredicate(This->solver->allPredicates, predicate);
  67                 pushVectorElement(This->solver->allElements, elem1);
  68                 pushVectorElement(This->solver->allElements, elem2);
  69         }
  70         return encodeConstraintSATEncoder(This, boolean);
  71 }
  72
  73 Edge inferOrderConstraintFromGraph(Order* order, uint64_t _first, uint64_t _second){
  74         if (order->graph != NULL) {
  75                 OrderGraph *graph=order->graph;
  76                 OrderNode *first=lookupOrderNodeFromOrderGraph(graph, _first);
  77                 OrderNode *second=lookupOrderNodeFromOrderGraph(graph, _second);
  78                 if ((first != NULL) && (second != NULL)) {
  79                         OrderEdge *edge=lookupOrderEdgeFromOrderGraph(graph, first, second);
  80                         if (edge != NULL) {
  81                                 if (edge->mustPos)
  82                                         return E_True;
  83                                 else if (edge->mustNeg)
  84                                         return E_False;
  85                         }
  86                         OrderEdge *invedge=getOrderEdgeFromOrderGraph(graph, second, first);
  87                         if (invedge != NULL) {
  88                                 if (invedge->mustPos)
  89                                         return E_False;
  90                                 else if (invedge->mustNeg)
  91                                         return E_True;
  92                         }
  93                 }
  94         }
  95         return E_NULL;
  96 }
  97
  98 Element* getOrderIntegerElement(SATEncoder* This,Order *order, uint64_t item) {
  99         HashSetOrderElement* eset = order->elementTable;
 100         OrderElement oelement ={item, NULL};
 101         if( !containsHashSetOrderElement(eset, &oelement)){
 102                 Element* elem = allocElementSet(order->set);
 103                 ElementEncoding* encoding = getElementEncoding(elem);
 104                 setElementEncodingType(encoding, BINARYINDEX);
 105                 encodingArrayInitialization(encoding);
 106                 encodeElementSATEncoder(This, elem);
 107                 addHashSetOrderElement(eset, allocOrderElement(item, elem));
 108                 return elem;
 109         }else
 110                 return getHashSetOrderElement(eset, &oelement)->elem;
 111 }
 112 Edge getPairConstraint(SATEncoder *This, Order *order, OrderPair *pair) {
 113         Edge gvalue = inferOrderConstraintFromGraph(order, pair->first, pair->second);
 114         if(!edgeIsNull(gvalue))
 115                 return gvalue;
 116
 117         HashTableOrderPair *table = order->orderPairTable;
 118         bool negate = false;
 119         OrderPair flipped;
 120         if (pair->first < pair->second) {
 121                 negate = true;
 122                 flipped.first = pair->second;
 123                 flipped.second = pair->first;
 124                 pair = &flipped;
 125         }
 126         Edge constraint;
 127         if (!containsOrderPair(table, pair)) {
 128                 constraint = getNewVarSATEncoder(This);
 129                 OrderPair *paircopy = allocOrderPair(pair->first, pair->second, constraint);
 130                 putOrderPair(table, paircopy, paircopy);
 131         } else
 132                 constraint = getOrderPair(table, pair)->constraint;
 133
 134         return negate ? constraintNegate(constraint) : constraint;
 135 }
 136
 137 Edge encodeTotalOrderSATEncoder(SATEncoder *This, BooleanOrder *boolOrder) {
 138         ASSERT(boolOrder->order->type == TOTAL);
 139         if (boolOrder->order->orderPairTable == NULL) {
 140                 initializeOrderHashTable(boolOrder->order);
 141                 bool doOptOrderStructure=GETVARTUNABLE(This->solver->tuner, boolOrder->order->type, OPTIMIZEORDERSTRUCTURE, &onoff);
 142                 if (doOptOrderStructure) {
 143                         boolOrder->order->graph = buildMustOrderGraph(boolOrder->order);
 144                         reachMustAnalysis(This->solver, boolOrder->order->graph, true);
 145                 }
 146                 createAllTotalOrderConstraintsSATEncoder(This, boolOrder->order);
 147         }
 148         OrderPair pair = {boolOrder->first, boolOrder->second, E_NULL};
 149         Edge constraint = getPairConstraint(This, boolOrder->order, &pair);
 150         return constraint;
 151 }
 152
 153
 154 void createAllTotalOrderConstraintsSATEncoder(SATEncoder *This, Order *order) {
 155 #ifdef TRACE_DEBUG
 156         model_print("in total order ...\n");
 157 #endif
 158         ASSERT(order->type == TOTAL);
 159         VectorInt *mems = order->set->members;
 160         uint size = getSizeVectorInt(mems);
 161         for (uint i = 0; i < size; i++) {
 162                 uint64_t valueI = getVectorInt(mems, i);
 163                 for (uint j = i + 1; j < size; j++) {
 164                         uint64_t valueJ = getVectorInt(mems, j);
 165                         OrderPair pairIJ = {valueI, valueJ};
 166                         Edge constIJ = getPairConstraint(This, order, &pairIJ);
 167                         for (uint k = j + 1; k < size; k++) {
 168                                 uint64_t valueK = getVectorInt(mems, k);
 169                                 OrderPair pairJK = {valueJ, valueK};
 170                                 OrderPair pairIK = {valueI, valueK};
 171                                 Edge constIK = getPairConstraint(This, order, &pairIK);
 172                                 Edge constJK = getPairConstraint(This, order, &pairJK);
 173                                 addConstraintCNF(This->cnf, generateTransOrderConstraintSATEncoder(This, constIJ, constJK, constIK));
 174                         }
 175                 }
 176         }
 177 }
 178
 179 Edge getOrderConstraint(HashTableOrderPair *table, OrderPair *pair) {
 180         ASSERT(pair->first != pair->second);
 181         bool negate = false;
 182         OrderPair flipped;
 183         if (pair->first < pair->second) {
 184                 negate = true;
 185                 flipped.first = pair->second;
 186                 flipped.second = pair->first;
 187                 pair = &flipped;
 188         }
 189         if (!containsOrderPair(table, pair)) {
 190                 return E_NULL;
 191         }
 192         Edge constraint = getOrderPair(table, pair)->constraint;
 193         ASSERT(!edgeIsNull(constraint));
 194         return negate ? constraintNegate(constraint) : constraint;
 195 }
 196
 197 Edge generateTransOrderConstraintSATEncoder(SATEncoder *This, Edge constIJ,Edge constJK,Edge constIK) {
 198         Edge carray[] = {constIJ, constJK, constraintNegate(constIK)};
 199         Edge loop1 = constraintOR(This->cnf, 3, carray);
 200         Edge carray2[] = {constraintNegate(constIJ), constraintNegate(constJK), constIK};
 201         Edge loop2 = constraintOR(This->cnf, 3, carray2 );
 202         return constraintAND2(This->cnf, loop1, loop2);
 203 }
 204
 205 Edge encodePartialOrderSATEncoder(SATEncoder *This, BooleanOrder *constraint) {
 206         ASSERT(constraint->order->type == PARTIAL);
 207         return E_BOGUS;
 208 }