src/HOL/Matrix/CplexMatrixConverter.ML
author wenzelm
Fri Dec 17 17:43:54 2010 +0100 (2010-12-17)
changeset 41229 d797baa3d57c
parent 37788 261c61fabc98
child 46531 eff798e48efc
permissions -rw-r--r--
replaced command 'nonterminals' by slightly modernized version 'nonterminal';
     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 (s, 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);