1 (* Title: HOL/Matrix/CplexMatrixConverter.ML |
|
2 Author: Steven Obua |
|
3 *) |
|
4 |
|
5 signature MATRIX_BUILDER = |
|
6 sig |
|
7 type vector |
|
8 type matrix |
|
9 |
|
10 val empty_vector : vector |
|
11 val empty_matrix : matrix |
|
12 |
|
13 exception Nat_expected of int |
|
14 val set_elem : vector -> int -> string -> vector |
|
15 val set_vector : matrix -> int -> vector -> matrix |
|
16 end; |
|
17 |
|
18 signature CPLEX_MATRIX_CONVERTER = |
|
19 sig |
|
20 structure cplex : CPLEX |
|
21 structure matrix_builder : MATRIX_BUILDER |
|
22 type vector = matrix_builder.vector |
|
23 type matrix = matrix_builder.matrix |
|
24 type naming = int * (int -> string) * (string -> int) |
|
25 |
|
26 exception Converter of string |
|
27 |
|
28 (* program must fulfill is_normed_cplexProg and must be an element of the image of elim_nonfree_bounds *) |
|
29 (* convert_prog maximize c A b naming *) |
|
30 val convert_prog : cplex.cplexProg -> bool * vector * matrix * vector * naming |
|
31 |
|
32 (* results must be optimal, converts_results returns the optimal value as string and the solution as vector *) |
|
33 (* convert_results results name2index *) |
|
34 val convert_results : cplex.cplexResult -> (string -> int) -> string * vector |
|
35 end; |
|
36 |
|
37 functor MAKE_CPLEX_MATRIX_CONVERTER (structure cplex: CPLEX and matrix_builder: MATRIX_BUILDER) : CPLEX_MATRIX_CONVERTER = |
|
38 struct |
|
39 |
|
40 structure cplex = cplex |
|
41 structure matrix_builder = matrix_builder |
|
42 type matrix = matrix_builder.matrix |
|
43 type vector = matrix_builder.vector |
|
44 type naming = int * (int -> string) * (string -> int) |
|
45 |
|
46 open matrix_builder |
|
47 open cplex |
|
48 |
|
49 exception Converter of string; |
|
50 |
|
51 fun neg_term (cplexNeg t) = t |
|
52 | neg_term (cplexSum ts) = cplexSum (map neg_term ts) |
|
53 | neg_term t = cplexNeg t |
|
54 |
|
55 fun convert_prog (cplexProg (_, goal, constrs, bounds)) = |
|
56 let |
|
57 fun build_naming index i2s s2i [] = (index, i2s, s2i) |
|
58 | build_naming index i2s s2i (cplexBounds (cplexNeg cplexInf, cplexLeq, cplexVar v, cplexLeq, cplexInf)::bounds) |
|
59 = build_naming (index+1) (Inttab.update (index, v) i2s) (Symtab.update_new (v, index) s2i) bounds |
|
60 | build_naming _ _ _ _ = raise (Converter "nonfree bound") |
|
61 |
|
62 val (varcount, i2s_tab, s2i_tab) = build_naming 0 Inttab.empty Symtab.empty bounds |
|
63 |
|
64 fun i2s i = case Inttab.lookup i2s_tab i of NONE => raise (Converter "index not found") |
|
65 | SOME n => n |
|
66 fun s2i s = case Symtab.lookup s2i_tab s of NONE => raise (Converter ("name not found: "^s)) |
|
67 | SOME i => i |
|
68 fun num2str positive (cplexNeg t) = num2str (not positive) t |
|
69 | num2str positive (cplexNum num) = if positive then num else "-"^num |
|
70 | num2str _ _ = raise (Converter "term is not a (possibly signed) number") |
|
71 |
|
72 fun setprod vec positive (cplexNeg t) = setprod vec (not positive) t |
|
73 | setprod vec positive (cplexVar v) = set_elem vec (s2i v) (if positive then "1" else "-1") |
|
74 | setprod vec positive (cplexProd (cplexNum num, cplexVar v)) = |
|
75 set_elem vec (s2i v) (if positive then num else "-"^num) |
|
76 | setprod _ _ _ = raise (Converter "term is not a normed product") |
|
77 |
|
78 fun sum2vec (cplexSum ts) = fold (fn t => fn vec => setprod vec true t) ts empty_vector |
|
79 | sum2vec t = setprod empty_vector true t |
|
80 |
|
81 fun constrs2Ab j A b [] = (A, b) |
|
82 | constrs2Ab j A b ((_, cplexConstr (cplexLeq, (t1,t2)))::cs) = |
|
83 constrs2Ab (j+1) (set_vector A j (sum2vec t1)) (set_elem b j (num2str true t2)) cs |
|
84 | constrs2Ab j A b ((_, cplexConstr (cplexGeq, (t1,t2)))::cs) = |
|
85 constrs2Ab (j+1) (set_vector A j (sum2vec (neg_term t1))) (set_elem b j (num2str true (neg_term t2))) cs |
|
86 | constrs2Ab j A b ((_, cplexConstr (cplexEq, (t1,t2)))::cs) = |
|
87 constrs2Ab j A b ((NONE, cplexConstr (cplexLeq, (t1,t2))):: |
|
88 (NONE, cplexConstr (cplexGeq, (t1, t2)))::cs) |
|
89 | constrs2Ab _ _ _ _ = raise (Converter "no strict constraints allowed") |
|
90 |
|
91 val (A, b) = constrs2Ab 0 empty_matrix empty_vector constrs |
|
92 |
|
93 val (goal_maximize, goal_term) = |
|
94 case goal of |
|
95 (cplexMaximize t) => (true, t) |
|
96 | (cplexMinimize t) => (false, t) |
|
97 in |
|
98 (goal_maximize, sum2vec goal_term, A, b, (varcount, i2s, s2i)) |
|
99 end |
|
100 |
|
101 fun convert_results (cplex.Optimal (opt, entries)) name2index = |
|
102 let |
|
103 fun setv (name, value) v = matrix_builder.set_elem v (name2index name) value |
|
104 in |
|
105 (opt, fold setv entries (matrix_builder.empty_vector)) |
|
106 end |
|
107 | convert_results _ _ = raise (Converter "No optimal result") |
|
108 |
|
109 end; |
|
110 |
|
111 structure SimpleMatrixBuilder : MATRIX_BUILDER = |
|
112 struct |
|
113 type vector = (int * string) list |
|
114 type matrix = (int * vector) list |
|
115 |
|
116 val empty_matrix = [] |
|
117 val empty_vector = [] |
|
118 |
|
119 exception Nat_expected of int; |
|
120 |
|
121 fun set_elem v i s = v @ [(i, s)] |
|
122 |
|
123 fun set_vector m i v = m @ [(i, v)] |
|
124 |
|
125 end; |
|
126 |
|
127 structure SimpleCplexMatrixConverter = |
|
128 MAKE_CPLEX_MATRIX_CONVERTER(structure cplex = Cplex and matrix_builder = SimpleMatrixBuilder); |
|