author | obua |
Thu, 07 Jun 2007 17:21:43 +0200 | |
changeset 23293 | 77577fc2f141 |
parent 22964 | 2284e0d02e7f |
child 23665 | 825bea0266db |
permissions | -rw-r--r-- |
20787
406d990006af
moved Matrix/cplex/MatrixLP.ML to Matrix/cplex/matrixlp.ML;
wenzelm
parents:
diff
changeset
|
1 |
(* Title: HOL/Matrix/cplex/MatrixLP.ML |
406d990006af
moved Matrix/cplex/MatrixLP.ML to Matrix/cplex/matrixlp.ML;
wenzelm
parents:
diff
changeset
|
2 |
ID: $Id$ |
406d990006af
moved Matrix/cplex/MatrixLP.ML to Matrix/cplex/matrixlp.ML;
wenzelm
parents:
diff
changeset
|
3 |
Author: Steven Obua |
406d990006af
moved Matrix/cplex/MatrixLP.ML to Matrix/cplex/matrixlp.ML;
wenzelm
parents:
diff
changeset
|
4 |
*) |
406d990006af
moved Matrix/cplex/MatrixLP.ML to Matrix/cplex/matrixlp.ML;
wenzelm
parents:
diff
changeset
|
5 |
|
406d990006af
moved Matrix/cplex/MatrixLP.ML to Matrix/cplex/matrixlp.ML;
wenzelm
parents:
diff
changeset
|
6 |
signature MATRIX_LP = |
406d990006af
moved Matrix/cplex/MatrixLP.ML to Matrix/cplex/matrixlp.ML;
wenzelm
parents:
diff
changeset
|
7 |
sig |
406d990006af
moved Matrix/cplex/MatrixLP.ML to Matrix/cplex/matrixlp.ML;
wenzelm
parents:
diff
changeset
|
8 |
val lp_dual_estimate_prt : string -> int -> thm |
406d990006af
moved Matrix/cplex/MatrixLP.ML to Matrix/cplex/matrixlp.ML;
wenzelm
parents:
diff
changeset
|
9 |
val lp_dual_estimate_prt_primitive : |
406d990006af
moved Matrix/cplex/MatrixLP.ML to Matrix/cplex/matrixlp.ML;
wenzelm
parents:
diff
changeset
|
10 |
cterm * (cterm * cterm) * (cterm * cterm) * cterm * (cterm * cterm) -> thm |
406d990006af
moved Matrix/cplex/MatrixLP.ML to Matrix/cplex/matrixlp.ML;
wenzelm
parents:
diff
changeset
|
11 |
val matrix_compute : cterm -> thm |
406d990006af
moved Matrix/cplex/MatrixLP.ML to Matrix/cplex/matrixlp.ML;
wenzelm
parents:
diff
changeset
|
12 |
val matrix_simplify : thm -> thm |
406d990006af
moved Matrix/cplex/MatrixLP.ML to Matrix/cplex/matrixlp.ML;
wenzelm
parents:
diff
changeset
|
13 |
val prove_bound : string -> int -> thm |
406d990006af
moved Matrix/cplex/MatrixLP.ML to Matrix/cplex/matrixlp.ML;
wenzelm
parents:
diff
changeset
|
14 |
val float2real : string * string -> Real.real |
406d990006af
moved Matrix/cplex/MatrixLP.ML to Matrix/cplex/matrixlp.ML;
wenzelm
parents:
diff
changeset
|
15 |
end |
406d990006af
moved Matrix/cplex/MatrixLP.ML to Matrix/cplex/matrixlp.ML;
wenzelm
parents:
diff
changeset
|
16 |
|
406d990006af
moved Matrix/cplex/MatrixLP.ML to Matrix/cplex/matrixlp.ML;
wenzelm
parents:
diff
changeset
|
17 |
structure MatrixLP : MATRIX_LP = |
406d990006af
moved Matrix/cplex/MatrixLP.ML to Matrix/cplex/matrixlp.ML;
wenzelm
parents:
diff
changeset
|
18 |
struct |
406d990006af
moved Matrix/cplex/MatrixLP.ML to Matrix/cplex/matrixlp.ML;
wenzelm
parents:
diff
changeset
|
19 |
|
406d990006af
moved Matrix/cplex/MatrixLP.ML to Matrix/cplex/matrixlp.ML;
wenzelm
parents:
diff
changeset
|
20 |
fun inst_real thm = |
406d990006af
moved Matrix/cplex/MatrixLP.ML to Matrix/cplex/matrixlp.ML;
wenzelm
parents:
diff
changeset
|
21 |
let val certT = ctyp_of (Thm.theory_of_thm thm) in |
406d990006af
moved Matrix/cplex/MatrixLP.ML to Matrix/cplex/matrixlp.ML;
wenzelm
parents:
diff
changeset
|
22 |
standard (Thm.instantiate |
406d990006af
moved Matrix/cplex/MatrixLP.ML to Matrix/cplex/matrixlp.ML;
wenzelm
parents:
diff
changeset
|
23 |
([(certT (TVar (hd (term_tvars (prop_of thm)))), certT HOLogic.realT)], []) thm) |
406d990006af
moved Matrix/cplex/MatrixLP.ML to Matrix/cplex/matrixlp.ML;
wenzelm
parents:
diff
changeset
|
24 |
end |
406d990006af
moved Matrix/cplex/MatrixLP.ML to Matrix/cplex/matrixlp.ML;
wenzelm
parents:
diff
changeset
|
25 |
|
22964 | 26 |
val spm_mult_le_dual_prts_no_let = thm "SparseMatrix.spm_mult_le_dual_prts_no_let"; |
27 |
val cert = cterm_of (Thm.theory_of_thm spm_mult_le_dual_prts_no_let); |
|
20787
406d990006af
moved Matrix/cplex/MatrixLP.ML to Matrix/cplex/matrixlp.ML;
wenzelm
parents:
diff
changeset
|
28 |
|
406d990006af
moved Matrix/cplex/MatrixLP.ML to Matrix/cplex/matrixlp.ML;
wenzelm
parents:
diff
changeset
|
29 |
fun lp_dual_estimate_prt_primitive (y, (A1, A2), (c1, c2), b, (r1, r2)) = |
406d990006af
moved Matrix/cplex/MatrixLP.ML to Matrix/cplex/matrixlp.ML;
wenzelm
parents:
diff
changeset
|
30 |
let |
406d990006af
moved Matrix/cplex/MatrixLP.ML to Matrix/cplex/matrixlp.ML;
wenzelm
parents:
diff
changeset
|
31 |
val th = inst_real spm_mult_le_dual_prts_no_let |
22964 | 32 |
fun var s x = (cert (Var ((s,0), FloatSparseMatrixBuilder.spmatT)), x) |
20787
406d990006af
moved Matrix/cplex/MatrixLP.ML to Matrix/cplex/matrixlp.ML;
wenzelm
parents:
diff
changeset
|
33 |
val th = Thm.instantiate ([], [var "A1" A1, var "A2" A2, var "y" y, var "c1" c1, var "c2" c2, |
406d990006af
moved Matrix/cplex/MatrixLP.ML to Matrix/cplex/matrixlp.ML;
wenzelm
parents:
diff
changeset
|
34 |
var "r1" r1, var "r2" r2, var "b" b]) th |
406d990006af
moved Matrix/cplex/MatrixLP.ML to Matrix/cplex/matrixlp.ML;
wenzelm
parents:
diff
changeset
|
35 |
in th end |
406d990006af
moved Matrix/cplex/MatrixLP.ML to Matrix/cplex/matrixlp.ML;
wenzelm
parents:
diff
changeset
|
36 |
|
406d990006af
moved Matrix/cplex/MatrixLP.ML to Matrix/cplex/matrixlp.ML;
wenzelm
parents:
diff
changeset
|
37 |
fun lp_dual_estimate_prt lptfile prec = |
406d990006af
moved Matrix/cplex/MatrixLP.ML to Matrix/cplex/matrixlp.ML;
wenzelm
parents:
diff
changeset
|
38 |
let |
406d990006af
moved Matrix/cplex/MatrixLP.ML to Matrix/cplex/matrixlp.ML;
wenzelm
parents:
diff
changeset
|
39 |
val certificate = |
406d990006af
moved Matrix/cplex/MatrixLP.ML to Matrix/cplex/matrixlp.ML;
wenzelm
parents:
diff
changeset
|
40 |
let |
22964 | 41 |
open Fspmlp |
20787
406d990006af
moved Matrix/cplex/MatrixLP.ML to Matrix/cplex/matrixlp.ML;
wenzelm
parents:
diff
changeset
|
42 |
val l = load lptfile prec false |
406d990006af
moved Matrix/cplex/MatrixLP.ML to Matrix/cplex/matrixlp.ML;
wenzelm
parents:
diff
changeset
|
43 |
in |
22964 | 44 |
(y l |> cert, A l |> pairself cert, c l |> pairself cert, b l |> cert, r12 l |> pairself cert) |
20787
406d990006af
moved Matrix/cplex/MatrixLP.ML to Matrix/cplex/matrixlp.ML;
wenzelm
parents:
diff
changeset
|
45 |
end |
406d990006af
moved Matrix/cplex/MatrixLP.ML to Matrix/cplex/matrixlp.ML;
wenzelm
parents:
diff
changeset
|
46 |
in |
406d990006af
moved Matrix/cplex/MatrixLP.ML to Matrix/cplex/matrixlp.ML;
wenzelm
parents:
diff
changeset
|
47 |
lp_dual_estimate_prt_primitive certificate |
406d990006af
moved Matrix/cplex/MatrixLP.ML to Matrix/cplex/matrixlp.ML;
wenzelm
parents:
diff
changeset
|
48 |
end |
406d990006af
moved Matrix/cplex/MatrixLP.ML to Matrix/cplex/matrixlp.ML;
wenzelm
parents:
diff
changeset
|
49 |
|
406d990006af
moved Matrix/cplex/MatrixLP.ML to Matrix/cplex/matrixlp.ML;
wenzelm
parents:
diff
changeset
|
50 |
fun is_meta_eq th = |
406d990006af
moved Matrix/cplex/MatrixLP.ML to Matrix/cplex/matrixlp.ML;
wenzelm
parents:
diff
changeset
|
51 |
let |
406d990006af
moved Matrix/cplex/MatrixLP.ML to Matrix/cplex/matrixlp.ML;
wenzelm
parents:
diff
changeset
|
52 |
fun check ((Const ("==", _)) $ _ $ _) = true |
406d990006af
moved Matrix/cplex/MatrixLP.ML to Matrix/cplex/matrixlp.ML;
wenzelm
parents:
diff
changeset
|
53 |
| check _ = false |
406d990006af
moved Matrix/cplex/MatrixLP.ML to Matrix/cplex/matrixlp.ML;
wenzelm
parents:
diff
changeset
|
54 |
in |
406d990006af
moved Matrix/cplex/MatrixLP.ML to Matrix/cplex/matrixlp.ML;
wenzelm
parents:
diff
changeset
|
55 |
check (concl_of th) |
406d990006af
moved Matrix/cplex/MatrixLP.ML to Matrix/cplex/matrixlp.ML;
wenzelm
parents:
diff
changeset
|
56 |
end |
406d990006af
moved Matrix/cplex/MatrixLP.ML to Matrix/cplex/matrixlp.ML;
wenzelm
parents:
diff
changeset
|
57 |
|
22964 | 58 |
fun prep ths = filter is_meta_eq ths @ map (standard o mk_meta_eq) (filter_out is_meta_eq ths) |
20787
406d990006af
moved Matrix/cplex/MatrixLP.ML to Matrix/cplex/matrixlp.ML;
wenzelm
parents:
diff
changeset
|
59 |
|
406d990006af
moved Matrix/cplex/MatrixLP.ML to Matrix/cplex/matrixlp.ML;
wenzelm
parents:
diff
changeset
|
60 |
fun inst_tvar ty thm = |
406d990006af
moved Matrix/cplex/MatrixLP.ML to Matrix/cplex/matrixlp.ML;
wenzelm
parents:
diff
changeset
|
61 |
let |
406d990006af
moved Matrix/cplex/MatrixLP.ML to Matrix/cplex/matrixlp.ML;
wenzelm
parents:
diff
changeset
|
62 |
val certT = Thm.ctyp_of (Thm.theory_of_thm thm); |
406d990006af
moved Matrix/cplex/MatrixLP.ML to Matrix/cplex/matrixlp.ML;
wenzelm
parents:
diff
changeset
|
63 |
val ord = prod_ord (prod_ord string_ord int_ord) (list_ord string_ord) |
406d990006af
moved Matrix/cplex/MatrixLP.ML to Matrix/cplex/matrixlp.ML;
wenzelm
parents:
diff
changeset
|
64 |
val v = TVar (hd (sort ord (term_tvars (prop_of thm)))) |
406d990006af
moved Matrix/cplex/MatrixLP.ML to Matrix/cplex/matrixlp.ML;
wenzelm
parents:
diff
changeset
|
65 |
in |
406d990006af
moved Matrix/cplex/MatrixLP.ML to Matrix/cplex/matrixlp.ML;
wenzelm
parents:
diff
changeset
|
66 |
standard (Thm.instantiate ([(certT v, certT ty)], []) thm) |
406d990006af
moved Matrix/cplex/MatrixLP.ML to Matrix/cplex/matrixlp.ML;
wenzelm
parents:
diff
changeset
|
67 |
end |
406d990006af
moved Matrix/cplex/MatrixLP.ML to Matrix/cplex/matrixlp.ML;
wenzelm
parents:
diff
changeset
|
68 |
|
406d990006af
moved Matrix/cplex/MatrixLP.ML to Matrix/cplex/matrixlp.ML;
wenzelm
parents:
diff
changeset
|
69 |
fun inst_tvars [] thms = thms |
406d990006af
moved Matrix/cplex/MatrixLP.ML to Matrix/cplex/matrixlp.ML;
wenzelm
parents:
diff
changeset
|
70 |
| inst_tvars (ty::tys) thms = inst_tvars tys (map (inst_tvar ty) thms) |
406d990006af
moved Matrix/cplex/MatrixLP.ML to Matrix/cplex/matrixlp.ML;
wenzelm
parents:
diff
changeset
|
71 |
|
406d990006af
moved Matrix/cplex/MatrixLP.ML to Matrix/cplex/matrixlp.ML;
wenzelm
parents:
diff
changeset
|
72 |
val matrix_compute = |
406d990006af
moved Matrix/cplex/MatrixLP.ML to Matrix/cplex/matrixlp.ML;
wenzelm
parents:
diff
changeset
|
73 |
let |
22964 | 74 |
val spvecT = FloatSparseMatrixBuilder.spvecT |
75 |
val spmatT = FloatSparseMatrixBuilder.spmatT |
|
20787
406d990006af
moved Matrix/cplex/MatrixLP.ML to Matrix/cplex/matrixlp.ML;
wenzelm
parents:
diff
changeset
|
76 |
val spvecT_elem = HOLogic.mk_prodT (HOLogic.natT, HOLogic.realT) |
406d990006af
moved Matrix/cplex/MatrixLP.ML to Matrix/cplex/matrixlp.ML;
wenzelm
parents:
diff
changeset
|
77 |
val spmatT_elem = HOLogic.mk_prodT (HOLogic.natT, spvecT) |
406d990006af
moved Matrix/cplex/MatrixLP.ML to Matrix/cplex/matrixlp.ML;
wenzelm
parents:
diff
changeset
|
78 |
val case_compute = map thm ["list_case_compute", "list_case_compute_empty", "list_case_compute_cons"] |
406d990006af
moved Matrix/cplex/MatrixLP.ML to Matrix/cplex/matrixlp.ML;
wenzelm
parents:
diff
changeset
|
79 |
val ths = |
406d990006af
moved Matrix/cplex/MatrixLP.ML to Matrix/cplex/matrixlp.ML;
wenzelm
parents:
diff
changeset
|
80 |
prep ( |
406d990006af
moved Matrix/cplex/MatrixLP.ML to Matrix/cplex/matrixlp.ML;
wenzelm
parents:
diff
changeset
|
81 |
(inst_tvars [HOLogic.intT, HOLogic.natT] (thms "Let_compute")) |
406d990006af
moved Matrix/cplex/MatrixLP.ML to Matrix/cplex/matrixlp.ML;
wenzelm
parents:
diff
changeset
|
82 |
@ (inst_tvars [HOLogic.intT, HOLogic.intT] (thms "Let_compute")) |
406d990006af
moved Matrix/cplex/MatrixLP.ML to Matrix/cplex/matrixlp.ML;
wenzelm
parents:
diff
changeset
|
83 |
@ (map (fn t => inst_tvar t (thm "If_True")) [HOLogic.intT, HOLogic.natT, HOLogic.realT, spvecT, spmatT, HOLogic.boolT]) |
406d990006af
moved Matrix/cplex/MatrixLP.ML to Matrix/cplex/matrixlp.ML;
wenzelm
parents:
diff
changeset
|
84 |
@ (map (fn t => inst_tvar t (thm "If_False")) [HOLogic.intT, HOLogic.natT, HOLogic.realT, spvecT, spmatT, HOLogic.boolT]) |
406d990006af
moved Matrix/cplex/MatrixLP.ML to Matrix/cplex/matrixlp.ML;
wenzelm
parents:
diff
changeset
|
85 |
@ (thms "MatrixLP.float_arith") |
406d990006af
moved Matrix/cplex/MatrixLP.ML to Matrix/cplex/matrixlp.ML;
wenzelm
parents:
diff
changeset
|
86 |
@ (map (inst_tvar HOLogic.realT) (thms "MatrixLP.sparse_row_matrix_arith_simps")) |
406d990006af
moved Matrix/cplex/MatrixLP.ML to Matrix/cplex/matrixlp.ML;
wenzelm
parents:
diff
changeset
|
87 |
@ (thms "MatrixLP.boolarith") |
406d990006af
moved Matrix/cplex/MatrixLP.ML to Matrix/cplex/matrixlp.ML;
wenzelm
parents:
diff
changeset
|
88 |
@ (inst_tvars [HOLogic.natT, HOLogic.realT] [thm "fst_compute", thm "snd_compute"]) |
22964 | 89 |
@ (inst_tvars [HOLogic.natT, FloatSparseMatrixBuilder.spvecT] [thm "fst_compute", thm "snd_compute"]) |
20787
406d990006af
moved Matrix/cplex/MatrixLP.ML to Matrix/cplex/matrixlp.ML;
wenzelm
parents:
diff
changeset
|
90 |
@ (inst_tvars [HOLogic.boolT, spmatT_elem] case_compute) |
406d990006af
moved Matrix/cplex/MatrixLP.ML to Matrix/cplex/matrixlp.ML;
wenzelm
parents:
diff
changeset
|
91 |
@ (inst_tvars [HOLogic.boolT, spvecT_elem] case_compute) |
406d990006af
moved Matrix/cplex/MatrixLP.ML to Matrix/cplex/matrixlp.ML;
wenzelm
parents:
diff
changeset
|
92 |
@ (inst_tvars [HOLogic.boolT, HOLogic.realT] case_compute) |
406d990006af
moved Matrix/cplex/MatrixLP.ML to Matrix/cplex/matrixlp.ML;
wenzelm
parents:
diff
changeset
|
93 |
@ (inst_tvars [spvecT] (thms "MatrixLP.sorted_sp_simps")) |
406d990006af
moved Matrix/cplex/MatrixLP.ML to Matrix/cplex/matrixlp.ML;
wenzelm
parents:
diff
changeset
|
94 |
@ (inst_tvars [HOLogic.realT] (thms "MatrixLP.sorted_sp_simps")) |
406d990006af
moved Matrix/cplex/MatrixLP.ML to Matrix/cplex/matrixlp.ML;
wenzelm
parents:
diff
changeset
|
95 |
@ [thm "zero_eq_Numeral0_nat", thm "one_eq_Numeral1_nat"] |
406d990006af
moved Matrix/cplex/MatrixLP.ML to Matrix/cplex/matrixlp.ML;
wenzelm
parents:
diff
changeset
|
96 |
@ (inst_tvars [HOLogic.intT] [thm "zero_eq_Numeral0_nring", thm "one_eq_Numeral1_nring"]) |
406d990006af
moved Matrix/cplex/MatrixLP.ML to Matrix/cplex/matrixlp.ML;
wenzelm
parents:
diff
changeset
|
97 |
@ (inst_tvars [HOLogic.realT] [thm "zero_eq_Numeral0_nring", thm "one_eq_Numeral1_nring"])) |
406d990006af
moved Matrix/cplex/MatrixLP.ML to Matrix/cplex/matrixlp.ML;
wenzelm
parents:
diff
changeset
|
98 |
|
406d990006af
moved Matrix/cplex/MatrixLP.ML to Matrix/cplex/matrixlp.ML;
wenzelm
parents:
diff
changeset
|
99 |
val c = Compute.basic_make (the_context ()) ths |
406d990006af
moved Matrix/cplex/MatrixLP.ML to Matrix/cplex/matrixlp.ML;
wenzelm
parents:
diff
changeset
|
100 |
in |
406d990006af
moved Matrix/cplex/MatrixLP.ML to Matrix/cplex/matrixlp.ML;
wenzelm
parents:
diff
changeset
|
101 |
Compute.rewrite c |
406d990006af
moved Matrix/cplex/MatrixLP.ML to Matrix/cplex/matrixlp.ML;
wenzelm
parents:
diff
changeset
|
102 |
end |
406d990006af
moved Matrix/cplex/MatrixLP.ML to Matrix/cplex/matrixlp.ML;
wenzelm
parents:
diff
changeset
|
103 |
|
406d990006af
moved Matrix/cplex/MatrixLP.ML to Matrix/cplex/matrixlp.ML;
wenzelm
parents:
diff
changeset
|
104 |
fun matrix_simplify th = |
406d990006af
moved Matrix/cplex/MatrixLP.ML to Matrix/cplex/matrixlp.ML;
wenzelm
parents:
diff
changeset
|
105 |
let |
406d990006af
moved Matrix/cplex/MatrixLP.ML to Matrix/cplex/matrixlp.ML;
wenzelm
parents:
diff
changeset
|
106 |
val simp_th = matrix_compute (cprop_of th) |
406d990006af
moved Matrix/cplex/MatrixLP.ML to Matrix/cplex/matrixlp.ML;
wenzelm
parents:
diff
changeset
|
107 |
val th = strip_shyps (equal_elim simp_th th) |
406d990006af
moved Matrix/cplex/MatrixLP.ML to Matrix/cplex/matrixlp.ML;
wenzelm
parents:
diff
changeset
|
108 |
fun removeTrue th = removeTrue (implies_elim th TrueI) handle _ => th |
406d990006af
moved Matrix/cplex/MatrixLP.ML to Matrix/cplex/matrixlp.ML;
wenzelm
parents:
diff
changeset
|
109 |
in |
406d990006af
moved Matrix/cplex/MatrixLP.ML to Matrix/cplex/matrixlp.ML;
wenzelm
parents:
diff
changeset
|
110 |
removeTrue th |
406d990006af
moved Matrix/cplex/MatrixLP.ML to Matrix/cplex/matrixlp.ML;
wenzelm
parents:
diff
changeset
|
111 |
end |
406d990006af
moved Matrix/cplex/MatrixLP.ML to Matrix/cplex/matrixlp.ML;
wenzelm
parents:
diff
changeset
|
112 |
|
406d990006af
moved Matrix/cplex/MatrixLP.ML to Matrix/cplex/matrixlp.ML;
wenzelm
parents:
diff
changeset
|
113 |
fun prove_bound lptfile prec = |
406d990006af
moved Matrix/cplex/MatrixLP.ML to Matrix/cplex/matrixlp.ML;
wenzelm
parents:
diff
changeset
|
114 |
let |
406d990006af
moved Matrix/cplex/MatrixLP.ML to Matrix/cplex/matrixlp.ML;
wenzelm
parents:
diff
changeset
|
115 |
val th = lp_dual_estimate_prt lptfile prec |
406d990006af
moved Matrix/cplex/MatrixLP.ML to Matrix/cplex/matrixlp.ML;
wenzelm
parents:
diff
changeset
|
116 |
in |
406d990006af
moved Matrix/cplex/MatrixLP.ML to Matrix/cplex/matrixlp.ML;
wenzelm
parents:
diff
changeset
|
117 |
matrix_simplify th |
406d990006af
moved Matrix/cplex/MatrixLP.ML to Matrix/cplex/matrixlp.ML;
wenzelm
parents:
diff
changeset
|
118 |
end |
406d990006af
moved Matrix/cplex/MatrixLP.ML to Matrix/cplex/matrixlp.ML;
wenzelm
parents:
diff
changeset
|
119 |
|
406d990006af
moved Matrix/cplex/MatrixLP.ML to Matrix/cplex/matrixlp.ML;
wenzelm
parents:
diff
changeset
|
120 |
val realFromStr = the o Real.fromString; |
406d990006af
moved Matrix/cplex/MatrixLP.ML to Matrix/cplex/matrixlp.ML;
wenzelm
parents:
diff
changeset
|
121 |
fun float2real (x, y) = realFromStr x * Math.pow (2.0, realFromStr y); |
406d990006af
moved Matrix/cplex/MatrixLP.ML to Matrix/cplex/matrixlp.ML;
wenzelm
parents:
diff
changeset
|
122 |
|
406d990006af
moved Matrix/cplex/MatrixLP.ML to Matrix/cplex/matrixlp.ML;
wenzelm
parents:
diff
changeset
|
123 |
end |