/* DO NOT EDIT THIS FILE - it is machine generated */
#include <jni.h>
#include "src/lglib.h"
#include "kodkod_engine_satlab_Lingeling.h"
#include <stdio.h>

/*
 * Class:     kodkod_engine_satlab_Lingeling
 * Method:    make
 * Signature: ()J
 */
JNIEXPORT jlong JNICALL Java_kodkod_engine_satlab_Lingeling_make
  (JNIEnv * env, jclass jc) {
	LGL* lgl = lglinit();
	return ((jlong) lgl);
}

/*
 * Class:     kodkod_engine_satlab_Lingeling
 * Method:    free
 * Signature: (J)V
 */
JNIEXPORT void JNICALL Java_kodkod_engine_satlab_Lingeling_free
  (JNIEnv * env, jobject obj, jlong lgl) {
	lglrelease((LGL*)lgl);
}

/*
 * Class:     kodkod_engine_satlab_Lingeling
 * Method:    addVariables
 * Signature: (JI)V
 */
JNIEXPORT void JNICALL Java_kodkod_engine_satlab_Lingeling_addVariables
  (JNIEnv * env, jobject obj, jlong lgl, jint nvars) {
	LGL* lglPtr = (LGL*)lgl;
	lgladd(lglPtr, nvars+1);
	lgladd(lglPtr, 0);
}

/*
 * Class:     kodkod_engine_satlab_Lingeling
 * Method:    addClause
 * Signature: (J[I)Z
 */
JNIEXPORT jboolean JNICALL Java_kodkod_engine_satlab_Lingeling_addClause
  (JNIEnv * env, jobject obj, jlong lgl, jintArray clause) {
	jsize length = (*env)->GetArrayLength(env, clause);
	jint* buf = (*env)->GetIntArrayElements(env, clause, JNI_FALSE);
	LGL* lglPtr = (LGL*)lgl;
	int i;
	for(i = 0; i < length; i++) {
		int lit = *(buf+i);
		lgladd (lglPtr, lit);
	}
	lgladd (lglPtr, 0);
	(*env)->ReleaseIntArrayElements(env, clause, buf, 0);
	return JNI_TRUE;
}

/*
 * Class:     kodkod_engine_satlab_Lingeling
 * Method:    solve
 * Signature: (J)Z
 */
JNIEXPORT jboolean JNICALL Java_kodkod_engine_satlab_Lingeling_solve
  (JNIEnv * env, jobject obj, jlong lgl) {
	LGL* lglPtr = (LGL*) lgl;
	return lglsat(lglPtr)==10;
}

/*
 * Class:     kodkod_engine_satlab_Lingeling
 * Method:    valueOf
 * Signature: (JI)Z
 */
JNIEXPORT jboolean JNICALL Java_kodkod_engine_satlab_Lingeling_valueOf
  (JNIEnv * env, jobject obj, jlong lgl, jint var) {
	return lglderef((LGL*)lgl, var) > 0;
}

