src/HOL/Matrix_LP/Cplex_tools.ML
author blanchet
Wed Feb 12 08:35:57 2014 +0100 (2014-02-12)
changeset 55415 05f5fdb8d093
parent 51940 958d439b3013
child 62505 9e2a65912111
permissions -rw-r--r--
renamed 'nat_{case,rec}' to '{case,rec}_nat'
wenzelm@47455
     1
(*  Title:      HOL/Matrix_LP/Cplex_tools.ML
obua@16784
     2
    Author:     Steven Obua
wenzelm@51940
     3
wenzelm@51940
     4
Relevant Isabelle environment settings:
wenzelm@51940
     5
wenzelm@51940
     6
  # LP_SOLVER is the default solver. It can be changed during runtime via Cplex.set_solver.
wenzelm@51940
     7
  # First option: use the commercial cplex solver
wenzelm@51940
     8
  #LP_SOLVER=CPLEX
wenzelm@51940
     9
  #CPLEX_PATH=cplex
wenzelm@51940
    10
  # Second option: use the open source glpk solver
wenzelm@51940
    11
  #LP_SOLVER=GLPK
wenzelm@51940
    12
  #GLPK_PATH=glpsol
obua@16784
    13
*)
obua@16784
    14
obua@16784
    15
signature CPLEX =
obua@16784
    16
sig
haftmann@22951
    17
haftmann@22951
    18
    datatype cplexTerm = cplexVar of string | cplexNum of string | cplexInf
haftmann@22951
    19
                       | cplexNeg of cplexTerm
haftmann@22951
    20
                       | cplexProd of cplexTerm * cplexTerm
haftmann@22951
    21
                       | cplexSum of (cplexTerm list)
haftmann@22951
    22
haftmann@22951
    23
    datatype cplexComp = cplexLe | cplexLeq | cplexEq | cplexGe | cplexGeq
haftmann@22951
    24
haftmann@22951
    25
    datatype cplexGoal = cplexMinimize of cplexTerm
haftmann@22951
    26
               | cplexMaximize of cplexTerm
haftmann@22951
    27
haftmann@22951
    28
    datatype cplexConstr = cplexConstr of cplexComp *
haftmann@22951
    29
                      (cplexTerm * cplexTerm)
haftmann@22951
    30
haftmann@22951
    31
    datatype cplexBounds = cplexBounds of cplexTerm * cplexComp * cplexTerm
haftmann@22951
    32
                      * cplexComp * cplexTerm
haftmann@22951
    33
             | cplexBound of cplexTerm * cplexComp * cplexTerm
haftmann@22951
    34
haftmann@22951
    35
    datatype cplexProg = cplexProg of string
haftmann@22951
    36
                      * cplexGoal
haftmann@22951
    37
                      * ((string option * cplexConstr)
haftmann@22951
    38
                         list)
haftmann@22951
    39
                      * cplexBounds list
haftmann@22951
    40
haftmann@22951
    41
    datatype cplexResult = Unbounded
haftmann@22951
    42
             | Infeasible
haftmann@22951
    43
             | Undefined
haftmann@22951
    44
             | Optimal of string *
haftmann@22951
    45
                      (((* name *) string *
haftmann@22951
    46
                    (* value *) string) list)
obua@16966
    47
obua@16966
    48
    datatype cplexSolver = SOLVER_DEFAULT | SOLVER_CPLEX | SOLVER_GLPK
haftmann@22951
    49
obua@16784
    50
    exception Load_cplexFile of string
obua@16784
    51
    exception Load_cplexResult of string
obua@16784
    52
    exception Save_cplexFile of string
obua@16784
    53
    exception Execute of string
obua@16784
    54
obua@16784
    55
    val load_cplexFile : string -> cplexProg
obua@16784
    56
haftmann@22951
    57
    val save_cplexFile : string -> cplexProg -> unit
obua@16784
    58
obua@16784
    59
    val elim_nonfree_bounds : cplexProg -> cplexProg
obua@16784
    60
obua@16784
    61
    val relax_strict_ineqs : cplexProg -> cplexProg
obua@16784
    62
obua@16784
    63
    val is_normed_cplexProg : cplexProg -> bool
obua@16784
    64
obua@16966
    65
    val get_solver : unit -> cplexSolver
obua@16966
    66
    val set_solver : cplexSolver -> unit
obua@16784
    67
    val solve : cplexProg -> cplexResult
obua@16784
    68
end;
obua@16784
    69
obua@16784
    70
structure Cplex  : CPLEX =
obua@16784
    71
struct
obua@16784
    72
obua@16966
    73
datatype cplexSolver = SOLVER_DEFAULT | SOLVER_CPLEX | SOLVER_GLPK
obua@16966
    74
wenzelm@32740
    75
val cplexsolver = Unsynchronized.ref SOLVER_DEFAULT;
obua@16966
    76
fun get_solver () = !cplexsolver;
obua@16966
    77
fun set_solver s = (cplexsolver := s);
obua@16966
    78
obua@16784
    79
exception Load_cplexFile of string;
obua@16784
    80
exception Load_cplexResult of string;
obua@16784
    81
exception Save_cplexFile of string;
haftmann@22951
    82
haftmann@22951
    83
datatype cplexTerm = cplexVar of string
haftmann@22951
    84
           | cplexNum of string
haftmann@22951
    85
           | cplexInf
haftmann@22951
    86
                   | cplexNeg of cplexTerm
haftmann@22951
    87
                   | cplexProd of cplexTerm * cplexTerm
haftmann@22951
    88
                   | cplexSum of (cplexTerm list)
haftmann@22951
    89
datatype cplexComp = cplexLe | cplexLeq | cplexEq | cplexGe | cplexGeq
obua@16784
    90
datatype cplexGoal = cplexMinimize of cplexTerm | cplexMaximize of cplexTerm
obua@16784
    91
datatype cplexConstr = cplexConstr of cplexComp * (cplexTerm * cplexTerm)
haftmann@22951
    92
datatype cplexBounds = cplexBounds of cplexTerm * cplexComp * cplexTerm
haftmann@22951
    93
                      * cplexComp * cplexTerm
haftmann@22951
    94
                     | cplexBound of cplexTerm * cplexComp * cplexTerm
haftmann@22951
    95
datatype cplexProg = cplexProg of string
haftmann@22951
    96
                  * cplexGoal
haftmann@22951
    97
                  * ((string option * cplexConstr) list)
haftmann@22951
    98
                  * cplexBounds list
haftmann@22951
    99
obua@16784
   100
fun rev_cmp cplexLe = cplexGe
obua@16784
   101
  | rev_cmp cplexLeq = cplexGeq
obua@16784
   102
  | rev_cmp cplexGe = cplexLe
obua@16784
   103
  | rev_cmp cplexGeq = cplexLeq
obua@16784
   104
  | rev_cmp cplexEq = cplexEq
obua@16784
   105
obua@16784
   106
fun the NONE = raise (Load_cplexFile "SOME expected")
haftmann@22951
   107
  | the (SOME x) = x;
haftmann@22951
   108
obua@16784
   109
fun modulo_signed is_something (cplexNeg u) = is_something u
obua@16784
   110
  | modulo_signed is_something u = is_something u
obua@16784
   111
obua@16784
   112
fun is_Num (cplexNum _) = true
obua@16784
   113
  | is_Num _ = false
obua@16784
   114
obua@16784
   115
fun is_Inf cplexInf = true
obua@16784
   116
  | is_Inf _ = false
obua@16784
   117
obua@16784
   118
fun is_Var (cplexVar _) = true
obua@16784
   119
  | is_Var _ = false
obua@16784
   120
haftmann@46531
   121
fun is_Neg (cplexNeg _) = true
obua@16784
   122
  | is_Neg _ = false
obua@16784
   123
haftmann@22951
   124
fun is_normed_Prod (cplexProd (t1, t2)) =
obua@16784
   125
    (is_Num t1) andalso (is_Var t2)
obua@16784
   126
  | is_normed_Prod x = is_Var x
obua@16784
   127
haftmann@22951
   128
fun is_normed_Sum (cplexSum ts) =
obua@16784
   129
    (ts <> []) andalso forall (modulo_signed is_normed_Prod) ts
obua@16784
   130
  | is_normed_Sum x = modulo_signed is_normed_Prod x
obua@16784
   131
haftmann@46531
   132
fun is_normed_Constr (cplexConstr (_, (t1, t2))) =
obua@16784
   133
    (is_normed_Sum t1) andalso (modulo_signed is_Num t2)
obua@16784
   134
obua@16784
   135
fun is_Num_or_Inf x = is_Inf x orelse is_Num x
obua@16784
   136
obua@16784
   137
fun is_normed_Bounds (cplexBounds (t1, c1, t2, c2, t3)) =
haftmann@22951
   138
    (c1 = cplexLe orelse c1 = cplexLeq) andalso
obua@16784
   139
    (c2 = cplexLe orelse c2 = cplexLeq) andalso
