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