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