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

lia: use branch and bound a bit

Browse source 
this should be removed when we use the intsolver, alongside a pure real
relaxation of int constraints…
This commit is contained in:
Simon Cruanes 2022-01-14 13:34:23 -05:00
parent eaf56a941f
commit f713106514
No known key found for this signature in database
GPG key ID: EBFFF6F283F3A2B4
1 changed files with 24 additions and 14 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

38
src/lia/Sidekick_arith_lia.ml
View file

@ -192,10 +192,12 @@ module Make(A : ARG) : S with module A = A = struct
u u
in in
(* TODO: remove
if A.has_ty_int t && not (is_int_const t) then ( if A.has_ty_int t && not (is_int_const t) then (
Log.debugf 10 (fun k->k "(@[lia.has-int-ty@ %a@])" T.pp t); Log.debugf 10 (fun k->k "(@[lia.has-int-ty@ %a@])" T.pp t);
SI.declare_pb_is_incomplete si; (* TODO: remove *) SI.declare_pb_is_incomplete si;
); );
*)
(* tell the CC this term exists *) (* tell the CC this term exists *)
let declare_term_to_cc t = let declare_term_to_cc t =
@ -411,21 +413,25 @@ module Make(A : ARG) : S with module A = A = struct
module Q_map = CCMap.Make(A.Q) module Q_map = CCMap.Make(A.Q)
let check_simplex_ self si acts : SimpSolver.Subst.t = let check_simplex_ ~n self si acts : SimpSolver.Subst.t option =
Log.debug 5 "(lia.check-simplex)"; Log.debugf 5 (fun k->k "(lia.check-simplex-bnb@ :n %d)" n);
let res = let res =
Profile.with_ "lia.simplex.solve" Profile.with_ "lia.simplex.solve" @@ fun () ->
(fun () -> SimpSolver.check_branch_and_bound self.simplex
SimpSolver.check self.simplex ~max_tree_nodes:n
~on_propagate:(on_propagate_ si acts)) ~on_propagate:(on_propagate_ si acts)
in in
begin match res with begin match res with
| SimpSolver.Sat m -> m | Some (SimpSolver.Sat m) -> Some m
| SimpSolver.Unsat cert -> | Some (SimpSolver.Unsat cert) ->
Log.debugf 10 Log.debugf 10
(fun k->k "(@[lia.check.unsat@ :cert %a@])" (fun k->k "(@[lia.check.unsat@ :cert %a@])"
SimpSolver.Unsat_cert.pp cert); SimpSolver.Unsat_cert.pp cert);
fail_with_cert si acts cert fail_with_cert si acts cert
| None ->
(* TODO: try harder? use a slow-but-complete decision procedure? *)
SI.declare_pb_is_incomplete si;
None
end end
(* partial checks is where we add literals from the trail to the (* partial checks is where we add literals from the trail to the
@ -469,7 +475,7 @@ module Make(A : ARG) : S with module A = A = struct
(* incremental check *) (* incremental check *)
if !changed then ( if !changed then (
ignore (check_simplex_ self si acts : SimpSolver.Subst.t); ignore (check_simplex_ ~n:2 self si acts : SimpSolver.Subst.t option);
); );
() ()
@ -567,10 +573,14 @@ module Make(A : ARG) : S with module A = A = struct
(* TODO: jiggle model to reduce the number of variables that (* TODO: jiggle model to reduce the number of variables that
have the same value *) have the same value *)
let model = check_simplex_ self si acts in begin match check_simplex_ ~n:15 self si acts with
Log.debugf 20 (fun k->k "(@[lia.model@ %a@])" SimpSolver.Subst.pp model); | Some model ->
Log.debug 5 "(lia: solver returns SAT)"; Log.debugf 20 (fun k->k "(@[lia.model@ %a@])" SimpSolver.Subst.pp model);
do_th_combination self si acts model; Log.debug 5 "(lia: solver returns SAT)";
do_th_combination self si acts model;
| None ->
() (* TODO: find a cut? *)
end;
() ()
(* raise conflict from certificate *) (* raise conflict from certificate *)