From 8b388ff57c3f67969f4d9864f3b02087feb8554a Mon Sep 17 00:00:00 2001
From: Levente Bajczi <bajczilevi@gmail.com>
Date: Mon, 4 Nov 2024 21:28:45 +0100
Subject: [PATCH] Fixed horn problems

---
 .../java/hu/bme/mit/theta/core/ChcUtils.kt    | 20 ++++++++++++-------
 .../mit/theta/xcfa/cli/XcfaCliVerifyTest.kt   |  2 --
 2 files changed, 13 insertions(+), 9 deletions(-)

diff --git a/subprojects/common/core/src/main/java/hu/bme/mit/theta/core/ChcUtils.kt b/subprojects/common/core/src/main/java/hu/bme/mit/theta/core/ChcUtils.kt
index b2a9ca4006..efd0e2917d 100644
--- a/subprojects/common/core/src/main/java/hu/bme/mit/theta/core/ChcUtils.kt
+++ b/subprojects/common/core/src/main/java/hu/bme/mit/theta/core/ChcUtils.kt
@@ -25,6 +25,7 @@ import hu.bme.mit.theta.core.type.booltype.BoolExprs.*
 import hu.bme.mit.theta.core.type.booltype.BoolType
 import hu.bme.mit.theta.core.type.functype.FuncExprs
 import hu.bme.mit.theta.core.type.functype.FuncType
+import hu.bme.mit.theta.core.type.inttype.IntExprs.Int
 import hu.bme.mit.theta.core.utils.ExprUtils
 import java.util.*
 
@@ -55,8 +56,7 @@ open class Relation(val name: String, vararg paramTypes: Type) {
 
   val arity: Int = paramTypes.size
   val rules: MutableList<Rule> = LinkedList()
-  val constDecl =
-    if (arity == 0) Const(name, Bool()) else Const(name, funcType(paramTypes.toList(), Bool()))
+  val constDecl = Const(name, funcType(paramTypes.toList(), Bool()))
 
   open operator fun invoke(params: List<Expr<*>>) = RelationApp(this, params)
 
@@ -114,11 +114,17 @@ data class RelationApp(
 
 data class Rule(val head: Expr<BoolType>, val constraints: List<Expr<BoolType>>) {
 
-  fun toExpr() =
-    Forall(
-      ExprUtils.getParams(head) + ExprUtils.getParams(constraints),
-      Imply(And(constraints), head),
-    )
+  fun toExpr(): Expr<BoolType> {
+    val params = ExprUtils.getParams(head) + ExprUtils.getParams(constraints)
+    val nontrivialConstraints = constraints.filter { it != True() }
+    return if (params.isNotEmpty()) {
+      Forall(params, Imply(And(nontrivialConstraints), head))
+    } else if (nontrivialConstraints.isNotEmpty()) {
+      Forall(listOf(Param("__dummy__", Int())), Imply(And(nontrivialConstraints), head))
+    } else {
+      head
+    }
+  }
 }
 
 operator fun Expr<BoolType>.plus(other: Expr<BoolType>) = listOf(this, other)
diff --git a/subprojects/xcfa/xcfa-cli/src/test/java/hu/bme/mit/theta/xcfa/cli/XcfaCliVerifyTest.kt b/subprojects/xcfa/xcfa-cli/src/test/java/hu/bme/mit/theta/xcfa/cli/XcfaCliVerifyTest.kt
index 198817117f..084cbdbd98 100644
--- a/subprojects/xcfa/xcfa-cli/src/test/java/hu/bme/mit/theta/xcfa/cli/XcfaCliVerifyTest.kt
+++ b/subprojects/xcfa/xcfa-cli/src/test/java/hu/bme/mit/theta/xcfa/cli/XcfaCliVerifyTest.kt
@@ -128,10 +128,8 @@ class XcfaCliVerifyTest {
     @JvmStatic
     fun cFilesShortInt(): Stream<Arguments> {
       return Stream.of(
-        Arguments.of("/c/litmustest/singlethread/00assignment.c", null),
         Arguments.of("/c/litmustest/singlethread/01cast.c", null),
         Arguments.of("/c/litmustest/singlethread/02types.c", null),
-        Arguments.of("/c/litmustest/singlethread/15addition.c", null),
         Arguments.of("/c/litmustest/singlethread/20testinline.c", null),
         Arguments.of("/c/litmustest/singlethread/21namecollision.c", null),
         Arguments.of("/c/litmustest/singlethread/22nondet.c", null),