From 9cc358dbf85a011660c6b59b9dee52cd67580cfb Mon Sep 17 00:00:00 2001 From: Rustam Sadykov Date: Mon, 23 May 2022 14:10:15 +0300 Subject: [PATCH 1/2] optimize solver cloning --- .../kotlin/org/utbot/engine/UtBotSymbolicEngine.kt | 5 +++++ .../src/main/kotlin/org/utbot/engine/pc/UtSolver.kt | 11 ++++------- 2 files changed, 9 insertions(+), 7 deletions(-) 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..2cadb1a29f 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.solver.expectUndefined = true val positiveCaseState = environment.state.updateQueued( edge, SymbolicStateUpdate( @@ -1435,6 +1436,9 @@ class UtBotSymbolicEngine( } else -> error("Unknown switch $current") } + if (successors.size > 1) { + environment.state.solver.expectUndefined = true + } 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.solver.expectUndefined = true 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 From cf9a22b629a07ea76cbb0de8c77e6b1cfa56a5b8 Mon Sep 17 00:00:00 2001 From: Rustam Sadykov Date: Mon, 23 May 2022 14:29:37 +0300 Subject: [PATCH 2/2] add method expectUndefined --- .../src/main/kotlin/org/utbot/engine/ExecutionState.kt | 10 ++++++++++ .../kotlin/org/utbot/engine/UtBotSymbolicEngine.kt | 6 +++--- 2 files changed, 13 insertions(+), 3 deletions(-) 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 2cadb1a29f..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,7 +1370,7 @@ class UtBotSymbolicEngine( val negativeCasePathConstraint = mkNot(positiveCasePathConstraint) positiveCaseEdge?.let { edge -> - environment.state.solver.expectUndefined = true + environment.state.expectUndefined() val positiveCaseState = environment.state.updateQueued( edge, SymbolicStateUpdate( @@ -1437,7 +1437,7 @@ class UtBotSymbolicEngine( else -> error("Unknown switch $current") } if (successors.size > 1) { - environment.state.solver.expectUndefined = true + environment.state.expectUndefined() } successors.forEach { (target, expr) -> pathSelector.offer( @@ -3436,7 +3436,7 @@ class UtBotSymbolicEngine( val symException = implicitThrown(exception, findNewAddr(), isInNestedMethod()) if (!traverseCatchBlock(environment.state.stmt, symException, conditions)) { - environment.state.solver.expectUndefined = true + environment.state.expectUndefined() val nextState = environment.state.createExceptionState( symException, queuedSymbolicStateUpdates