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