author  obua 
Mon, 01 Aug 2005 11:39:33 +0200  
changeset 16966  37e34f315057 
parent 16873  9ed940a1bebb 
child 17412  e26cb20ef0cc 
permissions  rwrr 
16784  1 
(* Title: HOL/Matrix/cplex/Cplex_tools.ML 
2 
ID: $Id$ 

3 
Author: Steven Obua 

4 
*) 

5 

6 
signature CPLEX = 

7 
sig 

8 

9 
datatype cplexTerm = cplexVar of string  cplexNum of string  cplexInf 

10 
 cplexNeg of cplexTerm 

11 
 cplexProd of cplexTerm * cplexTerm 

12 
 cplexSum of (cplexTerm list) 

13 

14 
datatype cplexComp = cplexLe  cplexLeq  cplexEq  cplexGe  cplexGeq 

15 

16 
datatype cplexGoal = cplexMinimize of cplexTerm 

17 
 cplexMaximize of cplexTerm 

18 

19 
datatype cplexConstr = cplexConstr of cplexComp * 

20 
(cplexTerm * cplexTerm) 

21 

22 
datatype cplexBounds = cplexBounds of cplexTerm * cplexComp * cplexTerm 

23 
* cplexComp * cplexTerm 

24 
 cplexBound of cplexTerm * cplexComp * cplexTerm 

25 

26 
datatype cplexProg = cplexProg of string 

27 
* cplexGoal 

28 
* ((string option * cplexConstr) 

29 
list) 

30 
* cplexBounds list 

31 

32 
datatype cplexResult = Unbounded 

33 
 Infeasible 

34 
 Undefined 

35 
 Optimal of string * 

36 
(((* name *) string * 

37 
(* value *) string) list) 

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

38 

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

39 
datatype cplexSolver = SOLVER_DEFAULT  SOLVER_CPLEX  SOLVER_GLPK 
16784  40 

41 
exception Load_cplexFile of string 

42 
exception Load_cplexResult of string 

43 
exception Save_cplexFile of string 

44 
exception Execute of string 

45 

46 
val load_cplexFile : string > cplexProg 

47 

48 
val save_cplexFile : string > cplexProg > unit 

49 

50 
val elim_nonfree_bounds : cplexProg > cplexProg 

51 

52 
val relax_strict_ineqs : cplexProg > cplexProg 

53 

54 
val is_normed_cplexProg : cplexProg > bool 

55 

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

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

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

60 

61 
structure Cplex : CPLEX = 

62 
struct 

63 

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

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

65 

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

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

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

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

69 

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

72 
exception Save_cplexFile of string; 

73 

74 
datatype cplexTerm = cplexVar of string 

75 
 cplexNum of string 

76 
 cplexInf 

77 
 cplexNeg of cplexTerm 

78 
 cplexProd of cplexTerm * cplexTerm 

79 
 cplexSum of (cplexTerm list) 

80 
datatype cplexComp = cplexLe  cplexLeq  cplexEq  cplexGe  cplexGeq 

81 
datatype cplexGoal = cplexMinimize of cplexTerm  cplexMaximize of cplexTerm 

82 
datatype cplexConstr = cplexConstr of cplexComp * (cplexTerm * cplexTerm) 

83 
datatype cplexBounds = cplexBounds of cplexTerm * cplexComp * cplexTerm 

84 
* cplexComp * cplexTerm 

85 
 cplexBound of cplexTerm * cplexComp * cplexTerm 

86 
datatype cplexProg = cplexProg of string 

87 
* cplexGoal 

88 
* ((string option * cplexConstr) list) 

89 
* cplexBounds list 

90 

91 
fun rev_cmp cplexLe = cplexGe 

92 
 rev_cmp cplexLeq = cplexGeq 

93 
 rev_cmp cplexGe = cplexLe 

94 
 rev_cmp cplexGeq = cplexLeq 

95 
 rev_cmp cplexEq = cplexEq 

96 

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

98 
 the (SOME x) = x; 

99 

100 
fun modulo_signed is_something (cplexNeg u) = is_something u 

101 
 modulo_signed is_something u = is_something u 

102 

103 
fun is_Num (cplexNum _) = true 

104 
 is_Num _ = false 

105 

106 
fun is_Inf cplexInf = true 

107 
 is_Inf _ = false 

108 

109 
fun is_Var (cplexVar _) = true 

110 
 is_Var _ = false 

111 

112 
fun is_Neg (cplexNeg x ) = true 

113 
 is_Neg _ = false 

114 

115 
fun is_normed_Prod (cplexProd (t1, t2)) = 

116 
(is_Num t1) andalso (is_Var t2) 

117 
 is_normed_Prod x = is_Var x 

118 

119 
fun is_normed_Sum (cplexSum ts) = 

120 
(ts <> []) andalso forall (modulo_signed is_normed_Prod) ts 

121 
 is_normed_Sum x = modulo_signed is_normed_Prod x 

