generateAnyValueBinaryValueEncoding(encoding);
}
- void SATEncoder::freezeElementVariables(ElementEncoding *encoding){
+ void SATEncoder::freezeElementVariables(ElementEncoding *encoding) {
ASSERT(encoding->element->frozen);
- for(uint i=0; i< encoding->numVars; i++){
+ for (uint i = 0; i < encoding->numVars; i++) {
Edge e = encoding->variables[i];
ASSERT(edgeIsVarConst(e));
freezeVariable(cnf, e);
}
+ for(uint i=0; i< encoding->encArraySize; i++){
+ if(encoding->isinUseElement(i) && encoding->encoding != EENC_NONE && encoding->numVars > 1){
+ Edge e = encoding->edgeArray[i];
+ if(!edgeIsNull(e)){
+ ASSERT(edgeIsVarConst(e));
+ freezeVariable(cnf, e);
+ }
+ }
+ }
}
void SATEncoder::generateBinaryIndexEncodingVars(ElementEncoding *encoding) {
}
int SATEncoder::getMaximumUsedSize(ElementEncoding *encoding) {
+ if(encoding->encArraySize == 1){
+ return 1;
+ }
for (int i = encoding->encArraySize - 1; i >= 0; i--) {
if (encoding->isinUseElement(i))
return i + 1;
--- /dev/null
-
+ #include <iostream>
+ #include <fstream>
+ #include "csolver.h"
+ #include "hashset.h"
+ #include "cppvector.h"
+
+ const char * assertstart = "ASSERTSTART";
+ const char * assertend = "ASSERTEND";
+ const char * satstart = "SATSTART";
+ const char * satend = "SATEND";
+
+ int skipahead(const char * token1, const char * token2);
+ char * readuntilend(const char * token);
+ BooleanEdge parseConstraint(CSolver * solver, char * constraint, int & offset);
+ void processEquality(char * constraint, int &offset);
+
+ std::ifstream * file;
+ Order * order;
+ MutableSet * set;
+ class intwrapper {
+ public:
+ intwrapper(int _val) : value(_val) {
+ }
+ int32_t value;
+ };
+
+ unsigned int iw_hash_function(intwrapper *i) {
+ return i->value;
+ }
+
+ bool iw_equals(intwrapper *key1, intwrapper *key2) {
+ return (key1->value == key2->value);
+ }
+
+ typedef Hashset<intwrapper *, uintptr_t, PTRSHIFT, iw_hash_function, iw_equals> HashsetIW;
+
+ class OrderRec {
+ public:
+ OrderRec() : set (NULL), value(-1), alloced(false) {
+ }
+ ~OrderRec() {
+ if (set != NULL) {
+ set->resetAndDelete();
+ delete set;
+ }
+ }
+ HashsetIW * set;
+ int32_t value;
+ bool alloced;
+ };
+
+ typedef Hashtable<intwrapper *, OrderRec *, uintptr_t, PTRSHIFT, iw_hash_function, iw_equals> HashtableIW;
+ typedef Hashtable<intwrapper *, Boolean *, uintptr_t, PTRSHIFT, iw_hash_function, iw_equals> HashtableBV;
- if (retval == 0)
++Vector<OrderRec*> * orderRecVector = NULL;
+ HashtableIW * ordertable = NULL;
+ HashtableBV * vartable = new HashtableBV();
+
++void cleanAndFreeOrderRecVector(){
++ for(uint i=0; i< orderRecVector->getSize(); i++){
++ delete orderRecVector->get(i);
++ }
++ orderRecVector->clear();
++}
++
+ int main(int numargs, char ** argv) {
+ file = new std::ifstream(argv[1]);
+ char * assert = NULL;
+ char * sat = NULL;
++ Vector<OrderRec*> orderRecs;
++ orderRecVector = &orderRecs;
+ while(true) {
+ int retval = skipahead(assertstart, satstart);
+ printf("%d\n", retval);
- if (assert != NULL)
++ if (retval == 0){
+ break;
++ }
+ if (retval == 1) {
- ordertable->resetAndDeleteVals();
++ if (assert != NULL){
+ free(assert);
++ assert = NULL;
++ }
+ assert = readuntilend(assertend);
+ printf("[%s]\n", assert);
+ } else if (retval == 2) {
+ if (sat != NULL) {
+ free(sat);
++ sat = NULL;
+ vartable->resetAndDeleteKeys();
-
++ ordertable->reset();
++ cleanAndFreeOrderRecVector();
+ } else {
+ ordertable = new HashtableIW();
+ }
+ sat = readuntilend(satend);
+ CSolver *solver = new CSolver();
++ solver->turnoffOptimizations();
+ set = solver->createMutableSet(1);
+ order = solver->createOrder(SATC_TOTAL, (Set *) set);
+ int offset = 0;
+ processEquality(sat, offset);
+ offset = 0;
+ processEquality(assert, offset);
+ offset = 0;
+ solver->addConstraint(parseConstraint(solver, sat, offset));
+ offset = 0;
+ solver->addConstraint(parseConstraint(solver, assert, offset));
+ printf("[%s]\n", sat);
+ solver->finalizeMutableSet(set);
+ solver->serialize();
+ solver->printConstraints();
+ delete solver;
+ }
+ }
++
++ cleanAndFreeOrderRecVector();
++ if(ordertable != NULL){
++ delete ordertable;
++ }
++ if(assert != NULL){
++ free(assert);
++ }
++ if(sat != NULL){
++ free(sat);
++ }
++ vartable->resetAndDeleteKeys();
++ delete vartable;
+ file->close();
++ delete file;
+ }
+
+ void skipwhitespace(char * constraint, int & offset) {
+ //skip whitespace
+ while (constraint[offset] == ' ' || constraint[offset] == '\n')
+ offset++;
+ }
+
+ void doExit() {
+ printf("PARSE ERROR\n");
+ exit(-1);
+ }
+
+ int32_t getOrderVar(char *constraint, int & offset) {
+ if (constraint[offset++] != 'O' || constraint[offset++] != '!' ) {
+ doExit();
+ }
+ int32_t num = 0;
+ while(true) {
+ char next = constraint[offset];
+ if (next >= '0' && next <= '9') {
+ num = (num * 10) + (next - '0');
+ offset++;
+ } else
+ return num;
+ }
+ }
+
+ int32_t getBooleanVar(char *constraint, int & offset) {
+ if (constraint[offset++] != 'S' || constraint[offset++] != '!' ) {
+ doExit();
+ }
+ int32_t num = 0;
+ while(true) {
+ char next = constraint[offset];
+ if (next >= '0' && next <= '9') {
+ num = (num * 10) + (next - '0');
+ offset++;
+ } else
+ return num;
+ }
+ }
+
+ BooleanEdge checkBooleanVar(CSolver *solver, int32_t value) {
+ intwrapper v(value);
+ if (vartable->contains(&v)) {
+ return BooleanEdge(vartable->get(&v));
+ } else {
+ Boolean* ve = solver->getBooleanVar(2).getBoolean();
+ vartable->put(new intwrapper(value), ve);
+ return BooleanEdge(ve);
+ }
+ }
+
+ void mergeVars(int32_t value1, int32_t value2) {
+ intwrapper v1(value1);
+ intwrapper v2(value2);
+ OrderRec *r1 = ordertable->get(&v1);
+ OrderRec *r2 = ordertable->get(&v2);
+ if (r1 == r2) {
+ if (r1 == NULL) {
+ OrderRec * r = new OrderRec();
++ orderRecVector->push(r);
+ r->value = value1;
+ r->set = new HashsetIW();
+ intwrapper * k1 = new intwrapper(v1);
+ intwrapper * k2 = new intwrapper(v2);
+ r->set->add(k1);
+ r->set->add(k2);
+ ordertable->put(k1, r);
+ ordertable->put(k2, r);
+ }
+ } else if (r1 == NULL) {
+ intwrapper * k = new intwrapper(v1);
+ ordertable->put(k, r2);
+ r2->set->add(k);
+ } else if (r2 == NULL) {
+ intwrapper * k = new intwrapper(v2);
+ ordertable->put(k, r1);
+ r1->set->add(k);
+ } else {
+ SetIterator<intwrapper *, uintptr_t, PTRSHIFT, iw_hash_function, iw_equals> * it1 = r1->set->iterator();
+ while (it1->hasNext()) {
+ intwrapper * k = it1->next();
+ ordertable->put(k, r2);
+ r2->set->add(k);
+ }
+ delete r2->set;
+ r2->set = NULL;
+ delete r2;
+ delete it1;
+ }
+ }
+
+ int32_t checkordervar(CSolver * solver, int32_t value) {
+ intwrapper v(value);
+ OrderRec * rec = ordertable->get(&v);
+ if (rec == NULL) {
+ intwrapper * k = new intwrapper(value);
+ rec = new OrderRec();
++ orderRecVector->push(rec);
+ rec->value = value;
++ rec->set = new HashsetIW();
++ rec->set->add(k);
+ ordertable->put(k, rec);
+ }
+ if (!rec->alloced) {
+ solver->addItem(set, rec->value);
+ rec->alloced = true;
+ }
+ return rec->value;
+ }
+
+ void processEquality(char * constraint, int &offset) {
+ skipwhitespace(constraint, offset);
+ if (strncmp(&constraint[offset], "(and",4) == 0) {
+ offset +=4;
+ Vector<BooleanEdge> vec;
+ while(true) {
+ skipwhitespace(constraint, offset);
+ if (constraint[offset] == ')') {
+ offset++;
+ return;
+ }
+ processEquality(constraint, offset);
+ }
+ } else if (strncmp(&constraint[offset], "(<", 2) == 0) {
+ offset+=2;
+ skipwhitespace(constraint, offset);
+ getOrderVar(constraint, offset);
+ skipwhitespace(constraint, offset);
+ getOrderVar(constraint, offset);
+ skipwhitespace(constraint, offset);
+ if (constraint[offset++] != ')')
+ doExit();
+ return;
+ } else if (strncmp(&constraint[offset], "(=", 2) == 0) {
+ offset+=2;
+ skipwhitespace(constraint, offset);
+ int v1=getOrderVar(constraint, offset);
+ skipwhitespace(constraint, offset);
+ int v2=getOrderVar(constraint, offset);
+ skipwhitespace(constraint, offset);
+ if (constraint[offset++] != ')')
+ doExit();
+ mergeVars(v1, v2);
+ return;
+ } else {
+ getBooleanVar(constraint, offset);
+ skipwhitespace(constraint, offset);
+ return;
+ }
+ }
+
+ BooleanEdge parseConstraint(CSolver * solver, char * constraint, int & offset) {
+ skipwhitespace(constraint, offset);
+ if (strncmp(&constraint[offset], "(and", 4) == 0) {
+ offset +=4;
+ Vector<BooleanEdge> vec;
+ while(true) {
+ skipwhitespace(constraint, offset);
+ if (constraint[offset] == ')') {
+ offset++;
+ return solver->applyLogicalOperation(SATC_AND, vec.expose(), vec.getSize());
+ }
+ vec.push(parseConstraint(solver, constraint, offset));
+ }
+ } else if (strncmp(&constraint[offset], "(<", 2) == 0) {
+ offset+=2;
+ skipwhitespace(constraint, offset);
+ int32_t v1 = getOrderVar(constraint, offset);
+ skipwhitespace(constraint, offset);
+ int32_t v2 = getOrderVar(constraint, offset);
+ skipwhitespace(constraint, offset);
+ if (constraint[offset++] != ')')
+ doExit();
+ return solver->orderConstraint(order, checkordervar(solver, v1), checkordervar(solver, v2));
+ } else if (strncmp(&constraint[offset], "(=", 2) == 0) {
+ offset+=2;
+ skipwhitespace(constraint, offset);
+ getOrderVar(constraint, offset);
+ skipwhitespace(constraint, offset);
+ getOrderVar(constraint, offset);
+ skipwhitespace(constraint, offset);
+ if (constraint[offset++] != ')')
+ doExit();
+ return solver->getBooleanTrue();
+ } else {
+ int32_t v = getBooleanVar(constraint, offset);
+ skipwhitespace(constraint, offset);
+ return checkBooleanVar(solver, v);
+ }
+ }
+
+ int skipahead(const char * token1, const char * token2) {
+ int index1 = 0, index2 = 0;
+ char buffer[256];
+ while(true) {
+ if (token1[index1] == 0)
+ return 1;
+ if (token2[index2] == 0)
+ return 2;
+ if (file->eof())
+ return 0;
+ file->read(buffer, 1);
+ if (buffer[0] == token1[index1])
+ index1++;
+ else
+ index1 = 0;
+ if (buffer[0] == token2[index2])
+ index2++;
+ else
+ index2 = 0;
+ }
+ }
+
+ char * readuntilend(const char * token) {
+ int index = 0;
+ char buffer[256];
+ int length = 256;
+ int offset = 0;
+ char * outbuffer = (char *) malloc(length);
+ while(true) {
+ if (token[index] == 0) {
+ outbuffer[offset - index] = 0;
+ return outbuffer;
+ }
+ if (file->eof()) {
+ free(outbuffer);
+ return NULL;
+ }
+
+ file->read(buffer, 1);
+ outbuffer[offset++] = buffer[0];
+ if (offset == length) {
+ length = length * 2;
+ outbuffer = (char *) realloc(outbuffer, length);
+ }
+ if (buffer[0] == token[index])
+ index++;
+ else
+ index=0;
+ }
+ }
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]);
+ 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]);
+ for (uint i = 0; i < asize; i++) {
+ constr[i] = BooleanEdge((Boolean *)array[i]);
}
return CCSOLVER(solver)->applyExactlyOneConstraint( constr, (uint) asize).getRaw();
}
return CCSOLVER(solver)->solve();
}
+int solveIncremental(void *solver) {
+ return CCSOLVER(solver)->solveIncremental();
+}
+
long getElementValue(void *solver,void *element) {
return (long) CCSOLVER(solver)->getElementValue((Element *)element);
}
+void freezeElement(void *solver,void *element) {
+ CCSOLVER(solver)->freezeElement((Element *)element);
+}
+
int getBooleanValue(void *solver, void *boolean) {
return CCSOLVER(solver)->getBooleanValue(BooleanEdge((Boolean *) boolean));
}
CCSOLVER(solver)->printConstraints();
}
+void turnoffOptimizations(void *solver) {
+ CCSOLVER(solver)->turnoffOptimizations();
+}
+
void serialize(void *solver) {
CCSOLVER(solver)->serialize();
unsat(false),
booleanVarUsed(false),
incrementalMode(false),
+ optimizationsOff(false),
tuner(NULL),
elapsedTime(0),
satsolverTimeout(NOTIMEOUT),
}
void CSolver::freezeElementsVariables() {
-
- for(uint i=0; i< allElements.getSize(); i++){
+
+ for (uint i = 0; i < allElements.getSize(); i++) {
Element *e = allElements.get(i);
- if(e->frozen){
+ if (e->frozen) {
satEncoder->freezeElementVariables(&e->encoding);
}
}
return applyLogicalOperation(op, newarray, asize);
}
- BooleanEdge CSolver::applyExactlyOneConstraint (BooleanEdge *array, uint 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++){
+ for (uint i = 0; i < asize; i++) {
BooleanEdge oprand1 = array[i];
- BooleanEdge carray [asize -1];
+ BooleanEdge carray [asize - 1];
uint index = 0;
- for( uint j =0; j< asize; j++){
- if(i != j){
+ 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);
+ ASSERT(index == asize - 1);
+ newarray[i] = applyLogicalOperation(SATC_AND, carray, asize - 1);
}
- return applyLogicalOperation(SATC_AND, newarray, asize+1);
+ return applyLogicalOperation(SATC_AND, newarray, asize + 1);
}
BooleanEdge CSolver::applyLogicalOperation(LogicOp op, BooleanEdge *array, uint asize) {
}
void CSolver::addConstraint(BooleanEdge constraint) {
- if (!useInterpreter()) {
+ if (!useInterpreter() && !optimizationsOff) {
if (isTrue(constraint))
return;
else if (isFalse(constraint)) {
if (isUnSAT()) {
return IS_UNSAT;
}
-
-
+
+
long long startTime = getTimeNano();
bool deleteTuner = false;
if (tuner == NULL) {
}
int result = IS_INDETER;
ASSERT (!useInterpreter());
-
- computePolarities(this);
+ if(!optimizationsOff){
+ computePolarities(this);
+ }
// long long time1 = getTimeNano();
// model_print("Polarity time: %f\n", (time1 - startTime) / NANOSEC);
// Preprocess pp(this);
//Doing element optimization on new constraints
// ElementOpt eop(this);
// eop.doTransform();
-
+
//Since no new element is added, we assuming adding new constraint
//has no impact on previous encoding decisions
// EncodingGraph eg(this);
time2 = getTimeNano();
elapsedTime = time2 - startTime;
model_print("CSOLVER solve time: %f\n", elapsedTime / NANOSEC);
-
+
if (deleteTuner) {
delete tuner;
tuner = NULL;
}
delete orderit;
}
+ long long time1, time2;
+
computePolarities(this);
- long long time1 = getTimeNano();
- model_print("Polarity time: %f\n", (time1 - startTime) / NANOSEC);
- Preprocess pp(this);
- pp.doTransform();
- long long time2 = getTimeNano();
- model_print("Preprocess time: %f\n", (time2 - time1) / NANOSEC);
-
- DecomposeOrderTransform dot(this);
- dot.doTransform();
time1 = getTimeNano();
- model_print("Decompose Order: %f\n", (time1 - time2) / NANOSEC);
+ model_print("Polarity time: %f\n", (time1 - startTime) / NANOSEC);
+ if(!optimizationsOff){
+ Preprocess pp(this);
+ pp.doTransform();
+ time2 = getTimeNano();
+ model_print("Preprocess time: %f\n", (time2 - time1) / NANOSEC);
- IntegerEncodingTransform iet(this);
- iet.doTransform();
+ DecomposeOrderTransform dot(this);
+ dot.doTransform();
+ time1 = getTimeNano();
+ model_print("Decompose Order: %f\n", (time1 - time2) / NANOSEC);
- ElementOpt eop(this);
- eop.doTransform();
+ IntegerEncodingTransform iet(this);
+ iet.doTransform();
- EncodingGraph eg(this);
- eg.encode();
+ ElementOpt eop(this);
+ eop.doTransform();
+ EncodingGraph eg(this);
+ eg.encode();
+ }
naiveEncodingDecision(this);
// eg.validate();
-
- VarOrderingOpt bor(this, satEncoder);
- bor.doTransform();
-
- time2 = getTimeNano();
- model_print("Encoding Graph Time: %f\n", (time2 - time1) / NANOSEC);
+ if(!optimizationsOff){
+ VarOrderingOpt bor(this, satEncoder);
+ bor.doTransform();
+ time2 = getTimeNano();
+ model_print("Encoding Graph Time: %f\n", (time2 - time1) / NANOSEC);
+ }
satEncoder->encodeAllSATEncoder(this);
time1 = getTimeNano();
model_print("Elapse Encode time: %f\n", (time1 - startTime) / NANOSEC);
model_print("Is problem UNSAT after encoding: %d\n", unsat);
-
+
result = unsat ? IS_UNSAT : satEncoder->solve(satsolverTimeout);
model_print("Result Computed in SAT solver:\t%s\n", result == IS_SAT ? "SAT" : result == IS_INDETER ? "INDETERMINATE" : " UNSAT");
exit(-1);
}
- void CSolver::freezeElement(Element *e){
+ void CSolver::freezeElement(Element *e) {
e->freezeElement();
- if(!incrementalMode){
+ if (!incrementalMode) {
incrementalMode = true;
}
}
Set *getElementRange (Element *element);
void mustHaveValue(Element *element);
-
+
BooleanEdge getBooleanTrue();
BooleanEdge getBooleanFalse();
/** 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. */
* Incremental Solving for SATUNE.
* It only supports incremental solving for elements!
* No support for BooleanVar, BooleanOrder or using interpreters
- * @return
+ * @return
*/
int solveIncremental();
-
+
/** After getting the solution from the SAT solver, client can get the value of an element via this function*/
uint64_t getElementValue(Element *element);
void freezeElement(Element *e);
-
-
+ void turnoffOptimizations(){optimizationsOff = true;}
-
/** After getting the solution from the SAT solver, client can get the value of a boolean via this function*/
bool getBooleanValue(BooleanEdge boolean);
SetIteratorBooleanEdge *getConstraints() { return constraints.iterator(); }
bool isConstraintEncoded(BooleanEdge be) { return encodedConstraints.contains(be);}
void addEncodedConstraint(BooleanEdge be) {encodedConstraints.add(be);}
-
+
SATEncoder *getSATEncoder() {return satEncoder;}
void replaceBooleanWithTrue(BooleanEdge bexpr);
void handleIFFTrue(BooleanLogic *bexpr, BooleanEdge child);
void handleANDTrue(BooleanLogic *bexpr, BooleanEdge child);
void handleFunction(ElementFunction *ef, BooleanEdge child);
-
+
//These two functions are helpers if the client has a pointer to a
//Boolean object that we have since replaced
BooleanEdge rewriteLogicalOperation(LogicOp op, BooleanEdge *array, uint asize);
bool unsat;
bool booleanVarUsed;
bool incrementalMode;
+ bool optimizationsOff;
Tuner *tuner;
long long elapsedTime;
long satsolverTimeout;
Interpreter *interpreter;
+ bool noOptimization;
friend class ElementOpt;
friend class VarOrderingOpt;
};
/* DO NOT EDIT THIS FILE - it is machine generated */
#include "satune_SatuneJavaAPI.h"
#include "ccsolver.h"
- #define CCSOLVER(solver) (void*)solver
+ #define CCSOLVER(solver) (void *)solver
/* Header for class SatuneJavaAPI */
/*
(JNIEnv *env, jobject obj)
{
return (jlong)createCCSolver();
-
+
}
/*
* Signature: (JI)J
*/
JNIEXPORT jlong JNICALL Java_satune_SatuneJavaAPI_getBooleanTrue
- (JNIEnv * env, jobject obj, jlong solver)
+ (JNIEnv *env, jobject obj, jlong solver)
{
return (jlong)getBooleanTrue((void *)solver);
}
* Signature: (JI)J
*/
JNIEXPORT jlong JNICALL Java_satune_SatuneJavaAPI_getBooleanFalse
- (JNIEnv * env, jobject obj, jlong solver)
+ (JNIEnv *env, jobject obj, jlong solver)
{
return (jlong)getBooleanFalse((void *)solver);
}
return (jint) solve((void *)solver);
}
+/*
+ * Class: SatuneJavaAPI
+ * Method: solveIncremental
+ * Signature: (J)I
+ */
+JNIEXPORT jint JNICALL Java_satune_SatuneJavaAPI_solveIncremental
+ (JNIEnv *env, jobject obj, jlong solver)
+{
+ return (jint) solveIncremental((void *)solver);
+}
+
/*
* Class: SatuneJavaAPI
* Method: getElementValue
return (jlong) getElementValue((void *)solver,(void *)element);
}
+/*
+ * Class: SatuneJavaAPI
+ * Method: freezeElement
+ * Signature: (JJ)J
+ */
+JNIEXPORT void JNICALL Java_satune_SatuneJavaAPI_freezeElement
+ (JNIEnv *env, jobject obj, jlong solver, jlong element)
+{
+ freezeElement((void *)solver,(void *)element);
+}
+
/*
* Class: SatuneJavaAPI
* Method: getBooleanValue
printConstraints((void *)solver);
}
+/*
+ * Class: SatuneJavaAPI
+ * Method: turnoffOptimizations
+ * Signature: (J)V
+ */
+JNIEXPORT void JNICALL Java_satune_SatuneJavaAPI_turnoffOptimizations
+ (JNIEnv *env, jobject obj, jlong solver)
+{
+ turnoffOptimizations((void *)solver);
+}
+
/*
* Class: SatuneJavaAPI
* Method: serialize
* Signature: (JIJI)J
*/
JNIEXPORT jlong JNICALL Java_satune_SatuneJavaAPI_createSet
- (JNIEnv *, jobject , jlong , jint , jlongArray arr);
+ (JNIEnv *, jobject, jlong, jint, jlongArray arr);
/*
* Class: satune_SatuneJavaAPI
JNIEXPORT jint JNICALL Java_satune_SatuneJavaAPI_solve
(JNIEnv *, jobject, jlong);
+/*
+ * Class: satune_SatuneJavaAPI
+ * Method: solveIncremental
+ * Signature: (J)I
+ */
+JNIEXPORT jint JNICALL Java_satune_SatuneJavaAPI_solveIncremental
+ (JNIEnv *, jobject, jlong);
+
/*
* Class: satune_SatuneJavaAPI
* Method: getElementValue
JNIEXPORT jlong JNICALL Java_satune_SatuneJavaAPI_getElementValue
(JNIEnv *, jobject, jlong, jlong);
+
+/*
+ * Class: satune_SatuneJavaAPI
+ * Method: getElementValue
+ * Signature: (JJ)J
+ */
+JNIEXPORT void JNICALL Java_satune_SatuneJavaAPI_freezeElement
+ (JNIEnv *, jobject, jlong, jlong);
+
/*
* Class: satune_SatuneJavaAPI
* Method: getBooleanValue
JNIEXPORT void JNICALL Java_satune_SatuneJavaAPI_printConstraints
(JNIEnv *, jobject, jlong);
+/*
+ * Class: satune_SatuneJavaAPI
+ * Method: turnoffOptimizations
+ * Signature: (J)V
+ */
+JNIEXPORT void JNICALL Java_satune_SatuneJavaAPI_turnoffOptimizations
+ (JNIEnv *, jobject, jlong);
+
/*
* Class: satune_SatuneJavaAPI
* Method: serialize
projects / satune.git / commitdiff