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

debug

Browse source
This commit is contained in:
Simon Cruanes 2022-02-07 10:57:39 -05:00
parent d11b9d585c
commit d9a701140c
No known key found for this signature in database
GPG key ID: EBFFF6F283F3A2B4
1 changed files with 4 additions and 4 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

8
src/lra/sidekick_arith_lra.ml
View file

@ -651,18 +651,18 @@ module Make(A : ARG) : S with module A = A = struct
let to_rat_t_ self q = A.mk_lra self.tst (LRA_const q)
(* help generating model *)
let model_gen_ (self:state) ~recurse:_ _si n : _ option =
let model_ask_ (self:state) ~recurse:_ _si n : _ option =
let t = N.term n in
begin match self.last_res with
| Some (SimpSolver.Sat m) ->
Log.debugf 50 (fun k->k "lra: model ask %a" T.pp t);
Log.debugf 50 (fun k->k "(@[lra.model-ask@ %a@])" T.pp t);
SimpSolver.V_map.get t m |> CCOpt.map (to_rat_t_ self)
| _ -> None
end
(* help generating model *)
let model_complete_ (self:state) _si ~add : unit =
Log.debugf 30 (fun k->k "lra: model complete");
Log.debugf 30 (fun k->k "(lra.model-complete)");
begin match self.last_res with
| Some (SimpSolver.Sat m) when T.Tbl.length self.in_model > 0 ->
Log.debugf 50 (fun k->k "(@[lra.in_model@ %a@])"
@ -689,7 +689,7 @@ module Make(A : ARG) : S with module A = A = struct
SI.on_preprocess si (preproc_lra st);
SI.on_final_check si (final_check_ st);
SI.on_partial_check si (partial_check_ st);
SI.on_model si ~ask:(model_gen_ st) ~complete:(model_complete_ st);
SI.on_model si ~ask:(model_ask_ st) ~complete:(model_complete_ st);
SI.on_cc_is_subterm si (on_subterm st);
SI.on_cc_post_merge si
(fun _ _ n1 n2 ->