From: Hamed Gorjiara <hgorjiar@uci.edu>
Date: Thu, 6 Sep 2018 20:27:37 +0000 (-0700)
Subject: Adding assertions, info logs, and validation functions for debugging purposes
X-Git-Url: http://plrg.eecs.uci.edu/git/?p=satune.git;a=commitdiff_plain;h=fb2b45c84b603f347ce3bbf37512408f6f404941

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

diff --git a/deploy-cs.sh b/deploy-cs.sh
index 3e3dcc7..98f98f1 100755
--- 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 2a741ae..8f50a03 100644
--- 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 ab9cac6..14f6e2b 100644
--- 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 e42f398..2fd6c30 100644
--- 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 fee6d9b..3269985 100644
--- 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 07a6168..fb35103 100644
--- 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);