122 

123 
fun is_normed_Constr (cplexConstr (c, (t1, t2))) = 

124 
(is_normed_Sum t1) andalso (modulo_signed is_Num t2) 

125 

126 
fun is_Num_or_Inf x = is_Inf x orelse is_Num x 

127 

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

129 
(c1 = cplexLe orelse c1 = cplexLeq) andalso 

130 
(c2 = cplexLe orelse c2 = cplexLeq) andalso 

131 
is_Var t2 andalso 

132 
modulo_signed is_Num_or_Inf t1 andalso 

133 
modulo_signed is_Num_or_Inf t3 

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

135 
(is_Var t1 andalso (modulo_signed is_Num_or_Inf t2)) 

136 
orelse 

137 
(c <> cplexEq andalso 

138 
is_Var t2 andalso (modulo_signed is_Num_or_Inf t1)) 

139 

140 
fun term_of_goal (cplexMinimize x) = x 

141 
 term_of_goal (cplexMaximize x) = x 

142 

143 
fun is_normed_cplexProg (cplexProg (name, goal, constraints, bounds)) = 

144 
is_normed_Sum (term_of_goal goal) andalso 

145 
forall (fn (_,x) => is_normed_Constr x) constraints andalso 

146 
forall is_normed_Bounds bounds 

147 

148 
fun is_NL s = s = "\n" 

149 

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

151 

152 
fun is_num a = 

153 
let 

154 
val b = String.explode a 

155 
fun num4 cs = forall Char.isDigit cs 

156 
fun num3 [] = true 

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

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

159 
num4 cs 

160 
else 

161 
num4 ds 

162 
fun num2 [] = true 

163 
 num2 (c::cs) = 

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

165 
else (Char.isDigit c) andalso num2 cs 

166 
fun num1 [] = true 

167 
 num1 (c::cs) = 

168 
if c = #"." then num2 cs 

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

170 
else (Char.isDigit c) andalso num1 cs 

171 
fun num [] = true 

172 
 num (c::cs) = 

173 
if c = #"." then num2 cs 

174 
else (Char.isDigit c) andalso num1 cs 

175 
in 

176 
num b 

177 
end 

178 

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

180 

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

182 
orelse s = ">=" orelse s = "=" 

183 

184 
fun is_symbol a = 

185 
let 

186 
val symbol_char = String.explode "!\"#$%&()/,.;?@_`'{}~" 

187 
fun is_symbol_char c = Char.isAlphaNum c orelse 

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

189 
fun is_symbol_start c = is_symbol_char c andalso 

190 
not (Char.isDigit c) andalso 

191 
not (c= #".") 

192 
val b = String.explode a 

193 
in 

194 
b <> [] andalso is_symbol_start (hd b) andalso 

195 
forall is_symbol_char b 

196 
end 

197 

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

199 

200 
fun keyword x = 

201 
let 

202 
val a = to_upper x 

203 
in 

204 
if a = "BOUNDS" orelse a = "BOUND" then 

205 
SOME "BOUNDS" 

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

207 
SOME "MINIMIZE" 

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

209 
SOME "MAXIMIZE" 

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

211 
SOME "ST" 

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

213 
SOME a 

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

215 
SOME "GENERAL" 

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

217 
SOME "INTEGER" 

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

219 
SOME "BINARY" 

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

221 
SOME "INF" 

222 
else 

223 
NONE 

224 
end 

225 

226 
val TOKEN_ERROR = ~1 

227 
val TOKEN_BLANK = 0 

228 
val TOKEN_NUM = 1 

229 
val TOKEN_DELIMITER = 2 

230 
val TOKEN_SYMBOL = 3 

231 
val TOKEN_LABEL = 4 

232 
val TOKEN_CMP = 5 

233 
val TOKEN_KEYWORD = 6 

234 
val TOKEN_NL = 7 

235 

236 
(* tokenize takes a list of chars as argument and returns a list of 

237 
int * string pairs, each string representing a "cplex token", 

238 
and each int being one of TOKEN_NUM, TOKEN_DELIMITER, TOKEN_CMP 

239 
or TOKEN_SYMBOL *) 

240 
fun tokenize s = 

241 
let 

242 
val flist = [(is_NL, TOKEN_NL), 

243 
(is_blank, TOKEN_BLANK), 

244 
(is_num, TOKEN_NUM), 

245 
(is_delimiter, TOKEN_DELIMITER), 

246 
(is_cmp, TOKEN_CMP), 

247 
(is_symbol, TOKEN_SYMBOL)] 

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

249 
 match_helper (f::fs) s = 

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

251 
fun match s = match_helper flist s 

252 
fun tok s = 

253 
if s = "" then [] else 

254 
let 

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

256 
val (f, j) = match h 

257 
fun len i = 

258 
if size s = i then i 

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

260 
len (i+1) 

261 
else i 

262 
in 

263 
if j < 0 then 

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

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

266 
^s))) 

