void EncodingGraph::encode() {
- if (solver->getTuner()->getTunable(ENCODINGGRAPHOPT, &offon) == 0)
+ if (solver->isUnSAT() || solver->getTuner()->getTunable(ENCODINGGRAPHOPT, &offon) == 0)
return;
buildGraph();
SetIteratorEncodingSubGraph *itesg = subgraphs.iterator();
#include "csolver.h"
void computePolarities(CSolver *This) {
+ if(This->isUnSAT()){
+ return;
+ }
SetIteratorBooleanEdge *iterator = This->getConstraints();
while (iterator->hasNext()) {
BooleanEdge boolean = iterator->next();
}
void DecomposeOrderTransform::doTransform() {
+ if(solver->isUnSAT())
+ return;
HashsetOrder *orders = solver->getActiveOrders()->copy();
SetIteratorOrder *orderit = orders->iterator();
while (orderit->hasNext()) {
}
void ElementOpt::doTransform() {
- if (solver->getTuner()->getTunable(ELEMENTOPT, &onoff) == 0)
+ if (solver->isUnSAT() || solver->getTuner()->getTunable(ELEMENTOPT, &onoff) == 0)
return;
//Set once we know we are going to use it.
}
void IntegerEncodingTransform::doTransform() {
+ if(solver->isUnSAT()){
+ return;
+ }
HashsetOrder *orders = solver->getActiveOrders()->copy();
SetIteratorOrder *orderit = orders->iterator();
while (orderit->hasNext()) {
}
void Preprocess::doTransform() {
- if (!solver->isBooleanVarUsed() || solver->getTuner()->getTunable(PREPROCESS, &onoff) == 0)
+ if (solver->isUnSAT() || !solver->isBooleanVarUsed() || solver->getTuner()->getTunable(PREPROCESS, &onoff) == 0)
return;
BooleanIterator bit(solver);
}
void VarOrderingOpt::doTransform() {
+ if(solver->isUnSAT()){
+ return;
+ }
BooleanVarOrdering direction = (BooleanVarOrdering)solver->getTuner()->getTunable(VARIABLEORDER, &boolVarOrderingDesc);
if ( direction == CONSTRAINTORDERING ) {
return;
}
void SATEncoder::encodeAllSATEncoder(CSolver *csolver) {
+ if(csolver->isUnSAT()){
+ return;
+ }
SetIteratorBooleanEdge *iterator = csolver->getConstraints();
while (iterator->hasNext()) {
BooleanEdge constraint = iterator->next();
#include <strings.h>
void naiveEncodingDecision(CSolver *This) {
+ if(This->isUnSAT()){
+ return;
+ }
SetIteratorBooleanEdge *iterator = This->getConstraints();
while (iterator->hasNext()) {
BooleanEdge b = iterator->next();
C_SOURCES := $(wildcard *.c) $(wildcard AST/*.c) $(wildcard ASTTransform/*.c) $(wildcard Translator/*.c) $(wildcard ASTAnalyses/*.c) $(wildcard ASTAnalyses/Order/*.c) $(wildcard ASTAnalyses/Encoding/*.c) $(wildcard ASTAnalyses/Polarity/*.c) $(wildcard Tuner/*.c) $(wildcard Collections/*.c) $(wildcard Backend/*.c) $(wildcard Encoders/*.c) $(wildcard Serialize/*.c) $(wildcard Interpreter/*.c)
+J_SOURCES := $(wildcard *.java)
+
HEADERS := $(wildcard *.h) $(wildcard AST/*.h) $(wildcard ASTTransform/*.h) $(wildcard Translator/*.h) $(wildcard ASTAnalyses/*.h) $(wildcard ASTAnalyses/Order/*.h) $(wildcard ASTAnalyses/Encoding/*.h) $(wildcard ASTAnalyses/Polarity/*.h) $(wildcard Tuner/*.h) $(wildcard Collections/*.h) $(wildcard Backend/*.h) $(wildcard Encoders/*.h) $(wildcard Serialize/*.h) $(wildcard Interpreter/*.h)
OBJECTS := $(CPP_SOURCES:%.cc=$(OBJ_DIR)/%.o) $(C_SOURCES:%.c=$(OBJ_DIR)/%.o)
+J_OBJECTS := $(J_SOURCES:%.java=$(OBJ_DIR)/%.class)
+
CFLAGS := -Wall -O0 -g
CXXFLAGS := -std=c++1y -pthread
-CFLAGS += -IAST -IASTTransform -IASTAnalyses -IASTAnalyses/Polarity -IASTAnalyses/Order -IASTAnalyses/Encoding -ITranslator -ICollections -IBackend -I. -IEncoders -ITuner -ISerialize -IInterpreter
+CFLAGS += -IAST -IASTTransform -IASTAnalyses -IASTAnalyses/Polarity -IASTAnalyses/Order -IASTAnalyses/Encoding -ITranslator -ICollections -IBackend -I. -IEncoders -ITuner -ISerialize -IInterpreter -I$(JAVA_INC) -I$(JAVA_INC)/linux
LDFLAGS := -ldl -lrt -rdynamic -g
SHARED := -shared
MARKDOWN := ../docs/Markdown/Markdown.pl
-all: directories ${OBJ_DIR}/$(LIB_SO)
+all: directories ${OBJ_DIR}/$(LIB_SO) javaapi
directories: ${OBJ_DIR}
${OBJ_DIR}/%.o: %.c
$(CC) -fPIC -c $< -o $@ $(CFLAGS) -Wno-unused-variable
+javaapi: $(J_OBJECTS)
+
+${OBJ_DIR}/%.class: %.java
+ $(JAVAC) -d ${OBJ_DIR} $<
+
-include $(OBJECTS:%=$OBJ_DIR/.%.d)
PHONY += clean
--- /dev/null
+
+public class SatuneJavaAPI{
+ static {
+ System.loadLibrary("_cons_comp"); // loads lib_cons_comp.so
+ }
+ public native long createCCSolver();
+ public native void deleteCCSolver(long solver);
+ public native long createSet(long solver, int type, long elements, int num);
+ public native long createRangeSet(long solver,int type, long lowrange, long highrange);
+ public native long createRangeVar(long solver,int type, long lowrange, long highrange);
+ public native long createMutableSet(long solver, int type);
+ public native void addItem(long solver,long set, long element);
+ public native void finalizeMutableSet(long solver,long set);
+ public native long getElementVar(long solver,long set);
+ public native long getElementConst(long solver, int type, long value);
+ public native long getElementRange (long solver,long element);
+ public native long getBooleanVar(long solver, int type);
+ public native long createFunctionOperator(long solver, int op, long range, int overflowbehavior);
+ public native long createPredicateOperator(long solver, int op);
+ public native long createPredicateTable(long solver,long table, int behavior);
+ public native long createTable(long solver, long range);
+ public native long createTableForPredicate(long solver);
+ public native void addTableEntry(long solver,long table, long inputs, int inputSize, long result);
+ public native long completeTable(long solver,long table, int behavior);
+ public native long applyFunction(long solver,long function, long array, int numArrays, long overflowstatus);
+ public native long applyPredicateTable(long solver,long predicate, long inputs, int numInputs, long undefinedStatus);
+ public native long applyPredicate(long solver,long predicate, long inputs, int numInputs);
+ public native long applyLogicalOperation(long solver, int op, long array, int asize);
+ public native long applyLogicalOperationTwo(long solver, int op, long arg1, long arg2);
+ public native long applyLogicalOperationOne(long solver, int op, long arg);
+ public native void addConstraint(long solver,long constraint);
+ public native long createOrder(long solver, int type, long set);
+ public native long orderConstraint(long solver,long order, long first, long second);
+ public native int solve(long solver);
+ public native long getElementValue(long solver,long element);
+ public native int getBooleanValue(long solver,long bool);
+ public native int getOrderConstraintValue(long solver,long order, long first, long second);
+ public native void printConstraints(long solver);
+ public native void serialize(long solver);
+ public native void mustHaveValue(long solver, long element);
+ public native void setInterpreter(long solver, int type);
+ public native long clone(long solver);
+
+ public static void main(String[] args)
+ {
+ SatuneJavaAPI satuneapi = new SatuneJavaAPI();
+ long solver = satuneapi.createCCSolver();
+ long constr = satuneapi.getBooleanVar(solver, 1);
+ satuneapi.addConstraint(solver, constr);
+ int value = satuneapi.solve(solver);
+ if (value == 1) {
+ System.out.println("B1 = " + satuneapi.getBooleanValue(solver, constr));
+ } else {
+ System.out.println("UNSAT");
+ }
+ satuneapi.deleteCCSolver(solver);
+ }
+}
+
+
int main(int argc, char **argv) {
printf("%d\n", argc);
- if (argc != 2 && argc != 3) {
+ if (argc < 2 && argc > 4) {
printf("You only specify the name of the file ...\n");
- printf("./run.sh deserializer test.dump [--alloy/--z3/--smtrat/--mathsat]\n");
+ printf("./run.sh deserializer test.dump [--alloy/--z3/--smtrat/--mathsat] [timeout]\n");
exit(-1);
}
CSolver *solver;
- if(argc == 3){
+ if(argc >= 3){
solver = CSolver::deserialize(argv[1], getInterpreterType(argv[2]));
+ if(argc == 4){
+ solver->setSatSolverTimeout(atol(argv[3]));
+ }
} else {
solver = CSolver::deserialize(argv[1]);
}
}
for (int i = 1; i < argc; i++) {
CSolver *solver = CSolver::deserialize(argv[i]);
+ solver->printConstraints();
int value = solver->solve();
if (value == 1) {
printf("%s is SAT\n", argv[i]);
} else {
printf("%s is UNSAT\n", argv[i]);
}
- solver->printConstraints();
delete solver;
}
delete CCSOLVER(solver);
}
+void resetCCSolver(void *solver) {
+ CCSOLVER(solver)->resetSolver();
+}
+
void *createSet(void *solver,unsigned int type, long *elements, unsigned int num) {
return CCSOLVER(solver)->createSet((VarType) type, (uint64_t *)elements, (uint) num);
}
return CCSOLVER(solver)->getBooleanVar((VarType) type).getRaw();
}
+void *getBooleanTrue(void *solver){
+ return CCSOLVER(solver)->getBooleanTrue().getRaw();
+}
+
+void *getBooleanFalse(void *solver){
+ return CCSOLVER(solver)->getBooleanFalse().getRaw();
+}
+
void *createFunctionOperator(void *solver,unsigned int op, void *range,unsigned int overflowbehavior) {
return CCSOLVER(solver)->createFunctionOperator((ArithOp) op, (Set *)range, (OverFlowBehavior) overflowbehavior);
}
CCSOLVER(solver)->addConstraint(BooleanEdge((Boolean *) constraint));
}
+void printConstraint(void *solver,void *constraint) {
+ CCSOLVER(solver)->printConstraint(BooleanEdge((Boolean *) constraint));
+}
+
void *createOrder(void *solver,unsigned int type, void *set) {
return CCSOLVER(solver)->createOrder((OrderType) type, (Set *)set);
}
#endif
void *createCCSolver();
void deleteCCSolver(void *solver);
+void resetCCSolver(void *solver);
void *createSet(void *solver,unsigned int type, long *elements, unsigned int num);
void *createRangeSet(void *solver,unsigned int type, long lowrange, long highrange);
void *createRangeVar(void *solver,unsigned int type, long lowrange, long highrange);
void *getElementConst(void *solver,unsigned int type, long value);
void *getElementRange (void *solver,void *element);
void *getBooleanVar(void *solver,unsigned int type);
+void *getBooleanTrue(void *solver);
+void *getBooleanFalse(void *solver);
void *createFunctionOperator(void *solver,unsigned int op, void *range,unsigned int overflowbehavior);
void *createPredicateOperator(void *solver,unsigned int op);
void *createPredicateTable(void *solver,void *table, unsigned int behavior);
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);
+void printConstraint(void *solver,void *constraint);
void *createOrder(void *solver,unsigned int type, void *set);
void *orderConstraint(void *solver,void *order, long first, long second);
int solve(void *solver);
CC := gcc
CXX := g++
+JAVAC := javac
UNAME := $(shell uname)
-
+JAVA_INC := /usr/lib/jvm/default-java/include/
LIB_NAME := cons_comp
LIB_SO := lib_$(LIB_NAME).so
}
int CSolver::solve() {
+ if(isUnSAT()){
+ return IS_UNSAT;
+ }
long long startTime = getTimeNano();
bool deleteTuner = false;
if (tuner == NULL) {
time2 = getTimeNano();
model_print("Encoding Graph Time: %f\n", (time2 - time1) / NANOSEC);
-
+
satEncoder->encodeAllSATEncoder(this);
time1 = getTimeNano();
/** When everything is done, the client calls this function and then csolver starts to encode*/
int solve();
-
+
/** After getting the solution from the SAT solver, client can get the value of an element via this function*/
uint64_t getElementValue(Element *element);
--- /dev/null
+#!/bin/bash
+# run as the following:
+# ./runalloy.sh [hexiom] [--alloy]
+# ./runalloy.sh [nqueens] [--alloy]
+# ./runalloy.sh [sudoku-csolver] [--alloy]
+# ./runalloy.sh [killerSudoku] [--alloy]
+
+#./run.sh deserializealloytest ../Benchmarks/sudoku-csolver/4x4.dump --alloy
+#./run.sh java edu.mit.csail.sdg.alloy4whole.ExampleAlloyCompilerNoViz satune.als > solution.log
+
+if [ "$#" -lt 2 ]; then
+ echo "Illegal number of argument"
+ echo "./runinterpreter.sh [benchmark] [--alloy/--z3/--smtrat/--mathsat] [timeout]"
+ exit 1
+fi
+
+
+BIN=./bin
+DUMP=$(find . -name "*.dump")
+cd $BIN
+for d in $DUMP; do
+ if [[ $d = *$1* ]]; then
+ echo $d
+ START=$(date +%s.%N)
+ ./run.sh deserializealloytest "."$d $2 $3
+ END=$(date +%s.%N)
+ DIFF=$(echo "$END - $START" | bc)
+ echo "CSOLVER solve time: $DIFF"
+ cat solution.sol
+ echo "Best tuner"
+ fi
+done
--- /dev/null
+/* DO NOT EDIT THIS FILE - it is machine generated */
+#include "satune_SatuneJavaAPI.h"
+#include "ccsolver.h"
+#define CCSOLVER(solver) (void*)solver
+/* Header for class SatuneJavaAPI */
+
+/*
+ * Class: SatuneJavaAPI
+ * Method: createCCSolver
+ * Signature: ()J
+ */
+
+JNIEXPORT jlong JNICALL Java_satune_SatuneJavaAPI_createCCSolver
+ (JNIEnv *env, jobject obj)
+{
+ return (jlong)createCCSolver();
+
+}
+
+/*
+ * Class: SatuneJavaAPI
+ * Method: deleteCCSolver
+ * Signature: (J)V
+ */
+JNIEXPORT void JNICALL Java_satune_SatuneJavaAPI_deleteCCSolver
+ (JNIEnv *env, jobject obj, jlong solver)
+{
+ deleteCCSolver(CCSOLVER(solver));
+}
+
+/*
+ * Class: SatuneJavaAPI
+ * Method: resetCCSolver
+ * Signature: (J)V
+ */
+JNIEXPORT void JNICALL Java_satune_SatuneJavaAPI_resetCCSolver
+ (JNIEnv *env, jobject obj, jlong solver)
+{
+ resetCCSolver(CCSOLVER(solver));
+}
+
+/*
+ * Class: SatuneJavaAPI
+ * Method: createSet
+ * Signature: (JIJI)J
+ */
+JNIEXPORT jlong JNICALL Java_satune_SatuneJavaAPI_createSet
+ (JNIEnv *env, jobject obj, jlong solver, jint type, jlong elements, jint num)
+{
+ return (jlong)createSet((void *)solver,(unsigned int) type, (long *)elements, (unsigned int) num);
+}
+
+/*
+ * Class: SatuneJavaAPI
+ * Method: createRangeSet
+ * Signature: (JIJJ)J
+ */
+JNIEXPORT jlong JNICALL Java_satune_SatuneJavaAPI_createRangeSet
+ (JNIEnv *env, jobject obj, jlong solver, jint type, jlong lowrange, jlong highrange)
+{
+ return (jlong)createRangeSet((void *)solver,(unsigned int) type, (long) lowrange, (long) highrange);
+}
+
+/*
+ * Class: SatuneJavaAPI
+ * Method: createRangeVar
+ * Signature: (JIJJ)J
+ */
+JNIEXPORT jlong JNICALL Java_satune_SatuneJavaAPI_createRangeVar
+ (JNIEnv *env, jobject obj, jlong solver, jint type, jlong lowrange, jlong highrange)
+{
+ return (jlong)createRangeVar((void *)solver,(unsigned int) type, (long) lowrange, (long) highrange);
+}
+
+/*
+ * Class: SatuneJavaAPI
+ * Method: createMutableSet
+ * Signature: (JI)J
+ */
+JNIEXPORT jlong JNICALL Java_satune_SatuneJavaAPI_createMutableSet
+ (JNIEnv *env, jobject obj, jlong solver, jint type)
+{
+ return (jlong)createMutableSet((void *)solver,(unsigned int) type);
+}
+
+/*
+ * Class: SatuneJavaAPI
+ * Method: addItem
+ * Signature: (JJJ)V
+ */
+JNIEXPORT void JNICALL Java_satune_SatuneJavaAPI_addItem
+ (JNIEnv *env, jobject obj, jlong solver, jlong set, jlong element)
+{
+ addItem((void *)solver,(void *)set, (long) element);
+}
+
+/*
+ * Class: SatuneJavaAPI
+ * Method: finalizeMutableSet
+ * Signature: (JJ)V
+ */
+JNIEXPORT void JNICALL Java_satune_SatuneJavaAPI_finalizeMutableSet
+ (JNIEnv *ev, jobject obj, jlong solver, jlong set)
+{
+ finalizeMutableSet((void *)solver,(void *)set);
+}
+
+/*
+ * Class: SatuneJavaAPI
+ * Method: getElementVar
+ * Signature: (JJ)J
+ */
+JNIEXPORT jlong JNICALL Java_satune_SatuneJavaAPI_getElementVar
+ (JNIEnv *env, jobject obj, jlong solver, jlong set)
+{
+ return (jlong) getElementVar((void *)solver,(void *)set);
+}
+
+/*
+ * Class: SatuneJavaAPI
+ * Method: getElementConst
+ * Signature: (JIJ)J
+ */
+JNIEXPORT jlong JNICALL Java_satune_SatuneJavaAPI_getElementConst
+ (JNIEnv *env, jobject obj, jlong solver, jint type, jlong value)
+{
+ return (jlong)getElementConst((void *)solver,(unsigned int) type, (long) value);
+}
+
+/*
+ * Class: SatuneJavaAPI
+ * Method: getElementRange
+ * Signature: (JJ)J
+ */
+JNIEXPORT jlong JNICALL Java_satune_SatuneJavaAPI_getElementRange
+ (JNIEnv *env, jobject obj, jlong solver, jlong element)
+{
+ return (jlong)getElementRange ((void *)solver,(void *)element);
+}
+
+/*
+ * Class: SatuneJavaAPI
+ * Method: getBooleanVar
+ * Signature: (JI)J
+ */
+JNIEXPORT jlong JNICALL Java_satune_SatuneJavaAPI_getBooleanVar
+ (JNIEnv *env, jobject obj, jlong solver, jint type)
+{
+ return (jlong)getBooleanVar((void *)solver,(unsigned int) type);
+}
+
+
+/*
+ * Class: SatuneJavaAPI
+ * Method: getBooleanVar
+ * Signature: (JI)J
+ */
+JNIEXPORT jlong JNICALL Java_satune_SatuneJavaAPI_getBooleanTrue
+ (JNIEnv * env, jobject obj, jlong solver)
+{
+ return (jlong)getBooleanTrue((void *)solver);
+}
+
+/*
+ * Class: SatuneJavaAPI
+ * Method: getBooleanVar
+ * Signature: (JI)J
+ */
+JNIEXPORT jlong JNICALL Java_satune_SatuneJavaAPI_getBooleanFalse
+ (JNIEnv * env, jobject obj, jlong solver)
+{
+ return (jlong)getBooleanFalse((void *)solver);
+}
+
+/*
+ * Class: SatuneJavaAPI
+ * Method: createFunctionOperator
+ * Signature: (JIJI)J
+ */
+JNIEXPORT jlong JNICALL Java_satune_SatuneJavaAPI_createFunctionOperator
+ (JNIEnv *env, jobject obj, jlong solver, jint op, jlong range, jint overflowbehavior)
+{
+ return (jlong)createFunctionOperator((void *)solver,(unsigned int) op, (void *)range,(unsigned int) overflowbehavior);
+}
+
+/*
+ * Class: SatuneJavaAPI
+ * Method: createPredicateOperator
+ * Signature: (JI)J
+ */
+JNIEXPORT jlong JNICALL Java_satune_SatuneJavaAPI_createPredicateOperator
+ (JNIEnv *env, jobject obj, jlong solver, jint op)
+{
+ return (jlong)createPredicateOperator((void *)solver,(unsigned int) op);
+}
+
+/*
+ * Class: SatuneJavaAPI
+ * Method: createPredicateTable
+ * Signature: (JJI)J
+ */
+JNIEXPORT jlong JNICALL Java_satune_SatuneJavaAPI_createPredicateTable
+ (JNIEnv *env, jobject obj, jlong solver, jlong table, jint behavior)
+{
+ return (jlong) createPredicateTable((void *)solver,(void *)table, (unsigned int) behavior);
+}
+
+/*
+ * Class: SatuneJavaAPI
+ * Method: createTable
+ * Signature: (JJ)J
+ */
+JNIEXPORT jlong JNICALL Java_satune_SatuneJavaAPI_createTable
+ (JNIEnv *env, jobject obj, jlong solver, jlong range)
+{
+ return (jlong)createTable((void *)solver, (void *)range);
+}
+
+/*
+ * Class: SatuneJavaAPI
+ * Method: createTableForPredicate
+ * Signature: (J)J
+ */
+JNIEXPORT jlong JNICALL Java_satune_SatuneJavaAPI_createTableForPredicate
+ (JNIEnv *env, jobject obj, jlong solver)
+{
+ return (jlong)createTableForPredicate((void *)solver);
+}
+
+/*
+ * Class: SatuneJavaAPI
+ * Method: addTableEntry
+ * Signature: (JJJIJ)V
+ */
+JNIEXPORT void JNICALL Java_satune_SatuneJavaAPI_addTableEntry
+ (JNIEnv *env, jobject obj, jlong solver, jlong table, jlong inputs, jint inputSize, jlong result)
+{
+ addTableEntry((void *)solver,(void *)table, (void *)inputs, (unsigned int) inputSize, (long) result);
+}
+
+/*
+ * Class: SatuneJavaAPI
+ * Method: completeTable
+ * Signature: (JJI)J
+ */
+JNIEXPORT jlong JNICALL Java_satune_SatuneJavaAPI_completeTable
+ (JNIEnv *env, jobject obj, jlong solver, jlong table, jint behavior)
+{
+ return (jlong)completeTable((void *)solver,(void *)table, (unsigned int) behavior);
+}
+
+/*
+ * Class: SatuneJavaAPI
+ * Method: applyFunction
+ * Signature: (JJJIJ)J
+ */
+JNIEXPORT jlong JNICALL Java_satune_SatuneJavaAPI_applyFunction
+ (JNIEnv *env, jobject obj, jlong solver, jlong function, jlong array, jint numArrays, jlong overflowstatus)
+{
+ return (jlong)applyFunction((void *)solver,(void *)function, (void **)array, (unsigned int) numArrays, (void *)overflowstatus);
+}
+
+/*
+ * Class: SatuneJavaAPI
+ * Method: applyPredicateTable
+ * Signature: (JJJIJ)J
+ */
+JNIEXPORT jlong JNICALL Java_satune_SatuneJavaAPI_applyPredicateTable
+ (JNIEnv *env, jobject obj, jlong solver, jlong predicate, jlong inputs, jint numInputs, jlong undefinedStatus)
+{
+ return (jlong) applyPredicateTable((void *)solver,(void *)predicate, (void **)inputs, (unsigned int) numInputs, (void *)undefinedStatus);
+}
+
+/*
+ * Class: SatuneJavaAPI
+ * Method: applyPredicate
+ * Signature: (JJJI)J
+ */
+JNIEXPORT jlong JNICALL Java_satune_SatuneJavaAPI_applyPredicate
+ (JNIEnv *env, jobject obj, jlong solver, jlong predicate, jlong inputs, jint numInputs)
+{
+ return (jlong)applyPredicate((void *)solver,(void *)predicate, (void **)inputs, (unsigned int) numInputs);
+}
+
+/*
+ * Class: SatuneJavaAPI
+ * Method: applyLogicalOperation
+ * Signature: (JIJI)J
+ */
+JNIEXPORT jlong JNICALL Java_satune_SatuneJavaAPI_applyLogicalOperation
+ (JNIEnv *env, jobject obj, jlong solver, jint op, jlong array, jint asize)
+{
+ return (jlong)applyLogicalOperation((void *)solver,(unsigned int) op, (void *)array, (unsigned int) asize);
+}
+
+/*
+ * Class: SatuneJavaAPI
+ * Method: applyLogicalOperationTwo
+ * Signature: (JIJJ)J
+ */
+JNIEXPORT jlong JNICALL Java_satune_SatuneJavaAPI_applyLogicalOperationTwo
+ (JNIEnv *env, jobject obj, jlong solver, jint op, jlong arg1, jlong arg2)
+{
+ return (jlong) applyLogicalOperationTwo((void *)solver,(unsigned int) op, (void *)arg1, (void *)arg2);
+}
+
+/*
+ * Class: SatuneJavaAPI
+ * Method: applyLogicalOperationOne
+ * Signature: (JIJ)J
+ */
+JNIEXPORT jlong JNICALL Java_satune_SatuneJavaAPI_applyLogicalOperationOne
+ (JNIEnv *env, jobject obj, jlong solver, jint op, jlong arg)
+{
+ return (jlong)applyLogicalOperationOne((void *)solver,(unsigned int) op, (void *)arg);
+}
+
+/*
+ * Class: SatuneJavaAPI
+ * Method: addConstraint
+ * Signature: (JJ)V
+ */
+JNIEXPORT void JNICALL Java_satune_SatuneJavaAPI_addConstraint
+ (JNIEnv *env, jobject obj, jlong solver, jlong constraint)
+{
+ addConstraint((void *)solver,(void *)constraint);
+}
+
+/*
+ * Class: SatuneJavaAPI
+ * Method: printConstraint
+ * Signature: (JJ)V
+ */
+JNIEXPORT void JNICALL Java_satune_SatuneJavaAPI_printConstraint
+ (JNIEnv *env, jobject obj, jlong solver, jlong constraint)
+{
+ printConstraint((void *)solver,(void *)constraint);
+}
+
+/*
+ * Class: SatuneJavaAPI
+ * Method: createOrder
+ * Signature: (JIJ)J
+ */
+JNIEXPORT jlong JNICALL Java_satune_SatuneJavaAPI_createOrder
+ (JNIEnv *env, jobject obj, jlong solver, jint type, jlong set)
+{
+ return (jlong)createOrder((void *)solver,(unsigned int) type, (void *)set);
+}
+
+/*
+ * Class: SatuneJavaAPI
+ * Method: orderConstraint
+ * Signature: (JJJJ)J
+ */
+JNIEXPORT jlong JNICALL Java_satune_SatuneJavaAPI_orderConstraint
+ (JNIEnv *env, jobject obj, jlong solver, jlong order, jlong first, jlong second)
+{
+ return (jlong)orderConstraint((void *)solver,(void *)order, (long) first, (long) second);
+}
+
+/*
+ * Class: SatuneJavaAPI
+ * Method: solve
+ * Signature: (J)I
+ */
+JNIEXPORT jint JNICALL Java_satune_SatuneJavaAPI_solve
+ (JNIEnv *env, jobject obj, jlong solver)
+{
+ return (jint) solve((void *)solver);
+}
+
+/*
+ * Class: SatuneJavaAPI
+ * Method: getElementValue
+ * Signature: (JJ)J
+ */
+JNIEXPORT jlong JNICALL Java_satune_SatuneJavaAPI_getElementValue
+ (JNIEnv *env, jobject obj, jlong solver, jlong element)
+{
+ return (jlong) getElementValue((void *)solver,(void *)element);
+}
+
+/*
+ * Class: SatuneJavaAPI
+ * Method: getBooleanValue
+ * Signature: (JJ)I
+ */
+JNIEXPORT jint JNICALL Java_satune_SatuneJavaAPI_getBooleanValue
+ (JNIEnv *env, jobject obj, jlong solver, jlong boolean)
+{
+ return (jint) getBooleanValue((void *)solver, (void *)boolean);
+}
+
+/*
+ * Class: SatuneJavaAPI
+ * Method: getOrderConstraintValue
+ * Signature: (JJJJ)I
+ */
+JNIEXPORT jint JNICALL Java_satune_SatuneJavaAPI_getOrderConstraintValue
+ (JNIEnv *env, jobject obj, jlong solver, jlong order, jlong first, jlong second)
+{
+ return (jint) getOrderConstraintValue((void *)solver,(void *)order, (long) first, (long) second);
+}
+
+/*
+ * Class: SatuneJavaAPI
+ * Method: printConstraints
+ * Signature: (J)V
+ */
+JNIEXPORT void JNICALL Java_satune_SatuneJavaAPI_printConstraints
+ (JNIEnv *env, jobject obj, jlong solver)
+{
+ printConstraints((void *)solver);
+}
+
+/*
+ * Class: SatuneJavaAPI
+ * Method: serialize
+ * Signature: (J)V
+ */
+JNIEXPORT void JNICALL Java_satune_SatuneJavaAPI_serialize
+ (JNIEnv *env, jobject obj, jlong solver)
+{
+ serialize((void *)solver);
+}
+
+/*
+ * Class: SatuneJavaAPI
+ * Method: mustHaveValue
+ * Signature: (JJ)V
+ */
+JNIEXPORT void JNICALL Java_satune_SatuneJavaAPI_mustHaveValue
+ (JNIEnv *env, jobject obj, jlong solver, jlong element)
+{
+ mustHaveValue((void *)solver, (void *)element);
+}
+
+/*
+ * Class: SatuneJavaAPI
+ * Method: setInterpreter
+ * Signature: (JI)V
+ */
+JNIEXPORT void JNICALL Java_satune_SatuneJavaAPI_setInterpreter
+ (JNIEnv *env, jobject obj, jlong solver, jint type)
+{
+ setInterpreter((void *)solver, (unsigned int) type);
+}
+
+/*
+ * Class: SatuneJavaAPI
+ * Method: clone
+ * Signature: (J)J
+ */
+JNIEXPORT jlong JNICALL Java_satune_SatuneJavaAPI_clone
+ (JNIEnv *env, jobject obj, jlong solver)
+{
+ return (jlong)clone((void *)solver);
+}
+
--- /dev/null
+/* DO NOT EDIT THIS FILE - it is machine generated */
+#include <jni.h>
+/* Header for class satune_SatuneJavaAPI */
+
+#ifndef _Included_satune_SatuneJavaAPI
+#define _Included_satune_SatuneJavaAPI
+#ifdef __cplusplus
+extern "C" {
+#endif
+/*
+ * Class: satune_SatuneJavaAPI
+ * Method: createCCSolver
+ * Signature: ()J
+ */
+JNIEXPORT jlong JNICALL Java_satune_SatuneJavaAPI_createCCSolver
+ (JNIEnv *, jobject);
+
+/*
+ * Class: satune_SatuneJavaAPI
+ * Method: deleteCCSolver
+ * Signature: (J)V
+ */
+JNIEXPORT void JNICALL Java_satune_SatuneJavaAPI_deleteCCSolver
+ (JNIEnv *, jobject, jlong);
+
+
+/*
+ * Class: satune_SatuneJavaAPI
+ * Method: resetCCSolver
+ * Signature: (J)V
+ */
+JNIEXPORT void JNICALL Java_satune_SatuneJavaAPI_resetCCSolver
+ (JNIEnv *, jobject, jlong);
+
+/*
+ * Class: satune_SatuneJavaAPI
+ * Method: createSet
+ * Signature: (JIJI)J
+ */
+JNIEXPORT jlong JNICALL Java_satune_SatuneJavaAPI_createSet
+ (JNIEnv *, jobject, jlong, jint, jlong, jint);
+
+/*
+ * Class: satune_SatuneJavaAPI
+ * Method: createRangeSet
+ * Signature: (JIJJ)J
+ */
+JNIEXPORT jlong JNICALL Java_satune_SatuneJavaAPI_createRangeSet
+ (JNIEnv *, jobject, jlong, jint, jlong, jlong);
+
+/*
+ * Class: satune_SatuneJavaAPI
+ * Method: createRangeVar
+ * Signature: (JIJJ)J
+ */
+JNIEXPORT jlong JNICALL Java_satune_SatuneJavaAPI_createRangeVar
+ (JNIEnv *, jobject, jlong, jint, jlong, jlong);
+
+/*
+ * Class: satune_SatuneJavaAPI
+ * Method: createMutableSet
+ * Signature: (JI)J
+ */
+JNIEXPORT jlong JNICALL Java_satune_SatuneJavaAPI_createMutableSet
+ (JNIEnv *, jobject, jlong, jint);
+
+/*
+ * Class: satune_SatuneJavaAPI
+ * Method: addItem
+ * Signature: (JJJ)V
+ */
+JNIEXPORT void JNICALL Java_satune_SatuneJavaAPI_addItem
+ (JNIEnv *, jobject, jlong, jlong, jlong);
+
+/*
+ * Class: satune_SatuneJavaAPI
+ * Method: finalizeMutableSet
+ * Signature: (JJ)V
+ */
+JNIEXPORT void JNICALL Java_satune_SatuneJavaAPI_finalizeMutableSet
+ (JNIEnv *, jobject, jlong, jlong);
+
+/*
+ * Class: satune_SatuneJavaAPI
+ * Method: getElementVar
+ * Signature: (JJ)J
+ */
+JNIEXPORT jlong JNICALL Java_satune_SatuneJavaAPI_getElementVar
+ (JNIEnv *, jobject, jlong, jlong);
+
+/*
+ * Class: satune_SatuneJavaAPI
+ * Method: getElementConst
+ * Signature: (JIJ)J
+ */
+JNIEXPORT jlong JNICALL Java_satune_SatuneJavaAPI_getElementConst
+ (JNIEnv *, jobject, jlong, jint, jlong);
+
+/*
+ * Class: satune_SatuneJavaAPI
+ * Method: getElementRange
+ * Signature: (JJ)J
+ */
+JNIEXPORT jlong JNICALL Java_satune_SatuneJavaAPI_getElementRange
+ (JNIEnv *, jobject, jlong, jlong);
+
+/*
+ * Class: satune_SatuneJavaAPI
+ * Method: getBooleanVar
+ * Signature: (JI)J
+ */
+JNIEXPORT jlong JNICALL Java_satune_SatuneJavaAPI_getBooleanVar
+ (JNIEnv *, jobject, jlong, jint);
+
+/*
+ * Class: satune_SatuneJavaAPI
+ * Method: getBooleanTrue
+ * Signature: (J)J
+ */
+JNIEXPORT jlong JNICALL Java_satune_SatuneJavaAPI_getBooleanTrue
+ (JNIEnv *, jobject, jlong);
+
+/*
+ * Class: satune_SatuneJavaAPI
+ * Method: getBooleanFalse
+ * Signature: (J)J
+ */
+JNIEXPORT jlong JNICALL Java_satune_SatuneJavaAPI_getBooleanFalse
+ (JNIEnv *, jobject, jlong);
+
+/*
+ * Class: satune_SatuneJavaAPI
+ * Method: createFunctionOperator
+ * Signature: (JIJI)J
+ */
+JNIEXPORT jlong JNICALL Java_satune_SatuneJavaAPI_createFunctionOperator
+ (JNIEnv *, jobject, jlong, jint, jlong, jint);
+
+/*
+ * Class: satune_SatuneJavaAPI
+ * Method: createPredicateOperator
+ * Signature: (JI)J
+ */
+JNIEXPORT jlong JNICALL Java_satune_SatuneJavaAPI_createPredicateOperator
+ (JNIEnv *, jobject, jlong, jint);
+
+/*
+ * Class: satune_SatuneJavaAPI
+ * Method: createPredicateTable
+ * Signature: (JJI)J
+ */
+JNIEXPORT jlong JNICALL Java_satune_SatuneJavaAPI_createPredicateTable
+ (JNIEnv *, jobject, jlong, jlong, jint);
+
+/*
+ * Class: satune_SatuneJavaAPI
+ * Method: createTable
+ * Signature: (JJ)J
+ */
+JNIEXPORT jlong JNICALL Java_satune_SatuneJavaAPI_createTable
+ (JNIEnv *, jobject, jlong, jlong);
+
+/*
+ * Class: satune_SatuneJavaAPI
+ * Method: createTableForPredicate
+ * Signature: (J)J
+ */
+JNIEXPORT jlong JNICALL Java_satune_SatuneJavaAPI_createTableForPredicate
+ (JNIEnv *, jobject, jlong);
+
+/*
+ * Class: satune_SatuneJavaAPI
+ * Method: addTableEntry
+ * Signature: (JJJIJ)V
+ */
+JNIEXPORT void JNICALL Java_satune_SatuneJavaAPI_addTableEntry
+ (JNIEnv *, jobject, jlong, jlong, jlong, jint, jlong);
+
+/*
+ * Class: satune_SatuneJavaAPI
+ * Method: completeTable
+ * Signature: (JJI)J
+ */
+JNIEXPORT jlong JNICALL Java_satune_SatuneJavaAPI_completeTable
+ (JNIEnv *, jobject, jlong, jlong, jint);
+
+/*
+ * Class: satune_SatuneJavaAPI
+ * Method: applyFunction
+ * Signature: (JJJIJ)J
+ */
+JNIEXPORT jlong JNICALL Java_satune_SatuneJavaAPI_applyFunction
+ (JNIEnv *, jobject, jlong, jlong, jlong, jint, jlong);
+
+/*
+ * Class: satune_SatuneJavaAPI
+ * Method: applyPredicateTable
+ * Signature: (JJJIJ)J
+ */
+JNIEXPORT jlong JNICALL Java_satune_SatuneJavaAPI_applyPredicateTable
+ (JNIEnv *, jobject, jlong, jlong, jlong, jint, jlong);
+
+/*
+ * Class: satune_SatuneJavaAPI
+ * Method: applyPredicate
+ * Signature: (JJJI)J
+ */
+JNIEXPORT jlong JNICALL Java_satune_SatuneJavaAPI_applyPredicate
+ (JNIEnv *, jobject, jlong, jlong, jlong, jint);
+
+/*
+ * Class: satune_SatuneJavaAPI
+ * Method: applyLogicalOperation
+ * Signature: (JIJI)J
+ */
+JNIEXPORT jlong JNICALL Java_satune_SatuneJavaAPI_applyLogicalOperation
+ (JNIEnv *, jobject, jlong, jint, jlong, jint);
+
+/*
+ * Class: satune_SatuneJavaAPI
+ * Method: applyLogicalOperationTwo
+ * Signature: (JIJJ)J
+ */
+JNIEXPORT jlong JNICALL Java_satune_SatuneJavaAPI_applyLogicalOperationTwo
+ (JNIEnv *, jobject, jlong, jint, jlong, jlong);
+
+/*
+ * Class: satune_SatuneJavaAPI
+ * Method: applyLogicalOperationOne
+ * Signature: (JIJ)J
+ */
+JNIEXPORT jlong JNICALL Java_satune_SatuneJavaAPI_applyLogicalOperationOne
+ (JNIEnv *, jobject, jlong, jint, jlong);
+
+/*
+ * Class: satune_SatuneJavaAPI
+ * Method: addConstraint
+ * Signature: (JJ)V
+ */
+JNIEXPORT void JNICALL Java_satune_SatuneJavaAPI_addConstraint
+ (JNIEnv *, jobject, jlong, jlong);
+
+/*
+ * Class: satune_SatuneJavaAPI
+ * Method: printConstraint
+ * Signature: (JJ)V
+ */
+JNIEXPORT void JNICALL Java_satune_SatuneJavaAPI_printConstraint
+ (JNIEnv *, jobject, jlong, jlong);
+
+/*
+ * Class: satune_SatuneJavaAPI
+ * Method: createOrder
+ * Signature: (JIJ)J
+ */
+JNIEXPORT jlong JNICALL Java_satune_SatuneJavaAPI_createOrder
+ (JNIEnv *, jobject, jlong, jint, jlong);
+
+/*
+ * Class: satune_SatuneJavaAPI
+ * Method: orderConstraint
+ * Signature: (JJJJ)J
+ */
+JNIEXPORT jlong JNICALL Java_satune_SatuneJavaAPI_orderConstraint
+ (JNIEnv *, jobject, jlong, jlong, jlong, jlong);
+
+/*
+ * Class: satune_SatuneJavaAPI
+ * Method: solve
+ * Signature: (J)I
+ */
+JNIEXPORT jint JNICALL Java_satune_SatuneJavaAPI_solve
+ (JNIEnv *, jobject, jlong);
+
+/*
+ * Class: satune_SatuneJavaAPI
+ * Method: getElementValue
+ * Signature: (JJ)J
+ */
+JNIEXPORT jlong JNICALL Java_satune_SatuneJavaAPI_getElementValue
+ (JNIEnv *, jobject, jlong, jlong);
+
+/*
+ * Class: satune_SatuneJavaAPI
+ * Method: getBooleanValue
+ * Signature: (JJ)I
+ */
+JNIEXPORT jint JNICALL Java_satune_SatuneJavaAPI_getBooleanValue
+ (JNIEnv *, jobject, jlong, jlong);
+
+/*
+ * Class: satune_SatuneJavaAPI
+ * Method: getOrderConstraintValue
+ * Signature: (JJJJ)I
+ */
+JNIEXPORT jint JNICALL Java_satune_SatuneJavaAPI_getOrderConstraintValue
+ (JNIEnv *, jobject, jlong, jlong, jlong, jlong);
+
+/*
+ * Class: satune_SatuneJavaAPI
+ * Method: printConstraints
+ * Signature: (J)V
+ */
+JNIEXPORT void JNICALL Java_satune_SatuneJavaAPI_printConstraints
+ (JNIEnv *, jobject, jlong);
+
+/*
+ * Class: satune_SatuneJavaAPI
+ * Method: serialize
+ * Signature: (J)V
+ */
+JNIEXPORT void JNICALL Java_satune_SatuneJavaAPI_serialize
+ (JNIEnv *, jobject, jlong);
+
+/*
+ * Class: satune_SatuneJavaAPI
+ * Method: mustHaveValue
+ * Signature: (JJ)V
+ */
+JNIEXPORT void JNICALL Java_satune_SatuneJavaAPI_mustHaveValue
+ (JNIEnv *, jobject, jlong, jlong);
+
+/*
+ * Class: satune_SatuneJavaAPI
+ * Method: setInterpreter
+ * Signature: (JI)V
+ */
+JNIEXPORT void JNICALL Java_satune_SatuneJavaAPI_setInterpreter
+ (JNIEnv *, jobject, jlong, jint);
+
+/*
+ * Class: satune_SatuneJavaAPI
+ * Method: clone
+ * Signature: (J)J
+ */
+JNIEXPORT jlong JNICALL Java_satune_SatuneJavaAPI_clone
+ (JNIEnv *, jobject, jlong);
+
+#ifdef __cplusplus
+}
+#endif
+#endif
projects / satune.git / commitdiff