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

Jump to bottom

Incremental version of the solver #1000

Open
wants to merge 17 commits into
base: next
Choose a base branch
from
Open

Incremental version of the solver #1000

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
17 commits
Select commit Hold shift + click to select a range
9cf1828
First version of full incremental solving loop
Stevendeo Dec 1, 2023
6790c68
Update tests
Stevendeo Mar 22, 2024
2fd8303
Interleaving full imperative and partial imperative modes
Stevendeo Mar 22, 2024
e918fa0
Update tests
Stevendeo Mar 22, 2024
c985aed
Reactivating abstract value printing and update tests
Stevendeo Mar 25, 2024
0f0dd69
Documentation and small fix
Stevendeo Mar 25, 2024
c10ad82
Style
Stevendeo Mar 25, 2024
4bbfc84
Indent
Stevendeo Mar 25, 2024
e844f17
Fix for test tests/cc/testfile-ac_cc002.ae
Stevendeo Mar 25, 2024
cfbc8bc
Poetry
Stevendeo Mar 28, 2024
f03b2e1
Disactivating push & pop in queries in non incremental mode
Stevendeo Apr 4, 2024
baba255
Linter
Stevendeo Apr 4, 2024
e02c791
Reinitializing current path to avoid double replay
Stevendeo Apr 5, 2024
cf3b8a2
Fix timeout issues
Stevendeo Apr 5, 2024
97353c0
Rename function
Stevendeo Apr 5, 2024
a91b605
Removing unit_tenv_queue
Stevendeo Apr 5, 2024
a0f518e
Fix for another issue I need to test my PR
Stevendeo Apr 5, 2024
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
8 changes: 6 additions & 2 deletions src/bin/common/parse_command.ml
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -303,7 +303,7 @@ let mk_context_opt replay replay_all_used_context replay_used_context
let mk_execution_opt input_format parse_only ()
preludes no_locs_in_answers colors_in_output no_headers_in_output
no_formatting_in_output no_forced_flush_in_output pretty_output
type_only type_smt2
type_only type_smt2 imperative_mode
=
let answers_with_loc = not no_locs_in_answers in
let output_with_colors = colors_in_output || pretty_output in
Expand All @@ -321,6 +321,7 @@ let mk_execution_opt input_format parse_only ()
set_type_only type_only;
set_type_smt2 type_smt2;
set_preludes preludes;
set_imperative_mode imperative_mode;
`Ok()

let mk_internal_opt
Expand Down Expand Up @@ -744,12 +745,15 @@ let parse_execution_opt =
let doc = "Stop after SMT2 typing." in
Arg.(value & flag & info ["type-smt2"] ~docs ~doc) in

let imperative_smt =
let doc = "Starts Alt-Ergo in incremental mode" in
Arg.(value & flag & info ["incremental-mode"] ~docs ~doc) in

Term.(ret (const mk_execution_opt $
input_format $ parse_only $ parsers $ preludes $
no_locs_in_answers $ colors_in_output $ no_headers_in_output $
no_formatting_in_output $ no_forced_flush_in_output $
pretty_output $ type_only $ type_smt2
pretty_output $ type_only $ type_smt2 $ imperative_smt
))

let parse_halt_opt =
Expand Down
Loading
Loading