From 5a363c9b07a03188da6153f12b1e3c2a9cf1d5f9 Mon Sep 17 00:00:00 2001 From: Jules Villard Date: Thu, 1 Apr 2021 10:24:51 -0700 Subject: [PATCH] [pulse][arith] small normalization improvement Summary: It's better (=possibly more efficient) to take the opportunity to normalize linear terms when we can instead of possibly having to apply the same normalization over and over on individual terms until the next round of proper normalization. Reviewed By: skcho Differential Revision: D27464885 fbshipit-source-id: 0dc01a089 --- infer/src/pulse/PulseFormula.ml | 9 +++++++-- 1 file changed, 7 insertions(+), 2 deletions(-) diff --git a/infer/src/pulse/PulseFormula.ml b/infer/src/pulse/PulseFormula.ml index 5d98babb8..7e8c6a498 100644 --- a/infer/src/pulse/PulseFormula.ml +++ b/infer/src/pulse/PulseFormula.ml @@ -1191,10 +1191,15 @@ module Formula = struct l''] or [y = y'], we could potentially discover the same equality over and over and diverge otherwise. Or could we? *) (* [l'] is possibly not normalized w.r.t. the current [phi] so take this opportunity to - normalize it *) + normalize it, and replace [v]'s current binding *) + let l'' = apply phi l' in + let phi = + if phys_equal l' l'' then phi + else {phi with linear_eqs= Var.Map.add (v :> Var.t) l'' phi.linear_eqs} + in if fuel > 0 then ( L.d_printfln "Consuming fuel solving linear equality (from %d)" fuel ; - solve_normalized_lin_eq ~fuel:(fuel - 1) new_eqs l (apply phi l') phi ) + solve_normalized_lin_eq ~fuel:(fuel - 1) new_eqs l l'' phi ) else ( (* [fuel = 0]: give up simplifying further for fear of diverging *) L.d_printfln "Ran out of fuel solving linear equality" ;