Added simplification/rewriting for assumptions (#940)

Author: Damtev

utbot-framework-test/src/test/kotlin/org/utbot/engine/pc/QueryOptimizationsTest.kt

@@ -51,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()).also {
+        this.with(hard = exprs.toList(), soft = emptyList(), assumptions = emptyList()).also {
             checker(it)
         }
 

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,

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)
 }

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

@@ -69,6 +69,9 @@ 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.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
@@ -1076,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 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 +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 = HardConstraint(),
-                    softConstraints = SoftConstraint()
+                    hardConstraints = emptyHardConstraint(),
+                    softConstraints = emptySoftConstraint(),
+                    assumptions = emptyAssumption()
                 )
                 SymbolicStateUpdateForResolvedCondition(onlyMemoryUpdates)
             }

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

@@ -31,6 +31,7 @@ import kotlinx.collections.immutable.toPersistentSet
 sealed class BaseQuery(
     open val hard: PersistentSet<UtBoolExpression>,
     open val soft: PersistentSet<UtBoolExpression>,
+    open val assumptions: PersistentSet<UtBoolExpression>,
     open val status: UtSolverStatus,
     open val lastAdded: Collection<UtBoolExpression>
 ) {
@@ -40,7 +41,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<UtBoolExpression>, soft: Collection<UtBoolExpression>): BaseQuery
+    abstract fun with(
+        hard: Collection<UtBoolExpression>,
+        soft: Collection<UtBoolExpression>,
+        assumptions: Collection<UtBoolExpression>
+    ): BaseQuery
 
     /**
      * Set [status] of the query.
@@ -55,11 +60,19 @@ sealed class BaseQuery(
  * UnsatQuery.[status] is [UtSolverStatusUNSAT].
  * UnsatQuery.[lastAdded] = [emptyList]
  */
