Optimize solver cloning (#12)

Author: SBOne-Kenobi

utbot-framework/src/main/kotlin/org/utbot/engine/ExecutionState.kt

@@ -12,6 +12,7 @@ import kotlinx.collections.immutable.persistentHashMapOf
 import kotlinx.collections.immutable.persistentHashSetOf
 import kotlinx.collections.immutable.persistentListOf
 import kotlinx.collections.immutable.plus
+import org.utbot.engine.pc.UtSolverStatusUNDEFINED
 import soot.SootMethod
 import soot.jimple.Stmt
 
@@ -205,6 +206,15 @@ data class ExecutionState(
         )
     }
 
+    /**
+     * Tell to solver that states with status [UtSolverStatusUNDEFINED] can be created from current state.
+     *
+     * Note: Solver optimize cloning respect this flag.
+     */
+    fun expectUndefined() {
+        solver.expectUndefined = true
+    }
+
     override fun close() {
         solver.close()
     }

utbot-framework/src/main/kotlin/org/utbot/engine/UtBotSymbolicEngine.kt

@@ -1370,6 +1370,7 @@ class UtBotSymbolicEngine(
         val negativeCasePathConstraint = mkNot(positiveCasePathConstraint)
 
         positiveCaseEdge?.let { edge ->
+            environment.state.expectUndefined()
             val positiveCaseState = environment.state.updateQueued(
                 edge,
                 SymbolicStateUpdate(
@@ -1435,6 +1436,9 @@ class UtBotSymbolicEngine(
             }
             else -> error("Unknown switch $current")
         }
+        if (successors.size > 1) {
+            environment.state.expectUndefined()
+        }
         successors.forEach { (target, expr) ->
             pathSelector.offer(
                 environment.state.updateQueued(
@@ -3432,6 +3436,7 @@ class UtBotSymbolicEngine(
 
         val symException = implicitThrown(exception, findNewAddr(), isInNestedMethod())
         if (!traverseCatchBlock(environment.state.stmt, symException, conditions)) {
+            environment.state.expectUndefined()
             val nextState = environment.state.createExceptionState(
                 symException,
                 queuedSymbolicStateUpdates

utbot-framework/src/main/kotlin/org/utbot/engine/pc/UtSolver.kt

@@ -161,16 +161,13 @@ data class UtSolver constructor(
     val assertions: Set<UtBoolExpression>
         get(): Set<UtBoolExpression> = constraints.hard
 
+    var expectUndefined: Boolean = false
+
     fun add(hard: HardConstraint, soft: SoftConstraint): UtSolver {
         // status can implicitly change here to UNDEFINED or UNSAT
         val newConstraints = constraints.with(hard.constraints, soft.constraints)
-        /*
-        Always there is at least one new state with SAT status if current status is SAT
-        Thus we can prioritize states like this to reuse current solver.
-         */
-        val isSAT = constraints.status is UtSolverStatusSAT
-        val wantClone = (isSAT && newConstraints.status is UtSolverStatusSAT)
-                || (!isSAT && newConstraints !is UnsatQuery)
+        val wantClone = (expectUndefined && newConstraints.status is UtSolverStatusUNDEFINED)
+                || (!expectUndefined && newConstraints.status !is UtSolverStatusUNSAT)
 
         return if (wantClone && canBeCloned) {
             // try to reuse z3 Solver with value SAT when possible