feat: subproject for z3 integration

4 files changed, 36 insertions, 0 deletions

diff --git a/gradle/libs.versions.toml b/gradle/libs.versions.toml
index 5f9dde6e..59d1ded5 100644
--- a/gradle/libs.versions.toml
+++ b/gradle/libs.versions.toml
@@ -41,6 +41,7 @@ mwe-utils = { group = "org.eclipse.emf", name = "org.eclipse.emf.mwe.utils", ver
 mwe2-launch = { group = "org.eclipse.emf", name = "org.eclipse.emf.mwe2.launch", version.ref = "mwe2" }
 mwe2-lib = { group = "org.eclipse.emf", name = "org.eclipse.emf.mwe2.lib", version.ref = "mwe2" }
 ortools = { group = "com.google.ortools", name = "ortools-java", version = "9.9.3963" }
+refinery-z3 = { group = "tools.refinery.z3", name = "refinery-z3-solver", version = "4.12.2" }
 slf4j-api = { group = "org.slf4j", name = "slf4j-api", version.ref = "slf4j" }
 slf4j-simple = { group = "org.slf4j", name = "slf4j-simple", version.ref = "slf4j" }
 slf4j-log4j = { group = "org.slf4j", name = "log4j-over-slf4j", version.ref = "slf4j" }
diff --git a/settings.gradle.kts b/settings.gradle.kts
index 11b188ea..6872b3b9 100644
--- a/settings.gradle.kts
+++ b/settings.gradle.kts
@@ -26,6 +26,7 @@ include(
                 "store-query-interpreter",
                 "store-reasoning",
                 "store-reasoning-scope",
+                "store-reasoning-smt",
 )
 
 for (project in rootProject.children) {
diff --git a/subprojects/store-reasoning-smt/build.gradle.kts b/subprojects/store-reasoning-smt/build.gradle.kts
new file mode 100644
index 00000000..4a784e42
--- /dev/null
+++ b/subprojects/store-reasoning-smt/build.gradle.kts
@@ -0,0 +1,15 @@
+/*
+ * SPDX-FileCopyrightText: 2021-2023 The Refinery Authors <https://refinery.tools/>
+ *
+ * SPDX-License-Identifier: EPL-2.0
+ */
+
+plugins {
+        id("tools.refinery.gradle.java-library")
+}
+
+dependencies {
+        api(project(":refinery-store-reasoning"))
+        implementation(libs.refinery.z3)
+        testImplementation(project(":refinery-store-query-interpreter"))
+}
diff --git a/subprojects/store-reasoning-smt/src/main/java/tools/refinery/store/reasoning/smt/SmtPropagator.java b/subprojects/store-reasoning-smt/src/main/java/tools/refinery/store/reasoning/smt/SmtPropagator.java
new file mode 100644
index 00000000..b63ab561
--- /dev/null
+++ b/subprojects/store-reasoning-smt/src/main/java/tools/refinery/store/reasoning/smt/SmtPropagator.java
@@ -0,0 +1,19 @@
+/*
+ * SPDX-FileCopyrightText: 2023 The Refinery Authors <https://refinery.tools/>
+ *
+ * SPDX-License-Identifier: EPL-2.0
+ */
+package tools.refinery.store.reasoning.smt;
+
+import com.microsoft.z3.Context;
+import tools.refinery.z3.Z3SolverLoader;
+
+public class SmtPropagator {
+        public void propagate() {
+                Z3SolverLoader.loadNativeLibraries();
+                try (var context = new Context()) {
+                        var solver = context.mkSolver();
+                        solver.check();
+                }
+        }
+}