From 008491e1f8f6b2d6610af0c1ecb667f3789bc06c Mon Sep 17 00:00:00 2001
From: bdemsky <bdemsky@uci.edu>
Date: Tue, 11 Jul 2017 15:18:57 -0700
Subject: [PATCH] Rewrite function operator code

---
 src/AST/element.c        |   4 +-
 src/AST/element.h        |   4 +-
 src/AST/function.c       |   9 +-
 src/AST/function.h       |   2 +-
 src/Backend/satencoder.c | 216 +++++++++++++++++++--------------------
 5 files changed, 113 insertions(+), 122 deletions(-)

diff --git a/src/AST/element.c b/src/AST/element.c
index f9b7579..5a056e9 100644
--- a/src/AST/element.c
+++ b/src/AST/element.c
@@ -23,7 +23,7 @@ Element* allocElementFunction(Function * function, Element ** array, uint numArr
 	initDefVectorASTNode(GETELEMENTPARENTS(This));
 	for(uint i=0;i<numArrays;i++)
 		pushVectorASTNode(GETELEMENTPARENTS(array[i]), (ASTNode *) This);
-	initElementEncoding(&This->domainencoding, (Element *) This);
+	initElementEncoding(&This->rangeencoding, (Element *) This);
 	initFunctionEncoding(&This->functionencoding, (Element *) This);
 	return &This->base;
 }
