author  haftmann 
Tue, 13 Jul 2010 11:38:04 +0200  
changeset 37788  261c61fabc98 
parent 37764  3489daf839d5 
child 40299  132e2349694b 
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 

111 
fun is_Neg (cplexNeg x ) = true 

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 

22951  122 
fun is_normed_Constr (cplexConstr (c, (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 

22951  142 
fun is_normed_cplexProg (cplexProg (name, 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)] 

247 
fun match_helper [] s = (fn x => false, TOKEN_ERROR) 

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 is_var (cplexVar _) = true 

520 
 is_var _ = false 

521 

522 
fun make_bounds c t1 t2 = 

523 
cplexBound (t1, c, t2) 

16784  524 

22951  525 
fun readBound () = 
526 
let 

527 
val _ = skip_NL () 

528 
val t1 = readTerm () 

529 
in 

530 
if t1 = NONE then NONE 

531 
else 

532 
let 

533 
val c1 = readCmp () 

534 
in 

535 
if c1 = NONE then 

536 
let 

537 
val c = readToken () 

538 
in 

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

540 
SOME ( 

541 
cplexBounds (cplexNeg cplexInf, 

542 
cplexLeq, 

543 
the t1, 

544 
cplexLeq, 

545 
cplexInf)) 

546 
else 

547 
raise (Load_cplexFile "FREE expected") 

548 
end 

549 
else 

550 
let 

551 
val t2 = readTerm () 

552 
in 

553 
if t2 = NONE then 

554 
raise (Load_cplexFile "term expected") 

555 
else 

556 
let val c2 = readCmp () in 

557 
if c2 = NONE then 

558 
SOME (make_bounds (the c1) 

559 
(the t1) 

560 
(the t2)) 

561 
else 

562 
SOME ( 

563 
cplexBounds (the t1, 

564 
the c1, 

565 
the t2, 

566 
the c2, 

567 
the (readTerm()))) 

568 
end 

569 
end 

570 
end 

571 
end 

16784  572 

22951  573 
fun readBounds () = 
574 
let 

575 
fun makestring b = "?" 

576 
fun readbody () = 

577 
let 

578 
val b = readBound () 

579 
in 

580 
if b = NONE then [] 

581 
else if (is_normed_Bounds (the b)) then 

582 
(the b)::(readbody()) 

583 
else ( 

584 
raise (Load_cplexFile 

585 
("bounds are not normed in: "^ 

586 
(makestring (the b))))) 

587 
end 

588 
in 

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

590 
readbody () 

591 
else raise (Load_cplexFile "BOUNDS expected") 

592 
end 

593 

594 
fun readEnd () = 

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

596 
else raise (Load_cplexFile "END expected") 

597 

598 
val result_Goal = readGoal () 

599 
val result_ST = readST () 

600 
val _ = ignore_NL := false 

16784  601 
val result_Bounds = readBounds () 
602 
val _ = ignore_NL := true 

603 
val _ = readEnd () 

22951  604 
val _ = TextIO.closeIn f 
16784  605 
in 
22951  606 
cplexProg (name, result_Goal, result_ST, result_Bounds) 
16784  607 
end 
608 

609 
fun save_cplexFile filename (cplexProg (name, goal, constraints, bounds)) = 

610 
let 

22951  611 
val f = TextIO.openOut filename 
612 

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

16784  614 

32740  615 
val linebuf = Unsynchronized.ref "" 
22951  616 
fun buf_flushline s = 
617 
(basic_write (!linebuf); 

618 
basic_write "\n"; 

619 
linebuf := s) 

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

16784  621 

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

624 
buf_flushline (" "^s) 

625 
else 

626 
buf_add s 

16784  627 

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

22951  629 

630 
fun write_term (cplexVar x) = write x 

631 
 write_term (cplexNum x) = write x 

632 
 write_term cplexInf = write "inf" 

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

634 
 write_term (cplexProd (a, b)) = 

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

16784  636 
 write_term (cplexNeg x) = (write "  "; write_term x) 
637 
 write_term (cplexSum ts) = write_terms ts 

22951  638 
and write_terms [] = () 
639 
 write_terms (t::ts) = 

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

641 
write_term t; write_terms ts) 

642 

643 
fun write_goal (cplexMaximize term) = 

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

645 
 write_goal (cplexMinimize term) = 

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

16784  647 

22951  648 
fun write_cmp cplexLe = write "<" 
649 
 write_cmp cplexLeq = write "<=" 

650 
 write_cmp cplexEq = write "=" 

651 
 write_cmp cplexGe = write ">" 

652 
 write_cmp cplexGeq = write ">=" 

653 

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

655 
(write_term a; 

656 
write " "; 

657 
write_cmp cmp; 

658 
write " "; 

659 
write_term b) 

16784  660 

22951  661 
fun write_constraints [] = () 
662 
 write_constraints (c::cs) = 

663 
(if (fst c <> NONE) 

664 
then 

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

666 
else 

667 
(); 

668 
write_constr (snd c); 

669 
writeln ""; 

670 
write_constraints cs) 

16784  671 

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

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

675 
andalso (c1 = cplexLeq orelse c1 = cplexLe) 

676 
andalso (c2 = cplexLeq orelse c2 = cplexLe) 

677 
then 

678 
(write_term t2; write " free") 

679 
else 

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

681 
write_term t2; write " "; write_cmp c2; write " "; 

682 
write_term t3) 

683 
); writeln ""; write_bounds bs) 

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

