From e79bd009c798a5bb7403338eb528209010616e02 Mon Sep 17 00:00:00 2001
From: Levente Bajczi <bajczilevi@gmail.com>
Date: Thu, 18 Jul 2024 01:07:54 +0200
Subject: [PATCH] Added tests

---
 subprojects/common/analysis/build.gradle.kts  |  1 +
 .../mit/theta/analysis/algorithm/HornTest.kt  | 56 +++++++++++++++++++
 2 files changed, 57 insertions(+)
 create mode 100644 subprojects/common/analysis/src/test/java/hu/bme/mit/theta/analysis/algorithm/HornTest.kt

diff --git a/subprojects/common/analysis/build.gradle.kts b/subprojects/common/analysis/build.gradle.kts
index b11621e1c0..f8205f008d 100644
--- a/subprojects/common/analysis/build.gradle.kts
+++ b/subprojects/common/analysis/build.gradle.kts
@@ -29,5 +29,6 @@ dependencies {
     implementation(project(":theta-graph-solver"))
     implementation(project(mapOf("path" to ":theta-solver-z3-legacy")))
     testImplementation(project(":theta-solver-z3-legacy"))
+    testImplementation(project(":theta-solver-z3"))
     implementation("com.corundumstudio.socketio:netty-socketio:2.0.6")
 }
diff --git a/subprojects/common/analysis/src/test/java/hu/bme/mit/theta/analysis/algorithm/HornTest.kt b/subprojects/common/analysis/src/test/java/hu/bme/mit/theta/analysis/algorithm/HornTest.kt
new file mode 100644
index 0000000000..89993cfc8e
--- /dev/null
+++ b/subprojects/common/analysis/src/test/java/hu/bme/mit/theta/analysis/algorithm/HornTest.kt
@@ -0,0 +1,56 @@
+/*
+ *  Copyright 2024 Budapest University of Technology and Economics
+ *
+ *  Licensed under the Apache License, Version 2.0 (the "License");
+ *  you may not use this file except in compliance with the License.
+ *  You may obtain a copy of the License at
+ *
+ *      http://www.apache.org/licenses/LICENSE-2.0
+ *
+ *  Unless required by applicable law or agreed to in writing, software
+ *  distributed under the License is distributed on an "AS IS" BASIS,
+ *  WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied.
+ *  See the License for the specific language governing permissions and
+ *  limitations under the License.
+ */
+
+package hu.bme.mit.theta.analysis.algorithm
+
+import hu.bme.mit.theta.analysis.algorithm.chc.HornChecker
+import hu.bme.mit.theta.common.logging.NullLogger
+import hu.bme.mit.theta.core.Relation
+import hu.bme.mit.theta.core.decl.Decls.Param
+import hu.bme.mit.theta.core.plus
+import hu.bme.mit.theta.core.type.inttype.IntExprs.*
+import hu.bme.mit.theta.solver.z3.Z3SolverFactory
+import org.junit.jupiter.api.Assertions
+import org.junit.jupiter.api.Test
+
+class HornTest {
+
+    @Test
+    fun testHornUnsafe() {
+        val inv = Relation("inv", Int())
+        val p0 = Param("P0", Int())
+        val p1 = Param("P1", Int())
+        inv(p0.ref) += Eq(p0.ref, Int(0))
+        inv(p1.ref) += inv(p0.ref).expr + Eq(p1.ref, Add(p0.ref, Int(1)))
+        !(inv(p0.ref) with Eq(p0.ref, Int(5)))
+
+        val checker = HornChecker(listOf(inv), Z3SolverFactory.getInstance(), NullLogger.getInstance())
+        Assertions.assertTrue(checker.check().isUnsafe)
+    }
+
+    @Test
+    fun testHornSafe() {
+        val inv = Relation("inv", Int())
+        val p0 = Param("P0", Int())
+        val p1 = Param("P1", Int())
+        inv(p0.ref) += Eq(p0.ref, Int(0))
+        inv(p1.ref) += inv(p0.ref).expr + Eq(p1.ref, Add(p0.ref, Int(2)))
+        !(inv(p0.ref) with Eq(p0.ref, Int(5)))
+
+        val checker = HornChecker(listOf(inv), Z3SolverFactory.getInstance(), NullLogger.getInstance())
+        Assertions.assertTrue(checker.check().isSafe)
+    }
+}
\ No newline at end of file