@@ -55,7 +55,7 @@ void deleteElement(Element *This) {
 	case ELEMFUNCRETURN: {
 		ElementFunction *ef = (ElementFunction *) This;
 		deleteInlineArrayElement(&ef->inputs);
-		deleteElementEncoding(&ef->domainencoding);
+		deleteElementEncoding(&ef->rangeencoding);
 		deleteFunctionEncoding(&ef->functionencoding);
 		break;
 	}
diff --git a/src/AST/element.h b/src/AST/element.h
index bce0073..26d4989 100644
--- a/src/AST/element.h
+++ b/src/AST/element.h
@@ -27,7 +27,7 @@ struct ElementFunction {
 	ArrayElement inputs;
 	Boolean * overflowstatus;
 	FunctionEncoding functionencoding;
-	ElementEncoding domainencoding;
+	ElementEncoding rangeencoding;
 };
 
 Element * allocElementSet(Set *s);
@@ -40,7 +40,7 @@ static inline ElementEncoding* getElementEncoding(Element* This){
 		case ELEMSET:
 			return &((ElementSet*)This)->encoding;
 		case ELEMFUNCRETURN:		
-			return &((ElementFunction*)This)->domainencoding;
+			return &((ElementFunction*)This)->rangeencoding;
 		default:
 			ASSERT(0);
 	}
diff --git a/src/AST/function.c b/src/AST/function.c
index 1aba4b7..20e57b0 100644
--- a/src/AST/function.c
+++ b/src/AST/function.c
@@ -20,19 +20,18 @@ Function* allocFunctionTable (Table* table){
 	return &This->base;
 }
 
-uint64_t applyFunctionOperator(FunctionOperator* This, uint64_t var1, uint64_t var2) {
-	uint64_t result = 0;
+uint64_t applyFunctionOperator(FunctionOperator* This, uint numVals, uint64_t * values) {
+	ASSERT(numVals == 2);
 	switch(This->op){
 		case ADD:
-			result = var1+ var2;
+			return values[0] + values[1];
 			break;
 		case SUB:
-			result = var1 - var2;
+			return values[0] - values[1];
 			break;
 		default:
 			ASSERT(0);
 	}
-	return result;
 }
 
 bool isInRangeFunction(FunctionOperator *This, uint64_t val) {
diff --git a/src/AST/function.h b/src/AST/function.h
index 17a3211..28f53c7 100644
--- a/src/AST/function.h
+++ b/src/AST/function.h
@@ -26,7 +26,7 @@ struct FunctionTable {
 
 Function* allocFunctionOperator(ArithOp op, Set ** domain, uint numDomain, Set * range, OverFlowBehavior overflowbehavior);
 Function* allocFunctionTable (Table* table);
-uint64_t applyFunctionOperator(FunctionOperator* This, uint64_t var1, uint64_t var2);
+uint64_t applyFunctionOperator(FunctionOperator* This, uint numVals, uint64_t * values);
 bool isInRangeFunction(FunctionOperator *This, uint64_t val);
 void deleteFunction(Function* This);
 
diff --git a/src/Backend/satencoder.c b/src/Backend/satencoder.c
index cfeb82a..5ef2c53 100644
--- a/src/Backend/satencoder.c
+++ b/src/Backend/satencoder.c
@@ -132,7 +132,6 @@ Edge encodeLogicSATEncoder(SATEncoder *This, BooleanLogic * constraint) {
 	}
 }
 
-
 Edge encodeOrderSATEncoder(SATEncoder *This, BooleanOrder * constraint) {
 	switch( constraint->order->type){
 		case PARTIAL:
@@ -161,16 +160,13 @@ Edge getPairConstraint(SATEncoder *This, HashTableOrderPair * table, OrderPair *
 		putOrderPair(table, paircopy, paircopy);
 	} else
 		constraint = getOrderPair(table, pair)->constraint;
-	if (negate)
-		return constraintNegate(constraint);
-	else
-		return constraint;
-	
+
+	return negate ? constraintNegate(constraint) : constraint;
 }
 
-Edge encodeTotalOrderSATEncoder(SATEncoder *This, BooleanOrder * boolOrder){
+Edge encodeTotalOrderSATEncoder(SATEncoder *This, BooleanOrder * boolOrder) {
 	ASSERT(boolOrder->order->type == TOTAL);
-	if(boolOrder->order->orderPairTable == NULL){
+	if(boolOrder->order->orderPairTable == NULL) {
 		initializeOrderHashTable(boolOrder->order);
 		createAllTotalOrderConstraintsSATEncoder(This, boolOrder->order);
 	}
@@ -222,41 +218,7 @@ Edge generateTransOrderConstraintSATEncoder(SATEncoder *This, Edge constIJ,Edge
 }
 
 Edge encodePartialOrderSATEncoder(SATEncoder *This, BooleanOrder * constraint){
-	// FIXME: we can have this implementation for partial order. Basically,
-	// we compute the transitivity between two order constraints specified by the client! (also can be used
-	// when client specify sparse constraints for the total order!)
 	ASSERT(constraint->order->type == PARTIAL);
-/*
-	HashTableOrderPair* boolToConsts = boolOrder->order->boolsToConstraints;
-	if( containsOrderPair(boolToConsts, boolOrder) ){
-		return getOrderPair(boolToConsts, boolOrder);
-	} else {
-		Edge constraint = getNewVarSATEncoder(This); 
-		putOrderPair(boolToConsts,boolOrder, constraint);
-		VectorBoolean* orderConstrs = &boolOrder->order->constraints;
-		uint size= getSizeVectorBoolean(orderConstrs);
-		for(uint i=0; i<size; i++){
-			ASSERT(GETBOOLEANTYPE( getVectorBoolean(orderConstrs, i)) == ORDERCONST );
-			BooleanOrder* tmp = (BooleanOrder*)getVectorBoolean(orderConstrs, i);
-			BooleanOrder* newBool;
-			Edge first, second;
-			if(tmp->second==boolOrder->first){
-				newBool = (BooleanOrder*)allocBooleanOrder(tmp->order,tmp->first,boolOrder->second);
-				first = encodeTotalOrderSATEncoder(This, tmp);
-				second = constraint;
-				
-			}else if (boolOrder->second == tmp->first){
-				newBool = (BooleanOrder*)allocBooleanOrder(tmp->order,boolOrder->first,tmp->second);
-				first = constraint;
-				second = encodeTotalOrderSATEncoder(This, tmp);
-			}else
-				continue;
-			Edge transConstr= encodeTotalOrderSATEncoder(This, newBool);
-			generateTransOrderConstraintSATEncoder(This, first, second, transConstr );
-		}
-		return constraint;
-	}
-*/	
 	return E_BOGUS;
 }
 
@@ -296,6 +258,9 @@ Edge encodeEnumTablePredicateSATEncoder(SATEncoder * This, BooleanPredicate * co
 		encodeElementSATEncoder(This, getArrayElement(inputs, i));
 	}
 	
+	//WARNING: THIS ASSUMES PREDICATE TABLE IS COMPLETE...SEEMS UNLIKELY TO BE SAFE IN MANY CASES...
+	//WONDER WHAT BEST WAY TO HANDLE THIS IS...
+	
 	uint size = getSizeVectorTableEntry(entries);
 	bool generateNegation = encType == ENUMERATEIMPLICATIONSNEGATE;
 	Edge constraints[size];
@@ -330,7 +295,7 @@ Edge encodeOperatorPredicateSATEncoder(SATEncoder * This, BooleanPredicate * con
 	return E_BOGUS;
 }
 
-Edge encodeEnumOperatorPredicateSATEncoder(SATEncoder * This, BooleanPredicate * constraint){
+Edge encodeEnumOperatorPredicateSATEncoder(SATEncoder * This, BooleanPredicate * constraint) {
 	PredicateOperator* predicate = (PredicateOperator*)constraint->predicate;
 	uint numDomains=getSizeArraySet(&predicate->domains);
 
@@ -425,80 +390,107 @@ Edge encodeTableElementFunctionSATEncoder(SATEncoder* encoder, ElementFunction*
 	return E_BOGUS;
 }
 
-Edge encodeOperatorElementFunctionSATEncoder(SATEncoder* encoder, ElementFunction* This){
-	ASSERT(GETFUNCTIONTYPE(This->function) == OPERATORFUNC);
-	ASSERT(getSizeArrayElement(&This->inputs)==2 );
-	Element* elem1 = getArrayElement(&This->inputs,0);
-	Element* elem2 = getArrayElement(&This->inputs,1);
-	encodeElementSATEncoder(encoder, elem1);
-	encodeElementSATEncoder(encoder , elem2);
+Edge encodeOperatorElementFunctionSATEncoder(SATEncoder* This, ElementFunction* func) {
+	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;
 	
-	ElementEncoding* elemEnc1 = getElementEncoding( getArrayElement(&This->inputs,0) );
-	ElementEncoding* elemEnc2 = getElementEncoding( getArrayElement(&This->inputs,1) );
-	Edge carray[elemEnc1->encArraySize*elemEnc2->encArraySize];
-	uint size=0;
-	Edge overFlowConstraint = ((BooleanVar*) This->overflowstatus)->var;
-	for(uint i=0; i<elemEnc1->encArraySize; i++){
-		if(isinUseElement(elemEnc1, i)){
-			for( uint j=0; j<elemEnc2->encArraySize; j++){
-				if(isinUseElement(elemEnc2, j)){
-					uint64_t result= applyFunctionOperator((FunctionOperator*)This->function,elemEnc1->encodingArray[i],
-						elemEnc2->encodingArray[j]);
-					bool isInRange = isInRangeFunction((FunctionOperator*)This->function, result);
-
-					//FIXME: instead of getElementValueConstraint, it might be useful to have another function
-					// that doesn't iterate over encodingArray and treats more efficient ...
-					Edge valConstrIn1 = getElementValueConstraint(encoder, elemEnc1->element, elemEnc1->encodingArray[i]);
-					Edge valConstrIn2 = getElementValueConstraint(encoder, elemEnc2->element, elemEnc2->encodingArray[j]);
-					Edge valConstrOut = getElementValueConstraint(encoder, (Element*) This, result);
-					if(edgeIsNull(valConstrOut))
-						continue; //FIXME:Should talk to brian about it!
-					Edge OpConstraint = constraintIMPLIES(encoder->cnf, constraintAND2(encoder->cnf, valConstrIn1, valConstrIn2), valConstrOut);
-					switch( ((FunctionOperator*)This->function)->overflowbehavior ){
-						case IGNORE:
-							if(isInRange){
-								carray[size++] = OpConstraint;
-							}
-							break;
-						case WRAPAROUND:
-							carray[size++] = OpConstraint;
-							break;
-						case FLAGFORCESOVERFLOW:
-							if(isInRange){
-								Edge const1 = constraintIMPLIES(encoder->cnf, constraintAND2(encoder->cnf, valConstrIn1, valConstrIn2), constraintNegate(overFlowConstraint));
-								carray[size++] = constraintAND2(encoder->cnf, const1, OpConstraint);
-							}
-							break;
-						case OVERFLOWSETSFLAG:
-							if(isInRange){
-								carray[size++] = OpConstraint;
-							} else{
-								carray[size++] = constraintIMPLIES(encoder->cnf, constraintAND2(encoder->cnf, valConstrIn1, valConstrIn2), overFlowConstraint);
-							}
-							break;
-						case FLAGIFFOVERFLOW:
-							if(isInRange){
-								Edge const1 = constraintIMPLIES(encoder->cnf, constraintAND2(encoder->cnf, valConstrIn1, valConstrIn2), constraintNegate(overFlowConstraint));
-								carray[size++] = constraintAND2(encoder->cnf, const1, OpConstraint);
-							} else {
-								carray[size++] = constraintIMPLIES(encoder->cnf, constraintAND2(encoder->cnf, valConstrIn1, valConstrIn2), overFlowConstraint);
-							}
-							break;
-						case NOOVERFLOW:
-							if(!isInRange){
-								ASSERT(0);
-							}
-							carray[size++] = OpConstraint;
-							break;
-						default:
-							ASSERT(0);
-					}
-					
+	bool notfinished=true;
+	while(notfinished) {
+		Edge carray[numDomains+2];
+
+		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=constraintAND(This->cnf, numDomains+1, carray);
+				break;
+			}
+			case FLAGFORCESOVERFLOW: {
+				carray[numDomains+1]=constraintNegate(overFlowConstraint);
+				clause=constraintAND(This->cnf, numDomains+2, carray);
+				break;
+			}
+			case OVERFLOWSETSFLAG: {
+				if (isInRange) {
+					clause=constraintAND(This->cnf, numDomains+1, carray);
+				} else {
+					carray[numDomains+1]=overFlowConstraint;
+					clause=constraintAND(This->cnf, numDomains+1, carray);
+				}
+				break;
+			}
+			case FLAGIFFOVERFLOW: {
+				if (isInRange) {
+				carray[numDomains+1]=constraintNegate(overFlowConstraint);
+					clause=constraintAND(This->cnf, numDomains+2, carray);
+				} else {
+					carray[numDomains+1]=overFlowConstraint;
+					clause=constraintAND(This->cnf, numDomains+1, carray);
 				}
+				break;
+			}
+			default:
+				ASSERT(0);
+			}
+			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);
 			}
 		}
 	}
-	return constraintAND(encoder->cnf, size, carray); 
+
+	Edge cor=constraintOR(This->cnf, getSizeVectorEdge(clauses), exposeArrayEdge(clauses));
+	deleteVectorEdge(clauses);
+	return cor;
 }
 
 Edge encodeEnumTableElemFunctionSATEncoder(SATEncoder* encoder, ElementFunction* This){
-- 
2.34.1