1.1 --- a/src/HOL/Matrix/Cplex_tools.ML Sat Mar 17 12:26:19 2012 +0100
1.2 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000
1.3 @@ -1,1192 +0,0 @@
1.4 -(* Title: HOL/Matrix/Cplex_tools.ML
1.5 - Author: Steven Obua
1.6 -*)
1.7 -
1.8 -signature CPLEX =
1.9 -sig
1.10 -
1.11 - datatype cplexTerm = cplexVar of string | cplexNum of string | cplexInf
1.12 - | cplexNeg of cplexTerm
1.13 - | cplexProd of cplexTerm * cplexTerm
1.14 - | cplexSum of (cplexTerm list)
1.15 -
1.16 - datatype cplexComp = cplexLe | cplexLeq | cplexEq | cplexGe | cplexGeq
1.17 -
1.18 - datatype cplexGoal = cplexMinimize of cplexTerm
1.19 - | cplexMaximize of cplexTerm
1.20 -
1.21 - datatype cplexConstr = cplexConstr of cplexComp *
1.22 - (cplexTerm * cplexTerm)
1.23 -
1.24 - datatype cplexBounds = cplexBounds of cplexTerm * cplexComp * cplexTerm
1.25 - * cplexComp * cplexTerm
1.26 - | cplexBound of cplexTerm * cplexComp * cplexTerm
1.27 -
1.28 - datatype cplexProg = cplexProg of string
1.29 - * cplexGoal
1.30 - * ((string option * cplexConstr)
1.31 - list)
1.32 - * cplexBounds list
1.33 -
1.34 - datatype cplexResult = Unbounded
1.35 - | Infeasible
1.36 - | Undefined
1.37 - | Optimal of string *
1.38 - (((* name *) string *
1.39 - (* value *) string) list)
1.40 -
1.41 - datatype cplexSolver = SOLVER_DEFAULT | SOLVER_CPLEX | SOLVER_GLPK
1.42 -
1.43 - exception Load_cplexFile of string
1.44 - exception Load_cplexResult of string
1.45 - exception Save_cplexFile of string
1.46 - exception Execute of string
1.47 -
1.48 - val load_cplexFile : string -> cplexProg
1.49 -
1.50 - val save_cplexFile : string -> cplexProg -> unit
1.51 -
1.52 - val elim_nonfree_bounds : cplexProg -> cplexProg
1.53 -
1.54 - val relax_strict_ineqs : cplexProg -> cplexProg
1.55 -
1.56 - val is_normed_cplexProg : cplexProg -> bool
1.57 -
1.58 - val get_solver : unit -> cplexSolver
1.59 - val set_solver : cplexSolver -> unit
1.60 - val solve : cplexProg -> cplexResult
1.61 -end;
1.62 -
1.63 -structure Cplex : CPLEX =
1.64 -struct
1.65 -
1.66 -datatype cplexSolver = SOLVER_DEFAULT | SOLVER_CPLEX | SOLVER_GLPK
1.67 -
1.68 -val cplexsolver = Unsynchronized.ref SOLVER_DEFAULT;
1.69 -fun get_solver () = !cplexsolver;
1.70 -fun set_solver s = (cplexsolver := s);
1.71 -
1.72 -exception Load_cplexFile of string;
1.73 -exception Load_cplexResult of string;
1.74 -exception Save_cplexFile of string;
1.75 -
1.76 -datatype cplexTerm = cplexVar of string
1.77 - | cplexNum of string
1.78 - | cplexInf
1.79 - | cplexNeg of cplexTerm
1.80 - | cplexProd of cplexTerm * cplexTerm
1.81 - | cplexSum of (cplexTerm list)
1.82 -datatype cplexComp = cplexLe | cplexLeq | cplexEq | cplexGe | cplexGeq
1.83 -datatype cplexGoal = cplexMinimize of cplexTerm | cplexMaximize of cplexTerm
1.84 -datatype cplexConstr = cplexConstr of cplexComp * (cplexTerm * cplexTerm)
1.85 -datatype cplexBounds = cplexBounds of cplexTerm * cplexComp * cplexTerm
1.86 - * cplexComp * cplexTerm
1.87 - | cplexBound of cplexTerm * cplexComp * cplexTerm
1.88 -datatype cplexProg = cplexProg of string
1.89 - * cplexGoal
1.90 - * ((string option * cplexConstr) list)
1.91 - * cplexBounds list
1.92 -
1.93 -fun rev_cmp cplexLe = cplexGe
1.94 - | rev_cmp cplexLeq = cplexGeq
1.95 - | rev_cmp cplexGe = cplexLe
1.96 - | rev_cmp cplexGeq = cplexLeq
1.97 - | rev_cmp cplexEq = cplexEq
1.98 -
1.99 -fun the NONE = raise (Load_cplexFile "SOME expected")
1.100 - | the (SOME x) = x;
1.101 -
1.102 -fun modulo_signed is_something (cplexNeg u) = is_something u
1.103 - | modulo_signed is_something u = is_something u
1.104 -
1.105 -fun is_Num (cplexNum _) = true
1.106 - | is_Num _ = false
1.107 -
1.108 -fun is_Inf cplexInf = true
1.109 - | is_Inf _ = false
1.110 -
1.111 -fun is_Var (cplexVar _) = true
1.112 - | is_Var _ = false
1.113 -
1.114 -fun is_Neg (cplexNeg _) = true
1.115 - | is_Neg _ = false
1.116 -
1.117 -fun is_normed_Prod (cplexProd (t1, t2)) =
1.118 - (is_Num t1) andalso (is_Var t2)
1.119 - | is_normed_Prod x = is_Var x
1.120 -
1.121 -fun is_normed_Sum (cplexSum ts) =
1.122 - (ts <> []) andalso forall (modulo_signed is_normed_Prod) ts
1.123 - | is_normed_Sum x = modulo_signed is_normed_Prod x
1.124 -
1.125 -fun is_normed_Constr (cplexConstr (_, (t1, t2))) =
1.126 - (is_normed_Sum t1) andalso (modulo_signed is_Num t2)
1.127 -
1.128 -fun is_Num_or_Inf x = is_Inf x orelse is_Num x
1.129 -
1.130 -fun is_normed_Bounds (cplexBounds (t1, c1, t2, c2, t3)) =
1.131 - (c1 = cplexLe orelse c1 = cplexLeq) andalso
1.132 - (c2 = cplexLe orelse c2 = cplexLeq) andalso
1.133 - is_Var t2 andalso
1.134 - modulo_signed is_Num_or_Inf t1 andalso
1.135 - modulo_signed is_Num_or_Inf t3
1.136 - | is_normed_Bounds (cplexBound (t1, c, t2)) =
1.137 - (is_Var t1 andalso (modulo_signed is_Num_or_Inf t2))
1.138 - orelse
1.139 - (c <> cplexEq andalso
1.140 - is_Var t2 andalso (modulo_signed is_Num_or_Inf t1))
1.141 -
1.142 -fun term_of_goal (cplexMinimize x) = x
1.143 - | term_of_goal (cplexMaximize x) = x
1.144 -
1.145 -fun is_normed_cplexProg (cplexProg (_, goal, constraints, bounds)) =
1.146 - is_normed_Sum (term_of_goal goal) andalso
1.147 - forall (fn (_,x) => is_normed_Constr x) constraints andalso
1.148 - forall is_normed_Bounds bounds
1.149 -
1.150 -fun is_NL s = s = "\n"
1.151 -
1.152 -fun is_blank s = forall (fn c => c <> #"\n" andalso Char.isSpace c) (String.explode s)
1.153 -
1.154 -fun is_num a =
1.155 - let
1.156 - val b = String.explode a
1.157 - fun num4 cs = forall Char.isDigit cs
1.158 - fun num3 [] = true
1.159 - | num3 (ds as (c::cs)) =
1.160 - if c = #"+" orelse c = #"-" then
1.161 - num4 cs
1.162 - else
1.163 - num4 ds
1.164 - fun num2 [] = true
1.165 - | num2 (c::cs) =
1.166 - if c = #"e" orelse c = #"E" then num3 cs
1.167 - else (Char.isDigit c) andalso num2 cs
1.168 - fun num1 [] = true
1.169 - | num1 (c::cs) =
1.170 - if c = #"." then num2 cs
1.171 - else if c = #"e" orelse c = #"E" then num3 cs
1.172 - else (Char.isDigit c) andalso num1 cs
1.173 - fun num [] = true
1.174 - | num (c::cs) =
1.175 - if c = #"." then num2 cs
1.176 - else (Char.isDigit c) andalso num1 cs
1.177 - in
1.178 - num b
1.179 - end
1.180 -
1.181 -fun is_delimiter s = s = "+" orelse s = "-" orelse s = ":"
1.182 -
1.183 -fun is_cmp s = s = "<" orelse s = ">" orelse s = "<="
1.184 - orelse s = ">=" orelse s = "="
1.185 -
1.186 -fun is_symbol a =
1.187 - let
1.188 - val symbol_char = String.explode "!\"#$%&()/,.;?@_`'{}|~"
1.189 - fun is_symbol_char c = Char.isAlphaNum c orelse
1.190 - exists (fn d => d=c) symbol_char
1.191 - fun is_symbol_start c = is_symbol_char c andalso
1.192 - not (Char.isDigit c) andalso
1.193 - not (c= #".")
1.194 - val b = String.explode a
1.195 - in
1.196 - b <> [] andalso is_symbol_start (hd b) andalso
1.197 - forall is_symbol_char b
1.198 - end
1.199 -
1.200 -fun to_upper s = String.implode (map Char.toUpper (String.explode s))
1.201 -
1.202 -fun keyword x =
1.203 - let
1.204 - val a = to_upper x
1.205 - in
1.206 - if a = "BOUNDS" orelse a = "BOUND" then
1.207 - SOME "BOUNDS"
1.208 - else if a = "MINIMIZE" orelse a = "MINIMUM" orelse a = "MIN" then
1.209 - SOME "MINIMIZE"
1.210 - else if a = "MAXIMIZE" orelse a = "MAXIMUM" orelse a = "MAX" then
1.211 - SOME "MAXIMIZE"
1.212 - else if a = "ST" orelse a = "S.T." orelse a = "ST." then
1.213 - SOME "ST"
1.214 - else if a = "FREE" orelse a = "END" then
1.215 - SOME a
1.216 - else if a = "GENERAL" orelse a = "GENERALS" orelse a = "GEN" then
1.217 - SOME "GENERAL"
1.218 - else if a = "INTEGER" orelse a = "INTEGERS" orelse a = "INT" then
1.219 - SOME "INTEGER"
1.220 - else if a = "BINARY" orelse a = "BINARIES" orelse a = "BIN" then
1.221 - SOME "BINARY"
1.222 - else if a = "INF" orelse a = "INFINITY" then
1.223 - SOME "INF"
1.224 - else
1.225 - NONE
1.226 - end
1.227 -
1.228 -val TOKEN_ERROR = ~1
1.229 -val TOKEN_BLANK = 0
1.230 -val TOKEN_NUM = 1
1.231 -val TOKEN_DELIMITER = 2
1.232 -val TOKEN_SYMBOL = 3
1.233 -val TOKEN_LABEL = 4
1.234 -val TOKEN_CMP = 5
1.235 -val TOKEN_KEYWORD = 6
1.236 -val TOKEN_NL = 7
1.237 -
1.238 -(* tokenize takes a list of chars as argument and returns a list of
1.239 - int * string pairs, each string representing a "cplex token",
1.240 - and each int being one of TOKEN_NUM, TOKEN_DELIMITER, TOKEN_CMP
1.241 - or TOKEN_SYMBOL *)
1.242 -fun tokenize s =
1.243 - let
1.244 - val flist = [(is_NL, TOKEN_NL),
1.245 - (is_blank, TOKEN_BLANK),
1.246 - (is_num, TOKEN_NUM),
1.247 - (is_delimiter, TOKEN_DELIMITER),
1.248 - (is_cmp, TOKEN_CMP),
1.249 - (is_symbol, TOKEN_SYMBOL)]
1.250 - fun match_helper [] s = (fn _ => false, TOKEN_ERROR)
1.251 - | match_helper (f::fs) s =
1.252 - if ((fst f) s) then f else match_helper fs s
1.253 - fun match s = match_helper flist s
1.254 - fun tok s =
1.255 - if s = "" then [] else
1.256 - let
1.257 - val h = String.substring (s,0,1)
1.258 - val (f, j) = match h
1.259 - fun len i =
1.260 - if size s = i then i
1.261 - else if f (String.substring (s,0,i+1)) then
1.262 - len (i+1)
1.263 - else i
1.264 - in
1.265 - if j < 0 then
1.266 - (if h = "\\" then []
1.267 - else raise (Load_cplexFile ("token expected, found: "
1.268 - ^s)))
1.269 - else
1.270 - let
1.271 - val l = len 1
1.272 - val u = String.substring (s,0,l)
1.273 - val v = String.extract (s,l,NONE)
1.274 - in
1.275 - if j = 0 then tok v else (j, u) :: tok v
1.276 - end
1.277 - end
1.278 - in
1.279 - tok s
1.280 - end
1.281 -
1.282 -exception Tokenize of string;
1.283 -
1.284 -fun tokenize_general flist s =
1.285 - let
1.286 - fun match_helper [] s = raise (Tokenize s)
1.287 - | match_helper (f::fs) s =
1.288 - if ((fst f) s) then f else match_helper fs s
1.289 - fun match s = match_helper flist s
1.290 - fun tok s =
1.291 - if s = "" then [] else
1.292 - let
1.293 - val h = String.substring (s,0,1)
1.294 - val (f, j) = match h
1.295 - fun len i =
1.296 - if size s = i then i
1.297 - else if f (String.substring (s,0,i+1)) then
1.298 - len (i+1)
1.299 - else i
1.300 - val l = len 1
1.301 - in
1.302 - (j, String.substring (s,0,l)) :: tok (String.extract (s,l,NONE))
1.303 - end
1.304 - in
1.305 - tok s
1.306 - end
1.307 -
1.308 -fun load_cplexFile name =
1.309 - let
1.310 - val f = TextIO.openIn name
1.311 - val ignore_NL = Unsynchronized.ref true
1.312 - val rest = Unsynchronized.ref []
1.313 -
1.314 - fun is_symbol s c = (fst c) = TOKEN_SYMBOL andalso (to_upper (snd c)) = s
1.315 -
1.316 - fun readToken_helper () =
1.317 - if length (!rest) > 0 then
1.318 - let val u = hd (!rest) in
1.319 - (
1.320 - rest := tl (!rest);
1.321 - SOME u
1.322 - )
1.323 - end
1.324 - else
1.325 - (case TextIO.inputLine f of
1.326 - NONE => NONE
1.327 - | SOME s =>
1.328 - let val t = tokenize s in
1.329 - if (length t >= 2 andalso
1.330 - snd(hd (tl t)) = ":")
1.331 - then
1.332 - rest := (TOKEN_LABEL, snd (hd t)) :: (tl (tl t))
1.333 - else if (length t >= 2) andalso is_symbol "SUBJECT" (hd (t))
1.334 - andalso is_symbol "TO" (hd (tl t))
1.335 - then
1.336 - rest := (TOKEN_SYMBOL, "ST") :: (tl (tl t))
1.337 - else
1.338 - rest := t;
1.339 - readToken_helper ()
1.340 - end)
1.341 -
1.342 - fun readToken_helper2 () =
1.343 - let val c = readToken_helper () in
1.344 - if c = NONE then NONE
1.345 - else if !ignore_NL andalso fst (the c) = TOKEN_NL then
1.346 - readToken_helper2 ()
1.347 - else if fst (the c) = TOKEN_SYMBOL
1.348 - andalso keyword (snd (the c)) <> NONE
1.349 - then SOME (TOKEN_KEYWORD, the (keyword (snd (the c))))
1.350 - else c
1.351 - end
1.352 -
1.353 - fun readToken () = readToken_helper2 ()
1.354 -
1.355 - fun pushToken a = rest := (a::(!rest))
1.356 -
1.357 - fun is_value token =
1.358 - fst token = TOKEN_NUM orelse (fst token = TOKEN_KEYWORD
1.359 - andalso snd token = "INF")
1.360 -
1.361 - fun get_value token =
1.362 - if fst token = TOKEN_NUM then
1.363 - cplexNum (snd token)
1.364 - else if fst token = TOKEN_KEYWORD andalso snd token = "INF"
1.365 - then
1.366 - cplexInf
1.367 - else
1.368 - raise (Load_cplexFile "num expected")
1.369 -
1.370 - fun readTerm_Product only_num =
1.371 - let val c = readToken () in
1.372 - if c = NONE then NONE
1.373 - else if fst (the c) = TOKEN_SYMBOL
1.374 - then (
1.375 - if only_num then (pushToken (the c); NONE)
1.376 - else SOME (cplexVar (snd (the c)))
1.377 - )
1.378 - else if only_num andalso is_value (the c) then
1.379 - SOME (get_value (the c))
1.380 - else if is_value (the c) then
1.381 - let val t1 = get_value (the c)
1.382 - val d = readToken ()
1.383 - in
1.384 - if d = NONE then SOME t1
1.385 - else if fst (the d) = TOKEN_SYMBOL then
1.386 - SOME (cplexProd (t1, cplexVar (snd (the d))))
1.387 - else
1.388 - (pushToken (the d); SOME t1)
1.389 - end
1.390 - else (pushToken (the c); NONE)
1.391 - end
1.392 -
1.393 - fun readTerm_Signed only_signed only_num =
1.394 - let
1.395 - val c = readToken ()
1.396 - in
1.397 - if c = NONE then NONE
1.398 - else
1.399 - let val d = the c in
1.400 - if d = (TOKEN_DELIMITER, "+") then
1.401 - readTerm_Product only_num
1.402 - else if d = (TOKEN_DELIMITER, "-") then
1.403 - SOME (cplexNeg (the (readTerm_Product
1.404 - only_num)))
1.405 - else (pushToken d;
1.406 - if only_signed then NONE
1.407 - else readTerm_Product only_num)
1.408 - end
1.409 - end
1.410 -
1.411 - fun readTerm_Sum first_signed =
1.412 - let val c = readTerm_Signed first_signed false in
1.413 - if c = NONE then [] else (the c)::(readTerm_Sum true)
1.414 - end
1.415 -
1.416 - fun readTerm () =
1.417 - let val c = readTerm_Sum false in
1.418 - if c = [] then NONE
1.419 - else if tl c = [] then SOME (hd c)
1.420 - else SOME (cplexSum c)
1.421 - end
1.422 -
1.423 - fun readLabeledTerm () =
1.424 - let val c = readToken () in
1.425 - if c = NONE then (NONE, NONE)
1.426 - else if fst (the c) = TOKEN_LABEL then
1.427 - let val t = readTerm () in
1.428 - if t = NONE then
1.429 - raise (Load_cplexFile ("term after label "^
1.430 - (snd (the c))^
1.431 - " expected"))
1.432 - else (SOME (snd (the c)), t)
1.433 - end
1.434 - else (pushToken (the c); (NONE, readTerm ()))
1.435 - end
1.436 -
1.437 - fun readGoal () =
1.438 - let
1.439 - val g = readToken ()
1.440 - in
1.441 - if g = SOME (TOKEN_KEYWORD, "MAXIMIZE") then
1.442 - cplexMaximize (the (snd (readLabeledTerm ())))
1.443 - else if g = SOME (TOKEN_KEYWORD, "MINIMIZE") then
1.444 - cplexMinimize (the (snd (readLabeledTerm ())))
1.445 - else raise (Load_cplexFile "MAXIMIZE or MINIMIZE expected")
1.446 - end
1.447 -
1.448 - fun str2cmp b =
1.449 - (case b of
1.450 - "<" => cplexLe
1.451 - | "<=" => cplexLeq
1.452 - | ">" => cplexGe
1.453 - | ">=" => cplexGeq
1.454 - | "=" => cplexEq
1.455 - | _ => raise (Load_cplexFile (b^" is no TOKEN_CMP")))
1.456 -
1.457 - fun readConstraint () =
1.458 - let
1.459 - val t = readLabeledTerm ()
1.460 - fun make_constraint b t1 t2 =
1.461 - cplexConstr
1.462 - (str2cmp b,
1.463 - (t1, t2))
1.464 - in
1.465 - if snd t = NONE then NONE
1.466 - else
1.467 - let val c = readToken () in
1.468 - if c = NONE orelse fst (the c) <> TOKEN_CMP
1.469 - then raise (Load_cplexFile "TOKEN_CMP expected")
1.470 - else
1.471 - let val n = readTerm_Signed false true in
1.472 - if n = NONE then
1.473 - raise (Load_cplexFile "num expected")
1.474 - else
1.475 - SOME (fst t,
1.476 - make_constraint (snd (the c))
1.477 - (the (snd t))
1.478 - (the n))
1.479 - end
1.480 - end
1.481 - end
1.482 -
1.483 - fun readST () =
1.484 - let
1.485 - fun readbody () =
1.486 - let val t = readConstraint () in
1.487 - if t = NONE then []
1.488 - else if (is_normed_Constr (snd (the t))) then
1.489 - (the t)::(readbody ())
1.490 - else if (fst (the t) <> NONE) then
1.491 - raise (Load_cplexFile
1.492 - ("constraint '"^(the (fst (the t)))^
1.493 - "'is not normed"))
1.494 - else
1.495 - raise (Load_cplexFile
1.496 - "constraint is not normed")
1.497 - end
1.498 - in
1.499 - if readToken () = SOME (TOKEN_KEYWORD, "ST")
1.500 - then
1.501 - readbody ()
1.502 - else
1.503 - raise (Load_cplexFile "ST expected")
1.504 - end
1.505 -
1.506 - fun readCmp () =
1.507 - let val c = readToken () in
1.508 - if c = NONE then NONE
1.509 - else if fst (the c) = TOKEN_CMP then
1.510 - SOME (str2cmp (snd (the c)))
1.511 - else (pushToken (the c); NONE)
1.512 - end
1.513 -
1.514 - fun skip_NL () =
1.515 - let val c = readToken () in
1.516 - if c <> NONE andalso fst (the c) = TOKEN_NL then
1.517 - skip_NL ()
1.518 - else
1.519 - (pushToken (the c); ())
1.520 - end
1.521 -
1.522 - fun make_bounds c t1 t2 =
1.523 - cplexBound (t1, c, t2)
1.524 -
1.525 - fun readBound () =
1.526 - let
1.527 - val _ = skip_NL ()
1.528 - val t1 = readTerm ()
1.529 - in
1.530 - if t1 = NONE then NONE
1.531 - else
1.532 - let
1.533 - val c1 = readCmp ()
1.534 - in
1.535 - if c1 = NONE then
1.536 - let
1.537 - val c = readToken ()
1.538 - in
1.539 - if c = SOME (TOKEN_KEYWORD, "FREE") then
1.540 - SOME (
1.541 - cplexBounds (cplexNeg cplexInf,
1.542 - cplexLeq,
1.543 - the t1,
1.544 - cplexLeq,
1.545 - cplexInf))
1.546 - else
1.547 - raise (Load_cplexFile "FREE expected")
1.548 - end
1.549 - else
1.550 - let
1.551 - val t2 = readTerm ()
1.552 - in
1.553 - if t2 = NONE then
1.554 - raise (Load_cplexFile "term expected")
1.555 - else
1.556 - let val c2 = readCmp () in
1.557 - if c2 = NONE then
1.558 - SOME (make_bounds (the c1)
1.559 - (the t1)
1.560 - (the t2))
1.561 - else
1.562 - SOME (
1.563 - cplexBounds (the t1,
1.564 - the c1,
1.565 - the t2,
1.566 - the c2,
1.567 - the (readTerm())))
1.568 - end
1.569 - end
1.570 - end
1.571 - end
1.572 -
1.573 - fun readBounds () =
1.574 - let
1.575 - fun makestring _ = "?"
1.576 - fun readbody () =
1.577 - let
1.578 - val b = readBound ()
1.579 - in
1.580 - if b = NONE then []
1.581 - else if (is_normed_Bounds (the b)) then
1.582 - (the b)::(readbody())
1.583 - else (
1.584 - raise (Load_cplexFile
1.585 - ("bounds are not normed in: "^
1.586 - (makestring (the b)))))
1.587 - end
1.588 - in
1.589 - if readToken () = SOME (TOKEN_KEYWORD, "BOUNDS") then
1.590 - readbody ()
1.591 - else raise (Load_cplexFile "BOUNDS expected")
1.592 - end
1.593 -
1.594 - fun readEnd () =
1.595 - if readToken () = SOME (TOKEN_KEYWORD, "END") then ()
1.596 - else raise (Load_cplexFile "END expected")
1.597 -
1.598 - val result_Goal = readGoal ()
1.599 - val result_ST = readST ()
1.600 - val _ = ignore_NL := false
1.601 - val result_Bounds = readBounds ()
1.602 - val _ = ignore_NL := true
1.603 - val _ = readEnd ()
1.604 - val _ = TextIO.closeIn f
1.605 - in
1.606 - cplexProg (name, result_Goal, result_ST, result_Bounds)
1.607 - end
1.608 -
1.609 -fun save_cplexFile filename (cplexProg (_, goal, constraints, bounds)) =
1.610 - let
1.611 - val f = TextIO.openOut filename
1.612 -
1.613 - fun basic_write s = TextIO.output(f, s)
1.614 -
1.615 - val linebuf = Unsynchronized.ref ""
1.616 - fun buf_flushline s =
1.617 - (basic_write (!linebuf);
1.618 - basic_write "\n";
1.619 - linebuf := s)
1.620 - fun buf_add s = linebuf := (!linebuf) ^ s
1.621 -
1.622 - fun write s =
1.623 - if (String.size s) + (String.size (!linebuf)) >= 250 then
1.624 - buf_flushline (" "^s)
1.625 - else
1.626 - buf_add s
1.627 -
1.628 - fun writeln s = (buf_add s; buf_flushline "")
1.629 -
1.630 - fun write_term (cplexVar x) = write x
1.631 - | write_term (cplexNum x) = write x
1.632 - | write_term cplexInf = write "inf"
1.633 - | write_term (cplexProd (cplexNum "1", b)) = write_term b
1.634 - | write_term (cplexProd (a, b)) =
1.635 - (write_term a; write " "; write_term b)
1.636 - | write_term (cplexNeg x) = (write " - "; write_term x)
1.637 - | write_term (cplexSum ts) = write_terms ts
1.638 - and write_terms [] = ()
1.639 - | write_terms (t::ts) =
1.640 - (if (not (is_Neg t)) then write " + " else ();
1.641 - write_term t; write_terms ts)
1.642 -
1.643 - fun write_goal (cplexMaximize term) =
1.644 - (writeln "MAXIMIZE"; write_term term; writeln "")
1.645 - | write_goal (cplexMinimize term) =
1.646 - (writeln "MINIMIZE"; write_term term; writeln "")
1.647 -
1.648 - fun write_cmp cplexLe = write "<"
1.649 - | write_cmp cplexLeq = write "<="
1.650 - | write_cmp cplexEq = write "="
1.651 - | write_cmp cplexGe = write ">"
1.652 - | write_cmp cplexGeq = write ">="
1.653 -
1.654 - fun write_constr (cplexConstr (cmp, (a,b))) =
1.655 - (write_term a;
1.656 - write " ";
1.657 - write_cmp cmp;
1.658 - write " ";
1.659 - write_term b)
1.660 -
1.661 - fun write_constraints [] = ()
1.662 - | write_constraints (c::cs) =
1.663 - (if (fst c <> NONE)
1.664 - then
1.665 - (write (the (fst c)); write ": ")
1.666 - else
1.667 - ();
1.668 - write_constr (snd c);
1.669 - writeln "";
1.670 - write_constraints cs)
1.671 -
1.672 - fun write_bounds [] = ()
1.673 - | write_bounds ((cplexBounds (t1,c1,t2,c2,t3))::bs) =
1.674 - ((if t1 = cplexNeg cplexInf andalso t3 = cplexInf
1.675 - andalso (c1 = cplexLeq orelse c1 = cplexLe)
1.676 - andalso (c2 = cplexLeq orelse c2 = cplexLe)
1.677 - then
1.678 - (write_term t2; write " free")
1.679 - else
1.680 - (write_term t1; write " "; write_cmp c1; write " ";
1.681 - write_term t2; write " "; write_cmp c2; write " ";
1.682 - write_term t3)
1.683 - ); writeln ""; write_bounds bs)
1.684 - | write_bounds ((cplexBound (t1, c, t2)) :: bs) =
1.685 - (write_term t1; write " ";
1.686 - write_cmp c; write " ";
1.687 - write_term t2; writeln ""; write_bounds bs)
1.688 -
1.689 - val _ = write_goal goal
1.690 - val _ = (writeln ""; writeln "ST")
1.691 - val _ = write_constraints constraints
1.692 - val _ = (writeln ""; writeln "BOUNDS")
1.693 - val _ = write_bounds bounds
1.694 - val _ = (writeln ""; writeln "END")
1.695 - val _ = TextIO.closeOut f
1.696 - in
1.697 - ()
1.698 - end
1.699 -
1.700 -fun norm_Constr (constr as cplexConstr (c, (t1, t2))) =
1.701 - if not (modulo_signed is_Num t2) andalso
1.702 - modulo_signed is_Num t1
1.703 - then
1.704 - [cplexConstr (rev_cmp c, (t2, t1))]
1.705 - else if (c = cplexLe orelse c = cplexLeq) andalso
1.706 - (t1 = (cplexNeg cplexInf) orelse t2 = cplexInf)
1.707 - then
1.708 - []
1.709 - else if (c = cplexGe orelse c = cplexGeq) andalso
1.710 - (t1 = cplexInf orelse t2 = cplexNeg cplexInf)
1.711 - then
1.712 - []
1.713 - else
1.714 - [constr]
1.715 -
1.716 -fun bound2constr (cplexBounds (t1,c1,t2,c2,t3)) =
1.717 - (norm_Constr(cplexConstr (c1, (t1, t2))))
1.718 - @ (norm_Constr(cplexConstr (c2, (t2, t3))))
1.719 - | bound2constr (cplexBound (t1, cplexEq, t2)) =
1.720 - (norm_Constr(cplexConstr (cplexLeq, (t1, t2))))
1.721 - @ (norm_Constr(cplexConstr (cplexLeq, (t2, t1))))
1.722 - | bound2constr (cplexBound (t1, c1, t2)) =
1.723 - norm_Constr(cplexConstr (c1, (t1,t2)))
1.724 -
1.725 -val emptyset = Symtab.empty
1.726 -
1.727 -fun singleton v = Symtab.update (v, ()) emptyset
1.728 -
1.729 -fun merge a b = Symtab.merge (op =) (a, b)
1.730 -
1.731 -fun mergemap f ts = fold (fn x => fn table => merge table (f x)) ts Symtab.empty
1.732 -
1.733 -fun diff a b = Symtab.fold (Symtab.delete_safe o fst) b a
1.734 -
1.735 -fun collect_vars (cplexVar v) = singleton v
1.736 - | collect_vars (cplexNeg t) = collect_vars t
1.737 - | collect_vars (cplexProd (t1, t2)) =
1.738 - merge (collect_vars t1) (collect_vars t2)
1.739 - | collect_vars (cplexSum ts) = mergemap collect_vars ts
1.740 - | collect_vars _ = emptyset
1.741 -
1.742 -(* Eliminates all nonfree bounds from the linear program and produces an
1.743 - equivalent program with only free bounds
1.744 - IF for the input program P holds: is_normed_cplexProg P *)
1.745 -fun elim_nonfree_bounds (cplexProg (name, goal, constraints, bounds)) =
1.746 - let
1.747 - fun collect_constr_vars (_, cplexConstr (_, (t1,_))) =
1.748 - (collect_vars t1)
1.749 -
1.750 - val cvars = merge (collect_vars (term_of_goal goal))
1.751 - (mergemap collect_constr_vars constraints)
1.752 -
1.753 - fun collect_lower_bounded_vars
1.754 - (cplexBounds (_, _, cplexVar v, _, _)) =
1.755 - singleton v
1.756 - | collect_lower_bounded_vars
1.757 - (cplexBound (_, cplexLe, cplexVar v)) =
1.758 - singleton v
1.759 - | collect_lower_bounded_vars
1.760 - (cplexBound (_, cplexLeq, cplexVar v)) =
1.761 - singleton v
1.762 - | collect_lower_bounded_vars
1.763 - (cplexBound (cplexVar v, cplexGe,_)) =
1.764 - singleton v
1.765 - | collect_lower_bounded_vars
1.766 - (cplexBound (cplexVar v, cplexGeq, _)) =
1.767 - singleton v
1.768 - | collect_lower_bounded_vars
1.769 - (cplexBound (cplexVar v, cplexEq, _)) =
1.770 - singleton v
1.771 - | collect_lower_bounded_vars _ = emptyset
1.772 -
1.773 - val lvars = mergemap collect_lower_bounded_vars bounds
1.774 - val positive_vars = diff cvars lvars
1.775 - val zero = cplexNum "0"
1.776 -
1.777 - fun make_pos_constr v =
1.778 - (NONE, cplexConstr (cplexGeq, ((cplexVar v), zero)))
1.779 -
1.780 - fun make_free_bound v =
1.781 - cplexBounds (cplexNeg cplexInf, cplexLeq,
1.782 - cplexVar v, cplexLeq,
1.783 - cplexInf)
1.784 -
1.785 - val pos_constrs = rev (Symtab.fold
1.786 - (fn (k, _) => cons (make_pos_constr k))
1.787 - positive_vars [])
1.788 - val bound_constrs = map (pair NONE)
1.789 - (maps bound2constr bounds)
1.790 - val constraints' = constraints @ pos_constrs @ bound_constrs
1.791 - val bounds' = rev (Symtab.fold (fn (v, _) => cons (make_free_bound v)) cvars []);
1.792 - in
1.793 - cplexProg (name, goal, constraints', bounds')
1.794 - end
1.795 -
1.796 -fun relax_strict_ineqs (cplexProg (name, goals, constrs, bounds)) =
1.797 - let
1.798 - fun relax cplexLe = cplexLeq
1.799 - | relax cplexGe = cplexGeq
1.800 - | relax x = x
1.801 -
1.802 - fun relax_constr (n, cplexConstr(c, (t1, t2))) =
1.803 - (n, cplexConstr(relax c, (t1, t2)))
1.804 -
1.805 - fun relax_bounds (cplexBounds (t1, c1, t2, c2, t3)) =
1.806 - cplexBounds (t1, relax c1, t2, relax c2, t3)
1.807 - | relax_bounds (cplexBound (t1, c, t2)) =
1.808 - cplexBound (t1, relax c, t2)
1.809 - in
1.810 - cplexProg (name,
1.811 - goals,
1.812 - map relax_constr constrs,
1.813 - map relax_bounds bounds)
1.814 - end
1.815 -
1.816 -datatype cplexResult = Unbounded
1.817 - | Infeasible
1.818 - | Undefined
1.819 - | Optimal of string * ((string * string) list)
1.820 -
1.821 -fun is_separator x = forall (fn c => c = #"-") (String.explode x)
1.822 -
1.823 -fun is_sign x = (x = "+" orelse x = "-")
1.824 -
1.825 -fun is_colon x = (x = ":")
1.826 -
1.827 -fun is_resultsymbol a =
1.828 - let
1.829 - val symbol_char = String.explode "!\"#$%&()/,.;?@_`'{}|~-"
1.830 - fun is_symbol_char c = Char.isAlphaNum c orelse
1.831 - exists (fn d => d=c) symbol_char
1.832 - fun is_symbol_start c = is_symbol_char c andalso
1.833 - not (Char.isDigit c) andalso
1.834 - not (c= #".") andalso
1.835 - not (c= #"-")
1.836 - val b = String.explode a
1.837 - in
1.838 - b <> [] andalso is_symbol_start (hd b) andalso
1.839 - forall is_symbol_char b
1.840 - end
1.841 -
1.842 -val TOKEN_SIGN = 100
1.843 -val TOKEN_COLON = 101
1.844 -val TOKEN_SEPARATOR = 102
1.845 -
1.846 -fun load_glpkResult name =
1.847 - let
1.848 - val flist = [(is_NL, TOKEN_NL),
1.849 - (is_blank, TOKEN_BLANK),
1.850 - (is_num, TOKEN_NUM),
1.851 - (is_sign, TOKEN_SIGN),
1.852 - (is_colon, TOKEN_COLON),
1.853 - (is_cmp, TOKEN_CMP),
1.854 - (is_resultsymbol, TOKEN_SYMBOL),
1.855 - (is_separator, TOKEN_SEPARATOR)]
1.856 -
1.857 - val tokenize = tokenize_general flist
1.858 -
1.859 - val f = TextIO.openIn name
1.860 -
1.861 - val rest = Unsynchronized.ref []
1.862 -
1.863 - fun readToken_helper () =
1.864 - if length (!rest) > 0 then
1.865 - let val u = hd (!rest) in
1.866 - (
1.867 - rest := tl (!rest);
1.868 - SOME u
1.869 - )
1.870 - end
1.871 - else
1.872 - (case TextIO.inputLine f of
1.873 - NONE => NONE
1.874 - | SOME s => (rest := tokenize s; readToken_helper()))
1.875 -
1.876 - fun is_tt tok ty = (tok <> NONE andalso (fst (the tok)) = ty)
1.877 -
1.878 - fun pushToken a = if a = NONE then () else (rest := ((the a)::(!rest)))
1.879 -
1.880 - fun readToken () =
1.881 - let val t = readToken_helper () in
1.882 - if is_tt t TOKEN_BLANK then
1.883 - readToken ()
1.884 - else if is_tt t TOKEN_NL then
1.885 - let val t2 = readToken_helper () in
1.886 - if is_tt t2 TOKEN_SIGN then
1.887 - (pushToken (SOME (TOKEN_SEPARATOR, "-")); t)
1.888 - else
1.889 - (pushToken t2; t)
1.890 - end
1.891 - else if is_tt t TOKEN_SIGN then
1.892 - let val t2 = readToken_helper () in
1.893 - if is_tt t2 TOKEN_NUM then
1.894 - (SOME (TOKEN_NUM, (snd (the t))^(snd (the t2))))
1.895 - else
1.896 - (pushToken t2; t)
1.897 - end
1.898 - else
1.899 - t
1.900 - end
1.901 -
1.902 - fun readRestOfLine P =
1.903 - let
1.904 - val t = readToken ()
1.905 - in
1.906 - if is_tt t TOKEN_NL orelse t = NONE
1.907 - then P
1.908 - else readRestOfLine P
1.909 - end
1.910 -
1.911 - fun readHeader () =
1.912 - let
1.913 - fun readStatus () = readRestOfLine ("STATUS", snd (the (readToken ())))
1.914 - fun readObjective () = readRestOfLine ("OBJECTIVE", snd (the (readToken (); readToken (); readToken ())))
1.915 - val t1 = readToken ()
1.916 - val t2 = readToken ()
1.917 - in
1.918 - if is_tt t1 TOKEN_SYMBOL andalso is_tt t2 TOKEN_COLON
1.919 - then
1.920 - case to_upper (snd (the t1)) of
1.921 - "STATUS" => (readStatus ())::(readHeader ())
1.922 - | "OBJECTIVE" => (readObjective())::(readHeader ())
1.923 - | _ => (readRestOfLine (); readHeader ())
1.924 - else
1.925 - (pushToken t2; pushToken t1; [])
1.926 - end
1.927 -
1.928 - fun skip_until_sep () =
1.929 - let val x = readToken () in
1.930 - if is_tt x TOKEN_SEPARATOR then
1.931 - readRestOfLine ()
1.932 - else
1.933 - skip_until_sep ()
1.934 - end
1.935 -
1.936 - fun load_value () =
1.937 - let
1.938 - val t1 = readToken ()
1.939 - val t2 = readToken ()
1.940 - in
1.941 - if is_tt t1 TOKEN_NUM andalso is_tt t2 TOKEN_SYMBOL then
1.942 - let
1.943 - val t = readToken ()
1.944 - val state = if is_tt t TOKEN_NL then readToken () else t
1.945 - val _ = if is_tt state TOKEN_SYMBOL then () else raise (Load_cplexResult "state expected")
1.946 - val k = readToken ()
1.947 - in
1.948 - if is_tt k TOKEN_NUM then
1.949 - readRestOfLine (SOME (snd (the t2), snd (the k)))
1.950 - else
1.951 - raise (Load_cplexResult "number expected")
1.952 - end
1.953 - else
1.954 - (pushToken t2; pushToken t1; NONE)
1.955 - end
1.956 -
1.957 - fun load_values () =
1.958 - let val v = load_value () in
1.959 - if v = NONE then [] else (the v)::(load_values ())
1.960 - end
1.961 -
1.962 - val header = readHeader ()
1.963 -
1.964 - val result =
1.965 - case AList.lookup (op =) header "STATUS" of
1.966 - SOME "INFEASIBLE" => Infeasible
1.967 - | SOME "UNBOUNDED" => Unbounded
1.968 - | SOME "OPTIMAL" => Optimal (the (AList.lookup (op =) header "OBJECTIVE"),
1.969 - (skip_until_sep ();
1.970 - skip_until_sep ();
1.971 - load_values ()))
1.972 - | _ => Undefined
1.973 -
1.974 - val _ = TextIO.closeIn f
1.975 - in
1.976 - result
1.977 - end
1.978 - handle (Tokenize s) => raise (Load_cplexResult ("Tokenize: "^s))
1.979 - | Option => raise (Load_cplexResult "Option")
1.980 -
1.981 -fun load_cplexResult name =
1.982 - let
1.983 - val flist = [(is_NL, TOKEN_NL),
1.984 - (is_blank, TOKEN_BLANK),
1.985 - (is_num, TOKEN_NUM),
1.986 - (is_sign, TOKEN_SIGN),
1.987 - (is_colon, TOKEN_COLON),
1.988 - (is_cmp, TOKEN_CMP),
1.989 - (is_resultsymbol, TOKEN_SYMBOL)]
1.990 -
1.991 - val tokenize = tokenize_general flist
1.992 -
1.993 - val f = TextIO.openIn name
1.994 -
1.995 - val rest = Unsynchronized.ref []
1.996 -
1.997 - fun readToken_helper () =
1.998 - if length (!rest) > 0 then
1.999 - let val u = hd (!rest) in
1.1000 - (
1.1001 - rest := tl (!rest);
1.1002 - SOME u
1.1003 - )
1.1004 - end
1.1005 - else
1.1006 - (case TextIO.inputLine f of
1.1007 - NONE => NONE
1.1008 - | SOME s => (rest := tokenize s; readToken_helper()))
1.1009 -
1.1010 - fun is_tt tok ty = (tok <> NONE andalso (fst (the tok)) = ty)
1.1011 -
1.1012 - fun pushToken a = if a = NONE then () else (rest := ((the a)::(!rest)))
1.1013 -
1.1014 - fun readToken () =
1.1015 - let val t = readToken_helper () in
1.1016 - if is_tt t TOKEN_BLANK then
1.1017 - readToken ()
1.1018 - else if is_tt t TOKEN_SIGN then
1.1019 - let val t2 = readToken_helper () in
1.1020 - if is_tt t2 TOKEN_NUM then
1.1021 - (SOME (TOKEN_NUM, (snd (the t))^(snd (the t2))))
1.1022 - else
1.1023 - (pushToken t2; t)
1.1024 - end
1.1025 - else
1.1026 - t
1.1027 - end
1.1028 -
1.1029 - fun readRestOfLine P =
1.1030 - let
1.1031 - val t = readToken ()
1.1032 - in
1.1033 - if is_tt t TOKEN_NL orelse t = NONE
1.1034 - then P
1.1035 - else readRestOfLine P
1.1036 - end
1.1037 -
1.1038 - fun readHeader () =
1.1039 - let
1.1040 - fun readStatus () = readRestOfLine ("STATUS", snd (the (readToken ())))
1.1041 - fun readObjective () =
1.1042 - let
1.1043 - val t = readToken ()
1.1044 - in
1.1045 - if is_tt t TOKEN_SYMBOL andalso to_upper (snd (the t)) = "VALUE" then
1.1046 - readRestOfLine ("OBJECTIVE", snd (the (readToken())))
1.1047 - else
1.1048 - readRestOfLine ("OBJECTIVE_NAME", snd (the t))
1.1049 - end
1.1050 -
1.1051 - val t = readToken ()
1.1052 - in
1.1053 - if is_tt t TOKEN_SYMBOL then
1.1054 - case to_upper (snd (the t)) of
1.1055 - "STATUS" => (readStatus ())::(readHeader ())
1.1056 - | "OBJECTIVE" => (readObjective ())::(readHeader ())
1.1057 - | "SECTION" => (pushToken t; [])
1.1058 - | _ => (readRestOfLine (); readHeader ())
1.1059 - else
1.1060 - (readRestOfLine (); readHeader ())
1.1061 - end
1.1062 -
1.1063 - fun skip_nls () =
1.1064 - let val x = readToken () in
1.1065 - if is_tt x TOKEN_NL then
1.1066 - skip_nls ()
1.1067 - else
1.1068 - (pushToken x; ())
1.1069 - end
1.1070 -
1.1071 - fun skip_paragraph () =
1.1072 - if is_tt (readToken ()) TOKEN_NL then
1.1073 - (if is_tt (readToken ()) TOKEN_NL then
1.1074 - skip_nls ()
1.1075 - else
1.1076 - skip_paragraph ())
1.1077 - else
1.1078 - skip_paragraph ()
1.1079 -
1.1080 - fun load_value () =
1.1081 - let
1.1082 - val t1 = readToken ()
1.1083 - val t1 = if is_tt t1 TOKEN_SYMBOL andalso snd (the t1) = "A" then readToken () else t1
1.1084 - in
1.1085 - if is_tt t1 TOKEN_NUM then
1.1086 - let
1.1087 - val name = readToken ()
1.1088 - val status = readToken ()
1.1089 - val value = readToken ()
1.1090 - in
1.1091 - if is_tt name TOKEN_SYMBOL andalso
1.1092 - is_tt status TOKEN_SYMBOL andalso
1.1093 - is_tt value TOKEN_NUM
1.1094 - then
1.1095 - readRestOfLine (SOME (snd (the name), snd (the value)))
1.1096 - else
1.1097 - raise (Load_cplexResult "column line expected")
1.1098 - end
1.1099 - else
1.1100 - (pushToken t1; NONE)
1.1101 - end
1.1102 -
1.1103 - fun load_values () =
1.1104 - let val v = load_value () in
1.1105 - if v = NONE then [] else (the v)::(load_values ())
1.1106 - end
1.1107 -
1.1108 - val header = readHeader ()
1.1109 -
1.1110 - val result =
1.1111 - case AList.lookup (op =) header "STATUS" of
1.1112 - SOME "INFEASIBLE" => Infeasible
1.1113 - | SOME "NONOPTIMAL" => Unbounded
1.1114 - | SOME "OPTIMAL" => Optimal (the (AList.lookup (op =) header "OBJECTIVE"),
1.1115 - (skip_paragraph ();
1.1116 - skip_paragraph ();
1.1117 - skip_paragraph ();
1.1118 - skip_paragraph ();
1.1119 - skip_paragraph ();
1.1120 - load_values ()))
1.1121 - | _ => Undefined
1.1122 -
1.1123 - val _ = TextIO.closeIn f
1.1124 - in
1.1125 - result
1.1126 - end
1.1127 - handle (Tokenize s) => raise (Load_cplexResult ("Tokenize: "^s))
1.1128 - | Option => raise (Load_cplexResult "Option")
1.1129 -
1.1130 -exception Execute of string;
1.1131 -
1.1132 -fun tmp_file s = Path.implode (Path.expand (File.tmp_path (Path.basic s)));
1.1133 -fun wrap s = "\""^s^"\"";
1.1134 -
1.1135 -fun solve_glpk prog =
1.1136 - let
1.1137 - val name = string_of_int (Time.toMicroseconds (Time.now ()))
1.1138 - val lpname = tmp_file (name^".lp")
1.1139 - val resultname = tmp_file (name^".txt")
1.1140 - val _ = save_cplexFile lpname prog
1.1141 - val cplex_path = getenv "GLPK_PATH"
1.1142 - val cplex = if cplex_path = "" then "glpsol" else cplex_path
1.1143 - val command = (wrap cplex)^" --lpt "^(wrap lpname)^" --output "^(wrap resultname)
1.1144 - val answer = #1 (Isabelle_System.bash_output command)
1.1145 - in
1.1146 - let
1.1147 - val result = load_glpkResult resultname
1.1148 - val _ = OS.FileSys.remove lpname
1.1149 - val _ = OS.FileSys.remove resultname
1.1150 - in
1.1151 - result
1.1152 - end
1.1153 - handle (Load_cplexResult s) => raise (Execute ("Load_cplexResult: "^s^"\nExecute: "^answer))
1.1154 - | _ => raise (Execute answer) (* FIXME avoid handle _ *)
1.1155 - end
1.1156 -
1.1157 -fun solve_cplex prog =
1.1158 - let
1.1159 - fun write_script s lp r =
1.1160 - let
1.1161 - val f = TextIO.openOut s
1.1162 - val _ = TextIO.output (f, "read\n"^lp^"\noptimize\nwrite\n"^r^"\nquit")
1.1163 - val _ = TextIO.closeOut f
1.1164 - in
1.1165 - ()
1.1166 - end
1.1167 -
1.1168 - val name = string_of_int (Time.toMicroseconds (Time.now ()))
1.1169 - val lpname = tmp_file (name^".lp")
1.1170 - val resultname = tmp_file (name^".txt")
1.1171 - val scriptname = tmp_file (name^".script")
1.1172 - val _ = save_cplexFile lpname prog
1.1173 - val _ = write_script scriptname lpname resultname
1.1174 - in
1.1175 - let
1.1176 - val result = load_cplexResult resultname
1.1177 - val _ = OS.FileSys.remove lpname
1.1178 - val _ = OS.FileSys.remove resultname
1.1179 - val _ = OS.FileSys.remove scriptname
1.1180 - in
1.1181 - result
1.1182 - end
1.1183 - end
1.1184 -
1.1185 -fun solve prog =
1.1186 - case get_solver () of
1.1187 - SOLVER_DEFAULT =>
1.1188 - (case getenv "LP_SOLVER" of
1.1189 - "CPLEX" => solve_cplex prog
1.1190 - | "GLPK" => solve_glpk prog
1.1191 - | _ => raise (Execute ("LP_SOLVER must be set to CPLEX or to GLPK")))
1.1192 - | SOLVER_CPLEX => solve_cplex prog
1.1193 - | SOLVER_GLPK => solve_glpk prog
1.1194 -
1.1195 -end;