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

refactor: smtlib driver now part of base; make it stateful

Browse source
This commit is contained in:
Simon Cruanes 2022-10-10 14:21:10 -04:00
parent 2f96f36e75
commit e3e71f3d76
No known key found for this signature in database
GPG key ID: EBFFF6F283F3A2B4
17 changed files with 242 additions and 208 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

4
dune-project
View file

@ -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

1
sidekick-bin.opam
View file

@ -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"

2
src/main/dune
View file

@ -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))

27
src/main/main.ml
View file

@ -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

252
src/smtlib/Process.ml → src/smtlib/Driver.ml
View file

@ -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 "(@[<hv1>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 "; @[<h>: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 "(@[<hv1>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 "(@[<hv1>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 "(@[<hv1>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

22
src/smtlib/Process.mli → src/smtlib/Driver.mli
View file

@ -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

7
src/smtlib/Sidekick_smtlib.ml
View file

@ -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

9
src/smtlib/Sidekick_smtlib.mli
View file

@ -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

6
src/smtlib/Typecheck.ml
View file

@ -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

9
src/smtlib/Typecheck.mli
View file

@ -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

55
src/smtlib/check_cc.ml Normal file
View file

@ -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
)))
()

2
src/smtlib/check_cc.mli Normal file
View file

@ -0,0 +1,2 @@
val theory : Solver.theory
(** theory that check validity of EUF conflicts, on the fly *)

16
src/smtlib/common_.ml Normal file
View file

@ -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

4
src/smtlib/dune
View file

@ -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))

26
src/smtlib/progress_bar.ml Normal file
View file

@ -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
)

7
src/smtlib/progress_bar.mli Normal file
View file

@ -0,0 +1,7 @@
(** Super simple progress bar *)
type t
val create : unit -> t
val tick : t -> unit
val clear_line : t -> unit

1
src/smtlib/solver.ml Normal file
View file

@ -0,0 +1 @@
include Sidekick_base.Solver