Bug fixes for Java API + Exactly one constraints + Adding support for getting the...

[satune.git] / src / csolver.cc

diff --git a/src/csolver.cc b/src/csolver.cc
index 1dfe9eb8ec9cf012f9af880c672e62a9ff95c81b..a02227e0b82ddedcb52c063ae99bb3611fa8fa2d 100644 (file)
--- a/src/csolver.cc
+++ b/src/csolver.cc
@@ -264,7 +264,6 @@ Element *CSolver::getElementConst(VarType type, uint64_t value) {
 
 
 Element *CSolver::applyFunction(Function *function, Element **array, uint numArrays, BooleanEdge overflowstatus) {
-       ASSERT(numArrays == 2);
        Element *element = new ElementFunction(function,array,numArrays,overflowstatus);
        Element *e = elemMap.get(element);
        if (e == NULL) {
@@ -396,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];