From 45bda60d0c548e27157100efb7855f45a5104606 Mon Sep 17 00:00:00 2001 From: bdemsky Date: Sat, 21 Oct 2017 17:21:22 -0700 Subject: [PATCH] New Resolver Design for Decompose Order --- src/ASTAnalyses/Order/orderanalysis.cc | 2 ++ src/ASTAnalyses/Order/ordergraph.cc | 18 ++++-------------- src/ASTAnalyses/Order/ordergraph.h | 2 -- src/ASTTransform/decomposeordertransform.cc | 12 +++++++----- src/Test/ordertest.cc | 1 - src/Translator/decomposeorderresolver.cc | 12 ++++++++++-- 6 files changed, 23 insertions(+), 24 deletions(-) diff --git a/src/ASTAnalyses/Order/orderanalysis.cc b/src/ASTAnalyses/Order/orderanalysis.cc index abec0c0..c8c7e36 100644 --- a/src/ASTAnalyses/Order/orderanalysis.cc +++ b/src/ASTAnalyses/Order/orderanalysis.cc @@ -39,6 +39,8 @@ void DFSClearContradictions(CSolver *solver, OrderGraph *graph, Vectoriterator(); while (srciterator->hasNext()) { OrderNode *srcnode = srciterator->next(); + if (srcnode->removed) + continue; OrderEdge *newedge = graph->getOrderEdgeFromOrderGraph(srcnode, node); newedge->mustPos = true; newedge->polPos = true; diff --git a/src/ASTAnalyses/Order/ordergraph.cc b/src/ASTAnalyses/Order/ordergraph.cc index d518b1b..85a0207 100644 --- a/src/ASTAnalyses/Order/ordergraph.cc +++ b/src/ASTAnalyses/Order/ordergraph.cc @@ -12,7 +12,6 @@ OrderGraph::OrderGraph(Order *_order) : OrderGraph *buildOrderGraph(Order *order) { ASSERT(order->graph == NULL); OrderGraph *orderGraph = new OrderGraph(order); - order->graph = orderGraph; uint constrSize = order->constraints.getSize(); for (uint j = 0; j < constrSize; j++) { orderGraph->addOrderConstraintToOrderGraph(order->constraints.get(j)); @@ -124,7 +123,6 @@ OrderNode *OrderGraph::getOrderNodeFromOrderGraph(uint64_t id) { node = tmp; } else { nodes.add(node); - allNodes.push(node); } return node; } @@ -172,16 +170,8 @@ void OrderGraph::addMustOrderConstraintToOrderGraph(BooleanOrder *bOrder) { } OrderGraph::~OrderGraph() { - uint size=allNodes.getSize(); - for(uint i=0;ihasNext()) { - OrderEdge *edge = eiterator->next(); - delete edge; - } - delete eiterator; + nodes.resetAndDelete(); + edges.resetAndDelete(); } bool OrderGraph::isTherePath(OrderNode *source, OrderNode *destination) { @@ -236,7 +226,7 @@ void OrderGraph::DFS(Vector *finishNodes) { SetIteratorOrderNode *iterator = getNodes(); while (iterator->hasNext()) { OrderNode *node = iterator->next(); - if (node->status == NOTVISITED) { + if (node->status == NOTVISITED && !node->removed) { node->status = VISITED; DFSNodeVisit(node, finishNodes, false, false, 0); node->status = FINISHED; @@ -250,7 +240,7 @@ void OrderGraph::DFSMust(Vector *finishNodes) { SetIteratorOrderNode *iterator = getNodes(); while (iterator->hasNext()) { OrderNode *node = iterator->next(); - if (node->status == NOTVISITED) { + if (node->status == NOTVISITED && !node->removed) { node->status = VISITED; DFSNodeVisit(node, finishNodes, false, true, 0); node->status = FINISHED; diff --git a/src/ASTAnalyses/Order/ordergraph.h b/src/ASTAnalyses/Order/ordergraph.h index fc82966..e7e958e 100644 --- a/src/ASTAnalyses/Order/ordergraph.h +++ b/src/ASTAnalyses/Order/ordergraph.h @@ -35,12 +35,10 @@ public: void computeStronglyConnectedComponentGraph(); void resetNodeInfoStatusSCC(); void completePartialOrderGraph(); - void removeNode(OrderNode *node) {nodes.remove(node);} CMEMALLOC; private: HashsetOrderNode nodes; - Vector allNodes; HashsetOrderEdge edges; Order *order; void DFSNodeVisit(OrderNode *node, Vector *finishNodes, bool isReverse, bool mustvisit, uint sccNum); diff --git a/src/ASTTransform/decomposeordertransform.cc b/src/ASTTransform/decomposeordertransform.cc index 01a667d..4c95db8 100644 --- a/src/ASTTransform/decomposeordertransform.cc +++ b/src/ASTTransform/decomposeordertransform.cc @@ -81,7 +81,7 @@ void DecomposeOrderTransform::doTransform() { } -void DecomposeOrderTransform::decomposeOrder (Order *currOrder, OrderGraph *currGraph, HashsetOrderEdge *edgesRemoved, DecomposeOrderResolver *dor) { +void DecomposeOrderTransform::decomposeOrder(Order *currOrder, OrderGraph *currGraph, HashsetOrderEdge *edgesRemoved, DecomposeOrderResolver *dor) { Vector partialcandidatevec; uint size = currOrder->constraints.getSize(); for (uint i = 0; i < size; i++) { @@ -203,18 +203,21 @@ void DecomposeOrderTransform::bypassMustBeTrueNode(OrderGraph *graph, OrderNode OrderNode *srcNode = inEdge->source; srcNode->outEdges.remove(inEdge); edgesRemoved->add(inEdge); + bool removeOutgoingEdges = !iterin->hasNext(); + SetIteratorOrderEdge *iterout = node->outEdges.iterator(); while (iterout->hasNext()) { OrderEdge *outEdge = iterout->next(); OrderNode *sinkNode = outEdge->sink; - sinkNode->inEdges.remove(outEdge); - edgesRemoved->add(outEdge); + if (removeOutgoingEdges) { + sinkNode->inEdges.remove(outEdge); + edgesRemoved->add(outEdge); + } //Adding new edge to new sink and src nodes ... if (srcNode == sinkNode) { solver->setUnSAT(); delete iterout; delete iterin; - graph->removeNode(node); return; } //Add new order constraint @@ -233,7 +236,6 @@ void DecomposeOrderTransform::bypassMustBeTrueNode(OrderGraph *graph, OrderNode delete iterout; } delete iterin; - graph->removeNode(node); } void DecomposeOrderTransform::removeMustBeTrueNodes(OrderGraph *graph, HashsetOrderEdge *edgesRemoved) { diff --git a/src/Test/ordertest.cc b/src/Test/ordertest.cc index 148235a..74d5eba 100644 --- a/src/Test/ordertest.cc +++ b/src/Test/ordertest.cc @@ -16,7 +16,6 @@ int main(int numargs, char **argv) { solver->addConstraint(solver->applyLogicalOperation(SATC_OR, b1, solver->applyLogicalOperation(SATC_NOT, b2))); solver->addConstraint(solver->applyLogicalOperation(SATC_OR, b2, solver->applyLogicalOperation(SATC_NOT, b1))); - solver->serialize(); if (solver->solve() == 1) { printf("SAT\n"); printf("O(5,1)=%d O(1,4)=%d O(5,4)=%d O(1,5)=%d\n", diff --git a/src/Translator/decomposeorderresolver.cc b/src/Translator/decomposeorderresolver.cc index 0e652d8..c2e9db4 100644 --- a/src/Translator/decomposeorderresolver.cc +++ b/src/Translator/decomposeorderresolver.cc @@ -79,6 +79,8 @@ void DecomposeOrderResolver::buildGraph() { bool isEdge = suborder->encoding.resolver->resolveOrder(doredge->newfirst, doredge->newsecond); if (isEdge) graph->addEdge(doredge->origfirst, doredge->origsecond); + else if (order->type == SATC_TOTAL) + graph->addEdge(doredge->origsecond, doredge->origfirst); } } delete iterator; @@ -92,9 +94,15 @@ bool DecomposeOrderResolver::resolveOrder(uint64_t first, uint64_t second) { buildGraph(); OrderNode *from = graph->lookupOrderNodeFromOrderGraph(first); - ASSERT(from != NULL); + if (from == NULL) { + ASSERT(order->type != SATC_TOTAL); + return false; + } OrderNode *to = graph->lookupOrderNodeFromOrderGraph(second); - ASSERT(to != NULL); + if (to == NULL) { + ASSERT(order->type != SATC_TOTAL); + return false; + } switch (order->type) { case SATC_TOTAL: return from->sccNum < to->sccNum; -- 2.34.1