From 2f171b5db8479462cc953b2663bdaa26c2b3b115 Mon Sep 17 00:00:00 2001
From: Hamed <hamed.gorjiara@gmail.com>
Date: Mon, 3 Jul 2017 14:43:47 -0700
Subject: [PATCH] Adding predicateOperator (equality operation ...)

---
 src/AST/predicate.c      | 25 +++++++++++++++++++++++++
 src/AST/predicate.h      |  2 ++
 src/Backend/satencoder.c | 30 ++++++++++++++++++++++++++----
 src/Backend/satencoder.h |  1 +
 4 files changed, 54 insertions(+), 4 deletions(-)

diff --git a/src/AST/predicate.c b/src/AST/predicate.c
index ebb3c14..116f152 100644
--- a/src/AST/predicate.c
+++ b/src/AST/predicate.c
@@ -1,4 +1,6 @@
 #include "predicate.h"
+#include "boolean.h"
+#include "set.h"
 
 Predicate* allocPredicateOperator(CompOp op, Set ** domain, uint numDomain){
 	PredicateOperator* predicate = ourmalloc(sizeof(PredicateOperator));
@@ -16,6 +18,29 @@ Predicate* allocPredicateTable(Table* table, UndefinedBehavior undefBehavior){
 	return &predicate->base;
 }
 
+void getEqualitySetIntersection(PredicateOperator* predicate, uint* size, uint64_t* result){
+	ASSERT( predicate->op == EQUALS);
+	//make sure equality has 2 operands
+	ASSERT(getSizeArraySet( &predicate->domains) == 2);
+	*size=0;
+	VectorInt* mems1 = getArraySet(&predicate->domains, 0)->members; 
+	uint size1 = getSizeVectorInt(mems1);
+	VectorInt* mems2 = getArraySet(&predicate->domains, 1)->members;
+	uint size2 = getSizeVectorInt(mems2);
+	//FIXME:This isn't efficient, if we a hashset datastructure for Set, we
+	// can reduce it to O(n), but for now .... HG
+	for(uint i=0; i<size1; i++){
+		uint64_t tmp= getVectorInt(mems1, i);
+		for(uint j=0; j<size2; j++){
+			if(tmp == getVectorInt(mems2, j)){
+				result[(*size)++]=tmp;
+				break;
+			}
+		}
+	}
+	
+}
+
 void deletePredicate(Predicate* predicate){
 	switch(GETPREDICATETYPE(predicate)) {
 	case OPERATORPRED: {
diff --git a/src/AST/predicate.h b/src/AST/predicate.h
index 13e5295..22f33d0 100644
--- a/src/AST/predicate.h
+++ b/src/AST/predicate.h
@@ -26,5 +26,7 @@ struct PredicateTable {
 
 Predicate* allocPredicateOperator(CompOp op, Set ** domain, uint numDomain);
 Predicate* allocPredicateTable(Table* table, UndefinedBehavior undefBehavior);
+// size and result will be modified by this function!
+void getEqualitySetIntersection(PredicateOperator* predicate, uint* size, uint64_t* result);
 void deletePredicate(Predicate* predicate);
 #endif
diff --git a/src/Backend/satencoder.c b/src/Backend/satencoder.c
index fa124a6..dc557b5 100644
--- a/src/Backend/satencoder.c
+++ b/src/Backend/satencoder.c
@@ -282,7 +282,7 @@ Constraint * encodePartialOrderSATEncoder(SATEncoder *This, BooleanOrder * const
 }
 
 Constraint * encodePredicateSATEncoder(SATEncoder * This, BooleanPredicate * constraint) {
-	switch(GETPREDICATETYPE(constraint) ){
+	switch(GETPREDICATETYPE(constraint->predicate) ){
 		case TABLEPRED:
 			return encodeTablePredicateSATEncoder(This, constraint);
 		case OPERATORPRED:
@@ -311,7 +311,7 @@ Constraint * encodeEnumTablePredicateSATEncoder(SATEncoder * This, BooleanPredic
 	VectorTableEntry* entries = &(((PredicateTable*)constraint->predicate)->table->entries);
 	FunctionEncodingType encType = constraint->encoding.type;
 	uint size = getSizeVectorTableEntry(entries);
-	Constraint* constraints[size]; //FIXME: should add a space for the case that didn't match any entries
+	Constraint* constraints[size];
 	for(uint i=0; i<size; i++){
 		TableEntry* entry = getVectorTableEntry(entries, i);
 		if(encType==ENUMERATEIMPLICATIONS && entry->output!= true)
@@ -323,19 +323,21 @@ Constraint * encodeEnumTablePredicateSATEncoder(SATEncoder * This, BooleanPredic
 		Constraint* carray[inputNum];
 		Element* el = getArrayElement(inputs, i);
 		for(uint j=0; j<inputNum; j++){
-			carray[inputNum] = getElementValueConstraint(el, entry->inputs[j]);
+			carray[j] = getElementValueConstraint(el, entry->inputs[j]);
 		}
 		constraints[i]=allocArrayConstraint(AND, inputNum, carray);
 	}
 	Constraint* result= allocArrayConstraint(OR, size, constraints);
+	//FIXME: if it didn't match with any entry
 	return encType==ENUMERATEIMPLICATIONS? result: negateConstraint(result);
 }
 
 Constraint * encodeOperatorPredicateSATEncoder(SATEncoder * This, BooleanPredicate * constraint){
 	switch(constraint->encoding.type){
 		case ENUMERATEIMPLICATIONS:
-			break;
+			return encodeEnumOperatorPredicateSATEncoder(This, constraint);
 		case CIRCUIT:
+			ASSERT(0);
 			break;
 		default:
 			ASSERT(0);
@@ -343,6 +345,26 @@ Constraint * encodeOperatorPredicateSATEncoder(SATEncoder * This, BooleanPredica
 	return NULL;
 }
 
+Constraint * encodeEnumOperatorPredicateSATEncoder(SATEncoder * This, BooleanPredicate * constraint){
+	ASSERT(GETPREDICATETYPE(constraint)==OPERATORPRED);
+	PredicateOperator* predicate = (PredicateOperator*)constraint->predicate;
+	ASSERT(predicate->op == EQUALS); //For now, we just only support equals
+	//getting maximum size of in common elements between two sets!
+	uint size=getSizeVectorInt( getArraySet( &predicate->domains, 0)->members);
+	uint64_t commonElements [size];
+	getEqualitySetIntersection(predicate, &size, commonElements);
+	Constraint*  carray[size];
+	Element* elem1 = getArrayElement( &constraint->inputs, 0);
+	Element* elem2 = getArrayElement( &constraint->inputs, 1);
+	for(uint i=0; i<size; i++){
+		
+		carray[i] =  allocConstraint(AND, getElementValueConstraint(elem1, commonElements[i]),
+			getElementValueConstraint(elem2, commonElements[i]) );
+	}
+	//FIXME: the case when there is no intersection ....
+	return allocArrayConstraint(OR, size, carray);
+}
+
 Constraint* encodeFunctionElementSATEncoder(SATEncoder* encoder, ElementFunction *This){
 	switch(GETFUNCTIONTYPE(This->function)){
 		case TABLEFUNC:
diff --git a/src/Backend/satencoder.h b/src/Backend/satencoder.h
index 46419a4..6963fee 100644
--- a/src/Backend/satencoder.h
+++ b/src/Backend/satencoder.h
@@ -27,6 +27,7 @@ Constraint * encodePredicateSATEncoder(SATEncoder * This, BooleanPredicate * con
 Constraint * encodeTablePredicateSATEncoder(SATEncoder * This, BooleanPredicate * constraint);
 Constraint * encodeEnumTablePredicateSATEncoder(SATEncoder * This, BooleanPredicate * constraint);
 Constraint * encodeOperatorPredicateSATEncoder(SATEncoder * This, BooleanPredicate * constraint);
+Constraint * encodeEnumOperatorPredicateSATEncoder(SATEncoder * This, BooleanPredicate * constraint);
 
 Constraint * getElementValueBinaryIndexConstraint(Element* This, uint64_t value);
 Constraint * getElementValueConstraint(Element* This, uint64_t value);
-- 
2.34.1