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