let join = String.concat " "

let structure name constructor fields =
  let width = List.fold_left (fun sum (_, _, size) -> sum + size) 0 fields in
  let arguments = join (List.map (fun (field, kind, _) -> Printf.sprintf "(%s %s)" field kind) fields) in
  let values = join (List.map (fun (field, _, _) -> field) fields) in
  let high = ref (width - 1) in
  let selectors = List.map (fun (field, kind, size) ->
    let low = !high - size + 1 in
    let result = Printf.sprintf
      "(define-fun %s ((cells %s)) %s ((_ extract %d %d) cells))" field name kind !high low in
    high := low - 1;
    result) fields in
  [Printf.sprintf "(define-sort %s () (_ BitVec %d))" name width;
   Printf.sprintf "(define-fun %s (%s) %s (concat %s))" constructor arguments name values] @ selectors

let record name prefix element count size =
  let fields = List.init count (fun i -> Printf.sprintf "%s%d" prefix i, element, size) in
  let lines = structure name prefix fields in
  let value = ref (Printf.sprintf "(%s%d cells)" prefix (count - 1)) in
  for i = count - 2 downto 0 do
    value := Printf.sprintf "(ite (= i #x%02x) (%s%d cells) %s)" i prefix i !value
  done;
  let fields = List.init count (fun i ->
    Printf.sprintf "(ite (= i #x%02x) v (%s%d cells))" i prefix i) in
  lines @ [Printf.sprintf "(define-fun at ((cells %s) (i Index)) %s\n  %s)" name element !value;
    Printf.sprintf "(define-fun update ((cells %s) (i Index) (v %s)) %s\n  (%s %s))"
      name element name prefix (join fields)]

let generate ~timeout =
  if timeout <= 0 then invalid_arg "timeout must be positive";
  let lines = ["(set-logic QF_BV)"; "(set-option :produce-models true)";
    Printf.sprintf "(set-option :timeout %d)" timeout;
    "(define-sort Index () (_ BitVec 8))"; "(define-sort Word () (_ BitVec 64))"] @
    record "Slots" "indices" "Index" 16 8 @
    record "Words" "words" "Word" 16 64 @
    record "Queues" "queues" "Words" 2 1024 @
    record "Positions" "positions" "Slots" 2 128 @
    structure "State" "state" [
      "memory", "Words", 1024; "registers", "Words", 1024;
      "counters", "Slots", 128; "heads", "Slots", 128; "tails", "Slots", 128;
      "addresses", "Positions", 256; "values", "Queues", 2048;
      "positions", "Positions", 256; "critical", "Slots", 128] in
  let constants = List.map (fun (name, kind, constructor, value, count) ->
    Printf.sprintf "(define-fun %s () %s\n  (%s %s))" name kind constructor
      (join (List.init count (fun _ -> value)))) [
    "zeros", "Words", "words", "#x0000000000000000", 16;
    "slots", "Slots", "indices", "#x00", 16;
    "absent", "Slots", "indices", "#xff", 16;
    "emptyqueues", "Queues", "queues", "zeros", 2;
    "emptypositions", "Positions", "positions", "slots", 2;
    "unseen", "Positions", "positions", "absent", 2] in
  String.concat "\n\n" (lines @ constants) ^ "\n"