Adding API for AtMostOneConstraint + bugfix for turning off the optimizations
authorHamed Gorjiara <hgorjiar@uci.edu>
Thu, 31 Oct 2019 20:14:31 +0000 (13:14 -0700)
committerHamed Gorjiara <hgorjiar@uci.edu>
Thu, 31 Oct 2019 20:14:31 +0000 (13:14 -0700)
src/ccsolver.cc
src/ccsolver.h
src/csolver.cc
src/csolver.h
src/pycsolver.py

index aca46a5..a1dd758 100644 (file)
@@ -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();
 }
index 8e708b8..638527c 100644 (file)
@@ -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);
index 17e2378..448fb9a 100644 (file)
@@ -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) {
index eba7b3c..5ef235d 100644 (file)
@@ -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. */
 
index a3e0f11..f08d164 100644 (file)
@@ -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]