Skip to content

Primitive Stream wrappers (no laziness and source mutations support) #871

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.

Sign up for GitHub

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

Merged
Damtev merged 19 commits into from
Sep 28, 2022
Merged

Primitive Stream wrappers (no laziness and source mutations support) #871

Show file tree
Hide file tree
Changes from 1 commit
Commits
Show all changes
19 commits
Select commit Hold shift + click to select a range
2b60de7
Fixed repeated `hashCode` calculation for `Edge`
Damtev Jul 12, 2022
b362960
Disabled strange failed naming check
Damtev Jul 22, 2022
adb0cec
Implemented wrappers for primitive streams
Damtev Jul 21, 2022
fc5d7eb
Added tests for primitive streams
Damtev Jul 21, 2022
91c6b74
Added `toArray` without ClassCastException check API
Damtev Jul 21, 2022
9797973
Restricted steps limit for a few tests (HACK)
Damtev Aug 1, 2022
75b2de8
Fixed UNSAT core debug logging
Damtev Sep 7, 2022
9ce941e
Fixed rebase errors
Damtev Sep 7, 2022
4a69e0b
Added wrapped methods for creating streams from primitive arrays
Damtev Sep 7, 2022
01ad8e5
Fixed failed tests
Damtev Sep 7, 2022
47b1b7b
Disabled distinct test
Damtev Sep 14, 2022
58c15a2
Fixed array casts
Damtev Sep 16, 2022
ff79a92
Fixed review issues
Damtev Sep 26, 2022
78c9c4f
More fixes for review issues
Damtev Sep 27, 2022
40ebea6
Fixed type resolving
Damtev Sep 27, 2022
a5d9da8
Fixed wrong resolved values for a primitive stream as a parameter
Damtev Sep 27, 2022
2aeb263
Marked primitive stream tests as slow
Damtev Sep 28, 2022
e3381ef
Fixed last review issues
Damtev Sep 28, 2022
d9e4a42
Marked mapTo* primitive stream tests as slow
Damtev Sep 28, 2022
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
Prev Previous commit
Next Next commit
Fixed UNSAT core debug logging
  • Loading branch information
@Damtev
Damtev committed Sep 28, 2022
commit 75b2de8b65d3e71a31957e0c3cfc80f2244b99b4
2 changes: 1 addition & 1 deletion utbot-framework/src/main/kotlin/org/utbot/engine/Memory.kt
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -535,7 +535,7 @@ class TypeRegistry {

if (sootClass.type.isJavaLangObject()) finalCost += -32

if (sootClass.isAnonymous) finalCost -= 128
if (sootClass.isAnonymous) finalCost += -128

if (sootClass.name.contains("$")) finalCost += -4096

Expand Down
17 changes: 8 additions & 9 deletions utbot-framework/src/main/kotlin/org/utbot/engine/pc/UtSolver.kt
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -272,9 +272,12 @@ data class UtSolver constructor(
UNSATISFIABLE -> {
val unsatCore = z3Solver.unsatCore

val failedSoftConstraints = unsatCore.filter { it in translatedSoft.keys }
val failedAssumptions = unsatCore.filter { it in translatedAssumptions.keys }

// if we don't have any soft constraints and enabled unsat cores
// for hard constraints, then calculate it and print the result using the logger
if (translatedSoft.isEmpty() && translatedAssumptions.isEmpty() && UtSettings.enableUnsatCoreCalculationForHardConstraints) {
if (failedSoftConstraints.isEmpty() && failedAssumptions.isEmpty() && UtSettings.enableUnsatCoreCalculationForHardConstraints) {
with(context.mkSolver()) {
check(*z3Solver.assertions)
val constraintsInUnsatCore = this.unsatCore.toList()
Expand All @@ -288,20 +291,16 @@ data class UtSolver constructor(
// an unsat core for hard constraints
if (unsatCore.isEmpty()) return UNSAT

val failedSoftConstraints = unsatCore.filter { it in translatedSoft.keys }

if (failedSoftConstraints.isNotEmpty()) {
failedSoftConstraints.forEach { translatedSoft.remove(it) }
// remove soft constraints first, only then try to remove assumptions
continue
}

unsatCore
.filter { it in translatedAssumptions.keys }
.forEach {
assumptionsInUnsatCore += translatedAssumptions.getValue(it)
translatedAssumptions.remove(it)
}
failedAssumptions.forEach {
assumptionsInUnsatCore += translatedAssumptions.getValue(it)
translatedAssumptions.remove(it)
}
}
else -> {
logger.debug { "Reason of UNKNOWN: ${z3Solver.reasonUnknown}" }
Expand Down