Skip to content
Snippets Groups Projects
Commit 5fff66fc authored by David Bühler's avatar David Bühler
Browse files

[Eva] Octagons: optimizes Deps.add.

parent 6bab9ac2
No related branches found
No related tags found
No related merge requests found
...@@ -1044,17 +1044,19 @@ module Deps = struct ...@@ -1044,17 +1044,19 @@ module Deps = struct
is_increasing previous_deps.indirect deps.indirect is_increasing previous_deps.indirect deps.indirect
let add var deps (m, i: t): t = let add var deps (m, i: t): t =
(* If [var] already exists in the state and had bigger dependencies (in rare let add_to (m, i) =
cases, a dependency can disappear by reduction), remove the previous deps VariableToDeps.add var deps m,
from the inverse map to ensure consistency between both maps. *) BaseToVariables.add_deps var deps i
let i =
match VariableToDeps.find_opt var m with
| Some previous_deps when not (are_bases_increasing previous_deps deps) ->
BaseToVariables.remove_deps var previous_deps i
| _ -> i
in in
VariableToDeps.add var deps m, match VariableToDeps.find_opt var m with
BaseToVariables.add_deps var deps i | Some previous_deps when Function_Froms.Deps.equal previous_deps deps ->
m, i
| Some previous_deps when not (are_bases_increasing previous_deps deps) ->
(* If [var] already exists in the state and had bigger dependencies (a
dependency can disappear by reduction), remove the previous deps
from the inverse map to ensure consistency between both maps. *)
add_to (m, BaseToVariables.remove_deps var previous_deps i)
| _ -> add_to (m, i)
let remove (var: Variable.t) ((m, i): t): t option = let remove (var: Variable.t) ((m, i): t): t option =
match VariableToDeps.find_opt var m with match VariableToDeps.find_opt var m with
......
0% Loading or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment