Adding assertions, info logs, and validation functions for debugging purposes

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

diff --git a/src/ASTAnalyses/Encoding/encodinggraph.cc b/src/ASTAnalyses/Encoding/encodinggraph.cc
index 2a741ae77b006e912cef4ad99d5ce453d7a4c5b2..8f50a038b17fbaa53d97db82171618ad78fd2996 100644 (file)
--- a/src/ASTAnalyses/Encoding/encodinggraph.cc
+++ b/src/ASTAnalyses/Encoding/encodinggraph.cc
@@ -52,6 +52,66 @@ void EncodingGraph::buildGraph() {
        decideEdges();
 }
 
+
+void EncodingGraph::validate() {
+       SetIteratorBooleanEdge* it= solver->getConstraints();
+       while(it->hasNext()){
+               BooleanEdge be = it->next();
+               if(be->type == PREDICATEOP){
+                       BooleanPredicate *b = (BooleanPredicate *)be.getBoolean();
+                       if(b->predicate->type == OPERATORPRED){
+                               PredicateOperator* predicate = (PredicateOperator*) b->predicate;
+                               if(predicate->getOp() == SATC_EQUALS){
+                                       ASSERT(b->inputs.getSize() == 2);
+                                       Element* e1= b->inputs.get(0);
+                                       Element* e2= b->inputs.get(1);
+                                       if(e1->type == ELEMCONST || e1->type == ELEMCONST)
+                                               continue;
+                                       ElementEncoding *enc1 = e1->getElementEncoding();
+                                       ElementEncoding *enc2 = e2->getElementEncoding();
+                                       ASSERT(enc1->getElementEncodingType() != ELEM_UNASSIGNED);
+                                       ASSERT(enc2->getElementEncodingType() != ELEM_UNASSIGNED);
+                                       if(enc1->getElementEncodingType() == enc2->getElementEncodingType() && enc1->getElementEncodingType() == BINARYINDEX && b->getFunctionEncoding()->type == CIRCUIT){
+                                               for(uint i=0; i<enc1->encArraySize; i++){
+                                                       if(enc1->isinUseElement(i)){
+                                                               uint64_t val1 = enc1->encodingArray[i];
+                                                               if(enc2->isinUseElement(i)){
+                                                                       ASSERT(val1 == enc2->encodingArray[i]);
+                                                               }else{
+                                                                       for(uint j=0; j< enc2->encArraySize; j++){
+                                                                               if(enc2->isinUseElement(j)){
+                                                                                       ASSERT(val1 != enc2->encodingArray[j]);
+                                                                               }
+                                                                       }
+                                                               }
+                                                       }
+                                               }
+                                       }
+                                       //Now make sure that all the elements in the set are appeared in the encoding array!
+                                       for(uint k=0; k< b->inputs.getSize(); k++){
+                                               Element *e = b->inputs.get(k);
+                                               ElementEncoding *enc = e->getElementEncoding();
+                                               Set *s = e->getRange();
+                                               for (uint i = 0; i < s->getSize(); i++) {
+                                                       uint64_t value = s->getElement(i);
+                                                       bool exist=false;
+                                                       for(uint j=0; j< enc->encArraySize; j++){
+                                                               if(enc->isinUseElement(j) && enc->encodingArray[j] == value){
+                                                                       exist = true;
+                                                                       break;
+                                                               }
+                                                       }
+                                                       ASSERT(exist);
+                                               }
+                                       }
+                               }
+                       }
+               }
+       }
+       delete it;
+}
+
+
 void EncodingGraph::encode() {
        SetIteratorEncodingSubGraph *itesg = subgraphs.iterator();
        while (itesg->hasNext()) {
@@ -91,6 +151,7 @@ void EncodingGraph::encode() {
                                                uint64_t value = s->getElement(i);
                                                uint encodingIndex = subgraph->getEncoding(n, value);
                                                encoding->setInUseElement(encodingIndex);
+                                               ASSERT(encoding->isinUseElement(encodingIndex));
                                                encoding->encodingArray[encodingIndex] = value;
                                        }
                                }
@@ -139,7 +200,7 @@ void EncodingGraph::mergeNodes(EncodingNode *first, EncodingNode *second) {
                first->setEncoding(BINARYINDEX);
        if (graph2 == NULL)
                second->setEncoding(BINARYINDEX);
-
+       
        if (graph1 == NULL && graph2 == NULL) {
                graph1 = new EncodingSubGraph();
                subgraphs.add(graph1);