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