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