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

fix: missing implied bound update

Browse source
This commit is contained in:
Simon Cruanes 2021-03-21 18:51:44 -04:00
parent 73c9878554
commit 9d3da47f3b
No known key found for this signature in database
GPG key ID: EBFFF6F283F3A2B4
1 changed files with 21 additions and 11 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

32
src/lra/simplex2.ml
View file

@ -848,6 +848,18 @@ module Make(Q : RATIONAL)(Var: VAR)
List.iter process_bount_lit x_i.all_bound_lits;
()
let update_implied_bounds_for_nbasic_
(self:t) (vs:var_state) ~on_propagate : unit =
(* section 3.2.5: update implied bounds on basic variables that
depend on [vs] *)
for i = 0 to Matrix.n_rows self.matrix -1 do
if Q.(Matrix.get self.matrix i vs.idx <> zero) then (
let x_i = Matrix.get_row_var self.matrix i in
update_implied_bounds_ self x_i;
propagate_basic_implied_bounds self ~on_propagate x_i;
);
done
let add_constraint ~on_propagate (self:t) (c:Constraint.t) (lit:V.lit) : unit =
let open Constraint in
@ -899,16 +911,7 @@ module Make(Q : RATIONAL)(Var: VAR)
Erat.(vs.value < new_bnd.b_val) then (
(* line 5: need to update non-basic variable *)
update_n_basic self vs new_bnd.b_val;
(* section 3.2.5: update implied bounds on basic variables that
depend on [vs] *)
for i = 0 to Matrix.n_rows self.matrix -1 do
if Q.(Matrix.get self.matrix i vs.idx <> zero) then (
let x_i = Matrix.get_row_var self.matrix i in
update_implied_bounds_ self x_i;
propagate_basic_implied_bounds self ~on_propagate x_i;
);
done;
update_implied_bounds_for_nbasic_ self vs ~on_propagate;
)
end
) else (
@ -944,7 +947,8 @@ module Make(Q : RATIONAL)(Var: VAR)
if Var_state.is_n_basic vs &&
Erat.(vs.value > new_bnd.b_val) then (
(* line 5: need to update non-basic variable *)
update_n_basic self vs new_bnd.b_val
update_n_basic self vs new_bnd.b_val;
update_implied_bounds_for_nbasic_ self vs ~on_propagate;
)
end
)
@ -1027,11 +1031,14 @@ module Make(Q : RATIONAL)(Var: VAR)
let cert = Unsat_cert.unsat_basic x_i (op, bnd) le bounds in
cert
let out_ = open_out "pivots"
(* main satisfiability check.
page 15, figure 3.2 *)
let check_exn ~on_propagate:_ (self:t) : unit =
let exception Stop in
Log.debugf 20 (fun k->k "(@[simplex2.check@ %a@])" pp_stats self);
Printf.fprintf out_ "check\n";
Stat.incr self.stat_check;
let m = self.matrix in
@ -1069,6 +1076,7 @@ module Make(Q : RATIONAL)(Var: VAR)
Log.debugf 50
(fun k->k "(@[simplex2.pivot@ :basic %a@ :n-basic %a@])"
Var_state.pp x_i Var_state.pp x_j);
Printf.fprintf out_ "pivot x%d -> x%d\n%!" x_i.idx x_j.idx;
pivot_and_update self x_i x_j bnd.b_val
) else (
(* line 10 *)
@ -1092,10 +1100,12 @@ module Make(Q : RATIONAL)(Var: VAR)
Log.debugf 50
(fun k->k "(@[simplex2.pivot@ :basic %a@ :n-basic %a@])"
Var_state.pp x_i Var_state.pp x_j);
Printf.fprintf out_ "pivot x%d -> x%d\n%!" x_i.idx x_j.idx;
pivot_and_update self x_i x_j bnd.b_val
)
done;
with Stop ->
Printf.fprintf out_ "done\n";
Log.debugf 50 (fun k->k "(@[simplex2.check.done@])");
()