685 
(write_term t1; write " "; 

686 
write_cmp c; write " "; 

687 
write_term t2; writeln ""; write_bounds bs) 

688 

689 
val _ = write_goal goal 

16784  690 
val _ = (writeln ""; writeln "ST") 
22951  691 
val _ = write_constraints constraints 
16784  692 
val _ = (writeln ""; writeln "BOUNDS") 
22951  693 
val _ = write_bounds bounds 
694 
val _ = (writeln ""; writeln "END") 

16784  695 
val _ = TextIO.closeOut f 
696 
in 

22951  697 
() 
16784  698 
end 
699 

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

702 
modulo_signed is_Num t1 

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

708 
[] 

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

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

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

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

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

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

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

22951  722 
 bound2constr (cplexBound (t1, c1, t2)) = 
16784  723 
norm_Constr(cplexConstr (c1, (t1,t2))) 
724 

725 
val emptyset = Symtab.empty 

726 

17412  727 
fun singleton v = Symtab.update (v, ()) emptyset 
16784  728 

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

730 

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

37116  733 
fun diff a b = Symtab.fold (Symtab.delete_safe o fst) b a 
22951  734 

16784  735 
fun collect_vars (cplexVar v) = singleton v 
736 
 collect_vars (cplexNeg t) = collect_vars t 

22951  737 
 collect_vars (cplexProd (t1, t2)) = 
16784  738 
merge (collect_vars t1) (collect_vars t2) 
739 
 collect_vars (cplexSum ts) = mergemap collect_vars ts 

740 
 collect_vars _ = emptyset 

741 

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

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

746 
let 

22951  747 
fun collect_constr_vars (_, cplexConstr (c, (t1,_))) = 
748 
(collect_vars t1) 

749 

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

751 
(mergemap collect_constr_vars constraints) 

752 

753 
fun collect_lower_bounded_vars 

754 
(cplexBounds (t1, c1, cplexVar v, c2, t3)) = 

755 
singleton v 

756 
 collect_lower_bounded_vars 

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

758 
singleton v 

759 
 collect_lower_bounded_vars 

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

761 
singleton v 

762 
 collect_lower_bounded_vars 

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

764 
singleton v 

765 
 collect_lower_bounded_vars 

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

767 
singleton v 

768 
 collect_lower_bounded_vars 

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

