-
Notifications
You must be signed in to change notification settings - Fork 80
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
fix --early-exit #437
Merged
+1,544
−857
Merged
fix --early-exit #437
Changes from 1 commit
Commits
Show all changes
46 commits
Select commit
Hold shift + click to select a range
93c32f6
add build directory to .gitignore
0xkarmacoma d419691
add psutil to dependencies
0xkarmacoma 57151cf
add PopenFuture and PopenExecutor
0xkarmacoma 771dea6
WIP: add traces.py
0xkarmacoma 076caae
XXX sort data into contract, function and path contexts
0xkarmacoma 926e733
XXX early exit wired actually wired
0xkarmacoma e72b36d
add triage for solver models
0xkarmacoma 45d9e67
add basic smtlib parsing
0xkarmacoma 1bdafec
actually parse external solver output using smtlib
0xkarmacoma db346c0
fix counterexample output
0xkarmacoma bfe126d
make z3 the default --solver-command (so we always dump queries)
0xkarmacoma cdf4e16
bring back refinement
0xkarmacoma 175ede3
fix solve invocation in setup
0xkarmacoma cf85376
bring back timeouts, clean children after timeout
0xkarmacoma ea3d493
migrate build output parsing function in build.py
0xkarmacoma 2239231
move solving-related functions to solve.py
0xkarmacoma 19c772f
fix setup_exs_no_error access pattern
0xkarmacoma 5d1a24f
merge smtlib.py into solve.py
0xkarmacoma b1ebdc6
adjust halmos_var_pattern to support p_ prefix
0xkarmacoma d847464
speed up early exit
0xkarmacoma 03ed948
bring back model output in solve_end_to_end
0xkarmacoma a6fd067
shutdown executors on signal
0xkarmacoma f41a3cb
disable ExecutorRegistry().shutdown_all() for now
0xkarmacoma 7b38cdc
fix bad merge
0xkarmacoma 0125a3d
fix z3 thread safety issue (--print-failed-states disabled for now)
0xkarmacoma 51657ba
fix setup() with multiple paths
0xkarmacoma 01dcb3b
share a SolvingContext between FunctionContext and PathContext
0xkarmacoma 85ca04c
use tempfile and path to manage smt2 files
0xkarmacoma 5831899
TemporaryDirectory 3.11 compatibility support
0xkarmacoma 61834c0
trying a thing on windows
0xkarmacoma d3a63a3
try specifying full path to z3
0xkarmacoma 955f410
warn if z3 is not found
0xkarmacoma 9355d09
update uv version
0xkarmacoma 9859579
fix bad reference
0xkarmacoma b9f2985
XXX print path to see what's up on windows ci
0xkarmacoma 5068e59
finish merge
0xkarmacoma 60ef79c
print venv contents
0xkarmacoma 5803051
dynamically locate z3 in the venv
0xkarmacoma 1fc8649
fix: avoid raising when path exploration > first cex
0xkarmacoma f705954
cleanup: print trace counterexample in the right place
0xkarmacoma 3a501ae
bring back the executor shutdown in on_exit
0xkarmacoma d7dddf8
fix status display condition
0xkarmacoma 9a9d3cd
fix unsafe setup_ex.path.to_smt2() access
0xkarmacoma 7d5d350
simplify PotentialModel
0xkarmacoma e918408
only render paths to string when debug is active
0xkarmacoma 0b7dc6e
switch halmos-solady to bitwuzla
0xkarmacoma File filter
Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
There are no files selected for viewing
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Oops, something went wrong.
Add this suggestion to a batch that can be applied as a single commit.
This suggestion is invalid because no changes were made to the code.
Suggestions cannot be applied while the pull request is closed.
Suggestions cannot be applied while viewing a subset of changes.
Only one suggestion per line can be applied in a batch.
Add this suggestion to a batch that can be applied as a single commit.
Applying suggestions on deleted lines is not supported.
You must change the existing code in this line in order to create a valid suggestion.
Outdated suggestions cannot be applied.
This suggestion has been applied or marked resolved.
Suggestions cannot be applied from pending reviews.
Suggestions cannot be applied on multi-line comments.
Suggestions cannot be applied while the pull request is queued to merge.
Suggestion cannot be applied right now. Please check back later.
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
oh wow. great catch. (curious why it wasn't caught earlier by my performance regression testing.)
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
it has a disproportionate effect on the morpho test because it bumps against the loop limit and also has very complex path conditions, not much visible effect on other tests