From 3c33c8ed7c4600da543b2a82bcffd5aca86f0eb9 Mon Sep 17 00:00:00 2001 From: Hamed Gorjiara Date: Thu, 31 Oct 2019 13:14:31 -0700 Subject: [PATCH] Adding API for AtMostOneConstraint + bugfix for turning off the optimizations --- src/ccsolver.cc | 8 ++++++++ src/ccsolver.h | 1 + src/csolver.cc | 38 ++++++++++++++++++++------------------ src/csolver.h | 3 +++ src/pycsolver.py | 6 ++++++ 5 files changed, 38 insertions(+), 18 deletions(-) diff --git a/src/ccsolver.cc b/src/ccsolver.cc index aca46a5..a1dd758 100644 --- 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 8e708b8..638527c 100644 --- 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 17e2378..448fb9a 100644 --- 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 eba7b3c..5ef235d 100644 --- 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 a3e0f11..f08d164 100644 --- 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] -- 2.34.1