From a4b5202780b0b68354227b613204c5597a51ea8b Mon Sep 17 00:00:00 2001 From: Kamenev Yury Date: Fri, 16 Sep 2022 11:08:44 +0300 Subject: [PATCH 1/2] Added simplification/rewriting for assumptions --- .../utbot/engine/pc/QueryOptimizationsTest.kt | 3 +- .../examples/stream/BaseStreamExampleTest.kt | 1 - .../kotlin/org/utbot/engine/DataClasses.kt | 17 ++--- .../main/kotlin/org/utbot/engine/Traverser.kt | 18 ++--- .../main/kotlin/org/utbot/engine/pc/Query.kt | 68 ++++++++++++++++--- .../kotlin/org/utbot/engine/pc/UtSolver.kt | 9 +-- .../engine/symbolic/SymbolicStateUpdate.kt | 20 ++++-- .../examples/stream/BaseStreamExample.java | 2 +- 8 files changed, 92 insertions(+), 46 deletions(-) diff --git a/utbot-framework-test/src/test/kotlin/org/utbot/engine/pc/QueryOptimizationsTest.kt b/utbot-framework-test/src/test/kotlin/org/utbot/engine/pc/QueryOptimizationsTest.kt index 43dcb3a39c..df1fe9b2ad 100644 --- a/utbot-framework-test/src/test/kotlin/org/utbot/engine/pc/QueryOptimizationsTest.kt +++ b/utbot-framework-test/src/test/kotlin/org/utbot/engine/pc/QueryOptimizationsTest.kt @@ -34,6 +34,7 @@ import kotlinx.collections.immutable.persistentListOf import org.junit.jupiter.api.AfterAll import org.junit.jupiter.api.BeforeAll import org.junit.jupiter.api.Test +import org.utbot.engine.symbolic.EmptyAssumption private var expressionSimplificationValue: Boolean = UtSettings.useExpressionSimplification @@ -51,7 +52,7 @@ fun afterAll() { class QueryOptimizationsTest { private fun BaseQuery.check(vararg exprs: UtBoolExpression, checker: (BaseQuery) -> Unit = {}): BaseQuery = - this.with(hard = exprs.toList(), soft = emptyList()).also { + this.with(hard = exprs.toList(), soft = emptyList(), assumptions = EmptyAssumption).also { checker(it) } diff --git a/utbot-framework-test/src/test/kotlin/org/utbot/examples/stream/BaseStreamExampleTest.kt b/utbot-framework-test/src/test/kotlin/org/utbot/examples/stream/BaseStreamExampleTest.kt index 0f7d6d99eb..9ac18d9a8e 100644 --- a/utbot-framework-test/src/test/kotlin/org/utbot/examples/stream/BaseStreamExampleTest.kt +++ b/utbot-framework-test/src/test/kotlin/org/utbot/examples/stream/BaseStreamExampleTest.kt @@ -87,7 +87,6 @@ class BaseStreamExampleTest : UtValueTestCaseChecker( } @Test - @Disabled("Java 11 transition -- Yura looks at this. We have similar issue with Strings") fun testDistinctExample() { check( BaseStreamExample::distinctExample, diff --git a/utbot-framework/src/main/kotlin/org/utbot/engine/DataClasses.kt b/utbot-framework/src/main/kotlin/org/utbot/engine/DataClasses.kt index bb7ce114ed..39bef94ff8 100644 --- a/utbot-framework/src/main/kotlin/org/utbot/engine/DataClasses.kt +++ b/utbot-framework/src/main/kotlin/org/utbot/engine/DataClasses.kt @@ -8,10 +8,7 @@ import org.utbot.engine.pc.UtIsExpression import org.utbot.engine.pc.UtTrue import org.utbot.engine.pc.mkAnd import org.utbot.engine.pc.mkOr -import org.utbot.engine.symbolic.Assumption -import org.utbot.engine.symbolic.HardConstraint -import org.utbot.engine.symbolic.SoftConstraint -import org.utbot.engine.symbolic.SymbolicStateUpdate +import org.utbot.engine.symbolic.* import org.utbot.framework.plugin.api.FieldId import org.utbot.framework.plugin.api.UtInstrumentation import java.util.Objects @@ -133,17 +130,17 @@ data class MethodResult( constructor( symbolicResult: SymbolicResult, - hardConstraints: HardConstraint = HardConstraint(), - softConstraints: SoftConstraint = SoftConstraint(), - assumption: Assumption = Assumption(), + hardConstraints: HardConstraint = EmptyHardConstraint, + softConstraints: SoftConstraint = EmptySoftConstraint, + assumption: Assumption = EmptyAssumption, memoryUpdates: MemoryUpdate = MemoryUpdate() ) : this(symbolicResult, SymbolicStateUpdate(hardConstraints, softConstraints, assumption, memoryUpdates)) constructor( value: SymbolicValue, - hardConstraints: HardConstraint = HardConstraint(), - softConstraints: SoftConstraint = SoftConstraint(), - assumption: Assumption = Assumption(), + hardConstraints: HardConstraint = EmptyHardConstraint, + softConstraints: SoftConstraint = EmptySoftConstraint, + assumption: Assumption = EmptyAssumption, memoryUpdates: MemoryUpdate = MemoryUpdate(), ) : this(SymbolicSuccess(value), hardConstraints, softConstraints, assumption, memoryUpdates) } diff --git a/utbot-framework/src/main/kotlin/org/utbot/engine/Traverser.kt b/utbot-framework/src/main/kotlin/org/utbot/engine/Traverser.kt index 8c9673c439..973a3e1813 100644 --- a/utbot-framework/src/main/kotlin/org/utbot/engine/Traverser.kt +++ b/utbot-framework/src/main/kotlin/org/utbot/engine/Traverser.kt @@ -66,14 +66,7 @@ import org.utbot.engine.pc.mkNot import org.utbot.engine.pc.mkOr import org.utbot.engine.pc.select import org.utbot.engine.pc.store -import org.utbot.engine.symbolic.HardConstraint -import org.utbot.engine.symbolic.SoftConstraint -import org.utbot.engine.symbolic.Assumption -import org.utbot.engine.symbolic.SymbolicStateUpdate -import org.utbot.engine.symbolic.asHardConstraint -import org.utbot.engine.symbolic.asSoftConstraint -import org.utbot.engine.symbolic.asAssumption -import org.utbot.engine.symbolic.asUpdate +import org.utbot.engine.symbolic.* import org.utbot.engine.util.trusted.isFromTrustedLibrary import org.utbot.engine.util.statics.concrete.associateEnumSootFieldsWithConcreteValues import org.utbot.engine.util.statics.concrete.isEnumAffectingExternalStatics @@ -1076,8 +1069,8 @@ class Traverser( } // Depending on existance of assumeExpr we have to add corresponding hardConstraints and assumptions - val hardConstraints = if (!isAssumeExpr) negativeCasePathConstraint.asHardConstraint() else HardConstraint() - val assumption = if (isAssumeExpr) negativeCasePathConstraint.asAssumption() else Assumption() + val hardConstraints = if (!isAssumeExpr) negativeCasePathConstraint.asHardConstraint() else EmptyHardConstraint + val assumption = if (isAssumeExpr) negativeCasePathConstraint.asAssumption() else EmptyAssumption val negativeCaseState = environment.state.updateQueued( negativeCaseEdge, @@ -2958,8 +2951,9 @@ class Traverser( return when (expr) { is UtInstanceOfExpression -> { // for now only this type of expression produces deferred updates val onlyMemoryUpdates = expr.symbolicStateUpdate.copy( - hardConstraints = HardConstraint(), - softConstraints = SoftConstraint() + hardConstraints = EmptyHardConstraint, + softConstraints = EmptySoftConstraint, + assumptions = EmptyAssumption ) SymbolicStateUpdateForResolvedCondition(onlyMemoryUpdates) } diff --git a/utbot-framework/src/main/kotlin/org/utbot/engine/pc/Query.kt b/utbot-framework/src/main/kotlin/org/utbot/engine/pc/Query.kt index 51e41560ba..5b28c878f3 100644 --- a/utbot-framework/src/main/kotlin/org/utbot/engine/pc/Query.kt +++ b/utbot-framework/src/main/kotlin/org/utbot/engine/pc/Query.kt @@ -19,6 +19,9 @@ import kotlinx.collections.immutable.mutate import kotlinx.collections.immutable.persistentHashMapOf import kotlinx.collections.immutable.persistentHashSetOf import kotlinx.collections.immutable.toPersistentSet +import org.utbot.engine.symbolic.Assumption +import org.utbot.engine.symbolic.EmptyAssumption +import org.utbot.engine.symbolic.asAssumption /** * Base class that represents immutable query of constraints to solver. @@ -31,6 +34,7 @@ import kotlinx.collections.immutable.toPersistentSet sealed class BaseQuery( open val hard: PersistentSet, open val soft: PersistentSet, + open val assumptions: Assumption, open val status: UtSolverStatus, open val lastAdded: Collection ) { @@ -40,7 +44,11 @@ sealed class BaseQuery( * @param hard - new constraints that must be satisfied. * @param soft - new constraints that are suggested to be satisfied if possible. */ - abstract fun with(hard: Collection, soft: Collection): BaseQuery + abstract fun with( + hard: Collection, + soft: Collection, + assumptions: Assumption + ): BaseQuery /** * Set [status] of the query. @@ -55,11 +63,19 @@ sealed class BaseQuery( * UnsatQuery.[status] is [UtSolverStatusUNSAT]. * UnsatQuery.[lastAdded] = [emptyList] */ -class UnsatQuery(hard: PersistentSet) : - BaseQuery(hard, persistentHashSetOf(), UtSolverStatusUNSAT(UtSolverStatusKind.UNSAT), emptyList()) { +class UnsatQuery(hard: PersistentSet) : BaseQuery( + hard, + soft = persistentHashSetOf(), + EmptyAssumption, + UtSolverStatusUNSAT(UtSolverStatusKind.UNSAT), + lastAdded = emptyList() +) { - override fun with(hard: Collection, soft: Collection): BaseQuery = - error("State with UnsatQuery isn't eliminated. Adding constraints to $this isn't allowed.") + override fun with( + hard: Collection, + soft: Collection, + assumptions: Assumption + ): BaseQuery = error("State with UnsatQuery isn't eliminated. Adding constraints to $this isn't allowed.") override fun withStatus(newStatus: UtSolverStatus) = this @@ -78,12 +94,13 @@ class UnsatQuery(hard: PersistentSet) : data class Query( override val hard: PersistentSet = persistentHashSetOf(), override val soft: PersistentSet = persistentHashSetOf(), + override val assumptions: Assumption = EmptyAssumption, override val status: UtSolverStatus = UtSolverStatusUNDEFINED, override val lastAdded: Collection = emptyList(), private val eqs: PersistentMap = persistentHashMapOf(), private val lts: PersistentMap = persistentHashMapOf(), private val gts: PersistentMap = persistentHashMapOf() -) : BaseQuery(hard, soft, status, lastAdded) { +) : BaseQuery(hard, soft, assumptions, status, lastAdded) { val rewriter: RewritingVisitor get() = RewritingVisitor(eqs, lts, gts) @@ -179,6 +196,7 @@ data class Query( private fun addSimplified( hard: Collection, soft: Collection, + assumptions: Assumption ): BaseQuery { val addedHard = hard.simplify().filterNot { it is UtTrue } if (addedHard.isEmpty() && soft.isEmpty()) { @@ -266,8 +284,27 @@ data class Query( .filterNot { it is UtBoolLiteral } .toPersistentSet() + // Apply simplifications to assumptions in query. + // We do not filter out UtFalse here because we need them to get UNSAT in corresponding cases and run concrete instead. + val newAssumptions = this.assumptions + .plus(assumptions) + .constraints + .simplify(newEqs, newLts, newGts) + .toPersistentSet() + .asAssumption() + val diffHard = newHard - this.hard - return Query(newHard, newSoft, status.checkFastSatAndReturnStatus(diffHard), diffHard, newEqs, newLts, newGts) + + return Query( + newHard, + newSoft, + newAssumptions, + status.checkFastSatAndReturnStatus(diffHard), + lastAdded = diffHard, + newEqs, + newLts, + newGts + ) } /** @@ -275,11 +312,22 @@ data class Query( * @param hard - set of constraints that must be satisfied. * @param soft - set of constraints that should be satisfied if possible. */ - override fun with(hard: Collection, soft: Collection): BaseQuery { + override fun with( + hard: Collection, + soft: Collection, + assumptions: Assumption + ): BaseQuery { return if (useExpressionSimplification) { - addSimplified(hard, soft) + addSimplified(hard, soft, assumptions) } else { - Query(this.hard.addAll(hard), this.soft.addAll(soft), status.checkFastSatAndReturnStatus(hard), hard, this.eqs) + Query( + this.hard.addAll(hard), + this.soft.addAll(soft), + this.assumptions.plus(assumptions), + status.checkFastSatAndReturnStatus(hard), + lastAdded = hard, + this.eqs + ) } } 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 d8dd4d0682..6998a41e42 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 @@ -31,6 +31,7 @@ import com.microsoft.z3.Status.UNSATISFIABLE import kotlinx.collections.immutable.PersistentSet import kotlinx.collections.immutable.persistentHashSetOf import mu.KotlinLogging +import org.utbot.engine.symbolic.EmptyAssumption import soot.ByteType import soot.CharType import soot.IntType @@ -131,7 +132,7 @@ data class UtSolver constructor( // Constraints that should not be added in the solver as hypothesis. // Instead, we use `check` to find out if they are satisfiable. // It is required to have unsat cores with them. - var assumption: Assumption = Assumption(), + var assumption: Assumption = EmptyAssumption, //new constraints for solver (kind of incremental behavior) private var hardConstraintsNotYetAddedToZ3Solver: PersistentSet = persistentHashSetOf(), @@ -175,9 +176,9 @@ data class UtSolver constructor( var expectUndefined: Boolean = false - fun add(hard: HardConstraint, soft: SoftConstraint, assumption: Assumption = Assumption()): UtSolver { + fun add(hard: HardConstraint, soft: SoftConstraint, assumption: Assumption): UtSolver { // status can implicitly change here to UNDEFINED or UNSAT - val newConstraints = constraints.with(hard.constraints, soft.constraints) + val newConstraints = constraints.with(hard.constraints, soft.constraints, assumption) val wantClone = (expectUndefined && newConstraints.status is UtSolverStatusUNDEFINED) || (!expectUndefined && newConstraints.status !is UtSolverStatusUNSAT) @@ -204,7 +205,7 @@ data class UtSolver constructor( copy( constraints = constraintsWithStatus, hardConstraintsNotYetAddedToZ3Solver = newConstraints.hard, - assumption = this.assumption + assumption, + assumption = newConstraints.assumptions, z3Solver = context.mkSolver().also { it.setParameters(params) }, ) } diff --git a/utbot-framework/src/main/kotlin/org/utbot/engine/symbolic/SymbolicStateUpdate.kt b/utbot-framework/src/main/kotlin/org/utbot/engine/symbolic/SymbolicStateUpdate.kt index 0b883d0a76..a6a4e44e61 100644 --- a/utbot-framework/src/main/kotlin/org/utbot/engine/symbolic/SymbolicStateUpdate.kt +++ b/utbot-framework/src/main/kotlin/org/utbot/engine/symbolic/SymbolicStateUpdate.kt @@ -22,23 +22,27 @@ sealed class Constraint>(constraints: Set = /** * Represents hard constraints. */ -class HardConstraint( +open class HardConstraint( constraints: Set = emptySet() ) : Constraint(constraints) { override fun plus(other: HardConstraint): HardConstraint = HardConstraint(addConstraints(other.constraints)) } +object EmptyHardConstraint : HardConstraint() + /** * Represents soft constraints. */ -class SoftConstraint( +open class SoftConstraint( constraints: Set = emptySet() ) : Constraint(constraints) { override fun plus(other: SoftConstraint): SoftConstraint = SoftConstraint(addConstraints(other.constraints)) } +object EmptySoftConstraint : SoftConstraint() + /** * Represent constraints that must be satisfied for symbolic execution. * At the same time, if they don't, the state they belong to still @@ -46,7 +50,7 @@ class SoftConstraint( * * @see */ -class Assumption( +open class Assumption( constraints: Set = emptySet() ): Constraint(constraints) { override fun plus(other: Assumption): Assumption = Assumption(addConstraints(other.constraints)) @@ -54,15 +58,17 @@ class Assumption( override fun toString() = constraints.joinToString(System.lineSeparator()) } +object EmptyAssumption : Assumption() + /** * Represents one or more updates that can be applied to [SymbolicState]. * * TODO: move [localMemoryUpdates] to another place */ data class SymbolicStateUpdate( - val hardConstraints: HardConstraint = HardConstraint(), - val softConstraints: SoftConstraint = SoftConstraint(), - val assumptions: Assumption = Assumption(), + val hardConstraints: HardConstraint = EmptyHardConstraint, + val softConstraints: SoftConstraint = EmptySoftConstraint, + val assumptions: Assumption = EmptyAssumption, val memoryUpdates: MemoryUpdate = MemoryUpdate(), val localMemoryUpdates: LocalMemoryUpdate = LocalMemoryUpdate() ) { @@ -107,7 +113,7 @@ fun Collection.asSoftConstraint() = SoftConstraint(transformTo fun UtBoolExpression.asSoftConstraint() = SoftConstraint(setOf(this)) -fun Collection.asAssumption() = Assumption(toSet()) +fun Collection.asAssumption() = Assumption(transformToSet()) fun UtBoolExpression.asAssumption() = Assumption(setOf(this)) diff --git a/utbot-sample/src/main/java/org/utbot/examples/stream/BaseStreamExample.java b/utbot-sample/src/main/java/org/utbot/examples/stream/BaseStreamExample.java index 326f3b12b9..f8ba8061cb 100644 --- a/utbot-sample/src/main/java/org/utbot/examples/stream/BaseStreamExample.java +++ b/utbot-sample/src/main/java/org/utbot/examples/stream/BaseStreamExample.java @@ -68,7 +68,7 @@ boolean distinctExample(List list) { int prevSize = list.size(); - int newSize = list.stream().distinct().toArray().length; + int newSize = (int) list.stream().distinct().count(); return prevSize != newSize; } From 069a5154fe71fd94b6fa891189fd1034149d5cd0 Mon Sep 17 00:00:00 2001 From: Kamenev Yury Date: Fri, 16 Sep 2022 14:37:06 +0300 Subject: [PATCH 2/2] Fixed review issues --- .../utbot/engine/pc/QueryOptimizationsTest.kt | 3 +- .../kotlin/org/utbot/engine/DataClasses.kt | 12 ++++---- .../main/kotlin/org/utbot/engine/Traverser.kt | 22 +++++++++++---- .../main/kotlin/org/utbot/engine/pc/Query.kt | 23 ++++++--------- .../kotlin/org/utbot/engine/pc/UtSolver.kt | 9 +++--- .../engine/symbolic/SymbolicStateUpdate.kt | 28 +++++++++++++------ 6 files changed, 57 insertions(+), 40 deletions(-) diff --git a/utbot-framework-test/src/test/kotlin/org/utbot/engine/pc/QueryOptimizationsTest.kt b/utbot-framework-test/src/test/kotlin/org/utbot/engine/pc/QueryOptimizationsTest.kt index df1fe9b2ad..498c3ee2e5 100644 --- a/utbot-framework-test/src/test/kotlin/org/utbot/engine/pc/QueryOptimizationsTest.kt +++ b/utbot-framework-test/src/test/kotlin/org/utbot/engine/pc/QueryOptimizationsTest.kt @@ -34,7 +34,6 @@ import kotlinx.collections.immutable.persistentListOf import org.junit.jupiter.api.AfterAll import org.junit.jupiter.api.BeforeAll import org.junit.jupiter.api.Test -import org.utbot.engine.symbolic.EmptyAssumption private var expressionSimplificationValue: Boolean = UtSettings.useExpressionSimplification @@ -52,7 +51,7 @@ fun afterAll() { class QueryOptimizationsTest { private fun BaseQuery.check(vararg exprs: UtBoolExpression, checker: (BaseQuery) -> Unit = {}): BaseQuery = - this.with(hard = exprs.toList(), soft = emptyList(), assumptions = EmptyAssumption).also { + this.with(hard = exprs.toList(), soft = emptyList(), assumptions = emptyList()).also { checker(it) } diff --git a/utbot-framework/src/main/kotlin/org/utbot/engine/DataClasses.kt b/utbot-framework/src/main/kotlin/org/utbot/engine/DataClasses.kt index 39bef94ff8..1b11f25c07 100644 --- a/utbot-framework/src/main/kotlin/org/utbot/engine/DataClasses.kt +++ b/utbot-framework/src/main/kotlin/org/utbot/engine/DataClasses.kt @@ -130,17 +130,17 @@ data class MethodResult( constructor( symbolicResult: SymbolicResult, - hardConstraints: HardConstraint = EmptyHardConstraint, - softConstraints: SoftConstraint = EmptySoftConstraint, - assumption: Assumption = EmptyAssumption, + hardConstraints: HardConstraint = emptyHardConstraint(), + softConstraints: SoftConstraint = emptySoftConstraint(), + assumption: Assumption = emptyAssumption(), memoryUpdates: MemoryUpdate = MemoryUpdate() ) : this(symbolicResult, SymbolicStateUpdate(hardConstraints, softConstraints, assumption, memoryUpdates)) constructor( value: SymbolicValue, - hardConstraints: HardConstraint = EmptyHardConstraint, - softConstraints: SoftConstraint = EmptySoftConstraint, - assumption: Assumption = EmptyAssumption, + hardConstraints: HardConstraint = emptyHardConstraint(), + softConstraints: SoftConstraint = emptySoftConstraint(), + assumption: Assumption = emptyAssumption(), memoryUpdates: MemoryUpdate = MemoryUpdate(), ) : this(SymbolicSuccess(value), hardConstraints, softConstraints, assumption, memoryUpdates) } diff --git a/utbot-framework/src/main/kotlin/org/utbot/engine/Traverser.kt b/utbot-framework/src/main/kotlin/org/utbot/engine/Traverser.kt index 973a3e1813..12107cecd8 100644 --- a/utbot-framework/src/main/kotlin/org/utbot/engine/Traverser.kt +++ b/utbot-framework/src/main/kotlin/org/utbot/engine/Traverser.kt @@ -66,7 +66,17 @@ import org.utbot.engine.pc.mkNot import org.utbot.engine.pc.mkOr import org.utbot.engine.pc.select import org.utbot.engine.pc.store -import org.utbot.engine.symbolic.* +import org.utbot.engine.symbolic.HardConstraint +import org.utbot.engine.symbolic.SoftConstraint +import org.utbot.engine.symbolic.Assumption +import org.utbot.engine.symbolic.emptyAssumption +import org.utbot.engine.symbolic.emptyHardConstraint +import org.utbot.engine.symbolic.emptySoftConstraint +import org.utbot.engine.symbolic.SymbolicStateUpdate +import org.utbot.engine.symbolic.asHardConstraint +import org.utbot.engine.symbolic.asSoftConstraint +import org.utbot.engine.symbolic.asAssumption +import org.utbot.engine.symbolic.asUpdate import org.utbot.engine.util.trusted.isFromTrustedLibrary import org.utbot.engine.util.statics.concrete.associateEnumSootFieldsWithConcreteValues import org.utbot.engine.util.statics.concrete.isEnumAffectingExternalStatics @@ -1069,8 +1079,8 @@ class Traverser( } // Depending on existance of assumeExpr we have to add corresponding hardConstraints and assumptions - val hardConstraints = if (!isAssumeExpr) negativeCasePathConstraint.asHardConstraint() else EmptyHardConstraint - val assumption = if (isAssumeExpr) negativeCasePathConstraint.asAssumption() else EmptyAssumption + val hardConstraints = if (!isAssumeExpr) negativeCasePathConstraint.asHardConstraint() else emptyHardConstraint() + val assumption = if (isAssumeExpr) negativeCasePathConstraint.asAssumption() else emptyAssumption() val negativeCaseState = environment.state.updateQueued( negativeCaseEdge, @@ -2951,9 +2961,9 @@ class Traverser( return when (expr) { is UtInstanceOfExpression -> { // for now only this type of expression produces deferred updates val onlyMemoryUpdates = expr.symbolicStateUpdate.copy( - hardConstraints = EmptyHardConstraint, - softConstraints = EmptySoftConstraint, - assumptions = EmptyAssumption + hardConstraints = emptyHardConstraint(), + softConstraints = emptySoftConstraint(), + assumptions = emptyAssumption() ) SymbolicStateUpdateForResolvedCondition(onlyMemoryUpdates) } diff --git a/utbot-framework/src/main/kotlin/org/utbot/engine/pc/Query.kt b/utbot-framework/src/main/kotlin/org/utbot/engine/pc/Query.kt index 5b28c878f3..6911237cea 100644 --- a/utbot-framework/src/main/kotlin/org/utbot/engine/pc/Query.kt +++ b/utbot-framework/src/main/kotlin/org/utbot/engine/pc/Query.kt @@ -19,9 +19,6 @@ import kotlinx.collections.immutable.mutate import kotlinx.collections.immutable.persistentHashMapOf import kotlinx.collections.immutable.persistentHashSetOf import kotlinx.collections.immutable.toPersistentSet -import org.utbot.engine.symbolic.Assumption -import org.utbot.engine.symbolic.EmptyAssumption -import org.utbot.engine.symbolic.asAssumption /** * Base class that represents immutable query of constraints to solver. @@ -34,7 +31,7 @@ import org.utbot.engine.symbolic.asAssumption sealed class BaseQuery( open val hard: PersistentSet, open val soft: PersistentSet, - open val assumptions: Assumption, + open val assumptions: PersistentSet, open val status: UtSolverStatus, open val lastAdded: Collection ) { @@ -47,7 +44,7 @@ sealed class BaseQuery( abstract fun with( hard: Collection, soft: Collection, - assumptions: Assumption + assumptions: Collection ): BaseQuery /** @@ -66,7 +63,7 @@ sealed class BaseQuery( class UnsatQuery(hard: PersistentSet) : BaseQuery( hard, soft = persistentHashSetOf(), - EmptyAssumption, + assumptions = persistentHashSetOf(), UtSolverStatusUNSAT(UtSolverStatusKind.UNSAT), lastAdded = emptyList() ) { @@ -74,7 +71,7 @@ class UnsatQuery(hard: PersistentSet) : BaseQuery( override fun with( hard: Collection, soft: Collection, - assumptions: Assumption + assumptions: Collection ): BaseQuery = error("State with UnsatQuery isn't eliminated. Adding constraints to $this isn't allowed.") override fun withStatus(newStatus: UtSolverStatus) = this @@ -94,7 +91,7 @@ class UnsatQuery(hard: PersistentSet) : BaseQuery( data class Query( override val hard: PersistentSet = persistentHashSetOf(), override val soft: PersistentSet = persistentHashSetOf(), - override val assumptions: Assumption = EmptyAssumption, + override val assumptions: PersistentSet = persistentHashSetOf(), override val status: UtSolverStatus = UtSolverStatusUNDEFINED, override val lastAdded: Collection = emptyList(), private val eqs: PersistentMap = persistentHashMapOf(), @@ -196,7 +193,7 @@ data class Query( private fun addSimplified( hard: Collection, soft: Collection, - assumptions: Assumption + assumptions: Collection ): BaseQuery { val addedHard = hard.simplify().filterNot { it is UtTrue } if (addedHard.isEmpty() && soft.isEmpty()) { @@ -287,11 +284,9 @@ data class Query( // Apply simplifications to assumptions in query. // We do not filter out UtFalse here because we need them to get UNSAT in corresponding cases and run concrete instead. val newAssumptions = this.assumptions - .plus(assumptions) - .constraints + .addAll(assumptions) .simplify(newEqs, newLts, newGts) .toPersistentSet() - .asAssumption() val diffHard = newHard - this.hard @@ -315,7 +310,7 @@ data class Query( override fun with( hard: Collection, soft: Collection, - assumptions: Assumption + assumptions: Collection ): BaseQuery { return if (useExpressionSimplification) { addSimplified(hard, soft, assumptions) @@ -323,7 +318,7 @@ data class Query( Query( this.hard.addAll(hard), this.soft.addAll(soft), - this.assumptions.plus(assumptions), + this.assumptions.addAll(assumptions), status.checkFastSatAndReturnStatus(hard), lastAdded = hard, this.eqs 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 6998a41e42..57184aed87 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 @@ -31,7 +31,8 @@ import com.microsoft.z3.Status.UNSATISFIABLE import kotlinx.collections.immutable.PersistentSet import kotlinx.collections.immutable.persistentHashSetOf import mu.KotlinLogging -import org.utbot.engine.symbolic.EmptyAssumption +import org.utbot.engine.symbolic.asAssumption +import org.utbot.engine.symbolic.emptyAssumption import soot.ByteType import soot.CharType import soot.IntType @@ -132,7 +133,7 @@ data class UtSolver constructor( // Constraints that should not be added in the solver as hypothesis. // Instead, we use `check` to find out if they are satisfiable. // It is required to have unsat cores with them. - var assumption: Assumption = EmptyAssumption, + var assumption: Assumption = emptyAssumption(), //new constraints for solver (kind of incremental behavior) private var hardConstraintsNotYetAddedToZ3Solver: PersistentSet = persistentHashSetOf(), @@ -178,7 +179,7 @@ data class UtSolver constructor( fun add(hard: HardConstraint, soft: SoftConstraint, assumption: Assumption): UtSolver { // status can implicitly change here to UNDEFINED or UNSAT - val newConstraints = constraints.with(hard.constraints, soft.constraints, assumption) + val newConstraints = constraints.with(hard.constraints, soft.constraints, assumption.constraints) val wantClone = (expectUndefined && newConstraints.status is UtSolverStatusUNDEFINED) || (!expectUndefined && newConstraints.status !is UtSolverStatusUNSAT) @@ -205,7 +206,7 @@ data class UtSolver constructor( copy( constraints = constraintsWithStatus, hardConstraintsNotYetAddedToZ3Solver = newConstraints.hard, - assumption = newConstraints.assumptions, + assumption = newConstraints.assumptions.asAssumption(), z3Solver = context.mkSolver().also { it.setParameters(params) }, ) } diff --git a/utbot-framework/src/main/kotlin/org/utbot/engine/symbolic/SymbolicStateUpdate.kt b/utbot-framework/src/main/kotlin/org/utbot/engine/symbolic/SymbolicStateUpdate.kt index a6a4e44e61..63c73e60e6 100644 --- a/utbot-framework/src/main/kotlin/org/utbot/engine/symbolic/SymbolicStateUpdate.kt +++ b/utbot-framework/src/main/kotlin/org/utbot/engine/symbolic/SymbolicStateUpdate.kt @@ -27,21 +27,29 @@ open class HardConstraint( ) : Constraint(constraints) { override fun plus(other: HardConstraint): HardConstraint = HardConstraint(addConstraints(other.constraints)) + + companion object { + internal val EMPTY: HardConstraint = HardConstraint() + } } -object EmptyHardConstraint : HardConstraint() +fun emptyHardConstraint(): HardConstraint = HardConstraint.EMPTY /** * Represents soft constraints. */ -open class SoftConstraint( +class SoftConstraint( constraints: Set = emptySet() ) : Constraint(constraints) { override fun plus(other: SoftConstraint): SoftConstraint = SoftConstraint(addConstraints(other.constraints)) + + companion object { + internal val EMPTY: SoftConstraint = SoftConstraint() + } } -object EmptySoftConstraint : SoftConstraint() +fun emptySoftConstraint(): SoftConstraint = SoftConstraint.EMPTY /** * Represent constraints that must be satisfied for symbolic execution. @@ -50,15 +58,19 @@ object EmptySoftConstraint : SoftConstraint() * * @see */ -open class Assumption( +class Assumption( constraints: Set = emptySet() ): Constraint(constraints) { override fun plus(other: Assumption): Assumption = Assumption(addConstraints(other.constraints)) override fun toString() = constraints.joinToString(System.lineSeparator()) + + companion object { + internal val EMPTY: Assumption = Assumption() + } } -object EmptyAssumption : Assumption() +fun emptyAssumption(): Assumption = Assumption.EMPTY /** * Represents one or more updates that can be applied to [SymbolicState]. @@ -66,9 +78,9 @@ object EmptyAssumption : Assumption() * TODO: move [localMemoryUpdates] to another place */ data class SymbolicStateUpdate( - val hardConstraints: HardConstraint = EmptyHardConstraint, - val softConstraints: SoftConstraint = EmptySoftConstraint, - val assumptions: Assumption = EmptyAssumption, + val hardConstraints: HardConstraint = emptyHardConstraint(), + val softConstraints: SoftConstraint = emptySoftConstraint(), + val assumptions: Assumption = emptyAssumption(), val memoryUpdates: MemoryUpdate = MemoryUpdate(), val localMemoryUpdates: LocalMemoryUpdate = LocalMemoryUpdate() ) {