legacy/oldnonlinear/nonlinear/ineq_cell23.hl

   1 (* ========================================================================== *)
   2 (* FLYSPECK - BOOK FORMALIZATION                                              *)
   3 (*                                                                            *)
   4 (* Chapter: Nonlinear                                                  *)
   5 (* Author: Thomas C. Hales                                                    *)
   6 (* Date: 2012-06-15                                                           *)
   7 (* ========================================================================== *)
   8
   9
  10 (* Oct 2012. thales.
  11 This looks like junk.  Can it be deleted?
  12 *)
  13
  14 Functional_equation.functional_overload();;
  15
  16
  17
  18 module Ineq_cell23 = struct
  19   open Sphere;;
  20   open Ineq;;
  21 end;;
  22
  23 let newcases = ["QZECFIC wt1";
  24  "QZECFIC wt2";
  25  "GRKIBMP";
  26  "RQWUDDU";
  27  "TEWNSCJ";
  28  "TXQTPVC";
  29  "PEMKWKU";
  30  "FHBVYXZv2 a";
  31  "GLFVCVK4 2477216213 y4supercrit";
  32  "GLFVCVK4 2477216213 y4crit";
  33  "GLFVCVK4 2477216213 y4subcrit";
  34  "QITNPEAv2 4003532128"];;
  35
  36
  37 let execute_interval bool =
  38   let cases = [
  39  "GRKIBMP";
  40  ] in
  41   map (fun t -> try (Auto_lib.testsplit bool t) with Failure _ -> [()]) cases;;
  42
  43 type_of `dih4_x_div_sqrtdelta_posbranch`;;
  44 Auto_lib.testsplit true "GRKIBMP";;
  45 execute_interval true;;
  46
  47 let idq = hd (Ineq.getexact "GLFVCVK4 2477216213 y4crit");;
  48   let splits = Optimize.preprocess_split_idq idq;;
  49  (fun (s,tags,testineq) -> Auto_lib.execute_interval true tags s testineq) (List.nth splits 7);;
  50 let testsplit_idq ex idq =
  51   let splits = Optimize.preprocess_split_idq idq in
  52     map (fun (s,tags,testineq) -> execute_interval ex tags s testineq) splits;;
  53
  54 cfsqp newcases;;
  55
  56 one_cfsqp "QZECFIC wt1";;
  57 one_cfsqp "QZECFIC wt2";;
  58 one_cfsqp "GRKIBMP";;
  59 one_cfsqp "RQWUDDU";;
  60 one_cfsqp "TEWNSCJ";;
  61 one_cfsqp "TXQTPVC";;
  62 one_cfsqp "PEMKWKU";;
  63 one_cfsqp "FHBVYXZv2 a";;
  64 one_cfsqp "GLFVCVK4 2477216213 y4supercrit";;
  65 one_cfsqp "GLFVCVK4 2477216213 y4crit";;
  66 one_cfsqp "GLFVCVK4 2477216213 y4subcrit";;
  67 one_cfsqp "QITNPEAv2 4003532128";;