-class UnsatQuery(hard: PersistentSet<UtBoolExpression>) :
-    BaseQuery(hard, persistentHashSetOf(), UtSolverStatusUNSAT(UtSolverStatusKind.UNSAT), emptyList()) {
+class UnsatQuery(hard: PersistentSet<UtBoolExpression>) : BaseQuery(
+    hard,
+    soft = persistentHashSetOf(),
+    assumptions = persistentHashSetOf(),
+    UtSolverStatusUNSAT(UtSolverStatusKind.UNSAT),
+    lastAdded = emptyList()
+) {
 
-    override fun with(hard: Collection<UtBoolExpression>, soft: Collection<UtBoolExpression>): BaseQuery =
-        error("State with UnsatQuery isn't eliminated. Adding constraints to $this isn't allowed.")
+    override fun with(
+        hard: Collection<UtBoolExpression>,
+        soft: Collection<UtBoolExpression>,
+        assumptions: Collection<UtBoolExpression>
+    ): BaseQuery = error("State with UnsatQuery isn't eliminated. Adding constraints to $this isn't allowed.")
 
     override fun withStatus(newStatus: UtSolverStatus) = this
 
@@ -78,12 +91,13 @@ class UnsatQuery(hard: PersistentSet<UtBoolExpression>) :
 data class Query(
     override val hard: PersistentSet<UtBoolExpression> = persistentHashSetOf(),
     override val soft: PersistentSet<UtBoolExpression> = persistentHashSetOf(),
+    override val assumptions: PersistentSet<UtBoolExpression> = persistentHashSetOf(),
     override val status: UtSolverStatus = UtSolverStatusUNDEFINED,
     override val lastAdded: Collection<UtBoolExpression> = emptyList(),
     private val eqs: PersistentMap<UtExpression, UtExpression> = persistentHashMapOf(),
     private val lts: PersistentMap<UtExpression, Long> = persistentHashMapOf(),
     private val gts: PersistentMap<UtExpression, Long> = persistentHashMapOf()
-) : BaseQuery(hard, soft, status, lastAdded) {
+) : BaseQuery(hard, soft, assumptions, status, lastAdded) {
 
     val rewriter: RewritingVisitor
         get() = RewritingVisitor(eqs, lts, gts)
@@ -179,6 +193,7 @@ data class Query(
     private fun addSimplified(
         hard: Collection<UtBoolExpression>,
         soft: Collection<UtBoolExpression>,
+        assumptions: Collection<UtBoolExpression>
     ): BaseQuery {
         val addedHard = hard.simplify().filterNot { it is UtTrue }
         if (addedHard.isEmpty() && soft.isEmpty()) {
@@ -266,20 +281,48 @@ 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
+            .addAll(assumptions)
+            .simplify(newEqs, newLts, newGts)
+            .toPersistentSet()
+
         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
+        )
     }
 
     /**
      * Add constraints to query and apply simplifications if [useExpressionSimplification] is true.
      * @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<UtBoolExpression>, soft: Collection<UtBoolExpression>): BaseQuery {
+    override fun with(
+        hard: Collection<UtBoolExpression>,
+        soft: Collection<UtBoolExpression>,
+        assumptions: Collection<UtBoolExpression>
+    ): 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.addAll(assumptions),
+                status.checkFastSatAndReturnStatus(hard),
+                lastAdded = hard,
+                this.eqs
+            )
         }
     }
 

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

@@ -31,6 +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.asAssumption
+import org.utbot.engine.symbolic.emptyAssumption
 import soot.ByteType
 import soot.CharType
 import soot.IntType
@@ -131,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 = Assumption(),
+    var assumption: Assumption = emptyAssumption(),
 
     //new constraints for solver (kind of incremental behavior)
     private var hardConstraintsNotYetAddedToZ3Solver: PersistentSet<UtBoolExpression> = persistentHashSetOf(),
@@ -175,9 +177,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.constraints)
         val wantClone = (expectUndefined && newConstraints.status is UtSolverStatusUNDEFINED)
                 || (!expectUndefined && newConstraints.status !is UtSolverStatusUNSAT)
 
@@ -204,7 +206,7 @@ data class UtSolver constructor(
             copy(
                 constraints = constraintsWithStatus,
                 hardConstraintsNotYetAddedToZ3Solver = newConstraints.hard,
-                assumption = this.assumption + assumption,
+                assumption = newConstraints.assumptions.asAssumption(),
                 z3Solver = context.mkSolver().also { it.setParameters(params) },
             )
         }

utbot-framework/src/main/kotlin/org/utbot/engine/symbolic/SymbolicStateUpdate.kt

@@ -22,13 +22,19 @@ sealed class Constraint<T : Constraint<T>>(constraints: Set<UtBoolExpression> =
 /**
  * Represents hard constraints.
  */
-class HardConstraint(
+open class HardConstraint(
     constraints: Set<UtBoolExpression> = emptySet()
 ) : Constraint<HardConstraint>(constraints) {
     override fun plus(other: HardConstraint): HardConstraint =
         HardConstraint(addConstraints(other.constraints))
+
+    companion object {
+        internal val EMPTY: HardConstraint = HardConstraint()
+    }
 }
 
+fun emptyHardConstraint(): HardConstraint = HardConstraint.EMPTY
+
 /**
  * Represents soft constraints.
  */
@@ -37,8 +43,14 @@ class SoftConstraint(
 ) : Constraint<SoftConstraint>(constraints) {
     override fun plus(other: SoftConstraint): SoftConstraint =
         SoftConstraint(addConstraints(other.constraints))
+
+    companion object {
+        internal val EMPTY: SoftConstraint = SoftConstraint()
+    }
 }
 
+fun emptySoftConstraint(): SoftConstraint = SoftConstraint.EMPTY
+
 /**
  * Represent constraints that must be satisfied for symbolic execution.
  * At the same time, if they don't, the state they belong to still
@@ -52,17 +64,23 @@ class Assumption(
     override fun plus(other: Assumption): Assumption = Assumption(addConstraints(other.constraints))
 
     override fun toString() = constraints.joinToString(System.lineSeparator())
+
+    companion object {
+        internal val EMPTY: Assumption = Assumption()
+    }
 }
 
+fun emptyAssumption(): Assumption = Assumption.EMPTY
+
 /**
  * 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 +125,7 @@ fun Collection<UtBoolExpression>.asSoftConstraint() = SoftConstraint(transformTo
 
 fun UtBoolExpression.asSoftConstraint() = SoftConstraint(setOf(this))
 
-fun Collection<UtBoolExpression>.asAssumption() = Assumption(toSet())
+fun Collection<UtBoolExpression>.asAssumption() = Assumption(transformToSet())
 
 fun UtBoolExpression.asAssumption() = Assumption(setOf(this))
 

utbot-sample/src/main/java/org/utbot/examples/stream/BaseStreamExample.java

@@ -68,7 +68,7 @@ boolean distinctExample(List<Integer> list) {
 
         int prevSize = list.size();
 
-        int newSize = list.stream().distinct().toArray().length;
+        int newSize = (int) list.stream().distinct().count();
 
         return prevSize != newSize;
     }