From bc1be69d88600d87df55d84f4591292d4c7656c1 Mon Sep 17 00:00:00 2001 From: Kristóf Marussy Date: Fri, 1 Dec 2023 19:19:12 +0100 Subject: feat: subproject for z3 integration --- subprojects/store-reasoning-smt/build.gradle.kts | 15 +++++++++++++++ .../refinery/store/reasoning/smt/SmtPropagator.java | 19 +++++++++++++++++++ 2 files changed, 34 insertions(+) create mode 100644 subprojects/store-reasoning-smt/build.gradle.kts create mode 100644 subprojects/store-reasoning-smt/src/main/java/tools/refinery/store/reasoning/smt/SmtPropagator.java (limited to 'subprojects') 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 + * + * 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 + * + * 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(); + } + } +} -- cgit v1.2.3-70-g09d2