Bug patches
authorbdemsky <bdemsky@uci.edu>
Thu, 21 Sep 2017 23:48:12 +0000 (16:48 -0700)
committerbdemsky <bdemsky@uci.edu>
Thu, 21 Sep 2017 23:48:12 +0000 (16:48 -0700)
src/ASTAnalyses/Encoding/encodinggraph.cc
src/ASTAnalyses/Encoding/encodinggraph.h
src/ASTAnalyses/Encoding/subgraph.cc
src/Test/ordertest.cc

index 6589976..ebe6d7a 100644 (file)
@@ -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);
index ccd2a5c..301a74a 100644 (file)
@@ -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;
index 50cc2d0..afddea1 100644 (file)
@@ -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;
index 9ffcab5..e2c46e0 100644 (file)
@@ -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");