let rec term_to_string ?(pretty:bool = true) (term: term) : string =
  match term with
    | Var var ->
        Var.to_string var

    | Const const ->
        if Symbol.is_fd_element const then
          "'" ^ Symbol.to_string ~pretty:pretty const
        else
          Symbol.to_string ~pretty:pretty const

    | Func func when Array.length func.subterms = 0 ->
        (* a constant in disguise *)
        let const = func.symbol in
        if Symbol.is_fd_element const then
          "'" ^ Symbol.to_string ~pretty:pretty const
        else
          Symbol.to_string ~pretty:pretty const

    | Func func ->
        if pretty && Symbol.equal Symbol.equality func.symbol then begin
          "(" ^ term_to_string ~pretty:pretty func.subterms.(0)
            ^ " = "
            ^ term_to_string ~pretty:pretty  func.subterms.(1) ^ ")"
        end

        (* finite model: r(a, ...) ---> r_a(...) *)
        else if pretty
          &&
          Symbol.is_fd_relation func.symbol
        then begin
          let constant, subterms =
            match Array.to_list func.subterms with
              | []
              | _ :: [] ->
                  failwith ("Term.term_to_string: fd relation of arity < 2: " ^ Symbol.to_string func.symbol);

              | head :: tail ->
                  head, tail
          in
          let index =
            if is_term_var constant then
              "r_" ^ string_of_int (Symbol.arity func.symbol - 1)
            else
              "r_" ^ Symbol.to_string ~pretty:pretty (top_symbol_term constant)
          in
            index
            ^ "("
            ^ String.concat ", " (List.map (term_to_string ~pretty:pretty) subterms)
            ^ ")"
        end

        else begin
          Symbol.to_string ~pretty:pretty func.symbol
          ^ "("
          ^ String.concat ", " (List.map (term_to_string ~pretty:pretty) (Array.to_list func.subterms))
          ^ ")"
        end