(* ========================================================================== *)
(* FLYSPECK - CODE FORMALIZATION                                              *)
(*                                                                            *)
(* Program: Linear Programs                                                   *)
(* Author: Thomas C. Hales                                                    *)
(* Date: 2010-08-01                                                           *)
(* ========================================================================== *)


(*
Local build file for linear programs.
*)

flyspeck_needs "nonlinear/ineq.hl";;
flyspeck_needs   "nonlinear/parse_ineq.hl";;
flyspeck_needs "../glpk/glpk_link.ml";;
flyspeck_needs "../glpk/tame_archive/lpproc.ml";;
flyspeck_needs "../glpk/sphere.ml";;
flyspeck_needs "../glpk/tame_archive/hard_lp.ml";;
flyspeck_needs "../glpk/tame_archive/scaffolding.hl";;

module Build_lp = struct

let test_nonlinear_lp() = let lpineq = Ineq.getfield Lp in
  Parse_ineq.execute_cfsqp_list lpineq;;

let rebuild_body_mod() =
  let _ = Parse_ineq.output_filestring "/tmp/body.mod" (Parse_ineq.lpstring()) in
  let _ = Sys.command("diff /tmp/body.mod "^flyspeck_dir^"/../glpk/tame_archive/body.mod") in
    "--end of diff--  To install, move /tmp/body.mod to glpk/tame_archive/body.mod";;

(*
test_nonlinear_lp();;
rebuild_body_mod();;
*)


let execute() = 
  let _ = Sys.command("date") in
  let startdate = process_to_string  "date" in
  let lpdata = Lpproc.execute() in
  let  (tame_bb,feasible_bb,hard_bb,easy_bb,
	remaining_easy_bb) = lpdata in
  let output = 
    if (remaining_easy_bb=[]) then (([],[],[],[],[]),Hard_lp.execute(),"finished output")
    else (lpdata,[[]],"easy cases remain- aborted") in
  let _ = Sys.command("date") in
  let enddate = process_to_string "date" in
    (startdate,!Glpk_link.solve_counter,output,enddate);;

end;;


(* LOG OF RUNS:


run_all();; 
!Glpk_link.solve_counter;;

Run of Hard_lp.execute();;
started at Thu Aug  5 16:58:26 ICT 2010
finished Aug  5 23:20.
STACK 1 15413 (so about 30K linear programs)
val it : Lpproc.branchnbound list list =
  [[]; []; []; []; []; []; []; []; []; []; []; []]

retested Sep 22 on Thackmac, identical results, svn 1978.

retested Oct 22, 2010 on Malt, 2026, some weakened ineqs.


All retested svn 2402 on Malt
May 10, 2011, eliminated ineq 7676202716 from body.mod.
Still passes. So this inequality can be eliminated entirely!
STACK 1 16604
val it : Lpproc.branchnbound list list =
  [[]; []; []; []; []; []; []; []; []; []; []; []]


May 18, svn 2411 on malt,
experiment 0.696 -> 0.616, and moved 3 more cases to hardid. 

let run_output = run_all();;

STACK 1 18925
val hard_out : Lpproc.branchnbound list list =
  [[]; []; []; []; []; []; []; []; []; []; []; []; []; []; []]
I also ran the new hex cases (at least those with a pent), and they all pass easily.


svn 2412 on malt, May 22, 2011,
tameTableD[6,0]->0.712, tameTableD[4,1]->0.616.
This only affects the hexagon cases.  Graph generator for hexagons was rerun.

Lpproc.archiveraw :=  (Filename.concat archive_dir "string_hex_may2011.txt");;
!Lpproc.archiveraw;;
let lpdata = Lpproc.execute();;
let  (tame_bb,feasible_bb,hard_bb,easy_bb,remaining_easy_bb) = lpdata;;
(no hexagons in the hardid list)

April 14, 2012. Preparing new run. Seems to be running fine on Thackmac.


Quad Inequalities "6944699408 a" and "7043724150 a" have been removed.
Everything still goes through.
val build_lp_out :
  string * int *
  ((Lpproc.branchnbound list * Lpproc.branchnbound list *
    Lpproc.branchnbound list * Lpproc.branchnbound list *
    Lpproc.branchnbound list) *
   Lpproc.branchnbound list list * string) *
  string =
  ("Mon Jul 29 14:50:39 EDT 2013\n", 62748,
   (([], [], [], [], []),
    [[]; []; []; []; []; []; []; []; []; []; []; []; []; []; []],
    "finished output"),
   "Mon Jul 29 20:31:03 EDT 2013\n")

*)