770 
singleton v 

771 
 collect_lower_bounded_vars _ = emptyset 

772 

773 
val lvars = mergemap collect_lower_bounded_vars bounds 

774 
val positive_vars = diff cvars lvars 

775 
val zero = cplexNum "0" 

776 

777 
fun make_pos_constr v = 

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

779 

780 
fun make_free_bound v = 

781 
cplexBounds (cplexNeg cplexInf, cplexLeq, 

782 
cplexVar v, cplexLeq, 

783 
cplexInf) 

784 

785 
val pos_constrs = rev (Symtab.fold 

786 
(fn (k, v) => cons (make_pos_constr k)) 

787 
positive_vars []) 

21056  788 
val bound_constrs = map (pair NONE) 
22951  789 
(maps bound2constr bounds) 
790 
val constraints' = constraints @ pos_constrs @ bound_constrs 

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

16784  792 
in 
22951  793 
cplexProg (name, goal, constraints', bounds') 
16784  794 
end 
795 

22951  796 
fun relax_strict_ineqs (cplexProg (name, goals, constrs, bounds)) = 
16784  797 
let 
22951  798 
fun relax cplexLe = cplexLeq 
799 
 relax cplexGe = cplexGeq 

800 
 relax x = x 

801 

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

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

804 

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

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

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

808 
cplexBound (t1, relax c, t2) 

16784  809 
in 
22951  810 
cplexProg (name, 
811 
goals, 

812 
map relax_constr constrs, 

813 
map relax_bounds bounds) 

16784  814 
end 
815 

22951  816 
datatype cplexResult = Unbounded 
817 
 Infeasible 

818 
 Undefined 

819 
 Optimal of string * ((string * string) list) 

16784  820 

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

822 

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

824 

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

826 

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

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

832 
fun is_symbol_start c = is_symbol_char c andalso 

833 
not (Char.isDigit c) andalso 

