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.

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

A synchronous mode for SMT queries (+ tactic), plus a change to --split_queries #2776

Merged
merged 15 commits into from
Apr 18, 2023
Merged

A synchronous mode for SMT queries (+ tactic), plus a change to --split_queries #2776

Changes from 1 commit
Commits
Show all changes
15 commits
Select commit Hold shift + click to select a range
b5ec73c
typechecker: env: remove stale dummy_solver
mtzguido Nov 14, 2022
b8ff498
smtencoding: refactoring the solver query process
mtzguido Nov 29, 2022
d5293e0
smtencoding: introduce solve_sync
mtzguido Nov 29, 2022
c0b8285
tactics: introduce smt_sync
mtzguido Nov 29, 2022
6093262
tests: add a test for smt_sync
mtzguido Nov 29, 2022
d7e1851
options: make --split_queries tri-valued: no, on_failure, always
mtzguido Apr 5, 2023
649ae08
snap
mtzguido Apr 10, 2023
1f12660
fix uses of --split_queries
mtzguido Apr 10, 2023
a6578ef
tactics: making t_smt_sync take an explicit vconfig
mtzguido Apr 11, 2023
e5c126c
snap
mtzguido Apr 11, 2023
339e5a0
CHANGES.md: add a note about --split_queries
mtzguido Apr 11, 2023
3e292f8
ocaml bindings for new tactic primitives
mtzguido Apr 11, 2023
e6ee126
snap
mtzguido Apr 11, 2023
0eb3a3c
update expected output (line number changed)
mtzguido Apr 11, 2023
07c0872
Merge branch 'master' of github:FStarLang/FStar into _guido_split_que…
mtzguido Apr 17, 2023
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
CHANGES.md: add a note about --split_queries
  • Loading branch information
@mtzguido
mtzguido committed Apr 11, 2023
commit 339e5a0d630714c674e1134d6774cc095a947370
8 changes: 8 additions & 0 deletions CHANGES.md
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -569,6 +569,14 @@ Guidelines for the changelog:
which to enable profiling. The output of F* on its finished
message changed to not print the time it took to verify a module.

* [PR #2776](https://github.com/FStarLang/FStar/pull/2776): The
`--split_queries` option now takes an argument, one of `no`,
`on_failure` and `always`. The default is `on_failure`, with
the same behavior as previously (split a query and retry when
the SMT solver does not return a helpful error). Using
`--split_queries always` mimics the old `--split_queries`,
splitting all queries eagerly. Using `--split_queries no` disables
splitting altogether.

## Editors

Expand Down