Adding checks to avoid further processing on UNSAT Problems

[satune.git] / src / ASTAnalyses / Encoding / encodinggraph.cc

diff --git a/src/ASTAnalyses/Encoding/encodinggraph.cc b/src/ASTAnalyses/Encoding/encodinggraph.cc
index 2ac69c1de22ddbedb684e04eb44cc51cc76e61f4..84166a88ddf6dd51773c04765f0e0107053e0a9b 100644 (file)
--- a/src/ASTAnalyses/Encoding/encodinggraph.cc
+++ b/src/ASTAnalyses/Encoding/encodinggraph.cc
@@ -113,8 +113,11 @@ void EncodingGraph::validate() {
 
 
 void EncodingGraph::encode() {
+       if (solver->isUnSAT() || solver->getTuner()->getTunable(ENCODINGGRAPHOPT, &offon) == 0)
+               return;
+       buildGraph();
        SetIteratorEncodingSubGraph *itesg = subgraphs.iterator();
-       model_print("#SubGraph = %u", subgraphs.getSize());
+       model_print("#SubGraph = %u\n", subgraphs.getSize());
        while (itesg->hasNext()) {
                EncodingSubGraph *sg = itesg->next();
                sg->encode();
@@ -155,9 +158,6 @@ void EncodingGraph::encode() {
                                                ASSERT(encoding->isinUseElement(encodingIndex));
                                                encoding->encodingArray[encodingIndex] = value;
                                        }
-                               } else {
-                                       model_print("DAMN in encode()\n");
-                                       e->print();
                                }
                        }
                        break;
@@ -305,7 +305,6 @@ void EncodingGraph::processPredicate(BooleanPredicate *b) {
 }
 
 uint convertSize(uint cost) {
-       cost = FUDGEFACTOR * cost;// fudge factor
        return NEXTPOW2(cost);
 }
 
@@ -333,58 +332,38 @@ void EncodingGraph::decideEdges() {
                        EncodingNode *tmp = left; left = right; right = tmp;
                        EncodingSubGraph *tmpsg = leftGraph; leftGraph = rightGraph; rightGraph = tmpsg;
                }
-               //model_print("Right=%p RGraph=%p\tLeft=%p LGraph=%p\n", right, rightGraph, left, leftGraph);
-               uint leftSize = 0, rightSize = 0, newSize = 0, max = 0;
-               uint64_t totalCost = 0;
-               bool merge = false;
-//             model_print("**************decideEdge*************\n");
-//             model_print("LeftNode Size = %u\n", left->getSize());
-//             model_print("rightNode Size = %u\n", right->getSize());
-//             model_print("UnionSize = %u\n", left->s->getUnionSize(right->s));
 
+               uint leftSize = 0, rightSize = 0, newSize = 0, min = 0;
+               bool merge = false;
                if (leftGraph == NULL && rightGraph == NULL) {
                        leftSize = convertSize(left->getSize());
                        rightSize = convertSize(right->getSize());
                        newSize = convertSize(left->s->getUnionSize(right->s));
                        newSize = (leftSize > newSize) ? leftSize : newSize;
                        newSize = (rightSize > newSize) ? rightSize : newSize;
-                       totalCost = (newSize - leftSize) * left->elements.getSize() +
-                                                                       (newSize - rightSize) * right->elements.getSize();
-                       //model_print("leftSize=%u\trighSize=%u\tnewSize=%u\n", leftSize, rightSize, newSize);
-                       max = rightSize > leftSize ? rightSize : leftSize;
-                       if (newSize == max) {
-                               merge = true;
-                       }
+                       min = rightSize > leftSize ? leftSize : rightSize;
+                       merge = left->measureSimilarity(right) > 1.5 || min == newSize;
                } else if (leftGraph != NULL && rightGraph == NULL) {
-                       leftSize = convertSize(leftGraph->encodingSize);
+                       leftSize = convertSize(leftGraph->numValues());
                        rightSize = convertSize(right->getSize());
                        newSize = convertSize(leftGraph->estimateNewSize(right));
                        newSize = (leftSize > newSize) ? leftSize : newSize;
                        newSize = (rightSize > newSize) ? rightSize : newSize;
-                       totalCost = (newSize - leftSize) * leftGraph->numElements +
-                                                                       (newSize - rightSize) * right->elements.getSize();
-                       //model_print("leftSize=%u\trighSize=%u\tnewSize=%u\n", leftSize, rightSize, newSize);
-                       max = rightSize > leftSize ? rightSize : leftSize;
-                       if (newSize == max) {
-                               merge = true;
-                       }
+                       min = rightSize > leftSize ? leftSize : rightSize;
+                       merge = leftGraph->measureSimilarity(right) > 1.5 || min == newSize;
+//                     model_print("Merge=%s\tsimilarity=%f\n", merge?"TRUE":"FALSE", leftGraph->measureSimilarity(right));
                } else {
                        //Neither are null
-                       leftSize = convertSize(leftGraph->encodingSize);
-                       rightSize = convertSize(rightGraph->encodingSize);
+                       leftSize = convertSize(leftGraph->numValues());
+                       rightSize = convertSize(rightGraph->numValues());
                        newSize = convertSize(leftGraph->estimateNewSize(rightGraph));
+//                     model_print("MergingSubGraphs: left=%u\tright=%u\tnewSize=%u\n", leftSize, rightSize, newSize);
                        newSize = (leftSize > newSize) ? leftSize : newSize;
                        newSize = (rightSize > newSize) ? rightSize : newSize;
-                       totalCost = (newSize - leftSize) * leftGraph->numElements +
-                                                                       (newSize - rightSize) * rightGraph->numElements;
-//                     model_print("LeftGraph size=%u\n", leftGraph->encodingSize);
-//                     model_print("RightGraph size=%u\n", rightGraph->encodingSize);
-//                     model_print("UnionGraph size = %u\n", leftGraph->estimateNewSize(rightGraph));
-                       if (rightSize < 64 && leftSize < 64) {
-                               merge = true;
-                       }
+                       min = rightSize > leftSize ? leftSize : rightSize;
+                       merge = leftGraph->measureSimilarity(rightGraph) > 1.5 || min == newSize;
+//                     model_print("Merge=%s\tsimilarity=%f\n", merge?"TRUE":"FALSE", leftGraph->measureSimilarity(rightGraph));
                }
-//             model_print("******************************\n");
                if (merge) {
                        //add the edge
                        mergeNodes(left, right);
@@ -441,11 +420,32 @@ uint EncodingNode::getSize() const {
        return s->getSize();
 }
 
+uint64_t EncodingNode::getIndex(uint index) {
+       return s->getElement(index);
+}
+
 VarType EncodingNode::getType() const {
        return s->getType();
 }
 
-static TunableDesc NodeEncodingDesc(ELEM_UNASSIGNED, BINARYINDEX, ELEM_UNASSIGNED);
+double EncodingNode::measureSimilarity(EncodingNode *node) {
+       uint common = 0;
+       for (uint i = 0, j = 0; i < s->getSize() && j < node->s->getSize(); ) {
+               uint64_t item = s->getElement(i);
+               uint64_t item2 = node->s->getElement(j);
+               if (item < item2)
+                       i++;
+               else if (item2 > item)
+                       j++;
+               else {
+                       i++;
+                       j++;
+                       common++;
+               }
+       }
+
+       return common * 1.0 / s->getSize() + common * 1.0 / node->getSize();
+}
 
 EncodingNode *EncodingGraph::createNode(Element *e) {
        if (e->type == ELEMCONST)