Merge pull request #294 from ftsrg/xsts-cli-fix

XSTS Cli fixes
ftsrg · Aug 13, 2024 · 289781e · 289781e
2 parents 575544c + 10e6793
commit 289781e
Show file tree

Hide file tree

Showing 3 changed files with 9 additions and 3 deletions.
diff --git a/build.gradle.kts b/build.gradle.kts
@@ -28,7 +28,7 @@ buildscript {
 
 allprojects {
     group = "hu.bme.mit.theta"
-    version = "6.5.0"
+    version = "6.5.1"
 
     apply(from = rootDir.resolve("gradle/shared-with-buildSrc/mirrors.gradle.kts"))
 }

diff --git a/subprojects/xsts/xsts-cli/src/main/kotlin/hu/bme/mit/theta/xsts/cli/XstsCliBaseCommand.kt b/subprojects/xsts/xsts-cli/src/main/kotlin/hu/bme/mit/theta/xsts/cli/XstsCliBaseCommand.kt
@@ -19,6 +19,7 @@ package hu.bme.mit.theta.xsts.cli
 import com.github.ajalt.clikt.core.CliktCommand
 import com.github.ajalt.clikt.parameters.groups.provideDelegate
 import com.github.ajalt.clikt.parameters.options.default
+import com.github.ajalt.clikt.parameters.options.defaultLazy
 import com.github.ajalt.clikt.parameters.options.option
 import com.github.ajalt.clikt.parameters.options.versionOption
 import com.github.ajalt.clikt.parameters.types.file
@@ -51,7 +52,8 @@ abstract class XstsCliBaseCommand(name: String? = null, help: String = "") :
 
     protected val inputOptions by InputOptions()
     protected val outputOptions by OutputOptions()
-    protected val solver: String by option(help = "The solver to use for the check").default("Z3")
+    protected open val defaultSolver: String = "Z3"
+    protected val solver: String by option(help = "The solver to use for the check").defaultLazy { defaultSolver }
     private val smtHome: File by option().file().default(SmtLibSolverManager.HOME.toFile())
     protected val logger: Logger by lazy {
         if (outputOptions.benchmarkMode) NullLogger.getInstance() else ConsoleLogger(outputOptions.logLevel)
@@ -78,7 +80,7 @@ abstract class XstsCliBaseCommand(name: String? = null, help: String = "") :
         listOf(
             status.isSafe,
             totalTimeMs,
-            if (status.isUnsafe) "${status.asUnsafe().cex!!.length()}" else "",
+            if (status.isUnsafe) "${status.asUnsafe().cex?.length() ?: "N/A"}" else "",
             xsts.vars.size,
         ).forEach(writer::cell)
     }

diff --git a/subprojects/xsts/xsts-cli/src/main/kotlin/hu/bme/mit/theta/xsts/cli/XstsCliChc.kt b/subprojects/xsts/xsts-cli/src/main/kotlin/hu/bme/mit/theta/xsts/cli/XstsCliChc.kt
@@ -16,6 +16,8 @@
 
 package hu.bme.mit.theta.xsts.cli
 
+import com.github.ajalt.clikt.parameters.options.default
+import com.github.ajalt.clikt.parameters.options.option
 import com.google.common.base.Stopwatch
 import hu.bme.mit.theta.analysis.algorithm.SafetyResult
 import hu.bme.mit.theta.analysis.algorithm.chc.CexTree
@@ -33,6 +35,8 @@ class XstsCliChc : XstsCliBaseCommand(
     help = "Model checking using the Horn solving backend"
 ) {
 
+    override val defaultSolver: String = "z3:4.13.0"
+
     private fun printResult(status: SafetyResult<Invariant, CexTree>, xsts: XSTS, totalTimeMs: Long) {
         if (!outputOptions.benchmarkMode) return
         printCommonResult(status, xsts, totalTimeMs)