From e92740e75e2aab690f9e7c84075630c8ea4e41d5 Mon Sep 17 00:00:00 2001 From: Guillaume Bury Date: Sat, 15 Nov 2014 00:59:09 +0100 Subject: [PATCH] Better integration of smt into sat-solve (sic) --- sat/res.ml | 9 +- smt/smt.ml | 36 ++---- smt/smt.mli | 18 +-- tests/{smt => sat}/test-007.smt2 | 0 tests/{smt => unsat}/test-008.smt2 | 0 util/sat_solve.ml | 18 ++- util/smt_solve.ml | 198 ----------------------------- util/smtlib/satlib.ml | 103 --------------- util/smtlib/satlib.mli | 3 - util/smtlib/smtlib.ml | 4 +- 10 files changed, 32 insertions(+), 357 deletions(-) rename tests/{smt => sat}/test-007.smt2 (100%) rename tests/{smt => unsat}/test-008.smt2 (100%) delete mode 100644 util/smt_solve.ml delete mode 100644 util/smtlib/satlib.ml delete mode 100644 util/smtlib/satlib.mli diff --git a/sat/res.ml b/sat/res.ml index 19e13e65..c74efb88 100644 --- a/sat/res.ml +++ b/sat/res.ml @@ -49,13 +49,10 @@ module Make(St : Solver_types.S) = struct let fresh_pcl_name () = incr _c; "P" ^ (string_of_int !_c) (* Printing functions *) - let print_atom fmt a = - Format.fprintf fmt "%s%d" St.(if a.var.pa == a then "" else "¬ ") St.(a.var.vid + 1) - let rec print_cl fmt = function | [] -> Format.fprintf fmt "[]" - | [a] -> print_atom fmt a - | a :: ((_ :: _) as r) -> Format.fprintf fmt "%a ∨ %a" print_atom a print_cl r + | [a] -> St.print_atom fmt a + | a :: ((_ :: _) as r) -> Format.fprintf fmt "%a ∨ %a" St.print_atom a print_cl r (* Compute resolution of 2 clauses *) let resolve l = @@ -322,7 +319,7 @@ module Make(St : Solver_types.S) = struct Format.fprintf fmt "%s -> %s;@\n" id_c id_d let print_res_atom id fmt a = - Format.fprintf fmt "%s [label=\"%a\"]" id print_atom a + Format.fprintf fmt "%s [label=\"%a\"]" id St.print_atom a let print_res_node concl p1 p2 fmt atom = let id = new_id () in diff --git a/smt/smt.ml b/smt/smt.ml index 1d0317ee..8a886c83 100644 --- a/smt/smt.ml +++ b/smt/smt.ml @@ -10,33 +10,35 @@ module Fsmt = struct type var = string type t = - | Fresh of int + | Prop of int | Equal of var * var | Distinct of var * var - let dummy = Fresh 0 + let dummy = Prop 0 let max_fresh = ref 0 let fresh () = incr max_fresh; - Fresh !max_fresh + Prop (2 * !max_fresh + 1) + + let mk_prop i = + if i <> 0 && i < max_int / 2 then Prop (2 * i) + else raise Invalid_var let mk_var i = - if i <> "" then - i - else - raise Invalid_var + if i <> "" then i + else raise Invalid_var let mk_eq i j = Equal (mk_var i, mk_var j) let mk_neq i j = Distinct (mk_var i, mk_var j) let neg = function - | Fresh i -> Fresh (-i) + | Prop i -> Prop (-i) | Equal (a, b) -> Distinct (a, b) | Distinct (a, b) -> Equal (a, b) let norm = function - | Fresh i -> Fresh (abs i), i < 0 + | Prop i -> Prop (abs i), i < 0 | Equal (a, b) -> Equal (min a b, max a b), false | Distinct (a, b) -> Equal (min a b, max a b), true @@ -50,9 +52,9 @@ module Fsmt = struct let add_label _ _ = () let print fmt = function - | Fresh i -> Format.fprintf fmt "%sv%d" (if i < 0 then "¬ " else "") (abs i) + | Prop i -> Format.fprintf fmt "%s%s%d" (if i < 0 then "¬ " else "") (if i mod 2 = 0 then "v" else "f") (abs i) | Equal (a, b) -> Format.fprintf fmt "%s = %s" a b - | Distinct (a, b) -> Format.fprintf fmt "%s <> %s" a b + | Distinct (a, b) -> Format.fprintf fmt "%s ≠ %s" a b end @@ -89,7 +91,7 @@ module Tsmt = struct try for i = s.start to s.start + s.length - 1 do match s.get i with - | Fsmt.Fresh _ -> () + | Fsmt.Prop _ -> () | Fsmt.Equal (i, j) as f -> env := { !env with seen = f :: !env.seen }; env := { !env with uf = U.union !env.uf i j } @@ -118,16 +120,6 @@ module Make(Dummy:sig end) = struct | Unsat let _i = ref 0 - - let make_eq = Fsmt.mk_eq - let make_neq = Fsmt.mk_neq - - let neg = Fsmt.neg - - let hash = Fsmt.hash - let equal = Fsmt.equal - let compare = Fsmt.compare - let solve () = try SmtSolver.solve (); diff --git a/smt/smt.mli b/smt/smt.mli index 4ecc42e6..be63f304 100644 --- a/smt/smt.mli +++ b/smt/smt.mli @@ -6,6 +6,7 @@ Copyright 2014 Simon Cruanes module Fsmt : sig include Formula_intf.S + val mk_prop : int -> t val mk_eq : string -> string -> t val mk_neq : string -> string -> t end @@ -27,23 +28,6 @@ module Make(Dummy: sig end) : sig type res = Sat | Unsat (** Type of results returned by the solve function. *) - val make_eq : string -> string -> atom - (** Returns the literal corresponding to equality of the given variables - @raise Invalid_var if given [0] as argument.*) - - val make_neq : string -> string -> atom - (** Returns the literal corresponding to disequality of the given variables - @raise Invalid_var if given [0] as argument.*) - - val neg : atom -> atom - (** [neg a] returns the negation of a literal. Involutive, i.e [neg (neg a) = a]. *) - - val hash : atom -> int - val equal : atom -> atom -> bool - val compare : atom -> atom -> int - (** Usual hash and comparison functions. For now, directly uses - [Pervasives] and [Hashtbl] builtins. *) - val solve : unit -> res (** Returns the satisfiability status of the current set of assumptions. *) diff --git a/tests/smt/test-007.smt2 b/tests/sat/test-007.smt2 similarity index 100% rename from tests/smt/test-007.smt2 rename to tests/sat/test-007.smt2 diff --git a/tests/smt/test-008.smt2 b/tests/unsat/test-008.smt2 similarity index 100% rename from tests/smt/test-008.smt2 rename to tests/unsat/test-008.smt2 diff --git a/util/sat_solve.ml b/util/sat_solve.ml index 5e098748..f0e72dfe 100644 --- a/util/sat_solve.ml +++ b/util/sat_solve.ml @@ -1,5 +1,7 @@ -module S = Sat.Make(struct end) +module F = Smt.Fsmt +module T = Smt.Tseitin +module S = Smt.Make(struct end) exception Out_of_time exception Out_of_space @@ -60,8 +62,8 @@ let format_of_filename s = let parse_with_input file = function | Auto -> assert false - | Dimacs -> List.rev_map (List.rev_map S.make) (Parsedimacs.parse file) - | Smtlib -> rev_flat_map Sat.Tseitin.make_cnf [] (Satlib.parse file) + | Dimacs -> List.rev_map (List.rev_map F.mk_prop) (Parsedimacs.parse file) + | Smtlib -> rev_flat_map T.make_cnf [] (Smtlib.parse file) let parse_input file = parse_with_input file (match !input with @@ -79,15 +81,17 @@ let print_proof proof = match !output with | Standard -> () | Dot -> S.print_proof std proof +(* let print_assign () = match !output with | Standard -> S.iter_atoms (fun a -> Format.fprintf std "%a -> %s,@ " S.print_atom a (if S.eval a then "T" else "F")) | Dot -> () +*) let rec print_cl fmt = function | [] -> Format.fprintf fmt "[]" - | [a] -> Sat.Fsat.print fmt a - | a :: ((_ :: _) as r) -> Format.fprintf fmt "%a ∨ %a" Sat.Fsat.print a print_cl r + | [a] -> F.print fmt a + | a :: ((_ :: _) as r) -> Format.fprintf fmt "%a ∨ %a" F.print a print_cl r let print_lcl l = List.iter (fun c -> Format.fprintf std "%a@\n" print_cl c) l @@ -189,9 +193,11 @@ let main () = S.assume cnf; match S.solve () with | S.Sat -> - print "Sat"; + print "Sat" + (* if !p_assign then print_assign () + *) | S.Unsat -> print "Unsat"; if !p_proof_check then begin diff --git a/util/smt_solve.ml b/util/smt_solve.ml deleted file mode 100644 index 66315f9d..00000000 --- a/util/smt_solve.ml +++ /dev/null @@ -1,198 +0,0 @@ - -module S = Smt.Make(struct end) - -exception Out_of_time -exception Out_of_space - -(* IO wrappers *) -(* Types for input/output languages *) -type sat_input = - | Auto - | Smtlib - -type sat_output = - | Standard (* Only output problem status *) - | Dot - -let input = ref Auto -let output = ref Standard - -let input_list = [ - "auto", Auto; - "smtlib", Smtlib; -] -let output_list = [ - "dot", Dot; -] - -let error_msg opt arg l = - Format.fprintf Format.str_formatter "'%s' is not a valid argument for '%s', valid arguments are : %a" - arg opt (fun fmt -> List.iter (fun (s, _) -> Format.fprintf fmt "%s, " s)) l; - Format.flush_str_formatter () - -let set_io opt arg flag l = - try - flag := List.assoc arg l - with Not_found -> - invalid_arg (error_msg opt arg l) - -let set_input s = set_io "Input" s input input_list -let set_output s = set_io "Output" s output output_list - -(* Input Parsing *) -let rec rev_flat_map f acc = function - | [] -> acc - | a :: r -> rev_flat_map f (List.rev_append (f a) acc) r - -let format_of_filename s = - let last n = - try String.sub s (String.length s - n) n - with Invalid_argument _ -> "" - in - if last 5 = ".smt2" then - Smtlib - else (* Default choice *) - Smtlib - -let parse_with_input file = function - | Auto -> assert false - | Smtlib -> rev_flat_map Smt.Tseitin.make_cnf [] (Smtlib.parse file) - -let parse_input file = - parse_with_input file (match !input with - | Auto -> format_of_filename file - | f -> f) - -(* Printing wrappers *) -let std = Format.std_formatter - -let print format = match !output with - | Standard -> Format.fprintf std "%( fmt %)@." format - | Dot -> Format.fprintf std "/* %( fmt %) */@." format - -let print_proof proof = match !output with - | Standard -> () - | Dot -> S.print_proof std proof - -let rec print_cl fmt = function - | [] -> Format.fprintf fmt "[]" - | [a] -> Smt.Fsmt.print fmt a - | a :: ((_ :: _) as r) -> Format.fprintf fmt "%a ∨ %a" Smt.Fsmt.print a print_cl r - -let print_lcl l = - List.iter (fun c -> Format.fprintf std "%a@\n" print_cl c) l - -let print_lclause l = - List.iter (fun c -> Format.fprintf std "%a@\n" S.print_clause c) l - -(* Arguments parsing *) -let file = ref "" -let p_cnf = ref false -let p_proof_check = ref false -let p_proof_print = ref false -let p_unsat_core = ref false -let time_limit = ref 300. -let size_limit = ref 1000_000_000. - -let int_arg r arg = - let l = String.length arg in - let multiplier m = - let arg1 = String.sub arg 0 (l-1) in - r := m *. (float_of_string arg1) - in - if l = 0 then raise (Arg.Bad "bad numeric argument") - else - try - match arg.[l-1] with - | 'k' -> multiplier 1e3 - | 'M' -> multiplier 1e6 - | 'G' -> multiplier 1e9 - | 'T' -> multiplier 1e12 - | 's' -> multiplier 1. - | 'm' -> multiplier 60. - | 'h' -> multiplier 3600. - | 'd' -> multiplier 86400. - | '0'..'9' -> r := float_of_string arg - | _ -> raise (Arg.Bad "bad numeric argument") - with Failure "float_of_string" -> raise (Arg.Bad "bad numeric argument") - -let setup_gc_stat () = - at_exit (fun () -> - Gc.print_stat stdout; - ) - -let input_file = fun s -> file := s - -let usage = "Usage : main [options] " -let argspec = Arg.align [ - "-bt", Arg.Unit (fun () -> Printexc.record_backtrace true), - " Enable stack traces"; - "-cnf", Arg.Set p_cnf, - " Prints the cnf used."; - "-check", Arg.Set p_proof_check, - " Build, check and print the proof (if output is set), if unsat"; - "-gc", Arg.Unit setup_gc_stat, - " Outputs statistics about the GC"; - "-i", Arg.String set_input, - " Sets the input format (default auto)"; - "-o", Arg.String set_output, - " Sets the output format (default none)"; - "-size", Arg.String (int_arg size_limit), - "[kMGT] Sets the size limit for the sat solver"; - "-time", Arg.String (int_arg time_limit), - "[smhd] Sets the time limit for the sat solver"; - "-u", Arg.Set p_unsat_core, - " Prints the unsat-core explanation of the unsat proof (if used with -check)"; - "-v", Arg.Int (fun i -> Log.set_debug i), - " Sets the debug verbose level"; - ] - -(* Limits alarm *) -let check () = - let t = Sys.time () in - let heap_size = (Gc.quick_stat ()).Gc.heap_words in - let s = float heap_size *. float Sys.word_size /. 8. in - if t > !time_limit then - raise Out_of_time - else if s > !size_limit then - raise Out_of_space - -(* Entry file parsing *) -let get_cnf () = parse_input !file - -let main () = - (* Administrative duties *) - Arg.parse argspec input_file usage; - if !file = "" then begin - Arg.usage argspec usage; - exit 2 - end; - ignore(Gc.create_alarm check); - - (* Interesting stuff happening *) - let cnf = get_cnf () in - if !p_cnf then - print_lcl cnf; - S.assume cnf; - match S.solve () with - | S.Sat -> - print "Sat"; - | S.Unsat -> - print "Unsat"; - if !p_proof_check then begin - let p = S.get_proof () in - print_proof p; - if !p_unsat_core then - print_lclause (S.unsat_core p) - end - -let () = - try - main () - with - | Out_of_time -> - print "Time limit exceeded"; - exit 2 - | Out_of_space -> - print "Size limit exceeded"; - exit 3 diff --git a/util/smtlib/satlib.ml b/util/smtlib/satlib.ml deleted file mode 100644 index 56f1196e..00000000 --- a/util/smtlib/satlib.ml +++ /dev/null @@ -1,103 +0,0 @@ -(* Copyright 2014 INRIA **) - -open Smtlib_syntax - -module F = Sat.Fsat -module T = Sat.Tseitin - -exception Bad_arity of string -exception Unknown_command -exception Incomplete_translation - -(* Environment *) -let env : (string, T.t) Hashtbl.t = Hashtbl.create 57;; -Hashtbl.add env "true" T.f_true;; -Hashtbl.add env "false" T.f_false;; - -let get_var = - fun s -> - try - Hashtbl.find env s - with Not_found -> - let f = T.make_atom (F.fresh ()) in - Hashtbl.add env s f; - f - -(* Term translation *) -let translate_const = function - | SpecConstsDec(_, s) - | SpecConstNum(_, s) - | SpecConstString(_, s) - | SpecConstsHex(_, s) - | SpecConstsBinary(_, s) -> get_var s - -let translate_symbol = function - | Symbol(_, s) - | SymbolWithOr(_, s) -> s - -let translate_id = function - | IdSymbol(_, s) -> translate_symbol s - | IdUnderscoreSymNum(_, s, n) -> raise Incomplete_translation - -let translate_sort = function - | SortIdentifier(_, id) -> - let s = translate_id id in - if s <> "Bool" then raise Incomplete_translation - | _ -> raise Incomplete_translation - -let translate_qualid = function - | QualIdentifierId(_, id) -> translate_id id - | QualIdentifierAs(_, id, s) -> raise Incomplete_translation - -let left_assoc s f = function - | x :: r -> List.fold_left f x r - | _ -> raise (Bad_arity s) - -let right_assoc s f = function - | x :: r -> List.fold_right f r x - | _ -> raise (Bad_arity s) - -let rec translate_term = function - | TermSpecConst(_, const) -> translate_const const - | TermQualIdentifier(_, id) -> get_var (translate_qualid id) - | TermQualIdTerm(_, f, (_, l)) -> - begin match (translate_qualid f), (List.map translate_term l) with - (* CORE theory translation - '=', 'distinct','ite' not yet implemented *) - | "not", [e] -> T.make_not e - | "not", _ -> raise (Bad_arity "not") - | "and", l -> T.make_and l - | "or", l -> T.make_or l - | "xor" as s, l -> left_assoc s T.make_xor l - | "=>" as s, l -> right_assoc s T.make_imply l - | _ -> raise Unknown_command - end - | _ -> raise Incomplete_translation - -(* Command Translation *) -let translate_command = function - | CommandDeclareFun(_, s, (_, []), ret) -> - ignore (translate_sort ret); - ignore (get_var (translate_symbol s)); - None - | CommandAssert(_, t) -> - Some (translate_term t) - | _ -> None - -let rec translate_command_list acc = function - | [] -> acc - | c :: r -> - begin match translate_command c with - | None -> translate_command_list acc r - | Some t -> translate_command_list (t :: acc) r - end - -let translate = function - | Some Commands (_, (_, l)) -> List.rev (translate_command_list [] l) - | None -> [] - -let parse file = - let f = open_in file in - let lexbuf = Lexing.from_channel f in - let commands = Parsesmtlib.main Lexsmtlib.token lexbuf in - close_in f; - translate commands diff --git a/util/smtlib/satlib.mli b/util/smtlib/satlib.mli deleted file mode 100644 index 19ff02bc..00000000 --- a/util/smtlib/satlib.mli +++ /dev/null @@ -1,3 +0,0 @@ -(* Copyright 2014 INRIA *) - -val parse : string -> Sat.Tseitin.t list diff --git a/util/smtlib/smtlib.ml b/util/smtlib/smtlib.ml index f472908c..c018d01f 100644 --- a/util/smtlib/smtlib.ml +++ b/util/smtlib/smtlib.ml @@ -14,7 +14,7 @@ let env : (string, T.t) Hashtbl.t = Hashtbl.create 57;; Hashtbl.add env "true" T.f_true;; Hashtbl.add env "false" T.f_false;; -let get_var s = +let get_atom s = try Hashtbl.find env s with Not_found -> @@ -75,7 +75,7 @@ let rec translate_term = function | _ -> raise Unknown_command end end - | _ -> raise Incomplete_translation + | e -> (get_atom (translate_atom e)) (* Command Translation *) let translate_command = function