author  wenzelm 
Sat, 07 Apr 2012 16:41:59 +0200  
changeset 47389  e8552cba702d 
parent 46988  9f492f5b0cec 
child 47455  26315a545e26 
permissions  rwrr 
37788  1 
(* Title: HOL/Matrix/Cplex_tools.ML 
16784  2 
Author: Steven Obua 
3 
*) 

4 

5 
signature CPLEX = 

6 
sig 

22951  7 

8 
datatype cplexTerm = cplexVar of string  cplexNum of string  cplexInf 

9 
 cplexNeg of cplexTerm 

10 
 cplexProd of cplexTerm * cplexTerm 

11 
 cplexSum of (cplexTerm list) 

12 

13 
datatype cplexComp = cplexLe  cplexLeq  cplexEq  cplexGe  cplexGeq 

14 

15 
datatype cplexGoal = cplexMinimize of cplexTerm 

16 
 cplexMaximize of cplexTerm 

17 

18 
datatype cplexConstr = cplexConstr of cplexComp * 

19 
(cplexTerm * cplexTerm) 

20 

21 
datatype cplexBounds = cplexBounds of cplexTerm * cplexComp * cplexTerm 

22 
* cplexComp * cplexTerm 

23 
 cplexBound of cplexTerm * cplexComp * cplexTerm 

24 

25 
datatype cplexProg = cplexProg of string 

26 
* cplexGoal 

27 
* ((string option * cplexConstr) 

28 
list) 

29 
* cplexBounds list 

30 

31 
datatype cplexResult = Unbounded 

32 
 Infeasible 

33 
 Undefined 

34 
 Optimal of string * 

35 
(((* name *) string * 

36 
(* value *) string) list) 

16966
37e34f315057
1. changed configuration variables for linear programming (Cplex_tools):
obua
parents:
16873
diff
changeset

37 

37e34f315057
1. changed configuration variables for linear programming (Cplex_tools):
obua
parents:
16873
diff
changeset

38 
datatype cplexSolver = SOLVER_DEFAULT  SOLVER_CPLEX  SOLVER_GLPK 
22951  39 

16784  40 
exception Load_cplexFile of string 
41 
exception Load_cplexResult of string 

42 
exception Save_cplexFile of string 

43 
exception Execute of string 

44 

45 
val load_cplexFile : string > cplexProg 

46 

22951  47 
val save_cplexFile : string > cplexProg > unit 
16784  48 

49 
val elim_nonfree_bounds : cplexProg > cplexProg 

50 

51 
val relax_strict_ineqs : cplexProg > cplexProg 

52 

53 
val is_normed_cplexProg : cplexProg > bool 

54 

16966
37e34f315057
1. changed configuration variables for linear programming (Cplex_tools):
obua
parents:
16873
diff
changeset

55 
val get_solver : unit > cplexSolver 
37e34f315057
1. changed configuration variables for linear programming (Cplex_tools):
obua
parents:
16873
diff
changeset

56 
val set_solver : cplexSolver > unit 
16784  57 
val solve : cplexProg > cplexResult 
58 
end; 

59 

60 
structure Cplex : CPLEX = 

61 
struct 

62 

16966
37e34f315057
1. changed configuration variables for linear programming (Cplex_tools):
obua
parents:
16873
diff
changeset

63 
datatype cplexSolver = SOLVER_DEFAULT  SOLVER_CPLEX  SOLVER_GLPK 
37e34f315057
1. changed configuration variables for linear programming (Cplex_tools):
obua
parents:
16873
diff
changeset

64 

32740  65 
val cplexsolver = Unsynchronized.ref SOLVER_DEFAULT; 
16966
37e34f315057
1. changed configuration variables for linear programming (Cplex_tools):
obua
parents:
16873
diff
changeset

66 
fun get_solver () = !cplexsolver; 
37e34f315057
1. changed configuration variables for linear programming (Cplex_tools):
obua
parents:
16873
diff
changeset

67 
fun set_solver s = (cplexsolver := s); 
37e34f315057
1. changed configuration variables for linear programming (Cplex_tools):
obua
parents:
16873
diff
changeset

68 

16784  69 
exception Load_cplexFile of string; 
70 
exception Load_cplexResult of string; 

71 
exception Save_cplexFile of string; 

22951  72 

73 
datatype cplexTerm = cplexVar of string 

74 
 cplexNum of string 

75 
 cplexInf 

76 
 cplexNeg of cplexTerm 

77 
 cplexProd of cplexTerm * cplexTerm 

78 
 cplexSum of (cplexTerm list) 

79 
datatype cplexComp = cplexLe  cplexLeq  cplexEq  cplexGe  cplexGeq 

16784  80 
datatype cplexGoal = cplexMinimize of cplexTerm  cplexMaximize of cplexTerm 
81 
datatype cplexConstr = cplexConstr of cplexComp * (cplexTerm * cplexTerm) 

22951  82 
datatype cplexBounds = cplexBounds of cplexTerm * cplexComp * cplexTerm 
83 
* cplexComp * cplexTerm 

84 
 cplexBound of cplexTerm * cplexComp * cplexTerm 

85 
datatype cplexProg = cplexProg of string 

86 
* cplexGoal 

87 
* ((string option * cplexConstr) list) 

88 
* cplexBounds list 

89 

16784  90 
fun rev_cmp cplexLe = cplexGe 
91 
 rev_cmp cplexLeq = cplexGeq 

92 
 rev_cmp cplexGe = cplexLe 

93 
 rev_cmp cplexGeq = cplexLeq 

94 
 rev_cmp cplexEq = cplexEq 

95 

96 
fun the NONE = raise (Load_cplexFile "SOME expected") 

22951  97 
 the (SOME x) = x; 
98 

16784  99 
fun modulo_signed is_something (cplexNeg u) = is_something u 
100 
 modulo_signed is_something u = is_something u 

101 

102 
fun is_Num (cplexNum _) = true 

103 
 is_Num _ = false 

104 

105 
fun is_Inf cplexInf = true 

106 
 is_Inf _ = false 

107 

108 
fun is_Var (cplexVar _) = true 

109 
 is_Var _ = false 

110 

46531  111 
fun is_Neg (cplexNeg _) = true 
16784  112 
 is_Neg _ = false 
113 

22951  114 
fun is_normed_Prod (cplexProd (t1, t2)) = 
16784  115 
(is_Num t1) andalso (is_Var t2) 
116 
 is_normed_Prod x = is_Var x 

117 

22951  118 
fun is_normed_Sum (cplexSum ts) = 
16784  119 
(ts <> []) andalso forall (modulo_signed is_normed_Prod) ts 
120 
 is_normed_Sum x = modulo_signed is_normed_Prod x 

121 

