From ee4d70af73bc9e5cc40378814b226e6c9970f42e Mon Sep 17 00:00:00 2001 From: Konstantin Chukharev Date: Thu, 26 Nov 2020 18:13:45 +0300 Subject: [PATCH 1/3] (WIP) Add jni wrapper for splr solver (in Rust) --- .gitignore | 1 + kotlin-satlib-jni/Cargo.lock | 198 ++++++++++++++++++ kotlin-satlib-jni/Cargo.toml | 18 ++ kotlin-satlib-jni/build.gradle.kts | 22 ++ .../github/lipen/satlib/solver/jni/JSplr.kt | 156 ++++++++++++++ kotlin-satlib-jni/src/main/rust/JSplr.rs | 168 +++++++++++++++ 6 files changed, 563 insertions(+) create mode 100644 kotlin-satlib-jni/Cargo.lock create mode 100644 kotlin-satlib-jni/Cargo.toml create mode 100644 kotlin-satlib-jni/src/main/kotlin/com/github/lipen/satlib/solver/jni/JSplr.kt create mode 100644 kotlin-satlib-jni/src/main/rust/JSplr.rs diff --git a/.gitignore b/.gitignore index a26bf0a..d38fc95 100644 --- a/.gitignore +++ b/.gitignore @@ -5,6 +5,7 @@ # Build folders out/ build/ +target/ # Images *.png diff --git a/kotlin-satlib-jni/Cargo.lock b/kotlin-satlib-jni/Cargo.lock new file mode 100644 index 0000000..d0774fd --- /dev/null +++ b/kotlin-satlib-jni/Cargo.lock @@ -0,0 +1,198 @@ +# This file is automatically @generated by Cargo. +# It is not intended for manual editing. +[[package]] +name = "bitflags" +version = "1.2.1" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "cf1de2fe8c75bc145a2f577add951f8134889b4795d47466a54a5c846d691693" + +[[package]] +name = "bytes" +version = "0.5.6" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "0e4cec68f03f32e44924783795810fa50a7035d8c8ebe78580ad7e6c703fba38" + +[[package]] +name = "cesu8" +version = "1.1.0" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "6d43a04d8753f35258c91f8ec639f792891f748a1edbd759cf1dcea3382ad83c" + +[[package]] +name = "cfg-if" +version = "0.1.10" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "4785bdd1c96b2a846b2bd7cc02e86b6b3dbf14e7e53446c4f54c92a361040822" + +[[package]] +name = "combine" +version = "4.4.0" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "b9417a0c314565e2abffaece67e95a8cb51f9238cd39f3764d9dfdf09e72b20c" +dependencies = [ + "bytes", + "memchr", + "pin-project-lite", +] + +[[package]] +name = "jni" +version = "0.18.0" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "24967112a1e4301ca5342ea339763613a37592b8a6ce6cf2e4494537c7a42faf" +dependencies = [ + "cesu8", + "combine", + "jni-sys", + "log", + "thiserror", + "walkdir", +] + +[[package]] +name = "jni-sys" +version = "0.3.0" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "8eaf4bc02d17cbdd7ff4c7438cafcdf7fb9a4613313ad11b4f8fefe7d3fa0130" + +[[package]] +name = "kotlin-satlib-jni-splr" +version = "0.1.0" +dependencies = [ + "jni", + "splr", +] + +[[package]] +name = "log" +version = "0.4.11" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "4fabed175da42fed1fa0746b0ea71f412aa9d35e76e95e59b192c64b9dc2bf8b" +dependencies = [ + "cfg-if", +] + +[[package]] +name = "memchr" +version = "2.3.4" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "0ee1c47aaa256ecabcaea351eae4a9b01ef39ed810004e298d2511ed284b1525" + +[[package]] +name = "pin-project-lite" +version = "0.1.11" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "c917123afa01924fc84bb20c4c03f004d9c38e5127e3c039bbf7f4b9c76a2f6b" + +[[package]] +name = "proc-macro2" +version = "1.0.24" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "1e0704ee1a7e00d7bb417d0770ea303c1bccbabf0ef1667dae92b5967f5f8a71" +dependencies = [ + "unicode-xid", +] + +[[package]] +name = "quote" +version = "1.0.7" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "aa563d17ecb180e500da1cfd2b028310ac758de548efdd203e18f283af693f37" +dependencies = [ + "proc-macro2", +] + +[[package]] +name = "same-file" +version = "1.0.6" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "93fc1dc3aaa9bfed95e02e6eadabb4baf7e3078b0bd1b4d7b6b0b68378900502" +dependencies = [ + "winapi-util", +] + +[[package]] +name = "splr" +version = "0.5.0" +dependencies = [ + "bitflags", +] + +[[package]] +name = "syn" +version = "1.0.51" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "3b4f34193997d92804d359ed09953e25d5138df6bcc055a71bf68ee89fdf9223" +dependencies = [ + "proc-macro2", + "quote", + "unicode-xid", +] + +[[package]] +name = "thiserror" +version = "1.0.22" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "0e9ae34b84616eedaaf1e9dd6026dbe00dcafa92aa0c8077cb69df1fcfe5e53e" +dependencies = [ + "thiserror-impl", +] + +[[package]] +name = "thiserror-impl" +version = "1.0.22" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "9ba20f23e85b10754cd195504aebf6a27e2e6cbe28c17778a0c930724628dd56" +dependencies = [ + "proc-macro2", + "quote", + "syn", +] + +[[package]] +name = "unicode-xid" +version = "0.2.1" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "f7fe0bb3479651439c9112f72b6c505038574c9fbb575ed1bf3b797fa39dd564" + +[[package]] +name = "walkdir" +version = "2.3.1" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "777182bc735b6424e1a57516d35ed72cb8019d85c8c9bf536dccb3445c1a2f7d" +dependencies = [ + "same-file", + "winapi", + "winapi-util", +] + +[[package]] +name = "winapi" +version = "0.3.9" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "5c839a674fcd7a98952e593242ea400abe93992746761e38641405d28b00f419" +dependencies = [ + "winapi-i686-pc-windows-gnu", + "winapi-x86_64-pc-windows-gnu", +] + +[[package]] +name = "winapi-i686-pc-windows-gnu" +version = "0.4.0" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "ac3b87c63620426dd9b991e5ce0329eff545bccbbb34f3be09ff6fb6ab51b7b6" + +[[package]] +name = "winapi-util" +version = "0.1.5" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "70ec6ce85bb158151cae5e5c87f95a8e97d2c0c4b001223f33a334e3ce5de178" +dependencies = [ + "winapi", +] + +[[package]] +name = "winapi-x86_64-pc-windows-gnu" +version = "0.4.0" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "712e227841d057c1ee1cd2fb22fa7e5a5461ae8e48fa2ca79ec42cfc1931183f" diff --git a/kotlin-satlib-jni/Cargo.toml b/kotlin-satlib-jni/Cargo.toml new file mode 100644 index 0000000..b474bae --- /dev/null +++ b/kotlin-satlib-jni/Cargo.toml @@ -0,0 +1,18 @@ +[package] +name = "kotlin-satlib-jni-splr" +version = "0.1.0" +authors = ["Konstantin Chukharev "] + +[lib] +name = "jsplr" +path = "src/main/rust/JSplr.rs" +crate-type = ["cdylib"] + +[dependencies] +jni = "0.18" + +[dependencies.splr] +#version = "0.5.0" +path = "D:/dev/Rust/splr" +default-features = false +features = ["incremental_solver"] diff --git a/kotlin-satlib-jni/build.gradle.kts b/kotlin-satlib-jni/build.gradle.kts index e23ae5f..dfb1837 100644 --- a/kotlin-satlib-jni/build.gradle.kts +++ b/kotlin-satlib-jni/build.gradle.kts @@ -1,5 +1,8 @@ +import io.github.liurenjie1024.gradle.rust.CargoBuildTask + plugins { id(Plugins.Jmh.id) + id("io.github.liurenjie1024.gradle.rust") version "0.1.0" } dependencies { @@ -12,3 +15,22 @@ jmh { resultsFile = project.file("${project.buildDir}/reports/jmh/results.json") resultFormat = "JSON" } + +tasks.withType(CargoBuildTask::class.java).configureEach { + // verbose = true + release = true +} + +tasks.register("copyRustLibDllToResources") { + doLast { + val libName = "jsplr.dll" + val src = projectDir.resolve("target/release").resolve(libName) + val dest = projectDir.resolve("src/main/resources/lib/win64").resolve(libName) + if (dest.exists()) { + dest.delete() + } + println("Copying $src to $dest...") + src.copyTo(dest, overwrite = true) + println("Done copying rust lib dll.") + } +} diff --git a/kotlin-satlib-jni/src/main/kotlin/com/github/lipen/satlib/solver/jni/JSplr.kt b/kotlin-satlib-jni/src/main/kotlin/com/github/lipen/satlib/solver/jni/JSplr.kt new file mode 100644 index 0000000..02bb16b --- /dev/null +++ b/kotlin-satlib-jni/src/main/kotlin/com/github/lipen/satlib/solver/jni/JSplr.kt @@ -0,0 +1,156 @@ +/** + * © 2020 Konstantin Chukharev, ITMO University + */ + +package com.github.lipen.satlib.solver.jni + +import com.github.lipen.satlib.utils.useWith + +@Suppress("FunctionName", "MemberVisibilityCanBePrivate") +class JSplr : AutoCloseable { + private var handle: Long = 0 + private var solvable: Boolean = false + + var numberOfVariables: Int = 0 + private set + var numberOfClauses: Int = 0 + private set + var model: IntArray? = null + private set + + @Suppress("PropertyName") + val _numberOfVariablesInternal: Int + get() = splr_nvars(handle) + + init { + reset() + } + + fun reset() { + if (handle != 0L) splr_delete(handle) + handle = splr_create() + if (handle == 0L) error("splr_create returned 0-pointer") + solvable = true + numberOfVariables = 0 + numberOfClauses = 0 + } + + override fun close() { + if (handle != 0L) { + splr_delete(handle) + handle = 0 + } + } + + fun hello() { + splr_hello() + } + + fun newVariable(): Int { + return splr_new_var(handle) + .also { numberOfVariables = it } + .also { println("newVariable() -> $it") } + } + + fun addClause(lit1: Int): Boolean { + ++numberOfClauses + if (!splr_add_clause(handle, lit1)) solvable = false + return solvable + } + + fun addClause(lit1: Int, lit2: Int): Boolean { + ++numberOfClauses + if (!splr_add_clause(handle, lit1, lit2)) { + solvable = false + } + return solvable + } + + fun addClause(lit1: Int, lit2: Int, lit3: Int): Boolean { + ++numberOfClauses + if (!splr_add_clause(handle, lit1, lit2, lit3)) solvable = false + return solvable + } + + fun addClause(vararg literals: Int): Boolean { + return addClause_(literals) + } + + fun addClause_(literals: IntArray): Boolean { + ++numberOfClauses + if (!splr_add_clause(handle, literals)) solvable = false + return solvable + } + + fun solve(): Boolean { + model = if (!solvable) { + null + } else { + splr_solve(handle) + } + solvable = model != null + return solvable + } + + private external fun splr_hello() + private external fun splr_create(): Long + private external fun splr_delete(handle: Long) + private external fun splr_new_var(handle: Long): Int + private external fun splr_nvars(handle: Long): Int + private external fun splr_add_clause(handle: Long): Boolean + private external fun splr_add_clause(handle: Long, lit: Int): Boolean + private external fun splr_add_clause(handle: Long, lit1: Int, lit2: Int): Boolean + private external fun splr_add_clause(handle: Long, lit1: Int, lit2: Int, lit3: Int): Boolean + private external fun splr_add_clause(handle: Long, literals: IntArray): Boolean + private external fun splr_solve(handle: Long): IntArray + + companion object { + init { + Loader.load("jsplr") + } + } +} + +fun main() { + JSplr + + val timeStart = System.currentTimeMillis() + + @Suppress("DuplicatedCode") + JSplr().useWith { + hello() + + val x = newVariable() + val y = newVariable() + val z = newVariable() + + println("Encoding exactlyOne({x, y, z})") + addClause(-x, -y) + addClause(-x, -z) + addClause(-y, -z) + addClause(x, y, z) + + println("nVars = $numberOfVariables, nClauses = $numberOfClauses") + println("Solving...") + check(solve()) { "Unexpected UNSAT" } + println("model = ${model!!.asList()}") + // println("x = ${getValue(x)}, y = ${getValue(y)}, z = ${getValue(z)}") + // println("model = ${getModel().drop(1)}") + + println("Adding unit-clause [${-x}]") + addClause(-x) + check(solve()) { "Unexpected UNSAT" } + println("model = ${model!!.asList()}") + + println("Adding unit-clause [${-y}]") + addClause(-y) + check(solve()) { "Unexpected UNSAT" } + println("model = ${model!!.asList()}") + + println("Adding unit-clause [${-z}]") + addClause(-z) + check(!solve()) { "Unexpected SAT with model = ${model!!.asList()}" } + } + + println("\nAll done in %.2f s.".format((System.currentTimeMillis() - timeStart) / 1000f)) +} diff --git a/kotlin-satlib-jni/src/main/rust/JSplr.rs b/kotlin-satlib-jni/src/main/rust/JSplr.rs new file mode 100644 index 0000000..f50335b --- /dev/null +++ b/kotlin-satlib-jni/src/main/rust/JSplr.rs @@ -0,0 +1,168 @@ +extern crate jni; +extern crate splr; + +use std::convert::TryFrom; + +use jni::JNIEnv; +use jni::objects::{JObject, ReleaseMode}; +use jni::sys::{jboolean, jint, jintArray, jlong, jsize}; +use splr::*; +use splr::types::*; + +fn encode(solver: Solver) -> jlong { + Box::into_raw(Box::new(solver)) as jlong +} + +fn decode(solver_ptr: jlong) -> &'static mut Solver { + unsafe { &mut *(solver_ptr as *mut Solver) } +} + +#[no_mangle] +pub extern "system" +fn Java_com_github_lipen_satlib_solver_jni_JSplr_splr_1hello( + _env: JNIEnv, + _object: JObject, +) { + println!("Hello from Rust!"); + + let v: Vec> = vec![vec![1, 2], vec![-1, 3], vec![1, -3], vec![-1, 2]]; + for (i, v) in Solver::try_from((Config::default(), v.as_ref())).expect("panic").iter().enumerate() { + println!("{}-th answer: {:?}", i, v); + } + + let cnf = CNFDescription { + num_of_variables: 4, + ..CNFDescription::default() + }; + let mut s = Solver::instantiate(&Config::default(), &cnf); + s.add_clause(vec![1, 2]).unwrap(); + s.add_clause(vec![-2]).unwrap(); + s.inject_assignment(&[-1i32]); + println!("{:?}", s.validate()); + + println!("OK"); +} + +#[no_mangle] +pub extern "system" fn Java_com_github_lipen_satlib_solver_jni_JSplr_splr_1create( + _env: JNIEnv, + _object: JObject, +) -> jlong { + // let solver = Solver::default(); + let solver = Solver::instantiate(&Config::default(), &CNFDescription::default()); + encode(solver) +} + +#[no_mangle] +pub extern "system" fn Java_com_github_lipen_satlib_solver_jni_JSplr_splr_1delete( + _env: JNIEnv, + _object: JObject, + solver_ptr: jlong, +) { + let _boxed_solver = unsafe { Box::from_raw(solver_ptr as *mut Solver) }; + // Let this boxed solver drop. +} + +#[no_mangle] +pub extern "system" fn Java_com_github_lipen_satlib_solver_jni_JSplr_splr_1new_1var( + _env: JNIEnv, + _object: JObject, + solver_ptr: jlong, +) -> jint { + let solver = decode(solver_ptr); + solver.add_var() as jint +} + +#[no_mangle] +pub extern "system" fn Java_com_github_lipen_satlib_solver_jni_JSplr_splr_1nvars( + _env: JNIEnv, + _object: JObject, + solver_ptr: jlong, +) -> jint { + let solver = decode(solver_ptr); + solver.asg.num_vars as jint +} + +// #[no_mangle] +// pub extern "system" fn Java_com_github_lipen_satlib_solver_jni_JSplr_splr_1add_1clause__J( +// _env: JNIEnv, +// _object: JObject, +// solver_ptr: jlong, +// ) -> jboolean { +// let solver = decode(solver_ptr); +// solver.add_clause(vec![]).is_ok() as jboolean +// } + +#[no_mangle] +pub extern "system" fn Java_com_github_lipen_satlib_solver_jni_JSplr_splr_1add_1clause__JI( + _env: JNIEnv, + _object: JObject, + solver_ptr: jlong, + lit: jint, +) -> jboolean { + let solver = decode(solver_ptr); + // solver.add_clause(vec![lit]).is_ok() as jboolean + solver.add_assignment(lit).is_ok() as jboolean +} + +#[no_mangle] +pub extern "system" fn Java_com_github_lipen_satlib_solver_jni_JSplr_splr_1add_1clause__JII( + _env: JNIEnv, + _object: JObject, + solver_ptr: jlong, + lit1: jint, + lit2: jint, +) -> jboolean { + let solver = decode(solver_ptr); + solver.add_clause(vec![lit1, lit2]).is_ok() as jboolean +} + +#[no_mangle] +pub extern "system" fn Java_com_github_lipen_satlib_solver_jni_JSplr_splr_1add_1clause__JIII( + _env: JNIEnv, + _object: JObject, + solver_ptr: jlong, + lit1: jint, + lit2: jint, + lit3: jint, +) -> jboolean { + let solver = decode(solver_ptr); + solver.add_clause(vec![lit1, lit2, lit3]).is_ok() as jboolean +} + +#[no_mangle] +pub extern "system" fn Java_com_github_lipen_satlib_solver_jni_JSplr_splr_1add_1clause__J_3I( + env: JNIEnv, + _object: JObject, + solver_ptr: jlong, + literals: jintArray, +) -> jboolean { + let solver = decode(solver_ptr); + let len = env.get_array_length(literals).unwrap() as usize; + let ptr = env + .get_auto_primitive_array_critical(literals, ReleaseMode::CopyBack) + .unwrap() + .as_ptr(); + let vec = unsafe { Vec::from_raw_parts(ptr as *mut jint, len, len) }; + let res = solver.add_clause(&vec); + std::mem::forget(vec); + res.is_ok() as jboolean +} + +#[no_mangle] +pub extern "system" fn Java_com_github_lipen_satlib_solver_jni_JSplr_splr_1solve( + env: JNIEnv, + _object: JObject, + solver_ptr: jlong, +) -> jintArray { + let solver = decode(solver_ptr); + solver.reset(); + if let Ok(Certificate::SAT(model)) = solver.solve() { + let len = model.len() as jsize; + let output = env.new_int_array(len).unwrap(); + env.set_int_array_region(output, 0, &model).unwrap(); + output + } else { + *JObject::null() + } +} From de137085d64e9fb14006526ac46ba5ea1751c45b Mon Sep 17 00:00:00 2001 From: Konstantin Chukharev Date: Thu, 26 Nov 2020 18:38:45 +0300 Subject: [PATCH 2/3] Fix Rust Gradle plugin config --- build.gradle.kts | 1 + buildSrc/src/main/kotlin/Dependencies.kt | 7 +++++++ kotlin-satlib-jni/build.gradle.kts | 2 +- 3 files changed, 9 insertions(+), 1 deletion(-) diff --git a/build.gradle.kts b/build.gradle.kts index bef9e25..0a6e522 100644 --- a/build.gradle.kts +++ b/build.gradle.kts @@ -12,6 +12,7 @@ plugins { with(Plugins.GradleVersions) { id(id) version (version) } with(Plugins.Shadow) { id(id) version (version) } with(Plugins.Jmh) { id(id) version (version) apply false } + with(Plugins.Rust) { id(id) version (version) apply false } `maven-publish` } diff --git a/buildSrc/src/main/kotlin/Dependencies.kt b/buildSrc/src/main/kotlin/Dependencies.kt index a6f272d..a99114e 100644 --- a/buildSrc/src/main/kotlin/Dependencies.kt +++ b/buildSrc/src/main/kotlin/Dependencies.kt @@ -16,6 +16,7 @@ object Versions { const val multiarray = "0.6.1" const val okio = "2.9.0" const val shadow = "5.2.0" + const val rust_gradle_plugin = "0.1.0" } object Libs { @@ -100,4 +101,10 @@ object Plugins { const val version = Versions.jmh_gradle_plugin const val id = "me.champeau.gradle.jmh" } + + // https://github.com/liurenjie1024/rust-gradle-plugin + object Rust { + const val version = Versions.rust_gradle_plugin + const val id = "io.github.liurenjie1024.gradle.rust" + } } diff --git a/kotlin-satlib-jni/build.gradle.kts b/kotlin-satlib-jni/build.gradle.kts index dfb1837..a9f0913 100644 --- a/kotlin-satlib-jni/build.gradle.kts +++ b/kotlin-satlib-jni/build.gradle.kts @@ -2,7 +2,7 @@ import io.github.liurenjie1024.gradle.rust.CargoBuildTask plugins { id(Plugins.Jmh.id) - id("io.github.liurenjie1024.gradle.rust") version "0.1.0" + id(Plugins.Rust.id) } dependencies { From 8317422243933a4472df4d10c2a001f0c686d513 Mon Sep 17 00:00:00 2001 From: Konstantin Chukharev Date: Thu, 26 Nov 2020 18:55:56 +0300 Subject: [PATCH 3/3] Exclude cargo tasks from CI cmd --- .github/workflows/build-windows.yml | 2 +- .github/workflows/build.yml | 2 +- 2 files changed, 2 insertions(+), 2 deletions(-) diff --git a/.github/workflows/build-windows.yml b/.github/workflows/build-windows.yml index c22f715..a29b867 100644 --- a/.github/workflows/build-windows.yml +++ b/.github/workflows/build-windows.yml @@ -64,7 +64,7 @@ jobs: g++ -Wall -O3 -fPIC -shared -s -I${JAVA_HOME}/include -I${JAVA_HOME}/include/win32 -Ibuild/headers -Iglucose-src -I. -Lglucose-src/build src/main/cpp/JGlucose.cpp -lglucose -o build/lib/jglucose.dll - name: Build package using Gradle wrapper - run: ./gradlew build -x test --stacktrace + run: ./gradlew build -x test --stacktrace -x :jni:cargoBuild -x :jni:cargoTest -x :jni:cargoClean - name: Upload to GH Releases uses: softprops/action-gh-release@v1 diff --git a/.github/workflows/build.yml b/.github/workflows/build.yml index 7b36103..00e6834 100644 --- a/.github/workflows/build.yml +++ b/.github/workflows/build.yml @@ -55,7 +55,7 @@ jobs: run: echo "$(realpath bin/)" >> $GITHUB_PATH - name: Build package using Gradle wrapper - run: ./gradlew build --stacktrace --scan + run: ./gradlew build --stacktrace --scan -x :jni:cargoBuild -x :jni:cargoTest -x :jni:cargoClean - name: Upload to GH Releases uses: softprops/action-gh-release@v1