X-Git-Url: http://plrg.eecs.uci.edu/git/?a=blobdiff_plain;f=src%2FBackend%2Fsatencoder.c;h=f5362b882160095f38babade394286bc6b79709d;hb=c216ff2cc756b03e9f4ed21839ac1fb43ba22895;hp=dc557b5ee40b7147744e22cc84dc54cebb10c144;hpb=eda32d99c1abb9415fb1b44dbf523de3436de41c;p=satune.git

diff --git a/src/Backend/satencoder.c b/src/Backend/satencoder.c
index dc557b5..f5362b8 100644
--- a/src/Backend/satencoder.c
+++ b/src/Backend/satencoder.c
@@ -10,97 +10,38 @@
 #include "table.h"
 #include "order.h"
 #include "predicate.h"
-#include "orderpair.h"
 #include "set.h"
+#include "satfuncopencoder.h"
 
-SATEncoder * allocSATEncoder() {
-	SATEncoder *This=ourmalloc(sizeof (SATEncoder));
-	This->varcount=1;
+//TODO: Should handle sharing of AST Nodes without recoding them a second time
+
+SATEncoder *allocSATEncoder(CSolver *solver) {
+	SATEncoder *This = ourmalloc(sizeof (SATEncoder));
+	This->solver = solver;
+	This->varcount = 1;
+	This->cnf = createCNF();
 	return This;
 }
 
 void deleteSATEncoder(SATEncoder *This) {
+	deleteCNF(This->cnf);
 	ourfree(This);
 }
 
-void initializeConstraintVars(CSolver* csolver, SATEncoder* This){
-	/** We really should not walk the free list to generate constraint
-			variables...walk the constraint tree instead.  Or even better
-			yet, just do this as you need to during the encodeAllSATEncoder
-			walk.  */
-
-//	FIXME!!!!(); // Make sure Hamed sees comment above
-
-	uint size = getSizeVectorElement(csolver->allElements);
-	for(uint i=0; i<size; i++){
-		Element* element = getVectorElement(csolver->allElements, i);
-		generateElementEncodingVariables(This,getElementEncoding(element));
+void encodeAllSATEncoder(CSolver *csolver, SATEncoder *This) {
+	HSIteratorBoolean *iterator=iteratorBoolean(csolver->constraints);
+	while(hasNextBoolean(iterator)) {
+		Boolean *constraint = nextBoolean(iterator);
+		model_print("Encoding All ...\n\n");
+		Edge c = encodeConstraintSATEncoder(This, constraint);
+		model_print("Returned Constraint in EncodingAll:\n");
+		addConstraintCNF(This->cnf, c);
 	}
+	deleteIterBoolean(iterator);
 }
 
-
-Constraint * getElementValueConstraint(Element* This, uint64_t value) {
-	switch(getElementEncoding(This)->type){
-		case ONEHOT:
-			ASSERT(0);
-			break;
-		case UNARY:
-			ASSERT(0);
-			break;
-		case BINARYINDEX:
-			ASSERT(0);
-			break;
-		case ONEHOTBINARY:
-			return getElementValueBinaryIndexConstraint(This, value);
-			break;
-		case BINARYVAL:
-			ASSERT(0);
-			break;
-		default:
-			ASSERT(0);
-			break;
-	}
-	return NULL;
-}
-Constraint * getElementValueBinaryIndexConstraint(Element* This, uint64_t value) {
-	ASTNodeType type = GETELEMENTTYPE(This);
-	ASSERT(type == ELEMSET || type == ELEMFUNCRETURN);
-	ElementEncoding* elemEnc = getElementEncoding(This);
-	for(uint i=0; i<elemEnc->encArraySize; i++){
-		if( isinUseElement(elemEnc, i) && elemEnc->encodingArray[i]==value){
-			return generateBinaryConstraint(elemEnc->numVars,
-				elemEnc->variables, i);
-		}
-	}
-	return NULL;
-}
-
-void encodeAllSATEncoder(CSolver *csolver, SATEncoder * This) {
-	VectorBoolean *constraints=csolver->constraints;
-	uint size=getSizeVectorBoolean(constraints);
-	for(uint i=0;i<size;i++) {
-		Boolean *constraint=getVectorBoolean(constraints, i);
-		encodeConstraintSATEncoder(This, constraint);
-	}
-	
-//	FIXME: Following line for element!
-//	size = getSizeVectorElement(csolver->allElements);
-//	for(uint i=0; i<size; i++){
-//		Element* element = getVectorElement(csolver->allElements, i);
-//		switch(GETELEMENTTYPE(element)){
-//			case ELEMFUNCRETURN: 
-//				encodeFunctionElementSATEncoder(This, (ElementFunction*) element);
-//				break;
-//			default:	
-//				continue;
-//				//ElementSets that aren't used in any constraints/functions
-//				//will be eliminated.
-//		}
-//	}
-}
-
-Constraint * encodeConstraintSATEncoder(SATEncoder *This, Boolean *constraint) {
-	switch(GETBOOLEANTYPE(constraint)) {
+Edge encodeConstraintSATEncoder(SATEncoder *This, Boolean *constraint) {
+	switch (GETBOOLEANTYPE(constraint)) {
 	case ORDERCONST:
 		return encodeOrderSATEncoder(This, (BooleanOrder *) constraint);
 	case BOOLEANVAR:
@@ -115,305 +56,111 @@ Constraint * encodeConstraintSATEncoder(SATEncoder *This, Boolean *constraint) {
 	}
 }
 
-void getArrayNewVarsSATEncoder(SATEncoder* encoder, uint num, Constraint **carray) {
-	for(uint i=0;i<num;i++)
-		carray[i]=getNewVarSATEncoder(encoder);
+void getArrayNewVarsSATEncoder(SATEncoder *encoder, uint num, Edge *carray) {
+	for (uint i = 0; i < num; i++)
+		carray[i] = getNewVarSATEncoder(encoder);
 }
 
-Constraint * getNewVarSATEncoder(SATEncoder *This) {
-	Constraint * var=allocVarConstraint(VAR, This->varcount);
-	Constraint * varneg=allocVarConstraint(NOTVAR, This->varcount++);
-	setNegConstraint(var, varneg);
-	setNegConstraint(varneg, var);
-	return var;
+Edge getNewVarSATEncoder(SATEncoder *This) {
+	return constraintNewVar(This->cnf);
 }
 
-Constraint * encodeVarSATEncoder(SATEncoder *This, BooleanVar * constraint) {
-	if (constraint->var == NULL) {
-		constraint->var=getNewVarSATEncoder(This);
+Edge encodeVarSATEncoder(SATEncoder *This, BooleanVar *constraint) {
+	if (edgeIsNull(constraint->var)) {
+		constraint->var = getNewVarSATEncoder(This);
 	}
 	return constraint->var;
 }
 
-Constraint * encodeLogicSATEncoder(SATEncoder *This, BooleanLogic * constraint) {
-	Constraint * array[getSizeArrayBoolean(&constraint->inputs)];
-	for(uint i=0;i<getSizeArrayBoolean(&constraint->inputs);i++)
-		array[i]=encodeConstraintSATEncoder(This, getArrayBoolean(&constraint->inputs, i));
+Edge encodeLogicSATEncoder(SATEncoder *This, BooleanLogic *constraint) {
+	Edge array[getSizeArrayBoolean(&constraint->inputs)];
+	for (uint i = 0; i < getSizeArrayBoolean(&constraint->inputs); i++)
+		array[i] = encodeConstraintSATEncoder(This, getArrayBoolean(&constraint->inputs, i));
 
-	switch(constraint->op) {
+	switch (constraint->op) {
 	case L_AND:
-		return allocArrayConstraint(AND, getSizeArrayBoolean(&constraint->inputs), array);
+		return constraintAND(This->cnf, getSizeArrayBoolean(&constraint->inputs), array);
 	case L_OR:
-		return allocArrayConstraint(OR, getSizeArrayBoolean(&constraint->inputs), array);
+		return constraintOR(This->cnf, getSizeArrayBoolean(&constraint->inputs), array);
 	case L_NOT:
-		ASSERT(constraint->numArray==1);
-		return negateConstraint(array[0]);
-	case L_XOR: {
-		ASSERT(constraint->numArray==2);
-		Constraint * nleft=negateConstraint(cloneConstraint(array[0]));
-		Constraint * nright=negateConstraint(cloneConstraint(array[1]));
-		return allocConstraint(OR,
-													 allocConstraint(AND, array[0], nright),
-													 allocConstraint(AND, nleft, array[1]));
-	}
+		ASSERT( getSizeArrayBoolean(&constraint->inputs) == 1);
+		return constraintNegate(array[0]);
+	case L_XOR:
+		ASSERT( getSizeArrayBoolean(&constraint->inputs) == 2);
+		return constraintXOR(This->cnf, array[0], array[1]);
 	case L_IMPLIES:
-		ASSERT(constraint->numArray==2);
-		return allocConstraint(IMPLIES, array[0], array[1]);
+		ASSERT( getSizeArrayBoolean( &constraint->inputs) == 2);
+		return constraintIMPLIES(This->cnf, array[0], array[1]);
 	default:
 		model_print("Unhandled case in encodeLogicSATEncoder %u", constraint->op);
 		exit(-1);
 	}
 }
 
-
-Constraint * encodeOrderSATEncoder(SATEncoder *This, BooleanOrder * constraint) {
-	switch( constraint->order->type){
-		case PARTIAL:
-			return encodePartialOrderSATEncoder(This, constraint);
-		case TOTAL:
-			return encodeTotalOrderSATEncoder(This, constraint);
-		default:
-			ASSERT(0);
-	}
-	return NULL;
-}
-
-
-Constraint * encodeTotalOrderSATEncoder(SATEncoder *This, BooleanOrder * boolOrder){
-	ASSERT(boolOrder->order->type == TOTAL);
-	HashTableBoolConst* boolToConsts = boolOrder->order->boolsToConstraints;
-	OrderPair* pair = allocOrderPair(boolOrder->first, boolOrder->second);
-	if( !containsBoolConst(boolToConsts, pair) ){
-		createAllTotalOrderConstraintsSATEncoder(This, boolOrder->order);
-	}
-	Constraint* constraint = getOrderConstraint(boolToConsts, pair);
-	deleteOrderPair(pair);
-	return constraint;
-}
-
-void createAllTotalOrderConstraintsSATEncoder(SATEncoder* This, Order* order){
-	ASSERT(order->type == TOTAL);
-	VectorInt* mems = order->set->members;
-	HashTableBoolConst* table = order->boolsToConstraints;
-	uint size = getSizeVectorInt(mems);
-	for(uint i=0; i<size; i++){
-		uint64_t valueI = getVectorInt(mems, i);
-		for(uint j=i+1; j<size;j++){
-			uint64_t valueJ = getVectorInt(mems, j);
-			OrderPair* pairIJ = allocOrderPair(valueI, valueJ);
-			ASSERT(!containsBoolConst(table, pairIJ));
-			Constraint* constIJ = getNewVarSATEncoder(This);
-			putBoolConst(table, pairIJ, constIJ);
-			for(uint k=j+1; k<size; k++){
-				uint64_t valueK = getVectorInt(mems, k);
-				OrderPair* pairJK = allocOrderPair(valueJ, valueK);
-				OrderPair* pairIK = allocOrderPair(valueI, valueK);
-				Constraint* constJK, *constIK;
-				if(!containsBoolConst(table, pairJK)){
-					constJK = getNewVarSATEncoder(This);
-					putBoolConst(table, pairJK, constJK);
-				}
-				if(!containsBoolConst(table, pairIK)){
-					constIK = getNewVarSATEncoder(This);
-					putBoolConst(table, pairIK, constIK);
-				}
-				generateTransOrderConstraintSATEncoder(This, constIJ, constJK, constIK); 
-			}
-		}
-	}
-}
-
-Constraint* getOrderConstraint(HashTableBoolConst *table, OrderPair *pair){
-	ASSERT(pair->first!= pair->second);
-	Constraint* constraint= getBoolConst(table, pair);
-	ASSERT(constraint!= NULL);
-	if(pair->first > pair->second)
-		return constraint;
-	else
-		return negateConstraint(constraint);
-}
-
-Constraint * generateTransOrderConstraintSATEncoder(SATEncoder *This, Constraint *constIJ,Constraint *constJK,Constraint *constIK){
-	//FIXME: first we should add the the constraint to the satsolver!
-	Constraint *carray[] = {constIJ, constJK, negateConstraint(constIK)};
-	Constraint * loop1= allocArrayConstraint(OR, 3, carray);
-	Constraint * carray2[] = {negateConstraint(constIJ), negateConstraint(constJK), constIK};
-	Constraint * loop2= allocArrayConstraint(OR, 3,carray2 );
-	return allocConstraint(AND, loop1, loop2);
-}
-
-Constraint * 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(boolOrder->order->type == PARTIAL);
-/*
-	HashTableBoolConst* boolToConsts = boolOrder->order->boolsToConstraints;
-	if( containsBoolConst(boolToConsts, boolOrder) ){
-		return getBoolConst(boolToConsts, boolOrder);
-	} else {
-		Constraint* constraint = getNewVarSATEncoder(This); 
-		putBoolConst(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;
-			Constraint* 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;
-			Constraint* transConstr= encodeTotalOrderSATEncoder(This, newBool);
-			generateTransOrderConstraintSATEncoder(This, first, second, transConstr );
-		}
-		return constraint;
-	}
-*/	
-	return NULL;
-}
-
-Constraint * encodePredicateSATEncoder(SATEncoder * This, BooleanPredicate * constraint) {
-	switch(GETPREDICATETYPE(constraint->predicate) ){
-		case TABLEPRED:
-			return encodeTablePredicateSATEncoder(This, constraint);
-		case OPERATORPRED:
-			return encodeOperatorPredicateSATEncoder(This, constraint);
-		default:
-			ASSERT(0);
-	}
-	return NULL;
-}
-
-Constraint * encodeTablePredicateSATEncoder(SATEncoder * This, BooleanPredicate * constraint){
-	switch(constraint->encoding.type){
-		case ENUMERATEIMPLICATIONS:
-		case ENUMERATEIMPLICATIONSNEGATE:
-			return encodeEnumTablePredicateSATEncoder(This, constraint);
-		case CIRCUIT:
-			ASSERT(0);
-			break;
-		default:
-			ASSERT(0);
-	}
-	return NULL;
-}
-
-Constraint * encodeEnumTablePredicateSATEncoder(SATEncoder * This, BooleanPredicate * constraint){
-	VectorTableEntry* entries = &(((PredicateTable*)constraint->predicate)->table->entries);
-	FunctionEncodingType encType = constraint->encoding.type;
-	uint size = getSizeVectorTableEntry(entries);
-	Constraint* constraints[size];
-	for(uint i=0; i<size; i++){
-		TableEntry* entry = getVectorTableEntry(entries, i);
-		if(encType==ENUMERATEIMPLICATIONS && entry->output!= true)
-			continue;
-		else if(encType==ENUMERATEIMPLICATIONSNEGATE && entry->output !=false)
-			continue;
-		ArrayElement* inputs = &constraint->inputs;
-		uint inputNum =getSizeArrayElement(inputs);
-		Constraint* carray[inputNum];
-		Element* el = getArrayElement(inputs, i);
-		for(uint j=0; j<inputNum; 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:
-			return encodeEnumOperatorPredicateSATEncoder(This, constraint);
-		case CIRCUIT:
-			ASSERT(0);
-			break;
-		default:
-			ASSERT(0);
-	}
-	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]) );
+Edge encodePredicateSATEncoder(SATEncoder *This, BooleanPredicate *constraint) {
+	switch (GETPREDICATETYPE(constraint->predicate) ) {
+	case TABLEPRED:
+		return encodeTablePredicateSATEncoder(This, constraint);
+	case OPERATORPRED:
+		return encodeOperatorPredicateSATEncoder(This, constraint);
+	default:
+		ASSERT(0);
 	}
-	//FIXME: the case when there is no intersection ....
-	return allocArrayConstraint(OR, size, carray);
+	return E_BOGUS;
 }
 
-Constraint* encodeFunctionElementSATEncoder(SATEncoder* encoder, ElementFunction *This){
-	switch(GETFUNCTIONTYPE(This->function)){
-		case TABLEFUNC:
-			return encodeTableElementFunctionSATEncoder(encoder, This);
-		case OPERATORFUNC:
-			return encodeOperatorElementFunctionSATEncoder(encoder, This);
-		default:
-			ASSERT(0);
+Edge encodeTablePredicateSATEncoder(SATEncoder *This, BooleanPredicate *constraint) {
+	switch (constraint->encoding.type) {
+	case ENUMERATEIMPLICATIONS:
+	case ENUMERATEIMPLICATIONSNEGATE:
+		return encodeEnumTablePredicateSATEncoder(This, constraint);
+	case CIRCUIT:
+		ASSERT(0);
+		break;
+	default:
+		ASSERT(0);
+	}
+	return E_BOGUS;
+}
+
+void encodeElementSATEncoder(SATEncoder *encoder, Element *This) {
+	switch ( GETELEMENTTYPE(This) ) {
+	case ELEMFUNCRETURN:
+		generateElementEncoding(encoder, This);
+		encodeElementFunctionSATEncoder(encoder, (ElementFunction *) This);
+		break;
+	case ELEMSET:
+		generateElementEncoding(encoder, This);
+		return;
+	case ELEMCONST:
+		return;
+	default:
+		ASSERT(0);
 	}
-	return NULL;
 }
 
-Constraint* encodeTableElementFunctionSATEncoder(SATEncoder* encoder, ElementFunction* This){
-	switch(getElementFunctionEncoding(This)->type){
-		case ENUMERATEIMPLICATIONS:
-			return encodeEnumTableElemFunctionSATEncoder(encoder, This);
-			break;
-		case CIRCUIT:
-			ASSERT(0);
-			break;
-		default:
-			ASSERT(0);
+void encodeElementFunctionSATEncoder(SATEncoder *encoder, ElementFunction *This) {
+	switch (GETFUNCTIONTYPE(This->function)) {
+	case TABLEFUNC:
+		encodeTableElementFunctionSATEncoder(encoder, This);
+		break;
+	case OPERATORFUNC:
+		encodeOperatorElementFunctionSATEncoder(encoder, This);
+		break;
+	default:
+		ASSERT(0);
 	}
-	return NULL;
 }
 
-Constraint* encodeOperatorElementFunctionSATEncoder(SATEncoder* encoder, ElementFunction* This){
-	//FIXME: for now it just adds/substracts inputs exhustively
-	return NULL;
-}
-
-Constraint* encodeEnumTableElemFunctionSATEncoder(SATEncoder* encoder, ElementFunction* This){
-	ASSERT(GETFUNCTIONTYPE(This->function)==TABLEFUNC);
-	ArrayElement* elements= &This->inputs;
-	Table* table = ((FunctionTable*) (This->function))->table;
-	uint size = getSizeVectorTableEntry(&table->entries);
-	Constraint* constraints[size]; //FIXME: should add a space for the case that didn't match any entries
-	for(uint i=0; i<size; i++){
-		TableEntry* entry = getVectorTableEntry(&table->entries, i);
-		uint inputNum =getSizeArrayElement(elements);
-		Element* el= getArrayElement(elements, i);
-		Constraint* carray[inputNum];
-		for(uint j=0; j<inputNum; j++){
-			carray[inputNum] = getElementValueConstraint(el, entry->inputs[j]);
-		}
-		Constraint* row= allocConstraint(IMPLIES, allocArrayConstraint(AND, inputNum, carray),
-			getElementValueBinaryIndexConstraint((Element*)This, entry->output));
-		constraints[i]=row;
+void encodeTableElementFunctionSATEncoder(SATEncoder *encoder, ElementFunction *This) {
+	switch (getElementFunctionEncoding(This)->type) {
+	case ENUMERATEIMPLICATIONS:
+		encodeEnumTableElemFunctionSATEncoder(encoder, This);
+		break;
+	case CIRCUIT:
+		ASSERT(0);
+		break;
+	default:
+		ASSERT(0);
 	}
-	Constraint* result = allocArrayConstraint(OR, size, constraints);
-	return result;
 }