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

Approximation of tree incrementality for Z3 solver #104

Merged
merged 2 commits into from
Sep 15, 2023

Conversation

Columpio
Copy link
Collaborator

@Columpio Columpio commented Aug 3, 2023

No description provided.

@Columpio Columpio force-pushed the columpio/tree-incrementality branch 4 times, most recently from a0c8bc0 to dbe9a21 Compare August 8, 2023 12:50
@Columpio Columpio force-pushed the columpio/tree-incrementality branch 4 times, most recently from 9ee7ed9 to 11492ba Compare August 15, 2023 11:09
@codecov-commenter
Copy link

codecov-commenter commented Aug 15, 2023

Codecov Report

Merging #104 (78ff83a) into main (ede8d25) will increase coverage by 0.26%.
The diff coverage is 81.21%.

❗ Current head 78ff83a differs from pull request most recent head 926bd20. Consider uploading reports for the commit 926bd20 to get more accurate results

@@            Coverage Diff             @@
##             main     #104      +/-   ##
==========================================
+ Coverage   65.41%   65.68%   +0.26%     
==========================================
  Files         211      212       +1     
  Lines       28678    29083     +405     
  Branches     6374     6430      +56     
==========================================
+ Hits        18759    19102     +343     
- Misses       7431     7464      +33     
- Partials     2488     2517      +29     
Files Changed Coverage Δ
include/klee/Expr/Constraints.h 50.00% <ø> (ø)
include/klee/Solver/IncompleteSolver.h 100.00% <ø> (ø)
include/klee/Solver/SolverImpl.h 50.00% <ø> (ø)
lib/Core/ImpliedValue.cpp 0.00% <0.00%> (ø)
lib/Core/TimingSolver.h 100.00% <ø> (ø)
lib/Solver/SolverCmdLine.cpp 100.00% <ø> (ø)
lib/Solver/Z3Builder.cpp 28.57% <0.00%> (ø)
lib/Solver/IncompleteSolver.cpp 12.65% <33.33%> (-4.63%) ⬇️
lib/Core/TimingSolver.cpp 50.27% <47.82%> (+2.85%) ⬆️
lib/Solver/ValidatingSolver.cpp 29.50% <60.00%> (+1.77%) ⬆️
... and 20 more

... and 5 files with indirect coverage changes

@Columpio Columpio force-pushed the columpio/tree-incrementality branch 6 times, most recently from 66c8081 to a406b44 Compare August 21, 2023 09:44
@Columpio Columpio force-pushed the columpio/tree-incrementality branch 7 times, most recently from dbd54db to dd2a4f0 Compare August 29, 2023 07:37
@Columpio Columpio force-pushed the columpio/tree-incrementality branch 3 times, most recently from 60b21a4 to 926bd20 Compare September 12, 2023 13:53
Solvers:
- Fixed CexCachingSolver so that the core solver (Z3/STP) does not get stupid queries, like `false` or `not false`

Tests:
- Changed total queries in `Feature/DanglingConcreteReadExpr.c` test from 2 to 1 as its first query to Z3 was `not false`
- Decreased QCexCacheHits in `Solver/CexCacheValidityCoresCheck.c` test by one for the same reason
- Activated tests in `test/Solver`
@misonijnik misonijnik marked this pull request as ready for review September 15, 2023 21:00
@misonijnik misonijnik merged commit 7f5db38 into main Sep 15, 2023
20 checks passed
@Columpio Columpio deleted the columpio/tree-incrementality branch September 18, 2023 07:41
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Labels
None yet
Projects
None yet
Development

Successfully merging this pull request may close these issues.

3 participants