267 
else 

268 
let 

269 
val l = len 1 

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

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

272 
in 

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

274 
end 

275 
end 

276 
in 

277 
tok s 

278 
end 

279 

280 
exception Tokenize of string; 

281 

282 
fun tokenize_general flist s = 

283 
let 

284 
fun match_helper [] s = raise (Tokenize s) 

285 
 match_helper (f::fs) s = 

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

287 
fun match s = match_helper flist s 

288 
fun tok s = 

289 
if s = "" then [] else 

290 
let 

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

292 
val (f, j) = match h 

293 
fun len i = 

294 
if size s = i then i 

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

296 
len (i+1) 

297 
else i 

298 
val l = len 1 

299 
in 

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

301 
end 

302 
in 

303 
tok s 

304 
end 

305 

306 
fun load_cplexFile name = 

307 
let 

308 
val f = TextIO.openIn name 

309 
val ignore_NL = ref true 

310 
val rest = ref [] 

311 

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

313 

314 
fun readToken_helper () = 

315 
if length (!rest) > 0 then 

316 
let val u = hd (!rest) in 

317 
( 

318 
rest := tl (!rest); 

319 
SOME u 

320 
) 

321 
end 

322 
else 

323 
let val s = TextIO.inputLine f in 

324 
if s = "" then NONE else 

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 () 

337 
end 

338 
end 

339 

340 
fun readToken_helper2 () = 

341 
let val c = readToken_helper () in 

342 
if c = NONE then NONE 

343 
else if !ignore_NL andalso fst (the c) = TOKEN_NL then 

344 
readToken_helper2 () 

345 
else if fst (the c) = TOKEN_SYMBOL 

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

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

348 
else c 

349 
end 

350 

351 
fun readToken () = readToken_helper2 () 

352 

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

354 

355 
fun is_value token = 

356 
fst token = TOKEN_NUM orelse (fst token = TOKEN_KEYWORD 

357 
andalso snd token = "INF") 

358 

359 
fun get_value token = 

360 
if fst token = TOKEN_NUM then 

361 
cplexNum (snd token) 

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

363 
then 

364 
cplexInf 

365 
else 

366 
raise (Load_cplexFile "num expected") 

367 

368 
fun readTerm_Product only_num = 

369 
let val c = readToken () in 

370 
if c = NONE then NONE 

371 
else if fst (the c) = TOKEN_SYMBOL 

372 
then ( 

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

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

375 
) 

376 
else if only_num andalso is_value (the c) then 

377 
SOME (get_value (the c)) 

378 
else if is_value (the c) then 

379 
let val t1 = get_value (the c) 

380 
val d = readToken () 

381 
in 

382 
if d = NONE then SOME t1 

383 
else if fst (the d) = TOKEN_SYMBOL then 

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

385 
else 

386 
(pushToken (the d); SOME t1) 

387 
end 

388 
else (pushToken (the c); NONE) 

389 
end 

390 

391 
fun readTerm_Signed only_signed only_num = 

392 
let 

393 
val c = readToken () 

394 
in 

395 
if c = NONE then NONE 

396 
else 

397 
let val d = the c in 

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

399 
readTerm_Product only_num 

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

401 
SOME (cplexNeg (the (readTerm_Product 

402 
only_num))) 

403 
else (pushToken d; 

404 
if only_signed then NONE 

405 
else readTerm_Product only_num) 

406 
end 

407 
end 

408 

409 
fun readTerm_Sum first_signed = 

410 
let val c = readTerm_Signed first_signed false in 

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

412 
end 

413 

414 
fun readTerm () = 

415 
let val c = readTerm_Sum false in 

416 
if c = [] then NONE 

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

418 
else SOME (cplexSum c) 

419 
end 

420 

421 
fun readLabeledTerm () = 

422 
let val c = readToken () in 

423 
if c = NONE then (NONE, NONE) 

424 
else if fst (the c) = TOKEN_LABEL then 

425 
let val t = readTerm () in 

426 
if t = NONE then 

427 
raise (Load_cplexFile ("term after label "^ 

428 
(snd (the c))^ 

429 
" expected")) 

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

431 
end 

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

433 
end 

434 

435 
fun readGoal () = 

436 
let 

437 
val g = readToken () 

438 
in 

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

440 
cplexMaximize (the (snd (readLabeledTerm ()))) 

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

442 
cplexMinimize (the (snd (readLabeledTerm ()))) 

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

444 
end 

445 

446 
fun str2cmp b = 

447 
(case b of 

448 
"<" => cplexLe 

449 
 "<=" => cplexLeq 

450 
 ">" => cplexGe 

451 
 ">=" => cplexGeq 

452 
 "=" => cplexEq 

453 
 _ => raise (Load_cplexFile (b^" is no TOKEN_CMP"))) 

454 

455 
fun readConstraint () = 

456 
let 