46531  122 
fun is_normed_Constr (cplexConstr (_, (t1, t2))) = 
16784  123 
(is_normed_Sum t1) andalso (modulo_signed is_Num t2) 
124 

125 
fun is_Num_or_Inf x = is_Inf x orelse is_Num x 

126 

127 
fun is_normed_Bounds (cplexBounds (t1, c1, t2, c2, t3)) = 

22951  128 
(c1 = cplexLe orelse c1 = cplexLeq) andalso 
16784  129 
(c2 = cplexLe orelse c2 = cplexLeq) andalso 
130 
is_Var t2 andalso 

131 
modulo_signed is_Num_or_Inf t1 andalso 

132 
modulo_signed is_Num_or_Inf t3 

133 
 is_normed_Bounds (cplexBound (t1, c, t2)) = 

22951  134 
(is_Var t1 andalso (modulo_signed is_Num_or_Inf t2)) 
16784  135 
orelse 
22951  136 
(c <> cplexEq andalso 
16784  137 
is_Var t2 andalso (modulo_signed is_Num_or_Inf t1)) 
22951  138 

16784  139 
fun term_of_goal (cplexMinimize x) = x 
140 
 term_of_goal (cplexMaximize x) = x 

141 

46531  142 
fun is_normed_cplexProg (cplexProg (_, goal, constraints, bounds)) = 
16784  143 
is_normed_Sum (term_of_goal goal) andalso 
144 
forall (fn (_,x) => is_normed_Constr x) constraints andalso 

145 
forall is_normed_Bounds bounds 

146 

147 
fun is_NL s = s = "\n" 

148 

