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

diff --git a/src/Backend/inc_solver.cc b/src/Backend/inc_solver.cc
index 2d6b8a48d993aa6ad9164e2060b413c50533e0b6..72d34083dcd4b096b32aee4b51816a361f708600 100644 (file)
--- a/src/Backend/inc_solver.cc
+++ b/src/Backend/inc_solver.cc
@@ -102,6 +102,16 @@ int getSolution(IncrementalSolver *This) {
                }
                readSolver(This, &This->solution[1], numVars * sizeof(int));
                This->solutionsize = numVars;
+       } else { //Reading unsat explanation
+               int numVars = readIntSolver(This);
+               if (numVars > This->solutionsize) {
+                       if (This->solution != NULL)
+                               ourfree(This->solution);
+                       This->solution = (int *) ourmalloc((numVars + 1) * sizeof(int));
+                       This->solution[0] = 0;
+               }
+               readSolver(This, &This->solution[1], numVars * sizeof(int));
+               This->solutionsize = numVars;
        }
        return result;
 }

diff --git a/src/ccsolver.cc b/src/ccsolver.cc
index d77352288e709f45aaed97f217891dfbeabad31a..fa2e3426211b50e34f786e506e865307d3aa2d04 100644 (file)
--- a/src/ccsolver.cc
+++ b/src/ccsolver.cc
@@ -102,8 +102,20 @@ void *applyPredicate(void *solver,void *predicate, void **inputs, unsigned int n
        return CCSOLVER(solver)->applyPredicate((Predicate *)predicate, (Element **)inputs, (uint) numInputs).getRaw();
 }
 
