(* TODO: *)
(* replace div with bottom in problem??? *)
- let special_k =
- let all_tms = (match div with None -> [] | Some div -> [(div :> i_n_var)]) @ nums @ conv in
- compute_special_k (Listx.from_list (all_tms :> nf list)) in (* compute initial special K *)
+ let all_tms = (match div with None -> [] | Some div -> [(div :> i_n_var)]) @ nums @ conv in
+ if all_tms = [] then failwith "FIXME: empty problem";
+ let initialSpecialK = compute_special_k (Listx.from_list (all_tms :> nf list)) in
let freshno = List.length var_names in
let deltas =
let dummy = `Var (max_int / 2, -666) in
[ ref (Array.to_list (Array.init (List.length ps) (fun i -> i, dummy))) ] in
let trail = [] in
let sigma = [] in
- let p = {freshno; div; conv; ps; sigma; deltas; initialSpecialK=special_k; trail; var_names; label} in
+ let p = {freshno; div; conv; ps; sigma; deltas; initialSpecialK; trail; var_names; label} in
p, check p
;;