Pre-release refactorings

Use unmodifiable set wrapper instead of copy

Upgrade gradle, kotlin and z3 versions

Replace all uses of mutableSet/Map with hashSet/Map

Refactorings

BaseTransformer without default method implementations

buildSrc/src/main/kotlin/Properties.kt

@@ -1,7 +1,9 @@
 import org.gradle.api.Project
 
 fun Project.booleanProperty(name: String): Boolean? {
-    if (!project.hasProperty(name)) return null
-    val value = project.property(name)
-    return value?.toString()?.toBoolean()
+    if (!project.hasProperty(name)) {
+        return null
+    }
+
+    return project.property(name)?.toString()?.toBoolean()
 }

buildSrc/src/main/kotlin/Publications.kt

@@ -4,11 +4,12 @@ import org.gradle.api.component.SoftwareComponent
 import org.gradle.kotlin.dsl.get
 
 fun Project.removeTestFixtures(softwareComponent: SoftwareComponent) {
-    val componenet = softwareComponent as AdhocComponentWithVariants
-    componenet.withVariantsFromConfiguration(configurations["testFixturesApiElements"]) {
-        skip()
-    }
-    componenet.withVariantsFromConfiguration(configurations["testFixturesRuntimeElements"]) {
-        skip()
+    with(softwareComponent as AdhocComponentWithVariants) {
+        withVariantsFromConfiguration(configurations["testFixturesApiElements"]) {
+            skip()
+        }
+        withVariantsFromConfiguration(configurations["testFixturesRuntimeElements"]) {
+            skip()
+        }
     }
 }

buildSrc/src/main/kotlin/SmtLibBenchmarkUtil.kt

@@ -9,11 +9,12 @@ fun Project.mkSmtLibBenchmarkTestData(name: String) = tasks.register("smtLibBenc
     doLast {
         val path = buildDir.resolve("smtLibBenchmark/$name")
         val downloadTarget = path.resolve("$name.zip")
-        val repoUrl = "https://clc-gitlab.cs.uiowa.edu:2443"
-        val url = "$repoUrl/api/v4/projects/SMT-LIB-benchmarks%2F$name/repository/archive.zip"
+        val url = "$BENCHMARK_REPO_URL/api/v4/projects/SMT-LIB-benchmarks%2F$name/repository/archive.zip"
+
         download(url, downloadTarget)
 
         val unpackCompleteMarker = path.resolve("unpack-complete")
+
         if (!unpackCompleteMarker.exists()) {
             copy {
                 from(zipTree(downloadTarget))
@@ -23,10 +24,10 @@ fun Project.mkSmtLibBenchmarkTestData(name: String) = tasks.register("smtLibBenc
             unpackCompleteMarker.createNewFile()
         }
 
-        val testResources = testResourceDir()!!
+        val testResources = testResourceDir() ?: error("No resource directory found for $name benchmark")
         val testData = testResources.resolve("testData")
-
         val testDataCopyCompleteMarker = testData.resolve("$name-copy-complete")
+
         if (!testDataCopyCompleteMarker.exists()) {
             val smtFiles = path.walkTopDown().filter { it.extension == "smt2" }.toList()
             copy {
@@ -42,5 +43,7 @@ fun Project.mkSmtLibBenchmarkTestData(name: String) = tasks.register("smtLibBenc
 
 private fun Project.testResourceDir(): File? {
     val sourceSets = (this as ExtensionAware).extensions.getByName("sourceSets") as SourceSetContainer
-    return sourceSets["test"].output.resourcesDir
+    return sourceSets["test"]?.output?.resourcesDir
 }
+
+private const val BENCHMARK_REPO_URL = "https://clc-gitlab.cs.uiowa.edu:2443"

gradle/wrapper/gradle-wrapper.properties

@@ -1,5 +1,5 @@
 distributionBase=GRADLE_USER_HOME
 distributionPath=wrapper/dists
-distributionUrl=https\://services.gradle.org/distributions/gradle-7.4.2-bin.zip
+distributionUrl=https\://services.gradle.org/distributions/gradle-7.5.1-bin.zip
 zipStoreBase=GRADLE_USER_HOME
 zipStorePath=wrapper/dists

gradlew

@@ -205,6 +205,12 @@ set -- \
         org.gradle.wrapper.GradleWrapperMain \
         "$@"
 
+# Stop when "xargs" is not available.
+if ! command -v xargs >/dev/null 2>&1
+then
+    die "xargs is not available"
+fi
+
 # Use "xargs" to parse quoted args.
 #
 # With -n1 it outputs one arg per line, with the quotes and backslashes removed.

gradlew.bat

@@ -14,7 +14,7 @@
 @rem limitations under the License.
 @rem
 
-@if "%DEBUG%" == "" @echo off
+@if "%DEBUG%"=="" @echo off
 @rem ##########################################################################
 @rem
 @rem  Gradle startup script for Windows
@@ -25,7 +25,7 @@
 if "%OS%"=="Windows_NT" setlocal
 
 set DIRNAME=%~dp0
-if "%DIRNAME%" == "" set DIRNAME=.
+if "%DIRNAME%"=="" set DIRNAME=.
 set APP_BASE_NAME=%~n0
 set APP_HOME=%DIRNAME%
 
@@ -40,7 +40,7 @@ if defined JAVA_HOME goto findJavaFromJavaHome
 
 set JAVA_EXE=java.exe
 %JAVA_EXE% -version >NUL 2>&1
-if "%ERRORLEVEL%" == "0" goto execute
+if %ERRORLEVEL% equ 0 goto execute
 
 echo.
 echo ERROR: JAVA_HOME is not set and no 'java' command could be found in your PATH.
@@ -75,13 +75,15 @@ set CLASSPATH=%APP_HOME%\gradle\wrapper\gradle-wrapper.jar
 
 :end
 @rem End local scope for the variables with windows NT shell
-if "%ERRORLEVEL%"=="0" goto mainEnd
+if %ERRORLEVEL% equ 0 goto mainEnd
 
 :fail
 rem Set variable GRADLE_EXIT_CONSOLE if you need the _script_ return code instead of
 rem the _cmd.exe /c_ return code!
-if  not "" == "%GRADLE_EXIT_CONSOLE%" exit 1
-exit /b 1
+set EXIT_CODE=%ERRORLEVEL%
+if %EXIT_CODE% equ 0 set EXIT_CODE=1
+if not ""=="%GRADLE_EXIT_CONSOLE%" exit %EXIT_CODE%
+exit /b %EXIT_CODE%
 
 :mainEnd
 if "%OS%"=="Windows_NT" endlocal

ksmt-bitwuzla/src/main/kotlin/org/ksmt/solver/bitwuzla/KBitwuzlaContext.kt

@@ -9,13 +9,14 @@ import org.ksmt.solver.bitwuzla.bindings.BitwuzlaSort
 import org.ksmt.solver.bitwuzla.bindings.BitwuzlaTerm
 import org.ksmt.solver.bitwuzla.bindings.Native
 import org.ksmt.sort.KSort
+import java.util.Collections
 import kotlin.time.Duration
 import kotlin.time.ExperimentalTime
 import kotlin.time.TimeMark
 import kotlin.time.TimeSource
 
 open class KBitwuzlaContext : AutoCloseable {
-    private var closed = false
+    private var isClosed = false
 
     val bitwuzla = Native.bitwuzlaNew()
 
@@ -39,11 +40,11 @@ open class KBitwuzlaContext : AutoCloseable {
      * internalization of already internalized expressions.
      *
      * [internalizer] must use special functions to internalize BitVec values ([internalizeBvValue])
-     * and constants ([mkConstant])
+     * and constants ([mkConstant]).
      * */
     fun internalizeExpr(expr: KExpr<*>, internalizer: (KExpr<*>) -> BitwuzlaTerm): BitwuzlaTerm =
         expressions.getOrPut(expr) {
-            internalizer(expr) // don't reverse cache bitwuzla term since it may be rewrited
+            internalizer(expr) // don't reverse cache bitwuzla term since it may be rewrote
         }
 
     fun internalizeSort(sort: KSort, internalizer: (KSort) -> BitwuzlaSort): BitwuzlaSort =
@@ -58,7 +59,8 @@ open class KBitwuzlaContext : AutoCloseable {
             internalizer(decl)
         }
 
-    /** Internalize and reverse cache Bv value to support Bv values conversion.
+    /**
+     * Internalize and reverse cache Bv value to support Bv values conversion.
      *
      * Since [Native.bitwuzlaGetBvValue] is only available after check-sat call
      * we must reverse cache Bv values to be able to convert all previously internalized
@@ -78,41 +80,45 @@ open class KBitwuzlaContext : AutoCloseable {
 
     fun convertValue(value: BitwuzlaTerm): KExpr<*>? = bvValues[value]
 
-    // constant is known only if it was previously internalized
+    // Constant is known only if it was previously internalized
     fun convertConstantIfKnown(term: BitwuzlaTerm): KDecl<*>? = bitwuzlaConstants[term]
 
     private val normalConstantScope: NormalConstantScope = NormalConstantScope()
     var currentConstantScope: ConstantScope = normalConstantScope
 
-    fun declaredConstants(): Set<KDecl<*>> = normalConstantScope.constants.toSet()
+    fun declaredConstants(): Set<KDecl<*>> = Collections.unmodifiableSet(normalConstantScope.constants)
 
-    /** Internalize constant.
+    /**
+     * Internalize constant.
      *  1. Since [Native.bitwuzlaMkConst] creates fresh constant on each invocation caches are used
-     *   to guarantee that if two constants are equal in ksmt they are also equal in Bitwuzla
-     *  2. Scoping is used to support quantifier bound variables (see [withConstantScope])
+     *  to guarantee that if two constants are equal in ksmt they are also equal in Bitwuzla;
+     *  2. Scoping is used to support quantifier bound variables (see [withConstantScope]).
      * */
     fun mkConstant(decl: KDecl<*>, sort: BitwuzlaSort): BitwuzlaTerm = currentConstantScope.mkConstant(decl, sort)
 
-    /** Constant scope for quantifiers.
+    /**
+     * Constant scope for quantifiers.
      *
      * Quantifier bound variables:
-     * 1. may clash with constants from outer scope
-     * 2. must be replaced with vars in quantifier body
+     * 1. may clash with constants from outer scope;
+     * 2. must be replaced with vars in quantifier body.
      *
      * @see QuantifiedConstantScope
      * */
     inline fun <reified T> withConstantScope(body: QuantifiedConstantScope.() -> T): T {
         val oldScope = currentConstantScope
         val newScope = QuantifiedConstantScope(currentConstantScope)
+
         currentConstantScope = newScope
         val result = newScope.body()
         currentConstantScope = oldScope
+
         return result
     }
 
 
     /**
-     * keep strong reference to bitwuzla timeout callback to avoid sigsegv
+     * Keep strong reference to bitwuzla timeout callback to avoid sigsegv.
      * */
     private var timeoutTerminator: BitwuzlaTimeout? = null
 
@@ -122,9 +128,11 @@ open class KBitwuzlaContext : AutoCloseable {
             Native.bitwuzlaResetTerminationCallback(bitwuzla)
             return body()
         }
+
         val currentTime = TimeSource.Monotonic.markNow()
         val finishTime = currentTime + timeout
         timeoutTerminator = BitwuzlaTimeout(finishTime)
+
         try {
             Native.bitwuzlaSetTerminationCallback(bitwuzla, timeoutTerminator, state = null)
             return body()
@@ -142,7 +150,7 @@ open class KBitwuzlaContext : AutoCloseable {
     }
 
     override fun close() {
-        closed = true
+        isClosed = true
         sorts.clear()
         bitwuzlaSorts.clear()
         expressions.clear()
@@ -153,7 +161,7 @@ open class KBitwuzlaContext : AutoCloseable {
     }
 
     fun ensureActive() {
-        check(!closed) { "context already closed" }
+        check(!isClosed) { "The context is already closed." }
     }
 
     private inline fun <K, V> convert(
@@ -169,6 +177,7 @@ open class KBitwuzlaContext : AutoCloseable {
         val converted = converter(key)
         cache.putIfAbsent(converted, key)
         reverseCache[key] = converted
+
         return converted
     }
 
@@ -177,10 +186,11 @@ open class KBitwuzlaContext : AutoCloseable {
     }
 
 
-    /** Produce normal constants for KSmt declarations.
+    /**
+     * Produce normal constants for KSMT declarations.
      *
-     *  Guarantee that if two declarations are equal
-     *  then same Bitwuzla native pointer is returned.
+     * Guarantee that if two declarations are equal
+     * then the same Bitwuzla native pointer is returned.
      * */
     inner class NormalConstantScope : ConstantScope {
         val constants = hashSetOf<KDecl<*>>()
@@ -194,16 +204,18 @@ open class KBitwuzlaContext : AutoCloseable {
         override fun mkConstant(decl: KDecl<*>, sort: BitwuzlaSort): BitwuzlaTerm = constantCache.create(decl, sort)
     }
 
-    /** Constant quantification.
+    /**
+     * Constant quantification.
      *
-     * If constant declaration registered as quantified variable,
+     * If constant declaration is registered as quantified variable,
      * then the corresponding var is returned instead of constant.
      * */
     inner class QuantifiedConstantScope(private val parent: ConstantScope) : ConstantScope {
         private val constants = hashMapOf<Pair<KDecl<*>, BitwuzlaSort>, BitwuzlaTerm>()
-        fun mkVar(decl: KDecl<*>, sort: BitwuzlaSort): BitwuzlaTerm = constants.getOrPut(decl to sort) {
-            Native.bitwuzlaMkVar(bitwuzla, sort, decl.name)
-        }
+        fun mkVar(decl: KDecl<*>, sort: BitwuzlaSort): BitwuzlaTerm =
+            constants.getOrPut(decl to sort) {
+                Native.bitwuzlaMkVar(bitwuzla, sort, decl.name)
+            }
 
         override fun mkConstant(decl: KDecl<*>, sort: BitwuzlaSort): BitwuzlaTerm =
             constants[decl to sort] ?: parent.mkConstant(decl, sort)
@@ -213,5 +225,4 @@ open class KBitwuzlaContext : AutoCloseable {
     class BitwuzlaTimeout(private val finishTime: TimeMark) : Native.BitwuzlaTerminationCallback {
         override fun terminate(state: Pointer?): Int = if (finishTime.hasNotPassedNow()) 0 else 1
     }
-
 }