From 081e954fa3566ad9a2522ca45bef8e29472d2a72 Mon Sep 17 00:00:00 2001 From: Hamed Gorjiara Date: Wed, 12 Jun 2019 18:12:09 -0700 Subject: [PATCH] Bug fixes for Java API + Exactly one constraints + Adding support for getting the wrong assumptions from SAT solver --- src/Backend/inc_solver.cc | 10 ++++++++++ src/ccsolver.cc | 16 ++++++++++++++-- src/ccsolver.h | 3 ++- src/csolver.cc | 20 ++++++++++++++++++++ src/csolver.h | 5 ++++- src/pycsolver.py | 2 ++ src/satune_SatuneJavaAPI.cc | 33 +++++++++++++++++++++++++++------ src/satune_SatuneJavaAPI.h | 16 ++++++++++++---- 8 files changed, 91 insertions(+), 14 deletions(-) diff --git a/src/Backend/inc_solver.cc b/src/Backend/inc_solver.cc index 2d6b8a4..72d3408 100644 --- 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 d773522..fa2e342 100644 --- 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 c668fbc..86d5a46 100644 --- 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 81aeb8e..a02227e 100644 --- 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 b99cf80..0ff566e 100644 --- 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 000ff18..461a859 100644 --- 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 65d316a..21cd504 100644 --- 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 db22513..68703bc 100644 --- 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 -- 2.34.1