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

Fixed a bug in proof dot printer (+ indent)

Browse source
This commit is contained in:
Guillaume Bury 2014-11-07 17:46:32 +01:00
parent cac9df4510
commit d6cfd27f32
2 changed files with 22 additions and 23 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

19
sat/res.ml
View file

@ -208,8 +208,8 @@ module Make(St : Solver_types.S)(Proof : sig type proof end) = struct
let d = match St.(a.var.level, a.var.reason) with let d = match St.(a.var.level, a.var.reason) with
| 0, Some d -> d | 0, Some d -> d
| 0, None -> | 0, None ->
let d, cl_d = unit_hyp a in let d, cl_d = unit_hyp a in
if is_proved (d, cl_d) then d else raise Exit if is_proved (d, cl_d) then d else raise Exit
| _ -> raise Exit | _ -> raise Exit
in in
prove d; prove d;
@ -274,16 +274,15 @@ module Make(St : Solver_types.S)(Proof : sig type proof end) = struct
Hashtbl.iter (fun c (_, id) -> Hashtbl.replace ids c (false, id)) ids Hashtbl.iter (fun c (_, id) -> Hashtbl.replace ids c (false, id)) ids
let is_drawn c = let is_drawn c =
try ignore (c_id c);
fst (Hashtbl.find ids c) fst (Hashtbl.find ids c)
with Not_found ->
false
let has_drawn c = let has_drawn c =
assert (Hashtbl.mem ids c); if not (is_drawn c) then
let b, id = Hashtbl.find ids c in let b, id = Hashtbl.find ids c in
assert (not b); Hashtbl.replace ids c (true, id)
Hashtbl.replace ids c (true, id) else
()
let print_clause fmt c = print_cl fmt (to_list c) let print_clause fmt c = print_cl fmt (to_list c)

26
util/sat_solve.ml
View file

@ -7,32 +7,32 @@ exception Out_of_space
(* IO wrappers *) (* IO wrappers *)
(* Types for input/output languages *) (* Types for input/output languages *)
type sat_input = type sat_input =
| Dimacs | Dimacs
type sat_output = type sat_output =
| Standard (* Only output problem status *) | Standard (* Only output problem status *)
| Dot | Dot
let input = ref Dimacs let input = ref Dimacs
let output = ref Standard let output = ref Standard
let input_list = [ let input_list = [
"dimacs", Dimacs; "dimacs", Dimacs;
] ]
let output_list = [ let output_list = [
"dot", Dot; "dot", Dot;
] ]
let error_msg opt arg l = let error_msg opt arg l =
Format.fprintf Format.str_formatter "'%s' is not a valid argument for '%s', valid arguments are : %a" 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; arg opt (fun fmt -> List.iter (fun (s, _) -> Format.fprintf fmt "%s, " s)) l;
Format.flush_str_formatter () Format.flush_str_formatter ()
let set_io opt arg flag l = let set_io opt arg flag l =
try try
flag := List.assoc arg l flag := List.assoc arg l
with Not_found -> with Not_found ->
invalid_arg (error_msg opt arg l) invalid_arg (error_msg opt arg l)
let set_input s = set_io "Input" s input input_list let set_input s = set_io "Input" s input input_list
let set_output s = set_io "Output" s output output_list let set_output s = set_io "Output" s output output_list
@ -149,8 +149,8 @@ let main () =
| S.Unsat -> | S.Unsat ->
print "Unsat"; print "Unsat";
if !p_proof_check then begin if !p_proof_check then begin
let p = S.get_proof () in let p = S.get_proof () in
print_proof p print_proof p
end end
let () = let () =