Skip to content

Commit a97bda1

Browse files
authored
Remove unsat states from invokes (#1071)
1 parent 61ece8e commit a97bda1

File tree

3 files changed

+39
-0
lines changed
  • utbot-framework/src/main/kotlin/org/utbot/engine
  • utbot-framework-test/src/test/kotlin/org/utbot/examples/collections
  • utbot-sample/src/main/java/org/utbot/examples/collections

3 files changed

+39
-0
lines changed

utbot-framework-test/src/test/kotlin/org/utbot/examples/collections/MapsPart1Test.kt

+13
Original file line numberDiff line numberDiff line change
@@ -1,5 +1,6 @@
11
package org.utbot.examples.collections
22

3+
import org.junit.jupiter.api.Tag
34
import org.utbot.tests.infrastructure.UtValueTestCaseChecker
45
import org.utbot.tests.infrastructure.AtLeast
56
import org.utbot.tests.infrastructure.DoNotCalculate
@@ -10,6 +11,7 @@ import org.utbot.framework.plugin.api.MockStrategyApi
1011
import org.junit.jupiter.api.Test
1112
import org.utbot.testcheckers.eq
1213
import org.utbot.testcheckers.ge
14+
import org.utbot.testcheckers.withPushingStateFromPathSelectorForConcrete
1315
import org.utbot.testcheckers.withoutMinimization
1416
import org.utbot.tests.infrastructure.CodeGeneration
1517

@@ -149,6 +151,17 @@ internal class MapsPart1Test : UtValueTestCaseChecker(
149151
)
150152
}
151153

154+
@Test
155+
@Tag("slow") // it takes about 20 minutes to execute this test
156+
fun testMapOperator() {
157+
withPushingStateFromPathSelectorForConcrete {
158+
check(
159+
Maps::mapOperator,
160+
ignoreExecutionsNumber
161+
)
162+
}
163+
}
164+
152165
@Test
153166
fun testComputeValue() {
154167
check(

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

+10
Original file line numberDiff line numberDiff line change
@@ -46,6 +46,7 @@ import org.utbot.engine.pc.UtPrimitiveSort
4646
import org.utbot.engine.pc.UtShortSort
4747
import org.utbot.engine.pc.UtSolver
4848
import org.utbot.engine.pc.UtSolverStatusSAT
49+
import org.utbot.engine.pc.UtSolverStatusUNSAT
4950
import org.utbot.engine.pc.UtSubNoOverflowExpression
5051
import org.utbot.engine.pc.UtTrue
5152
import org.utbot.engine.pc.addrEq
@@ -2535,6 +2536,15 @@ class Traverser(
25352536
*/
25362537
val artificialMethodOverride = overrideInvocation(invocation, target = null)
25372538

2539+
// The problem here is that we might have an unsat current state.
2540+
// We get states with `SAT` last status only for traversing,
2541+
// but during the parameters resolving this status might be changed.
2542+
// It happens inside the `org.utbot.engine.Traverser.initStringLiteral` function.
2543+
// So, if it happens, we should just drop the state we processing now.
2544+
if (environment.state.solver.lastStatus is UtSolverStatusUNSAT) {
2545+
return emptyList()
2546+
}
2547+
25382548
// If so, return the result of the override
25392549
if (artificialMethodOverride.success) {
25402550
if (artificialMethodOverride.results.size > 1) {

utbot-sample/src/main/java/org/utbot/examples/collections/Maps.java

+16
Original file line numberDiff line numberDiff line change
@@ -1,7 +1,9 @@
11
package org.utbot.examples.collections;
22

3+
import java.util.ArrayList;
34
import java.util.HashMap;
45
import java.util.LinkedHashMap;
6+
import java.util.List;
57
import java.util.Map;
68

79
public class Maps {
@@ -245,4 +247,18 @@ CustomClass removeCustomObject(Map<CustomClass, CustomClass> map, int i) {
245247
return removed;
246248
}
247249
}
250+
251+
public List<String> mapOperator(Map<String, String> map) {
252+
List<String> result = new ArrayList<>();
253+
for (Map.Entry<String, String> entry : map.entrySet()) {
254+
if (entry.getValue().equals("key")) {
255+
result.add(entry.getKey());
256+
}
257+
}
258+
if (result.size() > 1) {
259+
return result;
260+
} else {
261+
return new ArrayList<>(map.values());
262+
}
263+
}
248264
}

0 commit comments

Comments
 (0)