From 8d95cecba4f00e34fee908453410e70e9234f621 Mon Sep 17 00:00:00 2001 From: Guillaume Bury Date: Sat, 1 Nov 2014 17:17:50 +0100 Subject: [PATCH] Correct indentation. --- common/vec.ml | 6 +-- sat/sat.ml | 140 +++++++++++++++++++++++++------------------------- sat/sat.mli | 46 ++++++++--------- sat/solver.ml | 4 +- util/log.ml | 20 ++++---- util/log.mli | 10 ++-- util/test.ml | 42 +++++++-------- 7 files changed, 134 insertions(+), 134 deletions(-) diff --git a/common/vec.ml b/common/vec.ml index 4cff679c..0300bdb3 100644 --- a/common/vec.ml +++ b/common/vec.ml @@ -114,9 +114,9 @@ let sort t f = t.data <- sub_arr let iter f t = - for i = 0 to size t - 1 do - f (get t i) - done + for i = 0 to size t - 1 do + f (get t i) + done (* template diff --git a/sat/sat.ml b/sat/sat.ml index 7851bdf5..07602202 100644 --- a/sat/sat.ml +++ b/sat/sat.ml @@ -1,51 +1,51 @@ (* Copyright 2014 Guillaume Bury *) module Fsat = struct - exception Out_of_int + exception Out_of_int - (* Until the constant true_ and false_ are not needed anymore, - * wa can't simply use sigend integers to represent literals *) - type t = { - (* Invariant : var >= 0 *) - var : int; - pos : bool; - } + (* Until the constant true_ and false_ are not needed anymore, + * wa can't simply use sigend integers to represent literals *) + type t = { + (* Invariant : var >= 0 *) + var : int; + pos : bool; + } - let max_index = ref 0 + let max_index = ref 0 - let true_ = { var = 0; pos = true } - let false_ = { var = 0; pos = false } - let dummy = { var = -1; pos = true } + let true_ = { var = 0; pos = true } + let false_ = { var = 0; pos = false } + let dummy = { var = -1; pos = true } - let unsafe_make i = { var = i; pos = true } - let make i = if i > 0 then unsafe_make i else dummy + let unsafe_make i = { var = i; pos = true } + let make i = if i > 0 then unsafe_make i else dummy - let neg a = { a with pos = not a.pos } - let norm a = unsafe_make a.var, not a.pos + let neg a = { a with pos = not a.pos } + let norm a = unsafe_make a.var, not a.pos - let hash = Hashtbl.hash - let equal = (=) - let compare = Pervasives.compare + let hash = Hashtbl.hash + let equal = (=) + let compare = Pervasives.compare - let label a = Hstring.make "" - let add_label _ _ = () + let label a = Hstring.make "" + let add_label _ _ = () - let create, iter = - let create () = - if !max_index <> max_int then - (incr max_index; unsafe_make !max_index) - else - raise Out_of_int - in - let iter: (t -> unit) -> unit = fun f -> - for j = 1 to !max_index do - f (unsafe_make j) - done - in - create, iter + let create, iter = + let create () = + if !max_index <> max_int then + (incr max_index; unsafe_make !max_index) + else + raise Out_of_int + in + let iter: (t -> unit) -> unit = fun f -> + for j = 1 to !max_index do + f (unsafe_make j) + done + in + create, iter - let print fmt a = - Format.fprintf fmt "%s%d" (if not a.pos then "~" else "") a.var + let print fmt a = + Format.fprintf fmt "%s%d" (if not a.pos then "~" else "") a.var end @@ -54,53 +54,53 @@ module Stypes = Solver_types.Make(Fsat) module Exp = Explanation.Make(Stypes) module Tsat = struct - (* We don't have anything to do since the SAT Solver already - * does propagation and conflict detection *) + (* We don't have anything to do since the SAT Solver already + * does propagation and conflict detection *) - type t = int - type formula = Fsat.t - type explanation = Exp.t + type t = int + type formula = Fsat.t + type explanation = Exp.t - exception Inconsistent of explanation + exception Inconsistent of explanation - let dummy = -1 - let empty () = 0 - let assume ~cs:_ _ _ _ = 0 + let dummy = -1 + let empty () = 0 + let assume ~cs:_ _ _ _ = 0 end module Make(Dummy : sig end) = struct - module SatSolver = Solver.Make(Fsat)(Stypes)(Exp)(Tsat) + module SatSolver = Solver.Make(Fsat)(Stypes)(Exp)(Tsat) - type res = - | Sat - | Unsat + type res = + | Sat + | Unsat - let _i = ref 0 + let _i = ref 0 - type atom = Fsat.t - type state = SatSolver.t + type atom = Fsat.t + type state = SatSolver.t - let neg = Fsat.neg - let new_atom = Fsat.create + let neg = Fsat.neg + let new_atom = Fsat.create - let hash = Fsat.hash - let equal = Fsat.equal - let compare = Fsat.compare + let hash = Fsat.hash + let equal = Fsat.equal + let compare = Fsat.compare - let print_atom = Fsat.print - let iter_atoms = Fsat.iter + let print_atom = Fsat.print + let iter_atoms = Fsat.iter - let solve () = - try - SatSolver.solve (); - assert false - with - | SatSolver.Sat -> Sat - | SatSolver.Unsat _ -> Unsat + let solve () = + try + SatSolver.solve (); + assert false + with + | SatSolver.Sat -> Sat + | SatSolver.Unsat _ -> Unsat - let assume l = - incr _i; - SatSolver.assume l !_i + let assume l = + incr _i; + SatSolver.assume l !_i - let eval = SatSolver.eval + let eval = SatSolver.eval end diff --git a/sat/sat.mli b/sat/sat.mli index 77a00b0f..132de97d 100644 --- a/sat/sat.mli +++ b/sat/sat.mli @@ -1,39 +1,39 @@ (* Copyright 2014 Guillaume Bury *) module Make(Dummy: sig end) : sig - (** Fonctor to make a pure SAT Solver module with built-in literals. *) + (** Fonctor to make a pure SAT Solver module with built-in literals. *) - type atom - (** Abstract type for atoms, i.e boolean literals. *) + type atom + (** Abstract type for atoms, i.e boolean literals. *) - type res = Sat | Unsat - (** Type of results returned by the solve function. *) + type res = Sat | Unsat + (** Type of results returned by the solve function. *) - val new_atom : unit -> atom - (** [new_atom ()] returns a fresh literal. *) + val new_atom : unit -> atom + (** [new_atom ()] returns a fresh literal. *) - val neg : atom -> atom - (** [neg a] returns the negation of a literal. Involutive, i.e [neg (neg a) = a]. *) + 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 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 print_atom : Format.formatter -> atom -> unit - (** Print the atom on the given formatter. *) + val print_atom : Format.formatter -> atom -> unit + (** Print the atom on the given formatter. *) - val iter_atoms : (atom -> unit) -> unit - (** Allows iteration over all atoms created (even if unused). *) + val iter_atoms : (atom -> unit) -> unit + (** Allows iteration over all atoms created (even if unused). *) - val solve : unit -> res - (** Returns the satisfiability status of the current set of assumptions. *) + val solve : unit -> res + (** Returns the satisfiability status of the current set of assumptions. *) - val eval : atom -> bool - (** Return the current assignement of the literals. *) + val eval : atom -> bool + (** Return the current assignement of the literals. *) - val assume : atom list list -> unit - (** Add a list of clauses to the set of assumptions. *) + val assume : atom list list -> unit + (** Add a list of clauses to the set of assumptions. *) end diff --git a/sat/solver.ml b/sat/solver.ml index 18915bfe..3af38613 100644 --- a/sat/solver.ml +++ b/sat/solver.ml @@ -189,7 +189,7 @@ module Make (F : Formula_intf.S) Vec.push env.trail_lim (Vec.size env.trail); Vec.push env.tenv_queue env.tenv; (* save the current tenv *) Log.debug 5 "New decision level : %d (%d in env queue)(%d in trail)" - (Vec.size env.trail_lim) (Vec.size env.tenv_queue) (Vec.size env.trail); + (Vec.size env.trail_lim) (Vec.size env.tenv_queue) (Vec.size env.trail); () let attach_clause c = @@ -253,7 +253,7 @@ module Make (F : Formula_intf.S) assert (v.pa.is_true || v.na.is_true); pick_branch_lit () end else - v + v let enqueue a lvl reason = assert (not a.is_true && not a.neg.is_true && diff --git a/util/log.ml b/util/log.ml index f8f3018e..151d17c8 100644 --- a/util/log.ml +++ b/util/log.ml @@ -50,14 +50,14 @@ let need_cleanup = ref false let debug l format = let b = Buffer.create 15 in if l <= !debug_level_ - then ( - (if !need_cleanup then clear_line ()); - Printf.bprintf b "%% [%.3f] " (get_total_time ()); - Printf.kbprintf - (fun b -> print_endline (Buffer.contents b)) - b format) - else - Printf.ifprintf b format + then ( + (if !need_cleanup then clear_line ()); + Printf.bprintf b "%% [%.3f] " (get_total_time ()); + Printf.kbprintf + (fun b -> print_endline (Buffer.contents b)) + b format) + else + Printf.ifprintf b format let pp_pos pos = let open Lexing in @@ -76,8 +76,8 @@ let fprintf oc format = let buffer = Buffer.create 64 in Printf.kbprintf (fun fmt -> Buffer.output_buffer oc buffer) - buffer - format + buffer + format let printf format = fprintf stdout format let eprintf format = fprintf stderr format diff --git a/util/log.mli b/util/log.mli index 80a0d4d8..3a5c6b42 100644 --- a/util/log.mli +++ b/util/log.mli @@ -40,7 +40,7 @@ val get_debug : unit -> int (** Current debug level *) val need_cleanup : bool ref (** Cleanup line before printing? *) val debug : int -> ('a, Buffer.t, unit, unit) format4 -> 'a - (** debug message *) +(** debug message *) val pp_pos : Lexing.position -> string @@ -57,18 +57,18 @@ val on_fmt : (Format.formatter -> 'a -> 'b) -> 'a -> string val on_buffer : (Buffer.t -> 'a -> unit) -> 'a -> string val pp_pair: ?sep:string -> (Buffer.t -> 'a -> unit) -> - (Buffer.t -> 'b -> unit) -> Buffer.t -> ('a * 'b) -> unit + (Buffer.t -> 'b -> unit) -> Buffer.t -> ('a * 'b) -> unit val pp_opt : (Buffer.t -> 'a -> unit) -> Buffer.t -> 'a option -> unit (** print a list of items using the printing function *) val pp_list: ?sep:string -> (Buffer.t -> 'a -> unit) - -> Buffer.t -> 'a list -> unit + -> Buffer.t -> 'a list -> unit (** print an array of items with printing function *) val pp_array: ?sep:string -> (Buffer.t -> 'a -> unit) - -> Buffer.t -> 'a array -> unit + -> Buffer.t -> 'a array -> unit (** print an array, giving the printing function both index and item *) val pp_arrayi: ?sep:string -> (Buffer.t -> int -> 'a -> unit) - -> Buffer.t -> 'a array -> unit + -> Buffer.t -> 'a array -> unit diff --git a/util/test.ml b/util/test.ml index 3a8f8dc1..9acc4568 100644 --- a/util/test.ml +++ b/util/test.ml @@ -2,36 +2,36 @@ module S = Sat.Make(struct end) let init () = - let v = Array.init 5 (fun _ -> S.new_atom ()) in - [ [ - [v.(0); v.(1)]; - [S.neg v.(0); v.(2)]; - [S.neg v.(1); v.(2)]; - ]; - [ - [v.(3); v.(4)]; - [S.neg v.(3); S.neg v.(2)]; - [S.neg v.(4); S.neg v.(2)]; - ] + let v = Array.init 5 (fun _ -> S.new_atom ()) in + [ [ + [v.(0); v.(1)]; + [S.neg v.(0); v.(2)]; + [S.neg v.(1); v.(2)]; + ]; + [ + [v.(3); v.(4)]; + [S.neg v.(3); S.neg v.(2)]; + [S.neg v.(4); S.neg v.(2)]; ] + ] let print_assign fmt () = - S.iter_atoms (fun a -> - Format.fprintf fmt "%a -> %s,@ " + S.iter_atoms (fun a -> + Format.fprintf fmt "%a -> %s,@ " S.print_atom a (if S.eval a then "true" else "false") ) let main () = - Log.set_debug 10; - Format.printf "Hello World !@."; - List.iter (fun l -> - List.iter (fun c -> Format.printf "Adding : %a@." + Log.set_debug 10; + Format.printf "Hello World !@."; + List.iter (fun l -> + List.iter (fun c -> Format.printf "Adding : %a@." (fun _ -> List.iter (fun a -> Format.printf "%a " S.print_atom a)) c) l; - S.assume l; - match S.solve () with - | S.Sat -> Format.printf "Sat@\n%a@." print_assign () - | S.Unsat -> Format.printf "Unsat@.") (init ()); + S.assume l; + match S.solve () with + | S.Sat -> Format.printf "Sat@\n%a@." print_assign () + | S.Unsat -> Format.printf "Unsat@.") (init ()); ;; main ()