X-Git-Url: http://plrg.eecs.uci.edu/git/?p=satune.git;a=blobdiff_plain;f=src%2FBackend%2Fsattranslator.c;h=ca0fdaeccda4aeb69dcc1c5bfaa2f43b92832304;hp=7736f941a0acb29fdb53834fefe609d9174aa02d;hb=4221735881b9d1cd53ef410d9448efd2d12a51ad;hpb=c12192d653bb50ff7890aa395af19f34b85cde2b

diff --git a/src/Backend/sattranslator.c b/src/Backend/sattranslator.c
index 7736f94..ca0fdae 100644
--- a/src/Backend/sattranslator.c
+++ b/src/Backend/sattranslator.c
@@ -6,49 +6,49 @@
 #include "order.h"
 #include "orderpair.h"
 
-uint64_t getElementValueBinaryIndexSATTranslator(CSolver* This, ElementEncoding* elemEnc){
-	uint index=0;
-	for(int i=elemEnc->numVars-1;i>=0;i--) {
-		index=index<<1;
+uint64_t getElementValueBinaryIndexSATTranslator(CSolver *This, ElementEncoding *elemEnc) {
+	uint index = 0;
+	for (int i = elemEnc->numVars - 1; i >= 0; i--) {
+		index = index << 1;
 		if (getValueSolver(This->satEncoder->cnf->solver, getEdgeVar( elemEnc->variables[i] )))
 			index |= 1;
 	}
 	model_print("index:%u\tencArraySize:%u\tisInUseElement:%u\n", index, elemEnc->encArraySize, isinUseElement(elemEnc, index));
-	ASSERT(elemEnc->encArraySize >index && isinUseElement(elemEnc, index));
+	ASSERT(elemEnc->encArraySize > index && isinUseElement(elemEnc, index));
 	return elemEnc->encodingArray[index];
 }
 
-uint64_t getElementValueBinaryValueSATTranslator(CSolver* This, ElementEncoding* elemEnc){
-	uint64_t value=0;
-	for(int i=elemEnc->numVars-1;i>=0;i--) {
-		value=value<<1;
+uint64_t getElementValueBinaryValueSATTranslator(CSolver *This, ElementEncoding *elemEnc) {
+	uint64_t value = 0;
+	for (int i = elemEnc->numVars - 1; i >= 0; i--) {
+		value = value << 1;
 		if (getValueSolver(This->satEncoder->cnf->solver, getEdgeVar( elemEnc->variables[i] )) )
 			value |= 1;
 	}
 	if (elemEnc->isBinaryValSigned &&
-			This->satEncoder->cnf->solver->solution[ getEdgeVar( elemEnc->variables[elemEnc->numVars-1])]) {
+			This->satEncoder->cnf->solver->solution[ getEdgeVar( elemEnc->variables[elemEnc->numVars - 1])]) {
 		//Do sign extension of negative number
-		uint64_t highbits=0xffffffffffffffff - ((1 << (elemEnc->numVars)) - 1);
-		value+=highbits;
+		uint64_t highbits = 0xffffffffffffffff - ((1 << (elemEnc->numVars)) - 1);
+		value += highbits;
 	}
-	value+=elemEnc->offset;
+	value += elemEnc->offset;
 	return value;
 }
 
-uint64_t getElementValueOneHotSATTranslator(CSolver* This, ElementEncoding* elemEnc){
-	uint index=0;
-	for(uint i=0; i< elemEnc->numVars; i++) {
+uint64_t getElementValueOneHotSATTranslator(CSolver *This, ElementEncoding *elemEnc) {
+	uint index = 0;
+	for (uint i = 0; i < elemEnc->numVars; i++) {
 		if (getValueSolver(This->satEncoder->cnf->solver, getEdgeVar( elemEnc->variables[i] )))
 			index = i;
 	}
-	ASSERT(elemEnc->encArraySize >index && isinUseElement(elemEnc, index));
+	ASSERT(elemEnc->encArraySize > index && isinUseElement(elemEnc, index));
 	return elemEnc->encodingArray[index];
 }
 
-uint64_t getElementValueUnarySATTranslator(CSolver* This, ElementEncoding* elemEnc){
+uint64_t getElementValueUnarySATTranslator(CSolver *This, ElementEncoding *elemEnc) {
 	uint i;
-	for(i=0;i<elemEnc->numVars;i++) {
-		if (! getValueSolver(This->satEncoder->cnf->solver, getEdgeVar( elemEnc->variables[i] )) ) {
+	for (i = 0; i < elemEnc->numVars; i++) {
+		if (!getValueSolver(This->satEncoder->cnf->solver, getEdgeVar( elemEnc->variables[i] )) ) {
 			break;
 		}
 	}
@@ -56,41 +56,41 @@ uint64_t getElementValueUnarySATTranslator(CSolver* This, ElementEncoding* elemE
 	return elemEnc->encodingArray[i];
 }
 
-uint64_t getElementValueSATTranslator(CSolver* This, Element* element){
-	ElementEncoding* elemEnc = getElementEncoding(element);
-	if(elemEnc->numVars == 0)	//case when the set has only one item
+uint64_t getElementValueSATTranslator(CSolver *This, Element *element) {
+	ElementEncoding *elemEnc = getElementEncoding(element);
+	if (elemEnc->numVars == 0)//case when the set has only one item
 		return getSetElement(getElementSet(element), 0);
-	switch(elemEnc->type){
-		case ONEHOT:
-			return getElementValueOneHotSATTranslator(This, elemEnc);
-		case UNARY:
-			return getElementValueUnarySATTranslator(This, elemEnc);
-		case BINARYINDEX:
-			return getElementValueBinaryIndexSATTranslator(This, elemEnc);
-		case ONEHOTBINARY:
-			ASSERT(0);
-			break;
-		case BINARYVAL:
-			ASSERT(0);
-			break;
-		default:
-			ASSERT(0);
-			break;
+	switch (elemEnc->type) {
+	case ONEHOT:
+		return getElementValueOneHotSATTranslator(This, elemEnc);
+	case UNARY:
+		return getElementValueUnarySATTranslator(This, elemEnc);
+	case BINARYINDEX:
+		return getElementValueBinaryIndexSATTranslator(This, elemEnc);
+	case ONEHOTBINARY:
+		ASSERT(0);
+		break;
+	case BINARYVAL:
+		ASSERT(0);
+		break;
+	default:
+		ASSERT(0);
+		break;
 	}
 	return -1;
 }
 
-bool getBooleanVariableValueSATTranslator( CSolver* This , Boolean* boolean){
-	int index = getEdgeVar( ((BooleanVar*) boolean)->var );
+bool getBooleanVariableValueSATTranslator( CSolver *This, Boolean *boolean) {
+	int index = getEdgeVar( ((BooleanVar *) boolean)->var );
 	return getValueSolver(This->satEncoder->cnf->solver, index);
 }
 
-HappenedBefore getOrderConstraintValueSATTranslator(CSolver* This, Order * order, uint64_t first, uint64_t second){
-	ASSERT(order->orderPairTable!= NULL);
-	OrderPair pair={first, second, E_NULL};
-	Edge var = getOrderConstraint(order->orderPairTable, &pair); 
-	if(edgeIsNull(var))
+HappenedBefore getOrderConstraintValueSATTranslator(CSolver *This, Order *order, uint64_t first, uint64_t second) {
+	ASSERT(order->orderPairTable != NULL);
+	OrderPair pair = {first, second, E_NULL};
+	Edge var = getOrderConstraint(order->orderPairTable, &pair);
+	if (edgeIsNull(var))
 		return UNORDERED;
-	return getValueCNF(This->satEncoder->cnf, var)? FIRST: SECOND;
+	return getValueCNF(This->satEncoder->cnf, var) ? FIRST : SECOND;
 }