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

Only pass stable reluctant_vs to postsolver #960

Merged
merged 3 commits into from
Dec 27, 2022
Merged

Only pass stable reluctant_vs to postsolver #960

Changes from all commits
Commits
Show all changes
3 commits
Select commit Hold shift + click to select a range
5b9503d
Reluctant incremental analysis: only pass stable reluctant_vs to post…
jerhard Dec 23, 2022
9093218
Use stable_reluctant_vs also for reachable and superstable.
jerhard Dec 23, 2022
9c423ef
Remove debug printout.
jerhard Dec 23, 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
9 changes: 5 additions & 4 deletions src/solvers/td3.ml
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -725,7 +725,6 @@ module Base =
HM.iter (fun x (old_rho, old_infl) ->
ignore @@ Pretty.printf "test for %a\n" Node.pretty_trace (S.Var.node x);
solve x Widen;
VS.iter (fun k -> ignore @@ Pretty.printf "in infl after solving: %a\n" Node.pretty_trace (S.Var.node k)) (HM.find_default infl x VS.empty);
if not (S.Dom.equal (HM.find rho x) old_rho) then (
print_endline "Further destabilization happened ...";
)
Expand Down Expand Up @@ -879,6 +878,9 @@ module Base =
end
in

let stable_reluctant_vs =
List.filter (fun x -> HM.mem stable x) !reluctant_vs
in
let reachable_and_superstable =
if incr_verify && not consider_superstable_reached then
(* Perform reachability on whole constraint system, but cheaply by using logged dependencies *)
Expand All @@ -893,7 +895,7 @@ module Base =
Option.may (VS.iter one_var') (HM.find_option side_infl x)
)
in
(Timing.wrap "cheap_full_reach" (List.iter one_var')) (vs @ !reluctant_vs);
(Timing.wrap "cheap_full_reach" (List.iter one_var')) (vs @ stable_reluctant_vs);

reachable_and_superstable (* consider superstable reached if it is still reachable: stop recursion (evaluation) and keep from being pruned *)
else if incr_verify then
Expand Down Expand Up @@ -1010,8 +1012,7 @@ module Base =
in

let module Post = PostSolver.MakeIncrList (MakeIncrListArg) in

Post.post st (!reluctant_vs @ vs) rho;
Post.post st (stable_reluctant_vs @ vs) rho;

print_data data "Data after postsolve";

Expand Down