457 
val t = readLabeledTerm () 

458 
fun make_constraint b t1 t2 = 

459 
cplexConstr 

460 
(str2cmp b, 

461 
(t1, t2)) 

462 
in 

463 
if snd t = NONE then NONE 

464 
else 

465 
let val c = readToken () in 

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

467 
then raise (Load_cplexFile "TOKEN_CMP expected") 

468 
else 

469 
let val n = readTerm_Signed false true in 

470 
if n = NONE then 

471 
raise (Load_cplexFile "num expected") 

472 
else 

473 
SOME (fst t, 

474 
make_constraint (snd (the c)) 

475 
(the (snd t)) 

476 
(the n)) 

477 
end 

478 
end 

479 
end 

480 

481 
fun readST () = 

482 
let 

483 
fun readbody () = 

484 
let val t = readConstraint () in 

485 
if t = NONE then [] 

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

487 
(the t)::(readbody ()) 

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

489 
raise (Load_cplexFile 

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

491 
"'is not normed")) 

492 
else 

493 
raise (Load_cplexFile 

494 
"constraint is not normed") 

495 
end 

496 
in 

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

498 
then 

499 
readbody () 

500 
else 

501 
raise (Load_cplexFile "ST expected") 

502 
end 

503 

504 
fun readCmp () = 

505 
let val c = readToken () in 

506 
if c = NONE then NONE 

507 
else if fst (the c) = TOKEN_CMP then 

508 
SOME (str2cmp (snd (the c))) 

509 
else (pushToken (the c); NONE) 

510 
end 

511 

512 
fun skip_NL () = 

513 
let val c = readToken () in 

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

515 
skip_NL () 

516 
else 

517 
(pushToken (the c); ()) 

518 
end 

519 

520 
fun is_var (cplexVar _) = true 

521 
 is_var _ = false 

522 

523 
fun make_bounds c t1 t2 = 

524 
cplexBound (t1, c, t2) 

525 

526 
fun readBound () = 

527 
let 

528 
val _ = skip_NL () 

529 
val t1 = readTerm () 

530 
in 

531 
if t1 = NONE then NONE 

532 
else 

533 
let 

534 
val c1 = readCmp () 

535 
in 

536 
if c1 = NONE then 

537 
let 

538 
val c = readToken () 

539 
in 

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

541 
SOME ( 

542 
cplexBounds (cplexNeg cplexInf, 

543 
cplexLeq, 

544 
the t1, 

545 
cplexLeq, 

546 
cplexInf)) 

547 
else 

548 
raise (Load_cplexFile "FREE expected") 

549 
end 

550 
else 

551 
let 

552 
val t2 = readTerm () 

553 
in 

554 
if t2 = NONE then 

555 
raise (Load_cplexFile "term expected") 

556 
else 

557 
let val c2 = readCmp () in 

558 
if c2 = NONE then 

559 
SOME (make_bounds (the c1) 

560 
(the t1) 

561 
(the t2)) 

562 
else 

563 
SOME ( 

564 
cplexBounds (the t1, 

565 
the c1, 

566 
the t2, 

567 
the c2, 

568 
the (readTerm()))) 

569 
end 

570 
end 

571 
end 

572 
end 

573 

574 
fun readBounds () = 

575 
let 

576 
fun makestring b = "?" 

577 
fun readbody () = 

578 
let 

579 
val b = readBound () 

580 
in 

581 
if b = NONE then [] 

582 
else if (is_normed_Bounds (the b)) then 

583 
(the b)::(readbody()) 

584 
else ( 

585 
raise (Load_cplexFile 

586 
("bounds are not normed in: "^ 

587 
(makestring (the b))))) 

588 
end 

589 
in 

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

591 
readbody () 

592 
else raise (Load_cplexFile "BOUNDS expected") 

593 
end 

594 

595 
fun readEnd () = 

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

597 
else raise (Load_cplexFile "END expected") 

598 

599 
val result_Goal = readGoal () 

600 
val result_ST = readST () 

601 
val _ = ignore_NL := false 

602 
val result_Bounds = readBounds () 

603 
val _ = ignore_NL := true 

604 
val _ = readEnd () 

605 
val _ = TextIO.closeIn f 

606 
in 

607 
cplexProg (name, result_Goal, result_ST, result_Bounds) 

608 
end 

609 

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

611 
let 

612 
val f = TextIO.openOut filename 

613 

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

615 

616 
val linebuf = ref "" 

617 
fun buf_flushline s = 

618 
(basic_write (!linebuf); 

619 
basic_write "\n"; 

620 
linebuf := s) 

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

622 

623 
fun write s = 

624 
if (String.size s) + (String.size (!linebuf)) >= 250 then 

625 
buf_flushline (" "^s) 

626 
else 

627 
buf_add s 

628 

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

630 

631 
fun write_term (cplexVar x) = write x 

632 
 write_term (cplexNum x) = write x 