obua@16784
   140
    is_Var t2 andalso
obua@16784
   141
    modulo_signed is_Num_or_Inf t1 andalso
obua@16784
   142
    modulo_signed is_Num_or_Inf t3
obua@16784
   143
  | is_normed_Bounds (cplexBound (t1, c, t2)) =
haftmann@22951
   144
    (is_Var t1 andalso (modulo_signed is_Num_or_Inf t2))
obua@16784
   145
    orelse
haftmann@22951
   146
    (c <> cplexEq andalso
obua@16784
   147
     is_Var t2 andalso (modulo_signed is_Num_or_Inf t1))
haftmann@22951
   148
obua@16784
   149
fun term_of_goal (cplexMinimize x) = x
obua@16784
   150
  | term_of_goal (cplexMaximize x) = x
obua@16784
   151
haftmann@46531
   152
fun is_normed_cplexProg (cplexProg (_, goal, constraints, bounds)) =
obua@16784
   153
    is_normed_Sum (term_of_goal goal) andalso
obua@16784
   154
    forall (fn (_,x) => is_normed_Constr x) constraints andalso
obua@16784
   155
    forall is_normed_Bounds bounds
obua@16784
   156
obua@16784
   157
fun is_NL s = s = "\n"
obua@16784
   158
obua@16784
   159
