diff --git a/README.md b/README.md index 0e22100..b55dc32 100644 --- a/README.md +++ b/README.md @@ -1,2 +1,19 @@ # ratio4J -Java API for the oRatio solver + +Java API for the [oRatio](https://github.com/ratioSolver/oRatio) solver. + +## Installation + +Recursively clone this repository through `git clone --recurse-submodules https://github.com/ratioSolver/ratio4J`. + +Compile and install the native libraries. + +```shell +cd src/main/cpp +mkdir build +cd build +cmake .. +sudo make install +``` + +Go back at ratio4J level and compile the Java code using `mvn install`. diff --git a/pom.xml b/pom.xml index d2ca68b..e53953b 100644 --- a/pom.xml +++ b/pom.xml @@ -17,11 +17,6 @@ - - com.fasterxml.jackson.core - jackson-databind - 2.13.3 - org.junit.jupiter junit-jupiter diff --git a/src/main/cpp/CMakeLists.txt b/src/main/cpp/CMakeLists.txt index 8b9c1e3..a688aab 100644 --- a/src/main/cpp/CMakeLists.txt +++ b/src/main/cpp/CMakeLists.txt @@ -38,6 +38,7 @@ endif() install( TARGETS ${PROJECT_NAME} LIBRARY DESTINATION ${CMAKE_INSTALL_LIBDIR} + ARCHIVE DESTINATION ${CMAKE_INSTALL_LIBDIR} ) install( FILES ${RATIO_CORE_HEADERS} ${CMAKE_CURRENT_BINARY_DIR}/ratio4j_export.h diff --git a/src/main/cpp/extern/plexa b/src/main/cpp/extern/plexa index 3cedb39..c275d00 160000 --- a/src/main/cpp/extern/plexa +++ b/src/main/cpp/extern/plexa @@ -1 +1 @@ -Subproject commit 3cedb39b2b9602e10ba52c8f01afd05dd9266978 +Subproject commit c275d002df294a003db97e29b67e735d8bd595da diff --git a/src/main/cpp/include/it_cnr_istc_pst_oratio_TimelinesExecutor.h b/src/main/cpp/include/it_cnr_istc_pst_oratio_TimelinesExecutor.h index 78473b9..9095d9b 100644 --- a/src/main/cpp/include/it_cnr_istc_pst_oratio_TimelinesExecutor.h +++ b/src/main/cpp/include/it_cnr_istc_pst_oratio_TimelinesExecutor.h @@ -23,6 +23,54 @@ JNIEXPORT jlong JNICALL Java_it_cnr_istc_pst_oratio_TimelinesExecutor_new_1insta JNIEXPORT void JNICALL Java_it_cnr_istc_pst_oratio_TimelinesExecutor_dispose (JNIEnv *, jobject); +/* + * Class: it_cnr_istc_pst_oratio_TimelinesExecutor + * Method: adapt + * Signature: (Ljava/lang/String;)V + */ +JNIEXPORT void JNICALL Java_it_cnr_istc_pst_oratio_TimelinesExecutor_adapt__Ljava_lang_String_2 + (JNIEnv *, jobject, jstring); + +/* + * Class: it_cnr_istc_pst_oratio_TimelinesExecutor + * Method: adapt + * Signature: ([Ljava/lang/String;)V + */ +JNIEXPORT void JNICALL Java_it_cnr_istc_pst_oratio_TimelinesExecutor_adapt___3Ljava_lang_String_2 + (JNIEnv *, jobject, jobjectArray); + +/* + * Class: it_cnr_istc_pst_oratio_TimelinesExecutor + * Method: is_executing + * Signature: ()Z + */ +JNIEXPORT jboolean JNICALL Java_it_cnr_istc_pst_oratio_TimelinesExecutor_is_1executing + (JNIEnv *, jobject); + +/* + * Class: it_cnr_istc_pst_oratio_TimelinesExecutor + * Method: start_execution + * Signature: ()V + */ +JNIEXPORT void JNICALL Java_it_cnr_istc_pst_oratio_TimelinesExecutor_start_1execution + (JNIEnv *, jobject); + +/* + * Class: it_cnr_istc_pst_oratio_TimelinesExecutor + * Method: pause_execution + * Signature: ()V + */ +JNIEXPORT void JNICALL Java_it_cnr_istc_pst_oratio_TimelinesExecutor_pause_1execution + (JNIEnv *, jobject); + +/* + * Class: it_cnr_istc_pst_oratio_TimelinesExecutor + * Method: is_finished + * Signature: ()Z + */ +JNIEXPORT jboolean JNICALL Java_it_cnr_istc_pst_oratio_TimelinesExecutor_is_1finished + (JNIEnv *, jobject); + /* * Class: it_cnr_istc_pst_oratio_TimelinesExecutor * Method: tick diff --git a/src/main/cpp/src/it_cnr_istc_pst_oratio_TimelinesExecutor.cpp b/src/main/cpp/src/it_cnr_istc_pst_oratio_TimelinesExecutor.cpp index 37c3c41..1412667 100644 --- a/src/main/cpp/src/it_cnr_istc_pst_oratio_TimelinesExecutor.cpp +++ b/src/main/cpp/src/it_cnr_istc_pst_oratio_TimelinesExecutor.cpp @@ -29,6 +29,52 @@ JNIEXPORT void JNICALL Java_it_cnr_istc_pst_oratio_TimelinesExecutor_dispose(JNI env->SetLongField(obj, env->GetFieldID(env->GetObjectClass(obj), "native_handle", "J"), 0); } +JNIEXPORT void JNICALL Java_it_cnr_istc_pst_oratio_TimelinesExecutor_adapt__Ljava_lang_String_2(JNIEnv *env, jobject obj, jstring script) +{ + jboolean is_copy; + const char *utf_script = env->GetStringUTFChars(script, &is_copy); + try + { + get_executor(env, obj)->adapt(utf_script); + } + catch (const std::exception &e) + { + env->ThrowNew(env->FindClass("it/cnr/istc/pst/oratio/ExecutorException"), e.what()); + } + if (is_copy == JNI_TRUE) + env->ReleaseStringUTFChars(script, utf_script); +} + +JNIEXPORT void JNICALL Java_it_cnr_istc_pst_oratio_TimelinesExecutor_adapt___3Ljava_lang_String_2(JNIEnv *env, jobject obj, jobjectArray files) +{ + std::vector c_files; + for (jsize i = 0; i < env->GetArrayLength(files); ++i) + { + jboolean is_copy; + jstring c_file = reinterpret_cast(env->GetObjectArrayElement(files, i)); + const char *utf_file = env->GetStringUTFChars(c_file, &is_copy); + c_files.push_back(utf_file); + if (is_copy == JNI_TRUE) + env->ReleaseStringUTFChars(c_file, utf_file); + } + try + { + get_executor(env, obj)->adapt(c_files); + } + catch (const std::exception &e) + { + env->ThrowNew(env->FindClass("it/cnr/istc/pst/oratio/ExecutorException"), e.what()); + } +} + +JNIEXPORT jboolean JNICALL Java_it_cnr_istc_pst_oratio_TimelinesExecutor_is_1executing(JNIEnv *env, jobject obj) { return get_executor(env, obj)->is_executing(); } + +JNIEXPORT void JNICALL Java_it_cnr_istc_pst_oratio_TimelinesExecutor_start_1execution(JNIEnv *env, jobject obj) { get_executor(env, obj)->start_execution(); } + +JNIEXPORT void JNICALL Java_it_cnr_istc_pst_oratio_TimelinesExecutor_pause_1execution(JNIEnv *env, jobject obj) { get_executor(env, obj)->pause_execution(); } + +JNIEXPORT jboolean JNICALL Java_it_cnr_istc_pst_oratio_TimelinesExecutor_is_1finished(JNIEnv *env, jobject obj) { return get_executor(env, obj)->is_finished(); } + JNIEXPORT void JNICALL Java_it_cnr_istc_pst_oratio_TimelinesExecutor_tick(JNIEnv *env, jobject obj) { try diff --git a/src/main/java/it/cnr/istc/pst/oratio/Atom.java b/src/main/java/it/cnr/istc/pst/oratio/Atom.java index 9b9170d..4fb3be8 100644 --- a/src/main/java/it/cnr/istc/pst/oratio/Atom.java +++ b/src/main/java/it/cnr/istc/pst/oratio/Atom.java @@ -1,16 +1,8 @@ package it.cnr.istc.pst.oratio; -import java.io.IOException; -import java.util.Map; import java.util.stream.Collectors; import java.util.stream.Stream; -import com.fasterxml.jackson.core.JsonGenerator; -import com.fasterxml.jackson.databind.SerializerProvider; -import com.fasterxml.jackson.databind.annotation.JsonSerialize; -import com.fasterxml.jackson.databind.ser.std.StdSerializer; - -@JsonSerialize(using = Atom.AtomSerializer.class) public class Atom extends Item { private final long sigma; @@ -83,51 +75,4 @@ public String toString() { } }).collect(Collectors.joining(", ")) + ")"; } - - static class AtomSerializer extends StdSerializer { - - private AtomSerializer() { - super(Atom.class); - } - - @Override - public void serialize(final Atom value, final JsonGenerator gen, final SerializerProvider provider) - throws IOException { - gen.writeStartObject(); - gen.writeNumberField("sigma", value.sigma); - gen.writeStringField("predicate", value.type.name); - for (final Map.Entry expr : value.exprs.entrySet()) { - switch (expr.getValue().getType().getName()) { - case Solver.BOOL: - gen.writeBooleanField(expr.getKey(), - ((Item.BoolItem) expr.getValue()).getValue().booleanValue()); - break; - case Solver.INT: - case Solver.REAL: - case Solver.TP: - gen.writeNumberField(expr.getKey(), - ((Item.ArithItem) expr.getValue()).getValue().doubleValue()); - break; - case Solver.STRING: - gen.writeStringField(expr.getKey(), ((Item.StringItem) expr.getValue()).getValue()); - break; - default: - if (expr.getValue() instanceof EnumItem) { - if (((EnumItem) expr.getValue()).getVals().length == 1) - gen.writeStringField(expr.getKey(), - ((EnumItem) expr.getValue()).getVals()[0].getName()); - else { - gen.writeArrayFieldStart(expr.getKey()); - for (final Item val : ((EnumItem) expr.getValue()).getVals()) { - gen.writeString(val.getName()); - } - gen.writeEndArray(); - } - } else - gen.writeStringField(expr.getKey(), expr.getValue().getName()); - } - } - gen.writeEndObject(); - } - } } \ No newline at end of file diff --git a/src/main/java/it/cnr/istc/pst/oratio/Bound.java b/src/main/java/it/cnr/istc/pst/oratio/Bound.java index 41553da..8e53aa9 100644 --- a/src/main/java/it/cnr/istc/pst/oratio/Bound.java +++ b/src/main/java/it/cnr/istc/pst/oratio/Bound.java @@ -1,13 +1,5 @@ package it.cnr.istc.pst.oratio; -import java.io.IOException; - -import com.fasterxml.jackson.core.JsonGenerator; -import com.fasterxml.jackson.databind.SerializerProvider; -import com.fasterxml.jackson.databind.annotation.JsonSerialize; -import com.fasterxml.jackson.databind.ser.std.StdSerializer; - -@JsonSerialize(using = Bound.BoundSerializer.class) public class Bound { public static final int INF = Integer.MAX_VALUE / 2 - 1; @@ -27,21 +19,4 @@ public String toString() { final String c_max = max == INF ? "+inf" : Integer.toString(max); return "[" + c_min + ", " + c_max + "]"; } - - static class BoundSerializer extends StdSerializer { - - private BoundSerializer() { - super(Bound.class); - } - - @Override - public void serialize(Bound value, JsonGenerator gen, SerializerProvider provider) throws IOException { - gen.writeStartObject(); - if (value.min != -Bound.INF) - gen.writeNumberField("min", value.min); - if (value.max != Bound.INF) - gen.writeNumberField("max", value.max); - gen.writeEndObject(); - } - } } \ No newline at end of file diff --git a/src/main/java/it/cnr/istc/pst/oratio/Rational.java b/src/main/java/it/cnr/istc/pst/oratio/Rational.java index 1445223..f648fa0 100644 --- a/src/main/java/it/cnr/istc/pst/oratio/Rational.java +++ b/src/main/java/it/cnr/istc/pst/oratio/Rational.java @@ -1,13 +1,5 @@ package it.cnr.istc.pst.oratio; -import java.io.IOException; - -import com.fasterxml.jackson.core.JsonGenerator; -import com.fasterxml.jackson.databind.SerializerProvider; -import com.fasterxml.jackson.databind.annotation.JsonSerialize; -import com.fasterxml.jackson.databind.ser.std.StdSerializer; - -@JsonSerialize(using = Rational.RationalSerializer.class) public class Rational extends Number implements Comparable { private static final long serialVersionUID = 1L; @@ -490,19 +482,4 @@ private static long lcm(long u, long v) { } return u * (v / gcd(u, v)); } - - static class RationalSerializer extends StdSerializer { - - private RationalSerializer() { - super(Rational.class); - } - - @Override - public void serialize(Rational value, JsonGenerator gen, SerializerProvider provider) throws IOException { - gen.writeStartObject(); - gen.writeNumberField("num", value.getNumerator()); - gen.writeNumberField("den", value.getDenominator()); - gen.writeEndObject(); - } - } } \ No newline at end of file diff --git a/src/main/java/it/cnr/istc/pst/oratio/TimelinesExecutor.java b/src/main/java/it/cnr/istc/pst/oratio/TimelinesExecutor.java index 9ea8d2e..30de172 100644 --- a/src/main/java/it/cnr/istc/pst/oratio/TimelinesExecutor.java +++ b/src/main/java/it/cnr/istc/pst/oratio/TimelinesExecutor.java @@ -28,6 +28,18 @@ public TimelinesExecutor(final Solver solver, final Rational units_per_tick) { public native void dispose(); + public synchronized native void adapt(String script) throws SolverException; + + public synchronized native void adapt(String[] files) throws SolverException; + + public synchronized native boolean is_executing(); + + public synchronized native void start_execution(); + + public synchronized native void pause_execution(); + + public synchronized native boolean is_finished(); + public synchronized native void tick() throws ExecutorException; public void dontStartYet(Set atoms) throws ExecutorException {