graph_generator/graph_control.hl

   1 (* ========================================================================== *)
   2 (* FLYSPECK - CODE FORMALIZATION                                              *)
   3 (*                                                                            *)
   4 (* Software: Graph Generator                                                     *)
   5 (* Author: Thomas C. Hales                                                    *)
   6 (* Date: 2010-09-28                                                           *)
   7 (* ========================================================================== *)
   8
   9 (* Code to control the graph generator *)
  10
  11 module Graph_control = struct
  12
  13 let graph_dir = flyspeck_dir ^ "/../graph_generator";;
  14 let graph_src = graph_dir ^ "/src";;
  15 let graph_classes = graph_dir ^ "/classes";;
  16
  17 let graph_out = Filename.temp_file "graph_out" ".txt";; (*  "/tmp/graph_out.txt";; *)
  18 let render_out = Filename.temp_file "render_out" ".txt";; (* "/tmp/render_out.txt";; *)
  19
  20 let tmp_graph_properties = Filename.temp_file "graph" ".properties";;
  21 let tmp_graph_properties = "/tmp/graph.properties";;  (* Still hard-wired into java code *)
  22
  23 (* duplicated code *)
  24 let unsplit d f = function
  25   | (x::xs) ->  List.fold_left (fun s t -> s^d^(f t)) (f x) xs
  26   | [] -> "";;
  27
  28 let join_comma  = unsplit "," (fun x-> x);;
  29
  30 let join_lines  = unsplit "\n" (fun x-> x);;
  31
  32 let join_space  = unsplit " " (fun x-> x);;
  33
  34 let output_filestring tmpfile a =
  35   let outs = open_out tmpfile in
  36   let _ = try (Printf.fprintf outs "%s" a)
  37   with _ as t -> (close_out outs; raise t) in
  38    close_out outs ;;
  39
  40 (* duplicated code *)
  41
  42
  43
  44 type graph_generator_properties =
  45   {
  46     properties_id : string;
  47     ignore_archive : bool;
  48     exclude_degree2 : bool;
  49     exclude_pent_qrtet : bool;
  50     exclude_2_in_quad : bool;
  51     exclude_1_in_tri : bool;
  52     vertex_count_min : int;
  53     vertex_count_max : int;
  54     node_card_max : int;
  55     node_card_max_at_exceptional_vertex : int;
  56     squander_target : int;
  57     score_target : int;
  58     table_weight_d : int list;
  59     table_weight_a : (int*int) list;
  60     table_weight_b : (int*int*int) list;
  61   };;
  62
  63 let string_of_properties (x:graph_generator_properties) =
  64   let p = Printf.sprintf in
  65   let b t = if t then "true" else "false" in
  66   let weightd = zip (0-- (List.length x.table_weight_d -1)) (x.table_weight_d) in
  67     join_lines
  68       ([
  69          p"#This properties files is machine generated";
  70          p"#Graph Generator %s" (flyspeck_version());
  71          p"#Properties file: %s" (x.properties_id);
  72          p"ignoreArchive=%s" (b x.ignore_archive);
  73          p"excludeDegree2=%s" (b x.exclude_degree2);
  74          p"excludePentQRTet=%s" (b x.exclude_pent_qrtet);
  75          p"exclude2inQuad=%s" (b x.exclude_2_in_quad);
  76          p"exclude1inTri=%s" (b x.exclude_1_in_tri);
  77          p"vertexCountMin=%d" x.vertex_count_min;
  78          p"vertexCountMax=%d" x.vertex_count_max;
  79          p"nodeCardMax=%d" x.node_card_max;
  80          p"nodeCardMaxAtExceptionalVertex=%d" x.node_card_max_at_exceptional_vertex;
  81          p"squanderTarget=%d" x.squander_target;
  82          p"scoreTarget=%d" x.score_target;
  83          (join_lines (map (fun (m,n) -> p"tableWeightD%d=%d" m n) weightd));
  84          (join_lines (map (fun (m,n) -> p"tableWeightA%d=%d" m n) x.table_weight_a));
  85          (join_lines (map (fun (a,b,v) -> p"tableWeightB%d%d=%d" a b v) x.table_weight_b))
  86        ]);;
  87
  88 let flyspeck_properties =
  89   {
  90     properties_id = "flyspeck properties";
  91     ignore_archive=true;
  92     exclude_degree2=true;
  93     exclude_pent_qrtet=true; (* because degrees must be at least 2 *)
  94     exclude_2_in_quad=false;
  95     exclude_1_in_tri=false;
  96     vertex_count_min=13;
  97     vertex_count_max=15;
  98     node_card_max=7;
  99     node_card_max_at_exceptional_vertex=6;
 100     squander_target=15410;
 101     score_target= -1;
 102     table_weight_d = [0;0;0;0;2060;4819;7120;15410;15410];
 103     table_weight_a = [(5,6300)];
 104     (* exclude b02 because degrees are at least 3.  b50 is a special calculation *)
 105     table_weight_b = [(0,3,6180);(0,4,9700);(1,2,6560);(1,3,6180);
 106                       (2,1,7970);(2,2,4120);(2,3,12851);
 107                       (3,1,3110);(3,2,8170);(4,0,3470);(4,1,3660);
 108                       (5,0,400);(5,1,11360);(6,0,6860);(7,0,14500);];
 109   };;
 110
 111 let bauer_nipkow_deprecated_properties =
 112   {
 113     properties_id = "flyspeck properties from the Bauer Nipkow Isabelle classification Fall 2010."^
 114       " table_weight_d is out of date in the 7578 entry." ^
 115       " This should produce (9,1105,15991,1657) graphs in the pass with n=3,4,5,6, respectively";
 116     ignore_archive=true;
 117     exclude_degree2=true;
 118     exclude_pent_qrtet=true; (* because degrees must be at least 2 *)
 119     exclude_2_in_quad=false;
 120     exclude_1_in_tri=false;
 121     vertex_count_min=13;
 122     vertex_count_max=15;
 123     node_card_max=7;
 124     node_card_max_at_exceptional_vertex=6;
 125     squander_target=15410;
 126     score_target= -1;
 127     table_weight_d = [0;0;0;0;2060;4819;7578;15410;15410];
 128     table_weight_a = [(5,6300)];
 129     (* exclude b02 because degrees are at least 3.  b50 is a special calculation *)
 130     table_weight_b = [(0,3,6180);(0,4,9700);(1,2,6560);(1,3,6180);
 131                       (2,1,7970);(2,2,4120);(2,3,12851);
 132                       (3,1,3110);(3,2,8170);(4,0,3470);(4,1,3660);
 133                       (5,0,400);(5,1,11360);(6,0,6860);(7,0,14500);];
 134   };;
 135
 136 let kepler98_deprecated_properties =
 137   {
 138     properties_id = "values from the original 1998 proof of the Kepler conjecture, but relaxed to eliminate score";
 139     ignore_archive=true;
 140     exclude_degree2=true;
 141     exclude_pent_qrtet=true;
 142     exclude_2_in_quad=true;
 143     exclude_1_in_tri=true;
 144     vertex_count_min=10;
 145     vertex_count_max=100;
 146     node_card_max=6;
 147     node_card_max_at_exceptional_vertex=5;
 148     squander_target=14800;
 149     score_target= -1;
 150     table_weight_d = [0;0;0;0;2378;4896;7414;9932;10916];
 151     table_weight_a = [(3,1400);(4,1500)];
 152     table_weight_b = [(0,3,7135);(0,4,10649);(1,2,6950);(1,3,7135);
 153                       (2,1,8500);(2,2,4756);(2,3,12981);
 154                       (3,1,3642);(3,2,8334);(4,0,4139);(4,1,3781);
 155                       (5,0,550);(5,1,11220);(6,0,6339)];
 156   };;
 157
 158
 159
 160 let fejes_toth_contact_conjecture_properties =
 161   {
 162     properties_id = "Fejes Toth's Contact Conjecture";
 163     ignore_archive=true;
 164     exclude_degree2=false;
 165     exclude_pent_qrtet=true;
 166     exclude_2_in_quad=true;
 167     exclude_1_in_tri=true;
 168     vertex_count_min=12;
 169     vertex_count_max=12;
 170     node_card_max=4;
 171     node_card_max_at_exceptional_vertex=4;
 172     squander_target=1541;
 173     score_target= -1;
 174     (* table_weight_d = [0;0;0;0;206;480;756;1031;1306];  change sep 23, 2012 *)
 175     table_weight_d = [0;0;0;0;206;476;746;1016;1286];
 176     table_weight_a = [(0,0);(1,0);(2,0);(3,0)];
 177     table_weight_b = [(0,3,618);(1,3,618);(2,2,412)];
 178   };;
 179
 180 let mclaughlin_dodecaheral_conjecture_properties=
 181 {
 182   properties_id="McLaughlin's Dodecahedral Theorem";
 183   ignore_archive=true;
 184   exclude_degree2=false;
 185   exclude_pent_qrtet=true;
 186   exclude_2_in_quad=true;
 187   exclude_1_in_tri=true;
 188   vertex_count_min=13;
 189   vertex_count_max=100;
 190   node_card_max=6;
 191   node_card_max_at_exceptional_vertex=5;
 192   squander_target=178;
 193   score_target= -1;
 194   table_weight_d = [0;0;0;0;31;76;121;166;200];
 195   table_weight_a = [(3,0);(4,16)];
 196   table_weight_b = [(0,3,93);(0,4,125);(1,2,91);(1,3,93);
 197                     (2,1,133);(2,2,62);(3,1,43);(3,2,118);(4,0,53);(4,1,31);(5,0,4)];
 198 };;
 199
 200 (* deprecated
 201 let set_properties file_name =
 202     Sys.command(Printf.sprintf "cd %s; cp %s /tmp/graph.properties" graph_dir file_name);;
 203 *)
 204
 205 let set_prop_file (x:graph_generator_properties) =
 206   output_filestring tmp_graph_properties (string_of_properties x);;
 207
 208 let compile () =
 209   Sys.command(Printf.sprintf "cd %s; javac -d ../classes graph/Generator.java " graph_src);;
 210
 211 let execute () =
 212   Sys.command(Printf.sprintf "cd %s; java -Xms300m -Xmx1g graph/Generator | tee %s" graph_classes graph_out);;
 213
 214 let run(x:graph_generator_properties)=
 215   let _ = set_prop_file (x) in
 216   let _ = compile() in
 217   let _ = execute() in
 218     "execution complete.  Results tee'd to " ^ graph_out;;
 219
 220 (* rendering *)
 221
 222 let compile_render () =
 223   Sys.command(Printf.sprintf "cd %s; javac -d ../classes render/Gendot.java " graph_src);;
 224
 225 let compile_gentikz () =
 226   Sys.command(Printf.sprintf "cd %s; javac -d ../classes render/Gentikz.java " graph_src);;
 227
 228 let execute_render s =
 229   let _ = Sys.command(Printf.sprintf "cd %s; java render/Gendot \"%s\" |tee %s" graph_classes s render_out) in
 230     "execution complete. Results tee'd to " ^ render_out;;
 231
 232 let execute_g prm s =
 233   let _ = Sys.command(Printf.sprintf "cd %s; java render/%s \"%s\" |tee %s" graph_classes prm s render_out) in
 234     "execution complete. Results tee'd to " ^ render_out;;
 235
 236 let execute_gendot = execute_g "Gendot";;
 237
 238 let execute_gentikz = execute_g "Gentikz";;
 239
 240 let example_graph = "0 24 3 0 1 2 3 0 2 3 3 3 2 4 3 4 2 1 3 4 1 5 3 5 1 0 3 5 0 6 3 6 0 7 3 7 0 3 3 7 3 8 3 8 3 9 3 9 3 4 3 9 4 10 3 10 4 5 3 10 5 11 3 11 5 6 3 11 6 12 3 12 6 7 3 12 7 8 3 12 8 13 3 13 8 9 3 11 12 13 3 10 11 13 3 13 9 10 ";;
 241
 242 let example_render() =
 243   let _ = compile_render() in
 244     execute_render example_graph;;
 245
 246 let example_gentikz() =
 247   let _ = compile_gentikz() in
 248     execute_gentikz example_graph;;
 249
 250 let execute() =
 251   let _ = example_render() in
 252   let _ = example_gentikz() in
 253     run(flyspeck_properties);;
 254
 255
 256 end;;