From: Hamed <hamed.gorjiara@gmail.com>
Date: Sat, 5 Aug 2017 20:16:10 +0000 (-0700)
Subject: Fixing some bugs ...
X-Git-Url: http://plrg.eecs.uci.edu/git/?p=satune.git;a=commitdiff_plain;h=c12192d653bb50ff7890aa395af19f34b85cde2b

Fixing some bugs ...
---

diff --git a/src/Backend/satfunctableencoder.c b/src/Backend/satfunctableencoder.c
index f92f1e6..0609c7c 100644
--- a/src/Backend/satfunctableencoder.c
+++ b/src/Backend/satfunctableencoder.c
@@ -268,30 +268,33 @@ void encodeEnumTableElemFunctionSATEncoder(SATEncoder* This, ElementFunction* el
 		switch(function->undefBehavior) {
 			case UNDEFINEDSETSFLAG: {
 				if (isInRange) {
+					//FIXME: Talk to Brian, It should be IFF not only IMPLY. --HG
 					clause=constraintIMPLIES(This->cnf,constraintAND(This->cnf, numDomains, carray), carray[numDomains]);
 				} else {
-					clause=constraintIMPLIES(This->cnf,constraintAND(This->cnf, numDomains, carray), undefConstraint);
+					addConstraintCNF(This->cnf, constraintIMPLIES(This->cnf,constraintAND(This->cnf, numDomains, carray), undefConstraint));
 				}
 				break;
 			}
 			case FLAGIFFUNDEFINED: {
 				if (isInRange) {
-					clause=constraintIMPLIES(This->cnf,constraintAND(This->cnf, numDomains, carray), constraintAND2(This->cnf, carray[numDomains], constraintNegate(undefConstraint)));
+					clause=constraintIMPLIES(This->cnf,constraintAND(This->cnf, numDomains, carray), carray[numDomains]);
+					addConstraintCNF(This->cnf, constraintIMPLIES(This->cnf, constraintAND(This->cnf, numDomains, carray), constraintNegate(undefConstraint) ));
 				} else {
-					clause=constraintIMPLIES(This->cnf,constraintAND(This->cnf, numDomains, carray), undefConstraint);
+					addConstraintCNF(This->cnf,constraintIMPLIES(This->cnf, constraintAND(This->cnf, numDomains, carray), undefConstraint));
 				}
 				break;
 			}
 			default:
 				ASSERT(0);
 		}
+		if(isInRange){
 #ifdef TRACE_DEBUG
-		model_print("added clause in function table enumeration ...\n");
-		printCNF(clause);
-		model_print("\n");
+			model_print("added clause in function table enumeration ...\n");
+			printCNF(clause);
+			model_print("\n");
 #endif
-		pushVectorEdge(clauses, clause);
-
+			pushVectorEdge(clauses, clause);
+		}
 		
 		notfinished=false;
 		for(uint i=0;i<numDomains; i++) {
diff --git a/src/Backend/satorderencoder.c b/src/Backend/satorderencoder.c
index 36c16f2..e8a7f3d 100644
--- a/src/Backend/satorderencoder.c
+++ b/src/Backend/satorderencoder.c
@@ -58,7 +58,6 @@ void createAllTotalOrderConstraintsSATEncoder(SATEncoder* This, Order* order){
 	VectorInt* mems = order->set->members;
 	HashTableOrderPair* table = order->orderPairTable;
 	uint size = getSizeVectorInt(mems);
-	uint csize =0;
 	for(uint i=0; i<size; i++){
 		uint64_t valueI = getVectorInt(mems, i);
 		for(uint j=i+1; j<size;j++){
diff --git a/src/Backend/sattranslator.c b/src/Backend/sattranslator.c
index a9c89fe..7736f94 100644
--- a/src/Backend/sattranslator.c
+++ b/src/Backend/sattranslator.c
@@ -8,18 +8,19 @@
 
 uint64_t getElementValueBinaryIndexSATTranslator(CSolver* This, ElementEncoding* elemEnc){
 	uint index=0;
-	for(uint i=elemEnc->numVars-1;i>=0;i--) {
+	for(int i=elemEnc->numVars-1;i>=0;i--) {
 		index=index<<1;
 		if (getValueSolver(This->satEncoder->cnf->solver, getEdgeVar( elemEnc->variables[i] )))
 			index |= 1;
 	}
+	model_print("index:%u\tencArraySize:%u\tisInUseElement:%u\n", index, elemEnc->encArraySize, isinUseElement(elemEnc, index));
 	ASSERT(elemEnc->encArraySize >index && isinUseElement(elemEnc, index));
 	return elemEnc->encodingArray[index];
 }
 
 uint64_t getElementValueBinaryValueSATTranslator(CSolver* This, ElementEncoding* elemEnc){
 	uint64_t value=0;
-	for(uint i=elemEnc->numVars-1;i>=0;i--) {
+	for(int i=elemEnc->numVars-1;i>=0;i--) {
 		value=value<<1;
 		if (getValueSolver(This->satEncoder->cnf->solver, getEdgeVar( elemEnc->variables[i] )) )
 			value |= 1;
diff --git a/src/Test/tablefuncencodetest.c b/src/Test/tablefuncencodetest.c
index 13337ea..12a589e 100644
--- a/src/Test/tablefuncencodetest.c
+++ b/src/Test/tablefuncencodetest.c
@@ -5,10 +5,10 @@
  * e3= f(e1, e2) 
  *	1 5 => 7
  *	2 3 => 5
- *	1 7 => 1
- *	2 7 => 2
+ *	1 7 => 3
+ *	2 7 => 5
  *	2 5 => 3
- *	1 3 => 4
+ *	1 3 => 5
  * e4 = {6, 10, 19}
  * e4 <= e3
  * Result: e1=1, e2=5, e3=7, e4=6, overflow=0
@@ -36,10 +36,10 @@ int main(int numargs, char ** argv) {
 	uint64_t row6[] = {1, 3};
 	addTableEntry(solver, t1, row1, 2, 7);
 	addTableEntry(solver, t1, row2, 2, 5);
-	addTableEntry(solver, t1, row3, 2, 1);
-	addTableEntry(solver, t1, row4, 2, 2);
+	addTableEntry(solver, t1, row3, 2, 3);
+	addTableEntry(solver, t1, row4, 2, 5);
 	addTableEntry(solver, t1, row5, 2, 3);
-	addTableEntry(solver, t1, row6, 2, 4);
+	addTableEntry(solver, t1, row6, 2, 5);
 	Function * f1 = completeTable(solver, t1, FLAGIFFUNDEFINED);	
 	Element * e3 = applyFunction(solver, f1, (Element* []){e1,e2}, 2, overflow);