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 [lit:%a] vpremise={{%a}}" 
      (sign a) (a.var.vid+1) (value a) Literal.LT.print a.lit
      premise a.var.vpremise


  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} cpremise={{%a}}" name atoms_vec arr premise cp



end