From e3e71f3d76f8a311faec9a6d0673a9aa769e8e37 Mon Sep 17 00:00:00 2001 From: Simon Cruanes Date: Mon, 10 Oct 2022 14:21:10 -0400 Subject: [PATCH] refactor: smtlib driver now part of base; make it stateful --- dune-project | 4 - sidekick-bin.opam | 1 - src/main/dune | 2 +- src/main/main.ml | 27 ++- src/smtlib/{Process.ml => Driver.ml} | 252 +++++++++---------------- src/smtlib/{Process.mli => Driver.mli} | 22 ++- src/smtlib/Sidekick_smtlib.ml | 7 +- src/smtlib/Sidekick_smtlib.mli | 9 +- src/smtlib/Typecheck.ml | 6 +- src/smtlib/Typecheck.mli | 9 +- src/smtlib/check_cc.ml | 55 ++++++ src/smtlib/check_cc.mli | 2 + src/smtlib/common_.ml | 16 ++ src/smtlib/dune | 4 +- src/smtlib/progress_bar.ml | 26 +++ src/smtlib/progress_bar.mli | 7 + src/smtlib/solver.ml | 1 + 17 files changed, 242 insertions(+), 208 deletions(-) rename src/smtlib/{Process.ml => Driver.ml} (51%) rename src/smtlib/{Process.mli => Driver.mli} (59%) create mode 100644 src/smtlib/check_cc.ml create mode 100644 src/smtlib/check_cc.mli create mode 100644 src/smtlib/common_.ml create mode 100644 src/smtlib/progress_bar.ml create mode 100644 src/smtlib/progress_bar.mli create mode 100644 src/smtlib/solver.ml diff --git a/dune-project b/dune-project index 4ec7b415..d221a42b 100644 --- a/dune-project +++ b/dune-project @@ -71,10 +71,6 @@ (synopsis "SMT solver based on msat and CDCL(T) (standalone binary)") (depends zarith - (smtlib-utils - (and - (>= "0.1") - (< "0.4"))) (sidekick (= :version)) (sidekick-base diff --git a/sidekick-bin.opam b/sidekick-bin.opam index 81b78cca..3fa436d2 100644 --- a/sidekick-bin.opam +++ b/sidekick-bin.opam @@ -10,7 +10,6 @@ bug-reports: "https://github.com/c-cube/sidekick/issues/" depends: [ "dune" {>= "2.0"} "zarith" - "smtlib-utils" {>= "0.1" & < "0.4"} "sidekick" {= version} "sidekick-base" {= version} "menhir" diff --git a/src/main/dune b/src/main/dune index 7727142d..cea88d77 100644 --- a/src/main/dune +++ b/src/main/dune @@ -7,7 +7,7 @@ (modules main pure_sat_solver) (modes native) (libraries containers iter result sidekick.sat sidekick.core sidekick-base - sidekick.smt-solver sidekick-bin.smtlib sidekick.tef sidekick.drup + sidekick.smt-solver sidekick-base.smtlib sidekick.tef sidekick.drup sidekick.memtrace sidekick-bin.lib) (flags :standard -safe-string -color always -open Sidekick_util)) diff --git a/src/main/main.ml b/src/main/main.ml index 4312ea90..acbfb528 100644 --- a/src/main/main.ml +++ b/src/main/main.ml @@ -10,7 +10,7 @@ module Fmt = CCFormat module Term = Sidekick_base.Term module Config = Sidekick_base.Config module Solver = Sidekick_smtlib.Solver -module Process = Sidekick_smtlib.Process +module Driver = Sidekick_smtlib.Driver module Proof = Sidekick_smtlib.Proof_trace open E.Infix @@ -28,7 +28,6 @@ let check = ref false let time_limit = ref 300. let mem_limit = ref 1_000_000_000. let restarts = ref true -let gc = ref true let p_stat = ref false let p_gc_stat = ref false let p_progress = ref false @@ -77,8 +76,6 @@ let argspec = Arg.Set check, " build, check and print the proof (if output is set), if unsat" ); "--no-check", Arg.Clear check, " inverse of -check"; - "--gc", Arg.Set gc, " enable garbage collection"; - "--no-gc", Arg.Clear gc, " disable garbage collection"; "--restarts", Arg.Set restarts, " enable restarts"; "--no-restarts", Arg.Clear restarts, " disable restarts"; "--stat", Arg.Set p_stat, " print statistics"; @@ -196,13 +193,13 @@ let main_smt ~config () : _ result = let solver = (* TODO: probes, to load only required theories *) let theories = - let th_bool = Process.th_bool config in + let th_bool = Driver.th_bool config in Log.debugf 1 (fun k -> k "(@[main.th-bool.pick@ %S@])" (Sidekick_smt_solver.Theory.name th_bool)); - [ th_bool; Process.th_ty_unin; Process.th_data; Process.th_lra ] + [ th_bool; Driver.th_ty_unin; Driver.th_data; Driver.th_lra ] in - Process.Solver.create_default ~tracer ~proof ~theories tst + Solver.create_default ~tracer ~proof ~theories tst in let finally () = @@ -218,7 +215,7 @@ let main_smt ~config () : _ result = in if !check then (* might have to check conflicts *) - Solver.add_theory solver Process.Check_cc.theory; + Solver.add_theory solver Sidekick_smtlib.Check_cc.theory; let parse_res = let@ () = Profile.with_ "parse" ~args:[ "file", !file ] in @@ -226,15 +223,15 @@ let main_smt ~config () : _ result = in parse_res >>= fun input -> + let driver = + Driver.create ~restarts:!restarts ~pp_cnf:!p_cnf ~time:!time_limit + ~memory:!mem_limit ~pp_model:!p_model ?proof_file ~check:!check + ~progress:!p_progress solver + in + (* process statements *) let res = - try - E.fold_l - (fun () -> - Process.process_stmt ~gc:!gc ~restarts:!restarts ~pp_cnf:!p_cnf - ~time:!time_limit ~memory:!mem_limit ~pp_model:!p_model ?proof_file - ~check:!check ~progress:!p_progress solver) - () input + try E.fold_l (fun () stmt -> Driver.process_stmt driver stmt) () input with Exit -> E.return () in res diff --git a/src/smtlib/Process.ml b/src/smtlib/Driver.ml similarity index 51% rename from src/smtlib/Process.ml rename to src/smtlib/Driver.ml index 88a94ab9..62da044d 100644 --- a/src/smtlib/Process.ml +++ b/src/smtlib/Driver.ml @@ -1,8 +1,7 @@ -(** {2 Conversion into {!Term.t}} *) - open Sidekick_core module Profile = Sidekick_util.Profile open! Sidekick_base +open Common_ [@@@ocaml.warning "-32"] @@ -10,65 +9,6 @@ type 'a or_error = ('a, string) CCResult.t module E = CCResult module Fmt = CCFormat -module Solver = Sidekick_base.Solver - -module Check_cc = struct - module SI = Sidekick_smt_solver.Solver_internal - module MCC = Sidekick_mini_cc - - let pp_c out c = Fmt.fprintf out "(@[%a@])" (Util.pp_list ~sep:" ∨ " Lit.pp) c - - let pp_and out c = - Fmt.fprintf out "(@[%a@])" (Util.pp_list ~sep:" ∧ " Lit.pp) c - - let add_cc_lit (cc : MCC.t) (lit : Lit.t) : unit = - let t = Lit.term lit in - MCC.add_lit cc t (Lit.sign lit) - - (* check that this is a proper CC conflict *) - let check_conflict si _cc (confl : Lit.t list) : unit = - Log.debugf 15 (fun k -> k "(@[check-cc-conflict@ %a@])" pp_c confl); - let tst = SI.tst si in - let cc = MCC.create_default tst in - (* add [¬confl] and check it's unsat *) - List.iter (fun lit -> add_cc_lit cc @@ Lit.neg lit) confl; - if MCC.check_sat cc then - Error.errorf - "@[<2>check-cc-conflict:@ @[clause %a@]@ is not a UF tautology \ - (negation is sat)@]" - pp_c confl - else - Log.debugf 15 (fun k -> k "(@[check-cc-conflict.ok@ %a@])" pp_c confl) - - let check_propagation si _cc p reason : unit = - let reason = reason () in - Log.debugf 15 (fun k -> - k "(@[check-cc-prop@ %a@ :reason %a@])" Lit.pp p pp_and reason); - let tst = SI.tst si in - let cc = MCC.create_default tst in - (* add [reason & ¬lit] and check it's unsat *) - List.iter (add_cc_lit cc) reason; - add_cc_lit cc (Lit.neg p); - if MCC.check_sat cc then - Error.errorf - "@[<2>check-cc-prop:@ @[%a => %a@]@ is not a UF tautology (negation is \ - sat)@]" - pp_and reason Lit.pp p - else - Log.debugf 15 (fun k -> - k "(@[check-cc-prop.ok@ @[%a => %a@]@])" pp_and reason Lit.pp p) - - let theory = - Solver.mk_theory ~name:"cc-check" - ~create_and_setup:(fun ~id:_ si -> - let n_calls = Stat.mk_int (SI.stats si) "check-cc.call" in - SI.on_cc_conflict si (fun { cc; th; c } -> - if not th then ( - Stat.incr n_calls; - check_conflict si cc c - ))) - () -end (* TODO: use external proof checker instead: check-sat(φ + model) (* check SMT model *) @@ -113,78 +53,85 @@ end Vec.iter check_c hyps *) -let reset_line = "\x1b[2K\r" -let start = Sys.time () - -let mk_progress (_s : Solver.t) : _ -> unit = - let n = ref 0 in - let syms = "|\\-/" in - fun _s -> - let diff = Sys.time () -. start in - incr n; - (* TODO: print some core stats in the progress bar - let n_cl = Solver.pp_stats - *) - (* limit frequency *) - if float !n > 6. *. diff then ( - let sym = String.get syms (!n mod String.length syms) in - Printf.printf "%s[%.2fs %c]" reset_line diff sym; - n := 0; - flush stdout - ) - -let with_file_out (file : string) (f : out_channel -> 'a) : 'a = - if Filename.extension file = ".gz" then ( - let p = - Unix.open_process_out - (Printf.sprintf "gzip -c - > \"%s\"" (String.escaped file)) - in - CCFun.finally1 ~h:(fun () -> Unix.close_process_out p) f p - ) else - CCIO.with_out file f +type t = { + progress: Progress_bar.t option; + solver: Solver.t; + time_start: float; + time_limit: float; + memory_limit: float; + proof_file: string option; + pp_model: bool; + pp_cnf: bool; + check: bool; + restarts: bool; +} (* call the solver to check-sat *) -let solve ?gc:_ ?restarts:_ ?proof_file ?(pp_model = false) ?(check = false) - ?time ?memory ?(progress = false) ~assumptions s : Solver.res = - let t1 = Sys.time () in - let on_progress = +let create ?(restarts = true) ?(pp_cnf = false) ?proof_file ?(pp_model = false) + ?(check = false) ?time ?memory ?(progress = false) (solver : Solver.t) : t = + let time_start = now () in + let progress = if progress then - Some (mk_progress s) + Some (Progress_bar.create ()) else None - and clear_line () = if progress then Printf.printf "%s%!" reset_line in + in - let should_stop = - match time, memory with - | None, None -> None - | _ -> - let time = Option.value ~default:3600. time in - (* default: 1 hour *) - let memory = Option.value ~default:4e9 memory in - (* default: 4 GB *) - let stop _ _ = - if Sys.time () -. t1 > time then ( - Log.debugf 0 (fun k -> k "timeout"); - true - ) else if float (Gc.quick_stat ()).Gc.heap_words *. 8. > memory then ( - Log.debugf 0 (fun k -> k "%S" "exceeded memory limit"); - true - ) else - false - in - Some stop + let time_limit = Option.value ~default:3600. time in + (* default: 1 hour *) + let memory_limit = Option.value ~default:4e9 memory in + + { + time_start; + restarts; + progress; + solver; + proof_file; + pp_model; + pp_cnf; + check; + time_limit; + memory_limit; + } + +let decl_sort (_self : t) c n : unit = + (* TODO: more? pass to abstract solver? *) + Log.debugf 1 (fun k -> k "(@[declare-sort %a@ :arity %d@])" ID.pp c n) + +let decl_fun (_self : t) id args ret : unit = + (* TODO: more? record for model building *) + Log.debugf 1 (fun k -> + k "(@[declare-fun %a@ :args (@[%a@])@ :ret %a@])" ID.pp id + (Util.pp_list Ty.pp) args Ty.pp ret) + +(* call the solver to check satisfiability *) +let solve (self : t) ~assumptions () : Solver.res = + let t1 = now () in + let should_stop _ _ = + if now () -. self.time_start > self.time_limit then ( + Log.debugf 0 (fun k -> k "timeout"); + true + ) else if float (Gc.quick_stat ()).Gc.heap_words *. 8. > self.memory_limit + then ( + Log.debugf 0 (fun k -> k "%S" "exceeded memory limit"); + true + ) else + false + in + + let on_progress = + Option.map (fun p _s -> Progress_bar.tick p) self.progress in let res = let@ () = Profile.with_ "process.solve" in - Solver.solve ~assumptions ?on_progress ?should_stop s - (* ?gc ?restarts ?time ?memory ?progress *) + Solver.solve ~assumptions ?on_progress ~should_stop self.solver in - let t2 = Sys.time () in + let t2 = now () in flush stdout; (match res with | Solver.Sat m -> - if pp_model then + if self.pp_model then (* TODO: use actual {!Model} in the solver? or build it afterwards *) Format.printf "(@[model@ %a@])@." Sidekick_smt_solver.Model.pp m; (* TODO @@ -193,11 +140,11 @@ let solve ?gc:_ ?restarts:_ ?proof_file ?(pp_model = false) ?(check = false) CCOpt.iter (fun h -> check_smt_model (Solver.solver s) h m) hyps; ); *) - let t3 = Sys.time () in + let t3 = now () in Fmt.printf "sat@."; - Fmt.printf "; (%.3f/%.3f/%.3f)@." (t1 -. start) (t2 -. t1) (t3 -. t2) + Fmt.printf "; (%.3f/%.3f/%.3f)@." (t1 -. time_start) (t2 -. t1) (t3 -. t2) | Solver.Unsat { unsat_step_id; unsat_core = _ } -> - if check then + if self.check then () (* FIXME: check trace? match proof_opt with @@ -206,12 +153,12 @@ let solve ?gc:_ ?restarts:_ ?proof_file ?(pp_model = false) ?(check = false) | _ -> () *); - (match proof_file with + (match self.proof_file with | Some file -> (match unsat_step_id () with | None -> () | Some step_id -> - let proof = Solver.proof s in + let proof = Solver.proof self.solver in let proof_quip = Profile.with_ "proof.to-quip" @@ fun () -> assert false (* TODO @@ -226,14 +173,14 @@ let solve ?gc:_ ?restarts:_ ?proof_file ?(pp_model = false) ?(check = false) flush oc) | _ -> ()); - let t3 = Sys.time () in + let t3 = now () in Fmt.printf "unsat@."; - Fmt.printf "; (%.3f/%.3f/%.3f)@." (t1 -. start) (t2 -. t1) (t3 -. t2) + Fmt.printf "; (%.3f/%.3f/%.3f)@." (t1 -. time_start) (t2 -. t1) (t3 -. t2) | Solver.Unknown reas -> Fmt.printf "unknown@."; Fmt.printf "; @[:reason %a@]@." Solver.Unknown.pp reas | exception exn -> - clear_line (); + Option.iter Progress_bar.clear_line self.progress; raise exn); res @@ -241,24 +188,12 @@ let known_logics = [ "QF_UF"; "QF_LRA"; "QF_UFLRA"; "QF_DT"; "QF_UFDT"; "QF_LIA"; "QF_UFLIA" ] (* process a single statement *) -let process_stmt ?gc ?restarts ?(pp_cnf = false) ?proof_file ?pp_model - ?(check = false) ?time ?memory ?progress (solver : Solver.t) - (stmt : Statement.t) : unit or_error = +let process_stmt (self : t) (stmt : Statement.t) : unit or_error = let@ () = Profile.with_ "smtlib.process-stmt" in Log.debugf 5 (fun k -> k "(@[smtlib.process-statement@ %a@])" Statement.pp stmt); - let decl_sort c n : unit = - Log.debugf 1 (fun k -> k "(@[declare-sort %a@ :arity %d@])" ID.pp c n) - (* TODO: more? *) - in - let decl_fun id args ret : unit = - Log.debugf 1 (fun k -> - k "(@[declare-fun %a@ :args (@[%a@])@ :ret %a@])" ID.pp id - (Util.pp_list Ty.pp) args Ty.pp ret) - (* TODO: more? *) - in - let add_step r = Proof_trace.add_step (Solver.proof solver) r in + let add_step r = Proof_trace.add_step (Solver.proof self.solver) r in match stmt with | Statement.Stmt_set_logic logic -> @@ -276,47 +211,44 @@ let process_stmt ?gc ?restarts ?(pp_cnf = false) ?proof_file ?pp_model | Statement.Stmt_check_sat l -> (* FIXME: how to map [l] to [assumptions] in proof? *) let assumptions = - List.map (fun (sign, t) -> Solver.mk_lit_t solver ~sign t) l + List.map (fun (sign, t) -> Solver.mk_lit_t self.solver ~sign t) l in - ignore - (solve ?gc ?restarts ~check ?pp_model ?proof_file ?time ?memory ?progress - ~assumptions solver - : Solver.res); + ignore (solve self ~assumptions () : Solver.res); E.return () | Statement.Stmt_ty_decl (id, n) -> - decl_sort id n; + decl_sort self id n; E.return () | Statement.Stmt_decl (f, ty_args, ty_ret) -> - decl_fun f ty_args ty_ret; + decl_fun self f ty_args ty_ret; E.return () | Statement.Stmt_assert t -> - if pp_cnf then Format.printf "(@[assert@ %a@])@." Term.pp t; - let lit = Solver.mk_lit_t solver t in - Solver.add_clause solver [| lit |] + if self.pp_cnf then Format.printf "(@[assert@ %a@])@." Term.pp t; + let lit = Solver.mk_lit_t self.solver t in + Solver.add_clause self.solver [| lit |] (add_step @@ fun () -> Proof_sat.sat_input_clause [ lit ]); E.return () | Statement.Stmt_assert_clause c_ts -> - if pp_cnf then + if self.pp_cnf then Format.printf "(@[assert-clause@ %a@])@." (Util.pp_list Term.pp) c_ts; - let c = CCList.map (fun t -> Solver.mk_lit_t solver t) c_ts in + let c = CCList.map (fun t -> Solver.mk_lit_t self.solver t) c_ts in (* proof of assert-input + preprocessing *) let pr = add_step @@ fun () -> - let lits = List.map (Solver.mk_lit_t solver) c_ts in + let lits = List.map (Solver.mk_lit_t self.solver) c_ts in Proof_sat.sat_input_clause lits in - Solver.add_clause solver (CCArray.of_list c) pr; + Solver.add_clause self.solver (CCArray.of_list c) pr; E.return () | Statement.Stmt_get_model -> - (match Solver.last_res solver with + (match Solver.last_res self.solver with | Some (Solver.Sat m) -> Fmt.printf "%a@." Sidekick_smt_solver.Model.pp m | _ -> Error.errorf "cannot access model"); E.return () | Statement.Stmt_get_value l -> - (match Solver.last_res solver with + (match Solver.last_res self.solver with | Some (Solver.Sat m) -> let l = List.map @@ -333,9 +265,11 @@ let process_stmt ?gc ?restarts ?(pp_cnf = false) ?proof_file ?pp_model | _ -> Error.errorf "cannot access model"); E.return () | Statement.Stmt_data ds -> - List.iter (fun d -> Solver.add_ty solver (Data_ty.data_as_ty d)) ds; + List.iter (fun d -> Solver.add_ty self.solver (Data_ty.data_as_ty d)) ds; E.return () - | Statement.Stmt_define _ -> Error.errorf "cannot deal with definitions yet" + | Statement.Stmt_define _ -> + (* TODO *) + Error.errorf "cannot deal with definitions yet" open Sidekick_base diff --git a/src/smtlib/Process.mli b/src/smtlib/Driver.mli similarity index 59% rename from src/smtlib/Process.mli rename to src/smtlib/Driver.mli index 8e0501e0..fd9d3f7c 100644 --- a/src/smtlib/Process.mli +++ b/src/smtlib/Driver.mli @@ -1,7 +1,11 @@ -(** {1 Process Statements} *) +(** Driver. + + The driver is responsible for processing statements from a SMTLIB file, + and interacting with the solver based on the statement (asserting formulas, + calling "solve", etc.) +*) open Sidekick_base -module Solver = Sidekick_base.Solver val th_bool_dyn : Solver.theory val th_bool_static : Solver.theory @@ -12,13 +16,10 @@ val th_ty_unin : Solver.theory type 'a or_error = ('a, string) CCResult.t -module Check_cc : sig - val theory : Solver.theory - (** theory that check validity of conflicts *) -end +type t +(** The SMTLIB driver *) -val process_stmt : - ?gc:bool -> +val create : ?restarts:bool -> ?pp_cnf:bool -> ?proof_file:string -> @@ -28,5 +29,6 @@ val process_stmt : ?memory:float -> ?progress:bool -> Solver.t -> - Statement.t -> - unit or_error + t + +val process_stmt : t -> Statement.t -> unit or_error diff --git a/src/smtlib/Sidekick_smtlib.ml b/src/smtlib/Sidekick_smtlib.ml index 47b0ee1d..26f43235 100644 --- a/src/smtlib/Sidekick_smtlib.ml +++ b/src/smtlib/Sidekick_smtlib.ml @@ -1,12 +1,11 @@ -(** {1 Process Statements} *) - module Loc = Smtlib_utils.V_2_6.Loc module Parse_ast = Smtlib_utils.V_2_6.Ast -module Process = Process -module Solver = Process.Solver +module Driver = Driver +module Solver = Solver module Term = Sidekick_base.Term module Stmt = Sidekick_base.Statement module Proof_trace = Sidekick_core.Proof_trace +module Check_cc = Check_cc type 'a or_error = ('a, string) CCResult.t diff --git a/src/smtlib/Sidekick_smtlib.mli b/src/smtlib/Sidekick_smtlib.mli index 6f7e92f4..c3921b89 100644 --- a/src/smtlib/Sidekick_smtlib.mli +++ b/src/smtlib/Sidekick_smtlib.mli @@ -1,6 +1,6 @@ -(** {1 SMTLib-2 Interface} *) +(** SMTLib-2.6 Driver *) -(** This library provides a parser, a type-checker, and a solver interface +(** This library provides a parser, a type-checker, and a driver for processing SMTLib-2 problems. *) @@ -8,9 +8,10 @@ type 'a or_error = ('a, string) CCResult.t module Term = Sidekick_base.Term module Stmt = Sidekick_base.Statement -module Process = Process -module Solver = Process.Solver +module Driver = Driver +module Solver = Solver module Proof_trace = Sidekick_core.Proof_trace +module Check_cc = Check_cc val parse : Term.store -> string -> Stmt.t list or_error val parse_stdin : Term.store -> Stmt.t list or_error diff --git a/src/smtlib/Typecheck.ml b/src/smtlib/Typecheck.ml index 61b157f0..c54a7de6 100644 --- a/src/smtlib/Typecheck.ml +++ b/src/smtlib/Typecheck.ml @@ -1,7 +1,5 @@ (* This file is free software. See file "license" for more details. *) -(** {1 Preprocessing AST} *) - open! Sidekick_base module Loc = Smtlib_utils.V_2_6.Loc module PA = Smtlib_utils.V_2_6.Ast @@ -16,9 +14,7 @@ type 'a or_error = ('a, string) CCResult.t let pp_loc_opt = Loc.pp_opt -(** {2 Parsing} *) - -module StrTbl = CCHashtbl.Make (CCString) +module StrTbl = Util.Str_tbl module Ctx = struct type kind = K_ty of ty_kind | K_fun of Term.t diff --git a/src/smtlib/Typecheck.mli b/src/smtlib/Typecheck.mli index 9df06a46..3727fe15 100644 --- a/src/smtlib/Typecheck.mli +++ b/src/smtlib/Typecheck.mli @@ -1,6 +1,4 @@ -(* This file is free software. See file "license" for more details. *) - -(** {1 Preprocessing AST} *) +(** Typing AST *) module Loc = Smtlib_utils.V_2_6.Loc module PA = Smtlib_utils.V_2_6.Ast @@ -9,8 +7,9 @@ module Stmt = Sidekick_base.Statement type 'a or_error = ('a, string) CCResult.t -(** {2 Parsing and Typing} *) +(** {2 Type-checking and type inference} *) +(** Typing context *) module Ctx : sig type t @@ -19,5 +18,7 @@ module Ctx : sig val create : T.store -> t end +(** {2 Conversion from smtlib-utils} *) + val conv_term : Ctx.t -> PA.term -> T.t val conv_statement : Ctx.t -> PA.statement -> Stmt.t list diff --git a/src/smtlib/check_cc.ml b/src/smtlib/check_cc.ml new file mode 100644 index 00000000..4bb128aa --- /dev/null +++ b/src/smtlib/check_cc.ml @@ -0,0 +1,55 @@ +open Sidekick_core +module SI = Sidekick_smt_solver.Solver_internal +module MCC = Sidekick_mini_cc + +let pp_c out c = Fmt.fprintf out "(@[%a@])" (Util.pp_list ~sep:" ∨ " Lit.pp) c + +let pp_and out c = Fmt.fprintf out "(@[%a@])" (Util.pp_list ~sep:" ∧ " Lit.pp) c + +let add_cc_lit (cc : MCC.t) (lit : Lit.t) : unit = + let t = Lit.term lit in + MCC.add_lit cc t (Lit.sign lit) + +(* check that this is a proper CC conflict *) +let check_conflict si _cc (confl : Lit.t list) : unit = + Log.debugf 15 (fun k -> k "(@[check-cc-conflict@ %a@])" pp_c confl); + let tst = SI.tst si in + let cc = MCC.create_default tst in + (* add [¬confl] and check it's unsat *) + List.iter (fun lit -> add_cc_lit cc @@ Lit.neg lit) confl; + if MCC.check_sat cc then + Error.errorf + "@[<2>check-cc-conflict:@ @[clause %a@]@ is not a UF tautology (negation \ + is sat)@]" + pp_c confl + else + Log.debugf 15 (fun k -> k "(@[check-cc-conflict.ok@ %a@])" pp_c confl) + +let check_propagation si _cc p reason : unit = + let reason = reason () in + Log.debugf 15 (fun k -> + k "(@[check-cc-prop@ %a@ :reason %a@])" Lit.pp p pp_and reason); + let tst = SI.tst si in + let cc = MCC.create_default tst in + (* add [reason & ¬lit] and check it's unsat *) + List.iter (add_cc_lit cc) reason; + add_cc_lit cc (Lit.neg p); + if MCC.check_sat cc then + Error.errorf + "@[<2>check-cc-prop:@ @[%a => %a@]@ is not a UF tautology (negation is \ + sat)@]" + pp_and reason Lit.pp p + else + Log.debugf 15 (fun k -> + k "(@[check-cc-prop.ok@ @[%a => %a@]@])" pp_and reason Lit.pp p) + +let theory = + Solver.mk_theory ~name:"cc-check" + ~create_and_setup:(fun ~id:_ si -> + let n_calls = Stat.mk_int (SI.stats si) "check-cc.call" in + SI.on_cc_conflict si (fun { cc; th; c } -> + if not th then ( + Stat.incr n_calls; + check_conflict si cc c + ))) + () diff --git a/src/smtlib/check_cc.mli b/src/smtlib/check_cc.mli new file mode 100644 index 00000000..266cb197 --- /dev/null +++ b/src/smtlib/check_cc.mli @@ -0,0 +1,2 @@ +val theory : Solver.theory +(** theory that check validity of EUF conflicts, on the fly *) diff --git a/src/smtlib/common_.ml b/src/smtlib/common_.ml new file mode 100644 index 00000000..3f0031d6 --- /dev/null +++ b/src/smtlib/common_.ml @@ -0,0 +1,16 @@ +(** Current timestamp *) +let now () : float = Unix.gettimeofday () + +(** Timestamp at the beginning of the program *) +let time_start = now () + +(** write to file, possibly with compression *) +let with_file_out (file : string) (f : out_channel -> 'a) : 'a = + if Filename.extension file = ".gz" then ( + let p = + Unix.open_process_out + (Printf.sprintf "gzip -c - > \"%s\"" (String.escaped file)) + in + CCFun.finally1 ~h:(fun () -> Unix.close_process_out p) f p + ) else + CCIO.with_out file f diff --git a/src/smtlib/dune b/src/smtlib/dune index e32fd5b9..82bb0fd3 100644 --- a/src/smtlib/dune +++ b/src/smtlib/dune @@ -1,6 +1,8 @@ (library (name sidekick_smtlib) - (public_name sidekick-bin.smtlib) + (public_name sidekick-base.smtlib) + (synopsis "SMTLIB 2.6 driver for Sidekick") + (private_modules Common_) (libraries containers zarith sidekick.core sidekick.util sidekick-base sidekick.mini-cc smtlib-utils sidekick.tef) (flags :standard -warn-error -a+8 -open Sidekick_util)) diff --git a/src/smtlib/progress_bar.ml b/src/smtlib/progress_bar.ml new file mode 100644 index 00000000..9fd6334c --- /dev/null +++ b/src/smtlib/progress_bar.ml @@ -0,0 +1,26 @@ +open Common_ + +let reset_line = "\x1b[2K\r" +let start = now () + +type t = unit -> unit + +let tick (self : t) = self () +let clear_line _ : unit = Printf.printf "%s%!" reset_line + +let create () : t = + let n = ref 0 in + let syms = "|\\-/" in + fun () -> + let diff = now () -. start in + incr n; + (* TODO: print some core stats in the progress bar + let n_cl = Solver.pp_stats + *) + (* limit frequency *) + if float !n > 6. *. diff then ( + let sym = String.get syms (!n mod String.length syms) in + Printf.printf "%s[%.2fs %c]" reset_line diff sym; + n := 0; + flush stdout + ) diff --git a/src/smtlib/progress_bar.mli b/src/smtlib/progress_bar.mli new file mode 100644 index 00000000..02ce6175 --- /dev/null +++ b/src/smtlib/progress_bar.mli @@ -0,0 +1,7 @@ +(** Super simple progress bar *) + +type t + +val create : unit -> t +val tick : t -> unit +val clear_line : t -> unit diff --git a/src/smtlib/solver.ml b/src/smtlib/solver.ml new file mode 100644 index 00000000..38549245 --- /dev/null +++ b/src/smtlib/solver.ml @@ -0,0 +1 @@ +include Sidekick_base.Solver