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 d4e185d1498483d944fd4852c14f827fae8c5cdd..c385ba5c4fd93d388f3d848b31ca441755cd9ac2 100644 (file)
--- 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 87c0ef8c49d1e324a9787387fc7da27744962bb3..62e0c4c111af9f5112ca4674c8de79e77c3c8a64 100644 (file)
--- 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 ac3b617156e023a287871bc0393c4de41befe4da..80e8a5e38e5be4aee0fad516ef9d4fb67fc0d03e 100644 (file)
--- 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 ac4d088b338554ca2326e61ca5c994f81471b2de..7fa1212197030e1761c7bfefd2bb00f59a7ad50e 100644 (file)
--- 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 701efde3f8393c7b2a6ec50b3709cf1f56549c41..3d829c94b5e57ed59676071fb63d57634f3c82f0 100644 (file)
--- a/src/ASTAnalyses/Order/orderanalysis.cc
+++ b/src/ASTAnalyses/Order/orderanalysis.cc
@@ -48,7 +48,7 @@ void DFSNodeVisit(OrderNode *node, Vector<OrderNode *> *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<OrderNode *> *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 b04ccfddc465ef6abef06c7a0e3c8e79e0a46092..89665a1fed0353bc4c01cfa8a77f287aa9978faf 100644 (file)
--- a/src/ASTAnalyses/Order/orderanalysis.h
+++ b/src/ASTAnalyses/Order/orderanalysis.h
@@ -11,9 +11,6 @@ void DFS(OrderGraph *graph, Vector<OrderNode *> *finishNodes);
 void DFSReverse(OrderGraph *graph, Vector<OrderNode *> *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<OrderNode *> *finishNodes);
 void DFSClearContradictions(CSolver *solver, OrderGraph *graph, Vector<OrderNode *> *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 50543ac8a7fb19f1d02af05f0f9fb9bc3a07e98b..0ae88679b956252f13b14da8c4338681bfd61fee 100644 (file)
--- 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 3b8571d4fd3f37e5aea1b30908d9f5d3d1103b74..fd5fda8fed7fcb6fd46b18a7648b1fa564f9637f 100644 (file)
--- 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<Order *> ordervec;
        Vector<Order *> 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 1a2865cef6f64033752be24696005db51d4091d5..8351ae0f632af276b3338913370665e06993225d 100644 (file)
--- 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 66a97d08602672d2eed1390f4788b7b50249bfa0..da6efd19154b0f1f3075114151e426923bc46fe9 100644 (file)
--- 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 6797c66bf530b9024fba0fd3627f43643799ce04..b066de34a341636eb7039d89b3bc5733c3bc030e 100644 (file)
--- 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 208d9a9f3d396918fe5cbe97bfd3604bb5f19c3a..7bbe9db740916c99d80d8607a8a27f5d4a1af1e6 100644 (file)
--- 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 fe3d9d91a0c69fd0e9854715eb3fcfbc20232e27..311ad0f5052ac00ac29ff03cbdbc1082912fcd94 100644 (file)
--- 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 71ee87487471fa99f9ee1091ff56ff0de00e00bd..15d5b453c8b697505ac40e22b4efe7b65cd03996 100644 (file)
--- 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<Order *> *getOrders() { return &allOrders;}
        HashsetOrder *getActiveOrders() { return &activeOrders;}