From f905b754aabc9b63740599644d9fbbe4b3b784a1 Mon Sep 17 00:00:00 2001 From: Simon Cruanes Date: Sun, 23 Oct 2022 20:55:25 -0400 Subject: [PATCH 1/5] wip: check models --- src/abstract-solver/asolver.ml | 3 +++ src/smt/solver.ml | 1 + src/smtlib/Driver.ml | 16 +++++++++------- 3 files changed, 13 insertions(+), 7 deletions(-) diff --git a/src/abstract-solver/asolver.ml b/src/abstract-solver/asolver.ml index ecf1d7ab..5f5919d6 100644 --- a/src/abstract-solver/asolver.ml +++ b/src/abstract-solver/asolver.ml @@ -26,6 +26,8 @@ class type t = method lit_of_term : ?sign:bool -> Term.t -> Lit.t (** Convert a term into a simplified literal. *) + method tst : Term.store + method solve : ?on_exit:(unit -> unit) list -> ?on_progress:(unit -> unit) -> @@ -52,6 +54,7 @@ class type t = (** TODO: remove, use Tracer instead *) end +let tst (self : #t) : Term.store = self#tst let assert_term (self : #t) t : unit = self#assert_term t 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 diff --git a/src/smt/solver.ml b/src/smt/solver.ml index 49e297e7..d0123f55 100644 --- a/src/smt/solver.ml +++ b/src/smt/solver.ml @@ -263,6 +263,7 @@ let solve ?(on_exit = []) ?(on_progress = fun _ -> ()) let as_asolver (self : t) : Sidekick_abstract_solver.Asolver.t = object + method tst = SI.tst self.si method assert_term t : unit = assert_term self t method assert_clause c p : unit = add_clause self c p method assert_clause_l c p : unit = add_clause_l self c p diff --git a/src/smtlib/Driver.ml b/src/smtlib/Driver.ml index c4054bb7..0a8c4ecb 100644 --- a/src/smtlib/Driver.ml +++ b/src/smtlib/Driver.ml @@ -15,6 +15,7 @@ type t = { progress: Progress_bar.t option; solver: Asolver.t; build_model: Build_model.t; + asserts: Term.t Vec.t; time_start: float; time_limit: float; memory_limit: float; @@ -42,6 +43,7 @@ let create ?(pp_cnf = false) ?proof_file ?(pp_model = false) ?(check = false) { time_start; build_model = Build_model.create (); + asserts = Vec.create (); progress; solver; proof_file; @@ -67,6 +69,8 @@ let decl_fun (self : t) f args ret const : unit = let build_model (self : t) (sat : Solver.sat_result) : Model.t = Build_model.build self.build_model sat +let check_model (self : t) (m : Model.t) : unit = assert false + (* call the solver to check satisfiability *) let solve (self : t) ~assumptions () : Solver.res = let t1 = now () in @@ -96,15 +100,9 @@ let solve (self : t) ~assumptions () : Solver.res = | Asolver.Check_res.Sat sat -> if self.pp_model then ( let m = build_model self sat in - (* TODO: use actual {!Model} in the solver? or build it afterwards *) + if self.check then check_model self m; Fmt.printf "%a@." Model.pp m ); - (* TODO - if check then ( - Solver.check_model s; - CCOpt.iter (fun h -> check_smt_model (Solver.solver s) h m) hyps; - ); - *) let t3 = now () in Fmt.printf "sat@."; Fmt.printf "; (%.3f/%.3f/%.3f)@." (t1 -. time_start) (t2 -. t1) (t3 -. t2) @@ -184,6 +182,7 @@ let process_stmt (self : t) (stmt : Statement.t) : unit or_error = E.return () | Statement.Stmt_assert t -> if self.pp_cnf then Format.printf "(@[assert@ %a@])@." Term.pp t; + if self.check then Vec.push self.asserts t; let lit = Asolver.lit_of_term self.solver t in Asolver.assert_clause self.solver [| lit |] (fun () -> Proof.Sat_rules.sat_input_clause [ lit ]); @@ -192,6 +191,8 @@ let process_stmt (self : t) (stmt : Statement.t) : unit or_error = if self.pp_cnf then Format.printf "(@[assert-clause@ %a@])@." (Util.pp_list Term.pp) c_ts; + if self.check then + Vec.push self.asserts (Form.or_l (Asolver.tst self.solver) c_ts); let c = CCList.map (fun t -> Asolver.lit_of_term self.solver t) c_ts in (* proof of assert-input + preprocessing *) @@ -206,6 +207,7 @@ let process_stmt (self : t) (stmt : Statement.t) : unit or_error = (match Asolver.last_res self.solver with | Some (Solver.Sat sat) -> let m = build_model self sat in + if self.check then check_model self m; Fmt.printf "%a@." Model.pp m | _ -> Error.errorf "cannot access model"); E.return () From 651f2c1150c83963a55d641d6099baebee034439 Mon Sep 17 00:00:00 2001 From: Simon Cruanes Date: Thu, 20 Oct 2022 16:12:52 -0400 Subject: [PATCH 2/5] warnings --- src/core-logic/sidekick_core_logic.ml | 1 - src/util/Sidekick_util.ml | 1 - 2 files changed, 2 deletions(-) diff --git a/src/core-logic/sidekick_core_logic.ml b/src/core-logic/sidekick_core_logic.ml index 4636cb39..c06f698a 100644 --- a/src/core-logic/sidekick_core_logic.ml +++ b/src/core-logic/sidekick_core_logic.ml @@ -4,7 +4,6 @@ module Bvar = Bvar module Const = Const module Subst = Subst module T_builtins = T_builtins -module Ser_sink = Ser_sink module Store = Term.Store (* TODO: move to separate library? *) diff --git a/src/util/Sidekick_util.ml b/src/util/Sidekick_util.ml index cafff83a..d1509ab4 100644 --- a/src/util/Sidekick_util.ml +++ b/src/util/Sidekick_util.ml @@ -25,6 +25,5 @@ module Profile = Profile module Chunk_stack = Chunk_stack module Ser_value = Ser_value module Ser_decode = Ser_decode -module Ser_sink = Ser_sink let[@inline] ( let@ ) f x = f x From f5ccbb476b2693e1259e3071c137d2983c781deb Mon Sep 17 00:00:00 2001 From: Simon Cruanes Date: Sun, 23 Oct 2022 20:58:25 -0400 Subject: [PATCH 3/5] add todo --- src/smtlib/Driver.ml | 5 ++++- 1 file changed, 4 insertions(+), 1 deletion(-) diff --git a/src/smtlib/Driver.ml b/src/smtlib/Driver.ml index 0a8c4ecb..9a572b91 100644 --- a/src/smtlib/Driver.ml +++ b/src/smtlib/Driver.ml @@ -69,7 +69,10 @@ let decl_fun (self : t) f args ret const : unit = let build_model (self : t) (sat : Solver.sat_result) : Model.t = Build_model.build self.build_model sat -let check_model (self : t) (m : Model.t) : unit = assert false +(* FIXME *) +let check_model (_self : t) (_m : Model.t) : unit = + Log.debugf 0 (fun k -> k "; TODO: check model"); + () (* call the solver to check satisfiability *) let solve (self : t) ~assumptions () : Solver.res = From 4c330e4ed67ee1e234c3a42243b71dd2c5fd3d96 Mon Sep 17 00:00:00 2001 From: Simon Cruanes Date: Thu, 23 Feb 2023 21:01:34 -0500 Subject: [PATCH 4/5] ocamlformat --- .ocamlformat | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/.ocamlformat b/.ocamlformat index 777b2f13..2ea44df4 100644 --- a/.ocamlformat +++ b/.ocamlformat @@ -1,4 +1,4 @@ -version = 0.20.1 +version = 0.24.1 profile=conventional margin=80 if-then-else=k-r From 40a743badb70f29ca47007eb4e394afdf1ff006d Mon Sep 17 00:00:00 2001 From: Simon Cruanes Date: Thu, 23 Feb 2023 21:01:38 -0500 Subject: [PATCH 5/5] update to handle mtime 2.0 --- dune-project | 3 ++- sidekick.opam | 6 +++++- src/tef/Sidekick_tef.real.ml | 2 +- 3 files changed, 8 insertions(+), 3 deletions(-) diff --git a/dune-project b/dune-project index 8637eef0..1ab4d8ff 100644 --- a/dune-project +++ b/dune-project @@ -33,7 +33,8 @@ (alcotest :with-test) (odoc :with-doc)) (depopts - mtime ; for profiling stuff + (mtime + (>= 2.0)) ; for profiling stuff memtrace ; memory profiling zarith ; for arith ) diff --git a/sidekick.opam b/sidekick.opam index c82c4a08..671080eb 100644 --- a/sidekick.opam +++ b/sidekick.opam @@ -16,7 +16,11 @@ depends: [ "alcotest" {with-test} "odoc" {with-doc} ] -depopts: ["mtime" "memtrace" "zarith"] +depopts: [ + "mtime" {>= "2.0"} + "memtrace" + "zarith" +] conflicts: [ "zarith" {< "1.8"} ] diff --git a/src/tef/Sidekick_tef.real.ml b/src/tef/Sidekick_tef.real.ml index e025ca10..61e698f8 100644 --- a/src/tef/Sidekick_tef.real.ml +++ b/src/tef/Sidekick_tef.real.ml @@ -31,7 +31,7 @@ module Make () : P.BACKEND = struct let get_ts () : float = let now = Mtime_clock.now () in - Mtime.Span.to_us (Mtime.span program_start now) + Mtime.Span.to_float_ns (Mtime.span program_start now) /. 1e3 let emit_sep_ () = if !first_ then