fun is_blank s = forall (fn c => c <> #"\n" andalso Char.isSpace c) (String.explode s)
haftmann@22951
   160
haftmann@22951
   161
fun is_num a =
haftmann@22951
   162
    let
haftmann@22951
   163
    val b = String.explode a
haftmann@22951
   164
    fun num4 cs = forall Char.isDigit cs
haftmann@22951
   165
    fun num3 [] = true
haftmann@22951
   166
      | num3 (ds as (c::cs)) =
haftmann@22951
   167
        if c = #"+" orelse c = #"-" then
haftmann@22951
   168
        num4 cs
haftmann@22951
   169
        else
haftmann@22951
   170
        num4 ds
haftmann@22951
   171
    fun num2 [] = true
haftmann@22951
   172
      | num2 (c::cs) =
haftmann@22951
   173
        if c = #"e" orelse c = #"E" then num3 cs
haftmann@22951
   174
        else (Char.isDigit c) andalso num2 cs
haftmann@22951
   175
    fun num1 [] = true
haftmann@22951
   176
      | num1 (c::cs) =
haftmann@22951
   177
        if c = #"." then num2 cs
haftmann@22951
   178
        else if c = #"e" orelse c = #"E" then num3 cs
haftmann@22951
   179
        else (Char.isDigit c) andalso num1 cs
haftmann@22951
   180
    fun num [] = true
haftmann@22951
   181
      | num (c::cs) =
haftmann@22951
   182
        if c = #"." then num2 cs
haftmann@22951
   183
        else (Char.isDigit c) andalso num1 cs
obua@16784
   184
    in
haftmann@22951
   185
    num b
haftmann@22951
   186
    end
obua@16784
   187
obua@16784
   188
fun is_delimiter s = s = "+" orelse s = "-" orelse s = ":"
obua@16784
   189
haftmann@22951
   190
fun is_cmp s = s = "<" orelse s = ">" orelse s = "<="
haftmann@22951
   191
             orelse s = ">=" orelse s = "="
haftmann@22951
   192
haftmann@22951
   193
fun is_symbol a =
obua@16784
   194
    let
haftmann@22951
   195
    val symbol_char = String.explode "!\"#$%&()/,.;?@_`'{}|~"
haftmann@22951
   196
    fun is_symbol_char c = Char.isAlphaNum c orelse
haftmann@22951
   197
                   exists (fn d => d=c) symbol_char
haftmann@22951
   198
    fun is_symbol_start c = is_symbol_char c andalso
haftmann@22951
   199
                not (Char.isDigit c) andalso
haftmann@22951
   200
                not (c= #".")
haftmann@22951
   201
    val b = String.explode a
obua@16784
   202
    in
haftmann@22951
   203
    b <> [] andalso is_symbol_start (hd b) andalso
haftmann@22951
   204
    forall is_symbol_char b
obua@16784
   205
    end
obua@16784
   206
obua@16784
   207
fun to_upper s = String.implode (map Char.toUpper (String.explode s))
obua@16784
   208
haftmann@22951
   209
fun keyword x =
haftmann@22951
   210
    let
haftmann@22951
   211
    val a = to_upper x
obua@16784
   212
    in
haftmann@22951
   213
    if a = "BOUNDS" orelse a = "BOUND" then
haftmann@22951
   214
        SOME "BOUNDS"
haftmann@22951
   215
    else if a = "MINIMIZE" orelse a = "MINIMUM" orelse a = "MIN" then
haftmann@22951
   216
        SOME "MINIMIZE"
haftmann@22951
   217
    else if a = "MAXIMIZE" orelse a = "MAXIMUM" orelse a = "MAX" then
haftmann@22951
   218
        SOME "MAXIMIZE"
haftmann@22951
   219
    else if a = "ST" orelse a = "S.T." orelse a = "ST." then
haftmann@22951
   220
        SOME "ST"
haftmann@22951
   221
    else if a = "FREE" orelse a = "END" then
haftmann@22951
   222
        SOME a
haftmann@22951
   223
    else if a = "GENERAL" orelse a = "GENERALS" orelse a = "GEN" then
haftmann@22951
   224
        SOME "GENERAL"
haftmann@22951
   225
    else if a = "INTEGER" orelse a = "INTEGERS" orelse a = "INT" then
haftmann@22951
   226
        SOME "INTEGER"
haftmann@22951
   227
    else if a = "BINARY" orelse a = "BINARIES" orelse a = "BIN" then
haftmann@22951
   228
        SOME "BINARY"
haftmann@22951
   229
    else if a = "INF" orelse a = "INFINITY" then
haftmann@22951
   230
        SOME "INF"
haftmann@22951
   231
    else
haftmann@22951
   232
        NONE
obua@16784
   233
    end
haftmann@22951
   234
obua@16784
   235
val TOKEN_ERROR = ~1
obua@16784
   236
val TOKEN_BLANK = 0
obua@16784
   237
val TOKEN_NUM = 1
obua@16784
   238
val TOKEN_DELIMITER = 2
obua@16784
   239
val TOKEN_SYMBOL = 3
obua@16784
   240
val TOKEN_LABEL = 4
obua@16784
   241
val TOKEN_CMP = 5
obua@16784
   242
val TOKEN_KEYWORD = 6
obua@16784
   243
val TOKEN_NL = 7
haftmann@22951
   244
obua@16784
   245
(* tokenize takes a list of chars as argument and returns a list of
haftmann@22951
   246
   int * string pairs, each string representing a "cplex token",
obua@16784
   247
   and each int being one of TOKEN_NUM, TOKEN_DELIMITER, TOKEN_CMP
obua@16784
   248
   or TOKEN_SYMBOL *)
haftmann@22951
   249
fun tokenize s =
obua@16784
   250
    let
haftmann@22951
   251
    val flist = [(is_NL, TOKEN_NL),
haftmann@22951
   252
             (is_blank, TOKEN_BLANK),
haftmann@22951
   253
             (is_num, TOKEN_NUM),
haftmann@22951
   254
                     (is_delimiter, TOKEN_DELIMITER),
haftmann@22951
   255
             (is_cmp, TOKEN_CMP),
haftmann@22951
   256
             (is_symbol, TOKEN_SYMBOL)]
haftmann@46531
   257
    fun match_helper [] s = (fn _ => false, TOKEN_ERROR)
haftmann@22951
   258
      | match_helper (f::fs) s =
haftmann@22951
   259
        if ((fst f) s) then f else match_helper fs s
haftmann@22951
   260
    fun match s = match_helper flist s
haftmann@22951
   261
    fun tok s =
haftmann@22951
   262
        if s = "" then [] else
haftmann@22951
   263
        let
haftmann@22951
   264
        val h = String.substring (s,0,1)
haftmann@22951
   265
        val (f, j) = match h
haftmann@22951
   266
        fun len i =
haftmann@22951
   267
            if size s = i then i
haftmann@22951
   268
            else if f (String.substring (s,0,i+1)) then
haftmann@22951
   269
            len (i+1)
haftmann@22951
   270
            else i
haftmann@22951
   271
        in
haftmann@22951
   272
        if j < 0 then
haftmann@22951
   273
            (if h = "\\" then []
haftmann@22951
   274
             else raise (Load_cplexFile ("token expected, found: "
haftmann@22951
   275
                         ^s)))
haftmann@22951
   276
        else
haftmann@22951
   277
            let
haftmann@22951
   278
            val l = len 1
haftmann@22951
   279
            val u = String.substring (s,0,l)
haftmann@22951
   280
            val v = String.extract (s,l,NONE)
haftmann@22951
   281
            in
haftmann@22951
   282
            if j = 0 then tok v else (j, u) :: tok v
haftmann@22951
   283
            end
haftmann@22951
   284
        end
obua@16784
   285
    in
haftmann@22951
   286
    tok s
obua@16784
   287
    end
obua@16784
   288
obua@16784
   289
exception Tokenize of string;
obua@16784
   290
haftmann@22951
   291
fun tokenize_general flist s =
obua@16784
   292
    let
haftmann@22951
   293
    fun match_helper [] s = raise (Tokenize s)
haftmann@22951
   294
      | match_helper (f::fs) s =
haftmann@22951
   295
        if ((fst f) s) then f else match_helper fs s
haftmann@22951
   296
    fun match s = match_helper flist s
haftmann@22951
   297
    fun tok s =
haftmann@22951
   298
        if s = "" then [] else
haftmann@22951
   299
        let
haftmann@22951
   300
        val h = String.substring (s,0,1)
haftmann@22951
   301
        val (f, j) = match h
haftmann@22951
   302
        fun len i =
haftmann@22951
   303
            if size s = i then i
haftmann@22951
   304
            else if f (String.substring (s,0,i+1)) then
haftmann@22951
   305
            len (i+1)
haftmann@22951
   306
            else i
haftmann@22951
   307
        val l = len 1
haftmann@22951
   308
        in
haftmann@22951
   309
        (j, String.substring (s,0,l)) :: tok (String.extract (s,l,NONE))
haftmann@22951
   310
        end
obua@16784
   311
    in
haftmann@22951
   312
    tok s
obua@16784
   313
    end
obua@16784
   314
haftmann@22951
   315
fun load_cplexFile name =
haftmann@22951
   316
    let
haftmann@22951
   317
    val f = TextIO.openIn name
wenzelm@32740
   318
        val ignore_NL = Unsynchronized.ref true
wenzelm@32740
   319
    val rest = Unsynchronized.ref []
haftmann@22951
   320
haftmann@22951
   321
    fun is_symbol s c = (fst c) = TOKEN_SYMBOL andalso (to_upper (snd c)) = s
obua@16784
   322
haftmann@22951
   323
    fun readToken_helper () =
haftmann@22951
   324
        if length (!rest) > 0 then
haftmann@22951
   325
        let val u = hd (!rest) in
haftmann@22951
   326
            (
haftmann@22951
   327
             rest := tl (!rest);
haftmann@22951
   328
             SOME u
haftmann@22951
   329
            )
haftmann@22951
   330
        end
haftmann@22951
   331
        else
wenzelm@23139
   332
          (case TextIO.inputLine f of
wenzelm@23139
   333
            NONE => NONE
wenzelm@23139
   334
          | SOME s =>
haftmann@22951
   335
            let val t = tokenize s in
haftmann@22951
   336
            if (length t >= 2 andalso
haftmann@22951
   337
                snd(hd (tl t)) = ":")
haftmann@22951
   338
            then
haftmann@22951
   339
                rest := (TOKEN_LABEL, snd (hd t)) :: (tl (tl t))
haftmann@22951
   340
            else if (length t >= 2) andalso is_symbol "SUBJECT" (hd (t))
haftmann@22951
   341
                andalso is_symbol "TO" (hd (tl t))
haftmann@22951
   342
            then
haftmann@22951
   343
                rest := (TOKEN_SYMBOL, "ST") :: (tl (tl t))
haftmann@22951
   344
            else
haftmann@22951
   345
                rest := t;
haftmann@22951
   346
            readToken_helper ()
wenzelm@23139
   347
            end)
haftmann@22951
   348
haftmann@22951
   349
    fun readToken_helper2 () =
haftmann@22951
   350
        let val c = readToken_helper () in
haftmann@22951
   351
            if c = NONE then NONE
obua@16784
   352
                    else if !ignore_NL andalso fst (the c) = TOKEN_NL then
haftmann@22951
   353
            readToken_helper2 ()
haftmann@22951
   354
            else if fst (the c) = TOKEN_SYMBOL
haftmann@22951
   355
                andalso keyword (snd (the c)) <> NONE
haftmann@22951
   356
            then SOME (TOKEN_KEYWORD, the (keyword (snd (the c))))
haftmann@22951
   357
            else c
haftmann@22951
   358
        end
haftmann@22951
   359
haftmann@22951
   360
    fun readToken () = readToken_helper2 ()
haftmann@22951
   361
haftmann@22951
   362
    fun pushToken a = rest := (a::(!rest))
haftmann@22951
   363
haftmann@22951
   364
    fun is_value token =
haftmann@22951
   365
        fst token = TOKEN_NUM orelse (fst token = TOKEN_KEYWORD
haftmann@22951
   366
                      andalso snd token = "INF")
haftmann@22951
   367
haftmann@22951
   368
        fun get_value token =
haftmann@22951
   369
        if fst token = TOKEN_NUM then
haftmann@22951
   370
        cplexNum (snd token)
haftmann@22951
   371
        else if fst token = TOKEN_KEYWORD andalso snd token = "INF"
haftmann@22951
   372
        then
haftmann@22951
   373
        cplexInf
haftmann@22951
   374
        else
haftmann@22951
   375
        raise (Load_cplexFile "num expected")
obua@16784
   376
haftmann@22951
   377
    fun readTerm_Product only_num =
haftmann@22951
   378
        let val c = readToken () in
haftmann@22951
   379
        if c = NONE then NONE
haftmann@22951
   380
        else if fst (the c) = TOKEN_SYMBOL
haftmann@22951
   381
        then (
haftmann@22951
   382
            if only_num then (pushToken (the c); NONE)
haftmann@22951
   383
            else SOME (cplexVar (snd (the c)))
haftmann@22951
   384
            )
haftmann@22951
   385
        else if only_num andalso is_value (the c) then
haftmann@22951
   386
            SOME (get_value (the c))
haftmann@22951
   387
        else if is_value (the c) then
haftmann@22951
   388
            let val t1 = get_value (the c)
haftmann@22951
   389
            val d = readToken ()
haftmann@22951
   390
            in
haftmann@22951
   391
            if d = NONE then SOME t1
haftmann@22951
   392
            else if fst (the d) = TOKEN_SYMBOL then
haftmann@22951
   393
                SOME (cplexProd (t1, cplexVar (snd (the d))))
haftmann@22951
   394
            else
haftmann@22951
   395
                (pushToken (the d); SOME t1)
haftmann@22951
   396
            end
haftmann@22951
   397
        else (pushToken (the c); NONE)
haftmann@22951
   398
        end
haftmann@22951
   399
haftmann@22951
   400
    fun readTerm_Signed only_signed only_num =
haftmann@22951
   401
        let
haftmann@22951
   402
        val c = readToken ()
haftmann@22951
   403
        in
haftmann@22951
   404
        if c = NONE then NONE
haftmann@22951
   405
        else
haftmann@22951
   406
            let val d = the c in
haftmann@22951
   407
            if d = (TOKEN_DELIMITER, "+") then
haftmann@22951
   408
                readTerm_Product only_num
haftmann@22951
   409
             else if d = (TOKEN_DELIMITER, "-") then
haftmann@22951
   410
                 SOME (cplexNeg (the (readTerm_Product
haftmann@22951
   411
                              only_num)))
haftmann@22951
   412
             else (pushToken d;
haftmann@22951
   413
                   if only_signed then NONE
haftmann@22951
   414
                   else readTerm_Product only_num)
haftmann@22951
   415
            end
haftmann@22951
   416
        end
haftmann@22951
   417
haftmann@22951
   418
    fun readTerm_Sum first_signed =
haftmann@22951
   419
        let val c = readTerm_Signed first_signed false in
haftmann@22951
   420
        if c = NONE then [] else (the c)::(readTerm_Sum true)
haftmann@22951
   421
        end
haftmann@22951
   422
haftmann@22951
   423
    fun readTerm () =
haftmann@22951
   424
        let val c = readTerm_Sum false in
haftmann@22951
   425
        if c = [] then NONE
haftmann@22951
   426
        else if tl c = [] then SOME (hd c)
haftmann@22951
   427
        else SOME (cplexSum c)
haftmann@22951
   428
        end
haftmann@22951
   429
haftmann@22951
   430
    fun readLabeledTerm () =
haftmann@22951
   431
        let val c = readToken () in
haftmann@22951
   432
        if c = NONE then (NONE, NONE)
haftmann@22951
   433
        else if fst (the c) = TOKEN_LABEL then
haftmann@22951
   434
            let val t = readTerm () in
haftmann@22951
   435
            if t = NONE then
haftmann@22951
   436
                raise (Load_cplexFile ("term after label "^
haftmann@22951
   437
                           (snd (the c))^
haftmann@22951
   438
                           " expected"))
haftmann@22951
   439
            else (SOME (snd (the c)), t)
haftmann@22951
   440
            end
haftmann@22951
   441
        else (pushToken (the c); (NONE, readTerm ()))
haftmann@22951
   442
        end
haftmann@22951
   443
haftmann@22951
   444
    fun readGoal () =
haftmann@22951
   445
        let
haftmann@22951
   446
        val g = readToken ()
haftmann@22951
   447
        in
haftmann@22951
   448
            if g = SOME (TOKEN_KEYWORD, "MAXIMIZE") then
haftmann@22951
   449
            cplexMaximize (the (snd (readLabeledTerm ())))
haftmann@22951
   450
        else if g = SOME (TOKEN_KEYWORD, "MINIMIZE") then
haftmann@22951
   451
            cplexMinimize (the (snd (readLabeledTerm ())))
haftmann@22951
   452
        else raise (Load_cplexFile "MAXIMIZE or MINIMIZE expected")
haftmann@22951
   453
        end
haftmann@22951
   454
haftmann@22951
   455
    fun str2cmp b =
haftmann@22951
   456
        (case b of
haftmann@22951
   457
         "<" => cplexLe
haftmann@22951
   458
           | "<=" => cplexLeq
haftmann@22951
   459
           | ">" => cplexGe
haftmann@22951
   460
           | ">=" => cplexGeq
obua@16784
   461
               | "=" => cplexEq
haftmann@22951
   462
           | _ => raise (Load_cplexFile (b^" is no TOKEN_CMP")))
haftmann@22951
   463
haftmann@22951
   464
    fun readConstraint () =
haftmann@22951
   465
            let
haftmann@22951
   466
        val t = readLabeledTerm ()
haftmann@22951
   467
        fun make_constraint b t1 t2 =
haftmann@22951
   468
                    cplexConstr
haftmann@22951
   469
            (str2cmp b,
haftmann@22951
   470
             (t1, t2))
haftmann@22951
   471
        in
haftmann@22951
   472
        if snd t = NONE then NONE
haftmann@22951
   473
        else
haftmann@22951
   474
            let val c = readToken () in
haftmann@22951
   475
            if c = NONE orelse fst (the c) <> TOKEN_CMP
haftmann@22951
   476
            then raise (Load_cplexFile "TOKEN_CMP expected")
haftmann@22951
   477
            else
haftmann@22951
   478
                let val n = readTerm_Signed false true in
haftmann@22951
   479
                if n = NONE then
haftmann@22951
   480
                    raise (Load_cplexFile "num expected")
haftmann@22951
   481
                else
haftmann@22951
   482
                    SOME (fst t,
haftmann@22951
   483
                      make_constraint (snd (the c))
haftmann@22951
   484
                              (the (snd t))
haftmann@22951
   485
                              (the n))
haftmann@22951
   486
                end
haftmann@22951
   487
            end
haftmann@22951
   488
        end
obua@16784
   489
haftmann@22951
   490
        fun readST () =
haftmann@22951
   491
        let
haftmann@22951
   492
        fun readbody () =
haftmann@22951
   493
            let val t = readConstraint () in
haftmann@22951
   494
            if t = NONE then []
haftmann@22951
   495
            else if (is_normed_Constr (snd (the t))) then
haftmann@22951
   496
                (the t)::(readbody ())
haftmann@22951
   497
            else if (fst (the t) <> NONE) then
haftmann@22951
   498
                raise (Load_cplexFile
haftmann@22951
   499
                       ("constraint '"^(the (fst (the t)))^
haftmann@22951
   500
                    "'is not normed"))
haftmann@22951
   501
            else
haftmann@22951
   502
                raise (Load_cplexFile
haftmann@22951
   503
                       "constraint is not normed")
haftmann@22951
   504
            end
haftmann@22951
   505
        in
haftmann@22951
   506
        if readToken () = SOME (TOKEN_KEYWORD, "ST")
haftmann@22951
   507
        then
haftmann@22951
   508
            readbody ()
haftmann@22951
   509
        else
haftmann@22951
   510
            raise (Load_cplexFile "ST expected")
haftmann@22951
   511
        end
haftmann@22951
   512
haftmann@22951
   513
    fun readCmp () =
haftmann@22951
   514
        let val c = readToken () in
haftmann@22951
   515
        if c = NONE then NONE
haftmann@22951
   516
        else if fst (the c) = TOKEN_CMP then
haftmann@22951
   517
            SOME (str2cmp (snd (the c)))
haftmann@22951
   518
        else (pushToken (the c); NONE)
haftmann@22951
   519
        end
haftmann@22951
   520
haftmann@22951
   521
    fun skip_NL () =
haftmann@22951
   522
        let val c = readToken () in
haftmann@22951
   523
        if c <> NONE andalso fst (the c) = TOKEN_NL then
haftmann@22951
   524
            skip_NL ()
haftmann@22951
   525
        else
haftmann@22951
   526
            (pushToken (the c); ())
haftmann@22951
   527
        end
haftmann@22951
   528
haftmann@22951
   529
    fun make_bounds c t1 t2 =
haftmann@22951
   530
        cplexBound (t1, c, t2)
obua@16784
   531
haftmann@22951
   532
    fun readBound () =
haftmann@22951
   533
        let
haftmann@22951
   534
        val _ = skip_NL ()
haftmann@22951
   535
        val t1 = readTerm ()
haftmann@22951
   536
        in
haftmann@22951
   537
        if t1 = NONE then NONE
haftmann@22951
   538
        else
haftmann@22951
   539
            let
haftmann@22951
   540
            val c1 = readCmp ()
haftmann@22951
   541
            in
haftmann@22951
   542
            if c1 = NONE then
haftmann@22951
   543
                let
haftmann@22951
   544
                val c = readToken ()
haftmann@22951
   545
                in
haftmann@22951
   546
                if c = SOME (TOKEN_KEYWORD, "FREE") then
haftmann@22951
   547
                    SOME (
haftmann@22951
   548
                    cplexBounds (cplexNeg cplexInf,
haftmann@22951
   549
                         cplexLeq,
haftmann@22951
   550
                         the t1,
haftmann@22951
   551
                         cplexLeq,
haftmann@22951
   552
                         cplexInf))
haftmann@22951
   553
                else
haftmann@22951
   554
                    raise (Load_cplexFile "FREE expected")
haftmann@22951
   555
                end
haftmann@22951
   556
            else
haftmann@22951
   557
                let
haftmann@22951
   558
                val t2 = readTerm ()
haftmann@22951
   559
                in
haftmann@22951
   560
                if t2 = NONE then
haftmann@22951
   561
                    raise (Load_cplexFile "term expected")
haftmann@22951
   562
                else
haftmann@22951
   563
                    let val c2 = readCmp () in
haftmann@22951
   564
                    if c2 = NONE then
haftmann@22951
   565
                        SOME (make_bounds (the c1)
haftmann@22951
   566
                                  (the t1)
haftmann@22951
   567
                                  (the t2))
haftmann@22951
   568
                    else
haftmann@22951
   569
                        SOME (
haftmann@22951
   570
                        cplexBounds (the t1,
haftmann@22951
   571
                             the c1,
haftmann@22951
   572
                             the t2,
haftmann@22951
   573
                             the c2,
haftmann@22951
   574
                             the (readTerm())))
haftmann@22951
   575
                    end
haftmann@22951
   576
                end
haftmann@22951
   577
            end
haftmann@22951
   578
        end
obua@16784
   579
haftmann@22951
   580
    fun readBounds () =
haftmann@22951
   581
        let
haftmann@46531
   582
        fun makestring _ = "?"
haftmann@22951
   583
        fun readbody () =
haftmann@22951
   584
            let
haftmann@22951
   585
            val b = readBound ()
haftmann@22951
   586
            in
haftmann@22951
   587
            if b = NONE then []
haftmann@22951
   588
            else if (is_normed_Bounds (the b)) then
haftmann@22951
   589
                (the b)::(readbody())
haftmann@22951
   590
            else (
haftmann@22951
   591
                raise (Load_cplexFile
haftmann@22951
   592
                       ("bounds are not normed in: "^
haftmann@22951
   593
                    (makestring (the b)))))
haftmann@22951
   594
            end
haftmann@22951
   595
        in
haftmann@22951
   596
        if readToken () = SOME (TOKEN_KEYWORD, "BOUNDS") then
haftmann@22951
   597
            readbody ()
haftmann@22951
   598
        else raise (Load_cplexFile "BOUNDS expected")
haftmann@22951
   599
        end
haftmann@22951
   600
haftmann@22951
   601
        fun readEnd () =
haftmann@22951
   602
        if readToken () = SOME (TOKEN_KEYWORD, "END") then ()
haftmann@22951
   603
        else raise (Load_cplexFile "END expected")
haftmann@22951
   604
haftmann@22951
   605
    val result_Goal = readGoal ()
haftmann@22951
   606
    val result_ST = readST ()
haftmann@22951
   607
    val _ =    ignore_NL := false
obua@16784
   608
        val result_Bounds = readBounds ()
obua@16784
   609
        val _ = ignore_NL := true
obua@16784
   610
        val _ = readEnd ()
haftmann@22951
   611
    val _ = TextIO.closeIn f
obua@16784
   612
    in
haftmann@22951
   613
    cplexProg (name, result_Goal, result_ST, result_Bounds)
obua@16784
   614
    end
obua@16784
   615
haftmann@46531
   616
fun save_cplexFile filename (cplexProg (_, goal, constraints, bounds)) =
obua@16784
   617
    let
haftmann@22951
   618
    val f = TextIO.openOut filename
haftmann@22951
   619
haftmann@22951
   620
    fun basic_write s = TextIO.output(f, s)
obua@16784
   621
wenzelm@32740
   622
    val linebuf = Unsynchronized.ref ""
haftmann@22951
   623
    fun buf_flushline s =
haftmann@22951
   624
        (basic_write (!linebuf);
haftmann@22951
   625
         basic_write "\n";
haftmann@22951
   626
         linebuf := s)
haftmann@22951
   627
    fun buf_add s = linebuf := (!linebuf) ^ s
obua@16784
   628
haftmann@22951
   629
    fun write s =
haftmann@22951
   630
        if (String.size s) + (String.size (!linebuf)) >= 250 then
haftmann@22951
   631
        buf_flushline ("    "^s)
haftmann@22951
   632
        else
haftmann@22951
   633
        buf_add s
obua@16784
   634
obua@16784
   635
        fun writeln s = (buf_add s; buf_flushline "")
haftmann@22951
   636
haftmann@22951
   637
    fun write_term (cplexVar x) = write x
haftmann@22951
   638
      | write_term (cplexNum x) = write x
haftmann@22951
   639
      | write_term cplexInf = write "inf"
haftmann@22951
   640
      | write_term (cplexProd (cplexNum "1", b)) = write_term b
haftmann@22951
   641
      | write_term (cplexProd (a, b)) =
haftmann@22951
   642
        (write_term a; write " "; write_term b)
obua@16784
   643
          | write_term (cplexNeg x) = (write " - "; write_term x)
obua@16784
   644
          | write_term (cplexSum ts) = write_terms ts
haftmann@22951
   645
    and write_terms [] = ()
haftmann@22951
   646
      | write_terms (t::ts) =
haftmann@22951
   647
        (if (not (is_Neg t)) then write " + " else ();
haftmann@22951
   648
         write_term t; write_terms ts)
haftmann@22951
   649
haftmann@22951
   650
    fun write_goal (cplexMaximize term) =
haftmann@22951
   651
        (writeln "MAXIMIZE"; write_term term; writeln "")
haftmann@22951
   652
      | write_goal (cplexMinimize term) =
haftmann@22951
   653
        (writeln "MINIMIZE"; write_term term; writeln "")
obua@16784
   654
haftmann@22951
   655
    fun write_cmp cplexLe = write "<"
haftmann@22951
   656
      | write_cmp cplexLeq = write "<="
haftmann@22951
   657
      | write_cmp cplexEq = write "="
haftmann@22951
   658
      | write_cmp cplexGe = write ">"
haftmann@22951
   659
      | write_cmp cplexGeq = write ">="
haftmann@22951
   660
haftmann@22951
   661
    fun write_constr (cplexConstr (cmp, (a,b))) =
haftmann@22951
   662
        (write_term a;
haftmann@22951
   663
         write " ";
haftmann@22951
   664
         write_cmp cmp;
haftmann@22951
   665
         write " ";
haftmann@22951
   666
         write_term b)
obua@16784
   667
haftmann@22951
   668
    fun write_constraints [] = ()
haftmann@22951
   669
      | write_constraints (c::cs) =
haftmann@22951
   670
        (if (fst c <> NONE)
haftmann@22951
   671
         then
haftmann@22951
   672
         (write (the (fst c)); write ": ")
haftmann@22951
   673
         else
haftmann@22951
   674
         ();
haftmann@22951
   675
         write_constr (snd c);
haftmann@22951
   676
         writeln "";
haftmann@22951
   677
         write_constraints cs)
obua@16784
   678
haftmann@22951
   679
    fun write_bounds [] = ()
haftmann@22951
   680
      | write_bounds ((cplexBounds (t1,c1,t2,c2,t3))::bs) =
haftmann@22951
   681
        ((if t1 = cplexNeg cplexInf andalso t3 = cplexInf
haftmann@22951
   682
         andalso (c1 = cplexLeq orelse c1 = cplexLe)
haftmann@22951
   683
         andalso (c2 = cplexLeq orelse c2 = cplexLe)
haftmann@22951
   684
          then
haftmann@22951
   685
          (write_term t2; write " free")
haftmann@22951
   686
          else
haftmann@22951
   687
          (write_term t1; write " "; write_cmp c1; write " ";
haftmann@22951
   688
           write_term t2; write " "; write_cmp c2; write " ";
haftmann@22951
   689
           write_term t3)
haftmann@22951
   690
         ); writeln ""; write_bounds bs)
haftmann@22951
   691
      | write_bounds ((cplexBound (t1, c, t2)) :: bs) =
haftmann@22951
   692
        (write_term t1; write " ";
haftmann@22951
   693
         write_cmp c; write " ";
haftmann@22951
   694
         write_term t2; writeln ""; write_bounds bs)
haftmann@22951
   695
haftmann@22951
   696
    val _ = write_goal goal
obua@16784
   697
        val _ = (writeln ""; writeln "ST")
haftmann@22951
   698
    val _ = write_constraints constraints
obua@16784
   699
        val _ = (writeln ""; writeln "BOUNDS")
haftmann@22951
   700
    val _ = write_bounds bounds
haftmann@22951
   701
        val _ = (writeln ""; writeln "END")
obua@16784
   702
        val _ = TextIO.closeOut f
obua@16784
   703
    in
haftmann@22951
   704
    ()
obua@16784
   705
    end
obua@16784
   706
haftmann@22951
   707
fun norm_Constr (constr as cplexConstr (c, (t1, t2))) =
haftmann@22951
   708
    if not (modulo_signed is_Num t2) andalso
haftmann@22951
   709
       modulo_signed is_Num t1
obua@16784
   710
    then
haftmann@22951
   711
    [cplexConstr (rev_cmp c, (t2, t1))]
obua@16784
   712
    else if (c = cplexLe orelse c = cplexLeq) andalso
haftmann@22951
   713
        (t1 = (cplexNeg cplexInf) orelse t2 = cplexInf)
haftmann@22951
   714
    then
haftmann@22951
   715
    []
obua@16784
   716
    else if (c = cplexGe orelse c = cplexGeq) andalso
haftmann@22951
   717
        (t1 = cplexInf orelse t2 = cplexNeg cplexInf)
obua@16784
   718
    then
haftmann@22951
   719
    []
obua@16784
   720
    else
haftmann@22951
   721
    [constr]
obua@16784
   722
obua@16784
   723
fun bound2constr (cplexBounds (t1,c1,t2,c2,t3)) =
obua@16784
   724
    (norm_Constr(cplexConstr (c1, (t1, t2))))
obua@16784
   725
    @ (norm_Constr(cplexConstr (c2, (t2, t3))))
obua@16784
   726
  | bound2constr (cplexBound (t1, cplexEq, t2)) =
obua@16784
   727
    (norm_Constr(cplexConstr (cplexLeq, (t1, t2))))
obua@16784
   728
    @ (norm_Constr(cplexConstr (cplexLeq, (t2, t1))))
haftmann@22951
   729
  | bound2constr (cplexBound (t1, c1, t2)) =
obua@16784
   730
    norm_Constr(cplexConstr (c1, (t1,t2)))
obua@16784
   731
obua@16784
   732
val emptyset = Symtab.empty
obua@16784
   733
wenzelm@17412
   734
fun singleton v = Symtab.update (v, ()) emptyset
obua@16784
   735
obua@16784
   736
fun merge a b = Symtab.merge (op =) (a, b)
obua@16784
   737
haftmann@21056
   738
fun mergemap f ts = fold (fn x => fn table => merge table (f x)) ts Symtab.empty
obua@16784
   739
wenzelm@37116
   740
fun diff a b = Symtab.fold (Symtab.delete_safe o fst) b a
haftmann@22951
   741
obua@16784
   742
fun collect_vars (cplexVar v) = singleton v
obua@16784
   743
  | collect_vars (cplexNeg t) = collect_vars t
haftmann@22951
   744
  | collect_vars (cplexProd (t1, t2)) =
obua@16784
   745
    merge (collect_vars t1) (collect_vars t2)
obua@16784
   746
  | collect_vars (cplexSum ts) = mergemap collect_vars ts
obua@16784
   747
  | collect_vars _ = emptyset
obua@16784
   748
obua@16784
   749
(* Eliminates all nonfree bounds from the linear program and produces an
haftmann@22951
   750
   equivalent program with only free bounds
obua@16784
   751
   IF for the input program P holds: is_normed_cplexProg P *)
obua@16784
   752
fun elim_nonfree_bounds (cplexProg (name, goal, constraints, bounds)) =
obua@16784
   753
    let
haftmann@46531
   754
    fun collect_constr_vars (_, cplexConstr (_, (t1,_))) =
haftmann@22951
   755
        (collect_vars t1)
haftmann@22951
   756
haftmann@22951
   757
    val cvars = merge (collect_vars (term_of_goal goal))
haftmann@22951
   758
              (mergemap collect_constr_vars constraints)
haftmann@22951
   759
haftmann@22951
   760
    fun collect_lower_bounded_vars
haftmann@46531
   761
        (cplexBounds (_, _, cplexVar v, _, _)) =
haftmann@22951
   762
        singleton v
haftmann@22951
   763
      |  collect_lower_bounded_vars
haftmann@22951
   764
         (cplexBound (_, cplexLe, cplexVar v)) =
haftmann@22951
   765
         singleton v
haftmann@22951
   766
      |  collect_lower_bounded_vars
haftmann@22951
   767
         (cplexBound (_, cplexLeq, cplexVar v)) =
haftmann@22951
   768
         singleton v
haftmann@22951
   769
      |  collect_lower_bounded_vars
haftmann@22951
   770
         (cplexBound (cplexVar v, cplexGe,_)) =
haftmann@22951
   771
         singleton v
haftmann@22951
   772
      |  collect_lower_bounded_vars
haftmann@22951
   773
         (cplexBound (cplexVar v, cplexGeq, _)) =
haftmann@22951
   774
         singleton v
haftmann@22951
   775
      | collect_lower_bounded_vars
haftmann@22951
   776
        (cplexBound (cplexVar v, cplexEq, _)) =
haftmann@22951
   777
        singleton v
haftmann@22951
   778
      |  collect_lower_bounded_vars _ = emptyset
haftmann@22951
   779
haftmann@22951
   780
    val lvars = mergemap collect_lower_bounded_vars bounds
haftmann@22951
   781
    val positive_vars = diff cvars lvars
haftmann@22951
   782
    val zero = cplexNum "0"
haftmann@22951
   783
haftmann@22951
   784
    fun make_pos_constr v =
haftmann@22951
   785
        (NONE, cplexConstr (cplexGeq, ((cplexVar v), zero)))
haftmann@22951
   786
haftmann@22951
   787
    fun make_free_bound v =
haftmann@22951
   788
        cplexBounds (cplexNeg cplexInf, cplexLeq,
haftmann@22951
   789
             cplexVar v, cplexLeq,
haftmann@22951
   790
             cplexInf)
haftmann@22951
   791
haftmann@22951
   792
    val pos_constrs = rev (Symtab.fold
haftmann@46531
   793
                  (fn (k, _) => cons (make_pos_constr k))
haftmann@22951
   794
                  positive_vars [])
haftmann@21056
   795
        val bound_constrs = map (pair NONE)
haftmann@22951
   796
                (maps bound2constr bounds)
haftmann@22951
   797
    val constraints' = constraints @ pos_constrs @ bound_constrs
haftmann@22951
   798
    val bounds' = rev (Symtab.fold (fn (v, _) => cons (make_free_bound v)) cvars []);
obua@16784
   799
    in
haftmann@22951
   800
    cplexProg (name, goal, constraints', bounds')
obua@16784
   801
    end
obua@16784
   802
haftmann@22951
   803
fun relax_strict_ineqs (cplexProg (name, goals, constrs, bounds)) =
obua@16784
   804
    let
haftmann@22951
   805
    fun relax cplexLe = cplexLeq
haftmann@22951
   806
      | relax cplexGe = cplexGeq
haftmann@22951
   807
      | relax x = x
haftmann@22951
   808
haftmann@22951
   809
    fun relax_constr (n, cplexConstr(c, (t1, t2))) =
haftmann@22951
   810
        (n, cplexConstr(relax c, (t1, t2)))
haftmann@22951
   811
haftmann@22951
   812
    fun relax_bounds (cplexBounds (t1, c1, t2, c2, t3)) =
haftmann@22951
   813
        cplexBounds (t1, relax c1, t2, relax c2, t3)
haftmann@22951
   814
      | relax_bounds (cplexBound (t1, c, t2)) =
haftmann@22951
   815
        cplexBound (t1, relax c, t2)
obua@16784
   816
    in
haftmann@22951
   817
    cplexProg (name,
haftmann@22951
   818
           goals,
haftmann@22951
   819
           map relax_constr constrs,
haftmann@22951
   820
           map relax_bounds bounds)
obua@16784
   821
    end
obua@16784
   822
haftmann@22951
   823
datatype cplexResult = Unbounded
haftmann@22951
   824
             | Infeasible
haftmann@22951
   825
             | Undefined
haftmann@22951
   826
             | Optimal of string * ((string * string) list)
obua@16784
   827
obua@16784
   828
fun is_separator x = forall (fn c => c = #"-") (String.explode x)
obua@16784
   829
obua@16784
   830
fun is_sign x = (x = "+" orelse x = "-")
obua@16784
   831
obua@16784
   832
fun is_colon x = (x = ":")
obua@16784
   833
haftmann@22951
   834
fun is_resultsymbol a =
obua@16784
   835
    let
haftmann@22951
   836
    val symbol_char = String.explode "!\"#$%&()/,.;?@_`'{}|~-"
haftmann@22951
   837
    fun is_symbol_char c = Char.isAlphaNum c orelse
haftmann@22951
   838
                   exists (fn d => d=c) symbol_char
haftmann@22951
   839
    fun is_symbol_start c = is_symbol_char c andalso
haftmann@22951
   840
                not (Char.isDigit c) andalso
haftmann@22951
   841
                not (c= #".") andalso
haftmann@22951
   842
                not (c= #"-")
haftmann@22951
   843
    val b = String.explode a
obua@16784
   844
    in
haftmann@22951
   845
    b <> [] andalso is_symbol_start (hd b) andalso
haftmann@22951
   846
    forall is_symbol_char b
obua@16784
   847
    end
obua@16784
   848
obua@16784
   849
val TOKEN_SIGN = 100
obua@16784
   850
val TOKEN_COLON = 101
obua@16784
   851
val TOKEN_SEPARATOR = 102
obua@16784
   852
haftmann@22951
   853
fun load_glpkResult name =
obua@16784
   854
    let
haftmann@22951
   855
    val flist = [(is_NL, TOKEN_NL),
haftmann@22951
   856
             (is_blank, TOKEN_BLANK),
haftmann@22951
   857
             (is_num, TOKEN_NUM),
haftmann@22951
   858
             (is_sign, TOKEN_SIGN),
obua@16784
   859
                     (is_colon, TOKEN_COLON),
haftmann@22951
   860
             (is_cmp, TOKEN_CMP),
haftmann@22951
   861
             (is_resultsymbol, TOKEN_SYMBOL),
haftmann@22951
   862
             (is_separator, TOKEN_SEPARATOR)]
haftmann@22951
   863
haftmann@22951
   864
    val tokenize = tokenize_general flist
haftmann@22951
   865
haftmann@22951
   866
    val f = TextIO.openIn name
haftmann@22951
   867
wenzelm@32740
   868
    val rest = Unsynchronized.ref []
obua@16784
   869
haftmann@22951
   870
    fun readToken_helper () =
haftmann@22951
   871
        if length (!rest) > 0 then
haftmann@22951
   872
        let val u = hd (!rest) in
haftmann@22951
   873
            (
haftmann@22951
   874
             rest := tl (!rest);
haftmann@22951
   875
             SOME u
haftmann@22951
   876
            )
haftmann@22951
   877
        end
haftmann@22951
   878
        else
wenzelm@23139
   879
        (case TextIO.inputLine f of
wenzelm@23139
   880
          NONE => NONE
wenzelm@23139
   881
        | SOME s => (rest := tokenize s; readToken_helper()))
obua@16784
   882
haftmann@22951
   883
    fun is_tt tok ty = (tok <> NONE andalso (fst (the tok)) = ty)
obua@16784
   884
haftmann@22951
   885
    fun pushToken a = if a = NONE then () else (rest := ((the a)::(!rest)))
obua@16784
   886
haftmann@22951
   887
    fun readToken () =
haftmann@22951
   888
        let val t = readToken_helper () in
haftmann@22951
   889
        if is_tt t TOKEN_BLANK then
haftmann@22951
   890
            readToken ()
haftmann@22951
   891
        else if is_tt t TOKEN_NL then
haftmann@22951
   892
            let val t2 = readToken_helper () in
haftmann@22951
   893
            if is_tt t2 TOKEN_SIGN then
haftmann@22951
   894
                (pushToken (SOME (TOKEN_SEPARATOR, "-")); t)
haftmann@22951
   895
            else
haftmann@22951
   896
                (pushToken t2; t)
haftmann@22951
   897
            end
haftmann@22951
   898
        else if is_tt t TOKEN_SIGN then
haftmann@22951
   899
            let val t2 = readToken_helper () in
haftmann@22951
   900
            if is_tt t2 TOKEN_NUM then
haftmann@22951
   901
                (SOME (TOKEN_NUM, (snd (the t))^(snd (the t2))))
haftmann@22951
   902
            else
haftmann@22951
   903
                (pushToken t2; t)
haftmann@22951
   904
            end
haftmann@22951
   905
        else
haftmann@22951
   906
            t
haftmann@22951
   907
        end
haftmann@22951
   908
haftmann@22951
   909
        fun readRestOfLine P =
haftmann@22951
   910
        let
haftmann@22951
   911
        val t = readToken ()
haftmann@22951
   912
        in
haftmann@22951
   913
        if is_tt t TOKEN_NL orelse t = NONE
haftmann@22951
   914
        then P
haftmann@22951
   915
        else readRestOfLine P
haftmann@22951
   916
        end
obua@16784
   917
haftmann@22951
   918
    fun readHeader () =
haftmann@22951
   919
        let
haftmann@22951
   920
        fun readStatus () = readRestOfLine ("STATUS", snd (the (readToken ())))
haftmann@22951
   921
        fun readObjective () = readRestOfLine ("OBJECTIVE", snd (the (readToken (); readToken (); readToken ())))
haftmann@22951
   922
        val t1 = readToken ()
haftmann@22951
   923
        val t2 = readToken ()
haftmann@22951
   924
        in
haftmann@22951
   925
        if is_tt t1 TOKEN_SYMBOL andalso is_tt t2 TOKEN_COLON
haftmann@22951
   926
        then
haftmann@22951
   927
            case to_upper (snd (the t1)) of
haftmann@22951
   928
            "STATUS" => (readStatus ())::(readHeader ())
haftmann@22951
   929
              | "OBJECTIVE" => (readObjective())::(readHeader ())
haftmann@22951
   930
              | _ => (readRestOfLine (); readHeader ())
haftmann@22951
   931
        else
haftmann@22951
   932
            (pushToken t2; pushToken t1; [])
haftmann@22951
   933
        end
obua@16784
   934
haftmann@22951
   935
    fun skip_until_sep () =
haftmann@22951
   936
        let val x = readToken () in
haftmann@22951
   937
        if is_tt x TOKEN_SEPARATOR then
haftmann@22951
   938
            readRestOfLine ()
haftmann@22951
   939
        else
haftmann@22951
   940
            skip_until_sep ()
haftmann@22951
   941
        end
obua@16784
   942
haftmann@22951
   943
    fun load_value () =
haftmann@22951
   944
        let
haftmann@22951
   945
        val t1 = readToken ()
haftmann@22951
   946
        val t2 = readToken ()
haftmann@22951
   947
        in
haftmann@22951
   948
        if is_tt t1 TOKEN_NUM andalso is_tt t2 TOKEN_SYMBOL then
haftmann@22951
   949
            let
haftmann@22951
   950
            val t = readToken ()
haftmann@22951
   951
            val state = if is_tt t TOKEN_NL then readToken () else t
haftmann@22951
   952
            val _ = if is_tt state TOKEN_SYMBOL then () else raise (Load_cplexResult "state expected")
haftmann@22951
   953
            val k = readToken ()
haftmann@22951
   954
            in
haftmann@22951
   955
            if is_tt k TOKEN_NUM then
haftmann@22951
   956
                readRestOfLine (SOME (snd (the t2), snd (the k)))
haftmann@22951
   957
            else
haftmann@22951
   958
                raise (Load_cplexResult "number expected")
haftmann@22951
   959
            end
haftmann@22951
   960
        else
haftmann@22951
   961
            (pushToken t2; pushToken t1; NONE)
haftmann@22951
   962
        end
obua@16784
   963
haftmann@22951
   964
    fun load_values () =
haftmann@22951
   965
        let val v = load_value () in
haftmann@22951
   966
        if v = NONE then [] else (the v)::(load_values ())
haftmann@22951
   967
        end
haftmann@22951
   968
haftmann@22951
   969
    val header = readHeader ()
obua@16784
   970
haftmann@22951
   971
    val result =
haftmann@22951
   972
        case AList.lookup (op =) header "STATUS" of
haftmann@22951
   973
        SOME "INFEASIBLE" => Infeasible
haftmann@22951
   974
          | SOME "UNBOUNDED" => Unbounded
haftmann@22951
   975
          | SOME "OPTIMAL" => Optimal (the (AList.lookup (op =) header "OBJECTIVE"),
haftmann@22951
   976
                       (skip_until_sep ();
haftmann@22951
   977
                        skip_until_sep ();
haftmann@22951
   978
                        load_values ()))
haftmann@22951
   979
          | _ => Undefined
obua@16784
   980
haftmann@22951
   981
    val _ = TextIO.closeIn f
obua@16784
   982
    in
haftmann@22951
   983
    result
obua@16784
   984
    end
obua@16784
   985
    handle (Tokenize s) => raise (Load_cplexResult ("Tokenize: "^s))
wenzelm@51930
   986
     | Option.Option => raise (Load_cplexResult "Option")
obua@16784
   987
haftmann@22951
   988
fun load_cplexResult name =
obua@16784
   989
    let
haftmann@22951
   990
    val flist = [(is_NL, TOKEN_NL),
haftmann@22951
   991
             (is_blank, TOKEN_BLANK),
haftmann@22951
   992
             (is_num, TOKEN_NUM),
haftmann@22951
   993
             (is_sign, TOKEN_SIGN),
obua@16784
   994
                     (is_colon, TOKEN_COLON),
haftmann@22951
   995
             (is_cmp, TOKEN_CMP),
haftmann@22951
   996
             (is_resultsymbol, TOKEN_SYMBOL)]
haftmann@22951
   997
haftmann@22951
   998
    val tokenize = tokenize_general flist
haftmann@22951
   999
haftmann@22951
  1000
    val f = TextIO.openIn name
haftmann@22951
  1001
wenzelm@32740
  1002
    val rest = Unsynchronized.ref []
obua@16784
  1003
haftmann@22951
  1004
    fun readToken_helper () =
haftmann@22951
  1005
        if length (!rest) > 0 then
haftmann@22951
  1006
        let val u = hd (!rest) in
haftmann@22951
  1007
            (
haftmann@22951
  1008
             rest := tl (!rest);
haftmann@22951
  1009
             SOME u
haftmann@22951
  1010
            )
haftmann@22951
  1011
        end
haftmann@22951
  1012
        else
wenzelm@23139
  1013
        (case TextIO.inputLine f of
wenzelm@23139
  1014
          NONE => NONE
wenzelm@23139
  1015
        | SOME s => (rest := tokenize s; readToken_helper()))
obua@16784
  1016
haftmann@22951
  1017
    fun is_tt tok ty = (tok <> NONE andalso (fst (the tok)) = ty)
obua@16784
  1018
haftmann@22951
  1019
    fun pushToken a = if a = NONE then () else (rest := ((the a)::(!rest)))
haftmann@22951
  1020
haftmann@22951
  1021
    fun readToken () =
haftmann@22951
  1022
        let val t = readToken_helper () in
haftmann@22951
  1023
        if is_tt t TOKEN_BLANK then
haftmann@22951
  1024
            readToken ()
haftmann@22951
  1025
        else if is_tt t TOKEN_SIGN then
haftmann@22951
  1026
            let val t2 = readToken_helper () in
haftmann@22951
  1027
            if is_tt t2 TOKEN_NUM then
haftmann@22951
  1028
                (SOME (TOKEN_NUM, (snd (the t))^(snd (the t2))))
haftmann@22951
  1029
            else
haftmann@22951
  1030
                (pushToken t2; t)
haftmann@22951
  1031
            end
haftmann@22951
  1032
        else
haftmann@22951
  1033
            t
haftmann@22951
  1034
        end
obua@16784
  1035
haftmann@22951
  1036
        fun readRestOfLine P =
haftmann@22951
  1037
        let
haftmann@22951
  1038
        val t = readToken ()
haftmann@22951
  1039
        in
haftmann@22951
  1040
        if is_tt t TOKEN_NL orelse t = NONE
haftmann@22951
  1041
        then P
haftmann@22951
  1042
        else readRestOfLine P
haftmann@22951
  1043
        end
obua@16784
  1044
haftmann@22951
  1045
    fun readHeader () =
haftmann@22951
  1046
        let
haftmann@22951
  1047
        fun readStatus () = readRestOfLine ("STATUS", snd (the (readToken ())))
haftmann@22951
  1048
        fun readObjective () =
haftmann@22951
  1049
            let
haftmann@22951
  1050
            val t = readToken ()
haftmann@22951
  1051
            in
haftmann@22951
  1052
            if is_tt t TOKEN_SYMBOL andalso to_upper (snd (the t)) = "VALUE" then
haftmann@22951
  1053
                readRestOfLine ("OBJECTIVE", snd (the (readToken())))
haftmann@22951
  1054
            else
haftmann@22951
  1055
                readRestOfLine ("OBJECTIVE_NAME", snd (the t))
haftmann@22951
  1056
            end
obua@16784
  1057
haftmann@22951
  1058
        val t = readToken ()
haftmann@22951
  1059
        in
haftmann@22951
  1060
        if is_tt t TOKEN_SYMBOL then
haftmann@22951
  1061
            case to_upper (snd (the t)) of
haftmann@22951
  1062
            "STATUS" => (readStatus ())::(readHeader ())
haftmann@22951
  1063
              | "OBJECTIVE" => (readObjective ())::(readHeader ())
haftmann@22951
  1064
              | "SECTION" => (pushToken t; [])
haftmann@22951
  1065
              | _ => (readRestOfLine (); readHeader ())
haftmann@22951
  1066
        else
haftmann@22951
  1067
            (readRestOfLine (); readHeader ())
haftmann@22951
  1068
        end
obua@16784
  1069
haftmann@22951
  1070
    fun skip_nls () =
haftmann@22951
  1071
        let val x = readToken () in
haftmann@22951
  1072
        if is_tt x TOKEN_NL then
haftmann@22951
  1073
            skip_nls ()
haftmann@22951
  1074
        else
haftmann@22951
  1075
            (pushToken x; ())
haftmann@22951
  1076
        end
obua@16784
  1077
haftmann@22951
  1078
    fun skip_paragraph () =
haftmann@22951
  1079
        if is_tt (readToken ()) TOKEN_NL then
haftmann@22951
  1080
        (if is_tt (readToken ()) TOKEN_NL then
haftmann@22951
  1081
             skip_nls ()
haftmann@22951
  1082
         else
haftmann@22951
  1083
             skip_paragraph ())
haftmann@22951
  1084
        else
haftmann@22951
  1085
        skip_paragraph ()
obua@16784
  1086
haftmann@22951
  1087
    fun load_value () =
haftmann@22951
  1088
        let
haftmann@22951
  1089
        val t1 = readToken ()
haftmann@22951
  1090
        val t1 = if is_tt t1 TOKEN_SYMBOL andalso snd (the t1) = "A" then readToken () else t1
haftmann@22951
  1091
        in
haftmann@22951
  1092
        if is_tt t1 TOKEN_NUM then
haftmann@22951
  1093
            let
haftmann@22951
  1094
            val name = readToken ()
haftmann@22951
  1095
            val status = readToken ()
haftmann@22951
  1096
            val value = readToken ()
haftmann@22951
  1097
            in
haftmann@22951
  1098
            if is_tt name TOKEN_SYMBOL andalso
haftmann@22951
  1099
               is_tt status TOKEN_SYMBOL andalso
haftmann@22951
  1100
               is_tt value TOKEN_NUM
haftmann@22951
  1101
            then
haftmann@22951
  1102
                readRestOfLine (SOME (snd (the name), snd (the value)))
haftmann@22951
  1103
            else
haftmann@22951
  1104
                raise (Load_cplexResult "column line expected")
haftmann@22951
  1105
            end
haftmann@22951
  1106
        else
haftmann@22951
  1107
            (pushToken t1; NONE)
haftmann@22951
  1108
        end
obua@16784
  1109
haftmann@22951
  1110
    fun load_values () =
haftmann@22951
  1111
        let val v = load_value () in
haftmann@22951
  1112
        if v = NONE then [] else (the v)::(load_values ())
haftmann@22951
  1113
        end
haftmann@22951
  1114
haftmann@22951
  1115
    val header = readHeader ()
obua@16784
  1116
haftmann@22951
  1117
    val result =
haftmann@22951
  1118
        case AList.lookup (op =) header "STATUS" of
haftmann@22951
  1119
        SOME "INFEASIBLE" => Infeasible
haftmann@22951
  1120
          | SOME "NONOPTIMAL" => Unbounded
haftmann@22951
  1121
          | SOME "OPTIMAL" => Optimal (the (AList.lookup (op =) header "OBJECTIVE"),
haftmann@22951
  1122
                       (skip_paragraph ();
haftmann@22951
  1123
                        skip_paragraph ();
haftmann@22951
  1124
                        skip_paragraph ();
haftmann@22951
  1125
                        skip_paragraph ();
haftmann@22951
  1126
                        skip_paragraph ();
haftmann@22951
  1127
                        load_values ()))
haftmann@22951
  1128
          | _ => Undefined
obua@16784
  1129
haftmann@22951
  1130
    val _ = TextIO.closeIn f
obua@16784
  1131
    in
haftmann@22951
  1132
    result
obua@16784
  1133
    end
obua@16784
  1134
    handle (Tokenize s) => raise (Load_cplexResult ("Tokenize: "^s))
wenzelm@51930
  1135
     | Option.Option => raise (Load_cplexResult "Option")
obua@16784
  1136
obua@16784
  1137
exception Execute of string;
obua@16784
  1138
wenzelm@43602
  1139
fun tmp_file s = Path.implode (Path.expand (File.tmp_path (Path.basic s)));
obua@16784
  1140
fun wrap s = "\""^s^"\"";
obua@16784
  1141
obua@16784
  1142
fun solve_glpk prog =
haftmann@22951
  1143
    let
wenzelm@41491
  1144
    val name = string_of_int (Time.toMicroseconds (Time.now ()))
haftmann@22951
  1145
    val lpname = tmp_file (name^".lp")
haftmann@22951
  1146
    val resultname = tmp_file (name^".txt")
haftmann@22951
  1147
    val _ = save_cplexFile lpname prog
haftmann@22951
  1148
    val cplex_path = getenv "GLPK_PATH"
haftmann@22951
  1149
    val cplex = if cplex_path = "" then "glpsol" else cplex_path
haftmann@22951
  1150
    val command = (wrap cplex)^" --lpt "^(wrap lpname)^" --output "^(wrap resultname)
wenzelm@43850
  1151
    val answer = #1 (Isabelle_System.bash_output command)
obua@16784
  1152
    in
haftmann@22951
  1153
    let
haftmann@22951
  1154
        val result = load_glpkResult resultname
haftmann@22951
  1155
        val _ = OS.FileSys.remove lpname
haftmann@22951
  1156
        val _ = OS.FileSys.remove resultname
obua@16784
  1157
    in
haftmann@22951
  1158
        result
haftmann@22951
  1159
    end
haftmann@22951
  1160
    handle (Load_cplexResult s) => raise (Execute ("Load_cplexResult: "^s^"\nExecute: "^answer))
wenzelm@50902
  1161
         | exn => if Exn.is_interrupt exn then reraise exn else raise (Execute answer)
obua@16784
  1162
    end
obua@16784
  1163
haftmann@22951
  1164
fun solve_cplex prog =
haftmann@22951
  1165
    let
haftmann@22951
  1166
    fun write_script s lp r =
haftmann@22951
  1167
        let
haftmann@22951
  1168
        val f = TextIO.openOut s
haftmann@22951
  1169
        val _ = TextIO.output (f, "read\n"^lp^"\noptimize\nwrite\n"^r^"\nquit")
haftmann@22951
  1170
        val _ = TextIO.closeOut f
haftmann@22951
  1171
        in
haftmann@22951
  1172
        ()
haftmann@22951
  1173
        end
haftmann@22951
  1174
wenzelm@41491
  1175
    val name = string_of_int (Time.toMicroseconds (Time.now ()))
haftmann@22951
  1176
    val lpname = tmp_file (name^".lp")
haftmann@22951
  1177
    val resultname = tmp_file (name^".txt")
haftmann@22951
  1178
    val scriptname = tmp_file (name^".script")
haftmann@22951
  1179
    val _ = save_cplexFile lpname prog
haftmann@22951
  1180
    val _ = write_script scriptname lpname resultname
haftmann@22951
  1181
    in
haftmann@22951
  1182
    let
haftmann@22951
  1183
        val result = load_cplexResult resultname
haftmann@22951
  1184
        val _ = OS.FileSys.remove lpname
haftmann@22951
  1185
        val _ = OS.FileSys.remove resultname
haftmann@22951
  1186
        val _ = OS.FileSys.remove scriptname
haftmann@22951
  1187
    in
haftmann@22951
  1188
        result
haftmann@22951
  1189
    end
haftmann@22951
  1190
    end
haftmann@22951
  1191
haftmann@22951
  1192
fun solve prog =
obua@16966
  1193
    case get_solver () of
haftmann@22951
  1194
      SOLVER_DEFAULT =>
obua@16966
  1195
        (case getenv "LP_SOLVER" of
haftmann@22951
  1196
       "CPLEX" => solve_cplex prog
obua@16966
  1197
         | "GLPK" => solve_glpk prog
obua@16966
  1198
         | _ => raise (Execute ("LP_SOLVER must be set to CPLEX or to GLPK")))
obua@16966
  1199
    | SOLVER_CPLEX => solve_cplex prog
obua@16966
  1200
    | SOLVER_GLPK => solve_glpk prog
haftmann@22951
  1201
obua@16784
  1202
end;