Adding API for AtMostOneConstraint + bugfix for turning off the optimizations

diff --git a/src/ccsolver.cc b/src/ccsolver.cc
index aca46a59e37331ee87b20281aaee464fa5e7e532..a1dd75898acc356574fe5089097f35d52b1d3913 100644 (file)
--- a/src/ccsolver.cc
+++ b/src/ccsolver.cc
@@ -118,6 +118,14 @@ void *applyExactlyOneConstraint(void *solver, void **array, unsigned int asize)
        return CCSOLVER(solver)->applyExactlyOneConstraint( constr, (uint) asize).getRaw();
 }
 
+void *applyAtMostOneConstraint(void *solver, void **array, unsigned int asize) {
+       BooleanEdge constr [asize];
+       for (uint i = 0; i < asize; i++) {
+               constr[i] = BooleanEdge((Boolean *)array[i]);
+       }
+       return CCSOLVER(solver)->applyAtMostOneConstraint( constr, (uint) asize).getRaw();
+}
+
 void *applyLogicalOperationTwo(void *solver,unsigned int op, void *arg1, void *arg2) {
        return CCSOLVER(solver)->applyLogicalOperation((LogicOp) op, BooleanEdge((Boolean *) arg1), BooleanEdge((Boolean *) arg2)).getRaw();
 }

diff --git a/src/ccsolver.h b/src/ccsolver.h
index 8e708b833e407aa2a4aed5205fd501cfd0919fb7..638527c54f0d3370233bf6d556441c97357d94da 100644 (file)
--- a/src/ccsolver.h
+++ b/src/ccsolver.h
@@ -33,6 +33,7 @@ void *applyPredicateTable(void *solver,void *predicate, void **inputs, unsigned
 void *applyPredicate(void *solver,void *predicate, void **inputs, unsigned int numInputs);
 void *applyLogicalOperation(void *solver,unsigned int op, void **array, unsigned int asize);
 void *applyExactlyOneConstraint(void *solver,void **array, unsigned int asize);
+void *applyAtMostOneConstraint(void *solver,void **array, unsigned int asize);
 void *applyLogicalOperationTwo(void *solver,unsigned int op, void *arg1, void *arg2);
 void *applyLogicalOperationOne(void *solver,unsigned int op, void *arg);
 void addConstraint(void *solver,void *constraint);

diff --git a/src/csolver.cc b/src/csolver.cc
index 17e237888caa78445af6b5cb91b1b9c4ebcfcd39..448fb9a7304e6b38a4b891883d151ff805d6a5d2 100644 (file)
--- 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) {

diff --git a/src/csolver.h b/src/csolver.h
index eba7b3ccf47ffa7abb4dbae45e398591a8fd025c..5ef235d3d8ce9b26032380b30c4cea82c85bd0f2 100644 (file)
--- a/src/csolver.h
+++ b/src/csolver.h
@@ -103,6 +103,9 @@ public:
 
        /** This exactly one element of array can be true! (i.e. a1 + a2 + a3 + ... + an = 1)*/
        BooleanEdge applyExactlyOneConstraint (BooleanEdge *array, uint asize);
+       
+       /** This exactly one element of array can be true! (i.e. a1 => !a2 & !a3 & ... & !an)*/
+       BooleanEdge applyAtMostOneConstraint (BooleanEdge *array, uint asize);
 
        /** This function applies a logical operation to the Booleans in its input. */
 

diff --git a/src/pycsolver.py b/src/pycsolver.py
index a3e0f11b3c5ed981997a84b2a44b006a86f8f352..f08d164e5d5edbbf094793c20270ea4b2fb77c06 100644 (file)
--- a/src/pycsolver.py
+++ b/src/pycsolver.py
@@ -65,6 +65,10 @@ def loadCSolver():
        csolverlb.getElementRange.restype = c_void_p
        csolverlb.getBooleanVar.argtypes = [c_void_p, c_uint]
        csolverlb.getBooleanVar.restype = c_void_p
+       csolverlb.getBooleanTrue.argtypes = [c_void_p]
+       csolverlb.getBooleanTrue.restype = c_void_p
+       csolverlb.getBooleanFalse.argtypes = [c_void_p]
+       csolverlb.getBooleanFalse.restype = c_void_p
        csolverlb.createFunctionOperator.argtypes = [c_void_p, c_uint, c_void_p, c_uint]
        csolverlb.createFunctionOperator.restype = c_void_p
        csolverlb.createPredicateOperator.argtypes = [c_void_p, c_uint]
@@ -89,6 +93,8 @@ def loadCSolver():
        csolverlb.applyLogicalOperation.restype = c_void_p
        csolverlb.applyExactlyOneConstraint.argtypes = [c_void_p, c_void_p, c_uint]
        csolverlb.applyExactlyOneConstraint.restype = c_void_p
+       csolverlb.applyAtMostOneConstraint.argtypes = [c_void_p, c_void_p, c_uint]
+       csolverlb.applyAtMostOneConstraint.restype = c_void_p
        csolverlb.applyLogicalOperationTwo.argtypes = [c_void_p, c_uint, c_void_p, c_void_p]
        csolverlb.applyLogicalOperationTwo.restype = c_void_p
        csolverlb.applyLogicalOperationOne.argtypes = [c_void_p, c_uint, c_void_p]