834 
not (c= #".") andalso 

835 
not (c= #"") 

836 
val b = String.explode a 

16784  837 
in 
22951  838 
b <> [] andalso is_symbol_start (hd b) andalso 
839 
forall is_symbol_char b 

16784  840 
end 
841 

842 
val TOKEN_SIGN = 100 

843 
val TOKEN_COLON = 101 

844 
val TOKEN_SEPARATOR = 102 

845 

22951  846 
fun load_glpkResult name = 
16784  847 
let 
22951  848 
val flist = [(is_NL, TOKEN_NL), 
849 
(is_blank, TOKEN_BLANK), 

850 
(is_num, TOKEN_NUM), 

851 
(is_sign, TOKEN_SIGN), 

16784  852 
(is_colon, TOKEN_COLON), 
22951  853 
(is_cmp, TOKEN_CMP), 
854 
(is_resultsymbol, TOKEN_SYMBOL), 

855 
(is_separator, TOKEN_SEPARATOR)] 

856 

857 
val tokenize = tokenize_general flist 

858 

859 
val f = TextIO.openIn name 

860 

32740  861 
val rest = Unsynchronized.ref [] 
16784  862 

22951  863 
fun readToken_helper () = 
864 
if length (!rest) > 0 then 

865 
let val u = hd (!rest) in 

866 
( 

867 
rest := tl (!rest); 

868 
SOME u 

869 
) 

870 
end 

871 
else 

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

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

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

874 
 SOME s => (rest := tokenize s; readToken_helper())) 
16784  875 

22951  876 
fun is_tt tok ty = (tok <> NONE andalso (fst (the tok)) = ty) 
16784  877 

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

22951  880 
fun readToken () = 
881 
let val t = readToken_helper () in 

882 
if is_tt t TOKEN_BLANK then 

883 
readToken () 

884 
else if is_tt t TOKEN_NL then 

885 
let val t2 = readToken_helper () in 

886 
if is_tt t2 TOKEN_SIGN then 

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

888 
else 

889 
(pushToken t2; t) 

890 
end 

891 
else if is_tt t TOKEN_SIGN then 

892 
let val t2 = readToken_helper () in 

893 
if is_tt t2 TOKEN_NUM then 

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

895 
else 

896 
(pushToken t2; t) 

897 
end 

898 
else 

899 
t 

900 
end 

901 

902 
fun readRestOfLine P = 

903 
let 

904 
val t = readToken () 

905 
in 

906 
if is_tt t TOKEN_NL orelse t = NONE 

907 
then P 

908 
else readRestOfLine P 

909 
end 

16784  910 

22951  911 
fun readHeader () = 
912 
let 

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

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

915 
val t1 = readToken () 

916 
val t2 = readToken () 

917 
in 

918 
if is_tt t1 TOKEN_SYMBOL andalso is_tt t2 TOKEN_COLON 

919 
then 

920 
case to_upper (snd (the t1)) of 

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

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

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

924 
else 

925 
(pushToken t2; pushToken t1; []) 

926 
end 

16784  927 

22951  928 
fun skip_until_sep () = 
929 
let val x = readToken () in 

930 
if is_tt x TOKEN_SEPARATOR then 

931 
readRestOfLine () 

932 
else 

933 
skip_until_sep () 

934 
end 

16784  935 

22951  936 
fun load_value () = 
937 
let 

938 
val t1 = readToken () 

939 
val t2 = readToken () 

940 
in 

941 
if is_tt t1 TOKEN_NUM andalso is_tt t2 TOKEN_SYMBOL then 

942 
let 

943 
val t = readToken () 

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

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

946 
val k = readToken () 

947 
in 

948 
if is_tt k TOKEN_NUM then 

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

950 
else 

951 
raise (Load_cplexResult "number expected") 

952 
end 

953 
else 

954 
(pushToken t2; pushToken t1; NONE) 

955 
end 

16784  956 

22951  957 
fun load_values () = 
958 
let val v = load_value () in 

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

960 
end 

961 

962 
val header = readHeader () 

16784  963 

22951  964 
val result = 
965 
case AList.lookup (op =) header "STATUS" of 

966 
SOME "INFEASIBLE" => Infeasible 

967 
 SOME "UNBOUNDED" => Unbounded 

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

969 
(skip_until_sep (); 

970 
skip_until_sep (); 

971 
load_values ())) 

972 
 _ => Undefined 

16784  973 

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

22951  979 
 Option => raise (Load_cplexResult "Option") 
980 
 x => raise x 

16784  981 

22951  982 
fun load_cplexResult name = 
16784  983 
let 
22951  984 
val flist = [(is_NL, TOKEN_NL), 
985 
(is_blank, TOKEN_BLANK), 

986 
(is_num, TOKEN_NUM), 

987 
(is_sign, TOKEN_SIGN), 

16784  988 
(is_colon, TOKEN_COLON), 
22951  989 
(is_cmp, TOKEN_CMP), 
990 
(is_resultsymbol, TOKEN_SYMBOL)] 

991 

992 
val tokenize = tokenize_general flist 

993 

994 
val f = TextIO.openIn name 

995 

32740  996 
val rest = Unsynchronized.ref [] 
16784  997 

22951  998 
fun readToken_helper () = 
999 
if length (!rest) > 0 then 

1000 
let val u = hd (!rest) in 

1001 
( 

1002 
rest := tl (!rest); 

1003 
SOME u 

1004 
) 

1005 
end 

1006 
else 

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

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

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

1009 
 SOME s => (rest := tokenize s; readToken_helper())) 
16784  1010 

22951  1011 
fun is_tt tok ty = (tok <> NONE andalso (fst (the tok)) = ty) 
16784  1012 

22951  1013 
fun pushToken a = if a = NONE then () else (rest := ((the a)::(!rest))) 
1014 

1015 
fun readToken () = 

1016 
let val t = readToken_helper () in 

