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

feat(asolver): add pp_stats

Browse source
This commit is contained in:
Simon Cruanes 2022-10-29 22:48:41 -04:00
parent 811c06b566
commit 8f2e2ac6de
No known key found for this signature in database
GPG key ID: EBFFF6F283F3A2B4
2 changed files with 3 additions and 0 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

2
src/abstract-solver/asolver.ml
View file

@ -27,6 +27,7 @@ class type t =
(** Convert a term into a simplified literal. *) (** Convert a term into a simplified literal. *)
method tst : Term.store method tst : Term.store
method pp_stats : unit Fmt.printer
method solve : method solve :
?on_exit:(unit -> unit) list -> ?on_exit:(unit -> unit) list ->
@ -60,6 +61,7 @@ let assert_clause (self : #t) c p : unit = self#assert_clause c p
let assert_clause_l (self : #t) c p : unit = self#assert_clause_l c p let assert_clause_l (self : #t) c p : unit = self#assert_clause_l c p
let add_ty (self : #t) ~ty : unit = self#add_ty ~ty let add_ty (self : #t) ~ty : unit = self#add_ty ~ty
let lit_of_term (self : #t) ?sign t : Lit.t = self#lit_of_term ?sign t let lit_of_term (self : #t) ?sign t : Lit.t = self#lit_of_term ?sign t
let pp_stats out (self : #t) : unit = self#pp_stats out ()
let solve (self : #t) ?on_exit ?on_progress ?should_stop ~assumptions () : let solve (self : #t) ?on_exit ?on_progress ?should_stop ~assumptions () :
Check_res.t = Check_res.t =

1
src/smt/solver.ml
View file

@ -271,6 +271,7 @@ let as_asolver (self : t) : Sidekick_abstract_solver.Asolver.t =
method proof_tracer = (self.tracer :> Proof.Tracer.t) method proof_tracer = (self.tracer :> Proof.Tracer.t)
method last_res = last_res self method last_res = last_res self
method add_ty ~ty = add_ty self ty method add_ty ~ty = add_ty self ty
method pp_stats out () = pp_stats out self
method solve ?on_exit ?on_progress ?should_stop ~assumptions () : res = method solve ?on_exit ?on_progress ?should_stop ~assumptions () : res =
solve ?on_exit ?on_progress ?should_stop ~assumptions self solve ?on_exit ?on_progress ?should_stop ~assumptions self