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