From 8e9bc54c4a0271cd22cadc2668929ecc1a483e31 Mon Sep 17 00:00:00 2001 From: Jules Villard Date: Thu, 1 Apr 2021 10:24:39 -0700 Subject: [PATCH] [pulse][arith] eval constant terms before other simplifications Summary: The simplifications done by `simplify_shallow` are all taken care of by `eval_const_shallow` as well, they just also happen to help when not *all* of the term is a constant. However, they might be less precise/efficient than in the constant case, in particular in the next diff that translates `x << c` into `x * 2^c` when `c` is constant. Reviewed By: skcho Differential Revision: D27464805 fbshipit-source-id: 452bc6ab1 --- infer/src/pulse/PulseFormula.ml | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/infer/src/pulse/PulseFormula.ml b/infer/src/pulse/PulseFormula.ml index 9c277b963..89de14d4d 100644 --- a/infer/src/pulse/PulseFormula.ml +++ b/infer/src/pulse/PulseFormula.ml @@ -968,7 +968,7 @@ module Atom = struct let rec eval_term t = let t = Term.map_direct_subterms ~f:eval_term t - |> Term.simplify_shallow |> Term.eval_const_shallow |> Term.linearize |> Term.simplify_linear + |> Term.eval_const_shallow |> Term.simplify_shallow |> Term.linearize |> Term.simplify_linear in match atom_of_term t with | Some atom ->