let () =
  let exit_code = ref 0 in
  try
    if Array.length Sys.argv < 2 then
      invalid_arg "usage: reorder check|repair|replay|contrast|compare|graph|audit|laws|layout|emit [file] [options]";
    let command = Sys.argv.(1) in
    let files = ref [] in
    let model = ref Syntax.Tso in
    let bound = ref None in
    let fences = ref [] in
    let folder = ref None in
    let animate = ref false in
    let delay = ref 0.7 in
    let width = ref 148 in
    let timeout = ref 300000 in
    let location text = match String.split_on_char ':' text with
      | [t; pc] -> int_of_string t, int_of_string pc
      | _ -> invalid_arg "fence locations use thread:instruction" in
    let options = [
      "--model", Arg.String (fun text -> model := Syntax.model text), "sc or tso";
      "--bound", Arg.Int (fun value -> bound := Some value), "maximum scheduler transitions";
      "--fence", Arg.String (fun text -> fences := !fences @ [location text]), "thread:instruction";
      "--out", Arg.String (fun path -> folder := Some path), "output file or directory";
      "--animate", Arg.Set animate, "animate actual execution and solver progress";
      "--delay", Arg.Set_float delay, "seconds per displayed transition";
      "--width", Arg.Set_int width, "terminal width between 78 and 180 columns";
      "--timeout", Arg.Set_int timeout, "solver budget in milliseconds";
    ] in
    let current = ref 1 in
    Arg.parse_argv ~current Sys.argv options (fun path -> files := !files @ [path]) "reorder";
    if !timeout < 1 || !timeout > 3600000 then invalid_arg "timeout outside 1..3600000 milliseconds";
    if not (Float.is_finite !delay) || !delay < 0. || !delay > 10. then
      invalid_arg "delay outside 0..10 seconds";
    let minimum, maximum = match command with
      | "layout" | "laws" -> 0, 0
      | "contrast" -> 2, 2
      | "graph" -> 1, 2
      | "check" | "repair" | "replay" | "compare" | "audit" | "emit" -> 1, 1
      | _ -> invalid_arg "unknown command" in
    let count = List.length !files in
    if count < minimum || count > maximum then
      invalid_arg (Printf.sprintf "%s expects %d..%d input files" command minimum maximum);
    let file () = match !files with path :: _ -> path | [] -> invalid_arg "missing input file" in
    let output fallback = Option.value !folder ~default:fallback in
    let load () =
      let case = Syntax.load (file ()) in
      let case = match !bound with None -> case | Some bound -> {case with Syntax.bound} in
      Syntax.validate case;
      case in
    let with_view case action =
      let view = View.create ~width:!width ~delay:!delay ~animate:!animate case in
      Fun.protect ~finally:(fun () -> View.finish view) (fun () -> action view) in
    let report case result =
      Printf.printf "%s\nmodel=%s  bound=%d  buffer<=8\n" (View.headline case.Syntax.name)
        (Syntax.model_name !model) case.bound;
      match result.Engine.witness with
      | None -> print_endline "UNSAT  requested outcome excluded within the bound"
      | Some witness ->
          Printf.printf "SAT  %d transitions; independent replay passed\n"
            (Array.fold_left (fun n actor -> if actor = 4 then n else n + 1) 0 witness.actors);
          exit_code := 1 in
    begin match command with
    | "check" ->
        let case = load () in
        let result = with_view case (fun view ->
          Engine.check ~timeout:!timeout ~tick:(fun () -> View.tick view)
            ~fences:!fences ~folder:(output "build/check") case !model) in
        report case result
    | "repair" ->
        let case = load () in
        let result = with_view case (fun view ->
          Engine.repair ~timeout:!timeout ~tick:(fun () -> View.tick view)
            ~notify:(View.notify view) case (output "build/repair")) in
        begin match result with
        | None -> print_endline "No repair exists at the candidate locations"; exit_code := 1
        | Some result ->
            Printf.printf "Minimum repair: %d fences; bound %d; %d checked counterexamples\n"
              (List.length result.fences) result.bound (List.length result.clauses)
        end
    | "replay" ->
        let witness = Engine.load_witness (file ()) in
        with_view witness.case (fun view -> View.play view witness)
    | "contrast" ->
        let witness_path, repair_path = match !files with
          | [left; right] -> left, right | _ -> invalid_arg "contrast needs a witness and a repair" in
        let witness = Engine.load_witness witness_path in
        let repair = Engine.certify ~timeout:!timeout repair_path in
        with_view witness.case (fun view -> View.contrast view witness repair)
    | "compare" ->
        let case = load () in
        with_view case (fun view ->
          View.phase view "enumerating sequentially consistent outcomes";
          let sc = Engine.outcomes ~timeout:!timeout ~tick:(fun () -> View.tick view) case Syntax.Sc in
          View.phase view "enumerating TSO outcomes";
          let tso = Engine.outcomes ~timeout:!timeout ~tick:(fun () -> View.tick view) case Syntax.Tso in
          View.outcomes view sc tso)
    | "graph" ->
        let case = load () in
        let fences = match !files with
          | [_; path] ->
              let repair = Engine.certify ~timeout:!timeout path in
              if case <> repair.case then invalid_arg "graph and repair cases differ";
              repair.fences
          | [_] -> !fences
          | _ -> invalid_arg "graph expects a case and an optional repair" in
        with_view case (fun view -> ignore (View.graph view fences))
    | "audit" ->
        let repair = Engine.audit ~timeout:!timeout (file ()) (output "build/audit") in
        Printf.printf "repair verified at bound %d\n%d witnesses replayed; lower-budget certificate UNSAT\n"
          repair.bound (List.length repair.clauses)
    | "layout" ->
        let path = output "build/layout.smt2" in
        Store.write path (Layout.generate ~timeout:!timeout);
        print_endline path
    | "emit" ->
        let case = load () in
        let query = Solver.compile ~timeout:!timeout case !model !fences case.bound in
        let path = output "build/query.smt2" in
        Store.write path (Solver.standalone query);
        print_endline path
    | "laws" ->
        let root = Store.root () in
        let text = Layout.generate ~timeout:!timeout ^
          Store.read (Filename.concat root "smt/machine.smt2") ^ "\n" ^
          Store.read (Filename.concat root "smt/laws.smt2") in
        Store.write (output "build/laws.smt2") text;
        let responses = Sexp.parse (Solver.script ~timeout:!timeout text) in
        if responses <> List.init 16 (fun _ -> Sexp.Atom "unsat") then failwith "machine law check failed";
        print_endline "16 SMT machine laws verified"
    | _ -> invalid_arg "unknown command"
    end;
    exit !exit_code
  with
  | Invalid_argument message | Failure message | Sys_error message ->
      Printf.eprintf "reorder: %s\n" message;
      exit 2
  | Unix.Unix_error (error, operation, _) ->
      Printf.eprintf "reorder: %s: %s\n" operation (Unix.error_message error);
      exit 2
  | Arg.Bad message -> prerr_string message; exit 2
  | Arg.Help message -> print_string message