1 (* ========================================================================== *)
2 (* FLYSPECK - BOOK FORMALIZATION *)
4 (* Linear Programming Link *)
5 (* Author: Thomas C. Hales *)
7 (* ========================================================================== *)
10 This file contains material that does not depend on the details of the LP.
11 list processing functions,
16 module Glpk_link = struct
20 needs new mktop on platforms that do not support dynamic loading of Str.
22 ocamlmktop unix.cma nums.cma str.cma -o ocampl
25 glpk needs to be installed, and glpsol needs to be found in the path.
27 needs lib.ml from HOL Light and flyspeck_lib.hl from Flyspeck.
33 let sprintf = Printf.sprintf;;
36 let counter = ref 0 in
38 counter:= !counter + 1;
39 !counter),(fun () -> (counter :=0)));;
43 let maxlist0 xs = fold_right max xs 0;; (* NB: value is always at least 0 *)
45 let get_values key xs =
46 map snd (find_all (function k,_ -> (k=key)) xs);;
49 let rec sort cmp lis = (* from HOL Light lib.ml *)
53 let r,l = partition (cmp piv) rest in
54 (sort cmp l) @ (piv::(sort cmp r));;
62 let rec (--) = fun m n -> if m > n then [] else m::((m + 1) -- n);; (* from HOL Light lib.ml *)
65 let up i = 0 -- (i-1);;
67 let rec rotateL i xs =
70 | x::xss -> rotateL ((i-1) mod length xs) (xss @ [x])
73 let rotateR i = rotateL (-i);;
76 let maxsz = maxlist0 (map length xs) in
77 flatten (map (fun i -> map (rotateL i) xs) (up maxsz));;
81 zip from Harrison's lib.ml.
82 List.combine causes a stack overflow :
83 let tt = up 30000 in combine tt tt;;
84 Stack overflow during evaluation (looping recursion?).
89 | (h1::t1,h2::t2) -> (h1,h2)::(zip t1 t2)
90 | _ -> failwith "zip";;
95 let enumerate xs = zip (up (length xs)) xs;;
98 let (p,_) = find (function _,j -> j=i) (enumerate xs) in
102 let ys = rotation xs in
103 (whereis x ys) mod (length xs);;
106 wheremod [[0;1;2];[3;4;5];[7;8;9]] [8;9;7];; (* 2 *)
109 let unsplit = Flyspeck_lib.unsplit;;
111 let nub = Flyspeck_lib.nub;;
113 let join_lines = Flyspeck_lib.join_lines;;
116 let rec nub = function
118 | x::xs -> x::filter ((!=) x) (nub xs);;
120 let unsplit d f = function
121 | (x::xs) -> fold_left (fun s t -> s^d^(f t)) (f x) xs
124 let join_lines = unsplit "\n" (fun x-> x);;
131 let load_and_close_channel do_close ic =
134 lf ic (Pervasives.input_line ic::a)
135 with End_of_file -> a in
137 if do_close then Pervasives.close_in ic else ();
140 let load_file filename =
141 let ic = Pervasives.open_in filename in load_and_close_channel true ic;;
145 let load_and_close_channel = Flyspeck_lib.load_and_close_channel;;
147 let load_file = Flyspeck_lib.load_file;;
149 let save_stringarray filename xs =
150 let oc = open_out filename in
151 for i=0 to length xs -1
153 Pervasives.output_string oc (nth xs i ^ "\n");
157 let strip_archive filename = (* strip // comments, blank lines, quotation marks etc. *)
158 let (ic,oc) = Unix.open_process(sprintf "cat %s | grep -v '=' | grep -v 'list' | grep -v '^//' | grep -v '^$' | grep '^[^a-z/-]' | sed 's/\"[,;]*//g' | sed 's/_//g' " filename) in
159 let s = load_and_close_channel false ic in
160 let _ = Unix.close_process (ic,oc) in
163 (* example of java style string from hypermap generator. *)
164 let pentstring = "13_150834109178 18 3 0 1 2 3 3 2 7 3 3 0 2 4 5 4 0 3 4 6 1 0 4 3 7 2 8 3 8 2 1 4 8 1 6 9 3 9 6 10 3 10 6 4 3 10 4 5 4 5 3 7 11 3 10 5 11 3 11 7 12 3 12 7 8 3 12 8 9 3 9 10 11 3 11 12 9 ";;
166 (* conversion to list. e.g. convert_to_list pentstring *)
168 let convert_to_list =
169 let split_sp= Str.split (regexp " +") in
170 let strip_ = global_replace (regexp "_") "" in
171 let rec movelist n (x,a) =
172 if n=0 then (x,a) else match x with y::ys -> movelist (n-1) (ys, y::a) in
173 let getone (x,a) = match x with
175 | y::ys -> let (u,v) = movelist y (ys,[]) in (u,v::a) in
176 let rec getall (x,a) =
177 if (x=[]) then (x,a) else getall (getone (x,a)) in
179 let h::ss = (split_sp (strip_ s)) in
180 let _::ns = map int_of_string ss in
181 let (_,a) = getall (ns,[]) in
182 (h,rev (map rev a));;
185 (* Linear programming *)
187 let display_ampl ampl_datafile ampl_of_bb bb = (* for debugging *)
188 let outs = open_out ampl_datafile in
189 let _ = ampl_of_bb outs bb in
190 let _ = close_out outs in
191 Sys.command(sprintf "cat %s" ampl_datafile);;
193 (* model should name the optimal value "optival" *)
195 let solve_counter=ref 0;;
197 let solve com model glpk_outfile varname ampl_of_bb bb =
198 let (ic,oc) = Unix.open_process(com) in
199 let _ = ampl_of_bb oc bb in
200 let _ = close_out oc in
201 let _ = (solve_counter := !solve_counter + 1) in
202 let inp = load_and_close_channel false ic in
203 let _ = Unix.close_process (ic,oc) in
204 (* test for no feasible solution. There are two different messages. *)
205 (* let _ = Sys.command("cat "^ glpk_outfile) in (* debug *) *)
206 let com2 = sprintf "grep \"PROBLEM HAS NO.*FEASIBLE SOLUTION\" %s" glpk_outfile in
207 let (ic,oc) =Unix.open_process(com2) in
208 let inp2 = load_and_close_channel false ic in
209 let _ = Unix.close_process(ic,oc) in
212 let solve_branch_f model glpk_outfile varname ampl_of_bb bb =
213 let com = sprintf "glpsol -m %s -d /dev/stdin | tee %s | grep '^%s' | sed 's/.val//' | sed 's/%s = //' " model glpk_outfile varname varname in
214 solve com model glpk_outfile varname ampl_of_bb bb;;
216 let solve_dual_f model glpk_outfile varname ampl_of_bb bb =
217 let com = sprintf "glpsol -m %s -d /dev/stdin --simplex --exact --dual -w /tmp/dual.out --output /tmp/output.out | tee %s | grep '^%s' | sed 's/.val//' | sed 's/%s = //' " model glpk_outfile varname varname in
218 solve com model glpk_outfile varname ampl_of_bb bb;;
220 let display_lp model ampl_datafile glpk_outfile ampl_of_bb bb =
221 let oc = open_out ampl_datafile in
222 let _ = ampl_of_bb oc bb in
223 let _ = close_out oc in
224 let com = sprintf "glpsol -m %s -d %s | tee %s" model ampl_datafile glpk_outfile in
225 let _ = Sys.command(com) in
228 let cpx_branch model cpxfile ampl_of_bb bb = (* debug *)
229 let com = sprintf "glpsol -m %s --wcpxlp %s -d /dev/stdin | grep '^opti' | sed 's/optival = //' " model cpxfile in
230 let (ic,oc) = Unix.open_process(com) in
231 let _ = ampl_of_bb oc bb in
232 let _ = close_out oc in
233 let _ = load_and_close_channel false ic in
234 let _ = Unix.close_process (ic,oc) in
235 sprintf "cplex file created of lp: %s" cpxfile;;
237 (* for debugging: reading optimal variables values from the glpk_outfile *)
239 let get_dumpvar glpk_outfile s = (* read variables from glpk_outfile *)
240 let com = sprintf "grep '%s' %s | sed 's/^.*= //' " s glpk_outfile in
241 let (ic,oc) = Unix.open_process(com) in
242 let _ = close_out oc in
243 let inp = load_and_close_channel false ic in
244 let _ = Unix.close_process(ic,oc) in
246 (* get_dumpvar "yn.0.*=";; *)