diff --git a/sat/sat.ml b/sat/sat.ml index 0ff23b98..fd7b1230 100644 --- a/sat/sat.ml +++ b/sat/sat.ml @@ -12,11 +12,11 @@ module Fsat = struct let max_index = ref 0 let make i = - if i <> 0 then begin - max_index := max !max_index (abs i); - i - end else - raise Dummy + if i <> 0 then begin + max_index := max !max_index (abs i); + i + end else + raise Dummy let dummy = 0 @@ -34,7 +34,7 @@ module Fsat = struct let create, iter = let create () = if !max_index <> max_lit then - (incr max_index; !max_index) + (incr max_index; !max_index) else raise Out_of_int in @@ -84,16 +84,16 @@ module Make(Dummy : sig end) = struct type state = SatSolver.t let new_atom () = - try - Fsat.create () - with Fsat.Out_of_int -> - raise Bad_atom + try + Fsat.create () + with Fsat.Out_of_int -> + raise Bad_atom let make i = - try - Fsat.make i - with Fsat.Dummy -> - raise Bad_atom + try + Fsat.make i + with Fsat.Dummy -> + raise Bad_atom let neg = Fsat.neg diff --git a/sat/solver.ml b/sat/solver.ml index f70d81f6..3a2a8f1a 100644 --- a/sat/solver.ml +++ b/sat/solver.ml @@ -414,8 +414,9 @@ module Make (F : Formula_intf.S) var_bump_activity q.var; q.var.seen <- true; seen := q :: !seen; - if q.var.level >= decision_level () then incr pathC - else begin + if q.var.level >= decision_level () then begin + incr pathC + end else begin learnt := q :: !learnt; incr size; blevel := max !blevel q.var.level diff --git a/util/test.ml b/util/test.ml index 0c06416a..41024d8f 100644 --- a/util/test.ml +++ b/util/test.ml @@ -38,39 +38,39 @@ let input_file = fun s -> file := s let usage = "Usage : main [options] " let argspec = Arg.align [ "-v", Arg.Int (fun i -> Log.set_debug i), - " Sets the debug verbose level"; + " Sets the debug verbose level"; "-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"; "-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"; "-model", Arg.Set p_assign, - " Outputs the boolean model found if sat"; -] + " Outputs the boolean model found if sat"; + ] (* 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 + 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 () = - let chan = open_in !file in - let lexbuf = Lexing.from_channel chan in - let l = Parsedimacs.file Lexdimacs.token lexbuf in - List.map (List.map S.make) l + let chan = open_in !file in + let lexbuf = Lexing.from_channel chan in + let l = Parsedimacs.file Lexdimacs.token lexbuf in + List.map (List.map S.make) l let print_cnf cnf = - Format.printf "CNF :@\n"; - List.iter (fun c -> - Format.fprintf Format.std_formatter "%a;@\n" + Format.printf "CNF :@\n"; + List.iter (fun c -> + Format.fprintf Format.std_formatter "%a;@\n" (fun fmt -> List.iter (fun a -> - Format.fprintf fmt "%a@ " S.print_atom a - ) + Format.fprintf fmt "%a@ " S.print_atom a + ) ) c ) cnf @@ -86,8 +86,8 @@ let main () = (* Administrative duties *) Arg.parse argspec input_file usage; if !file = "" then begin - Arg.usage argspec usage; - exit 2 + Arg.usage argspec usage; + exit 2 end; let al = Gc.create_alarm check in @@ -96,19 +96,19 @@ let main () = S.assume cnf; match S.solve () with | S.Sat -> - Format.printf "Sat@."; - if !p_assign then - print_assign Format.std_formatter () + Format.printf "Sat@."; + if !p_assign then + print_assign Format.std_formatter () | S.Unsat -> - Format.printf "Unsat@." + Format.printf "Unsat@." ;; try - main () + main () with | Out_of_time -> - Format.printf "Time limit exceeded@."; - exit 2 + Format.printf "Time limit exceeded@."; + exit 2 | Out_of_space -> - Format.printf "Size limit exceeded@."; - exit 3 + Format.printf "Size limit exceeded@."; + exit 3