From 62835b35d0e8a0d56207966018952ab283ee15a9 Mon Sep 17 00:00:00 2001 From: Guillaume Bury Date: Thu, 6 Nov 2014 18:56:39 +0100 Subject: [PATCH] Indentation + some debug output in res.ml --- sat/res.ml | 440 ++++++++++++++++++++++---------------------- sat/res_intf.ml | 4 +- sat/sat.ml | 6 +- sat/solver.mli | 4 +- sat/solver_types.ml | 6 +- util/parser.ml | 12 +- util/sat_solve.ml | 22 +-- util/sparse_vec.ml | 8 +- util/vec.ml | 18 +- 9 files changed, 263 insertions(+), 257 deletions(-) diff --git a/sat/res.ml b/sat/res.ml index 5712d6e9..5cd34a5f 100644 --- a/sat/res.ml +++ b/sat/res.ml @@ -8,255 +8,261 @@ module type S = Res_intf.S module Make(St : Solver_types.S)(Proof : sig type proof end) = struct - (* Type definitions *) - type lemma = Proof.proof - type clause = St.clause - type atom = St.atom - type int_cl = clause * St.atom list + (* Type definitions *) + type lemma = Proof.proof + type clause = St.clause + type atom = St.atom + type int_cl = clause * St.atom list - type node = - | Assumption - | Lemma of lemma - | Resolution of atom * int_cl * int_cl - (* lits, c1, c2 with lits the literals used to resolve c1 and c2 *) + type node = + | Assumption + | Lemma of lemma + | Resolution of atom * int_cl * int_cl + (* lits, c1, c2 with lits the literals used to resolve c1 and c2 *) - exception Resolution_error of string + exception Resolution_error of string - (* Proof graph *) - let hash_cl cl = - Hashtbl.hash (List.map (fun a -> St.(a.aid)) cl) + (* Proof graph *) + let hash_cl cl = + Hashtbl.hash (List.map (fun a -> St.(a.aid)) cl) - let equal_cl cl_c cl_d = - try - List.for_all2 (==) cl_c cl_d - with Invalid_argument _ -> - false + let equal_cl cl_c cl_d = + try + List.for_all2 (==) cl_c cl_d + with Invalid_argument _ -> + false - module H = Hashtbl.Make(struct - type t = St.atom list - let hash = hash_cl - let equal = equal_cl + module H = Hashtbl.Make(struct + type t = St.atom list + let hash = hash_cl + let equal = equal_cl end) - let proof : node H.t = H.create 1007;; + let proof : node H.t = H.create 1007;; - (* Misc functions *) - let equal_atoms a b = St.(a.aid) = St.(b.aid) - let compare_atoms a b = Pervasives.compare St.(a.aid) St.(b.aid) + (* Misc functions *) + let equal_atoms a b = St.(a.aid) = St.(b.aid) + let compare_atoms a b = Pervasives.compare St.(a.aid) St.(b.aid) - (* Compute resolution of 2 clauses *) - let resolve l = - let rec aux resolved acc = function - | [] -> resolved, acc - | [a] -> resolved, a :: acc - | a :: b :: r -> - if equal_atoms a b then - aux resolved (a :: acc) r - else if equal_atoms St.(a.neg) b then - aux (St.(a.var.pa) :: resolved) acc r - else - aux resolved (a :: acc) (b :: r) - in - let resolved, new_clause = aux [] [] l in - resolved, List.rev new_clause + (* 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 to_list c = - let v = St.(c.atoms) in - let l = ref [] in - for i = 0 to Vec.size v - 1 do - l := (Vec.get v i) :: !l - done; - let l, res = resolve (List.sort_uniq compare_atoms !l) in - if l <> [] then - raise (Resolution_error "Input cause is a tautology"); - res + 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 - (* Adding new proven clauses *) - let is_proved c = H.mem proof c - let is_proven c = is_proved (to_list c) + (* Compute resolution of 2 clauses *) + let resolve l = + let rec aux resolved acc = function + | [] -> resolved, acc + | [a] -> resolved, a :: acc + | a :: b :: r -> + if equal_atoms a b then + aux resolved (a :: acc) r + else if equal_atoms St.(a.neg) b then + aux (St.(a.var.pa) :: resolved) acc r + else + aux resolved (a :: acc) (b :: r) + in + let resolved, new_clause = aux [] [] l in + resolved, List.rev new_clause - let add_res (c, cl_c) (d, cl_d) = - Log.debug 7 "Resolving clauses :"; - Log.debug 7 " %a" St.pp_clause c; - Log.debug 7 " %a" St.pp_clause d; - let l = List.merge compare_atoms cl_c cl_d in - let resolved, new_clause = resolve l in - match resolved with - | [] -> raise (Resolution_error "No literal to resolve over") - | [a] -> - H.add proof new_clause (Resolution (a, (c, cl_c), (d, cl_d))); - let new_c = St.make_clause (St.fresh_name ()) new_clause (List.length new_clause) true [c; d] in - Log.debug 5 "New clause : %a" St.pp_clause new_c; - new_c, new_clause - | _ -> raise (Resolution_error "Resolved to a tautology") + let to_list c = + let v = St.(c.atoms) in + let l = ref [] in + for i = 0 to Vec.size v - 1 do + l := (Vec.get v i) :: !l + done; + let l, res = resolve (List.sort_uniq compare_atoms !l) in + if l <> [] then + raise (Resolution_error "Input cause is a tautology"); + res - let add_clause cl l = (* We assume that all clauses in c.cpremise are already proved ! *) - match l with - | a :: ((_ :: _) as r) -> - let new_c, new_cl = List.fold_left add_res a r in - assert (equal_cl cl new_cl) - | _ -> assert false + (* Adding new proven clauses *) + let is_proved c = H.mem proof c + let is_proven c = is_proved (to_list c) - let need_clause (c, cl) = - if is_proved cl then - [] - else if not St.(c.learnt) then begin - Log.debug 8 "Adding to hyps : %a" St.pp_clause c; - H.add proof cl Assumption; - [] + let add_res (c, cl_c) (d, cl_d) = + Log.debug 7 "Resolving clauses :"; + Log.debug 7 " %a" St.pp_clause c; + Log.debug 7 " %a" St.pp_clause d; + let l = List.merge compare_atoms cl_c cl_d in + let resolved, new_clause = resolve l in + match resolved with + | [] -> raise (Resolution_error "No literal to resolve over") + | [a] -> + H.add proof new_clause (Resolution (a, (c, cl_c), (d, cl_d))); + let new_c = St.make_clause (St.fresh_name ()) new_clause (List.length new_clause) true [c; d] in + Log.debug 5 "New clause : %a" St.pp_clause new_c; + new_c, new_clause + | _ -> raise (Resolution_error "Resolved to a tautology") + + let add_clause cl l = (* We assume that all clauses in c.cpremise are already proved ! *) + match l with + | a :: ((_ :: _) as r) -> + let new_c, new_cl = List.fold_left add_res a r in + if not (equal_cl cl new_cl) then begin + Log.debug 0 "Expected the following clauses to be equal :"; + Log.debug 0 "expected : %s" (Log.on_fmt print_cl cl); + Log.debug 0 "found : %a" St.pp_clause new_c; + assert false + end + | _ -> assert false + + let need_clause (c, cl) = + if is_proved cl then + [] + else if not St.(c.learnt) then begin + Log.debug 8 "Adding to hyps : %a" St.pp_clause c; + H.add proof cl Assumption; + [] + end else + St.(c.cpremise) + + let rec do_clause = function + | [] -> () + | c :: r -> + let cl = to_list c in + let l = need_clause (c, cl) in + if l = [] then (* c is either an asusmption, or already proved *) + do_clause r + else + let l' = List.rev_map (fun c -> c, to_list c) l in + let to_prove = List.filter (fun (_, cl) -> not (is_proved cl)) l' in + let to_prove = List.rev_map fst to_prove in + if to_prove = [] then begin + (* See wether we can prove c right now *) + add_clause cl l'; + do_clause r end else - St.(c.cpremise) + (* Or if we have to prove some other clauses first *) + do_clause (to_prove @ (c :: r)) - let rec do_clause = function - | [] -> () - | c :: r -> - let cl = to_list c in - let l = need_clause (c, cl) in - if l = [] then (* c is either an asusmption, or already proved *) - do_clause r - else - let l' = List.rev_map (fun c -> c, to_list c) l in - let to_prove = List.filter (fun (_, cl) -> not (is_proved cl)) l' in - let to_prove = List.rev_map fst to_prove in - if to_prove = [] then begin - (* See wether we can prove c right now *) - add_clause cl l'; - do_clause r - end else - (* Or if we have to prove some other clauses first *) - do_clause (to_prove @ (c :: r)) + let prove c = + Log.debug 3 "Proving : %a" St.pp_clause c; + do_clause [c]; + Log.debug 3 "Proved : %a" St.pp_clause c - let prove c = - Log.debug 3 "Proving : %a" St.pp_clause c; - do_clause [c]; - Log.debug 3 "Proved : %a" St.pp_clause c - - let clause_unit a = St.( - let l = if a.is_true then [a] else [a.neg] in - make_clause (fresh_name ()) l 1 true a.var.vpremise + let clause_unit a = St.( + let l = if a.is_true then [a] else [a.neg] in + make_clause (fresh_name ()) l 1 true a.var.vpremise ) - let rec prove_unsat_cl (c, cl) = match cl with - | [] -> true - | a :: r -> - try - Log.debug 2 "Eliminating %a in %a" St.pp_atom a St.pp_clause c; - let d = match St.(a.var.level, a.var.reason) with - | 0, Some d -> d - | 0, None -> clause_unit a - | _ -> raise Exit - in - prove d; - let cl_d = to_list d in - prove_unsat_cl (add_res (c, cl) (d, cl_d)) - with Exit -> false - - exception Cannot - let assert_can_prove_unsat c = - Log.debug 1 "=================== Proof ====================="; - prove c; - if not (prove_unsat_cl (c, to_list c)) then raise Cannot - - (* Interface exposed *) - type proof_node = { - conclusion : clause; - step : step; - } - and proof = unit -> proof_node - and step = - | Hypothesis - | Lemma of lemma - | Resolution of proof * proof * atom - - let rec return_proof (c, cl) () = - Log.debug 8 "Returning proof for : %a" St.pp_clause c; - let st = match H.find proof cl with - | Assumption -> Hypothesis - | Lemma l -> Lemma l - | Resolution (a, cl_c, cl_d) -> - Resolution (return_proof cl_c, return_proof cl_d, a) + let rec prove_unsat_cl (c, cl) = match cl with + | [] -> true + | a :: r -> + try + Log.debug 2 "Eliminating %a in %a" St.pp_atom a St.pp_clause c; + let d = match St.(a.var.level, a.var.reason) with + | 0, Some d -> d + | 0, None -> clause_unit a + | _ -> raise Exit in - { conclusion = c; step = st } + prove d; + let cl_d = to_list d in + prove_unsat_cl (add_res (c, cl) (d, cl_d)) + with Exit -> false - let prove_unsat c = - assert_can_prove_unsat c; - return_proof (St.empty_clause, []) + exception Cannot + let assert_can_prove_unsat c = + Log.debug 1 "=================== Proof ====================="; + prove c; + if not (prove_unsat_cl (c, to_list c)) then raise Cannot - (* Print proof graph *) - let _i = ref 0 - let new_id () = incr _i; "id_" ^ (string_of_int !_i) + (* Interface exposed *) + type proof_node = { + conclusion : clause; + step : step; + } + and proof = unit -> proof_node + and step = + | Hypothesis + | Lemma of lemma + | Resolution of proof * proof * atom - let ids : (clause, (bool * string)) Hashtbl.t = Hashtbl.create 1007;; - let c_id c = - try - snd (Hashtbl.find ids c) - with Not_found -> - let id = new_id () in - Hashtbl.add ids c (false, id); - id + let rec return_proof (c, cl) () = + Log.debug 8 "Returning proof for : %a" St.pp_clause c; + let st = match H.find proof cl with + | Assumption -> Hypothesis + | Lemma l -> Lemma l + | Resolution (a, cl_c, cl_d) -> + Resolution (return_proof cl_c, return_proof cl_d, a) + in + { conclusion = c; step = st } - let clear_ids () = - Hashtbl.iter (fun c (_, id) -> Hashtbl.replace ids c (false, id)) ids + let prove_unsat c = + assert_can_prove_unsat c; + return_proof (St.empty_clause, []) - let is_drawn c = - try - fst (Hashtbl.find ids c) - with Not_found -> - false + (* Print proof graph *) + let _i = ref 0 + let new_id () = incr _i; "id_" ^ (string_of_int !_i) - let has_drawn c = - assert (Hashtbl.mem ids c); - let b, id = Hashtbl.find ids c in - assert (not b); - Hashtbl.replace ids c (true, id) + let ids : (clause, (bool * string)) Hashtbl.t = Hashtbl.create 1007;; + let c_id c = + try + snd (Hashtbl.find ids c) + with Not_found -> + let id = new_id () in + Hashtbl.add ids c (false, id); + id - let print_atom fmt a = - Format.fprintf fmt "%s%d" St.(if a.var.pa == a then "" else "-") St.(a.var.vid + 1) + let clear_ids () = + Hashtbl.iter (fun c (_, id) -> Hashtbl.replace ids c (false, id)) ids - 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 + let is_drawn c = + try + fst (Hashtbl.find ids c) + with Not_found -> + false - let print_clause fmt c = print_cl fmt (to_list c) + let has_drawn c = + assert (Hashtbl.mem ids c); + let b, id = Hashtbl.find ids c in + assert (not b); + Hashtbl.replace ids c (true, id) - let print_dot_rule f arg fmt cl = - Format.fprintf fmt "%s [shape=plaintext, label=<%a
>];@\n" - (c_id cl) "BORDER=\"0\" CELLBORDER=\"1\" CELLSPACING=\"0\"" f arg + let print_clause fmt c = print_cl fmt (to_list c) - let print_dot_edge c fmt d = - Format.fprintf fmt "%s -> %s;@\n" (c_id c) (c_id d) + let print_dot_rule f arg fmt cl = + Format.fprintf fmt "%s [shape=plaintext, label=<%a
>];@\n" + (c_id cl) "BORDER=\"0\" CELLBORDER=\"1\" CELLSPACING=\"0\"" f arg - let rec print_dot_proof fmt p = - match p.step with - | Hypothesis -> - let aux fmt () = - Format.fprintf fmt "%a" - print_clause p.conclusion - in - print_dot_rule aux () fmt p.conclusion - | Lemma _ -> - let aux fmt () = - Format.fprintf fmt "%ato prove ..." - print_clause p.conclusion - in - print_dot_rule aux () fmt p.conclusion - | Resolution (proof1, proof2, a) -> - let aux fmt () = - Format.fprintf fmt "%a%a" - print_clause p.conclusion print_atom a - in - let p1 = proof1 () in - let p2 = proof2 () in - Format.fprintf fmt "%a%a%a%a%a" - (print_dot_rule aux ()) p.conclusion - (print_dot_edge p.conclusion) p1.conclusion - (print_dot_edge p.conclusion) p2.conclusion - print_dot_proof p1 - print_dot_proof p2 + let print_dot_edge c fmt d = + Format.fprintf fmt "%s -> %s;@\n" (c_id c) (c_id d) - let print_dot fmt proof = - clear_ids (); - Format.fprintf fmt "digraph proof {@\n%a@\n}@." print_dot_proof (proof ()) + let rec print_dot_proof fmt p = + match p.step with + | Hypothesis -> + let aux fmt () = + Format.fprintf fmt "%a" + print_clause p.conclusion + in + print_dot_rule aux () fmt p.conclusion + | Lemma _ -> + let aux fmt () = + Format.fprintf fmt "%ato prove ..." + print_clause p.conclusion + in + print_dot_rule aux () fmt p.conclusion + | Resolution (proof1, proof2, a) -> + let aux fmt () = + Format.fprintf fmt "%a%a" + print_clause p.conclusion print_atom a + in + let p1 = proof1 () in + let p2 = proof2 () in + Format.fprintf fmt "%a%a%a%a%a" + (print_dot_rule aux ()) p.conclusion + (print_dot_edge p.conclusion) p1.conclusion + (print_dot_edge p.conclusion) p2.conclusion + print_dot_proof p1 + print_dot_proof p2 + + let print_dot fmt proof = + clear_ids (); + Format.fprintf fmt "digraph proof {@\n%a@\n}@." print_dot_proof (proof ()) end diff --git a/sat/res_intf.ml b/sat/res_intf.ml index 4f245ee9..31085929 100644 --- a/sat/res_intf.ml +++ b/sat/res_intf.ml @@ -15,8 +15,8 @@ module type S = sig @raise Cannot if it is impossible. *) type proof_node = { - conclusion : clause; - step : step; + conclusion : clause; + step : step; } and proof = unit -> proof_node and step = diff --git a/sat/sat.ml b/sat/sat.ml index ec73246d..707ce520 100644 --- a/sat/sat.ml +++ b/sat/sat.ml @@ -120,9 +120,9 @@ module Make(Dummy : sig end) = struct let eval = SatSolver.eval let get_proof () = - match SatSolver.unsat_conflict () with - | None -> assert false - | Some c -> SatSolver.Proof.prove_unsat c + match SatSolver.unsat_conflict () with + | None -> assert false + | Some c -> SatSolver.Proof.prove_unsat c let print_proof = SatSolver.Proof.print_dot diff --git a/sat/solver.mli b/sat/solver.mli index ea651928..f49d201f 100644 --- a/sat/solver.mli +++ b/sat/solver.mli @@ -23,8 +23,8 @@ sig module Proof : Res.S with type atom = St.atom and - type clause = St.clause and - type lemma = Th.proof + type clause = St.clause and + type lemma = Th.proof val solve : unit -> unit (** Try and solves the current set of assumptions. diff --git a/sat/solver_types.ml b/sat/solver_types.ml index 0a8c5412..103a2f24 100644 --- a/sat/solver_types.ml +++ b/sat/solver_types.ml @@ -123,9 +123,9 @@ module Make (F : Formula_intf.S) = struct var, negated let made_vars_info vars = - Vec.grow_to_by_double vars !cpt_mk_var; - MA.iter (fun _ var -> Vec.set_unsafe vars var.vid var) !ma; - !cpt_mk_var + Vec.grow_to_by_double vars !cpt_mk_var; + MA.iter (fun _ var -> Vec.set_unsafe vars var.vid var) !ma; + !cpt_mk_var let add_atom lit = let var, negated = make_var lit in diff --git a/util/parser.ml b/util/parser.ml index 0098703e..cde0f4cf 100644 --- a/util/parser.ml +++ b/util/parser.ml @@ -15,12 +15,12 @@ type line = let rec _read_word s acc i len = assert (len>0); if i+len=String.length s - then String.sub s i len :: acc - else match s.[i+len] with - | ' ' | '\t' -> - let acc = String.sub s i len :: acc in - _skip_space s acc (i+len+1) - | _ -> _read_word s acc i (len+1) + then String.sub s i len :: acc + else match s.[i+len] with + | ' ' | '\t' -> + let acc = String.sub s i len :: acc in + _skip_space s acc (i+len+1) + | _ -> _read_word s acc i (len+1) and _skip_space s acc i = if i=String.length s then acc diff --git a/util/sat_solve.ml b/util/sat_solve.ml index 1d9af7b4..9f7fee14 100644 --- a/util/sat_solve.ml +++ b/util/sat_solve.ml @@ -35,26 +35,26 @@ let int_arg r arg = let setup_gc_stat () = at_exit (fun () -> - Gc.print_stat stdout; - ) + 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"; + " Enable stack traces"; "-gc", Arg.Unit setup_gc_stat, - " Outputs statistics about the GC"; + " Outputs statistics about the GC"; "-model", Arg.Set p_assign, - " Outputs the boolean model found if sat"; + " Outputs the boolean model found if sat"; "-p", Arg.Set p_proof, - " Outputs the proof found (in dot format) if unsat"; + " Outputs the proof found (in dot format) if unsat"; "-s", Arg.String (int_arg size_limit), - "[kMGT] Sets the size limit for the sat solver"; + "[kMGT] Sets the size limit for the sat solver"; "-t", Arg.String (int_arg time_limit), - "[smhd] Sets the time limit for the sat solver"; + "[smhd] Sets the time limit for the sat solver"; "-v", Arg.Int (fun i -> Log.set_debug i), - " Sets the debug verbose level"; + " Sets the debug verbose level"; ] (* Limits alarm *) @@ -109,8 +109,8 @@ let main () = | S.Unsat -> Format.printf "Unsat@."; if !p_proof then begin - let p = S.get_proof () in - S.print_proof Format.std_formatter p + let p = S.get_proof () in + S.print_proof Format.std_formatter p end let () = diff --git a/util/sparse_vec.ml b/util/sparse_vec.ml index 35f20fca..d6054011 100644 --- a/util/sparse_vec.ml +++ b/util/sparse_vec.ml @@ -8,7 +8,7 @@ Copyright 2014 Simon Cruanes (** {1 Sparse vector, filled with default value} *) let _size_too_big()= - failwith "Sparse_vec: capacity exceeds maximum array size" + failwith "Sparse_vec: capacity exceeds maximum array size" type 'a t = { default : 'a; mutable data : 'a array; mutable sz : int } @@ -17,8 +17,8 @@ let make sz default = { default; sz; data=Array.make sz default; } let init sz f default = - if sz > Sys.max_array_length then _size_too_big(); - {data = Array.init sz (fun i -> f i); sz ; default} + if sz > Sys.max_array_length then _size_too_big(); + {data = Array.init sz (fun i -> f i); sz ; default} let length {sz} = sz @@ -37,7 +37,7 @@ let rec grow_to_by_double t new_capa = let data = t.data in let capa = ref (Array.length data + 1) in while !capa < new_capa do - capa := min (2 * !capa) Sys.max_array_length; + capa := min (2 * !capa) Sys.max_array_length; done; grow_to t !capa diff --git a/util/vec.ml b/util/vec.ml index 7930216e..29aa6e1d 100644 --- a/util/vec.ml +++ b/util/vec.ml @@ -14,17 +14,17 @@ type 'a t = { mutable dummy: 'a; mutable data : 'a array; mutable sz : int } let _size_too_big()= - failwith "Vec: capacity exceeds maximum array size" + failwith "Vec: capacity exceeds maximum array size" let make capa d = - if capa > Sys.max_array_length then _size_too_big(); - {data = Array.make capa d; sz = 0; dummy = d} + if capa > Sys.max_array_length then _size_too_big(); + {data = Array.make capa d; sz = 0; dummy = d} let make_empty d = {data = [||]; sz=0; dummy=d } let init capa f d = - if capa > Sys.max_array_length then _size_too_big(); - {data = Array.init capa (fun i -> f i); sz = capa; dummy = d} + if capa > Sys.max_array_length then _size_too_big(); + {data = Array.init capa (fun i -> f i); sz = capa; dummy = d} let from_array data sz d = assert (sz <= Array.length data); @@ -53,16 +53,16 @@ let grow_to t new_capa = t.data <- Array.init new_capa (fun i -> if i < capa then data.(i) else t.dummy) let grow_to_double_size t = - if Array.length t.data = Sys.max_array_length then _size_too_big(); - let size = min Sys.max_array_length (2* Array.length t.data) in - grow_to t size + if Array.length t.data = Sys.max_array_length then _size_too_big(); + let size = min Sys.max_array_length (2* Array.length t.data) in + grow_to t size let rec grow_to_by_double t new_capa = if new_capa > Sys.max_array_length then _size_too_big (); let data = t.data in let capa = ref (Array.length data + 1) in while !capa < new_capa do - capa := min (2 * !capa) Sys.max_array_length; + capa := min (2 * !capa) Sys.max_array_length; done; grow_to t !capa