Fp support ( #23, #25 )

fp converter in z3, fp tests and fixes Partially add KFpRoundingMode back Transform KFpRoundingModeExpr into enum Basic fp operations Initial fp support
UnitTestBot · Sep 16, 2022 · de31bf7 · de31bf7
1 parent 484935a
commit de31bf7
Show file tree

Hide file tree

Showing 26 changed files with 3,645 additions and 115 deletions.
diff --git a/detekt.yml b/detekt.yml
@@ -594,7 +594,7 @@ style:
   RedundantVisibilityModifierRule:
     active: false
   ReturnCount:
-    active: true
+    active: false
     max: 2
     excludedFunctions: 'equals'
     excludeLabeled: false

diff --git a/ksmt-bitwuzla/src/main/kotlin/org/ksmt/solver/bitwuzla/KBitwuzlaExprInternalizer.kt b/ksmt-bitwuzla/src/main/kotlin/org/ksmt/solver/bitwuzla/KBitwuzlaExprInternalizer.kt
@@ -91,6 +91,8 @@ import org.ksmt.sort.KBv32Sort
 import org.ksmt.sort.KBv64Sort
 import org.ksmt.sort.KBv8Sort
 import org.ksmt.sort.KBvSort
+import org.ksmt.sort.KFpRoundingModeSort
+import org.ksmt.sort.KFpSort
 import org.ksmt.sort.KIntSort
 import org.ksmt.sort.KRealSort
 import org.ksmt.sort.KSort
@@ -587,6 +589,13 @@ open class KBitwuzlaExprInternalizer(
 
         override fun visit(sort: KUninterpretedSort): BitwuzlaSort =
             throw KSolverUnsupportedFeatureException("Unsupported sort $sort")
+
+        override fun <S : KFpSort> visit(sort: S): BitwuzlaSort =
+            TODO("We do not support KFP sort yet")
+
+        override fun visit(sort: KFpRoundingModeSort): BitwuzlaSort {
+            TODO("We do not support KFpRoundingModeSort yet")
+        }
     }
 
     open class FunctionSortInternalizer(

diff --git a/ksmt-core/src/main/kotlin/org/ksmt/KContext.kt b/ksmt-core/src/main/kotlin/org/ksmt/KContext.kt
diff --git a/ksmt-core/src/main/kotlin/org/ksmt/cache/Cache.kt b/ksmt-core/src/main/kotlin/org/ksmt/cache/Cache.kt
@@ -55,10 +55,23 @@ class Cache4<T, A0, A1, A2, A3>(val builder: (A0, A1, A2, A3) -> T) : AutoClosea
     }
 }
 
+class Cache5<T, A0, A1, A2, A3, A4>(val builder: (A0, A1, A2, A3, A4) -> T) : AutoCloseable {
+    private val cache = HashMap<List<*>, T>()
+
+    @Suppress("unused")
+    fun create(a0: A0, a1: A1, a2: A2, a3: A3, a4: A4): T =
+        cache.getOrPut(listOf(a0, a1, a2, a3, a4)) { builder(a0, a1, a2, a3, a4) }
+
+    override fun close() {
+        cache.clear()
+    }
+}
+
 fun <T> mkCache(builder: () -> T) = Cache0(builder)
 fun <T, A0> mkCache(builder: (A0) -> T) = Cache1(builder)
 fun <T, A0, A1> mkCache(builder: (A0, A1) -> T) = Cache2(builder)
 fun <T, A0, A1, A2> mkCache(builder: (A0, A1, A2) -> T) = Cache3(builder)
 
 @Suppress("unused")
 fun <T, A0, A1, A2, A3> mkCache(builder: (A0, A1, A2, A3) -> T) = Cache4(builder)
+fun <T, A0, A1, A2, A3, A4> mkCache(builder: (A0, A1, A2, A3, A4) -> T) = Cache5(builder)