Various fixes

* Fix timeout test * Fix convertation cache * Add libgmp to linux dependencies
UnitTestBot · Feb 4, 2023 · b56dfe8 · b56dfe8
1 parent 9201db5
commit b56dfe8
Show file tree

Hide file tree

Showing 3 changed files with 19 additions and 10 deletions.
diff --git a/ksmt-yices/dist/yices-native-linux-x86-64-0.0.zip b/ksmt-yices/dist/yices-native-linux-x86-64-0.0.zip
diff --git a/ksmt-yices/src/main/kotlin/org/ksmt/solver/yices/KYicesContext.kt b/ksmt-yices/src/main/kotlin/org/ksmt/solver/yices/KYicesContext.kt
@@ -4,7 +4,9 @@ import com.sri.yices.Terms
 import com.sri.yices.Types
 import com.sri.yices.Yices
 import org.ksmt.decl.KDecl
+import org.ksmt.expr.KConst
 import org.ksmt.expr.KExpr
+import org.ksmt.expr.KInterpretedValue
 import org.ksmt.sort.KSort
 import org.ksmt.utils.NativeLibraryLoader
 import org.ksmt.utils.uncheckedCast
@@ -33,11 +35,17 @@ open class KYicesContext : AutoCloseable {
 
     fun findConvertedDecl(decl: YicesTerm): KDecl<*>? = yicesDecls[decl]
 
-    fun <K: KExpr<*>> substituteDecls(expr: K, transform: (K) -> K): K =
+    fun <K : KExpr<*>> substituteDecls(expr: K, transform: (K) -> K): K =
         transformed.getOrPut(expr) { transform(expr) }.uncheckedCast()
 
     open fun internalizeExpr(expr: KExpr<*>, internalizer: (KExpr<*>) -> YicesTerm): YicesTerm =
-        internalize(expressions, yicesExpressions, expr, internalizer)
+        expressions.getOrPut(expr) {
+            internalizer(expr).also {
+                if (expr is KInterpretedValue<*> || expr is KConst<*>)
+                    yicesExpressions[it] = expr
+            }
+        }
+
 
     open fun internalizeSort(sort: KSort, internalizer: (KSort) -> YicesSort): YicesSort =
         internalize(sorts, yicesSorts, sort, internalizer)
@@ -227,13 +235,13 @@ open class KYicesContext : AutoCloseable {
             if (!Yices.isReady()) {
                 NativeLibraryLoader.load { os ->
                     when (os) {
-                        NativeLibraryLoader.OS.LINUX -> listOf("libyices", "libyices2java")
+                        NativeLibraryLoader.OS.LINUX -> listOf("libgmp-10", "libyices", "libyices2java")
                         NativeLibraryLoader.OS.WINDOWS -> listOf(
                             "libwinpthread-1", "libgcc_s_seh-1", "libstdc++-6",
                             "libgmp-10", "libyices", "libyices2java"
                         )
 
-                        else -> emptyList()
+                        NativeLibraryLoader.OS.MACOS -> TODO("Mac os platform is not supported")
                     }
                 }
                 Yices.init()

diff --git a/ksmt-yices/src/test/kotlin/org/ksmt/solver/yices/SolverTest.kt b/ksmt-yices/src/test/kotlin/org/ksmt/solver/yices/SolverTest.kt
@@ -105,26 +105,27 @@ class SolverTest {
         assertEquals(KSolverStatus.SAT, status)
     }
 
-    @Ignore
     @Test
     fun testTimeout(): Unit = with(ctx) {
         val solver = KYicesSolver(ctx)
-        val arrayBase by mkArraySort(mkBv32Sort(), mkBv8Sort())
-        val x by mkBv8Sort()
+        val arrayBase by mkArraySort(mkBv32Sort(), mkBv32Sort())
+        val x by mkBv32Sort()
 
         var array = arrayBase
         for (i in 0..1024) {
-            val v = mkBv((i xor 1024).toByte())
+            val v = mkBv((i xor 1024))
             array = array.store(mkBv(4198400 + i), v)
         }
 
         var xoredX = x
-        for (i in 0..3000) {
+        for (i in 0..1000) {
             val selectedValue = array.select(mkBv(4198500 + i))
             xoredX = mkBvXorExpr(xoredX, selectedValue)
+            xoredX = mkBvOrExpr(mkBvUnsignedDivExpr(xoredX, mkBv(3)), mkBvUnsignedRemExpr(xoredX, mkBv(3)))
         }
-        val someRandomValue = mkBv(42.toByte())
+        val someRandomValue = mkBv(42)
         val assertion = xoredX eq someRandomValue
+
         solver.assert(assertion)
 
         val status = solver.check(timeout = 1.milliseconds)