From 4e34bbdf59a05ded25ecac7453a5541053e3ac2f Mon Sep 17 00:00:00 2001 From: Guillaume Bury Date: Thu, 18 Dec 2014 16:04:17 +0100 Subject: [PATCH] Added some headers, and an interface for Expr --- msat.odocl | 43 ++++----- sat/sat.ml | 6 +- smt/expr.mli | 48 ++++++++++ smt/mcsat.ml | 3 +- smt/unionfind.ml | 5 ++ solver/expr_intf.ml | 21 ++--- solver/formula_intf.ml | 19 ++-- solver/mcsolver.ml | 16 ++-- solver/mcsolver.mli | 17 ++-- solver/plugin_intf.ml | 2 +- solver/res_intf.ml | 6 +- solver/theory_intf.ml | 2 +- util/bench_stats.ml | 162 ---------------------------------- util/either.ml | 5 ++ util/either.mli | 6 +- util/parselog.ml | 114 ------------------------ util/parselog.mli | 14 --- util/sat_solve.ml | 5 ++ util/smtlib/smtlib.ml | 6 +- util/smtlib/smtlib.mli | 6 +- util/smtlib/smtlib_syntax.mli | 6 +- util/smtlib/smtlib_util.mli | 6 ++ 22 files changed, 141 insertions(+), 377 deletions(-) create mode 100644 smt/expr.mli delete mode 100644 util/bench_stats.ml delete mode 100644 util/parselog.ml delete mode 100644 util/parselog.mli diff --git a/msat.odocl b/msat.odocl index b27aa779..4d7d1c98 100644 --- a/msat.odocl +++ b/msat.odocl @@ -1,27 +1,20 @@ -sat/Formula_intf -sat/Explanation -sat/Explanation_intf -sat/Res -sat/Res_intf -sat/Sat -sat/Solver -sat/Solver_types -sat/Solver_types_intf -sat/Theory_intf +solver/Formula_intf +solver/Expr_intf -#smt/Arith -#smt/Cc -#smt/Combine -#smt/Exception -#smt/Fm -#smt/Intervals -#smt/Literal -#smt/Polynome +solver/Res +solver/Res_intf +solver/Mcproof + +solver/Solver +solver/Solver_types +solver/Solver_types_intf +solver/Mcsolver +solver/Mcsolver_types +solver/Mcsolver_types_intf + +solver/Theory_intf +solver/Plugin_intf + +#sat/Sat #smt/Smt -#smt/Sum -#smt/Symbols -#smt/Term -#smt/Ty -#smt/Uf -#smt/Use - +#smt/Mcsat diff --git a/sat/sat.ml b/sat/sat.ml index 5a25e389..fbcfae89 100644 --- a/sat/sat.ml +++ b/sat/sat.ml @@ -1,4 +1,8 @@ -(* Copyright 2014 Guillaume Bury *) +(* +MSAT is free software, using the Apache license, see file LICENSE +Copyright 2014 Guillaume Bury +Copyright 2014 Simon Cruanes +*) module Fsat = struct exception Dummy of int diff --git a/smt/expr.mli b/smt/expr.mli new file mode 100644 index 00000000..cff2bf41 --- /dev/null +++ b/smt/expr.mli @@ -0,0 +1,48 @@ +(* +MSAT is free software, using the Apache license, see file LICENSE +Copyright 2014 Guillaume Bury +Copyright 2014 Simon Cruanes +*) + +type var = string +type formula = private + | Prop of int + | Equal of var * var + | Distinct of var * var + +type t = formula + +val dummy : t + +val fresh : unit -> t + +val mk_prop : int -> t +val mk_eq : var -> var -> t +val mk_neq : var -> var -> t + +val neg : t -> t +val norm : t -> t * bool + +val hash : t -> int +val equal : t -> t -> bool +val compare : t -> t -> int + +val label : t -> Hstring.t +val add_label : Hstring.t -> t -> unit + +val print : Format.formatter -> t -> unit + +module Term : sig + type t = var + val hash : t -> int + val equal : t -> t -> bool + val compare : t -> t -> int + val print : Format.formatter -> t -> unit +end +module Formula : sig + type t = formula + val hash : t -> int + val equal : t -> t -> bool + val compare : t -> t -> int + val print : Format.formatter -> t -> unit +end diff --git a/smt/mcsat.ml b/smt/mcsat.ml index f8f4c921..b9012b25 100644 --- a/smt/mcsat.ml +++ b/smt/mcsat.ml @@ -12,7 +12,7 @@ module Tsmt = struct module CC = Cc.Make(String) (* Type definitions *) - type term = Fsmt.var + type term = Fsmt.Term.t type formula = Fsmt.t type proof = unit @@ -72,7 +72,6 @@ module Tsmt = struct env := { !env with cc = CC.add_eq !env.cc i j } | Fsmt.Distinct (i, j) -> env := { !env with cc = CC.add_neq !env.cc i j } - | _ -> assert false done; Sat (current_level ()) with CC.Unsat x -> diff --git a/smt/unionfind.ml b/smt/unionfind.ml index fcf98da4..f77c440c 100644 --- a/smt/unionfind.ml +++ b/smt/unionfind.ml @@ -1,3 +1,8 @@ +(* +MSAT is free software, using the Apache license, see file LICENSE +Copyright 2014 Guillaume Bury +Copyright 2014 Simon Cruanes +*) (* Union-find Module *) module Make(T : Sig.OrderedType) = struct diff --git a/solver/expr_intf.ml b/solver/expr_intf.ml index 25338cd7..1117b05b 100644 --- a/solver/expr_intf.ml +++ b/solver/expr_intf.ml @@ -1,20 +1,11 @@ -(**************************************************************************) -(* *) -(* Cubicle *) -(* Combining model checking algorithms and SMT solvers *) -(* *) -(* Guillaume Bury *) -(* INRIA *) -(* Sylvain Conchon and Alain Mebsout *) -(* Universite Paris-Sud 11 *) -(* *) -(* Copyright 2011. This file is distributed under the terms of the *) -(* Apache Software License version 2.0 *) -(* *) -(**************************************************************************) +(* +MSAT is free software, using the Apache license, see file LICENSE +Copyright 2014 Guillaume Bury +Copyright 2014 Simon Cruanes +*) module type S = sig - (** Signature of formulas that parametrises the SMT Solver Module. *) + (** Signature of formulas that parametrises the Mcsat Solver Module. *) module Term : sig (** The type of terms *) diff --git a/solver/formula_intf.ml b/solver/formula_intf.ml index ac55cf23..712b9566 100644 --- a/solver/formula_intf.ml +++ b/solver/formula_intf.ml @@ -1,17 +1,8 @@ -(**************************************************************************) -(* *) -(* Cubicle *) -(* Combining model checking algorithms and SMT solvers *) -(* *) -(* Guillaume Bury *) -(* INRIA *) -(* Sylvain Conchon and Alain Mebsout *) -(* Universite Paris-Sud 11 *) -(* *) -(* Copyright 2011. This file is distributed under the terms of the *) -(* Apache Software License version 2.0 *) -(* *) -(**************************************************************************) +(* +MSAT is free software, using the Apache license, see file LICENSE +Copyright 2014 Guillaume Bury +Copyright 2014 Simon Cruanes +*) module type S = sig (** Signature of formulas that parametrises the SMT Solver Module. *) diff --git a/solver/mcsolver.ml b/solver/mcsolver.ml index 08b3748a..a6fa0acb 100644 --- a/solver/mcsolver.ml +++ b/solver/mcsolver.ml @@ -1,14 +1,8 @@ -(**************************************************************************) -(* *) -(* Alt-Ergo Zero *) -(* *) -(* Sylvain Conchon and Alain Mebsout *) -(* Universite Paris-Sud 11 *) -(* *) -(* Copyright 2011. This file is distributed under the terms of the *) -(* Apache Software License version 2.0 *) -(* *) -(**************************************************************************) +(* +MSAT is free software, using the Apache license, see file LICENSE +Copyright 2014 Guillaume Bury +Copyright 2014 Simon Cruanes +*) module Make (E : Expr_intf.S) (Th : Plugin_intf.S with type term = E.Term.t and type formula = E.Formula.t) = struct diff --git a/solver/mcsolver.mli b/solver/mcsolver.mli index ab7d43f9..120077f8 100644 --- a/solver/mcsolver.mli +++ b/solver/mcsolver.mli @@ -1,15 +1,8 @@ -(**************************************************************************) -(* *) -(* Cubicle *) -(* Combining model checking algorithms and SMT solvers *) -(* *) -(* Mohamed Iguernelala *) -(* Universite Paris-Sud 11 *) -(* *) -(* Copyright 2011. This file is distributed under the terms of the *) -(* Apache Software License version 2.0 *) -(* *) -(**************************************************************************) +(* +MSAT is free software, using the Apache license, see file LICENSE +Copyright 2014 Guillaume Bury +Copyright 2014 Simon Cruanes +*) module Make (E : Expr_intf.S) (Th : Plugin_intf.S with type term = E.Term.t and type formula = E.Formula.t) : sig diff --git a/solver/plugin_intf.ml b/solver/plugin_intf.ml index 8a4a9c36..0c7e9076 100644 --- a/solver/plugin_intf.ml +++ b/solver/plugin_intf.ml @@ -13,7 +13,7 @@ (**************************************************************************) module type S = sig - (** Singature for theories to be given to the Solver. *) + (** Signature for theories to be given to the Model Constructing Solver. *) type term (** The type of terms. Should be compatible with Expr_intf.Term.t*) diff --git a/solver/res_intf.ml b/solver/res_intf.ml index 58332393..78a9ce97 100644 --- a/solver/res_intf.ml +++ b/solver/res_intf.ml @@ -1,4 +1,8 @@ -(* Copyright 2014 Guillaume Bury *) +(* +MSAT is free software, using the Apache license, see file LICENSE +Copyright 2014 Guillaume Bury +Copyright 2014 Simon Cruanes +*) module type S = sig (** Signature for a module handling proof by resolution from sat solving traces *) diff --git a/solver/theory_intf.ml b/solver/theory_intf.ml index 8358f3e7..68f90f74 100644 --- a/solver/theory_intf.ml +++ b/solver/theory_intf.ml @@ -13,7 +13,7 @@ (**************************************************************************) module type S = sig - (** Singature for theories to be given to the Solver. *) + (** Signature for theories to be given to the Solver. *) type formula (** The type of formulas. Should be compatble with Formula_intf.S *) diff --git a/util/bench_stats.ml b/util/bench_stats.ml deleted file mode 100644 index 0c008db9..00000000 --- a/util/bench_stats.ml +++ /dev/null @@ -1,162 +0,0 @@ -(* -MSAT is free software, using the Apache license, see file LICENSE -Copyright 2014 Guillaume Bury -Copyright 2014 Simon Cruanes -*) - -exception Commit_not_found -exception Commit_ambiguous - -(* Arguments parsing *) -let usage = "Usage : ./bench_stats [options] [commit1 [commit2]]" - -let arg_commit = ref [] -let anon s = arg_commit := s :: !arg_commit - -let info_commit = ref false -let long_diff = ref false -let args = Arg.align [ - "-info", Arg.Set info_commit, - " Adds info on the commit when printing stats"; - "-long", Arg.Set long_diff, - " Print a long diff instead of a short one"; -] - -(* Access functions *) -let get_commit s = - let d = Filename.concat (Filename.dirname Sys.argv.(0)) "bench" in - match Parselog.complete (Filename.concat d "logs") s with - | [c] -> Filename.basename c, Parselog.parse_commit c - | [] -> raise Commit_not_found - | _ -> raise Commit_ambiguous - - -(* Stats computing *) -type commit_stats = { - nb_sat : int; - nb_unsat : int; - nb_timeout : int; - nb_spaceout : int; - avg_time : float -} - -let get_stats h = - let avg = ref 0. in - let sat = ref 0 in - let unsat = ref 0 in - let timeout = ref 0 in - let spaceout = ref 0 in - let nb_success () = - float (!sat + !unsat) - in - let update_avg t = - let n = nb_success () in - avg := (!avg *. n +. t) /. (n +. 1.) - in - let aux f pb = Parselog.( - match pb.pb_st with - | Sat -> - update_avg pb.pb_time; - incr sat - | Unsat -> - update_avg pb.pb_time; - incr unsat - | Timeout -> - incr timeout - | Spaceout -> - incr spaceout - ) in - Hashtbl.iter aux h; - { - nb_sat = !sat; - nb_unsat = !unsat; - nb_timeout = !timeout; - nb_spaceout = !spaceout; - avg_time = !avg; - } - -(* Diff computing *) -type diff = { - sat_limit : string list; - sat_nopb : string list; - unsat_limit : string list; - unsat_nopb : string list; - disagree : (Parselog.pb * Parselog.pb) list; -} - -let empty_diff = { - sat_limit = []; - sat_nopb = []; - unsat_limit = []; - unsat_nopb = []; - disagree = []; -} - -let diff h h' = - let aux f pb acc = - try - let pb' = Hashtbl.find h' f in - Parselog.(match pb.pb_st, pb'.pb_st with - | Sat, Timeout | Sat, Spaceout -> - { acc with sat_limit = f :: acc.sat_limit } - | Unsat, Timeout | Unsat, Spaceout -> - { acc with unsat_limit = f :: acc.unsat_limit } - | Sat, Unsat | Unsat, Sat -> - { acc with disagree = (pb, pb') :: acc.disagree } - | _, _ -> acc - ) - with Not_found -> - match Parselog.(pb.pb_st) with - | Parselog.Sat -> { acc with sat_nopb = f :: acc.sat_nopb } - | Parselog.Unsat -> { acc with unsat_nopb = f :: acc.unsat_nopb } - | _ -> acc - in - Hashtbl.fold aux h empty_diff - -(* Printing *) -let print_stats s = - let sha, h = get_commit s in - let st = get_stats h in - Format.printf "%s@\nAverage time : %f (%d / %d)@\nTimeouts : %d@\nSpaceouts : %d@." - (if !info_commit then Parselog.commit_info sha else sha) st.avg_time (st.nb_sat + st.nb_unsat) - (st.nb_sat + st.nb_unsat + st.nb_timeout + st.nb_spaceout) st.nb_timeout st.nb_spaceout - -let print_diff_short s1 s2 = - let sha1, h1 = get_commit s1 in - let sha2, h2 = get_commit s2 in - let only1 = diff h1 h2 in - let only2 = diff h2 h1 in - Format.printf "1:%s -> 2:%s@\n" sha1 sha2; - Format.printf "Lost (only in 1) : %d (+ %d not in pb list)@\n" - (List.length only1.sat_limit + List.length only1.unsat_limit) (List.length only1.sat_nopb + List.length only1.unsat_nopb); - Format.printf "Won (only in 2) : %d (+ %d not in pb list)@\n" - (List.length only2.sat_limit + List.length only2.unsat_limit) (List.length only2.sat_nopb + List.length only2.unsat_nopb); - match List.sort_uniq Pervasives.compare (List.rev_append only1.disagree only2.disagree) with - | [] -> () - | l -> Format.printf "WARNING : %d incoherence@\n" (List.length l) - -let print_full h = - let aux f pb = - () - in - Hashtbl.iter aux h - -(* Main function *) -let main () = - Arg.parse args anon usage; - match List.rev (!arg_commit) with - | [] -> print_stats (Parselog.last_commit ()) - | [c] -> print_stats c - | [c1; c2] -> print_diff_short c1 c2 - | _ -> Arg.usage args usage -;; - -try - main () -with -| Commit_not_found -> - Format.printf "No such commit found@."; - exit 2 -| Commit_ambiguous -> - Format.printf "Too many commits fit this prefix@."; - exit 2 diff --git a/util/either.ml b/util/either.ml index ba1eb9bc..be411cd2 100644 --- a/util/either.ml +++ b/util/either.ml @@ -1,3 +1,8 @@ +(* +MSAT is free software, using the Apache license, see file LICENSE +Copyright 2014 Guillaume Bury +Copyright 2014 Simon Cruanes +*) type ('a, 'b) t = | Left of 'a diff --git a/util/either.mli b/util/either.mli index 2e2a8ba8..7fde7015 100644 --- a/util/either.mli +++ b/util/either.mli @@ -1,4 +1,8 @@ - +(* +MSAT is free software, using the Apache license, see file LICENSE +Copyright 2014 Guillaume Bury +Copyright 2014 Simon Cruanes +*) type ('a, 'b) t = | Left of 'a diff --git a/util/parselog.ml b/util/parselog.ml deleted file mode 100644 index 44d1d1f1..00000000 --- a/util/parselog.ml +++ /dev/null @@ -1,114 +0,0 @@ -(* -MSAT is free software, using the Apache license, see file LICENSE -Copyright 2014 Guillaume Bury -Copyright 2014 Simon Cruanes -*) - -(* Misc directory/files manipulation *) -let list_dir s = - let d = Unix.opendir s in - let l = ref [] in - try - while true do - l := (Filename.concat s (Unix.readdir d)) :: !l - done; - assert false - with End_of_file -> - !l - -let list_dir_files_rec s = - let rec aux acc = function - | [] -> acc - | f :: r -> - let f' = Filename.basename f in - if f' = Filename.current_dir_name || f' = Filename.parent_dir_name then - aux acc r - else begin match Unix.((stat f).st_kind) with - | Unix.S_REG -> aux (f :: acc) r - | Unix.S_DIR -> aux acc (List.rev_append (list_dir f) r) - | _ -> aux acc r - end - in - aux [] [s] - -(* Commit sha completion *) -let complete root sha = - let l = list_dir root in - let aux s = try String.sub s 0 (String.length sha) with Invalid_argument _ -> "" in - let test s = sha = aux (Filename.basename s) in - List.filter test l - -let commit_info sha = - let cmd = "git show "^ sha in - let ch = Unix.open_process_in cmd in - let l = (input_line ch :: input_line ch :: input_line ch :: input_line ch :: input_line ch :: input_line ch :: []) in - ignore (Unix.close_process_in ch); - String.concat "\n" (List.rev l) - -let last_commit () = - let ch = Unix.open_process_in "git rev-parse HEAD" in - let s = input_line ch in - ignore (Unix.close_process_in ch); - s - -(* Raw log file parsing *) -exception Empty_raw of string -exception Unknown_status of string * string list - -type status = - | Sat - | Unsat - | Timeout - | Spaceout - -type pb = { - pb_name : string; - pb_st : status; - pb_time : float; -} - -let str_cut s start len = - try String.sub s start len - with Invalid_argument _ -> "" - -let status_of_lines f = function - | ["Sat"] -> Sat - | ["Unsat"] -> Unsat - | ["Time limit exceeded"; _] -> Timeout - | ["Size limit exceeded"; _] -> Spaceout - | l -> - Format.printf "For file '%s' : unknown return string :@\n" f; - List.iter (fun s -> Format.printf "%s@." s) l; - raise (Unknown_status (f, l)) - -let parse_raw base f = - let f_in = open_in f in - let f_lines = ref [] in - begin try - while true do - f_lines := input_line f_in :: !f_lines - done; - assert false - with End_of_file -> - close_in f_in; - end; - match !f_lines with - | [] -> raise (Empty_raw f) - | s :: r -> - let st = status_of_lines f (List.rev r) in - assert (str_cut f 0 (String.length base) = base); - let file_name = String.sub f (String.length base) (String.length f - String.length base) in - { pb_name = file_name; pb_st = st; pb_time = float_of_string s } - -let parse_commit root = - let s = Filename.concat root "raw" in - let l = list_dir_files_rec s in - let res = Hashtbl.create (List.length l) in - List.iter (fun f -> - try - let pb = parse_raw s f in - Hashtbl.add res pb.pb_name pb - with Empty_raw _ | Unknown_status _ -> () - ) l; - res - diff --git a/util/parselog.mli b/util/parselog.mli deleted file mode 100644 index 68f6aeaf..00000000 --- a/util/parselog.mli +++ /dev/null @@ -1,14 +0,0 @@ -(* -MSAT is free software, using the Apache license, see file LICENSE -Copyright 2014 Guillaume Bury -Copyright 2014 Simon Cruanes -*) - -val complete : string -> string -> string list -val commit_info : string -> string -val last_commit : unit -> string - -type status = Sat | Unsat | Timeout | Spaceout -type pb = { pb_name : string; pb_st : status; pb_time : float; } - -val parse_commit : string -> (string, pb) Hashtbl.t diff --git a/util/sat_solve.ml b/util/sat_solve.ml index 00797258..51e4980c 100644 --- a/util/sat_solve.ml +++ b/util/sat_solve.ml @@ -1,3 +1,8 @@ +(* +MSAT is free software, using the Apache license, see file LICENSE +Copyright 2014 Guillaume Bury +Copyright 2014 Simon Cruanes +*) module F = Expr module T = Cnf.S diff --git a/util/smtlib/smtlib.ml b/util/smtlib/smtlib.ml index b27ce41f..2a1719b5 100644 --- a/util/smtlib/smtlib.ml +++ b/util/smtlib/smtlib.ml @@ -1,4 +1,8 @@ -(* Copyright 2014 INRIA **) +(* +MSAT is free software, using the Apache license, see file LICENSE +Copyright 2014 Guillaume Bury +Copyright 2014 Simon Cruanes +*) open Smtlib_syntax diff --git a/util/smtlib/smtlib.mli b/util/smtlib/smtlib.mli index 1120b12c..c5c5bfed 100644 --- a/util/smtlib/smtlib.mli +++ b/util/smtlib/smtlib.mli @@ -1,3 +1,7 @@ -(* Copyright 2014 INRIA *) +(* +MSAT is free software, using the Apache license, see file LICENSE +Copyright 2014 Guillaume Bury +Copyright 2014 Simon Cruanes +*) val parse : string -> Cnf.S.t list diff --git a/util/smtlib/smtlib_syntax.mli b/util/smtlib/smtlib_syntax.mli index f4c0223d..491d229c 100644 --- a/util/smtlib/smtlib_syntax.mli +++ b/util/smtlib/smtlib_syntax.mli @@ -1,4 +1,8 @@ -(* Copyright 2014 INRIA *) +(* +MSAT is free software, using the Apache license, see file LICENSE +Copyright 2014 Guillaume Bury +Copyright 2014 Simon Cruanes +*) type dummy = Dummy and an_option = AnOptionAttribute of Smtlib_util.pd * attribute diff --git a/util/smtlib/smtlib_util.mli b/util/smtlib/smtlib_util.mli index 8afbce37..24ff66b8 100644 --- a/util/smtlib/smtlib_util.mli +++ b/util/smtlib/smtlib_util.mli @@ -1,3 +1,9 @@ +(* +MSAT is free software, using the Apache license, see file LICENSE +Copyright 2014 Guillaume Bury +Copyright 2014 Simon Cruanes +*) + type extradata = unit val initial_data : unit -> unit val file : string ref