X-Git-Url: http://demsky.eecs.uci.edu/git/?a=blobdiff_plain;f=src%2Fcsolver.cc;h=a02227e0b82ddedcb52c063ae99bb3611fa8fa2d;hb=081e954fa3566ad9a2522ca45bef8e29472d2a72;hp=81aeb8e84e12a333b4c6207a0454a830e3c54e8a;hpb=0097f3d8e023e8ac1158436fe9aac33f93681f8d;p=satune.git

diff --git a/src/csolver.cc b/src/csolver.cc
index 81aeb8e..a02227e 100644
--- a/src/csolver.cc
+++ b/src/csolver.cc
@@ -395,6 +395,26 @@ 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);
+			}
+		}
+		ASSERT(index == asize -1);
+		newarray[i] = applyLogicalOperation(SATC_AND, carray, asize-1);
+	}
+	return applyLogicalOperation(SATC_AND, newarray, asize+1);
+}
+
 BooleanEdge CSolver::applyLogicalOperation(LogicOp op, BooleanEdge *array, uint asize) {
 	if (!useInterpreter()) {
 		BooleanEdge newarray[asize];