From: Hamed <hamed.gorjiara@gmail.com>
Date: Thu, 20 Jul 2017 18:29:40 +0000 (-0700)
Subject: adding different handlers for predicatetable
X-Git-Url: http://plrg.eecs.uci.edu/git/?p=satune.git;a=commitdiff_plain;h=deb51959f6d6c404832bc332c54882fcd3d8c454

adding different handlers for predicatetable
---

diff --git a/src/Backend/satfunctableencoder.c b/src/Backend/satfunctableencoder.c
index 64b5efb..a9ba7b1 100644
--- a/src/Backend/satfunctableencoder.c
+++ b/src/Backend/satfunctableencoder.c
@@ -11,14 +11,13 @@
 #include "common.h"
 
 Edge encodeEnumEntriesTablePredicateSATEncoder(SATEncoder * This, BooleanPredicate * constraint){
+	ASSERT(GETPREDICATETYPE(constraint->predicate) == TABLEPRED);
+	UndefinedBehavior undefStatus = ((PredicateTable*)constraint->predicate)->undefinedbehavior;
+	ASSERT(undefStatus == IGNOREBEHAVIOR || undefStatus == FLAGFORCEUNDEFINED);
 	Table* table = ((PredicateTable*)constraint->predicate)->table;
 	FunctionEncodingType encType = constraint->encoding.type;
 	ArrayElement* inputs = &constraint->inputs;
 	uint inputNum =getSizeArrayElement(inputs);
-	//Encode all the inputs first ...
-	for(uint i=0; i<inputNum; i++){
-		encodeElementSATEncoder(This, getArrayElement(inputs, i));
-	}
 	uint size = getSizeHashSetTableEntry(table->entries);
 	bool generateNegation = encType == ENUMERATEIMPLICATIONSNEGATE;
 	Edge constraints[size];
@@ -35,15 +34,123 @@ Edge encodeEnumEntriesTablePredicateSATEncoder(SATEncoder * This, BooleanPredica
 			Element* el = getArrayElement(inputs, j);
 			carray[j] = getElementValueConstraint(This, el, entry->inputs[j]);
 		}
-		constraints[i++]=constraintAND(This->cnf, inputNum, carray);
+		Edge row;
+		switch(undefStatus){
+			case IGNOREBEHAVIOR:
+				row=constraintAND(This->cnf, inputNum, carray);
+				break;
+			case FLAGFORCEUNDEFINED:{
+				Edge undefConst = ((BooleanVar*)constraint->undefStatus)->var;
+				row=constraintIMPLIES(This->cnf,constraintAND(This->cnf, inputNum, carray),  constraintNegate(undefConst));
+				break;
+			}
+			default:
+				ASSERT(0);
+		}
+		constraints[i++] = row;
+		
 	}
 	Edge result=constraintOR(This->cnf, size, constraints);
 
 	return generateNegation ? constraintNegate(result) : result;
 }
 Edge encodeEnumTablePredicateSATEncoder(SATEncoder * This, BooleanPredicate * constraint){
-	//FIXME
-	return E_NULL;
+#ifdef TRACE_DEBUG
+	model_print("Enumeration Table Predicate ...\n");
+#endif
+	ASSERT(GETPREDICATETYPE(constraint->predicate) == TABLEPRED);
+	//First encode children
+	ArrayElement* inputs = &constraint->inputs;
+	uint inputNum =getSizeArrayElement(inputs);
+	//Encode all the inputs first ...
+	for(uint i=0; i<inputNum; i++){
+		encodeElementSATEncoder(This, getArrayElement(inputs, i));
+	}
+	PredicateTable* predicate = (PredicateTable*)constraint->predicate;
+	switch(predicate->undefinedbehavior){
+		case IGNOREBEHAVIOR:
+		case FLAGFORCEUNDEFINED:
+			return encodeEnumEntriesTablePredicateSATEncoder(This, constraint);
+		default:
+			break;
+	}
+	bool generateNegation = constraint->encoding.type == ENUMERATEIMPLICATIONSNEGATE;
+	uint numDomains=getSizeArraySet(&predicate->table->domains);
+
+	VectorEdge * clauses=allocDefVectorEdge(); // Setup array of clauses
+	
+	uint indices[numDomains]; //setup indices
+	bzero(indices, sizeof(uint)*numDomains);
+	
+	uint64_t vals[numDomains]; //setup value array
+	for(uint i=0;i<numDomains; i++) {
+		Set * set=getArraySet(&predicate->table->domains, i);
+		vals[i]=getSetElement(set, indices[i]);
+	}
+
+	Edge undefConstraint = ((BooleanVar*) constraint->undefStatus)->var;
+	
+	bool notfinished=true;
+	while(notfinished) {
+		Edge carray[numDomains];
+		TableEntry* tableEntry = getTableEntryFromTable(predicate->table, vals, numDomains);
+		bool isInRange = tableEntry!=NULL;
+		bool ignoreEntry = generateNegation == tableEntry->output;
+		ASSERT(predicate->undefinedbehavior == UNDEFINEDSETSFLAG || predicate->undefinedbehavior == FLAGIFFUNDEFINED);
+		//Include this in the set of terms
+		for(uint i=0;i<numDomains;i++) {
+			Element * elem = getArrayElement(&constraint->inputs, i);
+			carray[i] = getElementValueConstraint(This, elem, vals[i]);
+		}
+
+		Edge clause;
+		switch(predicate->undefinedbehavior) {
+			case UNDEFINEDSETSFLAG: {
+				if (isInRange && !ignoreEntry) {
+					clause=constraintAND(This->cnf, numDomains, carray);
+				} else if(!isInRange) {
+					clause=constraintIMPLIES(This->cnf,constraintAND(This->cnf, numDomains, carray), undefConstraint);
+				}
+				break;
+			}
+			case FLAGIFFUNDEFINED: {
+				if (isInRange && !ignoreEntry) {
+					clause=constraintIMPLIES(This->cnf,constraintAND(This->cnf, numDomains, carray), constraintAND2(This->cnf, carray[numDomains], constraintNegate(undefConstraint)));
+				} else if(!isInRange) {
+					clause=constraintIMPLIES(This->cnf,constraintAND(This->cnf, numDomains, carray), undefConstraint);
+				}
+				break;
+			}
+			default:
+				ASSERT(0);
+		}
+#ifdef TRACE_DEBUG
+		model_print("added clause in predicate table enumeration ...\n");
+		printCNF(clause);
+		model_print("\n");
+#endif
+		pushVectorEdge(clauses, clause);
+		
+		
+		notfinished=false;
+		for(uint i=0;i<numDomains; i++) {
+			uint index=++indices[i];
+			Set * set=getArraySet(&predicate->table->domains, i);
+
+			if (index < getSetSize(set)) {
+				vals[i]=getSetElement(set, index);
+				notfinished=true;
+				break;
+			} else {
+				indices[i]=0;
+				vals[i]=getSetElement(set, 0);
+			}
+		}
+	}
+
+	Edge cor=constraintOR(This->cnf, getSizeVectorEdge(clauses), exposeArrayEdge(clauses));
+	deleteVectorEdge(clauses);
+	return generateNegation ? constraintNegate(cor) : cor;
 }
 
 void encodeEnumEntriesTableElemFuncSATEncoder(SATEncoder* This, ElementFunction* func){
@@ -127,49 +234,44 @@ void encodeEnumTableElemFunctionSATEncoder(SATEncoder* This, ElementFunction* el
 		Edge carray[numDomains+1];
 		TableEntry* tableEntry = getTableEntryFromTable(function->table, vals, numDomains);
 		bool isInRange = tableEntry!=NULL;
-		bool needClause = isInRange;
-		if (function->undefBehavior == UNDEFINEDSETSFLAG || function->undefBehavior == FLAGIFFUNDEFINED) {
-			needClause=true;
+		ASSERT(function->undefBehavior == UNDEFINEDSETSFLAG || function->undefBehavior == FLAGIFFUNDEFINED);
+		//Include this in the set of terms
+		for(uint i=0;i<numDomains;i++) {
+			Element * elem = getArrayElement(&elemFunc->inputs, i);
+			carray[i] = getElementValueConstraint(This, elem, vals[i]);
+		}
+		if (isInRange) {
+			carray[numDomains] = getElementValueConstraint(This, (Element*)elemFunc, tableEntry->output);
 		}
-		
-		if (needClause) {
-			//Include this in the set of terms
-			for(uint i=0;i<numDomains;i++) {
-				Element * elem = getArrayElement(&elemFunc->inputs, i);
-				carray[i] = getElementValueConstraint(This, elem, vals[i]);
-			}
-			if (isInRange) {
-				carray[numDomains] = getElementValueConstraint(This, (Element*)elemFunc, tableEntry->output);
-			}
 
-			Edge clause;
-			switch(function->undefBehavior) {
-				case UNDEFINEDSETSFLAG: {
-					if (isInRange) {
-						clause=constraintIMPLIES(This->cnf,constraintAND(This->cnf, numDomains, carray), carray[numDomains]);
-					} else {
-						clause=constraintIMPLIES(This->cnf,constraintAND(This->cnf, numDomains, carray), undefConstraint);
-					}
-					break;
+		Edge clause;
+		switch(function->undefBehavior) {
+			case UNDEFINEDSETSFLAG: {
+				if (isInRange) {
+					clause=constraintIMPLIES(This->cnf,constraintAND(This->cnf, numDomains, carray), carray[numDomains]);
+				} else {
+					clause=constraintIMPLIES(This->cnf,constraintAND(This->cnf, numDomains, carray), undefConstraint);
 				}
-				case FLAGIFFUNDEFINED: {
-					if (isInRange) {
-						clause=constraintIMPLIES(This->cnf,constraintAND(This->cnf, numDomains, carray), constraintAND2(This->cnf, carray[numDomains], constraintNegate(undefConstraint)));
-					} else {
-						clause=constraintIMPLIES(This->cnf,constraintAND(This->cnf, numDomains, carray), undefConstraint);
-					}
-					break;
+				break;
+			}
+			case FLAGIFFUNDEFINED: {
+				if (isInRange) {
+					clause=constraintIMPLIES(This->cnf,constraintAND(This->cnf, numDomains, carray), constraintAND2(This->cnf, carray[numDomains], constraintNegate(undefConstraint)));
+				} else {
+					clause=constraintIMPLIES(This->cnf,constraintAND(This->cnf, numDomains, carray), undefConstraint);
 				}
-				default:
-					ASSERT(0);
+				break;
 			}
+			default:
+				ASSERT(0);
+		}
 #ifdef TRACE_DEBUG
-			model_print("added clause in 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++) {