-void *applyLogicalOperation(void *solver,unsigned int op, void *array, unsigned int asize) {
-       return CCSOLVER(solver)->applyLogicalOperation((LogicOp) op, (BooleanEdge *)array, (uint) asize).getRaw();
+void *applyLogicalOperation(void *solver,unsigned int op, void **array, unsigned int asize) {
+       BooleanEdge constr [asize];
+       for(uint i=0; i< asize; i++){
+               constr[i] = BooleanEdge((Boolean*)array[i]);
+       }
+       return CCSOLVER(solver)->applyLogicalOperation((LogicOp) op, constr, (uint) asize).getRaw();
+}
+
+void *applyExactlyOneConstraint(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)->applyExactlyOneConstraint( constr, (uint) asize).getRaw();
 }
 
 void *applyLogicalOperationTwo(void *solver,unsigned int op, void *arg1, void *arg2) {

diff --git a/src/ccsolver.h b/src/ccsolver.h
index c668fbccbb1249c6de87c1a2411a9dc85f5eaded..86d5a46374541cf88c6f1bd77fc643aedde6e826 100644 (file)
--- a/src/ccsolver.h
+++ b/src/ccsolver.h
@@ -31,7 +31,8 @@ void *completeTable(void *solver,void *table, unsigned int behavior);
 void *applyFunction(void *solver,void *function, void **array, unsigned int numArrays, void *overflowstatus);
 void *applyPredicateTable(void *solver,void *predicate, void **inputs, unsigned int numInputs, void *undefinedStatus);
 void *applyPredicate(void *solver,void *predicate, void **inputs, unsigned int numInputs);
-void *applyLogicalOperation(void *solver,unsigned int op, void *array, unsigned int asize);
+void *applyLogicalOperation(void *solver,unsigned int op, void **array, unsigned int asize);
+void *applyExactlyOneConstraint(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 81aeb8e84e12a333b4c6207a0454a830e3c54e8a..a02227e0b82ddedcb52c063ae99bb3611fa8fa2d 100644 (file)
--- a/src/csolver.cc
+++ b/src/csolver.cc
@@ -395,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];

diff --git a/src/csolver.h b/src/csolver.h
index b99cf804b5e416aa3f8c7fee6896ec1120b72801..0ff566e53cee07fd935e35a58a60d63d668943ea 100644 (file)
--- a/src/csolver.h
+++ b/src/csolver.h
@@ -101,8 +101,11 @@ public:
 
        BooleanEdge applyPredicate(Predicate *predicate, Element **inputs, uint numInputs);
 
+       /** This exactly one element of array can be true! (i.e. a1 + a2 + a3 + ... + an = 1)*/
+       BooleanEdge applyExactlyOneConstraint (BooleanEdge *array, uint asize);
+       
        /** This function applies a logical operation to the Booleans in its input. */
-
+       
        BooleanEdge applyLogicalOperation(LogicOp op, 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 000ff18f63663264b44bf508637cc241cd83ac03..461a8590b74f845c48f68e36079b6a4a108d8c89 100644 (file)
--- a/src/pycsolver.py
+++ b/src/pycsolver.py
@@ -87,6 +87,8 @@ def loadCSolver():
        csolverlb.applyPredicate.restype = c_void_p
        csolverlb.applyLogicalOperation.argtypes = [c_void_p, c_uint, c_void_p, c_uint]
        csolverlb.applyLogicalOperation.restype = c_void_p
+       csolverlb.applyExactlyOneConstraint.argtypes = [c_void_p, c_void_p, c_uint]
+       csolverlb.applyExactlyOneConstraint.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]

diff --git a/src/satune_SatuneJavaAPI.cc b/src/satune_SatuneJavaAPI.cc
index 65d316a2b4c366d3fec5f955b852d436c6834ac1..21cd504ff5f00029cff1c7ef6041496c97b7dcf0 100644 (file)
--- a/src/satune_SatuneJavaAPI.cc
+++ b/src/satune_SatuneJavaAPI.cc
@@ -45,9 +45,11 @@ JNIEXPORT void JNICALL Java_satune_SatuneJavaAPI_resetCCSolver
  * Signature: (JIJI)J
  */
 JNIEXPORT jlong JNICALL Java_satune_SatuneJavaAPI_createSet
-       (JNIEnv *env, jobject obj, jlong solver, jint type, jlong elements, jint num)
+       (JNIEnv *env, jobject obj, jlong solver, jint type, jlongArray arr)
 {
-       return (jlong)createSet((void *)solver,(unsigned int) type, (long *)elements, (unsigned int) num);
+       jsize num = env->GetArrayLength(arr);
+       jlong *elements = env->GetLongArrayElements(arr, 0);
+       return (jlong)createSet((void *)solver,(unsigned int) type, elements, (unsigned int) num);
 }
 
 /*
@@ -266,8 +268,10 @@ JNIEXPORT jlong JNICALL Java_satune_SatuneJavaAPI_applyFunction
  * Signature: (JJJIJ)J
  */
 JNIEXPORT jlong JNICALL Java_satune_SatuneJavaAPI_applyPredicateTable
-       (JNIEnv *env, jobject obj, jlong solver, jlong predicate, jlong inputs, jint numInputs, jlong undefinedStatus)
+       (JNIEnv *env, jobject obj, jlong solver, jlong predicate, jlongArray arr, jlong undefinedStatus)
 {
+       jsize numInputs = env->GetArrayLength(arr);
+       jlong *inputs = env->GetLongArrayElements(arr, 0);
        return (jlong) applyPredicateTable((void *)solver,(void *)predicate, (void **)inputs, (unsigned int) numInputs, (void *)undefinedStatus);
 }
 
@@ -277,8 +281,10 @@ JNIEXPORT jlong JNICALL Java_satune_SatuneJavaAPI_applyPredicateTable
  * Signature: (JJJI)J
  */
 JNIEXPORT jlong JNICALL Java_satune_SatuneJavaAPI_applyPredicate
-       (JNIEnv *env, jobject obj, jlong solver, jlong predicate, jlong inputs, jint numInputs)
+       (JNIEnv *env, jobject obj, jlong solver, jlong predicate, jlongArray arr)
 {
+       jsize numInputs = env->GetArrayLength(arr);
+       jlong *inputs = env->GetLongArrayElements(arr, 0);
        return (jlong)applyPredicate((void *)solver,(void *)predicate, (void **)inputs, (unsigned int) numInputs);
 }
 
@@ -288,9 +294,24 @@ JNIEXPORT jlong JNICALL Java_satune_SatuneJavaAPI_applyPredicate
  * Signature: (JIJI)J
  */
 JNIEXPORT jlong JNICALL Java_satune_SatuneJavaAPI_applyLogicalOperation
-       (JNIEnv *env, jobject obj, jlong solver, jint op, jlong array, jint asize)
+       (JNIEnv *env, jobject obj, jlong solver, jint op, jlongArray arr)
 {
-       return (jlong)applyLogicalOperation((void *)solver,(unsigned int) op, (void *)array, (unsigned int) asize);
+       jsize asize = env->GetArrayLength(arr);
+       jlong *array = env->GetLongArrayElements(arr, 0);
+       return (jlong)applyLogicalOperation((void *)solver,(unsigned int) op, (void **)array, (unsigned int) asize);
+}
+
+/*
+ * Class:     SatuneJavaAPI
+ * Method:    applyLogicalOperation
+ * Signature: (JIJI)J
+ */
+JNIEXPORT jlong JNICALL Java_satune_SatuneJavaAPI_applyExactlyOneConstraint
+       (JNIEnv *env, jobject obj, jlong solver, jlongArray arr)
+{
+       jsize asize = env->GetArrayLength(arr);
+       jlong *array = env->GetLongArrayElements(arr, 0);
+       return (jlong)applyExactlyOneConstraint((void *)solver,(void **)array, (unsigned int) asize);
 }
 
 /*

diff --git a/src/satune_SatuneJavaAPI.h b/src/satune_SatuneJavaAPI.h
index db225133493c4775b47ba52ab96cf63dcb0f01cc..68703bcbf8b55f7bb0b5239fb3ec38348e2abb71 100644 (file)
--- a/src/satune_SatuneJavaAPI.h
+++ b/src/satune_SatuneJavaAPI.h
@@ -38,7 +38,7 @@ JNIEXPORT void JNICALL Java_satune_SatuneJavaAPI_resetCCSolver
  * Signature: (JIJI)J
  */
 JNIEXPORT jlong JNICALL Java_satune_SatuneJavaAPI_createSet
-       (JNIEnv *, jobject, jlong, jint, jlong, jint);
+       (JNIEnv *, jobject , jlong , jint , jlongArray arr);
 
 /*
  * Class:     satune_SatuneJavaAPI
@@ -198,7 +198,7 @@ JNIEXPORT jlong JNICALL Java_satune_SatuneJavaAPI_applyFunction
  * Signature: (JJJIJ)J
  */
 JNIEXPORT jlong JNICALL Java_satune_SatuneJavaAPI_applyPredicateTable
-       (JNIEnv *, jobject, jlong, jlong, jlong, jint, jlong);
+       (JNIEnv *, jobject, jlong, jlong, jlongArray, jlong);
 
 /*
  * Class:     satune_SatuneJavaAPI
@@ -206,7 +206,7 @@ JNIEXPORT jlong JNICALL Java_satune_SatuneJavaAPI_applyPredicateTable
  * Signature: (JJJI)J
  */
 JNIEXPORT jlong JNICALL Java_satune_SatuneJavaAPI_applyPredicate
-       (JNIEnv *, jobject, jlong, jlong, jlong, jint);
+       (JNIEnv *, jobject, jlong, jlong, jlongArray);
 
 /*
  * Class:     satune_SatuneJavaAPI
@@ -214,7 +214,15 @@ JNIEXPORT jlong JNICALL Java_satune_SatuneJavaAPI_applyPredicate
  * Signature: (JIJI)J
  */
 JNIEXPORT jlong JNICALL Java_satune_SatuneJavaAPI_applyLogicalOperation
-       (JNIEnv *, jobject, jlong, jint, jlong, jint);
+       (JNIEnv *, jobject, jlong, jint, jlongArray);
+
+/*
+ * Class:     satune_SatuneJavaAPI
+ * Method:    applyExactlyOneConstraint
+ * Signature: (JIJI)J
+ */
+JNIEXPORT jlong JNICALL Java_satune_SatuneJavaAPI_applyExactlyOneConstraint
+       (JNIEnv *, jobject, jlong, jlongArray );
 
 /*
  * Class:     satune_SatuneJavaAPI