From 84f7a39423af5a3210678f000037791b8a8dc79d Mon Sep 17 00:00:00 2001 From: Simon Cruanes Date: Thu, 21 Oct 2021 20:42:12 -0400 Subject: [PATCH] fix doc test --- doc/guide.md | 18 +++++++++--------- src/base/Proof.ml | 2 ++ src/base/Proof.mli | 3 +++ src/proof-trace-dump/proof_trace_dump.ml | 17 +++++++++++------ 4 files changed, 25 insertions(+), 15 deletions(-) diff --git a/doc/guide.md b/doc/guide.md index c6102a80..6a4fa190 100644 --- a/doc/guide.md +++ b/doc/guide.md @@ -196,7 +196,7 @@ A list of theories can be added initially, or later using `Solver.add_theory`. ```ocaml -# let solver = Solver.create ~theories:[th_bool] ~proof:(Proof_stub.create()) tstore () ();; +# let solver = Solver.create ~theories:[th_bool] ~proof:(Proof.empty) tstore () ();; val solver : Solver.t = # Solver.add_theory;; @@ -238,7 +238,7 @@ whether the assertions and hypotheses are satisfiable together. Solver.mk_lit_t solver q ~sign:false];; - : Solver.res = Sidekick_base_solver.Solver.Unsat - {Sidekick_base_solver.Solver.unsat_core = } + {Sidekick_base_solver.Solver.unsat_core = ; unsat_proof_step = } ``` Here it's unsat, because we asserted "p = q", and then assumed "p" @@ -295,7 +295,7 @@ val q_imp_not_r : Term.t = (=> q (not r)) # Solver.solve ~assumptions:[] solver;; - : Solver.res = Sidekick_base_solver.Solver.Unsat - {Sidekick_base_solver.Solver.unsat_core = } + {Sidekick_base_solver.Solver.unsat_core = ; unsat_proof_step = } ``` This time we got _unsat_ and there is no way of undoing it. @@ -309,7 +309,7 @@ We can solve linear real arithmetic problems as well. Let's create a new solver and add the theory of reals to it. ```ocaml -# let solver = Solver.create ~theories:[th_bool; th_lra] ~proof:(Proof_stub.create()) tstore () ();; +# let solver = Solver.create ~theories:[th_bool; th_lra] ~proof:(Proof.empty) tstore () ();; val solver : Solver.t = ``` @@ -356,10 +356,10 @@ val b_leq_half : Term.t = (<= b 1/2) Solver.mk_lit_t solver b_leq_half];; val res : Solver.res = Sidekick_base_solver.Solver.Unsat - {Sidekick_base_solver.Solver.unsat_core = } + {Sidekick_base_solver.Solver.unsat_core = ; unsat_proof_step = } # match res with Solver.Unsat {unsat_core=us; _} -> us() |> Iter.to_list | _ -> assert false;; -- : Proof_stub.lit list = [(a >= 1); (b <= 1/2)] +- : Proof.lit list = [(a >= 1); (b <= 1/2)] ``` This just showed that `a=1, b=1/2, a>=b` is unsatisfiable. @@ -401,7 +401,7 @@ val f1_u1 : Term.t = (f1 u1) Anyway, Sidekick knows how to reason about functions. ```ocaml -# let solver = Solver.create ~theories:[] ~proof:(Proof_stub.create()) tstore () ();; +# let solver = Solver.create ~theories:[] ~proof:(Proof.empty) tstore () ();; val solver : Solver.t = # (* helper *) @@ -422,13 +422,13 @@ val appf1 : Term.t list -> Term.t = ~assumptions:[Solver.mk_lit_t solver ~sign:false (Term.eq tstore u1 (appf1[u1]))];; - : Solver.res = Sidekick_base_solver.Solver.Unsat - {Sidekick_base_solver.Solver.unsat_core = } + {Sidekick_base_solver.Solver.unsat_core = ; unsat_proof_step = } # Solver.solve solver ~assumptions:[Solver.mk_lit_t solver ~sign:false (Term.eq tstore u2 u3)];; - : Solver.res = Sidekick_base_solver.Solver.Unsat - {Sidekick_base_solver.Solver.unsat_core = } + {Sidekick_base_solver.Solver.unsat_core = ; unsat_proof_step = } ``` Assuming: `f1(u1)=u2, f1(u2)=u3, f1^2(u1)=u1, f1^3(u1)=u1`, diff --git a/src/base/Proof.ml b/src/base/Proof.ml index de8459c1..2fb04a6f 100644 --- a/src/base/Proof.ml +++ b/src/base/Proof.ml @@ -111,6 +111,8 @@ let create ?(config=Config.default) () : t = steps_writer; storage; dispose; } +let empty = create ~config:Config.empty () + let iter_chunks_ (r:CS.Reader.t) k = let rec loop () = CS.Reader.next r diff --git a/src/base/Proof.mli b/src/base/Proof.mli index 59e3de6d..02df8338 100644 --- a/src/base/Proof.mli +++ b/src/base/Proof.mli @@ -64,6 +64,9 @@ val create : ?config:Config.t -> unit -> t (** Create new proof. @param config modifies the proof behavior *) +val empty : t +(** Empty proof, stores nothing *) + val disable : t -> unit (** Disable proof, even if the config would enable it *) diff --git a/src/proof-trace-dump/proof_trace_dump.ml b/src/proof-trace-dump/proof_trace_dump.ml index 0a1353c5..68741091 100644 --- a/src/proof-trace-dump/proof_trace_dump.ml +++ b/src/proof-trace-dump/proof_trace_dump.ml @@ -2,10 +2,13 @@ module CS = Chunk_stack module Proof_ser = Sidekick_base_proof_trace.Proof_ser -let parse_file (file:string) : unit = - Log.debugf 2 (fun k->k"parsing file %S" file); +let file = ref "" +let quiet = ref false - CS.Reader.with_file_backward file @@ fun reader -> +let parse_file () : unit = + Log.debugf 2 (fun k->k"parsing file %S" !file); + + CS.Reader.with_file_backward !file @@ fun reader -> let n = ref 0 in let rec display_steps () = @@ -15,7 +18,9 @@ let parse_file (file:string) : unit = let decode = {Proof_ser.Bare.Decode.bs=b; off=i} in let step = Proof_ser.Step.decode decode in incr n; - Format.printf "@[<2>%a@]@." Proof_ser.Step.pp step; + if not !quiet then ( + Format.printf "@[<2>%a@]@." Proof_ser.Step.pp step; + ); display_steps(); ); in @@ -24,12 +29,12 @@ let parse_file (file:string) : unit = () let () = - let file = ref "" in let opts = [ "--bt", Arg.Unit (fun () -> Printexc.record_backtrace true), " enable stack traces"; "-d", Arg.Int Log.set_debug, " sets the debug verbose level"; + "-q", Arg.Set quiet, " quiet: do not print steps"; ] |> Arg.align in Arg.parse opts (fun f -> file := f) "proof-trace-dump "; if !file = "" then failwith "please provide a file"; - parse_file !file + parse_file ()