633 
 write_term cplexInf = write "inf" 

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

635 
 write_term (cplexProd (a, b)) = 

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

637 
 write_term (cplexNeg x) = (write "  "; write_term x) 

638 
 write_term (cplexSum ts) = write_terms ts 

639 
and write_terms [] = () 

640 
 write_terms (t::ts) = 

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

642 
write_term t; write_terms ts) 

643 

644 
fun write_goal (cplexMaximize term) = 

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

646 
 write_goal (cplexMinimize term) = 

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

648 

649 
fun write_cmp cplexLe = write "<" 

650 
 write_cmp cplexLeq = write "<=" 

651 
 write_cmp cplexEq = write "=" 

652 
 write_cmp cplexGe = write ">" 

653 
 write_cmp cplexGeq = write ">=" 

654 

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

656 
(write_term a; 

657 
write " "; 

658 
write_cmp cmp; 

659 
write " "; 

660 
write_term b) 

661 

662 
fun write_constraints [] = () 

663 
 write_constraints (c::cs) = 

664 
(if (fst c <> NONE) 

665 
then 

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

667 
else 

668 
(); 

669 
write_constr (snd c); 

670 
writeln ""; 

671 
write_constraints cs) 

672 

673 
fun write_bounds [] = () 

674 
 write_bounds ((cplexBounds (t1,c1,t2,c2,t3))::bs) = 

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

676 
andalso (c1 = cplexLeq orelse c1 = cplexLe) 

677 
andalso (c2 = cplexLeq orelse c2 = cplexLe) 

678 
then 

679 
(write_term t2; write " free") 

680 
else 

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

682 
write_term t2; write " "; write_cmp c2; write " "; 

683 
write_term t3) 

684 
); writeln ""; write_bounds bs) 

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

686 
(write_term t1; write " "; 

687 
write_cmp c; write " "; 

688 
write_term t2; writeln ""; write_bounds bs) 

689 

690 
val _ = write_goal goal 

691 
val _ = (writeln ""; writeln "ST") 

692 
val _ = write_constraints constraints 

693 
val _ = (writeln ""; writeln "BOUNDS") 

694 
val _ = write_bounds bounds 

695 
val _ = (writeln ""; writeln "END") 

696 
val _ = TextIO.closeOut f 

697 
in 

698 
() 

699 
end 

700 

701 
fun norm_Constr (constr as cplexConstr (c, (t1, t2))) = 

702 
if not (modulo_signed is_Num t2) andalso 

703 
modulo_signed is_Num t1 

704 
then 

705 
[cplexConstr (rev_cmp c, (t2, t1))] 

706 
else if (c = cplexLe orelse c = cplexLeq) andalso 

707 
(t1 = (cplexNeg cplexInf) orelse t2 = cplexInf) 

708 
then 

709 
[] 

710 
else if (c = cplexGe orelse c = cplexGeq) andalso 

711 
(t1 = cplexInf orelse t2 = cplexNeg cplexInf) 

712 
then 

713 
[] 

714 
else 

715 
[constr] 

716 

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

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

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

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

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

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

723 
 bound2constr (cplexBound (t1, c1, t2)) = 

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

725 

726 
val emptyset = Symtab.empty 

727 

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

729 

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

731 

732 
fun mergemap f ts = Library.foldl 

733 
(fn (table, x) => merge table (f x)) 

734 
(Symtab.empty, ts) 

735 

736 
fun diff a b = Symtab.foldl (fn (a, (k,v)) => 

737 
(Symtab.delete k a) handle UNDEF => a) 

738 
(a, b) 

739 

740 
fun collect_vars (cplexVar v) = singleton v 

741 
 collect_vars (cplexNeg t) = collect_vars t 

742 
 collect_vars (cplexProd (t1, t2)) = 

743 
merge (collect_vars t1) (collect_vars t2) 

744 
 collect_vars (cplexSum ts) = mergemap collect_vars ts 

745 
 collect_vars _ = emptyset 

746 

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

748 
equivalent program with only free bounds 

749 
IF for the input program P holds: is_normed_cplexProg P *) 

750 
fun elim_nonfree_bounds (cplexProg (name, goal, constraints, bounds)) = 

751 
let 

752 
fun collect_constr_vars (_, cplexConstr (c, (t1,_))) = 

753 
(collect_vars t1) 

754 

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

756 
(mergemap collect_constr_vars constraints) 

757 

758 
fun collect_lower_bounded_vars 

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

760 
singleton v 

761 
 collect_lower_bounded_vars 

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

763 
singleton v 

764 
 collect_lower_bounded_vars 

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

766 
singleton v 

767 
 collect_lower_bounded_vars 

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

769 
singleton v 

770 
 collect_lower_bounded_vars 

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

772 
singleton v 

773 
 collect_lower_bounded_vars 

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

775 
singleton v 

776 
 collect_lower_bounded_vars _ = emptyset 

777 

