From: Hamed <hamed.gorjiara@gmail.com>
Date: Thu, 20 Jul 2017 02:19:26 +0000 (-0700)
Subject: breaking functionencoding to different files
X-Git-Url: http://demsky.eecs.uci.edu/git/?a=commitdiff_plain;h=77683dd2de7fd732d855c5d190a46c26ba5e5db4;p=satune.git

breaking functionencoding to different files
---

diff --git a/src/Backend/satencoder.c b/src/Backend/satencoder.c
index 6148074..885aab8 100644
--- a/src/Backend/satencoder.c
+++ b/src/Backend/satencoder.c
@@ -11,6 +11,7 @@
 #include "order.h"
 #include "predicate.h"
 #include "set.h"
+#include "satfuncopencoder.h"
 
 //TODO: Should handle sharing of AST Nodes without recoding them a second time
 
diff --git a/src/Backend/satencoder.h b/src/Backend/satencoder.h
index 8241b93..aceb271 100644
--- a/src/Backend/satencoder.h
+++ b/src/Backend/satencoder.h
@@ -13,7 +13,7 @@ struct SATEncoder {
 
 #include "satelemencoder.h"
 #include "satorderencoder.h"
-#include "satfuncencoder.h"
+#include "satfunctableencoder.h"
 
 SATEncoder * allocSATEncoder();
 void deleteSATEncoder(SATEncoder *This);
diff --git a/src/Backend/satfuncencoder.c b/src/Backend/satfuncencoder.c
deleted file mode 100644
index 683336f..0000000
--- a/src/Backend/satfuncencoder.c
+++ /dev/null
@@ -1,402 +0,0 @@
-#include "satencoder.h"
-#include "common.h"
-#include "function.h"
-#include "ops.h"
-#include "predicate.h"
-#include "boolean.h"
-#include "table.h"
-#include "tableentry.h"
-#include "set.h"
-#include "element.h"
-#include "common.h"
-
-Edge encodeEnumEntriesTablePredicateSATEncoder(SATEncoder * This, BooleanPredicate * constraint){
-	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->entrie);
-	bool generateNegation = encType == ENUMERATEIMPLICATIONSNEGATE;
-	Edge constraints[size];
-	HSIteratorTableEntry* iterator = iteratorTableEntry(table->entrie);
-	uint i=0;
-	while(hasNextTableEntry(iterator)){
-		TableEntry* entry = nextTableEntry(iterator);
-		if(generateNegation == entry->output) {
-			//Skip the irrelevant entries
-			continue;
-		}
-		Edge carray[inputNum];
-		for(uint j=0; j<inputNum; j++){
-			Element* el = getArrayElement(inputs, j);
-			carray[j] = getElementValueConstraint(This, el, entry->inputs[j]);
-		}
-		constraints[i++]=constraintAND(This->cnf, inputNum, carray);
-	}
-	Edge result=constraintOR(This->cnf, size, constraints);
-
-	return generateNegation ? constraintNegate(result) : result;
-}
-Edge encodeEnumTablePredicateSATEncoder(SATEncoder * This, BooleanPredicate * constraint){
-	//FIXME
-	return E_NULL;
-}
-
-Edge encodeOperatorPredicateSATEncoder(SATEncoder * This, BooleanPredicate * constraint) {
-	switch(constraint->encoding.type){
-		case ENUMERATEIMPLICATIONS:
-			return encodeEnumOperatorPredicateSATEncoder(This, constraint);
-		case CIRCUIT:
-			return encodeCircuitOperatorPredicateEncoder(This, constraint);
-		default:
-			ASSERT(0);
-	}
-	exit(-1);
-}
-
-Edge encodeCircuitOperatorPredicateEncoder(SATEncoder *This, BooleanPredicate * constraint) {
-	PredicateOperator * predicate = (PredicateOperator*) constraint->predicate;
-	
-	switch(predicate->op) {
-	case EQUALS: {
-		return encodeCircuitEquals(This, constraint);
-	}
-	default:
-		ASSERT(0);
-	}
-	exit(-1);
-}
-
-Edge encodeCircuitEquals(SATEncoder * This, BooleanPredicate * constraint) {
-	PredicateOperator * predicate = (PredicateOperator*) constraint->predicate;
-	ASSERT(getSizeArraySet(&predicate->domains) == 2);
-	Element *elem0 = getArrayElement( &constraint->inputs, 0);
-	Element *elem1 = getArrayElement( &constraint->inputs, 1);
-	ElementEncoding *ee0=getElementEncoding(elem0);
-	ElementEncoding *ee1=getElementEncoding(elem1);
-	ASSERT(ee0->numVars==ee1->numVars);
-	uint numVars=ee0->numVars;
-	Edge carray[numVars];
-	for (uint i=0; i<numVars; i++) {
-		carray[i]=constraintIFF(This->cnf, ee0->variables[i], ee1->variables[i]);
-	}
-	return constraintAND(This->cnf, numVars, carray);
-}
-
-Edge encodeEnumOperatorPredicateSATEncoder(SATEncoder * This, BooleanPredicate * constraint) {
-	PredicateOperator* predicate = (PredicateOperator*)constraint->predicate;
-	uint numDomains=getSizeArraySet(&predicate->domains);
-
-	FunctionEncodingType encType = constraint->encoding.type;
-	bool generateNegation = encType == ENUMERATEIMPLICATIONSNEGATE;
-
-	/* Call base encoders for children */
-	for(uint i=0;i<numDomains;i++) {
-		Element *elem = getArrayElement( &constraint->inputs, i);
-		encodeElementSATEncoder(This, elem);
-	}
-	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->domains, i);
-		vals[i]=getSetElement(set, indices[i]);
-	}
-	
-	bool notfinished=true;
-	while(notfinished) {
-		Edge carray[numDomains];
-
-		if (evalPredicateOperator(predicate, vals) ^ generateNegation) {
-			//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 term=constraintAND(This->cnf, numDomains, carray);
-			pushVectorEdge(clauses, term);
-		}
-		
-		notfinished=false;
-		for(uint i=0;i<numDomains; i++) {
-			uint index=++indices[i];
-			Set * set=getArraySet(&predicate->domains, i);
-
-			if (index < getSetSize(set)) {
-				vals[i]=getSetElement(set, index);
-				notfinished=true;
-				break;
-			} else {
-				indices[i]=0;
-				vals[i]=getSetElement(set, 0);
-			}
-		}
-	}
-	if(getSizeVectorEdge(clauses) == 0)
-		return E_False;
-	Edge cor=constraintOR(This->cnf, getSizeVectorEdge(clauses), exposeArrayEdge(clauses));
-	deleteVectorEdge(clauses);
-	return generateNegation ? constraintNegate(cor) : cor;
-}
-
-
-void encodeOperatorElementFunctionSATEncoder(SATEncoder* This, ElementFunction* func) {
-#ifdef TRACE_DEBUG
-	model_print("Operator Function ...\n");
-#endif
-	FunctionOperator * function = (FunctionOperator *) func->function;
-	uint numDomains=getSizeArrayElement(&func->inputs);
-
-	/* Call base encoders for children */
-	for(uint i=0;i<numDomains;i++) {
-		Element *elem = getArrayElement( &func->inputs, i);
-		encodeElementSATEncoder(This, elem);
-	}
-
-	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=getElementSet(getArrayElement(&func->inputs, i));
-		vals[i]=getSetElement(set, indices[i]);
-	}
-
-	Edge overFlowConstraint = ((BooleanVar*) func->overflowstatus)->var;
-	
-	bool notfinished=true;
-	while(notfinished) {
-		Edge carray[numDomains+1];
-
-		uint64_t result=applyFunctionOperator(function, numDomains, vals);
-		bool isInRange = isInRangeFunction((FunctionOperator*)func->function, result);
-		bool needClause = isInRange;
-		if (function->overflowbehavior == OVERFLOWSETSFLAG || function->overflowbehavior == FLAGIFFOVERFLOW) {
-			needClause=true;
-		}
-		
-		if (needClause) {
-			//Include this in the set of terms
-			for(uint i=0;i<numDomains;i++) {
-				Element * elem = getArrayElement(&func->inputs, i);
-				carray[i] = getElementValueConstraint(This, elem, vals[i]);
-			}
-			if (isInRange) {
-				carray[numDomains] = getElementValueConstraint(This, &func->base, result);
-			}
-
-			Edge clause;
-			switch(function->overflowbehavior) {
-			case IGNORE:
-			case NOOVERFLOW:
-			case WRAPAROUND: {
-				clause=constraintIMPLIES(This->cnf,constraintAND(This->cnf, numDomains, carray), carray[numDomains]);
-				break;
-			}
-			case FLAGFORCESOVERFLOW: {
-				clause=constraintIMPLIES(This->cnf,constraintAND(This->cnf, numDomains, carray), constraintAND2(This->cnf, carray[numDomains], constraintNegate(overFlowConstraint)));
-				break;
-			}
-			case OVERFLOWSETSFLAG: {
-				if (isInRange) {
-					clause=constraintIMPLIES(This->cnf,constraintAND(This->cnf, numDomains, carray), carray[numDomains]);
-				} else {
-					clause=constraintIMPLIES(This->cnf,constraintAND(This->cnf, numDomains, carray), overFlowConstraint);
-				}
-				break;
-			}
-			case FLAGIFFOVERFLOW: {
-				if (isInRange) {
-					clause=constraintIMPLIES(This->cnf,constraintAND(This->cnf, numDomains, carray), constraintAND2(This->cnf, carray[numDomains], constraintNegate(overFlowConstraint)));
-				} else {
-					clause=constraintIMPLIES(This->cnf,constraintAND(This->cnf, numDomains, carray), overFlowConstraint);
-				}
-				break;
-			}
-			default:
-				ASSERT(0);
-			}
-#ifdef TRACE_DEBUG
-			model_print("added clause in operator function\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=getElementSet(getArrayElement(&func->inputs, i));
-
-			if (index < getSetSize(set)) {
-				vals[i]=getSetElement(set, index);
-				notfinished=true;
-				break;
-			} else {
-				indices[i]=0;
-				vals[i]=getSetElement(set, 0);
-			}
-		}
-	}
-
-	Edge cor=constraintAND(This->cnf, getSizeVectorEdge(clauses), exposeArrayEdge(clauses));
-	addConstraintCNF(This->cnf, cor);
-	deleteVectorEdge(clauses);
-}
-
-void encodeEnumEntriesTableElemFuncSATEncoder(SATEncoder* This, ElementFunction* func){
-	UndefinedBehavior undefStatus = ((FunctionTable*) func->function)->undefBehavior;
-	ASSERT(undefStatus == IGNOREBEHAVIOR || undefStatus == FLAGFORCEUNDEFINED);
-	ArrayElement* elements= &func->inputs;
-	Table* table = ((FunctionTable*) (func->function))->table;
-	uint size = getSizeHashSetTableEntry(table->entrie);
-	Edge constraints[size];
-	HSIteratorTableEntry* iterator = iteratorTableEntry(table->entrie);
-	uint i=0;
-	while(hasNextTableEntry(iterator)) {
-		TableEntry* entry = nextTableEntry(iterator);
-		ASSERT(entry!=NULL);
-		uint inputNum = getSizeArrayElement(elements);
-		Edge carray[inputNum];
-		for(uint j=0; j<inputNum; j++){
-			Element* el= getArrayElement(elements, j);
-			carray[j] = getElementValueConstraint(This, el, entry->inputs[j]);
-		}
-		Edge output = getElementValueConstraint(This, (Element*)func, entry->output);
-		Edge row;
-		switch(undefStatus ){
-			case IGNOREBEHAVIOR: {
-				row=constraintIMPLIES(This->cnf,constraintAND(This->cnf, inputNum, carray), output);
-				break;
-			}
-			case FLAGFORCEUNDEFINED: {
-				Edge undefConst = ((BooleanVar*)func->overflowstatus)->var;
-				row=constraintIMPLIES(This->cnf,constraintAND(This->cnf, inputNum, carray), constraintAND2(This->cnf, output, constraintNegate(undefConst)));
-				break;
-			}
-			default:
-				ASSERT(0);
-		
-		}
-		constraints[i++]=row;
-	}
-	deleteIterTableEntry(iterator);
-	addConstraintCNF(This->cnf, constraintAND(This->cnf, size, constraints));
-}
-
-void encodeEnumTableElemFunctionSATEncoder(SATEncoder* This, ElementFunction* elemFunc){
-#ifdef TRACE_DEBUG
-	model_print("Enumeration Table functions ...\n");
-#endif
-	ASSERT(GETFUNCTIONTYPE(elemFunc->function)==TABLEFUNC);
-	//First encode children
-	ArrayElement* elements= &elemFunc->inputs;
-	for(uint i=0; i<getSizeArrayElement(elements); i++){
-		Element *elem = getArrayElement( elements, i);
-		encodeElementSATEncoder(This, elem);
-	}
-
-	FunctionTable* function =(FunctionTable*)elemFunc;
-	switch(function->undefBehavior){
-		case IGNOREBEHAVIOR:
-		case FLAGFORCEUNDEFINED:
-			return encodeEnumEntriesTableElemFuncSATEncoder(This, elemFunc);
-		default:
-			break;
-	}
-	
-	uint numDomains=getSizeArraySet(&function->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(&function->table->domains, i);
-		vals[i]=getSetElement(set, indices[i]);
-	}
-
-	Edge undefConstraint = ((BooleanVar*) elemFunc->overflowstatus)->var;
-	
-	bool notfinished=true;
-	while(notfinished) {
-		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;
-		}
-		
-		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;
-				}
-				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;
-				}
-				default:
-					ASSERT(0);
-			}
-#ifdef TRACE_DEBUG
-			model_print("added clause in 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(&function->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=constraintAND(This->cnf, getSizeVectorEdge(clauses), exposeArrayEdge(clauses));
-	addConstraintCNF(This->cnf, cor);
-	deleteVectorEdge(clauses);
-	
-}
diff --git a/src/Backend/satfuncencoder.h b/src/Backend/satfuncencoder.h
deleted file mode 100644
index 8b8a9a2..0000000
--- a/src/Backend/satfuncencoder.h
+++ /dev/null
@@ -1,14 +0,0 @@
-#ifndef SATFUNCENCODER_H
-#define SATFUNCENCODER_H
-
-Edge encodeEnumEntriesTablePredicateSATEncoder(SATEncoder * This, BooleanPredicate * constraint);
-Edge encodeEnumTablePredicateSATEncoder(SATEncoder * This, BooleanPredicate * constraint);
-Edge encodeOperatorPredicateSATEncoder(SATEncoder * This, BooleanPredicate * constraint);
-Edge encodeEnumOperatorPredicateSATEncoder(SATEncoder * This, BooleanPredicate * constraint);
-void encodeOperatorElementFunctionSATEncoder(SATEncoder* encoder,ElementFunction* This);
-void encodeEnumTableElemFunctionSATEncoder(SATEncoder* encoder, ElementFunction* This);
-void encodeEnumEntriesTableElemFuncSATEncoder(SATEncoder* encoder, ElementFunction* This);
-Edge encodeCircuitOperatorPredicateEncoder(SATEncoder *This, BooleanPredicate * constraint);
-Edge encodeCircuitEquals(SATEncoder * This, BooleanPredicate * constraint);
-
-#endif
diff --git a/src/Backend/satfuncopencoder.c b/src/Backend/satfuncopencoder.c
new file mode 100644
index 0000000..67441d5
--- /dev/null
+++ b/src/Backend/satfuncopencoder.c
@@ -0,0 +1,220 @@
+#include "satencoder.h"
+#include "common.h"
+#include "function.h"
+#include "ops.h"
+#include "predicate.h"
+#include "boolean.h"
+#include "table.h"
+#include "tableentry.h"
+#include "set.h"
+#include "element.h"
+#include "common.h"
+#include "satfuncopencoder.h"
+
+Edge encodeOperatorPredicateSATEncoder(SATEncoder * This, BooleanPredicate * constraint) {
+	switch(constraint->encoding.type){
+		case ENUMERATEIMPLICATIONS:
+			return encodeEnumOperatorPredicateSATEncoder(This, constraint);
+		case CIRCUIT:
+			return encodeCircuitOperatorPredicateEncoder(This, constraint);
+		default:
+			ASSERT(0);
+	}
+	exit(-1);
+}
+
+Edge encodeEnumOperatorPredicateSATEncoder(SATEncoder * This, BooleanPredicate * constraint) {
+	PredicateOperator* predicate = (PredicateOperator*)constraint->predicate;
+	uint numDomains=getSizeArraySet(&predicate->domains);
+
+	FunctionEncodingType encType = constraint->encoding.type;
+	bool generateNegation = encType == ENUMERATEIMPLICATIONSNEGATE;
+
+	/* Call base encoders for children */
+	for(uint i=0;i<numDomains;i++) {
+		Element *elem = getArrayElement( &constraint->inputs, i);
+		encodeElementSATEncoder(This, elem);
+	}
+	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->domains, i);
+		vals[i]=getSetElement(set, indices[i]);
+	}
+	
+	bool notfinished=true;
+	while(notfinished) {
+		Edge carray[numDomains];
+
+		if (evalPredicateOperator(predicate, vals) ^ generateNegation) {
+			//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 term=constraintAND(This->cnf, numDomains, carray);
+			pushVectorEdge(clauses, term);
+		}
+		
+		notfinished=false;
+		for(uint i=0;i<numDomains; i++) {
+			uint index=++indices[i];
+			Set * set=getArraySet(&predicate->domains, i);
+
+			if (index < getSetSize(set)) {
+				vals[i]=getSetElement(set, index);
+				notfinished=true;
+				break;
+			} else {
+				indices[i]=0;
+				vals[i]=getSetElement(set, 0);
+			}
+		}
+	}
+	if(getSizeVectorEdge(clauses) == 0)
+		return E_False;
+	Edge cor=constraintOR(This->cnf, getSizeVectorEdge(clauses), exposeArrayEdge(clauses));
+	deleteVectorEdge(clauses);
+	return generateNegation ? constraintNegate(cor) : cor;
+}
+
+
+void encodeOperatorElementFunctionSATEncoder(SATEncoder* This, ElementFunction* func) {
+#ifdef TRACE_DEBUG
+	model_print("Operator Function ...\n");
+#endif
+	FunctionOperator * function = (FunctionOperator *) func->function;
+	uint numDomains=getSizeArrayElement(&func->inputs);
+
+	/* Call base encoders for children */
+	for(uint i=0;i<numDomains;i++) {
+		Element *elem = getArrayElement( &func->inputs, i);
+		encodeElementSATEncoder(This, elem);
+	}
+
+	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=getElementSet(getArrayElement(&func->inputs, i));
+		vals[i]=getSetElement(set, indices[i]);
+	}
+
+	Edge overFlowConstraint = ((BooleanVar*) func->overflowstatus)->var;
+	
+	bool notfinished=true;
+	while(notfinished) {
+		Edge carray[numDomains+1];
+
+		uint64_t result=applyFunctionOperator(function, numDomains, vals);
+		bool isInRange = isInRangeFunction((FunctionOperator*)func->function, result);
+		bool needClause = isInRange;
+		if (function->overflowbehavior == OVERFLOWSETSFLAG || function->overflowbehavior == FLAGIFFOVERFLOW) {
+			needClause=true;
+		}
+		
+		if (needClause) {
+			//Include this in the set of terms
+			for(uint i=0;i<numDomains;i++) {
+				Element * elem = getArrayElement(&func->inputs, i);
+				carray[i] = getElementValueConstraint(This, elem, vals[i]);
+			}
+			if (isInRange) {
+				carray[numDomains] = getElementValueConstraint(This, &func->base, result);
+			}
+
+			Edge clause;
+			switch(function->overflowbehavior) {
+			case IGNORE:
+			case NOOVERFLOW:
+			case WRAPAROUND: {
+				clause=constraintIMPLIES(This->cnf,constraintAND(This->cnf, numDomains, carray), carray[numDomains]);
+				break;
+			}
+			case FLAGFORCESOVERFLOW: {
+				clause=constraintIMPLIES(This->cnf,constraintAND(This->cnf, numDomains, carray), constraintAND2(This->cnf, carray[numDomains], constraintNegate(overFlowConstraint)));
+				break;
+			}
+			case OVERFLOWSETSFLAG: {
+				if (isInRange) {
+					clause=constraintIMPLIES(This->cnf,constraintAND(This->cnf, numDomains, carray), carray[numDomains]);
+				} else {
+					clause=constraintIMPLIES(This->cnf,constraintAND(This->cnf, numDomains, carray), overFlowConstraint);
+				}
+				break;
+			}
+			case FLAGIFFOVERFLOW: {
+				if (isInRange) {
+					clause=constraintIMPLIES(This->cnf,constraintAND(This->cnf, numDomains, carray), constraintAND2(This->cnf, carray[numDomains], constraintNegate(overFlowConstraint)));
+				} else {
+					clause=constraintIMPLIES(This->cnf,constraintAND(This->cnf, numDomains, carray), overFlowConstraint);
+				}
+				break;
+			}
+			default:
+				ASSERT(0);
+			}
+#ifdef TRACE_DEBUG
+			model_print("added clause in operator function\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=getElementSet(getArrayElement(&func->inputs, i));
+
+			if (index < getSetSize(set)) {
+				vals[i]=getSetElement(set, index);
+				notfinished=true;
+				break;
+			} else {
+				indices[i]=0;
+				vals[i]=getSetElement(set, 0);
+			}
+		}
+	}
+
+	Edge cor=constraintAND(This->cnf, getSizeVectorEdge(clauses), exposeArrayEdge(clauses));
+	addConstraintCNF(This->cnf, cor);
+	deleteVectorEdge(clauses);
+}
+
+Edge encodeCircuitOperatorPredicateEncoder(SATEncoder *This, BooleanPredicate * constraint) {
+	PredicateOperator * predicate = (PredicateOperator*) constraint->predicate;
+	
+	switch(predicate->op) {
+	case EQUALS: {
+		return encodeCircuitEquals(This, constraint);
+	}
+	default:
+		ASSERT(0);
+	}
+	exit(-1);
+}
+
+Edge encodeCircuitEquals(SATEncoder * This, BooleanPredicate * constraint) {
+	PredicateOperator * predicate = (PredicateOperator*) constraint->predicate;
+	ASSERT(getSizeArraySet(&predicate->domains) == 2);
+	Element *elem0 = getArrayElement( &constraint->inputs, 0);
+	Element *elem1 = getArrayElement( &constraint->inputs, 1);
+	ElementEncoding *ee0=getElementEncoding(elem0);
+	ElementEncoding *ee1=getElementEncoding(elem1);
+	ASSERT(ee0->numVars==ee1->numVars);
+	uint numVars=ee0->numVars;
+	Edge carray[numVars];
+	for (uint i=0; i<numVars; i++) {
+		carray[i]=constraintIFF(This->cnf, ee0->variables[i], ee1->variables[i]);
+	}
+	return constraintAND(This->cnf, numVars, carray);
+}
\ No newline at end of file
diff --git a/src/Backend/satfuncopencoder.h b/src/Backend/satfuncopencoder.h
new file mode 100644
index 0000000..0bfca3d
--- /dev/null
+++ b/src/Backend/satfuncopencoder.h
@@ -0,0 +1,10 @@
+#ifndef SATFUNCOPENCODER_H
+#define SATFUNCOPENCODER_H
+
+Edge encodeOperatorPredicateSATEncoder(SATEncoder * This, BooleanPredicate * constraint);
+Edge encodeEnumOperatorPredicateSATEncoder(SATEncoder * This, BooleanPredicate * constraint);
+void encodeOperatorElementFunctionSATEncoder(SATEncoder* encoder,ElementFunction* This);
+Edge encodeCircuitOperatorPredicateEncoder(SATEncoder *This, BooleanPredicate * constraint);
+Edge encodeCircuitEquals(SATEncoder * This, BooleanPredicate * constraint);
+
+#endif
diff --git a/src/Backend/satfunctableencoder.c b/src/Backend/satfunctableencoder.c
new file mode 100644
index 0000000..8ed9a2c
--- /dev/null
+++ b/src/Backend/satfunctableencoder.c
@@ -0,0 +1,194 @@
+#include "satencoder.h"
+#include "common.h"
+#include "function.h"
+#include "ops.h"
+#include "predicate.h"
+#include "boolean.h"
+#include "table.h"
+#include "tableentry.h"
+#include "set.h"
+#include "element.h"
+#include "common.h"
+
+Edge encodeEnumEntriesTablePredicateSATEncoder(SATEncoder * This, BooleanPredicate * constraint){
+	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->entrie);
+	bool generateNegation = encType == ENUMERATEIMPLICATIONSNEGATE;
+	Edge constraints[size];
+	HSIteratorTableEntry* iterator = iteratorTableEntry(table->entrie);
+	uint i=0;
+	while(hasNextTableEntry(iterator)){
+		TableEntry* entry = nextTableEntry(iterator);
+		if(generateNegation == entry->output) {
+			//Skip the irrelevant entries
+			continue;
+		}
+		Edge carray[inputNum];
+		for(uint j=0; j<inputNum; j++){
+			Element* el = getArrayElement(inputs, j);
+			carray[j] = getElementValueConstraint(This, el, entry->inputs[j]);
+		}
+		constraints[i++]=constraintAND(This->cnf, inputNum, carray);
+	}
+	Edge result=constraintOR(This->cnf, size, constraints);
+
+	return generateNegation ? constraintNegate(result) : result;
+}
+Edge encodeEnumTablePredicateSATEncoder(SATEncoder * This, BooleanPredicate * constraint){
+	//FIXME
+	return E_NULL;
+}
+
+void encodeEnumEntriesTableElemFuncSATEncoder(SATEncoder* This, ElementFunction* func){
+	UndefinedBehavior undefStatus = ((FunctionTable*) func->function)->undefBehavior;
+	ASSERT(undefStatus == IGNOREBEHAVIOR || undefStatus == FLAGFORCEUNDEFINED);
+	ArrayElement* elements= &func->inputs;
+	Table* table = ((FunctionTable*) (func->function))->table;
+	uint size = getSizeHashSetTableEntry(table->entrie);
+	Edge constraints[size];
+	HSIteratorTableEntry* iterator = iteratorTableEntry(table->entrie);
+	uint i=0;
+	while(hasNextTableEntry(iterator)) {
+		TableEntry* entry = nextTableEntry(iterator);
+		ASSERT(entry!=NULL);
+		uint inputNum = getSizeArrayElement(elements);
+		Edge carray[inputNum];
+		for(uint j=0; j<inputNum; j++){
+			Element* el= getArrayElement(elements, j);
+			carray[j] = getElementValueConstraint(This, el, entry->inputs[j]);
+		}
+		Edge output = getElementValueConstraint(This, (Element*)func, entry->output);
+		Edge row;
+		switch(undefStatus ){
+			case IGNOREBEHAVIOR: {
+				row=constraintIMPLIES(This->cnf,constraintAND(This->cnf, inputNum, carray), output);
+				break;
+			}
+			case FLAGFORCEUNDEFINED: {
+				Edge undefConst = ((BooleanVar*)func->overflowstatus)->var;
+				row=constraintIMPLIES(This->cnf,constraintAND(This->cnf, inputNum, carray), constraintAND2(This->cnf, output, constraintNegate(undefConst)));
+				break;
+			}
+			default:
+				ASSERT(0);
+		
+		}
+		constraints[i++]=row;
+	}
+	deleteIterTableEntry(iterator);
+	addConstraintCNF(This->cnf, constraintAND(This->cnf, size, constraints));
+}
+
+void encodeEnumTableElemFunctionSATEncoder(SATEncoder* This, ElementFunction* elemFunc){
+#ifdef TRACE_DEBUG
+	model_print("Enumeration Table functions ...\n");
+#endif
+	ASSERT(GETFUNCTIONTYPE(elemFunc->function)==TABLEFUNC);
+	//First encode children
+	ArrayElement* elements= &elemFunc->inputs;
+	for(uint i=0; i<getSizeArrayElement(elements); i++){
+		Element *elem = getArrayElement( elements, i);
+		encodeElementSATEncoder(This, elem);
+	}
+
+	FunctionTable* function =(FunctionTable*)elemFunc;
+	switch(function->undefBehavior){
+		case IGNOREBEHAVIOR:
+		case FLAGFORCEUNDEFINED:
+			return encodeEnumEntriesTableElemFuncSATEncoder(This, elemFunc);
+		default:
+			break;
+	}
+	
+	uint numDomains=getSizeArraySet(&function->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(&function->table->domains, i);
+		vals[i]=getSetElement(set, indices[i]);
+	}
+
+	Edge undefConstraint = ((BooleanVar*) elemFunc->overflowstatus)->var;
+	
+	bool notfinished=true;
+	while(notfinished) {
+		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;
+		}
+		
+		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;
+				}
+				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;
+				}
+				default:
+					ASSERT(0);
+			}
+#ifdef TRACE_DEBUG
+			model_print("added clause in 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(&function->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=constraintAND(This->cnf, getSizeVectorEdge(clauses), exposeArrayEdge(clauses));
+	addConstraintCNF(This->cnf, cor);
+	deleteVectorEdge(clauses);
+	
+}
diff --git a/src/Backend/satfunctableencoder.h b/src/Backend/satfunctableencoder.h
new file mode 100644
index 0000000..6ac111c
--- /dev/null
+++ b/src/Backend/satfunctableencoder.h
@@ -0,0 +1,9 @@
+#ifndef SATFUNCTABLEENCODER_H
+#define SATFUNCTABLEENCODER_H
+
+Edge encodeEnumEntriesTablePredicateSATEncoder(SATEncoder * This, BooleanPredicate * constraint);
+Edge encodeEnumTablePredicateSATEncoder(SATEncoder * This, BooleanPredicate * constraint);
+void encodeEnumTableElemFunctionSATEncoder(SATEncoder* encoder, ElementFunction* This);
+void encodeEnumEntriesTableElemFuncSATEncoder(SATEncoder* encoder, ElementFunction* This);
+
+#endif