glpk/tame_archive/scaffolding.hl

   1 (* ========================================================================== *)
   2 (* FLYSPECK - CODE FORMALIZATION                                              *)
   3 (*                                                                            *)
   4 (* Program: Linear Programs                                                   *)
   5 (* Author: Thomas C. Hales                                                    *)
   6 (* Date: 2010-08-01                                                           *)
   7 (* ========================================================================== *)
   8
   9
  10 (*
  11    This file contains code that has been used in the interaction to
  12    find inequalities and branching that work.  Once the working system
  13    has been designed, this file is no longer required.
  14 *)
  15
  16
  17 module Tame_scaffolding = struct
  18
  19
  20   let libsort = sort;;  (* from Hol light lib.ml, before we open List *)
  21
  22   open Glpk_link;;
  23   open Lpproc;;
  24   open Hard_lp;;
  25   open List;;
  26
  27 (* Old results from hard_lp.hl *)
  28
  29 (* preliminary version *)
  30
  31 let add_hints bb =
  32   if not(is_feas bb) then () else
  33   if not(bb.hints = []) then () else
  34     add_hints_force bb;;
  35
  36 let filter_feas_hint bbs = filter_feas_f add_hints bbs;;
  37
  38 let onepass_hint = function
  39   [] -> []
  40   | bb::bbss as bbs ->
  41   let _ = onepass_backup := bbs in
  42   let brs =  switch_hint bb in
  43   let brs1 = map set_face_numerics brs in
  44   let brs2 = map set_node_numerics brs1 in
  45   let _ = echo bbs in
  46     sortbb ((filter_feas_hint brs2) @ bbss);;
  47
  48 (* Generate graphics files of a branchnbound, save gif as a /tmp file.  *)
  49
  50 let mk_gif bb = (Sys.chdir
  51  "/Users/thomashales/Desktop/googlecode/flyspeck/graph_generator/classes";
  52  Sys.command
  53     ("java render/Gendot \""^bb.string_rep ^
  54       "\" | neato -s -n -Tgif -o "^
  55     (Filename.temp_file ("render"^bb.hypermap_id^"_") (".gif"))));;
  56
  57
  58
  59 let get_azim_table xs bb =
  60    let [y1;y2;y3] = map (yn bb) xs in
  61    let [y6;y4;y5] = map (fun i -> ye bb ( i, int_of_face xs bb)) xs in
  62    let [a1;a2;a3] = map (fun i -> azim bb (i, int_of_face xs bb)) xs in
  63    let b1 = dih_y y1 y2 y3 y4 y5 y6 in
  64    let b2 = dih_y y2 y3 y1 y5 y6 y4 in
  65    let b3 = dih_y y3 y1 y2 y6 y4 y5 in
  66    (y1,y2,y3,y4,y5,y6,("dih_lp",a1,"dih_y",b1,a1-. b1),("dih2_lp",a2,"dih2_y",b2,a2-. b2),("dih3_lp",a3,"dih3_y",b3,a3 -. b3),"soldiff",a1+. a2 +. a3 -.( b1 +. b2 +. b3));;
  67
  68 let testval f xs bb =
  69   let (y1,y2,y3,y4,y5,y6,_,_,_,_,_) = get_azim_table xs bb in
  70   f y1 y2 y3 y4 y5 y6;;
  71
  72 let testvalsym d  = testval (fun y1 y2 y3 y4 y5 y6 -> d y1 y3 y2 y4 y6 y5);;
  73
  74 (* for the purpose of debugging    *)
  75
  76 let check_basic_format bb =
  77     (subset bb.std3_small  (rotation bb.std_faces_not_super)) &
  78     (subset bb.std3_big (rotation bb.std_faces_not_super)) &
  79     (intersect (rotation bb.std3_small) (rotation bb.std3_big) = []) &
  80     (subset bb.node_218_236 bb.node_218_252) &
  81     (subset bb.node_236_252 bb.node_218_252);;
  82
  83 (* for debugging, we don't want overly long lists. Pick out random elts. *)
  84
  85 let random_elt xs =
  86   let i = Random.int (length xs) in
  87   let r = nth xs i in
  88    r, (subtract xs [r]);;
  89
  90 let rec random_elts n xs =
  91   if n=0 then ([],xs) else
  92     let (a,b) = random_elts (n-1)  xs in
  93     let (r,s) = random_elt b in (r::a,s);;
  94
  95 let get_highest n bbs =
  96   let eval bb = (match bb.lpvalue with Lp_value r -> r | _ -> 0.0  ) in
  97   (chop_list n (libsort (fun b1 b2 -> eval b1 > eval b2) bbs));;
  98
  99 let prune_results n bbs =
 100    if length bbs <= 2*n then bbs else
 101      let (b1,b2) = get_highest n bbs in
 102      b1 @ fst (random_elts n b2);;
 103
 104 let rec allpass_prune_hint prune count bbs =
 105    if  count <= 0 then bbs else allpass_prune_hint prune (count - 1) (prune_results prune (onepass_hint bbs));;
 106
 107 (* Code to help eliminate final cases. *)
 108
 109   let tmpfile = Filename.temp_file "display_ampl_" ".dat";;
 110
 111 let display_ampl =
 112    fun bb -> Glpk_link.display_ampl tmpfile Lpproc.ampl_of_bb bb;;
 113
 114 let display_lp bb = Glpk_link.display_lp
 115   Lpproc.model tmpfile Lpproc.glpk_outfile Lpproc.ampl_of_bb bb ;;
 116
 117 let remake_model =
 118   let bodyfile =  Filename.temp_file "body_" ".mod" in
 119   let m = Lpproc.model in
 120   fun () ->
 121     let _ = Lpproc.modelbody := bodyfile in
 122     let _ = Parse_ineq.output_filestring bodyfile (Parse_ineq.lpstring()) in
 123     let _ = Sys.chdir(tame_dir) in
 124       Sys.command("cp head.mod "^m^"; cat "^bodyfile^" >> "^
 125                      m^"; cat tail.mod >> "^m);;
 126
 127 (* remake_model();; *)
 128
 129 let clone bb = modify_bb bb false [] [];;
 130
 131 let unset_edge bb =
 132   let f = rotation (faces bb) in
 133   let g x = map (fun t -> [nth t 0; nth t 1]) x in
 134   libsort (<) (nub(subtract (g f) (g bb.d_edge_200_225 @ g bb.d_edge_225_252)));;
 135
 136
 137
 138 end;;