let rec print fmt = function
| True -> fprintf fmt "true"
| False -> fprintf fmt "false"
| Comp (x, op, y) ->
fprintf fmt "%a %s %a" Term.print x (str_op_comp op) Term.print y
| Ite (la, a1, a2) ->
fprintf fmt "@[ite(%a,@ %a,@ %a)@]"
(print_atoms false "&&") (SAtom.elements la) print a1 print a2
and print_atoms inline sep fmt = function
| [] -> ()
| [a] -> print fmt a
| a::l ->
if inline then
fprintf fmt "%a %s@ %a" print a sep (print_atoms inline sep) l
else
fprintf fmt "%a %s@\n%a" print a sep (print_atoms inline sep) l