diff --git a/utbot-framework/src/main/kotlin/org/utbot/engine/ExecutionState.kt b/utbot-framework/src/main/kotlin/org/utbot/engine/ExecutionState.kt index a2c5ef8c08..79ab953a89 100644 --- a/utbot-framework/src/main/kotlin/org/utbot/engine/ExecutionState.kt +++ b/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() } diff --git a/utbot-framework/src/main/kotlin/org/utbot/engine/UtBotSymbolicEngine.kt b/utbot-framework/src/main/kotlin/org/utbot/engine/UtBotSymbolicEngine.kt index 1e6ed3db37..12c4ef9bd5 100644 --- a/utbot-framework/src/main/kotlin/org/utbot/engine/UtBotSymbolicEngine.kt +++ b/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 diff --git a/utbot-framework/src/main/kotlin/org/utbot/engine/pc/UtSolver.kt b/utbot-framework/src/main/kotlin/org/utbot/engine/pc/UtSolver.kt index 6a408bdb1d..1ea07cfcba 100644 --- a/utbot-framework/src/main/kotlin/org/utbot/engine/pc/UtSolver.kt +++ b/utbot-framework/src/main/kotlin/org/utbot/engine/pc/UtSolver.kt @@ -161,16 +161,13 @@ data class UtSolver constructor( val assertions: Set get(): Set = 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