struct
    
  let sign a = if a==a.var.pa then "" else "-"
      
  let level a =
    match a.var.level, a.var.reason with
      | n, _ when n < 0 -> assert false
      | 0, Some c -> sprintf "->0/%s" c.name
      | 0, None   -> "@0"
      | n, Some c -> sprintf "->%d/%s" n c.name
      | n, None   -> sprintf "@@%d" n

  let value a =
    if a.is_true then sprintf "[T%s]" (level a)
    else if a.neg.is_true then sprintf "[F%s]" (level a)
    else ""

  let value_ms_like a =
    if a.is_true then sprintf ":1%s" (level a)
    else if a.neg.is_true then sprintf ":0%s" (level a)
    else ":X"

  let premise fmt v =
    List.iter (fun {name=name} -> fprintf fmt "%s," name) v

  let atom fmt a =
    fprintf fmt "%s%d%s [%a = %d]"
      (sign a) (a.var.vid+1) (value a) Hstring.print a.var.ident.iname
      ((* (snd (Vec.last a.var.ident.ivalues)) land *) a.value)


  let atoms_list fmt l = List.iter (fprintf fmt "%a ; " atom) l
  let atoms_array fmt arr = Array.iter (fprintf fmt "%a ; " atom) arr

  let atoms_vec fmt vec =
    for i = 0 to Vec.size vec - 1 do
      fprintf fmt "%a ; " atom (Vec.get vec i)
    done

  let clause fmt {name=name; atoms=arr; cpremise=cp} =
    fprintf fmt "%s:{ %a}" name atoms_vec arr


end