simon/sidekick
1
0
Fork 0
mirror of https://github.com/c-cube/sidekick.git synced 2025-12-06 11:15:43 -05:00
Code Issues Projects Releases Packages Wiki Activity Actions

fix: small perf improvement

Browse source
This commit is contained in:
Simon Cruanes 2020-11-13 23:28:39 -05:00
parent 39ed753b38
commit a6f6a99fb3
1 changed files with 3 additions and 5 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

8
src/arith/lra/simplex.ml
View file

@ -209,15 +209,13 @@ module Make_inner
(fun y -> if Var.compare x y = 0 then Q.one else Q.zero) (fun y -> if Var.compare x y = 0 then Q.one else Q.zero)
t.nbasic t.nbasic
(* TODO: avoid double lookup in maps *)
(* find expression of [x] *) (* find expression of [x] *)
let find_expr_total (t:t) (x:var) : Q.t Vec.vector = let find_expr_total (t:t) (x:var) : Q.t Vec.vector =
if mem_basic t x then match find_expr_basic_opt t x with
find_expr_basic t x | Some e -> e
else ( | None ->
assert (mem_nbasic t x); assert (mem_nbasic t x);
find_expr_nbasic t x find_expr_nbasic t x
)
(* compute value of basic variable. (* compute value of basic variable.
It can be computed by using [x]'s definition It can be computed by using [x]'s definition