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

diff --git a/deploy-cs.sh b/deploy-cs.sh
index 3e3dcc76fe84a43617ad19dd50da2261fae4e189..98f98f15af2031c32361d638455e4ebe4b9626ce 100755 (executable)
--- a/deploy-cs.sh
+++ b/deploy-cs.sh
@@ -8,6 +8,7 @@ SERVERS="dc-8.calit2.uci.edu dc-9.calit2.uci.edu dc-10.calit2.uci.edu dc-11.cali
 REMOTEDIR="/scratch/hamed/"
 INFILE="constraint_compiler/"
 SRC="constraint_compiler/src/"
+SHAREDDIR="~/"
 OUTFILE=csolver.tar.gz
 USER=hamed
 
@@ -17,6 +18,6 @@ rm -f $OUTFILE
 tar -czvf $OUTFILE $INFILE
 
 for SERVER in $SERVERS; do
-       scp $OUTFILE "$USER@$SERVER:$REMOTEDIR"
-       ssh $USER@$SERVER "cd $REMOTEDIR; sudo rm -r $SRC; tar -xzvf $OUTFILE; cd $SRC; make clean; ./setup.sh"
+       cp $OUTFILE $SHAREDDIR
+       ssh $USER@$SERVER "mv $SHAREDDIR$OUTFILE $REMOTEDIR; cd $REMOTEDIR; sudo rm -r $SRC; tar -xzvf $OUTFILE; cd $SRC; make clean; ./setup.sh"
 done

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);

diff --git a/src/ASTAnalyses/Encoding/encodinggraph.h b/src/ASTAnalyses/Encoding/encodinggraph.h
index ab9cac6cc3621e5d1f340cac4e95305c807f390a..14f6e2bc887e24130e407bf2b0bd8d6aef3845ef 100644 (file)
--- a/src/ASTAnalyses/Encoding/encodinggraph.h
+++ b/src/ASTAnalyses/Encoding/encodinggraph.h
@@ -10,6 +10,7 @@ public:
        ~EncodingGraph();
        void buildGraph();
        void encode();
+       void validate();
 
        CMEMALLOC;
 private:

diff --git a/src/Encoders/naiveencoder.cc b/src/Encoders/naiveencoder.cc
index e42f398a604c1a548ebe6af3476a2e2a6eaa0703..2fd6c30950291b38628ad15ef88d7431dee76522 100644 (file)
--- a/src/Encoders/naiveencoder.cc
+++ b/src/Encoders/naiveencoder.cc
@@ -65,6 +65,8 @@ void naiveEncodingPredicate(BooleanPredicate *This) {
 void naiveEncodingElement(Element *This) {
        ElementEncoding *encoding = This->getElementEncoding();
        if (encoding->getElementEncodingType() == ELEM_UNASSIGNED) {
+               if(This->type != ELEMCONST)
+                       model_print("INFO: naive encoder is making the decision about element %p....\n", This);
                encoding->setElementEncodingType(BINARYINDEX);
                encoding->encodingArrayInitialization();
        }

diff --git a/src/classlist.h b/src/classlist.h
index fee6d9bc7c14359893b61b1724d5e19fdc63ecc4..3269985504a2da78a90393ecb58a681bec7a19ca 100644 (file)
--- a/src/classlist.h
+++ b/src/classlist.h
@@ -68,6 +68,7 @@ class DecomposeOrderResolver;
 class EncodingGraph;
 class EncodingNode;
 class EncodingEdge;
+class EncodingSubGraph;
 
 struct IncrementalSolver;
 typedef struct IncrementalSolver IncrementalSolver;

diff --git a/src/csolver.cc b/src/csolver.cc
index 07a61688bcfb1e7ccad0bb23dfcb137854875fbf..fb351037c3ba12192db164b254db8d1f5e3f5d67 100644 (file)
--- a/src/csolver.cc
+++ b/src/csolver.cc
@@ -620,6 +620,8 @@ int CSolver::solve() {
        eg.encode();
 
        naiveEncodingDecision(this);
+//     eg.validate();
+       
        long long time5 = getTimeNano();
        model_print("Encoding Graph Time: %f\n", (time5 - time4) / NANOSEC);