From 5b9503dfc7d1e88dc026733473365b1760031a9f Mon Sep 17 00:00:00 2001 From: Julian Erhard Date: Fri, 23 Dec 2022 22:58:19 +0100 Subject: [PATCH 1/3] Reluctant incremental analysis: only pass stable reluctant_vs to postsolver. Previously, the postsolver reported unreached fixpoints when also unstable unknowns from reluctant_vs were passed to it. --- src/solvers/td3.ml | 6 ++++-- 1 file changed, 4 insertions(+), 2 deletions(-) diff --git a/src/solvers/td3.ml b/src/solvers/td3.ml index 9a4c839175..c72bfdc16b 100644 --- a/src/solvers/td3.ml +++ b/src/solvers/td3.ml @@ -1010,8 +1010,10 @@ module Base = in let module Post = PostSolver.MakeIncrList (MakeIncrListArg) in - - Post.post st (!reluctant_vs @ vs) rho; + let stable_reluctant_vars = + List.filter (fun x -> HM.mem stable x) !reluctant_vs + in + Post.post st (stable_reluctant_vars @ vs) rho; print_data data "Data after postsolve"; From 909321873ff74512cf59932fab61da254dfbd075 Mon Sep 17 00:00:00 2001 From: Julian Erhard Date: Fri, 23 Dec 2022 23:05:23 +0100 Subject: [PATCH 2/3] Use stable_reluctant_vs also for reachable and superstable. --- src/solvers/td3.ml | 10 +++++----- 1 file changed, 5 insertions(+), 5 deletions(-) diff --git a/src/solvers/td3.ml b/src/solvers/td3.ml index c72bfdc16b..74a2487bee 100644 --- a/src/solvers/td3.ml +++ b/src/solvers/td3.ml @@ -879,6 +879,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 *) @@ -893,7 +896,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 @@ -1010,10 +1013,7 @@ module Base = in let module Post = PostSolver.MakeIncrList (MakeIncrListArg) in - let stable_reluctant_vars = - List.filter (fun x -> HM.mem stable x) !reluctant_vs - in - Post.post st (stable_reluctant_vars @ vs) rho; + Post.post st (stable_reluctant_vs @ vs) rho; print_data data "Data after postsolve"; From 9c423efef2cb9c1acf239edc2ea2b0c5c438d18e Mon Sep 17 00:00:00 2001 From: Julian Erhard Date: Fri, 23 Dec 2022 23:21:14 +0100 Subject: [PATCH 3/3] Remove debug printout. --- src/solvers/td3.ml | 1 - 1 file changed, 1 deletion(-) diff --git a/src/solvers/td3.ml b/src/solvers/td3.ml index 74a2487bee..21540d17fa 100644 --- a/src/solvers/td3.ml +++ b/src/solvers/td3.ml @@ -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 ..."; )