778 
val lvars = mergemap collect_lower_bounded_vars bounds 

779 
val positive_vars = diff cvars lvars 

780 
val zero = cplexNum "0" 

781 

782 
fun make_pos_constr v = 

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

784 

785 
fun make_free_bound v = 

786 
cplexBounds (cplexNeg cplexInf, cplexLeq, 

787 
cplexVar v, cplexLeq, 

788 
cplexInf) 

789 

790 
val pos_constrs = rev(Symtab.foldl 

791 
(fn (l, (k,v)) => (make_pos_constr k) :: l) 

792 
([], positive_vars)) 

793 
val bound_constrs = map (fn x => (NONE, x)) 

794 
(Library.flat (map bound2constr bounds)) 

795 
val constraints' = constraints @ pos_constrs @ bound_constrs 

796 
val bounds' = rev(Symtab.foldl (fn (l, (v,_)) => 

797 
(make_free_bound v)::l) 

798 
([], cvars)) 

799 
in 

800 
cplexProg (name, goal, constraints', bounds') 

801 
end 

802 

803 
fun relax_strict_ineqs (cplexProg (name, goals, constrs, bounds)) = 

804 
let 

805 
fun relax cplexLe = cplexLeq 

806 
 relax cplexGe = cplexGeq 

807 
 relax x = x 

808 

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

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

811 

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

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

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

815 
cplexBound (t1, relax c, t2) 

816 
in 

817 
cplexProg (name, 

818 
goals, 

819 
map relax_constr constrs, 

820 
map relax_bounds bounds) 

821 
end 

822 

823 
datatype cplexResult = Unbounded 

824 
 Infeasible 

825 
 Undefined 

826 
 Optimal of string * ((string * string) list) 

827 

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

829 

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

831 

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

833 

834 
fun is_resultsymbol a = 

835 
let 

836 
val symbol_char = String.explode "!\"#$%&()/,.;?@_`'{}~" 

837 
fun is_symbol_char c = Char.isAlphaNum c orelse 

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

839 
fun is_symbol_start c = is_symbol_char c andalso 

840 
not (Char.isDigit c) andalso 

