Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Remove unsat states from invokes #1071

Merged
merged 1 commit into from
Oct 5, 2022
Merged
Show file tree
Hide file tree
Changes from all commits
Commits
File filter

Filter by extension

Filter by extension

Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
Original file line number Diff line number Diff line change
@@ -1,5 +1,6 @@
package org.utbot.examples.collections

import org.junit.jupiter.api.Tag
import org.utbot.tests.infrastructure.UtValueTestCaseChecker
import org.utbot.tests.infrastructure.AtLeast
import org.utbot.tests.infrastructure.DoNotCalculate
Expand All @@ -10,6 +11,7 @@ import org.utbot.framework.plugin.api.MockStrategyApi
import org.junit.jupiter.api.Test
import org.utbot.testcheckers.eq
import org.utbot.testcheckers.ge
import org.utbot.testcheckers.withPushingStateFromPathSelectorForConcrete
import org.utbot.testcheckers.withoutMinimization
import org.utbot.tests.infrastructure.CodeGeneration

Expand Down Expand Up @@ -149,6 +151,17 @@ internal class MapsPart1Test : UtValueTestCaseChecker(
)
}

@Test
@Tag("slow") // it takes about 20 minutes to execute this test
fun testMapOperator() {
withPushingStateFromPathSelectorForConcrete {
check(
Maps::mapOperator,
ignoreExecutionsNumber
)
}
}

@Test
fun testComputeValue() {
check(
Expand Down
10 changes: 10 additions & 0 deletions utbot-framework/src/main/kotlin/org/utbot/engine/Traverser.kt
Original file line number Diff line number Diff line change
Expand Up @@ -46,6 +46,7 @@ import org.utbot.engine.pc.UtPrimitiveSort
import org.utbot.engine.pc.UtShortSort
import org.utbot.engine.pc.UtSolver
import org.utbot.engine.pc.UtSolverStatusSAT
import org.utbot.engine.pc.UtSolverStatusUNSAT
import org.utbot.engine.pc.UtSubNoOverflowExpression
import org.utbot.engine.pc.UtTrue
import org.utbot.engine.pc.addrEq
Expand Down Expand Up @@ -2535,6 +2536,15 @@ class Traverser(
*/
val artificialMethodOverride = overrideInvocation(invocation, target = null)

// The problem here is that we might have an unsat current state.
// We get states with `SAT` last status only for traversing,
// but during the parameters resolving this status might be changed.
// It happens inside the `org.utbot.engine.Traverser.initStringLiteral` function.
// So, if it happens, we should just drop the state we processing now.
if (environment.state.solver.lastStatus is UtSolverStatusUNSAT) {
return emptyList()
}

// If so, return the result of the override
if (artificialMethodOverride.success) {
if (artificialMethodOverride.results.size > 1) {
Expand Down
Original file line number Diff line number Diff line change
@@ -1,7 +1,9 @@
package org.utbot.examples.collections;

import java.util.ArrayList;
import java.util.HashMap;
import java.util.LinkedHashMap;
import java.util.List;
import java.util.Map;

public class Maps {
Expand Down Expand Up @@ -245,4 +247,18 @@ CustomClass removeCustomObject(Map<CustomClass, CustomClass> map, int i) {
return removed;
}
}

public List<String> mapOperator(Map<String, String> map) {
List<String> result = new ArrayList<>();
for (Map.Entry<String, String> entry : map.entrySet()) {
if (entry.getValue().equals("key")) {
result.add(entry.getKey());
}
}
if (result.size() > 1) {
return result;
} else {
return new ArrayList<>(map.values());
}
}
}