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];