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

lra: better debug

Browse source
This commit is contained in:
Simon Cruanes 2022-02-17 21:21:40 -05:00
parent 8fb0152754
commit 8530c07c59
No known key found for this signature in database
GPG key ID: EBFFF6F283F3A2B4
2 changed files with 13 additions and 5 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

10
src/lra/sidekick_arith_lra.ml
View file

@ -563,13 +563,15 @@ module Make(A : ARG) : S with module A = A = struct
(** Check satisfiability of simplex, and sets [self.last_res] *)
let check_simplex_ self si acts : SimpSolver.Subst.t =
Log.debug 5 "(lra.check-simplex)";
Log.debugf 5
(fun k->k "(@[lra.check-simplex@ :n-vars %d :n-rows %d@])"
(SimpSolver.n_vars self.simplex) (SimpSolver.n_rows self.simplex));
let res =
Profile.with_ "lra.simplex.solve"
(fun () ->
Profile.with_ "lra.simplex.solve" @@ fun () ->
SimpSolver.check self.simplex
~on_propagate:(on_propagate_ si acts))
~on_propagate:(on_propagate_ si acts)
in
Log.debug 5 "(lra.check-simplex.done)";
self.last_res <- Some res;
begin match res with
| SimpSolver.Sat m -> m

6
src/simplex/sidekick_simplex.ml
View file

@ -152,6 +152,9 @@ module type S = sig
t -> result option
(** Try to solve and respect the integer constraints. *)
val n_vars: t -> int
val n_rows: t -> int
(**/**)
val _check_invariants : t -> unit
(* check internal invariants *)
@ -470,6 +473,9 @@ module Make(Arg: ARG)
~f:(fun f -> f());
()
let n_vars self = Vec.size self.vars
let n_rows self = Matrix.n_rows self.matrix
let pp_stats out (self:t) : unit =
Fmt.fprintf out "(@[simplex@ :n-vars %d@ :n-rows %d@])"
(Vec.size self.vars) (Matrix.n_rows self.matrix)