Bug patches

diff --git a/src/ASTAnalyses/Encoding/encodinggraph.cc b/src/ASTAnalyses/Encoding/encodinggraph.cc
index 658997604338d0a4e5d35074b7a7768601a8a479..ebe6d7a90049f9773f3c9debad2be8b9238bb7c9 100644 (file)
--- a/src/ASTAnalyses/Encoding/encodinggraph.cc
+++ b/src/ASTAnalyses/Encoding/encodinggraph.cc
@@ -124,6 +124,11 @@ void EncodingGraph::encodeParent(Element *e) {
 void EncodingGraph::mergeNodes(EncodingNode *first, EncodingNode *second) {
        EncodingSubGraph *graph1=graphMap.get(first);
        EncodingSubGraph *graph2=graphMap.get(second);
+       if (graph1 == NULL)
+               first->setEncoding(BINARYINDEX);
+       if (graph2 == NULL)
+               second->setEncoding(BINARYINDEX);
+
        if (graph1 == NULL && graph2 == NULL) {
                graph1 = new EncodingSubGraph();
                subgraphs.add(graph1);
@@ -226,8 +231,8 @@ void EncodingGraph::decideEdges() {
                EncodingNode *right = ee->right;
                
                if (ee->encoding != EDGE_UNASSIGNED ||
-                               left->encoding != BINARYINDEX ||
-                               right->encoding != BINARYINDEX)
+                               !left->couldBeBinaryIndex() ||
+                               !right->couldBeBinaryIndex())
                        continue;
                
                uint64_t eeValue = ee->getValue();
@@ -298,8 +303,8 @@ EncodingEdge * EncodingGraph::createEdge(EncodingNode *left, EncodingNode *right
                        v1=tmp;
                }
 
-               if ((left != NULL && left->encoding==BINARYINDEX) &&
-                               (right != NULL) && right->encoding==BINARYINDEX) {
+               if ((left != NULL && left->couldBeBinaryIndex()) &&
+                               (right != NULL) && right->couldBeBinaryIndex()) {
                        EdgeEncodingType type=(EdgeEncodingType)solver->getTuner()->getVarTunable(v1, v2, EDGEENCODING, &EdgeEncodingDesc);
                        result->setEncoding(type);
                        if (type == EDGE_MATCH) {
@@ -340,6 +345,7 @@ EncodingNode * EncodingGraph::createNode(Element *e) {
        if (n == NULL) {
                n = new EncodingNode(s);
                n->setEncoding((ElementEncodingType)solver->getTuner()->getVarTunable(n->getType(), NODEENCODING, &NodeEncodingDesc));
+               
                encodingMap.put(s, n);
        }
        n->addElement(e);

diff --git a/src/ASTAnalyses/Encoding/encodinggraph.h b/src/ASTAnalyses/Encoding/encodinggraph.h
index ccd2a5c79fa980dc870085fdbf8daf4947285915..301a74ab0bf8db0f4e2e9f54eded6c7f67c8b279 100644 (file)
--- a/src/ASTAnalyses/Encoding/encodinggraph.h
+++ b/src/ASTAnalyses/Encoding/encodinggraph.h
@@ -40,6 +40,7 @@ class EncodingNode {
        VarType getType() const;
        void setEncoding(ElementEncodingType e) {encoding=e;}
        ElementEncodingType getEncoding() {return encoding;}
+       bool couldBeBinaryIndex() {return encoding == BINARYINDEX || encoding == ELEM_UNASSIGNED;}
        CMEMALLOC;
  private:
        Set *s;

diff --git a/src/ASTAnalyses/Encoding/subgraph.cc b/src/ASTAnalyses/Encoding/subgraph.cc
index 50cc2d0da9678933f6400aea2f97b618ab593c66..afddea10ebe0d9dda337f89188a045e48149d302 100644 (file)
--- a/src/ASTAnalyses/Encoding/subgraph.cc
+++ b/src/ASTAnalyses/Encoding/subgraph.cc
@@ -215,8 +215,6 @@ void EncodingSubGraph::computeComparisons() {
                delete edgeit;
        }
        delete nodeit;
-       
-       
 }
 
 void EncodingSubGraph::orderEV(EncodingValue *earlier, EncodingValue *later) {
@@ -276,7 +274,8 @@ void EncodingSubGraph::generateComparison(EncodingNode *left, EncodingNode *righ
                                orderEV(last, rev);
                }
                if (lev != rev) {
-                       if (rev == NULL || lVal < rVal) {
+                       if (rev == NULL ||
+                                       (lev != NULL && lVal < rVal)) {
                                if (rev != NULL)
                                        orderEV(lev, rev);
                                last = lev;

diff --git a/src/Test/ordertest.cc b/src/Test/ordertest.cc
index 9ffcab56c91acf7efab1f200e02b9a021451c881..e2c46e0593c1df06d2144243eb52fbdc105ae622 100644 (file)
--- a/src/Test/ordertest.cc
+++ b/src/Test/ordertest.cc
@@ -13,8 +13,9 @@ int main(int numargs, char **argv) {
        Order *order = solver->createOrder(SATC_TOTAL, s);
        BooleanEdge b1 =  solver->orderConstraint(order, 5, 1);
        BooleanEdge b2 =  solver->orderConstraint(order, 1, 4);
-       solver->addConstraint(b1);
-       solver->addConstraint(b2);
+
+       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");