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