From: bdemsky Date: Mon, 28 Aug 2017 01:09:33 +0000 (-0700) Subject: Class renaming X-Git-Url: http://plrg.eecs.uci.edu/git/?p=satune.git;a=commitdiff_plain;h=4a0700a15422c8bacce0b27680bf8d3bd3351504 Class renaming --- diff --git a/src/ASTAnalyses/orderanalysis.cc b/src/ASTAnalyses/orderanalysis.cc new file mode 100644 index 0000000..57443c1 --- /dev/null +++ b/src/ASTAnalyses/orderanalysis.cc @@ -0,0 +1,371 @@ +#include "orderanalysis.h" +#include "structs.h" +#include "csolver.h" +#include "boolean.h" +#include "ordergraph.h" +#include "order.h" +#include "ordernode.h" +#include "rewriter.h" +#include "mutableset.h" +#include "tunable.h" + +void DFS(OrderGraph *graph, Vector *finishNodes) { + HSIteratorOrderNode *iterator = graph->getNodes(); + while (iterator->hasNext()) { + OrderNode *node = iterator->next(); + if (node->status == NOTVISITED) { + node->status = VISITED; + DFSNodeVisit(node, finishNodes, false, false, 0); + node->status = FINISHED; + finishNodes->push(node); + } + } + delete iterator; +} + +void DFSReverse(OrderGraph *graph, Vector *finishNodes) { + uint size = finishNodes->getSize(); + uint sccNum = 1; + for (int i = size - 1; i >= 0; i--) { + OrderNode *node = finishNodes->get(i); + if (node->status == NOTVISITED) { + node->status = VISITED; + DFSNodeVisit(node, NULL, true, false, sccNum); + node->sccNum = sccNum; + node->status = FINISHED; + sccNum++; + } + } +} + +void DFSNodeVisit(OrderNode *node, Vector *finishNodes, bool isReverse, bool mustvisit, uint sccNum) { + HSIteratorOrderEdge *iterator = isReverse ? node->inEdges.iterator() : node->outEdges.iterator(); + while (iterator->hasNext()) { + OrderEdge *edge = iterator->next(); + if (mustvisit) { + if (!edge->mustPos) + continue; + } else + if (!edge->polPos && !edge->pseudoPos) //Ignore edges that do not have positive polarity + continue; + + OrderNode *child = isReverse ? edge->source : edge->sink; + + if (child->status == NOTVISITED) { + child->status = VISITED; + DFSNodeVisit(child, finishNodes, isReverse, mustvisit, sccNum); + child->status = FINISHED; + if (finishNodes != NULL) + finishNodes->push(child); + if (isReverse) + child->sccNum = sccNum; + } + } + delete iterator; +} + +void resetNodeInfoStatusSCC(OrderGraph *graph) { + HSIteratorOrderNode *iterator = graph->getNodes(); + while (iterator->hasNext()) { + iterator->next()->status = NOTVISITED; + } + delete iterator; +} + +void computeStronglyConnectedComponentGraph(OrderGraph *graph) { + Vector finishNodes; + DFS(graph, &finishNodes); + resetNodeInfoStatusSCC(graph); + DFSReverse(graph, &finishNodes); + resetNodeInfoStatusSCC(graph); +} + +bool isMustBeTrueNode(OrderNode *node) { + HSIteratorOrderEdge *iterator = node->inEdges.iterator(); + while (iterator->hasNext()) { + OrderEdge *edge = iterator->next(); + if (!edge->mustPos) + return false; + } + delete iterator; + iterator = node->outEdges.iterator(); + while (iterator->hasNext()) { + OrderEdge *edge = iterator->next(); + if (!edge->mustPos) + return false; + } + delete iterator; + return true; +} + +void bypassMustBeTrueNode(CSolver *This, OrderGraph *graph, OrderNode *node) { + HSIteratorOrderEdge *iterin = node->inEdges.iterator(); + while (iterin->hasNext()) { + OrderEdge *inEdge = iterin->next(); + OrderNode *srcNode = inEdge->source; + srcNode->outEdges.remove(inEdge); + HSIteratorOrderEdge *iterout = node->outEdges.iterator(); + while (iterout->hasNext()) { + OrderEdge *outEdge = iterout->next(); + OrderNode *sinkNode = outEdge->sink; + sinkNode->inEdges.remove(outEdge); + //Adding new edge to new sink and src nodes ... + OrderEdge *newEdge = graph->getOrderEdgeFromOrderGraph(srcNode, sinkNode); + newEdge->mustPos = true; + newEdge->polPos = true; + if (newEdge->mustNeg) + This->setUnSAT(); + srcNode->outEdges.add(newEdge); + sinkNode->inEdges.add(newEdge); + } + delete iterout; + } + delete iterin; +} + +void removeMustBeTrueNodes(CSolver *This, OrderGraph *graph) { + HSIteratorOrderNode *iterator = graph->getNodes(); + while (iterator->hasNext()) { + OrderNode *node = iterator->next(); + if (isMustBeTrueNode(node)) { + bypassMustBeTrueNode(This, graph, node); + } + } + delete iterator; +} + +/** This function computes a source set for every nodes, the set of + nodes that can reach that node via pospolarity edges. It then + looks for negative polarity edges from nodes in the the source set + to determine whether we need to generate pseudoPos edges. */ + +void completePartialOrderGraph(OrderGraph *graph) { + Vector finishNodes; + DFS(graph, &finishNodes); + resetNodeInfoStatusSCC(graph); + HashTableNodeToNodeSet *table = new HashTableNodeToNodeSet(128, 0.25); + + Vector sccNodes; + + uint size = finishNodes.getSize(); + uint sccNum = 1; + for (int i = size - 1; i >= 0; i--) { + OrderNode *node = finishNodes.get(i); + HashSetOrderNode *sources = new HashSetOrderNode(4, 0.25); + table->put(node, sources); + + if (node->status == NOTVISITED) { + //Need to do reverse traversal here... + node->status = VISITED; + DFSNodeVisit(node, &sccNodes, true, false, sccNum); + node->status = FINISHED; + node->sccNum = sccNum; + sccNum++; + sccNodes.push(node); + + //Compute in set for entire SCC + uint rSize = sccNodes.getSize(); + for (uint j = 0; j < rSize; j++) { + OrderNode *rnode = sccNodes.get(j); + //Compute source sets + HSIteratorOrderEdge *iterator = rnode->inEdges.iterator(); + while (iterator->hasNext()) { + OrderEdge *edge = iterator->next(); + OrderNode *parent = edge->source; + if (edge->polPos) { + sources->add(parent); + HashSetOrderNode *parent_srcs = (HashSetOrderNode *)table->get(parent); + sources->addAll(parent_srcs); + } + } + delete iterator; + } + for (uint j = 0; j < rSize; j++) { + //Copy in set of entire SCC + OrderNode *rnode = sccNodes.get(j); + HashSetOrderNode *set = (j == 0) ? sources : sources->copy(); + table->put(rnode, set); + + //Use source sets to compute pseudoPos edges + HSIteratorOrderEdge *iterator = node->inEdges.iterator(); + while (iterator->hasNext()) { + OrderEdge *edge = iterator->next(); + OrderNode *parent = edge->source; + ASSERT(parent != rnode); + if (edge->polNeg && parent->sccNum != rnode->sccNum && + sources->contains(parent)) { + OrderEdge *newedge = graph->getOrderEdgeFromOrderGraph(rnode, parent); + newedge->pseudoPos = true; + } + } + delete iterator; + } + + sccNodes.clear(); + } + } + + table->resetanddelete(); + delete table; + resetNodeInfoStatusSCC(graph); +} + +void DFSMust(OrderGraph *graph, Vector *finishNodes) { + HSIteratorOrderNode *iterator = graph->getNodes(); + while (iterator->hasNext()) { + OrderNode *node = iterator->next(); + if (node->status == NOTVISITED) { + node->status = VISITED; + DFSNodeVisit(node, finishNodes, false, true, 0); + node->status = FINISHED; + finishNodes->push(node); + } + } + delete iterator; +} + +void DFSClearContradictions(CSolver *solver, OrderGraph *graph, Vector *finishNodes, bool computeTransitiveClosure) { + uint size = finishNodes->getSize(); + HashTableNodeToNodeSet *table = new HashTableNodeToNodeSet(128, 0.25); + + for (int i = size - 1; i >= 0; i--) { + OrderNode *node = finishNodes->get(i); + HashSetOrderNode *sources = new HashSetOrderNode(4, 0.25); + table->put(node, sources); + + { + //Compute source sets + HSIteratorOrderEdge *iterator = node->inEdges.iterator(); + while (iterator->hasNext()) { + OrderEdge *edge = iterator->next(); + OrderNode *parent = edge->source; + if (edge->mustPos) { + sources->add(parent); + HashSetOrderNode *parent_srcs = (HashSetOrderNode *) table->get(parent); + sources->addAll(parent_srcs); + } + } + delete iterator; + } + if (computeTransitiveClosure) { + //Compute full transitive closure for nodes + HSIteratorOrderNode *srciterator = sources->iterator(); + while (srciterator->hasNext()) { + OrderNode *srcnode = srciterator->next(); + OrderEdge *newedge = graph->getOrderEdgeFromOrderGraph(srcnode, node); + newedge->mustPos = true; + newedge->polPos = true; + if (newedge->mustNeg) + solver->setUnSAT(); + srcnode->outEdges.add(newedge); + node->inEdges.add(newedge); + } + delete srciterator; + } + { + //Use source sets to compute mustPos edges + HSIteratorOrderEdge *iterator = node->inEdges.iterator(); + while (iterator->hasNext()) { + OrderEdge *edge = iterator->next(); + OrderNode *parent = edge->source; + if (!edge->mustPos && sources->contains(parent)) { + edge->mustPos = true; + edge->polPos = true; + if (edge->mustNeg) + solver->setUnSAT(); + } + } + delete iterator; + } + { + //Use source sets to compute mustNeg for edges that would introduce cycle if true + HSIteratorOrderEdge *iterator = node->outEdges.iterator(); + while (iterator->hasNext()) { + OrderEdge *edge = iterator->next(); + OrderNode *child = edge->sink; + if (!edge->mustNeg && sources->contains(child)) { + edge->mustNeg = true; + edge->polNeg = true; + if (edge->mustPos) + solver->setUnSAT(); + } + } + delete iterator; + } + } + + table->resetanddelete(); + delete table; +} + +/* This function finds edges that would form a cycle with must edges + and forces them to be mustNeg. It also decides whether an edge + must be true because of transitivity from other must be true + edges. */ + +void reachMustAnalysis(CSolver *solver, OrderGraph *graph, bool computeTransitiveClosure) { + Vector finishNodes; + //Topologically sort the mustPos edge graph + DFSMust(graph, &finishNodes); + resetNodeInfoStatusSCC(graph); + + //Find any backwards edges that complete cycles and force them to be mustNeg + DFSClearContradictions(solver, graph, &finishNodes, computeTransitiveClosure); +} + +/* This function finds edges that must be positive and forces the + inverse edge to be negative (and clears its positive polarity if it + had one). */ + +void localMustAnalysisTotal(CSolver *solver, OrderGraph *graph) { + HSIteratorOrderEdge *iterator = graph->getEdges(); + while (iterator->hasNext()) { + OrderEdge *edge = iterator->next(); + if (edge->mustPos) { + OrderEdge *invEdge = graph->getInverseOrderEdge(edge); + if (invEdge != NULL) { + if (!invEdge->mustPos) { + invEdge->polPos = false; + } else { + solver->setUnSAT(); + } + invEdge->mustNeg = true; + invEdge->polNeg = true; + } + } + } + delete iterator; +} + +/** This finds edges that must be positive and forces the inverse edge + to be negative. It also clears the negative flag of this edge. + It also finds edges that must be negative and clears the positive + polarity. */ + +void localMustAnalysisPartial(CSolver *solver, OrderGraph *graph) { + HSIteratorOrderEdge *iterator = graph->getEdges(); + while (iterator->hasNext()) { + OrderEdge *edge = iterator->next(); + if (edge->mustPos) { + if (!edge->mustNeg) { + edge->polNeg = false; + } else + solver->setUnSAT(); + + OrderEdge *invEdge = graph->getInverseOrderEdge(edge); + if (invEdge != NULL) { + if (!invEdge->mustPos) + invEdge->polPos = false; + else + solver->setUnSAT(); + + invEdge->mustNeg = true; + invEdge->polNeg = true; + } + } + if (edge->mustNeg && !edge->mustPos) { + edge->polPos = false; + } + } + delete iterator; +} diff --git a/src/ASTAnalyses/orderanalysis.h b/src/ASTAnalyses/orderanalysis.h new file mode 100644 index 0000000..9a8daf9 --- /dev/null +++ b/src/ASTAnalyses/orderanalysis.h @@ -0,0 +1,25 @@ +#ifndef ORDERANALYSIS_H +#define ORDERANALYSIS_H +#include "classlist.h" +#include "structs.h" +#include "mymemory.h" + +void computeStronglyConnectedComponentGraph(OrderGraph *graph); +void initializeNodeInfoSCC(OrderGraph *graph); +void DFSNodeVisit(OrderNode *node, Vector *finishNodes, bool isReverse, bool mustvisit, uint sccNum); +void DFS(OrderGraph *graph, Vector *finishNodes); +void DFSReverse(OrderGraph *graph, Vector *finishNodes); +void completePartialOrderGraph(OrderGraph *graph); +void resetNodeInfoStatusSCC(OrderGraph *graph); +bool isMustBeTrueNode(OrderNode *node); +void bypassMustBeTrueNode(CSolver *This, OrderGraph *graph, OrderNode *node); +void removeMustBeTrueNodes(CSolver *This, OrderGraph *graph); +void completePartialOrderGraph(OrderGraph *graph); +void DFSMust(OrderGraph *graph, Vector *finishNodes); +void DFSClearContradictions(CSolver *solver, OrderGraph *graph, Vector *finishNodes, bool computeTransitiveClosure); +void reachMustAnalysis(CSolver *solver, OrderGraph *graph, bool computeTransitiveClosure); +void localMustAnalysisTotal(CSolver *solver, OrderGraph *graph); +void localMustAnalysisPartial(CSolver *solver, OrderGraph *graph); + +#endif + diff --git a/src/ASTAnalyses/orderencoder.cc b/src/ASTAnalyses/orderencoder.cc deleted file mode 100644 index 5d94206..0000000 --- a/src/ASTAnalyses/orderencoder.cc +++ /dev/null @@ -1,371 +0,0 @@ -#include "orderencoder.h" -#include "structs.h" -#include "csolver.h" -#include "boolean.h" -#include "ordergraph.h" -#include "order.h" -#include "ordernode.h" -#include "rewriter.h" -#include "mutableset.h" -#include "tunable.h" - -void DFS(OrderGraph *graph, Vector *finishNodes) { - HSIteratorOrderNode *iterator = graph->getNodes(); - while (iterator->hasNext()) { - OrderNode *node = iterator->next(); - if (node->status == NOTVISITED) { - node->status = VISITED; - DFSNodeVisit(node, finishNodes, false, false, 0); - node->status = FINISHED; - finishNodes->push(node); - } - } - delete iterator; -} - -void DFSReverse(OrderGraph *graph, Vector *finishNodes) { - uint size = finishNodes->getSize(); - uint sccNum = 1; - for (int i = size - 1; i >= 0; i--) { - OrderNode *node = finishNodes->get(i); - if (node->status == NOTVISITED) { - node->status = VISITED; - DFSNodeVisit(node, NULL, true, false, sccNum); - node->sccNum = sccNum; - node->status = FINISHED; - sccNum++; - } - } -} - -void DFSNodeVisit(OrderNode *node, Vector *finishNodes, bool isReverse, bool mustvisit, uint sccNum) { - HSIteratorOrderEdge *iterator = isReverse ? node->inEdges.iterator() : node->outEdges.iterator(); - while (iterator->hasNext()) { - OrderEdge *edge = iterator->next(); - if (mustvisit) { - if (!edge->mustPos) - continue; - } else - if (!edge->polPos && !edge->pseudoPos) //Ignore edges that do not have positive polarity - continue; - - OrderNode *child = isReverse ? edge->source : edge->sink; - - if (child->status == NOTVISITED) { - child->status = VISITED; - DFSNodeVisit(child, finishNodes, isReverse, mustvisit, sccNum); - child->status = FINISHED; - if (finishNodes != NULL) - finishNodes->push(child); - if (isReverse) - child->sccNum = sccNum; - } - } - delete iterator; -} - -void resetNodeInfoStatusSCC(OrderGraph *graph) { - HSIteratorOrderNode *iterator = graph->getNodes(); - while (iterator->hasNext()) { - iterator->next()->status = NOTVISITED; - } - delete iterator; -} - -void computeStronglyConnectedComponentGraph(OrderGraph *graph) { - Vector finishNodes; - DFS(graph, &finishNodes); - resetNodeInfoStatusSCC(graph); - DFSReverse(graph, &finishNodes); - resetNodeInfoStatusSCC(graph); -} - -bool isMustBeTrueNode(OrderNode *node) { - HSIteratorOrderEdge *iterator = node->inEdges.iterator(); - while (iterator->hasNext()) { - OrderEdge *edge = iterator->next(); - if (!edge->mustPos) - return false; - } - delete iterator; - iterator = node->outEdges.iterator(); - while (iterator->hasNext()) { - OrderEdge *edge = iterator->next(); - if (!edge->mustPos) - return false; - } - delete iterator; - return true; -} - -void bypassMustBeTrueNode(CSolver *This, OrderGraph *graph, OrderNode *node) { - HSIteratorOrderEdge *iterin = node->inEdges.iterator(); - while (iterin->hasNext()) { - OrderEdge *inEdge = iterin->next(); - OrderNode *srcNode = inEdge->source; - srcNode->outEdges.remove(inEdge); - HSIteratorOrderEdge *iterout = node->outEdges.iterator(); - while (iterout->hasNext()) { - OrderEdge *outEdge = iterout->next(); - OrderNode *sinkNode = outEdge->sink; - sinkNode->inEdges.remove(outEdge); - //Adding new edge to new sink and src nodes ... - OrderEdge *newEdge = graph->getOrderEdgeFromOrderGraph(srcNode, sinkNode); - newEdge->mustPos = true; - newEdge->polPos = true; - if (newEdge->mustNeg) - This->setUnSAT(); - srcNode->outEdges.add(newEdge); - sinkNode->inEdges.add(newEdge); - } - delete iterout; - } - delete iterin; -} - -void removeMustBeTrueNodes(CSolver *This, OrderGraph *graph) { - HSIteratorOrderNode *iterator = graph->getNodes(); - while (iterator->hasNext()) { - OrderNode *node = iterator->next(); - if (isMustBeTrueNode(node)) { - bypassMustBeTrueNode(This, graph, node); - } - } - delete iterator; -} - -/** This function computes a source set for every nodes, the set of - nodes that can reach that node via pospolarity edges. It then - looks for negative polarity edges from nodes in the the source set - to determine whether we need to generate pseudoPos edges. */ - -void completePartialOrderGraph(OrderGraph *graph) { - Vector finishNodes; - DFS(graph, &finishNodes); - resetNodeInfoStatusSCC(graph); - HashTableNodeToNodeSet *table = new HashTableNodeToNodeSet(128, 0.25); - - Vector sccNodes; - - uint size = finishNodes.getSize(); - uint sccNum = 1; - for (int i = size - 1; i >= 0; i--) { - OrderNode *node = finishNodes.get(i); - HashSetOrderNode *sources = new HashSetOrderNode(4, 0.25); - table->put(node, sources); - - if (node->status == NOTVISITED) { - //Need to do reverse traversal here... - node->status = VISITED; - DFSNodeVisit(node, &sccNodes, true, false, sccNum); - node->status = FINISHED; - node->sccNum = sccNum; - sccNum++; - sccNodes.push(node); - - //Compute in set for entire SCC - uint rSize = sccNodes.getSize(); - for (uint j = 0; j < rSize; j++) { - OrderNode *rnode = sccNodes.get(j); - //Compute source sets - HSIteratorOrderEdge *iterator = rnode->inEdges.iterator(); - while (iterator->hasNext()) { - OrderEdge *edge = iterator->next(); - OrderNode *parent = edge->source; - if (edge->polPos) { - sources->add(parent); - HashSetOrderNode *parent_srcs = (HashSetOrderNode *)table->get(parent); - sources->addAll(parent_srcs); - } - } - delete iterator; - } - for (uint j = 0; j < rSize; j++) { - //Copy in set of entire SCC - OrderNode *rnode = sccNodes.get(j); - HashSetOrderNode *set = (j == 0) ? sources : sources->copy(); - table->put(rnode, set); - - //Use source sets to compute pseudoPos edges - HSIteratorOrderEdge *iterator = node->inEdges.iterator(); - while (iterator->hasNext()) { - OrderEdge *edge = iterator->next(); - OrderNode *parent = edge->source; - ASSERT(parent != rnode); - if (edge->polNeg && parent->sccNum != rnode->sccNum && - sources->contains(parent)) { - OrderEdge *newedge = graph->getOrderEdgeFromOrderGraph(rnode, parent); - newedge->pseudoPos = true; - } - } - delete iterator; - } - - sccNodes.clear(); - } - } - - table->resetanddelete(); - delete table; - resetNodeInfoStatusSCC(graph); -} - -void DFSMust(OrderGraph *graph, Vector *finishNodes) { - HSIteratorOrderNode *iterator = graph->getNodes(); - while (iterator->hasNext()) { - OrderNode *node = iterator->next(); - if (node->status == NOTVISITED) { - node->status = VISITED; - DFSNodeVisit(node, finishNodes, false, true, 0); - node->status = FINISHED; - finishNodes->push(node); - } - } - delete iterator; -} - -void DFSClearContradictions(CSolver *solver, OrderGraph *graph, Vector *finishNodes, bool computeTransitiveClosure) { - uint size = finishNodes->getSize(); - HashTableNodeToNodeSet *table = new HashTableNodeToNodeSet(128, 0.25); - - for (int i = size - 1; i >= 0; i--) { - OrderNode *node = finishNodes->get(i); - HashSetOrderNode *sources = new HashSetOrderNode(4, 0.25); - table->put(node, sources); - - { - //Compute source sets - HSIteratorOrderEdge *iterator = node->inEdges.iterator(); - while (iterator->hasNext()) { - OrderEdge *edge = iterator->next(); - OrderNode *parent = edge->source; - if (edge->mustPos) { - sources->add(parent); - HashSetOrderNode *parent_srcs = (HashSetOrderNode *) table->get(parent); - sources->addAll(parent_srcs); - } - } - delete iterator; - } - if (computeTransitiveClosure) { - //Compute full transitive closure for nodes - HSIteratorOrderNode *srciterator = sources->iterator(); - while (srciterator->hasNext()) { - OrderNode *srcnode = srciterator->next(); - OrderEdge *newedge = graph->getOrderEdgeFromOrderGraph(srcnode, node); - newedge->mustPos = true; - newedge->polPos = true; - if (newedge->mustNeg) - solver->setUnSAT(); - srcnode->outEdges.add(newedge); - node->inEdges.add(newedge); - } - delete srciterator; - } - { - //Use source sets to compute mustPos edges - HSIteratorOrderEdge *iterator = node->inEdges.iterator(); - while (iterator->hasNext()) { - OrderEdge *edge = iterator->next(); - OrderNode *parent = edge->source; - if (!edge->mustPos && sources->contains(parent)) { - edge->mustPos = true; - edge->polPos = true; - if (edge->mustNeg) - solver->setUnSAT(); - } - } - delete iterator; - } - { - //Use source sets to compute mustNeg for edges that would introduce cycle if true - HSIteratorOrderEdge *iterator = node->outEdges.iterator(); - while (iterator->hasNext()) { - OrderEdge *edge = iterator->next(); - OrderNode *child = edge->sink; - if (!edge->mustNeg && sources->contains(child)) { - edge->mustNeg = true; - edge->polNeg = true; - if (edge->mustPos) - solver->setUnSAT(); - } - } - delete iterator; - } - } - - table->resetanddelete(); - delete table; -} - -/* This function finds edges that would form a cycle with must edges - and forces them to be mustNeg. It also decides whether an edge - must be true because of transitivity from other must be true - edges. */ - -void reachMustAnalysis(CSolver *solver, OrderGraph *graph, bool computeTransitiveClosure) { - Vector finishNodes; - //Topologically sort the mustPos edge graph - DFSMust(graph, &finishNodes); - resetNodeInfoStatusSCC(graph); - - //Find any backwards edges that complete cycles and force them to be mustNeg - DFSClearContradictions(solver, graph, &finishNodes, computeTransitiveClosure); -} - -/* This function finds edges that must be positive and forces the - inverse edge to be negative (and clears its positive polarity if it - had one). */ - -void localMustAnalysisTotal(CSolver *solver, OrderGraph *graph) { - HSIteratorOrderEdge *iterator = graph->getEdges(); - while (iterator->hasNext()) { - OrderEdge *edge = iterator->next(); - if (edge->mustPos) { - OrderEdge *invEdge = graph->getInverseOrderEdge(edge); - if (invEdge != NULL) { - if (!invEdge->mustPos) { - invEdge->polPos = false; - } else { - solver->setUnSAT(); - } - invEdge->mustNeg = true; - invEdge->polNeg = true; - } - } - } - delete iterator; -} - -/** This finds edges that must be positive and forces the inverse edge - to be negative. It also clears the negative flag of this edge. - It also finds edges that must be negative and clears the positive - polarity. */ - -void localMustAnalysisPartial(CSolver *solver, OrderGraph *graph) { - HSIteratorOrderEdge *iterator = graph->getEdges(); - while (iterator->hasNext()) { - OrderEdge *edge = iterator->next(); - if (edge->mustPos) { - if (!edge->mustNeg) { - edge->polNeg = false; - } else - solver->setUnSAT(); - - OrderEdge *invEdge = graph->getInverseOrderEdge(edge); - if (invEdge != NULL) { - if (!invEdge->mustPos) - invEdge->polPos = false; - else - solver->setUnSAT(); - - invEdge->mustNeg = true; - invEdge->polNeg = true; - } - } - if (edge->mustNeg && !edge->mustPos) { - edge->polPos = false; - } - } - delete iterator; -} diff --git a/src/ASTAnalyses/orderencoder.h b/src/ASTAnalyses/orderencoder.h deleted file mode 100644 index 57a6e5c..0000000 --- a/src/ASTAnalyses/orderencoder.h +++ /dev/null @@ -1,32 +0,0 @@ -/* - * File: orderencoder.h - * Author: hamed - * - * Created on August 8, 2017, 6:36 PM - */ - -#ifndef ORDERGRAPHBUILDER_H -#define ORDERGRAPHBUILDER_H -#include "classlist.h" -#include "structs.h" -#include "mymemory.h" - -void computeStronglyConnectedComponentGraph(OrderGraph *graph); -void initializeNodeInfoSCC(OrderGraph *graph); -void DFSNodeVisit(OrderNode *node, Vector *finishNodes, bool isReverse, bool mustvisit, uint sccNum); -void DFS(OrderGraph *graph, Vector *finishNodes); -void DFSReverse(OrderGraph *graph, Vector *finishNodes); -void completePartialOrderGraph(OrderGraph *graph); -void resetNodeInfoStatusSCC(OrderGraph *graph); -bool isMustBeTrueNode(OrderNode *node); -void bypassMustBeTrueNode(CSolver *This, OrderGraph *graph, OrderNode *node); -void removeMustBeTrueNodes(CSolver *This, OrderGraph *graph); -void completePartialOrderGraph(OrderGraph *graph); -void DFSMust(OrderGraph *graph, Vector *finishNodes); -void DFSClearContradictions(CSolver *solver, OrderGraph *graph, Vector *finishNodes, bool computeTransitiveClosure); -void reachMustAnalysis(CSolver *solver, OrderGraph *graph, bool computeTransitiveClosure); -void localMustAnalysisTotal(CSolver *solver, OrderGraph *graph); -void localMustAnalysisPartial(CSolver *solver, OrderGraph *graph); - -#endif/* ORDERGRAPHBUILDER_H */ - diff --git a/src/ASTTransform/orderdecompose.cc b/src/ASTTransform/orderdecompose.cc index 18602cc..9a60497 100644 --- a/src/ASTTransform/orderdecompose.cc +++ b/src/ASTTransform/orderdecompose.cc @@ -9,7 +9,7 @@ #include "mutableset.h" #include "ops.h" #include "csolver.h" -#include "orderencoder.h" +#include "orderanalysis.h" #include "tunable.h" #include "integerencoding.h" diff --git a/src/Backend/satorderencoder.cc b/src/Backend/satorderencoder.cc index 20d163b..750be42 100644 --- a/src/Backend/satorderencoder.cc +++ b/src/Backend/satorderencoder.cc @@ -6,7 +6,7 @@ #include "orderpair.h" #include "set.h" #include "tunable.h" -#include "orderencoder.h" +#include "orderanalysis.h" #include "ordergraph.h" #include "orderedge.h" #include "element.h" diff --git a/src/Tuner/autotuner.cc b/src/Tuner/autotuner.cc index 37a9d07..e1868c1 100644 --- a/src/Tuner/autotuner.cc +++ b/src/Tuner/autotuner.cc @@ -1,3 +1,7 @@ #include "autotuner.h" #include "csolver.h" +void AutoTuner::tune(CSolver *base) { + + +}