src/Encoders/orderencoder.c

   1 #include "orderencoder.h"
   2 #include "structs.h"
   3 #include "csolver.h"
   4 #include "boolean.h"
   5 #include "ordergraph.h"
   6 #include "order.h"
   7 #include "ordernode.h"
   8 #include "rewriter.h"
   9 #include "mutableset.h"
  10
  11 OrderGraph *buildOrderGraph(Order *order) {
  12         OrderGraph *orderGraph = allocOrderGraph(order);
  13         uint constrSize = getSizeVectorBooleanOrder(&order->constraints);
  14         for (uint j = 0; j < constrSize; j++) {
  15                 addOrderConstraintToOrderGraph(orderGraph, getVectorBooleanOrder(&order->constraints, j));
  16         }
  17         return orderGraph;
  18 }
  19
  20 void DFS(OrderGraph *graph, VectorOrderNode *finishNodes) {
  21         HSIteratorOrderNode *iterator = iteratorOrderNode(graph->nodes);
  22         while (hasNextOrderNode(iterator)) {
  23                 OrderNode *node = nextOrderNode(iterator);
  24                 if (node->status == NOTVISITED) {
  25                         node->status = VISITED;
  26                         DFSNodeVisit(node, finishNodes, false, 0);
  27                         node->status = FINISHED;
  28                         pushVectorOrderNode(finishNodes, node);
  29                 }
  30         }
  31         deleteIterOrderNode(iterator);
  32 }
  33
  34 void DFSReverse(OrderGraph *graph, VectorOrderNode *finishNodes) {
  35         uint size = getSizeVectorOrderNode(finishNodes);
  36         uint sccNum = 1;
  37         for (int i = size - 1; i >= 0; i--) {
  38                 OrderNode *node = getVectorOrderNode(finishNodes, i);
  39                 if (node->status == NOTVISITED) {
  40                         node->status = VISITED;
  41                         DFSNodeVisit(node, NULL, true, sccNum);
  42                         node->sccNum = sccNum;
  43                         node->status = FINISHED;
  44                         sccNum++;
  45                 }
  46         }
  47 }
  48
  49 void DFSNodeVisit(OrderNode *node, VectorOrderNode *finishNodes, bool isReverse, uint sccNum) {
  50         HSIteratorOrderEdge *iterator = isReverse ? iteratorOrderEdge(node->inEdges) : iteratorOrderEdge(node->outEdges);
  51         while (hasNextOrderEdge(iterator)) {
  52                 OrderEdge *edge = nextOrderEdge(iterator);
  53                 if (!edge->polPos && !edge->pseudoPos)//Ignore edges that do not have positive polarity
  54                         continue;
  55
  56                 OrderNode *child = isReverse ? edge->source : edge->sink;
  57
  58                 if (child->status == NOTVISITED) {
  59                         child->status = VISITED;
  60                         DFSNodeVisit(child, finishNodes, isReverse, sccNum);
  61                         child->status = FINISHED;
  62                         if (finishNodes != NULL)
  63                                 pushVectorOrderNode(finishNodes, child);
  64                         if (isReverse)
  65                                 child->sccNum = sccNum;
  66                 }
  67         }
  68         deleteIterOrderEdge(iterator);
  69 }
  70
  71 void resetNodeInfoStatusSCC(OrderGraph *graph) {
  72         HSIteratorOrderNode *iterator = iteratorOrderNode(graph->nodes);
  73         while (hasNextOrderNode(iterator)) {
  74                 nextOrderNode(iterator)->status = NOTVISITED;
  75         }
  76         deleteIterOrderNode(iterator);
  77 }
  78
  79 void computeStronglyConnectedComponentGraph(OrderGraph *graph) {
  80         VectorOrderNode finishNodes;
  81         initDefVectorOrderNode(&finishNodes);
  82         DFS(graph, &finishNodes);
  83         resetNodeInfoStatusSCC(graph);
  84         DFSReverse(graph, &finishNodes);
  85         resetNodeInfoStatusSCC(graph);
  86         deleteVectorArrayOrderNode(&finishNodes);
  87 }
  88
  89 void removeMustBeTrueNodes(OrderGraph *graph) {
  90         //TODO: Nodes that all the incoming/outgoing edges are MUST_BE_TRUE
  91 }
  92
  93 /** This function computes a source set for every nodes, the set of
  94                 nodes that can reach that node via pospolarity edges.  It then
  95                 looks for negative polarity edges from nodes in the the source set
  96                 to determine whether we need to generate pseudoPos edges. */
  97
  98 void completePartialOrderGraph(OrderGraph *graph) {
  99         VectorOrderNode finishNodes;
 100         initDefVectorOrderNode(&finishNodes);
 101         DFS(graph, &finishNodes);
 102         resetNodeInfoStatusSCC(graph);
 103         HashTableNodeToNodeSet *table = allocHashTableNodeToNodeSet(128, 0.25);
 104
 105         VectorOrderNode sccNodes;
 106         initDefVectorOrderNode(&sccNodes);
 107
 108         uint size = getSizeVectorOrderNode(&finishNodes);
 109         uint sccNum = 1;
 110         for (int i = size - 1; i >= 0; i--) {
 111                 OrderNode *node = getVectorOrderNode(&finishNodes, i);
 112                 HashSetOrderNode *sources = allocHashSetOrderNode(4, 0.25);
 113                 putNodeToNodeSet(table, node, sources);
 114
 115                 if (node->status == NOTVISITED) {
 116                         //Need to do reverse traversal here...
 117                         node->status = VISITED;
 118                         DFSNodeVisit(node, &sccNodes, true, sccNum);
 119                         node->status = FINISHED;
 120                         node->sccNum = sccNum;
 121                         sccNum++;
 122                         pushVectorOrderNode(&sccNodes, node);
 123
 124                         //Compute in set for entire SCC
 125                         uint rSize = getSizeVectorOrderNode(&sccNodes);
 126                         for (int j = 0; j < rSize; j++) {
 127                                 OrderNode *rnode = getVectorOrderNode(&sccNodes, j);
 128                                 //Compute source sets
 129                                 HSIteratorOrderEdge *iterator = iteratorOrderEdge(rnode->inEdges);
 130                                 while (hasNextOrderEdge(iterator)) {
 131                                         OrderEdge *edge = nextOrderEdge(iterator);
 132                                         OrderNode *parent = edge->source;
 133                                         if (edge->polPos) {
 134                                                 addHashSetOrderNode(sources, parent);
 135                                                 HashSetOrderNode *parent_srcs = (HashSetOrderNode *)getNodeToNodeSet(table, parent);
 136                                                 addAllHashSetOrderNode(sources, parent_srcs);
 137                                         }
 138                                 }
 139                                 deleteIterOrderEdge(iterator);
 140                         }
 141                         for (int j=0; j < rSize; j++) {
 142                                 //Copy in set of entire SCC
 143                                 OrderNode *rnode = getVectorOrderNode(&sccNodes, j);
 144                                 HashSetOrderNode * set = (j==0) ? sources : copyHashSetOrderNode(sources);
 145                                 putNodeToNodeSet(table, rnode, set);
 146
 147                                 //Use source sets to compute pseudoPos edges
 148                                 HSIteratorOrderEdge *iterator = iteratorOrderEdge(rnode->inEdges);
 149                                 while (hasNextOrderEdge(iterator)) {
 150                                         OrderEdge *edge = nextOrderEdge(iterator);
 151                                         OrderNode *parent = edge->source;
 152                                         ASSERT(parent != rnode);
 153                                         if (edge->polNeg && parent->sccNum != rnode->sccNum &&
 154                                                         containsHashSetOrderNode(sources, parent)) {
 155                                                 OrderEdge *newedge = getOrderEdgeFromOrderGraph(graph, rnode, parent);
 156                                                 newedge->pseudoPos = true;
 157                                         }
 158                                 }
 159                                 deleteIterOrderEdge(iterator);
 160                         }
 161
 162                         clearVectorOrderNode(&sccNodes);
 163                 }
 164         }
 165
 166         resetAndDeleteHashTableNodeToNodeSet(table);
 167         resetNodeInfoStatusSCC(graph);
 168         deleteVectorArrayOrderNode(&sccNodes);
 169         deleteVectorArrayOrderNode(&finishNodes);
 170 }
 171
 172 void DFSMust(OrderGraph *graph, VectorOrderNode *finishNodes) {
 173         HSIteratorOrderNode *iterator = iteratorOrderNode(graph->nodes);
 174         while (hasNextOrderNode(iterator)) {
 175                 OrderNode *node = nextOrderNode(iterator);
 176                 if (node->status == NOTVISITED) {
 177                         node->status = VISITED;
 178                         DFSMustNodeVisit(node, finishNodes);
 179                         node->status = FINISHED;
 180                         pushVectorOrderNode(finishNodes, node);
 181                 }
 182         }
 183         deleteIterOrderNode(iterator);
 184 }
 185
 186 void DFSMustNodeVisit(OrderNode *node, VectorOrderNode *finishNodes) {
 187         HSIteratorOrderEdge *iterator = iteratorOrderEdge(node->outEdges);
 188         while (hasNextOrderEdge(iterator)) {
 189                 OrderEdge *edge = nextOrderEdge(iterator);
 190                 OrderNode *child = edge->sink;
 191
 192                 if (!edge->mustPos)     //Ignore edges that are not must Positive edges
 193                         continue;
 194
 195                 if (child->status == NOTVISITED) {
 196                         child->status = VISITED;
 197                         DFSMustNodeVisit(child, finishNodes);
 198                         child->status = FINISHED;
 199                         pushVectorOrderNode(finishNodes, child);
 200                 }
 201         }
 202         deleteIterOrderEdge(iterator);
 203 }
 204
 205
 206 void DFSClearContradictions(CSolver *solver, OrderGraph *graph, VectorOrderNode *finishNodes, bool computeTransitiveClosure) {
 207         uint size = getSizeVectorOrderNode(finishNodes);
 208         HashTableNodeToNodeSet *table = allocHashTableNodeToNodeSet(128, 0.25);
 209
 210         for (int i = size - 1; i >= 0; i--) {
 211                 OrderNode *node = getVectorOrderNode(finishNodes, i);
 212                 HashSetOrderNode *sources = allocHashSetOrderNode(4, 0.25);
 213                 putNodeToNodeSet(table, node, sources);
 214
 215                 {
 216                         //Compute source sets
 217                         HSIteratorOrderEdge *iterator = iteratorOrderEdge(node->inEdges);
 218                         while (hasNextOrderEdge(iterator)) {
 219                                 OrderEdge *edge = nextOrderEdge(iterator);
 220                                 OrderNode *parent = edge->source;
 221                                 if (edge->mustPos) {
 222                                         addHashSetOrderNode(sources, parent);
 223                                         HashSetOrderNode *parent_srcs = (HashSetOrderNode *)getNodeToNodeSet(table, parent);
 224                                         addAllHashSetOrderNode(sources, parent_srcs);
 225                                 }
 226                         }
 227                         deleteIterOrderEdge(iterator);
 228                 }
 229                 if (computeTransitiveClosure) {
 230                         //Compute full transitive closure for nodes
 231                         HSIteratorOrderNode *srciterator = iteratorOrderNode(sources);
 232                         while (hasNextOrderNode(srciterator)) {
 233                                 OrderNode *srcnode = nextOrderNode(srciterator);
 234                                 OrderEdge *newedge = getOrderEdgeFromOrderGraph(graph, srcnode, node);
 235                                 newedge->mustPos = true;
 236                                 newedge->polPos = true;
 237                                 if (newedge->mustNeg)
 238                                         solver->unsat = true;
 239                                 addHashSetOrderEdge(srcnode->outEdges,newedge);
 240                                 addHashSetOrderEdge(node->inEdges,newedge);
 241                         }
 242                         deleteIterOrderNode(srciterator);
 243                 }
 244                 {
 245                         //Use source sets to compute mustPos edges
 246                         HSIteratorOrderEdge *iterator = iteratorOrderEdge(node->inEdges);
 247                         while (hasNextOrderEdge(iterator)) {
 248                                 OrderEdge *edge = nextOrderEdge(iterator);
 249                                 OrderNode *parent = edge->source;
 250                                 if (!edge->mustPos && containsHashSetOrderNode(sources, parent)) {
 251                                         edge->mustPos = true;
 252                                         edge->polPos = true;
 253                                         if (edge->mustNeg)
 254                                                 solver->unsat = true;
 255                                 }
 256                         }
 257                         deleteIterOrderEdge(iterator);
 258                 }
 259                 {
 260                         //Use source sets to compute mustNeg for edges that would introduce cycle if true
 261                         HSIteratorOrderEdge *iterator = iteratorOrderEdge(node->outEdges);
 262                         while (hasNextOrderEdge(iterator)) {
 263                                 OrderEdge *edge = nextOrderEdge(iterator);
 264                                 OrderNode *child = edge->sink;
 265                                 if (!edge->mustNeg && containsHashSetOrderNode(sources, child)) {
 266                                         edge->mustNeg = true;
 267                                         edge->polNeg = true;
 268                                         if (edge->mustPos)
 269                                                 solver->unsat = true;
 270                                 }
 271                         }
 272                         deleteIterOrderEdge(iterator);
 273                 }
 274         }
 275
 276         resetAndDeleteHashTableNodeToNodeSet(table);
 277 }
 278
 279 /* This function finds edges that would form a cycle with must edges
 280    and forces them to be mustNeg.  It also decides whether an edge
 281    must be true because of transitivity from other must be true
 282    edges. */
 283
 284 void reachMustAnalysis(CSolver * solver, OrderGraph *graph, bool computeTransitiveClosure) {
 285         VectorOrderNode finishNodes;
 286         initDefVectorOrderNode(&finishNodes);
 287         //Topologically sort the mustPos edge graph
 288         DFSMust(graph, &finishNodes);
 289         resetNodeInfoStatusSCC(graph);
 290
 291         //Find any backwards edges that complete cycles and force them to be mustNeg
 292         DFSClearContradictions(solver, graph, &finishNodes, computeTransitiveClosure);
 293         deleteVectorArrayOrderNode(&finishNodes);
 294 }
 295
 296 /* This function finds edges that must be positive and forces the
 297    inverse edge to be negative (and clears its positive polarity if it
 298    had one). */
 299
 300 void localMustAnalysisTotal(CSolver *solver, OrderGraph *graph) {
 301         HSIteratorOrderEdge *iterator = iteratorOrderEdge(graph->edges);
 302         while (hasNextOrderEdge(iterator)) {
 303                 OrderEdge *edge = nextOrderEdge(iterator);
 304                 if (edge->mustPos) {
 305                         OrderEdge *invEdge = getInverseOrderEdge(graph, edge);
 306                         if (invEdge != NULL) {
 307                                 if (!invEdge->mustPos) {
 308                                         invEdge->polPos = false;
 309                                 } else {
 310                                         solver->unsat = true;
 311                                 }
 312                                 invEdge->mustNeg = true;
 313                                 invEdge->polNeg = true;
 314                         }
 315                 }
 316         }
 317         deleteIterOrderEdge(iterator);
 318 }
 319
 320 /** This finds edges that must be positive and forces the inverse edge
 321     to be negative.  It also clears the negative flag of this edge.
 322     It also finds edges that must be negative and clears the positive
 323     polarity. */
 324
 325 void localMustAnalysisPartial(CSolver *solver, OrderGraph *graph) {
 326         HSIteratorOrderEdge *iterator = iteratorOrderEdge(graph->edges);
 327         while (hasNextOrderEdge(iterator)) {
 328                 OrderEdge *edge = nextOrderEdge(iterator);
 329                 if (edge->mustPos) {
 330                         if (!edge->mustNeg) {
 331                                 edge->polNeg = false;
 332                         } else
 333                                 solver->unsat = true;
 334
 335                         OrderEdge *invEdge = getInverseOrderEdge(graph, edge);
 336                         if (invEdge != NULL) {
 337                                 if (!invEdge->mustPos)
 338                                         invEdge->polPos = false;
 339                                 else
 340                                         solver->unsat = true;
 341                                 invEdge->mustNeg = true;
 342                                 invEdge->polNeg = true;
 343                         }
 344                 }
 345                 if (edge->mustNeg && !edge->mustPos) {
 346                         edge->polPos = false;
 347                 }
 348         }
 349         deleteIterOrderEdge(iterator);
 350 }
 351
 352 void decomposeOrder(CSolver *This, Order *order, OrderGraph *graph) {
 353         VectorOrder ordervec;
 354         initDefVectorOrder(&ordervec);
 355         uint size = getSizeVectorBooleanOrder(&order->constraints);
 356         for (uint i = 0; i < size; i++) {
 357                 BooleanOrder *orderconstraint = getVectorBooleanOrder(&order->constraints, i);
 358                 OrderNode *from = getOrderNodeFromOrderGraph(graph, orderconstraint->first);
 359                 OrderNode *to = getOrderNodeFromOrderGraph(graph, orderconstraint->second);
 360                 model_print("from->sccNum:%u\tto->sccNum:%u\n", from->sccNum, to->sccNum);
 361                 if (from->sccNum != to->sccNum) {
 362                         OrderEdge *edge = getOrderEdgeFromOrderGraph(graph, from, to);
 363                         if (edge->polPos) {
 364                                 replaceBooleanWithTrue(This, (Boolean *)orderconstraint);
 365                         } else if (edge->polNeg) {
 366                                 replaceBooleanWithFalse(This, (Boolean *)orderconstraint);
 367                         } else {
 368                                 //This case should only be possible if constraint isn't in AST
 369                                 ASSERT(0);
 370                         }
 371                 } else {
 372                         //Build new order and change constraint's order
 373                         Order *neworder = NULL;
 374                         if (getSizeVectorOrder(&ordervec) > from->sccNum)
 375                                 neworder = getVectorOrder(&ordervec, from->sccNum);
 376                         if (neworder == NULL) {
 377                                 Set *set = (Set *) allocMutableSet(order->set->type);
 378                                 neworder = allocOrder(order->type, set);
 379                                 pushVectorOrder(This->allOrders, neworder);
 380                                 setExpandVectorOrder(&ordervec, from->sccNum, neworder);
 381                         }
 382                         if (from->status != ADDEDTOSET) {
 383                                 from->status = ADDEDTOSET;
 384                                 addElementMSet((MutableSet *)neworder->set, from->id);
 385                         }
 386                         if (to->status != ADDEDTOSET) {
 387                                 to->status = ADDEDTOSET;
 388                                 addElementMSet((MutableSet *)neworder->set, to->id);
 389                         }
 390                         orderconstraint->order = neworder;
 391                         addOrderConstraint(neworder, orderconstraint);
 392                 }
 393         }
 394         for(uint i=0; i<getSizeVectorOrder(&ordervec); i++){
 395                 Order* order = getVectorOrder(&ordervec, i);
 396                 if(order!=NULL)
 397                         model_print("i=%u\t", i);
 398         }
 399         deleteVectorArrayOrder(&ordervec);
 400 }
 401
 402 void orderAnalysis(CSolver *This) {
 403         uint size = getSizeVectorOrder(This->allOrders);
 404         for (uint i = 0; i < size; i++) {
 405                 Order *order = getVectorOrder(This->allOrders, i);
 406                 OrderGraph *graph = buildOrderGraph(order);
 407                 if (order->type == PARTIAL) {
 408                         //Required to do SCC analysis for partial order graphs.  It
 409                         //makes sure we don't incorrectly optimize graphs with negative
 410                         //polarity edges
 411                         completePartialOrderGraph(graph);
 412                 }
 413
 414                 //This analysis is completely optional
 415                 reachMustAnalysis(This, graph, false);
 416
 417                 //This pair of analysis is also optional
 418                 if (order->type == PARTIAL) {
 419                         localMustAnalysisPartial(This, graph);
 420                 } else {
 421                         localMustAnalysisTotal(This, graph);
 422                 }
 423
 424                 //This optimization is completely optional
 425                 removeMustBeTrueNodes(graph);
 426
 427                 //This is needed for splitorder
 428                 computeStronglyConnectedComponentGraph(graph);
 429
 430                 decomposeOrder(This, order, graph);
 431
 432                 deleteOrderGraph(graph);
 433         }
 434 }