From: Hamed <hamed.gorjiara@gmail.com>
Date: Fri, 21 Jul 2017 09:29:38 +0000 (-0700)
Subject: A bug fix for the case IGNOREBEHAVIOR in table-base predicate
X-Git-Url: http://plrg.eecs.uci.edu/git/?a=commitdiff_plain;h=d2add7d9c5621f6ded2c94d8178e0d0f673cde71;p=satune.git

A bug fix for the case IGNOREBEHAVIOR in table-base predicate
---

diff --git a/src/Backend/satfunctableencoder.c b/src/Backend/satfunctableencoder.c
index 5ae30bf..da10a20 100644
--- a/src/Backend/satfunctableencoder.c
+++ b/src/Backend/satfunctableencoder.c
@@ -21,6 +21,10 @@ Edge encodeEnumEntriesTablePredicateSATEncoder(SATEncoder * This, BooleanPredica
 	uint size = getSizeHashSetTableEntry(table->entries);
 	bool generateNegation = encType == ENUMERATEIMPLICATIONSNEGATE;
 	Edge constraints[size];
+	VectorEdge * undefClauses=allocDefVectorEdge();
+	Edge undefConst = encodeConstraintSATEncoder(This, constraint->undefStatus);
+	printCNF(undefConst);
+	model_print("**\n");
 	HSIteratorTableEntry* iterator = iteratorTableEntry(table->entries);
 	uint i=0;
 	while(hasNextTableEntry(iterator)){
@@ -33,6 +37,8 @@ Edge encodeEnumEntriesTablePredicateSATEncoder(SATEncoder * This, BooleanPredica
 		for(uint j=0; j<inputNum; j++){
 			Element* el = getArrayElement(inputs, j);
 			carray[j] = getElementValueConstraint(This, el, entry->inputs[j]);
+			printCNF(carray[j]);
+			model_print("\n");
 		}
 		Edge row;
 		switch(undefStatus){
@@ -40,19 +46,26 @@ Edge encodeEnumEntriesTablePredicateSATEncoder(SATEncoder * This, BooleanPredica
 				row=constraintAND(This->cnf, inputNum, carray);
 				break;
 			case FLAGFORCEUNDEFINED:{
-				Edge undefConst = encodeConstraintSATEncoder(This, constraint->undefStatus);
-				row=constraintIMPLIES(This->cnf,constraintAND(This->cnf, inputNum, carray),  constraintNegate(undefConst));
+				row=constraintAND(This->cnf, inputNum, carray);
+				pushVectorEdge(undefClauses, constraintIMPLIES(This->cnf,constraintAND(This->cnf, inputNum, carray),  constraintNegate(undefConst)));
 				break;
 			}
 			default:
 				ASSERT(0);
 		}
 		constraints[i++] = row;
+		printCNF(row);
 		
+		model_print("\n\n");
 	}
-	Edge result=constraintOR(This->cnf, size, constraints);
-
-	return generateNegation ? constraintNegate(result) : result;
+	Edge result= generateNegation?constraintNegate(constraintOR(This->cnf, i, constraints))
+		:constraintOR(This->cnf, i, constraints);
+	Edge tmp = E_NULL;
+	if(getSizeVectorEdge(undefClauses) != 0)
+		tmp= constraintAND(This->cnf, getSizeVectorEdge(undefClauses), exposeArrayEdge(undefClauses));
+	deleteVectorEdge(undefClauses);
+	printCNF(result);
+	return edgeIsNull(tmp)? result: constraintAND2(This->cnf, tmp, result);
 }
 Edge encodeEnumTablePredicateSATEncoder(SATEncoder * This, BooleanPredicate * constraint){
 #ifdef TRACE_DEBUG
@@ -77,7 +90,8 @@ Edge encodeEnumTablePredicateSATEncoder(SATEncoder * This, BooleanPredicate * co
 	bool generateNegation = constraint->encoding.type == ENUMERATEIMPLICATIONSNEGATE;
 	uint numDomains=getSizeArraySet(&predicate->table->domains);
 
-	VectorEdge * clauses=allocDefVectorEdge(); // Setup array of clauses
+	VectorEdge * clauses=allocDefVectorEdge();
+	VectorEdge * undefClauses=allocDefVectorEdge();
 	
 	uint indices[numDomains]; //setup indices
 	bzero(indices, sizeof(uint)*numDomains);
@@ -127,7 +141,10 @@ Edge encodeEnumTablePredicateSATEncoder(SATEncoder * This, BooleanPredicate * co
 		printCNF(clause);
 		model_print("\n");
 #endif
-		pushVectorEdge(clauses, clause);
+		if(isInRange)
+			pushVectorEdge(clauses, clause);
+		else
+			pushVectorEdge(undefClauses, clause);
 NEXT:	
 		notfinished=false;
 		for(uint i=0;i<numDomains; i++) {
@@ -144,13 +161,22 @@ NEXT:
 			}
 		}
 	}
-	if(getSizeVectorEdge(clauses) == 0){
-		deleteVectorEdge(clauses);
-		return E_False;
+	Edge result = E_NULL;
+	if(getSizeVectorEdge(clauses) != 0){
+		result=constraintOR(This->cnf, getSizeVectorEdge(clauses), exposeArrayEdge(clauses));
+		if(generateNegation){
+			ASSERT(getSizeVectorEdge(undefClauses) == 0);
+			result = constraintNegate(result);
+		}
+	}
+	if(getSizeVectorEdge(undefClauses)!= 0){
+		ASSERT(!generateNegation);
+		Edge tmp = constraintAND(This->cnf, getSizeVectorEdge(undefClauses), exposeArrayEdge(undefClauses));
+		result= edgeIsNull(result)? tmp : constraintAND2(This->cnf, tmp, result);
 	}
-	Edge cor=constraintOR(This->cnf, getSizeVectorEdge(clauses), exposeArrayEdge(clauses));
 	deleteVectorEdge(clauses);
-	return generateNegation ? constraintNegate(cor) : cor;
+	deleteVectorEdge(undefClauses);
+	return result;
 }
 
 void encodeEnumEntriesTableElemFuncSATEncoder(SATEncoder* This, ElementFunction* func){