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

perf(lra): only call simplex.check if new things were asserted

Browse source
This commit is contained in:
Simon Cruanes 2021-02-15 17:09:38 -05:00
parent 2a6c224f08
commit 0634e7c356
1 changed files with 6 additions and 1 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

7
src/arith/lra/sidekick_arith_lra.ml
View file

@ -379,6 +379,8 @@ module Make(A : ARG) : S with module A = A = struct
simplex. *) simplex. *)
let partial_check_ self si acts trail : unit = let partial_check_ self si acts trail : unit =
Profile.with_ "lra.partial-check" @@ fun () -> Profile.with_ "lra.partial-check" @@ fun () ->
let changed = ref false in
trail trail
(fun lit -> (fun lit ->
let sign = SI.Lit.sign lit in let sign = SI.Lit.sign lit in
@ -395,6 +397,7 @@ module Make(A : ARG) : S with module A = A = struct
(fun k->k "(@[lra.partial-check.assert@ %a@])" (fun k->k "(@[lra.partial-check.assert@ %a@])"
SimpSolver.Constraint.pp constr); SimpSolver.Constraint.pp constr);
begin begin
changed := true;
try try
SimpSolver.add_var self.simplex v; SimpSolver.add_var self.simplex v;
SimpSolver.add_constraint self.simplex constr (Tag.Lit lit) SimpSolver.add_constraint self.simplex constr (Tag.Lit lit)
@ -407,7 +410,9 @@ module Make(A : ARG) : S with module A = A = struct
| _ -> ()); | _ -> ());
(* incremental check *) (* incremental check *)
ignore (check_simplex_ self si acts : SimpSolver.Subst.t); if !changed then (
ignore (check_simplex_ self si acts : SimpSolver.Subst.t);
);
() ()
let final_check_ (self:state) si (acts:SI.actions) (_trail:_ Iter.t) : unit = let final_check_ (self:state) si (acts:SI.actions) (_trail:_ Iter.t) : unit =