1017 
if is_tt t TOKEN_BLANK then 

1018 
readToken () 

1019 
else if is_tt t TOKEN_SIGN then 

1020 
let val t2 = readToken_helper () in 

1021 
if is_tt t2 TOKEN_NUM then 

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

1023 
else 

1024 
(pushToken t2; t) 

1025 
end 

1026 
else 

1027 
t 

1028 
end 

16784  1029 

22951  1030 
fun readRestOfLine P = 
1031 
let 

1032 
val t = readToken () 

1033 
in 

1034 
if is_tt t TOKEN_NL orelse t = NONE 

1035 
then P 

1036 
else readRestOfLine P 

1037 
end 

16784  1038 

22951  1039 
fun readHeader () = 
1040 
let 

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

1042 
fun readObjective () = 

1043 
let 

1044 
val t = readToken () 

1045 
in 

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

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

1048 
else 

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

1050 
end 

16784  1051 

22951  1052 
val t = readToken () 
1053 
in 

1054 
if is_tt t TOKEN_SYMBOL then 

1055 
case to_upper (snd (the t)) of 

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

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

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

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

1060 
else 

1061 
(readRestOfLine (); readHeader ()) 

1062 
end 

16784  1063 

22951  1064 
fun skip_nls () = 
1065 
let val x = readToken () in 

1066 
if is_tt x TOKEN_NL then 

1067 
skip_nls () 

1068 
else 

1069 
(pushToken x; ()) 

1070 
end 

16784  1071 

22951  1072 
fun skip_paragraph () = 
1073 
if is_tt (readToken ()) TOKEN_NL then 

1074 
(if is_tt (readToken ()) TOKEN_NL then 

1075 
skip_nls () 

1076 
else 

1077 
skip_paragraph ()) 

1078 
else 

1079 
skip_paragraph () 

16784  1080 

22951  1081 
fun load_value () = 
1082 
let 

1083 
val t1 = readToken () 

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

1085 
in 

1086 
if is_tt t1 TOKEN_NUM then 

1087 
let 

1088 
val name = readToken () 

1089 
val status = readToken () 

1090 
val value = readToken () 

1091 
in 

1092 
if is_tt name TOKEN_SYMBOL andalso 

1093 
is_tt status TOKEN_SYMBOL andalso 

1094 
is_tt value TOKEN_NUM 

1095 
then 

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

1097 
else 

1098 
raise (Load_cplexResult "column line expected") 

1099 
end 

1100 
else 

1101 
(pushToken t1; NONE) 

1102 
end 

16784  1103 

22951  1104 
fun load_values () = 
1105 
let val v = load_value () in 

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

1107 
end 

1108 

1109 
val header = readHeader () 

16784  1110 

22951  1111 
val result = 
1112 
case AList.lookup (op =) header "STATUS" of 

1113 
SOME "INFEASIBLE" => Infeasible 

1114 
 SOME "NONOPTIMAL" => Unbounded 

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

1116 
(skip_paragraph (); 

1117 
skip_paragraph (); 

1118 
skip_paragraph (); 

1119 
skip_paragraph (); 

1120 
skip_paragraph (); 

1121 
load_values ())) 

1122 
 _ => Undefined 

16784  1123 

22951  1124 
val _ = TextIO.closeIn f 
16784  1125 
in 
22951  1126 
result 
16784  1127 
end 
1128 
handle (Tokenize s) => raise (Load_cplexResult ("Tokenize: "^s)) 

22951  1129 
 Option => raise (Load_cplexResult "Option") 
1130 
 x => raise x 

16784  1131 

1132 
exception Execute of string; 

1133 

21858
05f57309170c
avoid conflict with Alice keywords: renamed pack > implode, unpack > explode, any > many, avoided assert;
wenzelm
parents:
21056
diff
changeset

1134 
fun tmp_file s = Path.implode (Path.expand (File.tmp_path (Path.make [s]))); 
16784  1135 
fun wrap s = "\""^s^"\""; 
1136 

