src/ASTAnalyses/Order/orderanalysis.cc

   1 #include <stdint.h>
   2
   3 #include "orderanalysis.h"
   4 #include "structs.h"
   5 #include "csolver.h"
   6 #include "boolean.h"
   7 #include "ordergraph.h"
   8 #include "order.h"
   9 #include "ordernode.h"
  10 #include "rewriter.h"
  11 #include "mutableset.h"
  12 #include "tunable.h"
  13
  14 /** Returns a table that maps a node to the set of nodes that can reach the node. */
  15 HashtableNodeToNodeSet * getMustReachMap(CSolver  *solver, OrderGraph *graph, Vector<OrderNode *> *finishNodes) {
  16         uint size = finishNodes->getSize();
  17         HashtableNodeToNodeSet *table = new HashtableNodeToNodeSet(128, 0.25);
  18
  19         for (int i = size - 1; i >= 0; i--) {
  20                 OrderNode *node = finishNodes->get(i);
  21                 HashsetOrderNode *sources = new HashsetOrderNode(4, 0.25);
  22                 table->put(node, sources);
  23
  24                 {
  25                         //Compute source sets
  26                         SetIteratorOrderEdge *iterator = node->inEdges.iterator();
  27                         while (iterator->hasNext()) {
  28                                 OrderEdge *edge = iterator->next();
  29                                 OrderNode *parent = edge->source;
  30                                 if (edge->mustPos) {
  31                                         sources->add(parent);
  32                                         HashsetOrderNode *parent_srcs = (HashsetOrderNode *) table->get(parent);
  33                                         sources->addAll(parent_srcs);
  34                                 }
  35                         }
  36                         delete iterator;
  37                 }
  38         }
  39         return table;
  40 }
  41
  42 void DFSClearContradictions(CSolver *solver, OrderGraph *graph, HashtableNodeToNodeSet * table, Vector<OrderNode *> *finishNodes, bool computeTransitiveClosure) {
  43         uint size = finishNodes->getSize();
  44
  45         for (int i = size - 1; i >= 0; i--) {
  46                 OrderNode *node = finishNodes->get(i);
  47                 HashsetOrderNode *sources = table->get(node);
  48
  49                 if (computeTransitiveClosure) {
  50                         //Compute full transitive closure for nodes
  51                         SetIteratorOrderNode *srciterator = sources->iterator();
  52                         while (srciterator->hasNext()) {
  53                                 OrderNode *srcnode = srciterator->next();
  54                                 OrderEdge *newedge = graph->getOrderEdgeFromOrderGraph(srcnode, node);
  55                                 newedge->mustPos = true;
  56                                 newedge->polPos = true;
  57                                 if (newedge->mustNeg)
  58                                         solver->setUnSAT();
  59                                 srcnode->outEdges.add(newedge);
  60                                 node->inEdges.add(newedge);
  61                         }
  62                         delete srciterator;
  63                 }
  64                 {
  65                         //Use source sets to compute mustPos edges
  66                         SetIteratorOrderEdge *iterator = node->inEdges.iterator();
  67                         while (iterator->hasNext()) {
  68                                 OrderEdge *edge = iterator->next();
  69                                 OrderNode *parent = edge->source;
  70                                 if (!edge->mustPos && sources->contains(parent)) {
  71                                         edge->mustPos = true;
  72                                         edge->polPos = true;
  73                                         if (edge->mustNeg)
  74                                                 solver->setUnSAT();
  75                                 }
  76                         }
  77                         delete iterator;
  78                 }
  79                 {
  80                         //Use source sets to compute mustNeg for edges that would introduce cycle if true
  81                         SetIteratorOrderEdge *iterator = node->outEdges.iterator();
  82                         while (iterator->hasNext()) {
  83                                 OrderEdge *edge = iterator->next();
  84                                 OrderNode *child = edge->sink;
  85                                 if (!edge->mustNeg && sources->contains(child)) {
  86                                         edge->mustNeg = true;
  87                                         edge->polNeg = true;
  88                                         if (edge->mustPos) {
  89                                                 solver->setUnSAT();
  90                                         }
  91                                 }
  92                         }
  93                         delete iterator;
  94                 }
  95         }
  96 }
  97
  98 /* This function finds edges that would form a cycle with must edges
  99    and forces them to be mustNeg.  It also decides whether an edge
 100    must be true because of transitivity from other must be true
 101    edges. */
 102
 103 void reachMustAnalysis(CSolver *solver, OrderGraph *graph, bool computeTransitiveClosure) {
 104         Vector<OrderNode *> finishNodes;
 105         //Topologically sort the mustPos edge graph
 106         graph->DFSMust(&finishNodes);
 107         graph->resetNodeInfoStatusSCC();
 108         HashtableNodeToNodeSet * table=getMustReachMap(solver, graph, & finishNodes);
 109         //Find any backwards edges that complete cycles and force them to be mustNeg
 110         DFSClearContradictions(solver, graph, table, &finishNodes, computeTransitiveClosure);
 111         table->resetAndDeleteVals();
 112         delete table;
 113 }
 114
 115 /* This function finds edges that must be positive and forces the
 116    inverse edge to be negative (and clears its positive polarity if it
 117    had one). */
 118
 119 void localMustAnalysisTotal(CSolver *solver, OrderGraph *graph) {
 120         SetIteratorOrderEdge *iterator = graph->getEdges();
 121         while (iterator->hasNext()) {
 122                 OrderEdge *edge = iterator->next();
 123                 if (edge->mustPos) {
 124                         OrderEdge *invEdge = graph->getInverseOrderEdge(edge);
 125                         if (invEdge != NULL) {
 126                                 if (!invEdge->mustPos) {
 127                                         invEdge->polPos = false;
 128                                 } else
 129                                         solver->setUnSAT();
 130                                 invEdge->mustNeg = true;
 131                                 invEdge->polNeg = true;
 132                         }
 133                 }
 134         }
 135         delete iterator;
 136 }
 137
 138 /** This finds edges that must be positive and forces the inverse edge
 139     to be negative.  It also clears the negative flag of this edge.
 140     It also finds edges that must be negative and clears the positive
 141     polarity. */
 142
 143 void localMustAnalysisPartial(CSolver *solver, OrderGraph *graph) {
 144         SetIteratorOrderEdge *iterator = graph->getEdges();
 145         while (iterator->hasNext()) {
 146                 OrderEdge *edge = iterator->next();
 147                 if (edge->mustPos) {
 148                         if (!edge->mustNeg) {
 149                                 edge->polNeg = false;
 150                         } else {
 151                                 solver->setUnSAT();
 152                         }
 153                         OrderEdge *invEdge = graph->getInverseOrderEdge(edge);
 154                         if (invEdge != NULL) {
 155                                 if (!invEdge->mustPos)
 156                                         invEdge->polPos = false;
 157                                 else
 158                                         solver->setUnSAT();
 159                                 invEdge->mustNeg = true;
 160                                 invEdge->polNeg = true;
 161                         }
 162                 }
 163                 if (edge->mustNeg && !edge->mustPos) {
 164                         edge->polPos = false;
 165                 }
 166         }
 167         delete iterator;
 168 }