841 
not (c= #".") andalso 

842 
not (c= #"") 

843 
val b = String.explode a 

844 
in 

845 
b <> [] andalso is_symbol_start (hd b) andalso 

846 
forall is_symbol_char b 

847 
end 

848 

849 
val TOKEN_SIGN = 100 

850 
val TOKEN_COLON = 101 

851 
val TOKEN_SEPARATOR = 102 

852 

853 
fun load_glpkResult name = 

854 
let 

855 
val flist = [(is_NL, TOKEN_NL), 

856 
(is_blank, TOKEN_BLANK), 

857 
(is_num, TOKEN_NUM), 

858 
(is_sign, TOKEN_SIGN), 

859 
(is_colon, TOKEN_COLON), 

860 
(is_cmp, TOKEN_CMP), 

861 
(is_resultsymbol, TOKEN_SYMBOL), 

862 
(is_separator, TOKEN_SEPARATOR)] 

863 

864 
val tokenize = tokenize_general flist 

865 

866 
val f = TextIO.openIn name 

867 

868 
val rest = ref [] 

869 

870 
fun readToken_helper () = 

871 
if length (!rest) > 0 then 

872 
let val u = hd (!rest) in 

873 
( 

874 
rest := tl (!rest); 

875 
SOME u 

876 
) 

877 
end 

878 
else 

879 
let val s = TextIO.inputLine f in 

880 
if s = "" then NONE else (rest := tokenize s; readToken_helper()) 

881 
end 

882 

883 
fun is_tt tok ty = (tok <> NONE andalso (fst (the tok)) = ty) 

884 

885 
fun pushToken a = if a = NONE then () else (rest := ((the a)::(!rest))) 

886 

887 
fun readToken () = 

888 
let val t = readToken_helper () in 

889 
if is_tt t TOKEN_BLANK then 

890 
readToken () 

891 
else if is_tt t TOKEN_NL then 

892 
let val t2 = readToken_helper () in 

893 
if is_tt t2 TOKEN_SIGN then 

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

895 
else 

896 
(pushToken t2; t) 

897 
end 

898 
else if is_tt t TOKEN_SIGN then 

899 
let val t2 = readToken_helper () in 

900 
if is_tt t2 TOKEN_NUM then 

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

902 
else 

903 
(pushToken t2; t) 

904 
end 

905 
else 

906 
t 

907 
end 

908 

909 
fun readRestOfLine P = 

910 
let 

911 
val t = readToken () 

912 
in 

913 
if is_tt t TOKEN_NL orelse t = NONE 

914 
then P 

915 
else readRestOfLine P 

916 
end 

917 

918 
fun readHeader () = 

919 
let 

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

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

922 
val t1 = readToken () 

923 
val t2 = readToken () 

924 
in 

925 
if is_tt t1 TOKEN_SYMBOL andalso is_tt t2 TOKEN_COLON 

926 
then 

927 
case to_upper (snd (the t1)) of 

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

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

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

931 
else 

932 
(pushToken t2; pushToken t1; []) 

933 
end 

934 

935 
fun skip_until_sep () = 

936 
let val x = readToken () in 

937 
if is_tt x TOKEN_SEPARATOR then 

938 
readRestOfLine () 

939 
else 

940 
skip_until_sep () 

941 
end 

942 

943 
fun load_value () = 

944 
let 

945 
val t1 = readToken () 

946 
val t2 = readToken () 

947 
in 

948 
if is_tt t1 TOKEN_NUM andalso is_tt t2 TOKEN_SYMBOL then 

949 
let 

950 
val t = readToken () 

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

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

953 
val k = readToken () 

954 
in 

955 
if is_tt k TOKEN_NUM then 

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

957 
else 

958 
raise (Load_cplexResult "number expected") 

959 
end 

960 
else 

961 
(pushToken t2; pushToken t1; NONE) 

962 
end 

963 

964 
fun load_values () = 

965 
let val v = load_value () in 

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

967 
end 

968 

969 
val header = readHeader () 

970 

971 
val result = 

972 
case assoc (header, "STATUS") of 

973 
SOME "INFEASIBLE" => Infeasible 

974 
 SOME "UNBOUNDED" => Unbounded 

975 
 SOME "OPTIMAL" => Optimal (the (assoc (header, "OBJECTIVE")), 

976 
(skip_until_sep (); 

977 
skip_until_sep (); 

978 
load_values ())) 

979 
 _ => Undefined 

980 

981 
val _ = TextIO.closeIn f 

982 
in 

983 
result 

984 
end 

985 
handle (Tokenize s) => raise (Load_cplexResult ("Tokenize: "^s)) 

986 
 Option => raise (Load_cplexResult "Option") 

987 
 x => raise x 

988 

989 
fun load_cplexResult name = 

990 
let 

991 
val flist = [(is_NL, TOKEN_NL), 

992 
(is_blank, TOKEN_BLANK), 

993 
(is_num, TOKEN_NUM), 

994 
(is_sign, TOKEN_SIGN), 

995 
(is_colon, TOKEN_COLON), 

996 
(is_cmp, TOKEN_CMP), 

997 
(is_resultsymbol, TOKEN_SYMBOL)] 

998 

999 
val tokenize = tokenize_general flist 

1000 

1001 
val f = TextIO.openIn name 

1002 

1003 
val rest = ref [] 

1004 

1005 
fun readToken_helper () = 

1006 
if length (!rest) > 0 then 

1007 
let val u = hd (!rest) in 

1008 
( 

1009 
rest := tl (!rest); 

1010 
SOME u 

1011 
) 

1012 
end 

1013 
else 

1014 
let 

1015 
val s = TextIO.inputLine f 

1016 
in 

1017 
if s = "" then NONE else (rest := tokenize s; readToken_helper()) 

1018 
end 

1019 

1020 
fun is_tt tok ty = (tok <> NONE andalso (fst (the tok)) = ty) 

1021 

1022 
fun pushToken a = if a = NONE then () else (rest := ((the a)::(!rest))) 

1023 

1024 
fun readToken () = 

1025 
let val t = readToken_helper () in 

1026 
if is_tt t TOKEN_BLANK then 

1027 
readToken () 

1028 
else if is_tt t TOKEN_SIGN then 

1029 
let val t2 = readToken_helper () in 

1030 
if is_tt t2 TOKEN_NUM then 

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

1032 
else 

1033 
(pushToken t2; t) 

1034 
end 

1035 
else 

1036 
t 

1037 
end 

1038 

1039 
fun readRestOfLine P = 

1040 
let 

1041 
val t = readToken () 

1042 
in 

1043 
if is_tt t TOKEN_NL orelse t = NONE 

1044 
then P 

1045 
else readRestOfLine P 

1046 
end 

1047 

1048 
fun readHeader () = 

1049 
let 

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

1051 
fun readObjective () = 

1052 
let 

1053 
val t = readToken () 

1054 
in 

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

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

1057 
else 

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

1059 
end 

1060 

1061 
val t = readToken () 

1062 
in 

1063 
if is_tt t TOKEN_SYMBOL then 

1064 
case to_upper (snd (the t)) of 

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

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

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

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

1069 
else 

1070 
(readRestOfLine (); readHeader ()) 

1071 
end 

1072 

1073 
fun skip_nls () = 

1074 
let val x = readToken () in 

1075 
if is_tt x TOKEN_NL then 

1076 
skip_nls () 

1077 
else 

1078 
(pushToken x; ()) 

1079 
end 

1080 

1081 
fun skip_paragraph () = 

1082 
if is_tt (readToken ()) TOKEN_NL then 

1083 
(if is_tt (readToken ()) TOKEN_NL then 

1084 
skip_nls () 

1085 
else 

1086 
skip_paragraph ()) 

1087 
else 

1088 
skip_paragraph () 

1089 

1090 
fun load_value () = 

1091 
let 

1092 
val t1 = readToken () 

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

1094 
in 

1095 
if is_tt t1 TOKEN_NUM then 

1096 
let 

1097 
val name = readToken () 

1098 
val status = readToken () 

1099 
val value = readToken () 

1100 
in 

1101 
if is_tt name TOKEN_SYMBOL andalso 

1102 
is_tt status TOKEN_SYMBOL andalso 

1103 
is_tt value TOKEN_NUM 

1104 
then 

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

1106 
else 

1107 
raise (Load_cplexResult "column line expected") 

1108 
end 

1109 
else 

1110 
(pushToken t1; NONE) 

1111 
end 

1112 

1113 
fun load_values () = 

1114 
let val v = load_value () in 

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

1116 
end 

1117 

1118 
val header = readHeader () 

1119 

1120 
val result = 

1121 
case assoc (header, "STATUS") of 

1122 
SOME "INFEASIBLE" => Infeasible 

1123 
 SOME "NONOPTIMAL" => Unbounded 

1124 
 SOME "OPTIMAL" => Optimal (the (assoc (header, "OBJECTIVE")), 

1125 
(skip_paragraph (); 

1126 
skip_paragraph (); 

1127 
skip_paragraph (); 

1128 
skip_paragraph (); 

1129 
skip_paragraph (); 

1130 
load_values ())) 

1131 
 _ => Undefined 

1132 

1133 
val _ = TextIO.closeIn f 

1134 
in 

1135 
result 

1136 
end 

1137 
handle (Tokenize s) => raise (Load_cplexResult ("Tokenize: "^s)) 

1138 
 Option => raise (Load_cplexResult "Option") 

1139 
 x => raise x 

1140 

1141 
exception Execute of string; 

1142 

1143 
fun tmp_file s = Path.pack (Path.expand (File.tmp_path (Path.make [s]))); 

1144 
fun wrap s = "\""^s^"\""; 

1145 

1146 
fun solve_glpk prog = 

1147 
let 

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

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

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

1151 
val _ = save_cplexFile lpname prog 

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

1152 
val cplex_path = getenv "GLPK_PATH" 
16784  1153 
val cplex = if cplex_path = "" then "glpsol" else cplex_path 
1154 
val command = (wrap cplex)^" lpt "^(wrap lpname)^" output "^(wrap resultname) 

1155 
val answer = execute command 

1156 
in 

1157 
let 

1158 
val result = load_glpkResult resultname 

1159 
val _ = OS.FileSys.remove lpname 

1160 
val _ = OS.FileSys.remove resultname 

1161 
in 

1162 
result 

1163 
end 

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

1165 
 _ => raise (Execute answer) 

1166 
end 

1167 

1168 
fun solve_cplex prog = 

1169 
let 

1170 
fun write_script s lp r = 

1171 
let 

1172 
val f = TextIO.openOut s 

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

1174 
val _ = TextIO.closeOut f 

1175 
in 

1176 
() 

1177 
end 

1178 

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

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

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

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

1183 
val _ = save_cplexFile lpname prog 

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

1184 
val cplex_path = getenv "CPLEX_PATH" 
16784  1185 
val cplex = if cplex_path = "" then "cplex" else cplex_path 
1186 
val _ = write_script scriptname lpname resultname 

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

1188 
val answer = "return code "^(Int.toString (system command)) 

1189 
in 

1190 
let 

1191 
val result = load_cplexResult resultname 

1192 
val _ = OS.FileSys.remove lpname 

1193 
val _ = OS.FileSys.remove resultname 

1194 
val _ = OS.FileSys.remove scriptname 

1195 
in 

1196 
result 

1197 
end 

1198 
end 

1199 

1200 
fun solve prog = 

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

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

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

1203 
(case getenv "LP_SOLVER" of 
37e34f315057
1. changed configuration variables for linear programming (Cplex_tools):
obua
parents:
16873
diff
changeset

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

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

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

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

1208 
 SOLVER_GLPK => solve_glpk prog 
16784  1209 

1210 
end; 

1211 

1212 
(* 

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

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

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

1216 

1217 
fun loadcplex () = Cplex.relax_strict_ineqs 

1218 
(Cplex.load_cplexFile demofile) 

1219 

1220 
fun writecplex lp = Cplex.save_cplexFile demoout lp 

1221 

1222 
fun test () = 

1223 
let 

1224 
val lp = loadcplex () 

1225 
val lp2 = Cplex.elim_nonfree_bounds lp 

1226 
in 

1227 
writecplex lp2 

1228 
end 

1229 

1230 
fun loadresult () = Cplex.load_cplexResult demoresult; 

1231 
*) 

1232 

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

1234 
val _ = Cplex.solve prog;*) 