Add IC3 to XSTS cli

subprojects/xsts/xsts-cli/src/main/kotlin/hu/bme/mit/theta/xsts/cli/XstsCliBounded.kt

@@ -31,7 +31,6 @@ import hu.bme.mit.theta.solver.SolverManager
 import hu.bme.mit.theta.xsts.XSTS
 import hu.bme.mit.theta.xsts.analysis.XstsAction
 import hu.bme.mit.theta.xsts.analysis.XstsState
-import hu.bme.mit.theta.xsts.analysis.hu.bme.mit.theta.xsts.analysis.toMonolithicExpr
 import hu.bme.mit.theta.xsts.analysis.hu.bme.mit.theta.xsts.analysis.valToAction
 import hu.bme.mit.theta.xsts.analysis.hu.bme.mit.theta.xsts.analysis.valToState
 import java.util.concurrent.TimeUnit
@@ -40,7 +39,7 @@ import kotlin.system.exitProcess
 typealias S = XstsState<ExplState>
 
 class XstsCliBounded :
-  XstsCliMonolithicBasedCommand(
+  XstsCliMonolithicBaseCommand(
     name = "BOUNDED",
     help =
       "Bounded model checking algorithms (BMC, IMC, KINDUCTION). Use --variant to select the algorithm (by default BMC is selected).",

subprojects/xsts/xsts-cli/src/main/kotlin/hu/bme/mit/theta/xsts/cli/XstsCliIC3.kt

@@ -0,0 +1,92 @@
+/*
+ *  Copyright 2025 Budapest University of Technology and Economics
+ *
+ *  Licensed under the Apache License, Version 2.0 (the "License");
+ *  you may not use this file except in compliance with the License.
+ *  You may obtain a copy of the License at
+ *
+ *      http://www.apache.org/licenses/LICENSE-2.0
+ *
+ *  Unless required by applicable law or agreed to in writing, software
+ *  distributed under the License is distributed on an "AS IS" BASIS,
+ *  WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied.
+ *  See the License for the specific language governing permissions and
+ *  limitations under the License.
+ */
+
+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.github.ajalt.clikt.parameters.types.boolean
+import com.google.common.base.Stopwatch
+import hu.bme.mit.theta.analysis.Trace
+import hu.bme.mit.theta.analysis.algorithm.EmptyProof
+import hu.bme.mit.theta.analysis.algorithm.SafetyResult
+import hu.bme.mit.theta.analysis.algorithm.bounded.*
+import hu.bme.mit.theta.analysis.algorithm.ic3.Ic3Checker
+import hu.bme.mit.theta.solver.SolverManager
+import hu.bme.mit.theta.xsts.XSTS
+import hu.bme.mit.theta.xsts.analysis.XstsAction
+import hu.bme.mit.theta.xsts.analysis.hu.bme.mit.theta.xsts.analysis.valToAction
+import hu.bme.mit.theta.xsts.analysis.hu.bme.mit.theta.xsts.analysis.valToState
+import java.util.concurrent.TimeUnit
+import kotlin.system.exitProcess
+
+class XstsCliIC3 :
+  XstsCliMonolithicBaseCommand(
+    name = "IC3",
+    help =
+      "Model checking using the IC3 algorithm.",
+  ) {
+
+  private val formerFramesOpt: Boolean by option().boolean().default(true)
+  private val unSatOpt: Boolean by option().boolean().default(true)
+  private val notBOpt: Boolean by option().boolean().default(true)
+  private val propagateOpt: Boolean by option().boolean().default(true)
+  private val filterOpt: Boolean by option().boolean().default(true)
+
+  private fun printResult(
+    status: SafetyResult<EmptyProof, Trace<S, XstsAction>>,
+    xsts: XSTS,
+    totalTimeMs: Long,
+  ) {
+    if (!outputOptions.benchmarkMode) return
+    printCommonResult(status, xsts, totalTimeMs)
+    writer.newRow()
+  }
+
+  override fun run() {
+    try {
+      doRun()
+    } catch (e: Exception) {
+      printError(e)
+        exitProcess(1)
+    }
+  }
+
+  private fun doRun() {
+    registerSolverManagers()
+    val solverFactory = SolverManager.resolveSolverFactory(solver)
+    val xsts = inputOptions.loadXsts()
+    val monolithicExpr = createMonolithicExpr(xsts)
+    val sw = Stopwatch.createStarted()
+    val checker = Ic3Checker(
+            monolithicExpr,
+            reversed,
+            solverFactory,
+            xsts::valToState,
+            xsts::valToAction,
+            formerFramesOpt,
+            unSatOpt,
+            notBOpt,
+            propagateOpt,
+            filterOpt,
+            false
+        )
+    val result = checker.check()
+    sw.stop()
+    printResult(result, xsts, sw.elapsed(TimeUnit.MILLISECONDS))
+    writeCex(result, xsts)
+  }
+}

subprojects/xsts/xsts-cli/src/main/kotlin/hu/bme/mit/theta/xsts/cli/XstsCliMain.kt

@@ -47,6 +47,7 @@ fun main(args: Array<String>) =
       XstsCliMdd(),
       XstsCliPetrinetMdd(),
       XstsCliChc(),
+      XstsCliIC3(),
       XstsCliHeader(),
       XstsCliMetrics(),
     )

subprojects/xsts/xsts-cli/src/main/kotlin/hu/bme/mit/theta/xsts/cli/XstsCliMonolithicBasedCommand.kt → subprojects/xsts/xsts-cli/src/main/kotlin/hu/bme/mit/theta/xsts/cli/XstsCliMonolithicBaseCommand.kt

@@ -25,12 +25,12 @@ import hu.bme.mit.theta.analysis.l2s.createMonolithicL2S
 import hu.bme.mit.theta.xsts.XSTS
 import hu.bme.mit.theta.xsts.analysis.hu.bme.mit.theta.xsts.analysis.toMonolithicExpr
 
-abstract class XstsCliMonolithicBasedCommand(name: String? = null, help: String = ""):
+abstract class XstsCliMonolithicBaseCommand(name: String? = null, help: String = ""):
     XstsCliBaseCommand(name = name, help = help) {
 
-    private val reversed: Boolean by option(help = "Reversed state space exploration").boolean().default(false)
-    private val livenessToSafety: Boolean by option(help = "Use liveness to safety transformation").boolean().default(false)
-    private val abstracted: Boolean by option(help = "Wrap analysis in CEGAR loop").boolean().default(false)
+    protected val reversed: Boolean by option(help = "Reversed state space exploration").boolean().default(false)
+    protected val livenessToSafety: Boolean by option(help = "Use liveness to safety transformation").boolean().default(false)
+    protected val abstracted: Boolean by option(help = "Wrap analysis in CEGAR loop").boolean().default(false)
 
     fun createMonolithicExpr(xsts: XSTS): MonolithicExpr {
         var monolithicExpr = xsts.toMonolithicExpr()