37788

1 
(* Title: HOL/Matrix/CplexMatrixConverter.ML

16784

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

22951

12 

16784

13 
exception Nat_expected of int

22951

14 
val set_elem : vector > int > string > vector

16784

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

22951

43 
type vector = matrix_builder.vector

16784

44 
type naming = int * (int > string) * (string > int)

22951

45 

16784

46 
open matrix_builder


47 
open cplex

22951

48 

16784

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

22951

54 

46531

55 
fun convert_prog (cplexProg (_, goal, constrs, bounds)) =

22951

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")

16784

61 

22951

62 
val (varcount, i2s_tab, s2i_tab) = build_naming 0 Inttab.empty Symtab.empty bounds

16784

63 

22951

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")

16784

71 

22951

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")

16784

77 

33245

78 
fun sum2vec (cplexSum ts) = fold (fn t => fn vec => setprod vec true t) ts empty_vector

22951

79 
 sum2vec t = setprod empty_vector true t

16784

80 

22951

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")

16784

90 

22951

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))

16784

99 
end


100 


101 
fun convert_results (cplex.Optimal (opt, entries)) name2index =


102 
let

33245

103 
fun setv (name, value) v = matrix_builder.set_elem v (name2index name) value

16784

104 
in

33245

105 
(opt, fold setv entries (matrix_builder.empty_vector))

16784

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 

22951

125 
end;

16784

126 

22951

127 
structure SimpleCplexMatrixConverter =


128 
MAKE_CPLEX_MATRIX_CONVERTER(structure cplex = Cplex and matrix_builder = SimpleMatrixBuilder);
