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

wip: feat(lra): clarify construction of bounds; fix sign error

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

42
src/lra/simplex2.ml
View file

@ -763,8 +763,10 @@ module Make(Q : RATIONAL)(Var: VAR)
(* gather all relevant lower (resp. upper) bounds for the definition (* gather all relevant lower (resp. upper) bounds for the definition
of the basic variable [x_i], and collect each relevant variable of the basic variable [x_i], and collect each relevant variable
with [map] into a list. *) with [map] into a list.
let gather_bounds_of_row_ (self:t) (x_i:var_state) ~map ~is_lower : _ list * _ = @param get_lower if true, means we select lower bounds of variables
with positive coeffs, and upper bounds of variables with negative coeffs. *)
let gather_bounds_of_row_ (self:t) (x_i:var_state) ~map ~get_lower : _ list * _ =
assert (Var_state.is_basic x_i); assert (Var_state.is_basic x_i);
let map_res = ref [] in let map_res = ref [] in
let bounds = ref V_map.empty in let bounds = ref V_map.empty in
@ -773,18 +775,9 @@ module Make(Q : RATIONAL)(Var: VAR)
if j <> x_i.idx then ( if j <> x_i.idx then (
let c = Matrix.get self.matrix x_i.basic_idx j in let c = Matrix.get self.matrix x_i.basic_idx j in
if Q.(c <> zero) then ( if Q.(c <> zero) then (
match is_lower, Q.(c > zero) with match get_lower, Q.(c > zero) with
| true, true | true, true
| false, false -> | false, false ->
begin match x_j.u_bound with
| Some u ->
map_res := (map c x_j u) :: !map_res;
let op = if Q.(u.b_val.eps_factor >= zero) then Op.Leq else Op.Lt in
bounds := V_map.add x_j.var (op, u) !bounds
| None -> assert false (* we could increase [x_j]?! *)
end
| true, false
| false, true ->
begin match x_j.l_bound with begin match x_j.l_bound with
| Some l -> | Some l ->
map_res := (map c x_j l) :: !map_res; map_res := (map c x_j l) :: !map_res;
@ -792,6 +785,15 @@ module Make(Q : RATIONAL)(Var: VAR)
bounds := V_map.add x_j.var (op, l) !bounds bounds := V_map.add x_j.var (op, l) !bounds
| None -> assert false (* we could decrease [x_j]?! *) | None -> assert false (* we could decrease [x_j]?! *)
end end
| true, false
| false, true ->
begin match x_j.u_bound with
| Some u ->
map_res := (map c x_j u) :: !map_res;
let op = if Q.(u.b_val.eps_factor >= zero) then Op.Leq else Op.Lt in
bounds := V_map.add x_j.var (op, u) !bounds
| None -> assert false (* we could increase [x_j]?! *)
end
) )
)) ))
self.vars; self.vars;
@ -801,9 +803,9 @@ module Make(Q : RATIONAL)(Var: VAR)
let propagate_basic_implied_bounds (self:t) ~on_propagate (x_i:var_state) : unit = let propagate_basic_implied_bounds (self:t) ~on_propagate (x_i:var_state) : unit =
assert (Var_state.is_basic x_i); assert (Var_state.is_basic x_i);
let lits_of_row_ ~is_lower : V.lit list = let lits_of_row_ ~get_lower : V.lit list =
let l, _ = let l, _ =
gather_bounds_of_row_ self x_i ~is_lower gather_bounds_of_row_ self x_i ~get_lower
~map:(fun _ _ bnd -> bnd.b_lit) in ~map:(fun _ _ bnd -> bnd.b_lit) in
l l
in in
@ -812,7 +814,7 @@ module Make(Q : RATIONAL)(Var: VAR)
if is_lower then ( if is_lower then (
if Erat.(bnd.b_val < x_i.l_implied) then ( if Erat.(bnd.b_val < x_i.l_implied) then (
(* implied lower bound subsumes this lower bound *) (* implied lower bound subsumes this lower bound *)
let reason = lits_of_row_ ~is_lower:true in let reason = lits_of_row_ ~get_lower:true in
on_propagate bnd.b_lit ~reason on_propagate bnd.b_lit ~reason
); );
if Erat.(bnd.b_val > x_i.u_implied) then ( if Erat.(bnd.b_val > x_i.u_implied) then (
@ -822,21 +824,21 @@ module Make(Q : RATIONAL)(Var: VAR)
Log.debugf 50 Log.debugf 50
(fun k->k"(@[lra.propagate.not@ :lower-bnd-of %a@ :bnd %a :lit %a@ :u-implied %a@])" (fun k->k"(@[lra.propagate.not@ :lower-bnd-of %a@ :bnd %a :lit %a@ :u-implied %a@])"
Var_state.pp x_i Erat.pp bnd.b_val V.pp_lit bnd.b_lit Erat.pp x_i.u_implied); Var_state.pp x_i Erat.pp bnd.b_val V.pp_lit bnd.b_lit Erat.pp x_i.u_implied);
let reason = lits_of_row_ ~is_lower:false in let reason = lits_of_row_ ~get_lower:false in
on_propagate not_lit ~reason on_propagate not_lit ~reason
| None -> () | None -> ()
) )
) else ( ) else (
if Erat.(bnd.b_val > x_i.u_implied) then ( if Erat.(bnd.b_val > x_i.u_implied) then (
(* implied upper bound subsumes this upper bound *) (* implied upper bound subsumes this upper bound *)
let reason = lits_of_row_ ~is_lower:false in let reason = lits_of_row_ ~get_lower:false in
on_propagate bnd.b_lit ~reason on_propagate bnd.b_lit ~reason
); );
if Erat.(bnd.b_val < x_i.l_implied) then ( if Erat.(bnd.b_val < x_i.l_implied) then (
(* upper bound is lower than implied lower bound *) (* upper bound is lower than implied lower bound *)
match V.not_lit bnd.b_lit with match V.not_lit bnd.b_lit with
| Some not_lit -> | Some not_lit ->
let reason = lits_of_row_ ~is_lower:true in let reason = lits_of_row_ ~get_lower:true in
on_propagate not_lit ~reason on_propagate not_lit ~reason
| None -> () | None -> ()
) )
@ -1011,7 +1013,9 @@ module Make(Q : RATIONAL)(Var: VAR)
is_lower Var_state.pp x_i); is_lower Var_state.pp x_i);
assert (Var_state.is_basic x_i); assert (Var_state.is_basic x_i);
let le, bounds = let le, bounds =
gather_bounds_of_row_ self x_i ~is_lower (* we get explanations for an (implied) upper bound
if [bnd] is a lower bound, and conversely *)
gather_bounds_of_row_ self x_i ~get_lower:(not is_lower)
~map:(fun c v _ -> c, v.var) ~map:(fun c v _ -> c, v.var)
in in