From a6f6a99fb380098cbf4b66bfd7bb44ec175b5494 Mon Sep 17 00:00:00 2001 From: Simon Cruanes Date: Fri, 13 Nov 2020 23:28:39 -0500 Subject: [PATCH] fix: small perf improvement --- src/arith/lra/simplex.ml | 8 +++----- 1 file changed, 3 insertions(+), 5 deletions(-) diff --git a/src/arith/lra/simplex.ml b/src/arith/lra/simplex.ml index c7520245..b0946208 100644 --- a/src/arith/lra/simplex.ml +++ b/src/arith/lra/simplex.ml @@ -209,15 +209,13 @@ module Make_inner (fun y -> if Var.compare x y = 0 then Q.one else Q.zero) t.nbasic - (* TODO: avoid double lookup in maps *) (* find expression of [x] *) let find_expr_total (t:t) (x:var) : Q.t Vec.vector = - if mem_basic t x then - find_expr_basic t x - else ( + match find_expr_basic_opt t x with + | Some e -> e + | None -> assert (mem_nbasic t x); find_expr_nbasic t x - ) (* compute value of basic variable. It can be computed by using [x]'s definition