From 8f2e2ac6debcd1160cca3c2c280ca8524f4594b7 Mon Sep 17 00:00:00 2001 From: Simon Cruanes Date: Sat, 29 Oct 2022 22:48:41 -0400 Subject: [PATCH] feat(asolver): add pp_stats --- src/abstract-solver/asolver.ml | 2 ++ src/smt/solver.ml | 1 + 2 files changed, 3 insertions(+) diff --git a/src/abstract-solver/asolver.ml b/src/abstract-solver/asolver.ml index 5f5919d6..d9bcc61a 100644 --- a/src/abstract-solver/asolver.ml +++ b/src/abstract-solver/asolver.ml @@ -27,6 +27,7 @@ class type t = (** Convert a term into a simplified literal. *) method tst : Term.store + method pp_stats : unit Fmt.printer method solve : ?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 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 pp_stats out (self : #t) : unit = self#pp_stats out () let solve (self : #t) ?on_exit ?on_progress ?should_stop ~assumptions () : Check_res.t = diff --git a/src/smt/solver.ml b/src/smt/solver.ml index d0123f55..7d6ae455 100644 --- a/src/smt/solver.ml +++ b/src/smt/solver.ml @@ -271,6 +271,7 @@ let as_asolver (self : t) : Sidekick_abstract_solver.Asolver.t = method proof_tracer = (self.tracer :> Proof.Tracer.t) method last_res = last_res self 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 = solve ?on_exit ?on_progress ?should_stop ~assumptions self