let add_constant (sorts: sorts) (constant: symbol) (existing: symbol) : unit =
  if SymbolTable.mem sorts.symbol_sorts constant then
    failwith ("Sort_inference.add_constant: symbol already known: " ^ Symbol.to_string constant);

  let sort =
    try
      result_sort (SymbolTable.find sorts.symbol_sorts existing)
    with
      | Not_found ->
          failwith ("Sort_inference.add_constant: symbol is unkown: " ^ Symbol.to_string existing);
  in 
  let composed_sort =
    Array.make 1 { sort = 0; repr = Some sort; size = 1 }
  in
    SymbolTable.add sorts.symbol_sorts constant composed_sort;

    let constants =
      List.sort sort_symbols (constant :: sorts.constants)
    in
    let constants_partition, max_size =
      partition_constants sorts.symbol_sorts constants sorts.number_of_sorts
    in
      sorts.constants <- constants;
      sorts.constants_partition <- constants_partition;
      sorts.max_constant_partition_size <- max_size