149 
fun is_blank s = forall (fn c => c <> #"\n" andalso Char.isSpace c) (String.explode s) 

22951  150 

151 
fun is_num a = 

152 
let 

153 
val b = String.explode a 

154 
fun num4 cs = forall Char.isDigit cs 

155 
fun num3 [] = true 

156 
 num3 (ds as (c::cs)) = 

157 
if c = #"+" orelse c = #"" then 

158 
num4 cs 

159 
else 

160 
num4 ds 

161 
fun num2 [] = true 

162 
 num2 (c::cs) = 

163 
if c = #"e" orelse c = #"E" then num3 cs 

164 
else (Char.isDigit c) andalso num2 cs 

165 
fun num1 [] = true 

166 
 num1 (c::cs) = 

167 
if c = #"." then num2 cs 

168 
else if c = #"e" orelse c = #"E" then num3 cs 

169 
else (Char.isDigit c) andalso num1 cs 

170 
fun num [] = true 

171 
 num (c::cs) = 

172 
if c = #"." then num2 cs 

173 
else (Char.isDigit c) andalso num1 cs 

16784  174 
in 
22951  175 
num b 
176 
end 

16784  177 

178 
fun is_delimiter s = s = "+" orelse s = "" orelse s = ":" 

179 

22951  180 
fun is_cmp s = s = "<" orelse s = ">" orelse s = "<=" 
181 
orelse s = ">=" orelse s = "=" 

182 

183 
fun is_symbol a = 

16784  184 
let 
22951  185 
val symbol_char = String.explode "!\"#$%&()/,.;?@_`'{}~" 
186 
fun is_symbol_char c = Char.isAlphaNum c orelse 

187 
exists (fn d => d=c) symbol_char 

188 
fun is_symbol_start c = is_symbol_char c andalso 

189 
not (Char.isDigit c) andalso 

190 
not (c= #".") 

191 
val b = String.explode a 

16784  192 
in 
22951  193 
b <> [] andalso is_symbol_start (hd b) andalso 
194 
forall is_symbol_char b 

16784  195 
end 
196 

197 
fun to_upper s = String.implode (map Char.toUpper (String.explode s)) 

198 

22951  199 
fun keyword x = 
200 
let 

201 
val a = to_upper x 

16784  202 
in 
22951  203 
if a = "BOUNDS" orelse a = "BOUND" then 
204 
SOME "BOUNDS" 

205 
else if a = "MINIMIZE" orelse a = "MINIMUM" orelse a = "MIN" then 

206 
SOME "MINIMIZE" 

207 
else if a = "MAXIMIZE" orelse a = "MAXIMUM" orelse a = "MAX" then 

208 
SOME "MAXIMIZE" 

209 
else if a = "ST" orelse a = "S.T." orelse a = "ST." then 

210 
SOME "ST" 

211 
else if a = "FREE" orelse a = "END" then 

212 
SOME a 

213 
else if a = "GENERAL" orelse a = "GENERALS" orelse a = "GEN" then 

214 
SOME "GENERAL" 

215 
else if a = "INTEGER" orelse a = "INTEGERS" orelse a = "INT" then 

216 
SOME "INTEGER" 

217 
else if a = "BINARY" orelse a = "BINARIES" orelse a = "BIN" then 

218 
SOME "BINARY" 

219 
else if a = "INF" orelse a = "INFINITY" then 

220 
SOME "INF" 

221 
else 

222 
NONE 

16784  223 
end 
22951  224 

16784  225 
val TOKEN_ERROR = ~1 
226 
val TOKEN_BLANK = 0 

227 
val TOKEN_NUM = 1 

228 
val TOKEN_DELIMITER = 2 

229 
val TOKEN_SYMBOL = 3 

230 
val TOKEN_LABEL = 4 

231 
val TOKEN_CMP = 5 

232 
val TOKEN_KEYWORD = 6 

233 
val TOKEN_NL = 7 

22951  234 

16784  235 
(* tokenize takes a list of chars as argument and returns a list of 
22951  236 
int * string pairs, each string representing a "cplex token", 
16784  237 
and each int being one of TOKEN_NUM, TOKEN_DELIMITER, TOKEN_CMP 
238 
or TOKEN_SYMBOL *) 

22951  239 
fun tokenize s = 
16784  240 
let 
22951  241 
val flist = [(is_NL, TOKEN_NL), 
242 
(is_blank, TOKEN_BLANK), 

243 
(is_num, TOKEN_NUM), 

244 
(is_delimiter, TOKEN_DELIMITER), 

245 
(is_cmp, TOKEN_CMP), 

246 
(is_symbol, TOKEN_SYMBOL)] 

46531  247 
fun match_helper [] s = (fn _ => false, TOKEN_ERROR) 
22951  248 
 match_helper (f::fs) s = 
249 
if ((fst f) s) then f else match_helper fs s 

250 
fun match s = match_helper flist s 

251 
fun tok s = 

252 
if s = "" then [] else 

253 
let 

254 
val h = String.substring (s,0,1) 

255 
val (f, j) = match h 

256 
fun len i = 

257 
if size s = i then i 

258 
else if f (String.substring (s,0,i+1)) then 

259 
len (i+1) 

260 
else i 

261 
in 

262 
if j < 0 then 

263 
(if h = "\\" then [] 

264 
else raise (Load_cplexFile ("token expected, found: " 

265 
^s))) 

266 
else 

267 
let 

268 
val l = len 1 

269 
val u = String.substring (s,0,l) 

270 
val v = String.extract (s,l,NONE) 

271 
in 

272 
if j = 0 then tok v else (j, u) :: tok v 

273 
end 

274 
end 

16784  275 
in 
22951  276 
tok s 
16784  277 
end 
278 

279 
exception Tokenize of string; 

280 

22951  281 
fun tokenize_general flist s = 
16784  282 
let 
22951  283 
fun match_helper [] s = raise (Tokenize s) 
284 
 match_helper (f::fs) s = 

285 
if ((fst f) s) then f else match_helper fs s 

286 
fun match s = match_helper flist s 

287 
fun tok s = 

288 
if s = "" then [] else 

289 
let 

290 
val h = String.substring (s,0,1) 

291 
val (f, j) = match h 

292 
fun len i = 

293 
if size s = i then i 

294 
else if f (String.substring (s,0,i+1)) then 

295 
len (i+1) 

296 
else i 

297 
val l = len 1 

298 
in 

299 
(j, String.substring (s,0,l)) :: tok (String.extract (s,l,NONE)) 

300 
end 

16784  301 
in 
22951  302 
tok s 
16784  303 
end 
304 

22951  305 
fun load_cplexFile name = 
306 
let 

307 
val f = TextIO.openIn name 

32740  308 
val ignore_NL = Unsynchronized.ref true 
309 
val rest = Unsynchronized.ref [] 

22951  310 

311 
fun is_symbol s c = (fst c) = TOKEN_SYMBOL andalso (to_upper (snd c)) = s 

16784  312 

22951  313 
fun readToken_helper () = 
314 
if length (!rest) > 0 then 

315 
let val u = hd (!rest) in 

316 
( 

317 
rest := tl (!rest); 

318 
SOME u 

319 
) 

320 
end 

321 
else 

23139
aa899bce7c3b
TextIO.inputLine: use present SML B library version;
wenzelm
parents:
22951
diff
changeset

322 
(case TextIO.inputLine f of 
aa899bce7c3b
TextIO.inputLine: use present SML B library version;
wenzelm
parents:
22951
diff
changeset

323 
NONE => NONE 
aa899bce7c3b
TextIO.inputLine: use present SML B library version;
wenzelm
parents:
22951
diff
changeset

324 
 SOME s => 
22951  325 
let val t = tokenize s in 
326 
if (length t >= 2 andalso 

327 
snd(hd (tl t)) = ":") 

328 
then 

329 
rest := (TOKEN_LABEL, snd (hd t)) :: (tl (tl t)) 

330 
else if (length t >= 2) andalso is_symbol "SUBJECT" (hd (t)) 

331 
andalso is_symbol "TO" (hd (tl t)) 

332 
then 

333 
rest := (TOKEN_SYMBOL, "ST") :: (tl (tl t)) 

334 
else 

335 
rest := t; 

336 
readToken_helper () 

23139
aa899bce7c3b
TextIO.inputLine: use present SML B library version;
wenzelm
parents:
22951
diff
changeset

337 
end) 
22951  338 

339 
fun readToken_helper2 () = 

340 
let val c = readToken_helper () in 

341 
if c = NONE then NONE 

16784  342 
else if !ignore_NL andalso fst (the c) = TOKEN_NL then 
22951  343 
readToken_helper2 () 
344 
else if fst (the c) = TOKEN_SYMBOL 

345 
andalso keyword (snd (the c)) <> NONE 

346 
then SOME (TOKEN_KEYWORD, the (keyword (snd (the c)))) 

347 
else c 

348 
end 

349 

350 
fun readToken () = readToken_helper2 () 

351 

352 
fun pushToken a = rest := (a::(!rest)) 

353 

354 
fun is_value token = 

355 
fst token = TOKEN_NUM orelse (fst token = TOKEN_KEYWORD 

356 
andalso snd token = "INF") 

357 

358 
fun get_value token = 

359 
if fst token = TOKEN_NUM then 

360 
cplexNum (snd token) 

361 
else if fst token = TOKEN_KEYWORD andalso snd token = "INF" 

362 
then 

363 
cplexInf 

364 
else 

365 
raise (Load_cplexFile "num expected") 

16784  366 

22951  367 
fun readTerm_Product only_num = 
368 
let val c = readToken () in 

369 
if c = NONE then NONE 

370 
else if fst (the c) = TOKEN_SYMBOL 

371 
then ( 

372 
if only_num then (pushToken (the c); NONE) 

373 
else SOME (cplexVar (snd (the c))) 

374 
) 

375 
else if only_num andalso is_value (the c) then 

376 
SOME (get_value (the c)) 

377 
else if is_value (the c) then 

378 
let val t1 = get_value (the c) 

379 
val d = readToken () 

380 
in 

381 
if d = NONE then SOME t1 

382 
else if fst (the d) = TOKEN_SYMBOL then 

383 
SOME (cplexProd (t1, cplexVar (snd (the d)))) 

384 
else 

385 
(pushToken (the d); SOME t1) 

386 
end 

387 
else (pushToken (the c); NONE) 

388 
end 

389 

390 
fun readTerm_Signed only_signed only_num = 

391 
let 

392 
val c = readToken () 

393 
in 

394 
if c = NONE then NONE 

395 
else 

396 
let val d = the c in 

397 
if d = (TOKEN_DELIMITER, "+") then 

398 
readTerm_Product only_num 

399 
else if d = (TOKEN_DELIMITER, "") then 

400 
SOME (cplexNeg (the (readTerm_Product 

401 
only_num))) 

402 
else (pushToken d; 

403 
if only_signed then NONE 

404 
else readTerm_Product only_num) 

405 
end 

406 
end 

407 

408 
fun readTerm_Sum first_signed = 

409 
let val c = readTerm_Signed first_signed false in 

410 
if c = NONE then [] else (the c)::(readTerm_Sum true) 

411 
end 

412 

413 
fun readTerm () = 

414 
let val c = readTerm_Sum false in 

415 
if c = [] then NONE 

416 
else if tl c = [] then SOME (hd c) 

417 
else SOME (cplexSum c) 

418 
end 

419 

420 
fun readLabeledTerm () = 

421 
let val c = readToken () in 

422 
if c = NONE then (NONE, NONE) 

423 
else if fst (the c) = TOKEN_LABEL then 

424 
let val t = readTerm () in 

425 
if t = NONE then 

426 
raise (Load_cplexFile ("term after label "^ 

427 
(snd (the c))^ 

428 
" expected")) 

429 
else (SOME (snd (the c)), t) 

430 
end 

431 
else (pushToken (the c); (NONE, readTerm ())) 

432 
end 

433 

434 
fun readGoal () = 

435 
let 

436 
val g = readToken () 

437 
in 

438 
if g = SOME (TOKEN_KEYWORD, "MAXIMIZE") then 

439 
cplexMaximize (the (snd (readLabeledTerm ()))) 

440 
else if g = SOME (TOKEN_KEYWORD, "MINIMIZE") then 

441 
cplexMinimize (the (snd (readLabeledTerm ()))) 

442 
else raise (Load_cplexFile "MAXIMIZE or MINIMIZE expected") 

443 
end 

444 

445 
fun str2cmp b = 

446 
(case b of 

447 
"<" => cplexLe 

448 
 "<=" => cplexLeq 

449 
 ">" => cplexGe 

450 
 ">=" => cplexGeq 

16784  451 
 "=" => cplexEq 
22951  452 
 _ => raise (Load_cplexFile (b^" is no TOKEN_CMP"))) 
453 

454 
fun readConstraint () = 

455 
let 

456 
val t = readLabeledTerm () 

457 
fun make_constraint b t1 t2 = 

458 
cplexConstr 

459 
(str2cmp b, 

460 
(t1, t2)) 

461 
in 

462 
if snd t = NONE then NONE 

463 
else 

464 
let val c = readToken () in 

465 
if c = NONE orelse fst (the c) <> TOKEN_CMP 

466 
then raise (Load_cplexFile "TOKEN_CMP expected") 

467 
else 

468 
let val n = readTerm_Signed false true in 

469 
if n = NONE then 

470 
raise (Load_cplexFile "num expected") 

471 
else 

472 
SOME (fst t, 

473 
make_constraint (snd (the c)) 

474 
(the (snd t)) 

475 
(the n)) 

476 
end 

477 
end 

478 
end 

16784  479 

22951  480 
fun readST () = 
481 
let 

482 
fun readbody () = 

483 
let val t = readConstraint () in 

484 
if t = NONE then [] 

485 
else if (is_normed_Constr (snd (the t))) then 

486 
(the t)::(readbody ()) 

487 
else if (fst (the t) <> NONE) then 

488 
raise (Load_cplexFile 

489 
("constraint '"^(the (fst (the t)))^ 

490 
"'is not normed")) 

491 
else 

492 
raise (Load_cplexFile 

493 
"constraint is not normed") 

494 
end 

495 
in 

496 
if readToken () = SOME (TOKEN_KEYWORD, "ST") 

497 
then 

498 
readbody () 

499 
else 

500 
raise (Load_cplexFile "ST expected") 

501 
end 

502 

503 
fun readCmp () = 

504 
let val c = readToken () in 

505 
if c = NONE then NONE 

506 
else if fst (the c) = TOKEN_CMP then 

507 
SOME (str2cmp (snd (the c))) 

508 
else (pushToken (the c); NONE) 

509 
end 

510 

511 
fun skip_NL () = 

512 
let val c = readToken () in 

513 
if c <> NONE andalso fst (the c) = TOKEN_NL then 

514 
skip_NL () 

515 
else 

516 
(pushToken (the c); ()) 

517 
end 

518 

519 
fun make_bounds c t1 t2 = 

520 
cplexBound (t1, c, t2) 

16784  521 

22951  522 
fun readBound () = 
523 
let 

524 
val _ = skip_NL () 

525 
val t1 = readTerm () 

526 
in 

527 
if t1 = NONE then NONE 

528 
else 

529 
let 

530 
val c1 = readCmp () 

531 
in 

532 
if c1 = NONE then 

533 
let 

534 
val c = readToken () 

535 
in 

536 
if c = SOME (TOKEN_KEYWORD, "FREE") then 

537 
SOME ( 

538 
cplexBounds (cplexNeg cplexInf, 

539 
cplexLeq, 

540 
the t1, 

541 
cplexLeq, 

542 
cplexInf)) 

543 
else 

544 
raise (Load_cplexFile "FREE expected") 

545 
end 

546 
else 

547 
let 

548 
val t2 = readTerm () 

549 
in 

550 
if t2 = NONE then 

551 
raise (Load_cplexFile "term expected") 

552 
else 

553 
let val c2 = readCmp () in 

554 
if c2 = NONE then 

555 
SOME (make_bounds (the c1) 

556 
(the t1) 

557 
(the t2)) 

558 
else 

559 
SOME ( 

560 
cplexBounds (the t1, 

561 
the c1, 

562 
the t2, 

563 
the c2, 

564 
the (readTerm()))) 

565 
end 

566 
end 

567 
end 

568 
end 

16784  569 

22951  570 
fun readBounds () = 
571 
let 

46531  572 
fun makestring _ = "?" 
22951  573 
fun readbody () = 
574 
let 

575 
val b = readBound () 

576 
in 

577 
if b = NONE then [] 

578 
else if (is_normed_Bounds (the b)) then 

579 
(the b)::(readbody()) 

580 
else ( 

581 
raise (Load_cplexFile 

582 
("bounds are not normed in: "^ 

583 
(makestring (the b))))) 

584 
end 

585 
in 

586 
if readToken () = SOME (TOKEN_KEYWORD, "BOUNDS") then 

587 
readbody () 

588 
else raise (Load_cplexFile "BOUNDS expected") 

589 
end 

590 

591 
fun readEnd () = 

592 
if readToken () = SOME (TOKEN_KEYWORD, "END") then () 

593 
else raise (Load_cplexFile "END expected") 

594 

595 
val result_Goal = readGoal () 

596 
val result_ST = readST () 

597 
val _ = ignore_NL := false 

16784  598 
val result_Bounds = readBounds () 
599 
val _ = ignore_NL := true 

600 
val _ = readEnd () 

22951  601 
val _ = TextIO.closeIn f 
16784  602 
in 
22951  603 
cplexProg (name, result_Goal, result_ST, result_Bounds) 
16784  604 
end 
605 

46531  606 
fun save_cplexFile filename (cplexProg (_, goal, constraints, bounds)) = 
16784  607 
let 
22951  608 
val f = TextIO.openOut filename 
609 

610 
fun basic_write s = TextIO.output(f, s) 

16784  611 

32740  612 
val linebuf = Unsynchronized.ref "" 
22951  613 
fun buf_flushline s = 
614 
(basic_write (!linebuf); 

615 
basic_write "\n"; 

616 
linebuf := s) 

617 
fun buf_add s = linebuf := (!linebuf) ^ s 

16784  618 

22951  619 
fun write s = 
620 
if (String.size s) + (String.size (!linebuf)) >= 250 then 

621 
buf_flushline (" "^s) 

622 
else 

623 
buf_add s 

16784  624 

625 
fun writeln s = (buf_add s; buf_flushline "") 

22951  626 

627 
fun write_term (cplexVar x) = write x 

628 
 write_term (cplexNum x) = write x 

629 
 write_term cplexInf = write "inf" 

630 
 write_term (cplexProd (cplexNum "1", b)) = write_term b 

631 
 write_term (cplexProd (a, b)) = 

632 
(write_term a; write " "; write_term b) 

16784  633 
 write_term (cplexNeg x) = (write "  "; write_term x) 
634 
 write_term (cplexSum ts) = write_terms ts 

22951  635 
and write_terms [] = () 
636 
 write_terms (t::ts) = 

637 
(if (not (is_Neg t)) then write " + " else (); 

638 
write_term t; write_terms ts) 

639 

640 
fun write_goal (cplexMaximize term) = 

641 
(writeln "MAXIMIZE"; write_term term; writeln "") 

642 
 write_goal (cplexMinimize term) = 

643 
(writeln "MINIMIZE"; write_term term; writeln "") 

16784  644 

22951  645 
fun write_cmp cplexLe = write "<" 
646 
 write_cmp cplexLeq = write "<=" 

647 
 write_cmp cplexEq = write "=" 

648 
 write_cmp cplexGe = write ">" 

649 
 write_cmp cplexGeq = write ">=" 

650 

651 
fun write_constr (cplexConstr (cmp, (a,b))) = 

652 
(write_term a; 

653 
write " "; 

654 
write_cmp cmp; 

655 
write " "; 

656 
write_term b) 

16784  657 

22951  658 
fun write_constraints [] = () 
659 
 write_constraints (c::cs) = 

660 
(if (fst c <> NONE) 

661 
then 

662 
(write (the (fst c)); write ": ") 

663 
else 

664 
(); 

665 
write_constr (snd c); 

666 
writeln ""; 

667 
write_constraints cs) 

16784  668 

22951  669 
fun write_bounds [] = () 
670 
 write_bounds ((cplexBounds (t1,c1,t2,c2,t3))::bs) = 

671 
((if t1 = cplexNeg cplexInf andalso t3 = cplexInf 

672 
andalso (c1 = cplexLeq orelse c1 = cplexLe) 

673 
andalso (c2 = cplexLeq orelse c2 = cplexLe) 

674 
then 

675 
(write_term t2; write " free") 

676 
else 

677 
(write_term t1; write " "; write_cmp c1; write " "; 

678 
write_term t2; write " "; write_cmp c2; write " "; 

679 
write_term t3) 

680 
); writeln ""; write_bounds bs) 

681 
 write_bounds ((cplexBound (t1, c, t2)) :: bs) = 

682 
(write_term t1; write " "; 

683 
write_cmp c; write " "; 

684 
write_term t2; writeln ""; write_bounds bs) 

685 

686 
val _ = write_goal goal 

16784  687 
val _ = (writeln ""; writeln "ST") 
22951  688 
val _ = write_constraints constraints 
16784  689 
val _ = (writeln ""; writeln "BOUNDS") 
22951  690 
val _ = write_bounds bounds 
691 
val _ = (writeln ""; writeln "END") 

16784  692 
val _ = TextIO.closeOut f 
693 
in 

22951  694 
() 
16784  695 
end 
696 

22951  697 
fun norm_Constr (constr as cplexConstr (c, (t1, t2))) = 
698 
if not (modulo_signed is_Num t2) andalso 

699 
modulo_signed is_Num t1 

16784  700 
then 
22951  701 
[cplexConstr (rev_cmp c, (t2, t1))] 
16784  702 
else if (c = cplexLe orelse c = cplexLeq) andalso 
22951  703 
(t1 = (cplexNeg cplexInf) orelse t2 = cplexInf) 
704 
then 

705 
[] 

16784  706 
else if (c = cplexGe orelse c = cplexGeq) andalso 
22951  707 
(t1 = cplexInf orelse t2 = cplexNeg cplexInf) 
16784  708 
then 
22951  709 
[] 
16784  710 
else 
22951  711 
[constr] 
16784  712 

713 
fun bound2constr (cplexBounds (t1,c1,t2,c2,t3)) = 

714 
(norm_Constr(cplexConstr (c1, (t1, t2)))) 

715 
@ (norm_Constr(cplexConstr (c2, (t2, t3)))) 

716 
 bound2constr (cplexBound (t1, cplexEq, t2)) = 

717 
(norm_Constr(cplexConstr (cplexLeq, (t1, t2)))) 

718 
@ (norm_Constr(cplexConstr (cplexLeq, (t2, t1)))) 

22951  719 
 bound2constr (cplexBound (t1, c1, t2)) = 
16784  720 
norm_Constr(cplexConstr (c1, (t1,t2))) 
721 

722 
val emptyset = Symtab.empty 

723 

17412  724 
fun singleton v = Symtab.update (v, ()) emptyset 
16784  725 

726 
fun merge a b = Symtab.merge (op =) (a, b) 

727 

21056  728 
fun mergemap f ts = fold (fn x => fn table => merge table (f x)) ts Symtab.empty 
16784  729 

37116  730 
fun diff a b = Symtab.fold (Symtab.delete_safe o fst) b a 
22951  731 

16784  732 
fun collect_vars (cplexVar v) = singleton v 
733 
 collect_vars (cplexNeg t) = collect_vars t 

22951  734 
 collect_vars (cplexProd (t1, t2)) = 
16784  735 
merge (collect_vars t1) (collect_vars t2) 
736 
 collect_vars (cplexSum ts) = mergemap collect_vars ts 

737 
 collect_vars _ = emptyset 

738 

739 
(* Eliminates all nonfree bounds from the linear program and produces an 

22951  740 
equivalent program with only free bounds 
16784  741 
IF for the input program P holds: is_normed_cplexProg P *) 
742 
fun elim_nonfree_bounds (cplexProg (name, goal, constraints, bounds)) = 

743 
let 

46531  744 
fun collect_constr_vars (_, cplexConstr (_, (t1,_))) = 
22951  745 
(collect_vars t1) 
746 

747 
val cvars = merge (collect_vars (term_of_goal goal)) 

748 
(mergemap collect_constr_vars constraints) 

749 

750 
fun collect_lower_bounded_vars 

46531  751 
(cplexBounds (_, _, cplexVar v, _, _)) = 
22951  752 
singleton v 
753 
 collect_lower_bounded_vars 

754 
(cplexBound (_, cplexLe, cplexVar v)) = 

755 
singleton v 

756 
 collect_lower_bounded_vars 

757 
(cplexBound (_, cplexLeq, cplexVar v)) = 

758 
singleton v 

759 
 collect_lower_bounded_vars 

760 
(cplexBound (cplexVar v, cplexGe,_)) = 

761 
singleton v 

762 
 collect_lower_bounded_vars 

763 
(cplexBound (cplexVar v, cplexGeq, _)) = 

764 
singleton v 

765 
 collect_lower_bounded_vars 

766 
(cplexBound (cplexVar v, cplexEq, _)) = 

767 
singleton v 

768 
 collect_lower_bounded_vars _ = emptyset 

769 

770 
val lvars = mergemap collect_lower_bounded_vars bounds 

771 
val positive_vars = diff cvars lvars 

772 
val zero = cplexNum "0" 

773 

774 
fun make_pos_constr v = 

775 
(NONE, cplexConstr (cplexGeq, ((cplexVar v), zero))) 

776 

777 
fun make_free_bound v = 

778 
cplexBounds (cplexNeg cplexInf, cplexLeq, 

779 
cplexVar v, cplexLeq, 

780 
cplexInf) 

781 

782 
val pos_constrs = rev (Symtab.fold 

46531  783 
(fn (k, _) => cons (make_pos_constr k)) 
22951  784 
positive_vars []) 
21056  785 
val bound_constrs = map (pair NONE) 
22951  786 
(maps bound2constr bounds) 
787 
val constraints' = constraints @ pos_constrs @ bound_constrs 

788 
val bounds' = rev (Symtab.fold (fn (v, _) => cons (make_free_bound v)) cvars []); 

16784  789 
in 
22951  790 
cplexProg (name, goal, constraints', bounds') 
16784  791 
end 
792 

22951  793 
fun relax_strict_ineqs (cplexProg (name, goals, constrs, bounds)) = 
16784  794 
let 
22951  795 
fun relax cplexLe = cplexLeq 
796 
 relax cplexGe = cplexGeq 

797 
 relax x = x 

798 

799 
fun relax_constr (n, cplexConstr(c, (t1, t2))) = 

800 
(n, cplexConstr(relax c, (t1, t2))) 

801 

802 
fun relax_bounds (cplexBounds (t1, c1, t2, c2, t3)) = 

803 
cplexBounds (t1, relax c1, t2, relax c2, t3) 

804 
 relax_bounds (cplexBound (t1, c, t2)) = 

805 
cplexBound (t1, relax c, t2) 

16784  806 
in 
22951  807 
cplexProg (name, 
808 
goals, 

809 
map relax_constr constrs, 

810 
map relax_bounds bounds) 

16784  811 
end 
812 

22951  813 
datatype cplexResult = Unbounded 
814 
 Infeasible 

815 
 Undefined 

816 
 Optimal of string * ((string * string) list) 

16784  817 

818 
fun is_separator x = forall (fn c => c = #"") (String.explode x) 

819 

820 
fun is_sign x = (x = "+" orelse x = "") 

821 

822 
fun is_colon x = (x = ":") 

823 

22951  824 
fun is_resultsymbol a = 
16784  825 
let 
22951  826 
val symbol_char = String.explode "!\"#$%&()/,.;?@_`'{}~" 
827 
fun is_symbol_char c = Char.isAlphaNum c orelse 

828 
exists (fn d => d=c) symbol_char 

829 
fun is_symbol_start c = is_symbol_char c andalso 

830 
not (Char.isDigit c) andalso 

831 
not (c= #".") andalso 

832 
not (c= #"") 

833 
val b = String.explode a 

16784  834 
in 
22951  835 
b <> [] andalso is_symbol_start (hd b) andalso 
836 
forall is_symbol_char b 

16784  837 
end 
838 

839 
val TOKEN_SIGN = 100 

840 
val TOKEN_COLON = 101 

841 
val TOKEN_SEPARATOR = 102 

842 

22951  843 
fun load_glpkResult name = 
16784  844 
let 
22951  845 
val flist = [(is_NL, TOKEN_NL), 
846 
(is_blank, TOKEN_BLANK), 

847 
(is_num, TOKEN_NUM), 

848 
(is_sign, TOKEN_SIGN), 

16784  849 
(is_colon, TOKEN_COLON), 
22951  850 
(is_cmp, TOKEN_CMP), 
851 
(is_resultsymbol, TOKEN_SYMBOL), 

852 
(is_separator, TOKEN_SEPARATOR)] 

853 

854 
val tokenize = tokenize_general flist 

855 

856 
val f = TextIO.openIn name 

857 

32740  858 
val rest = Unsynchronized.ref [] 
16784  859 

22951  860 
fun readToken_helper () = 
861 
if length (!rest) > 0 then 

862 
let val u = hd (!rest) in 

863 
( 

864 
rest := tl (!rest); 

865 
SOME u 

866 
) 

867 
end 

868 
else 

23139
aa899bce7c3b
TextIO.inputLine: use present SML B library version;
wenzelm
parents:
22951
diff
changeset

869 
(case TextIO.inputLine f of 
aa899bce7c3b
TextIO.inputLine: use present SML B library version;
wenzelm
parents:
22951
diff
changeset

870 
NONE => NONE 
aa899bce7c3b
TextIO.inputLine: use present SML B library version;
wenzelm
parents:
22951
diff
changeset

871 
 SOME s => (rest := tokenize s; readToken_helper())) 
16784  872 

22951  873 
fun is_tt tok ty = (tok <> NONE andalso (fst (the tok)) = ty) 
16784  874 

22951  875 
fun pushToken a = if a = NONE then () else (rest := ((the a)::(!rest))) 
16784  876 

22951  877 
fun readToken () = 
878 
let val t = readToken_helper () in 

879 
if is_tt t TOKEN_BLANK then 

880 
readToken () 

881 
else if is_tt t TOKEN_NL then 

882 
let val t2 = readToken_helper () in 

883 
if is_tt t2 TOKEN_SIGN then 

884 
(pushToken (SOME (TOKEN_SEPARATOR, "")); t) 

885 
else 

886 
(pushToken t2; t) 

887 
end 

888 
else if is_tt t TOKEN_SIGN then 

889 
let val t2 = readToken_helper () in 

890 
if is_tt t2 TOKEN_NUM then 

891 
(SOME (TOKEN_NUM, (snd (the t))^(snd (the t2)))) 

892 
else 

893 
(pushToken t2; t) 

894 
end 

895 
else 

896 
t 

897 
end 

898 

899 
fun readRestOfLine P = 

900 
let 

901 
val t = readToken () 

902 
in 

903 
if is_tt t TOKEN_NL orelse t = NONE 

904 
then P 

905 
else readRestOfLine P 

906 
end 

16784  907 

22951  908 
fun readHeader () = 
909 
let 

910 
fun readStatus () = readRestOfLine ("STATUS", snd (the (readToken ()))) 

911 
fun readObjective () = readRestOfLine ("OBJECTIVE", snd (the (readToken (); readToken (); readToken ()))) 

912 
val t1 = readToken () 

913 
val t2 = readToken () 

914 
in 

915 
if is_tt t1 TOKEN_SYMBOL andalso is_tt t2 TOKEN_COLON 

916 
then 

917 
case to_upper (snd (the t1)) of 

918 
"STATUS" => (readStatus ())::(readHeader ()) 

919 
 "OBJECTIVE" => (readObjective())::(readHeader ()) 

920 
 _ => (readRestOfLine (); readHeader ()) 

921 
else 

922 
(pushToken t2; pushToken t1; []) 

923 
end 

16784  924 

22951  925 
fun skip_until_sep () = 
926 
let val x = readToken () in 

927 
if is_tt x TOKEN_SEPARATOR then 

928 
readRestOfLine () 

929 
else 

930 
skip_until_sep () 

931 
end 

16784  932 

22951  933 
fun load_value () = 
934 
let 

935 
val t1 = readToken () 

936 
val t2 = readToken () 

937 
in 

938 
if is_tt t1 TOKEN_NUM andalso is_tt t2 TOKEN_SYMBOL then 

939 
let 

940 
val t = readToken () 

941 
val state = if is_tt t TOKEN_NL then readToken () else t 

942 
val _ = if is_tt state TOKEN_SYMBOL then () else raise (Load_cplexResult "state expected") 

943 
val k = readToken () 

944 
in 

945 
if is_tt k TOKEN_NUM then 

946 
readRestOfLine (SOME (snd (the t2), snd (the k))) 

947 
else 

948 
raise (Load_cplexResult "number expected") 

949 
end 

950 
else 

951 
(pushToken t2; pushToken t1; NONE) 

952 
end 

16784  953 

22951  954 
fun load_values () = 
955 
let val v = load_value () in 

956 
if v = NONE then [] else (the v)::(load_values ()) 

957 
end 

958 

959 
val header = readHeader () 

16784  960 

22951  961 
val result = 
962 
case AList.lookup (op =) header "STATUS" of 

963 
SOME "INFEASIBLE" => Infeasible 

964 
 SOME "UNBOUNDED" => Unbounded 

965 
 SOME "OPTIMAL" => Optimal (the (AList.lookup (op =) header "OBJECTIVE"), 

966 
(skip_until_sep (); 

967 
skip_until_sep (); 

968 
load_values ())) 

969 
 _ => Undefined 

16784  970 

22951  971 
val _ = TextIO.closeIn f 
16784  972 
in 
22951  973 
result 
16784  974 
end 
975 
handle (Tokenize s) => raise (Load_cplexResult ("Tokenize: "^s)) 

22951  976 
 Option => raise (Load_cplexResult "Option") 
16784  977 

22951  978 
fun load_cplexResult name = 
16784  979 
let 
22951  980 
val flist = [(is_NL, TOKEN_NL), 
981 
(is_blank, TOKEN_BLANK), 

982 
(is_num, TOKEN_NUM), 

983 
(is_sign, TOKEN_SIGN), 

16784  984 
(is_colon, TOKEN_COLON), 
22951  985 
(is_cmp, TOKEN_CMP), 
986 
(is_resultsymbol, TOKEN_SYMBOL)] 

987 

988 
val tokenize = tokenize_general flist 

989 

990 
val f = TextIO.openIn name 

991 

32740  992 
val rest = Unsynchronized.ref [] 
16784  993 

22951  994 
fun readToken_helper () = 
995 
if length (!rest) > 0 then 

996 
let val u = hd (!rest) in 

997 
( 

998 
rest := tl (!rest); 

999 
SOME u 

1000 
) 

1001 
end 

1002 
else 

23139
aa899bce7c3b
TextIO.inputLine: use present SML B library version;
wenzelm
parents:
22951
diff
changeset

1003 
(case TextIO.inputLine f of 
aa899bce7c3b
TextIO.inputLine: use present SML B library version;
wenzelm
parents:
22951
diff
changeset

1004 
NONE => NONE 
aa899bce7c3b
TextIO.inputLine: use present SML B library version;
wenzelm
parents:
22951
diff
changeset

1005 
 SOME s => (rest := tokenize s; readToken_helper())) 
16784  1006 

22951  1007 
fun is_tt tok ty = (tok <> NONE andalso (fst (the tok)) = ty) 
16784  1008 

22951  1009 
fun pushToken a = if a = NONE then () else (rest := ((the a)::(!rest))) 
1010 

1011 
fun readToken () = 

1012 
let val t = readToken_helper () in 

1013 
if is_tt t TOKEN_BLANK then 

1014 
readToken () 

1015 
else if is_tt t TOKEN_SIGN then 

1016 
let val t2 = readToken_helper () in 

1017 
if is_tt t2 TOKEN_NUM then 

1018 
(SOME (TOKEN_NUM, (snd (the t))^(snd (the t2)))) 

1019 
else 

1020 
(pushToken t2; t) 

1021 
end 

1022 
else 

1023 
t 

1024 
end 

16784  1025 

22951  1026 
fun readRestOfLine P = 
1027 
let 

1028 
val t = readToken () 

1029 
in 

1030 
if is_tt t TOKEN_NL orelse t = NONE 

1031 
then P 

1032 
else readRestOfLine P 

1033 
end 

16784  1034 

22951  1035 
fun readHeader () = 
1036 
let 

1037 
fun readStatus () = readRestOfLine ("STATUS", snd (the (readToken ()))) 

1038 
fun readObjective () = 

1039 
let 

1040 
val t = readToken () 

1041 
in 

1042 
if is_tt t TOKEN_SYMBOL andalso to_upper (snd (the t)) = "VALUE" then 

1043 
readRestOfLine ("OBJECTIVE", snd (the (readToken()))) 

1044 
else 

1045 
readRestOfLine ("OBJECTIVE_NAME", snd (the t)) 

1046 
end 

16784  1047 

22951  1048 
val t = readToken () 
1049 
in 

1050 
if is_tt t TOKEN_SYMBOL then 

1051 
case to_upper (snd (the t)) of 

1052 
"STATUS" => (readStatus ())::(readHeader ()) 

1053 
 "OBJECTIVE" => (readObjective ())::(readHeader ()) 

1054 
 "SECTION" => (pushToken t; []) 

1055 
 _ => (readRestOfLine (); readHeader ()) 

1056 
else 

1057 
(readRestOfLine (); readHeader ()) 

1058 
end 

16784  1059 

22951  1060 
fun skip_nls () = 
1061 
let val x = readToken () in 

1062 
if is_tt x TOKEN_NL then 

1063 
skip_nls () 

1064 
else 

1065 
(pushToken x; ()) 

1066 
end 

16784  1067 

22951  1068 
fun skip_paragraph () = 
1069 
if is_tt (readToken ()) TOKEN_NL then 

1070 
(if is_tt (readToken ()) TOKEN_NL then 

1071 
skip_nls () 

1072 
else 

1073 
skip_paragraph ()) 

1074 
else 

1075 
skip_paragraph () 

16784  1076 

22951  1077 
fun load_value () = 
1078 
let 

1079 
val t1 = readToken () 

1080 
val t1 = if is_tt t1 TOKEN_SYMBOL andalso snd (the t1) = "A" then readToken () else t1 

1081 
in 

1082 
if is_tt t1 TOKEN_NUM then 

1083 
let 

1084 
val name = readToken () 

1085 
val status = readToken () 

1086 
val value = readToken () 

1087 
in 

1088 
if is_tt name TOKEN_SYMBOL andalso 

1089 
is_tt status TOKEN_SYMBOL andalso 

1090 
is_tt value TOKEN_NUM 

1091 
then 

1092 
readRestOfLine (SOME (snd (the name), snd (the value))) 

1093 
else 

1094 
raise (Load_cplexResult "column line expected") 

1095 
end 

1096 
else 

1097 
(pushToken t1; NONE) 

1098 
end 

16784  1099 

22951  1100 
fun load_values () = 
1101 
let val v = load_value () in 

1102 
if v = NONE then [] else (the v)::(load_values ()) 

1103 
end 

1104 

1105 
val header = readHeader () 

16784  1106 

22951  1107 
val result = 
1108 
case AList.lookup (op =) header "STATUS" of 

1109 
SOME "INFEASIBLE" => Infeasible 

1110 
 SOME "NONOPTIMAL" => Unbounded 

1111 
 SOME "OPTIMAL" => Optimal (the (AList.lookup (op =) header "OBJECTIVE"), 

1112 
(skip_paragraph (); 

1113 
skip_paragraph (); 

1114 
skip_paragraph (); 

1115 
skip_paragraph (); 

1116 
skip_paragraph (); 

1117 
load_values ())) 

1118 
 _ => Undefined 

16784  1119 

22951  1120 
val _ = TextIO.closeIn f 
16784  1121 
in 
22951  1122 
result 
16784  1123 
end 
1124 
handle (Tokenize s) => raise (Load_cplexResult ("Tokenize: "^s)) 

22951  1125 
 Option => raise (Load_cplexResult "Option") 
16784  1126 

1127 
exception Execute of string; 

1128 

43602  1129 
fun tmp_file s = Path.implode (Path.expand (File.tmp_path (Path.basic s))); 
16784  1130 
fun wrap s = "\""^s^"\""; 
1131 

1132 
fun solve_glpk prog = 

22951  1133 
let 
41491  1134 
val name = string_of_int (Time.toMicroseconds (Time.now ())) 
22951  1135 
val lpname = tmp_file (name^".lp") 
1136 
val resultname = tmp_file (name^".txt") 

1137 
val _ = save_cplexFile lpname prog 

1138 
val cplex_path = getenv "GLPK_PATH" 

1139 
val cplex = if cplex_path = "" then "glpsol" else cplex_path 

1140 
val command = (wrap cplex)^" lpt "^(wrap lpname)^" output "^(wrap resultname) 

43850
7f2cbc713344
moved bash operations to Isabelle_System (cf. Scala version);
wenzelm
parents:
43602
diff
changeset

1141 
val answer = #1 (Isabelle_System.bash_output command) 
16784  1142 
in 
22951  1143 
let 
1144 
val result = load_glpkResult resultname 

1145 
val _ = OS.FileSys.remove lpname 

1146 
val _ = OS.FileSys.remove resultname 

16784  1147 
in 
22951  1148 
result 
1149 
end 

1150 
handle (Load_cplexResult s) => raise (Execute ("Load_cplexResult: "^s^"\nExecute: "^answer)) 

40299  1151 
 _ => raise (Execute answer) (* FIXME avoid handle _ *) 
16784  1152 
end 
1153 

22951  1154 
fun solve_cplex prog = 
1155 
let 

1156 
fun write_script s lp r = 

1157 
let 

1158 
val f = TextIO.openOut s 

1159 
val _ = TextIO.output (f, "read\n"^lp^"\noptimize\nwrite\n"^r^"\nquit") 

1160 
val _ = TextIO.closeOut f 

1161 
in 

1162 
() 

1163 
end 

1164 

41491  1165 
val name = string_of_int (Time.toMicroseconds (Time.now ())) 
22951  1166 
val lpname = tmp_file (name^".lp") 
1167 
val resultname = tmp_file (name^".txt") 

1168 
val scriptname = tmp_file (name^".script") 

1169 
val _ = save_cplexFile lpname prog 

1170 
val _ = write_script scriptname lpname resultname 

1171 
in 

1172 
let 

1173 
val result = load_cplexResult resultname 

1174 
val _ = OS.FileSys.remove lpname 

1175 
val _ = OS.FileSys.remove resultname 

1176 
val _ = OS.FileSys.remove scriptname 

1177 
in 

1178 
result 

1179 
end 

1180 
end 

1181 

1182 
fun solve prog = 

16966
37e34f315057
1. changed configuration variables for linear programming (Cplex_tools):
obua
parents:
16873
diff
changeset

1183 
case get_solver () of 
22951  1184 
SOLVER_DEFAULT => 
16966
37e34f315057
1. changed configuration variables for linear programming (Cplex_tools):
obua
parents:
16873
diff
changeset

1185 
(case getenv "LP_SOLVER" of 
22951  1186 
"CPLEX" => solve_cplex prog 
16966
37e34f315057
1. changed configuration variables for linear programming (Cplex_tools):
obua
parents:
16873
diff
changeset

1187 
 "GLPK" => solve_glpk prog 
37e34f315057
1. changed configuration variables for linear programming (Cplex_tools):
obua
parents:
16873
diff
changeset

1188 
 _ => raise (Execute ("LP_SOLVER must be set to CPLEX or to GLPK"))) 
37e34f315057
1. changed configuration variables for linear programming (Cplex_tools):
obua
parents:
16873
diff
changeset

1189 
 SOLVER_CPLEX => solve_cplex prog 
37e34f315057
1. changed configuration variables for linear programming (Cplex_tools):
obua
parents:
16873
diff
changeset

1190 
 SOLVER_GLPK => solve_glpk prog 
22951  1191 

16784  1192 
end; 