From 3d7a27487ec88670a2815e9193c5f6580e8eb396 Mon Sep 17 00:00:00 2001 From: bdemsky Date: Sat, 21 Oct 2017 23:57:54 -0700 Subject: [PATCH] More edits --- src/AST/boolean.cc | 3 + src/AST/boolean.h | 3 +- src/ASTTransform/decomposeordertransform.cc | 151 ++++++++++++++++---- src/ASTTransform/decomposeordertransform.h | 9 +- src/Tuner/tunable.h | 2 +- src/csolver.cc | 24 +++- 6 files changed, 160 insertions(+), 32 deletions(-) diff --git a/src/AST/boolean.cc b/src/AST/boolean.cc index f7d3e88..dcc201d 100644 --- a/src/AST/boolean.cc +++ b/src/AST/boolean.cc @@ -28,6 +28,9 @@ BooleanOrder::BooleanOrder(Order *_order, uint64_t _first, uint64_t _second) : order(_order), first(_first), second(_second) { +} + +void BooleanOrder::updateParents() { order->constraints.push(this); } diff --git a/src/AST/boolean.h b/src/AST/boolean.h index 9864d9b..467ceb1 100644 --- a/src/AST/boolean.h +++ b/src/AST/boolean.h @@ -56,7 +56,8 @@ public: Boolean *clone(CSolver *solver, CloneMap *map); void serialize(Serializer *serializer ); virtual void print(); - + void updateParents(); + Order *order; uint64_t first; uint64_t second; diff --git a/src/ASTTransform/decomposeordertransform.cc b/src/ASTTransform/decomposeordertransform.cc index 1e0426c..d5bb5cf 100644 --- a/src/ASTTransform/decomposeordertransform.cc +++ b/src/ASTTransform/decomposeordertransform.cc @@ -62,18 +62,20 @@ void DecomposeOrderTransform::doTransform() { } bool mustReachPrune = GETVARTUNABLE(solver->getTuner(), order->type, MUSTREACHPRUNE, &onoff); - HashsetOrderEdge *edgesRemoved = NULL; if (mustReachPrune) { - edgesRemoved = new HashsetOrderEdge(); - removeMustBeTrueNodes(graph, edgesRemoved); + removeMustBeTrueNodes(graph, dor); + } + + bool pruneEdges = GETVARTUNABLE(solver->getTuner(), order->type, MUSTEDGEPRUNE, &onoff); + + if (pruneEdges) { + mustEdgePrune(graph, dor); } //This is needed for splitorder graph->computeStronglyConnectedComponentGraph(); - decomposeOrder(order, graph, edgesRemoved, dor); - if (edgesRemoved != NULL) - delete edgesRemoved; + decomposeOrder(order, graph, dor); delete graph; } delete orderit; @@ -81,7 +83,7 @@ void DecomposeOrderTransform::doTransform() { } -void DecomposeOrderTransform::decomposeOrder(Order *currOrder, OrderGraph *currGraph, HashsetOrderEdge *edgesRemoved, DecomposeOrderResolver *dor) { +void DecomposeOrderTransform::decomposeOrder(Order *currOrder, OrderGraph *currGraph, DecomposeOrderResolver *dor) { Vector partialcandidatevec; uint size = currOrder->constraints.getSize(); for (uint i = 0; i < size; i++) { @@ -90,17 +92,8 @@ void DecomposeOrderTransform::decomposeOrder(Order *currOrder, OrderGraph *currG OrderNode *to = currGraph->getOrderNodeFromOrderGraph(orderconstraint->second); OrderEdge *edge = currGraph->lookupOrderEdgeFromOrderGraph(from, to); OrderEdge *invedge = currGraph->lookupOrderEdgeFromOrderGraph(to, from); - if (edgesRemoved != NULL) { - if (edgesRemoved->contains(edge)) { - dor->mustOrderEdge(from->getID(), to->getID()); - solver->replaceBooleanWithTrue(orderconstraint); - continue; - } else if (edgesRemoved->contains(invedge)) { - dor->mustOrderEdge(to->getID(), from->getID()); - solver->replaceBooleanWithFalse(orderconstraint); - continue; - } - } + if (from->removed || to->removed) + continue; if (from->sccNum != to->sccNum) { if (edge != NULL) { @@ -158,9 +151,10 @@ void DecomposeOrderTransform::decomposeOrder(Order *currOrder, OrderGraph *currG if (edge->polNeg) partialcandidatevec.setExpand(from->sccNum, NULL); } - orderconstraint->order = neworder; + BooleanEdge neworderconstraint=solver->orderConstraint(neworder, orderconstraint->first, orderconstraint->second); + solver->replaceBooleanWithBoolean(orderconstraint, neworderconstraint); + dor->setEdgeOrder(from->getID(), to->getID(), from->sccNum); - neworder->addOrderConstraint(orderconstraint); } } solver->getActiveOrders()->remove(currOrder); @@ -195,14 +189,17 @@ bool DecomposeOrderTransform::isMustBeTrueNode(OrderNode *node) { return true; } -void DecomposeOrderTransform::bypassMustBeTrueNode(OrderGraph *graph, OrderNode *node, HashsetOrderEdge *edgesRemoved) { +void DecomposeOrderTransform::bypassMustBeTrueNode(OrderGraph *graph, OrderNode *node, DecomposeOrderResolver *dor) { node->removed = true; + model_print("Removing %llu\n", node->getID()); SetIteratorOrderEdge *iterin = node->inEdges.iterator(); while (iterin->hasNext()) { OrderEdge *inEdge = iterin->next(); OrderNode *srcNode = inEdge->source; srcNode->outEdges.remove(inEdge); - edgesRemoved->add(inEdge); + dor->mustOrderEdge(srcNode->getID(), node->getID()); + BooleanEdge be=solver->orderConstraint(graph->getOrder(), srcNode->getID(), node->getID()); + solver->replaceBooleanWithTrue(be); bool removeOutgoingEdges = !iterin->hasNext(); SetIteratorOrderEdge *iterout = node->outEdges.iterator(); @@ -210,8 +207,10 @@ void DecomposeOrderTransform::bypassMustBeTrueNode(OrderGraph *graph, OrderNode OrderEdge *outEdge = iterout->next(); OrderNode *sinkNode = outEdge->sink; if (removeOutgoingEdges) { + dor->mustOrderEdge(node->getID(), sinkNode->getID()); sinkNode->inEdges.remove(outEdge); - edgesRemoved->add(outEdge); + BooleanEdge be2=solver->orderConstraint(graph->getOrder(), node->getID(), sinkNode->getID()); + solver->replaceBooleanWithTrue(be2); } //Adding new edge to new sink and src nodes ... if (srcNode == sinkNode) { @@ -238,13 +237,115 @@ void DecomposeOrderTransform::bypassMustBeTrueNode(OrderGraph *graph, OrderNode delete iterin; } -void DecomposeOrderTransform::removeMustBeTrueNodes(OrderGraph *graph, HashsetOrderEdge *edgesRemoved) { +void DecomposeOrderTransform::removeMustBeTrueNodes(OrderGraph *graph, DecomposeOrderResolver *dor) { SetIteratorOrderNode *iterator = graph->getNodes(); while (iterator->hasNext()) { OrderNode *node = iterator->next(); + if (node->removed) + continue; if (isMustBeTrueNode(node)) { - bypassMustBeTrueNode(graph, node, edgesRemoved); + bypassMustBeTrueNode(graph, node, dor); } } delete iterator; } + +void DecomposeOrderTransform::mustEdgePrune(OrderGraph *graph, DecomposeOrderResolver *dor) { + SetIteratorOrderNode *iterator = graph->getNodes(); + while (iterator->hasNext()) { + OrderNode *node = iterator->next(); + if (node->removed) + continue; + attemptNodeMerge(graph, node, dor); + } + delete iterator; +} + +void DecomposeOrderTransform::attemptNodeMerge(OrderGraph *graph, OrderNode *node, DecomposeOrderResolver *dor) { + SetIteratorOrderEdge * edgeit = node->outEdges.iterator(); + while(edgeit->hasNext()) { + OrderEdge *outedge=edgeit->next(); + OrderNode *dstnode=outedge->sink; + uint numOutEdges=node->outEdges.getSize(); + uint numInEdges=dstnode->inEdges.getSize(); + /* + Need to avoid a situation where we create new reachability by + the merge. This can only happen if there is an extra in edge to + the dstnode and an extra out edge to our node. + */ + + if (numOutEdges == 1 || numInEdges == 1) { + /* Safe to do the Merge */ + mergeNodes(graph, node, outedge, dstnode, dor); + + //Throw away the iterator and start over + delete edgeit; + edgeit=node->outEdges.iterator(); + } + } + delete edgeit; +} + +void DecomposeOrderTransform::mergeNodes(OrderGraph *graph, OrderNode *node, OrderEdge *edge, OrderNode *dstnode, DecomposeOrderResolver *dor) { + /* Fix up must edge between the two nodes */ + node->outEdges.remove(edge); + dstnode->inEdges.remove(edge); + dor->mustOrderEdge(node->getID(), dstnode->getID()); + + /* Go through the incoming edges to the new node */ + SetIteratorOrderEdge *inedgeit=dstnode->inEdges.iterator(); + while(inedgeit->hasNext()) { + OrderEdge *inedge=inedgeit->next(); + OrderNode *source=inedge->source; + //remove it from the source node + source->outEdges.remove(inedge); + //save the remapping that we did + dor->remapEdge(source->getID(), dstnode->getID(), source->getID(), node->getID()); + //create the new edge + OrderEdge *newedge=graph->getOrderEdgeFromOrderGraph(source, node); + //update the flags + newedge->polPos |= inedge->polPos; + newedge->polNeg |= inedge->polNeg; + newedge->mustPos |= inedge->mustPos; + newedge->mustNeg |= inedge->mustNeg; + newedge->pseudoPos |= inedge->pseudoPos; + //add new edge to both + source->outEdges.add(newedge); + node->inEdges.add(newedge); + + BooleanEdge be=solver->orderConstraint(graph->getOrder(), source->getID(), dstnode->getID()); + BooleanEdge benew=solver->orderConstraint(graph->getOrder(), source->getID(), node->getID()); + solver->replaceBooleanWithBoolean(be, benew); + + } + dstnode->inEdges.reset(); + delete inedgeit; + + /* Go through the outgoing edges from the new node */ + SetIteratorOrderEdge *outedgeit=dstnode->outEdges.iterator(); + while(outedgeit->hasNext()) { + OrderEdge *outedge=outedgeit->next(); + OrderNode *sink=outedge->sink; + //remove it from the sink node + sink->inEdges.remove(outedge); + //save the remapping that we did + dor->remapEdge(dstnode->getID(), sink->getID(), node->getID(), sink->getID()); + //create the new edge + OrderEdge *newedge=graph->getOrderEdgeFromOrderGraph(node, sink); + //update the flags + newedge->polPos |= outedge->polPos; + newedge->polNeg |= outedge->polNeg; + newedge->mustPos |= outedge->mustPos; + newedge->mustNeg |= outedge->mustNeg; + newedge->pseudoPos |= outedge->pseudoPos; + //add new edge to both + sink->inEdges.add(newedge); + node->outEdges.add(newedge); + //add it to the remove set + } + dstnode->outEdges.reset(); + delete outedgeit; + + /* Mark destination as removed */ + dstnode->removed = true; +} diff --git a/src/ASTTransform/decomposeordertransform.h b/src/ASTTransform/decomposeordertransform.h index 3f8092f..9020e1c 100644 --- a/src/ASTTransform/decomposeordertransform.h +++ b/src/ASTTransform/decomposeordertransform.h @@ -20,9 +20,12 @@ public: CMEMALLOC; private: bool isMustBeTrueNode(OrderNode *node); - void bypassMustBeTrueNode(OrderGraph *graph, OrderNode *node, HashsetOrderEdge *edgesRemoved); - void decomposeOrder(Order *currOrder, OrderGraph *currGraph, HashsetOrderEdge *edgesRemoved, DecomposeOrderResolver *dor); - void removeMustBeTrueNodes(OrderGraph *graph, HashsetOrderEdge *edgesRemoved); + void bypassMustBeTrueNode(OrderGraph *graph, OrderNode *node, DecomposeOrderResolver *dor); + void decomposeOrder(Order *currOrder, OrderGraph *currGraph, DecomposeOrderResolver *dor); + void removeMustBeTrueNodes(OrderGraph *graph, DecomposeOrderResolver *dor); + void mustEdgePrune(OrderGraph *graph, DecomposeOrderResolver *dor); + void attemptNodeMerge(OrderGraph *graph, OrderNode *node, DecomposeOrderResolver *dor); + void mergeNodes(OrderGraph *graph, OrderNode *node, OrderEdge *edge, OrderNode *dstnode, DecomposeOrderResolver *dor); }; diff --git a/src/Tuner/tunable.h b/src/Tuner/tunable.h index 012f420..9edcd3c 100644 --- a/src/Tuner/tunable.h +++ b/src/Tuner/tunable.h @@ -39,6 +39,6 @@ public: static TunableDesc onoff(0, 1, 1); static TunableDesc offon(0, 1, 0); -enum Tunables {DECOMPOSEORDER, MUSTREACHGLOBAL, MUSTREACHLOCAL, MUSTREACHPRUNE, OPTIMIZEORDERSTRUCTURE, ORDERINTEGERENCODING, PREPROCESS, NODEENCODING, EDGEENCODING}; +enum Tunables {DECOMPOSEORDER, MUSTREACHGLOBAL, MUSTREACHLOCAL, MUSTREACHPRUNE, OPTIMIZEORDERSTRUCTURE, ORDERINTEGERENCODING, PREPROCESS, NODEENCODING, EDGEENCODING, MUSTEDGEPRUNE}; typedef enum Tunables Tunables; #endif diff --git a/src/csolver.cc b/src/csolver.cc index 311ad0f..7fa33f2 100644 --- a/src/csolver.cc +++ b/src/csolver.cc @@ -387,9 +387,29 @@ BooleanEdge CSolver::applyLogicalOperation(LogicOp op, BooleanEdge *array, uint BooleanEdge CSolver::orderConstraint(Order *order, uint64_t first, uint64_t second) { ASSERT(first != second); + bool negate = false; + if (order->type == SATC_TOTAL) { + if (first > second) { + uint64_t tmp = first; + first = second; + second = tmp; + negate = true; + } + } Boolean *constraint = new BooleanOrder(order, first, second); - allBooleans.push(constraint); - return BooleanEdge(constraint); + Boolean *b = boolMap.get(constraint); + + if (b == NULL) { + allBooleans.push(constraint); + boolMap.put(constraint, constraint); + constraint->updateParents(); + } else { + delete constraint; + constraint = b; + } + + BooleanEdge be=BooleanEdge(constraint); + return negate ? be.negate() : be; } void CSolver::addConstraint(BooleanEdge constraint) { -- 2.34.1