From: bdemsky Date: Thu, 19 Oct 2017 20:13:42 +0000 (-0700) Subject: Bug fix for removing must edges...They also need to update constraints X-Git-Url: http://plrg.eecs.uci.edu/git/?p=satune.git;a=commitdiff_plain;h=23d460e60a4a44a1e7dab8fe9153cad37728a20d Bug fix for removing must edges...They also need to update constraints --- diff --git a/src/AST/astops.h b/src/AST/astops.h index d4e185d..c385ba5 100644 --- a/src/AST/astops.h +++ b/src/AST/astops.h @@ -17,6 +17,8 @@ typedef enum Polarity Polarity; enum BooleanValue {BV_UNDEFINED=0, BV_MUSTBETRUE=1, BV_MUSTBEFALSE=2, BV_UNSAT=3}; typedef enum BooleanValue BooleanValue; +extern const char *elemEncTypeNames[]; + enum ElementEncodingType { ELEM_UNASSIGNED, ONEHOT, UNARY, BINARYINDEX, BINARYVAL }; diff --git a/src/AST/element.cc b/src/AST/element.cc index 87c0ef8..62e0c4c 100644 --- a/src/AST/element.cc +++ b/src/AST/element.cc @@ -78,9 +78,11 @@ void ElementSet::serialize(Serializer *serializer) { } void ElementSet::print() { - model_print("{ElementSet:\n"); + model_print("{ElementSet:"); set->print(); - model_print("}\n"); + model_print(" %p ", this); + getElementEncoding()->print(); + model_print("}"); } void ElementConst::serialize(Serializer *serializer) { diff --git a/src/AST/predicate.cc b/src/AST/predicate.cc index ac3b617..80e8a5e 100644 --- a/src/AST/predicate.cc +++ b/src/AST/predicate.cc @@ -96,7 +96,9 @@ void PredicateOperator::serialize(Serializer *serializer) { } void PredicateOperator::print() { - model_print("{PredicateOperator: %s }\n", op == SATC_EQUALS ? "EQUAL" : "NOT-EQUAL"); + const char *names[] = {"==", "<", ">", "<=", ">="}; + + model_print("PredicateOperator: %s\n", names[(int)op]); } diff --git a/src/AST/set.cc b/src/AST/set.cc index ac4d088..7fa1212 100644 --- a/src/AST/set.cc +++ b/src/AST/set.cc @@ -146,7 +146,7 @@ void Set::serialize(Serializer *serializer) { void Set::print() { model_print("{Set:"); if (isRange) { - model_print("Range: low=%lu, high=%lu}\n\n", low, high); + model_print("Range: low=%lu, high=%lu}", low, high); } else { uint size = members->getSize(); model_print("Members: "); @@ -154,6 +154,6 @@ void Set::print() { uint64_t mem = members->get(i); model_print("%lu, ", mem); } - model_print("}\n"); + model_print("}"); } } diff --git a/src/ASTAnalyses/Order/orderanalysis.cc b/src/ASTAnalyses/Order/orderanalysis.cc index 701efde..3d829c9 100644 --- a/src/ASTAnalyses/Order/orderanalysis.cc +++ b/src/ASTAnalyses/Order/orderanalysis.cc @@ -48,7 +48,7 @@ void DFSNodeVisit(OrderNode *node, Vector *finishNodes, bool isReve if (!edge->mustPos) continue; } else - if (!edge->polPos && !edge->pseudoPos) //Ignore edges that do not have positive polarity + if (!edge->polPos && !edge->pseudoPos) //Ignore edges that do not have positive polarity continue; OrderNode *child = isReverse ? edge->source : edge->sink; @@ -56,8 +56,9 @@ void DFSNodeVisit(OrderNode *node, Vector *finishNodes, bool isReve child->status = VISITED; DFSNodeVisit(child, finishNodes, isReverse, mustvisit, sccNum); child->status = FINISHED; - if (finishNodes != NULL) + if (finishNodes != NULL) { finishNodes->push(child); + } if (isReverse) child->sccNum = sccNum; } @@ -81,69 +82,7 @@ void computeStronglyConnectedComponentGraph(OrderGraph *graph) { resetNodeInfoStatusSCC(graph); } -bool isMustBeTrueNode(OrderNode *node) { - SetIteratorOrderEdge *iterator = node->inEdges.iterator(); - while (iterator->hasNext()) { - OrderEdge *edge = iterator->next(); - if (!edge->mustPos) { - delete iterator; - return false; - } - } - delete iterator; - iterator = node->outEdges.iterator(); - while (iterator->hasNext()) { - OrderEdge *edge = iterator->next(); - if (!edge->mustPos) { - delete iterator; - return false; - } - } - delete iterator; - return true; -} - -void bypassMustBeTrueNode(CSolver *This, OrderGraph *graph, OrderNode *node) { - SetIteratorOrderEdge *iterin = node->inEdges.iterator(); - while (iterin->hasNext()) { - OrderEdge *inEdge = iterin->next(); - OrderNode *srcNode = inEdge->source; - srcNode->outEdges.remove(inEdge); - SetIteratorOrderEdge *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 ... - if (srcNode == sinkNode) { - This->setUnSAT(); - delete iterout; - delete iterin; - return; - } - 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) { - SetIteratorOrderNode *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 diff --git a/src/ASTAnalyses/Order/orderanalysis.h b/src/ASTAnalyses/Order/orderanalysis.h index b04ccfd..89665a1 100644 --- a/src/ASTAnalyses/Order/orderanalysis.h +++ b/src/ASTAnalyses/Order/orderanalysis.h @@ -11,9 +11,6 @@ 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 DFSMust(OrderGraph *graph, Vector *finishNodes); void DFSClearContradictions(CSolver *solver, OrderGraph *graph, Vector *finishNodes, bool computeTransitiveClosure); void reachMustAnalysis(CSolver *solver, OrderGraph *graph, bool computeTransitiveClosure); diff --git a/src/ASTAnalyses/Order/ordernode.h b/src/ASTAnalyses/Order/ordernode.h index 50543ac..0ae8867 100644 --- a/src/ASTAnalyses/Order/ordernode.h +++ b/src/ASTAnalyses/Order/ordernode.h @@ -22,6 +22,7 @@ public: OrderNode(uint64_t id); void addNewIncomingEdge(OrderEdge *edge); void addNewOutgoingEdge(OrderEdge *edge); + uint64_t getID() {return id;} uint64_t id; NodeStatus status; diff --git a/src/ASTTransform/decomposeordertransform.cc b/src/ASTTransform/decomposeordertransform.cc index 3b8571d..fd5fda8 100644 --- a/src/ASTTransform/decomposeordertransform.cc +++ b/src/ASTTransform/decomposeordertransform.cc @@ -62,20 +62,25 @@ void DecomposeOrderTransform::doTransform() { bool mustReachPrune = GETVARTUNABLE(solver->getTuner(), order->type, MUSTREACHPRUNE, &onoff); + HashsetOrderEdge *edgesRemoved = NULL; - if (mustReachPrune) - removeMustBeTrueNodes(solver, graph); + if (mustReachPrune) { + edgesRemoved = new HashsetOrderEdge(); + removeMustBeTrueNodes(graph, edgesRemoved); + } //This is needed for splitorder computeStronglyConnectedComponentGraph(graph); - decomposeOrder(order, graph); + decomposeOrder(order, graph, edgesRemoved); + if (edgesRemoved != NULL) + delete edgesRemoved; } delete orderit; delete orders; } -void DecomposeOrderTransform::decomposeOrder (Order *currOrder, OrderGraph *currGraph) { +void DecomposeOrderTransform::decomposeOrder (Order *currOrder, OrderGraph *currGraph, HashsetOrderEdge *edgesRemoved) { Vector ordervec; Vector partialcandidatevec; uint size = currOrder->constraints.getSize(); @@ -83,8 +88,19 @@ void DecomposeOrderTransform::decomposeOrder (Order *currOrder, OrderGraph *curr BooleanOrder *orderconstraint = currOrder->constraints.get(i); OrderNode *from = currGraph->getOrderNodeFromOrderGraph(orderconstraint->first); 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)) { + solver->replaceBooleanWithTrue(orderconstraint); + continue; + } else if (edgesRemoved->contains(invedge)) { + solver->replaceBooleanWithFalse(orderconstraint); + continue; + } + } + if (from->sccNum != to->sccNum) { - OrderEdge *edge = currGraph->lookupOrderEdgeFromOrderGraph(from, to); if (edge != NULL) { if (edge->polPos) { solver->replaceBooleanWithTrue(orderconstraint); @@ -96,7 +112,6 @@ void DecomposeOrderTransform::decomposeOrder (Order *currOrder, OrderGraph *curr ; } } else { - OrderEdge *invedge = currGraph->lookupOrderEdgeFromOrderGraph(to, from); if (invedge != NULL) { if (invedge->polPos) { solver->replaceBooleanWithFalse(orderconstraint); @@ -135,7 +150,6 @@ void DecomposeOrderTransform::decomposeOrder (Order *currOrder, OrderGraph *curr ((MutableSet *)neworder->set)->addElementMSet(to->id); } if (currOrder->type == SATC_PARTIAL) { - OrderEdge *edge = currGraph->getOrderEdgeFromOrderGraph(from, to); if (edge->polNeg) partialcandidatevec.setExpand(from->sccNum, NULL); } @@ -153,3 +167,74 @@ void DecomposeOrderTransform::decomposeOrder (Order *currOrder, OrderGraph *curr } } } + +bool DecomposeOrderTransform::isMustBeTrueNode(OrderNode *node) { + SetIteratorOrderEdge *iterator = node->inEdges.iterator(); + while (iterator->hasNext()) { + OrderEdge *edge = iterator->next(); + if (!edge->mustPos) { + delete iterator; + return false; + } + } + delete iterator; + iterator = node->outEdges.iterator(); + while (iterator->hasNext()) { + OrderEdge *edge = iterator->next(); + if (!edge->mustPos) { + delete iterator; + return false; + } + } + delete iterator; + return true; +} + +void DecomposeOrderTransform::bypassMustBeTrueNode(OrderGraph *graph, OrderNode *node, HashsetOrderEdge *edgesRemoved) { + SetIteratorOrderEdge *iterin = node->inEdges.iterator(); + while (iterin->hasNext()) { + OrderEdge *inEdge = iterin->next(); + OrderNode *srcNode = inEdge->source; + srcNode->outEdges.remove(inEdge); + edgesRemoved->add(inEdge); + SetIteratorOrderEdge *iterout = node->outEdges.iterator(); + while (iterout->hasNext()) { + OrderEdge *outEdge = iterout->next(); + OrderNode *sinkNode = outEdge->sink; + 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; + return; + } + //Add new order constraint + BooleanEdge orderconstraint = solver->orderConstraint(graph->getOrder(), srcNode->getID(), sinkNode->getID()); + solver->addConstraint(orderconstraint); + + //Add new edge + OrderEdge *newEdge = graph->getOrderEdgeFromOrderGraph(srcNode, sinkNode); + newEdge->mustPos = true; + newEdge->polPos = true; + if (newEdge->mustNeg) + solver->setUnSAT(); + srcNode->outEdges.add(newEdge); + sinkNode->inEdges.add(newEdge); + } + delete iterout; + } + delete iterin; +} + +void DecomposeOrderTransform::removeMustBeTrueNodes(OrderGraph *graph, HashsetOrderEdge *edgesRemoved) { + SetIteratorOrderNode *iterator = graph->getNodes(); + while (iterator->hasNext()) { + OrderNode *node = iterator->next(); + if (isMustBeTrueNode(node)) { + bypassMustBeTrueNode(graph, node, edgesRemoved); + } + } + delete iterator; +} diff --git a/src/ASTTransform/decomposeordertransform.h b/src/ASTTransform/decomposeordertransform.h index 1a2865c..8351ae0 100644 --- a/src/ASTTransform/decomposeordertransform.h +++ b/src/ASTTransform/decomposeordertransform.h @@ -16,11 +16,16 @@ public: DecomposeOrderTransform(CSolver *_solver); ~DecomposeOrderTransform(); void doTransform(); - void decomposeOrder (Order *currOrder, OrderGraph *currGraph); CMEMALLOC; private: + bool isMustBeTrueNode(OrderNode *node); + void bypassMustBeTrueNode(OrderGraph *graph, OrderNode *node, HashsetOrderEdge *edgesRemoved); + void decomposeOrder(Order *currOrder, OrderGraph *currGraph, HashsetOrderEdge *edgesRemoved); + void removeMustBeTrueNodes(OrderGraph *graph, HashsetOrderEdge *edgesRemoved); }; + + #endif/* ORDERTRANSFORM_H */ diff --git a/src/Encoders/elementencoding.cc b/src/Encoders/elementencoding.cc index 66a97d0..da6efd1 100644 --- a/src/Encoders/elementencoding.cc +++ b/src/Encoders/elementencoding.cc @@ -5,6 +5,8 @@ #include "satencoder.h" #include "set.h" +const char *elemEncTypeNames[] = {"UNASSIGNED", "ONEHOT", "UNARY", "BINARYINDEX", "BINARYVAL"}; + ElementEncoding::ElementEncoding(Element *_element) : type(ELEM_UNASSIGNED), element(_element), @@ -49,3 +51,17 @@ void ElementEncoding::encodingArrayInitialization() { setInUseElement(i); } } + +void ElementEncoding::print() { + model_print("%s ", elemEncTypeNames[type]); + if (type == BINARYINDEX) { + for (uint i = 0; i < encArraySize; i++) { + if (i != 0) + model_print(" ,"); + if (isinUseElement(i)) + model_print("%" PRIu64 "", encodingArray[i]); + else + model_print("_"); + } + } +} diff --git a/src/Encoders/elementencoding.h b/src/Encoders/elementencoding.h index 6797c66..b066de3 100644 --- a/src/Encoders/elementencoding.h +++ b/src/Encoders/elementencoding.h @@ -29,7 +29,7 @@ public: } return -1; } - + void print(); ElementEncodingType type; Element *element; diff --git a/src/Test/bug1.cc b/src/Test/bug1.cc index 208d9a9..7bbe9db 100644 --- a/src/Test/bug1.cc +++ b/src/Test/bug1.cc @@ -51,10 +51,9 @@ int main(int numargs, char **argv) { BooleanEdge v3 = solver->getBooleanVar(0); BooleanEdge v4 = solver->getBooleanVar(0); BooleanEdge v5 = solver->getBooleanVar(0); - solver->addConstraint( - solver->applyLogicalOperation(SATC_OR, - solver->applyLogicalOperation(SATC_IFF, v3, v4), - v5)); + BooleanEdge be = solver->applyLogicalOperation(SATC_IFF, v3, v4); + BooleanEdge sor = solver->applyLogicalOperation(SATC_OR, be, v5); + solver->addConstraint(sor); solver->addConstraint(solver->applyLogicalOperation(SATC_NOT, v5)); BooleanEdge v6 = solver->getBooleanVar(0); BooleanEdge v7 = solver->getBooleanVar(0); @@ -74,10 +73,9 @@ int main(int numargs, char **argv) { solver->applyLogicalOperation(SATC_OR, v10, v11), solver->applyLogicalOperation(SATC_IFF, v1, v12))); BooleanEdge b48 = solver->orderConstraint(order, 4, 8); - solver->addConstraint( - solver->applyLogicalOperation(SATC_OR, - solver->applyLogicalOperation(SATC_OR, v10, v11), - b48)); + BooleanEdge be1 = solver->applyLogicalOperation(SATC_OR, v10, v11); + BooleanEdge be2 = solver->applyLogicalOperation(SATC_OR, be1, b48); + solver->addConstraint(be2); BooleanEdge v13 = solver->getBooleanVar(0); BooleanEdge v14 = solver->getBooleanVar(0); solver->addConstraint( diff --git a/src/csolver.cc b/src/csolver.cc index fe3d9d9..311ad0f 100644 --- a/src/csolver.cc +++ b/src/csolver.cc @@ -393,9 +393,6 @@ BooleanEdge CSolver::orderConstraint(Order *order, uint64_t first, uint64_t seco } void CSolver::addConstraint(BooleanEdge constraint) { - if (constraint.isNegated()) - model_print("!"); - constraint.getBoolean()->print(); if (isTrue(constraint)) return; else if (isFalse(constraint)) { @@ -447,19 +444,19 @@ int CSolver::solve() { long long startTime = getTimeNano(); computePolarities(this); - //Preprocess pp(this); - //pp.doTransform(); + Preprocess pp(this); + pp.doTransform(); - //DecomposeOrderTransform dot(this); - // dot.doTransform(); + DecomposeOrderTransform dot(this); + dot.doTransform(); - //IntegerEncodingTransform iet(this); - // iet.doTransform(); - - //EncodingGraph eg(this); - //eg.buildGraph(); - //eg.encode(); + IntegerEncodingTransform iet(this); + iet.doTransform(); + EncodingGraph eg(this); + eg.buildGraph(); + eg.encode(); + printConstraints(); naiveEncodingDecision(this); satEncoder->encodeAllSATEncoder(this); model_print("Is problem UNSAT after encoding: %d\n", unsat); @@ -474,6 +471,19 @@ int CSolver::solve() { return result; } +void CSolver::printConstraints() { + SetIteratorBooleanEdge *it = getConstraints(); + while (it->hasNext()) { + BooleanEdge b = it->next(); + if (b.isNegated()) + model_print("!"); + b->print(); + model_print("\n"); + } + delete it; + +} + uint64_t CSolver::getElementValue(Element *element) { switch (element->type) { case ELEMSET: diff --git a/src/csolver.h b/src/csolver.h index 71ee874..15d5b45 100644 --- a/src/csolver.h +++ b/src/csolver.h @@ -132,9 +132,10 @@ public: bool isFalse(BooleanEdge b); void setUnSAT() { model_print("Setting UNSAT %%%%%%\n"); unsat = true; } - bool isUnSAT() { return unsat; } + void printConstraints(); + Vector *getOrders() { return &allOrders;} HashsetOrder *getActiveOrders() { return &activeOrders;}