X-Git-Url: http://demsky.eecs.uci.edu/git/?a=blobdiff_plain;f=src%2Fcsolver.cc;fp=src%2Fcsolver.cc;h=448fb9a7304e6b38a4b891883d151ff805d6a5d2;hb=3c33c8ed7c4600da543b2a82bcffd5aca86f0eb9;hp=17e237888caa78445af6b5cb91b1b9c4ebcfcd39;hpb=8ae6061f7eae5614e9f8bf1ccd9ad80bef9cd768;p=satune.git

diff --git a/src/csolver.cc b/src/csolver.cc
index 17e2378..448fb9a 100644
--- a/src/csolver.cc
+++ b/src/csolver.cc
@@ -409,28 +409,30 @@ BooleanEdge CSolver::rewriteLogicalOperation(LogicOp op, BooleanEdge *array, uin
 	return applyLogicalOperation(op, newarray, asize);
 }
 
-BooleanEdge CSolver::applyExactlyOneConstraint (BooleanEdge *array, uint asize) {
-	BooleanEdge newarray[asize + 1];
-
-	newarray[asize] = applyLogicalOperation(SATC_OR, array, asize);
-	for (uint i = 0; i < asize; i++) {
-		BooleanEdge oprand1 = array[i];
-		BooleanEdge carray [asize - 1];
-		uint index = 0;
-		for ( uint j = 0; j < asize; j++) {
-			if (i != j) {
-				BooleanEdge oprand2 = applyLogicalOperation(SATC_NOT, array[j]);
-				carray[index++] = applyLogicalOperation(SATC_IMPLIES, oprand1, oprand2);
-			}
+BooleanEdge CSolver::applyAtMostOneConstraint (BooleanEdge *array, uint asize) {
+	if(asize == 0 || asize == 1){
+		return getBooleanTrue();
+	}
+	BooleanEdge newarray[asize*(asize-1)];
+	uint newsize = 0;
+	for (uint i = 0; i < asize -1; i++) {
+		for(uint j = i +1; j < asize; j++){
+			BooleanEdge oprand1 = array[i];
+			BooleanEdge oprand2 = applyLogicalOperation(SATC_NOT, array[j]);
+			newarray[newsize++] = applyLogicalOperation(SATC_IMPLIES, oprand1, oprand2);
 		}
-		ASSERT(index == asize - 1);
-		newarray[i] = applyLogicalOperation(SATC_AND, carray, asize - 1);
 	}
-	return applyLogicalOperation(SATC_AND, newarray, asize + 1);
+	return applyLogicalOperation(SATC_AND, newarray, newsize);
+}
+
+BooleanEdge CSolver::applyExactlyOneConstraint (BooleanEdge *array, uint asize) {
+	BooleanEdge atleastOne = applyLogicalOperation(SATC_OR, array, asize);
+	BooleanEdge atmostOne = applyAtMostOneConstraint (array, asize);
+	return applyLogicalOperation(SATC_AND, atleastOne, atmostOne);
 }
 
 BooleanEdge CSolver::applyLogicalOperation(LogicOp op, BooleanEdge *array, uint asize) {
-	if (!useInterpreter()) {
+	if (!useInterpreter() && !optimizationsOff) {
 		BooleanEdge newarray[asize];
 		switch (op) {
 		case SATC_NOT: {
@@ -530,7 +532,7 @@ BooleanEdge CSolver::orderConstraint(Order *order, uint64_t first, uint64_t seco
 		}
 	}
 	Boolean *constraint = new BooleanOrder(order, first, second);
-	if (!useInterpreter() ) {
+	if (!useInterpreter() && !optimizationsOff ) {
 		Boolean *b = boolMap.get(constraint);
 
 		if (b == NULL) {