1137 
fun solve_glpk prog = 

22951  1138 
let 
1139 
val name = LargeInt.toString (Time.toMicroseconds (Time.now ())) 

1140 
val lpname = tmp_file (name^".lp") 

1141 
val resultname = tmp_file (name^".txt") 

1142 
val _ = save_cplexFile lpname prog 

1143 
val cplex_path = getenv "GLPK_PATH" 

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

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

35010
d6e492cea6e4
renamed system/system_out to bash/bash_output  to emphasized that this is really GNU bash, not some undefined POSIX sh;
wenzelm
parents:
32740
diff
changeset

1146 
val answer = #1 (bash_output command) 
16784  1147 
in 
22951  1148 
let 
1149 
val result = load_glpkResult resultname 

1150 
val _ = OS.FileSys.remove lpname 

1151 
val _ = OS.FileSys.remove resultname 

16784  1152 
in 
22951  1153 
result 
1154 
end 

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

1156 
 _ => raise (Execute answer) 

16784  1157 
end 
1158 

22951  1159 
fun solve_cplex prog = 
1160 
let 

1161 
fun write_script s lp r = 

1162 
let 

1163 
val f = TextIO.openOut s 

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

1165 
val _ = TextIO.closeOut f 

1166 
in 

1167 
() 

1168 
end 

1169 

1170 
val name = LargeInt.toString (Time.toMicroseconds (Time.now ())) 

1171 
val lpname = tmp_file (name^".lp") 

1172 
val resultname = tmp_file (name^".txt") 

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

1174 
val _ = save_cplexFile lpname prog 

1175 
val cplex_path = getenv "CPLEX_PATH" 

1176 
val cplex = if cplex_path = "" then "cplex" else cplex_path 

1177 
val _ = write_script scriptname lpname resultname 

1178 
val command = (wrap cplex)^" < "^(wrap scriptname)^" > /dev/null" 

35010
d6e492cea6e4
renamed system/system_out to bash/bash_output  to emphasized that this is really GNU bash, not some undefined POSIX sh;
wenzelm
parents:
32740
diff
changeset

1179 
val answer = "return code "^(Int.toString (bash command)) 
22951  1180 
in 
1181 
let 

1182 
val result = load_cplexResult resultname 

1183 
val _ = OS.FileSys.remove lpname 

1184 
val _ = OS.FileSys.remove resultname 

1185 
val _ = OS.FileSys.remove scriptname 

1186 
in 

1187 
result 

1188 
end 

1189 
end 

1190 

1191 
fun solve prog = 

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

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

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

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

1197 
 _ => 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

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

1199 
 SOLVER_GLPK => solve_glpk prog 
22951  1200 

16784  1201 
end; 
1202 

1203 
(* 

1204 
val demofile = "/home/obua/flyspeck/kepler/LP/cplexPent2.lp45" 

1205 
val demoout = "/home/obua/flyspeck/kepler/LP/test.out" 

1206 
val demoresult = "/home/obua/flyspeck/kepler/LP/try/test2.sol" 

22951  1207 

1208 
fun loadcplex () = Cplex.relax_strict_ineqs 

1209 
(Cplex.load_cplexFile demofile) 

16784  1210 

1211 
fun writecplex lp = Cplex.save_cplexFile demoout lp 

1212 

22951  1213 
fun test () = 
16784  1214 
let 
22951  1215 
val lp = loadcplex () 
1216 
val lp2 = Cplex.elim_nonfree_bounds lp 

16784  1217 
in 
22951  1218 
writecplex lp2 
16784  1219 
end 
1220 

1221 
fun loadresult () = Cplex.load_cplexResult demoresult; 

1222 
*) 

1223 

1224 
(*val prog = Cplex.load_cplexFile "/home/obua/tmp/pent/graph_0.lpt"; 

1225 
val _ = Cplex.solve prog;*) 