(* Title: HOL/Matrix_LP/Cplex_tools.ML
Author: Steven Obua
Relevant Isabelle environment settings:
# LP_SOLVER is the default solver. It can be changed during runtime via Cplex.set_solver.
# First option: use the commercial cplex solver
#LP_SOLVER=CPLEX
#CPLEX_PATH=cplex
# Second option: use the open source glpk solver
#LP_SOLVER=GLPK
#GLPK_PATH=glpsol
*)
signature CPLEX =
sig
datatype cplexTerm = cplexVar of string | cplexNum of string | cplexInf
| cplexNeg of cplexTerm
| cplexProd of cplexTerm * cplexTerm
| cplexSum of (cplexTerm list)
datatype cplexComp = cplexLe | cplexLeq | cplexEq | cplexGe | cplexGeq
datatype cplexGoal = cplexMinimize of cplexTerm
| cplexMaximize of cplexTerm
datatype cplexConstr = cplexConstr of cplexComp *
(cplexTerm * cplexTerm)
datatype cplexBounds = cplexBounds of cplexTerm * cplexComp * cplexTerm
* cplexComp * cplexTerm
| cplexBound of cplexTerm * cplexComp * cplexTerm
datatype cplexProg = cplexProg of string
* cplexGoal
* ((string option * cplexConstr)
list)
* cplexBounds list
datatype cplexResult = Unbounded
| Infeasible
| Undefined
| Optimal of string *
(((* name *) string *
(* value *) string) list)
datatype cplexSolver = SOLVER_DEFAULT | SOLVER_CPLEX | SOLVER_GLPK
exception Load_cplexFile of string
exception Load_cplexResult of string
exception Save_cplexFile of string
exception Execute of string
val load_cplexFile : string -> cplexProg
val save_cplexFile : string -> cplexProg -> unit
val elim_nonfree_bounds : cplexProg -> cplexProg
val relax_strict_ineqs : cplexProg -> cplexProg
val is_normed_cplexProg : cplexProg -> bool
val get_solver : unit -> cplexSolver
val set_solver : cplexSolver -> unit
val solve : cplexProg -> cplexResult
end;
structure Cplex : CPLEX =
struct
datatype cplexSolver = SOLVER_DEFAULT | SOLVER_CPLEX | SOLVER_GLPK
val cplexsolver = Unsynchronized.ref SOLVER_DEFAULT;
fun get_solver () = !cplexsolver;
fun set_solver s = (cplexsolver := s);
exception Load_cplexFile of string;
exception Load_cplexResult of string;
exception Save_cplexFile of string;
datatype cplexTerm = cplexVar of string
| cplexNum of string
| cplexInf
| cplexNeg of cplexTerm
| cplexProd of cplexTerm * cplexTerm
| cplexSum of (cplexTerm list)
datatype cplexComp = cplexLe | cplexLeq | cplexEq | cplexGe | cplexGeq
datatype cplexGoal = cplexMinimize of cplexTerm | cplexMaximize of cplexTerm
datatype cplexConstr = cplexConstr of cplexComp * (cplexTerm * cplexTerm)
datatype cplexBounds = cplexBounds of cplexTerm * cplexComp * cplexTerm
* cplexComp * cplexTerm
| cplexBound of cplexTerm * cplexComp * cplexTerm
datatype cplexProg = cplexProg of string
* cplexGoal
* ((string option * cplexConstr) list)
* cplexBounds list
fun rev_cmp cplexLe = cplexGe
| rev_cmp cplexLeq = cplexGeq
| rev_cmp cplexGe = cplexLe
| rev_cmp cplexGeq = cplexLeq
| rev_cmp cplexEq = cplexEq
fun the NONE = raise (Load_cplexFile "SOME expected")
| the (SOME x) = x;
fun modulo_signed is_something (cplexNeg u) = is_something u
| modulo_signed is_something u = is_something u
fun is_Num (cplexNum _) = true
| is_Num _ = false
fun is_Inf cplexInf = true
| is_Inf _ = false
fun is_Var (cplexVar _) = true
| is_Var _ = false
fun is_Neg (cplexNeg _) = true
| is_Neg _ = false
fun is_normed_Prod (cplexProd (t1, t2)) =
(is_Num t1) andalso (is_Var t2)
| is_normed_Prod x = is_Var x
fun is_normed_Sum (cplexSum ts) =
(ts <> []) andalso forall (modulo_signed is_normed_Prod) ts
| is_normed_Sum x = modulo_signed is_normed_Prod x
fun is_normed_Constr (cplexConstr (_, (t1, t2))) =
(is_normed_Sum t1) andalso (modulo_signed is_Num t2)
fun is_Num_or_Inf x = is_Inf x orelse is_Num x
fun is_normed_Bounds (cplexBounds (t1, c1, t2, c2, t3)) =
(c1 = cplexLe orelse c1 = cplexLeq) andalso
(c2 = cplexLe orelse c2 = cplexLeq) andalso
is_Var t2 andalso
modulo_signed is_Num_or_Inf t1 andalso
modulo_signed is_Num_or_Inf t3
| is_normed_Bounds (cplexBound (t1, c, t2)) =
(is_Var t1 andalso (modulo_signed is_Num_or_Inf t2))
orelse
(c <> cplexEq andalso
is_Var t2 andalso (modulo_signed is_Num_or_Inf t1))
fun term_of_goal (cplexMinimize x) = x
| term_of_goal (cplexMaximize x) = x
fun is_normed_cplexProg (cplexProg (_, goal, constraints, bounds)) =
is_normed_Sum (term_of_goal goal) andalso
forall (fn (_,x) => is_normed_Constr x) constraints andalso
forall is_normed_Bounds bounds
fun is_NL s = s = "\n"
fun is_blank s = forall (fn c => c <> #"\n" andalso Char.isSpace c) (String.explode s)
fun is_num a =
let
val b = String.explode a
fun num4 cs = forall Char.isDigit cs
fun num3 [] = true
| num3 (ds as (c::cs)) =
if c = #"+" orelse c = #"-" then
num4 cs
else
num4 ds
fun num2 [] = true
| num2 (c::cs) =
if c = #"e" orelse c = #"E" then num3 cs
else (Char.isDigit c) andalso num2 cs
fun num1 [] = true
| num1 (c::cs) =
if c = #"." then num2 cs
else if c = #"e" orelse c = #"E" then num3 cs
else (Char.isDigit c) andalso num1 cs
fun num [] = true
| num (c::cs) =
if c = #"." then num2 cs
else (Char.isDigit c) andalso num1 cs
in
num b
end
fun is_delimiter s = s = "+" orelse s = "-" orelse s = ":"
fun is_cmp s = s = "<" orelse s = ">" orelse s = "<="
orelse s = ">=" orelse s = "="
fun is_symbol a =
let
val symbol_char = String.explode "!\"#$%&()/,.;?@_`'{}|~"
fun is_symbol_char c = Char.isAlphaNum c orelse
exists (fn d => d=c) symbol_char
fun is_symbol_start c = is_symbol_char c andalso
not (Char.isDigit c) andalso
not (c= #".")
val b = String.explode a
in
b <> [] andalso is_symbol_start (hd b) andalso
forall is_symbol_char b
end
fun to_upper s = String.implode (map Char.toUpper (String.explode s))
fun keyword x =
let
val a = to_upper x
in
if a = "BOUNDS" orelse a = "BOUND" then
SOME "BOUNDS"
else if a = "MINIMIZE" orelse a = "MINIMUM" orelse a = "MIN" then
SOME "MINIMIZE"
else if a = "MAXIMIZE" orelse a = "MAXIMUM" orelse a = "MAX" then
SOME "MAXIMIZE"
else if a = "ST" orelse a = "S.T." orelse a = "ST." then
SOME "ST"
else if a = "FREE" orelse a = "END" then
SOME a
else if a = "GENERAL" orelse a = "GENERALS" orelse a = "GEN" then
SOME "GENERAL"
else if a = "INTEGER" orelse a = "INTEGERS" orelse a = "INT" then
SOME "INTEGER"
else if a = "BINARY" orelse a = "BINARIES" orelse a = "BIN" then
SOME "BINARY"
else if a = "INF" orelse a = "INFINITY" then
SOME "INF"
else
NONE
end
val TOKEN_ERROR = ~1
val TOKEN_BLANK = 0
val TOKEN_NUM = 1
val TOKEN_DELIMITER = 2
val TOKEN_SYMBOL = 3
val TOKEN_LABEL = 4
val TOKEN_CMP = 5
val TOKEN_KEYWORD = 6
val TOKEN_NL = 7
(* tokenize takes a list of chars as argument and returns a list of
int * string pairs, each string representing a "cplex token",
and each int being one of TOKEN_NUM, TOKEN_DELIMITER, TOKEN_CMP
or TOKEN_SYMBOL *)
fun tokenize s =
let
val flist = [(is_NL, TOKEN_NL),
(is_blank, TOKEN_BLANK),
(is_num, TOKEN_NUM),
(is_delimiter, TOKEN_DELIMITER),
(is_cmp, TOKEN_CMP),
(is_symbol, TOKEN_SYMBOL)]
fun match_helper [] s = (fn _ => false, TOKEN_ERROR)
| match_helper (f::fs) s =
if ((fst f) s) then f else match_helper fs s
fun match s = match_helper flist s
fun tok s =
if s = "" then [] else
let
val h = String.substring (s,0,1)
val (f, j) = match h
fun len i =
if size s = i then i
else if f (String.substring (s,0,i+1)) then
len (i+1)
else i
in
if j < 0 then
(if h = "\\" then []
else raise (Load_cplexFile ("token expected, found: "
^s)))
else
let
val l = len 1
val u = String.substring (s,0,l)
val v = String.extract (s,l,NONE)
in
if j = 0 then tok v else (j, u) :: tok v
end
end
in
tok s
end
exception Tokenize of string;
fun tokenize_general flist s =
let
fun match_helper [] s = raise (Tokenize s)
| match_helper (f::fs) s =
if ((fst f) s) then f else match_helper fs s
fun match s = match_helper flist s
fun tok s =
if s = "" then [] else
let
val h = String.substring (s,0,1)
val (f, j) = match h
fun len i =
if size s = i then i
else if f (String.substring (s,0,i+1)) then
len (i+1)
else i
val l = len 1
in
(j, String.substring (s,0,l)) :: tok (String.extract (s,l,NONE))
end
in
tok s
end
fun load_cplexFile name =
let
val f = TextIO.openIn name
val ignore_NL = Unsynchronized.ref true
val rest = Unsynchronized.ref []
fun is_symbol s c = (fst c) = TOKEN_SYMBOL andalso (to_upper (snd c)) = s
fun readToken_helper () =
if length (!rest) > 0 then
let val u = hd (!rest) in
(
rest := tl (!rest);
SOME u
)
end
else
(case TextIO.inputLine f of
NONE => NONE
| SOME s =>
let val t = tokenize s in
if (length t >= 2 andalso
snd(hd (tl t)) = ":")
then
rest := (TOKEN_LABEL, snd (hd t)) :: (tl (tl t))
else if (length t >= 2) andalso is_symbol "SUBJECT" (hd (t))
andalso is_symbol "TO" (hd (tl t))
then
rest := (TOKEN_SYMBOL, "ST") :: (tl (tl t))
else
rest := t;
readToken_helper ()
end)
fun readToken_helper2 () =
let val c = readToken_helper () in
if c = NONE then NONE
else if !ignore_NL andalso fst (the c) = TOKEN_NL then
readToken_helper2 ()
else if fst (the c) = TOKEN_SYMBOL
andalso keyword (snd (the c)) <> NONE
then SOME (TOKEN_KEYWORD, the (keyword (snd (the c))))
else c
end
fun readToken () = readToken_helper2 ()
fun pushToken a = rest := (a::(!rest))
fun is_value token =
fst token = TOKEN_NUM orelse (fst token = TOKEN_KEYWORD
andalso snd token = "INF")
fun get_value token =
if fst token = TOKEN_NUM then
cplexNum (snd token)
else if fst token = TOKEN_KEYWORD andalso snd token = "INF"
then
cplexInf
else
raise (Load_cplexFile "num expected")
fun readTerm_Product only_num =
let val c = readToken () in
if c = NONE then NONE
else if fst (the c) = TOKEN_SYMBOL
then (
if only_num then (pushToken (the c); NONE)
else SOME (cplexVar (snd (the c)))
)
else if only_num andalso is_value (the c) then
SOME (get_value (the c))
else if is_value (the c) then
let val t1 = get_value (the c)
val d = readToken ()
in
if d = NONE then SOME t1
else if fst (the d) = TOKEN_SYMBOL then
SOME (cplexProd (t1, cplexVar (snd (the d))))
else
(pushToken (the d); SOME t1)
end
else (pushToken (the c); NONE)
end
fun readTerm_Signed only_signed only_num =
let
val c = readToken ()
in
if c = NONE then NONE
else
let val d = the c in
if d = (TOKEN_DELIMITER, "+") then
readTerm_Product only_num
else if d = (TOKEN_DELIMITER, "-") then
SOME (cplexNeg (the (readTerm_Product
only_num)))
else (pushToken d;
if only_signed then NONE
else readTerm_Product only_num)
end
end
fun readTerm_Sum first_signed =
let val c = readTerm_Signed first_signed false in
if c = NONE then [] else (the c)::(readTerm_Sum true)
end
fun readTerm () =
let val c = readTerm_Sum false in
if c = [] then NONE
else if tl c = [] then SOME (hd c)
else SOME (cplexSum c)
end
fun readLabeledTerm () =
let val c = readToken () in
if c = NONE then (NONE, NONE)
else if fst (the c) = TOKEN_LABEL then
let val t = readTerm () in
if t = NONE then
raise (Load_cplexFile ("term after label "^
(snd (the c))^
" expected"))
else (SOME (snd (the c)), t)
end
else (pushToken (the c); (NONE, readTerm ()))
end
fun readGoal () =
let
val g = readToken ()
in
if g = SOME (TOKEN_KEYWORD, "MAXIMIZE") then
cplexMaximize (the (snd (readLabeledTerm ())))
else if g = SOME (TOKEN_KEYWORD, "MINIMIZE") then
cplexMinimize (the (snd (readLabeledTerm ())))
else raise (Load_cplexFile "MAXIMIZE or MINIMIZE expected")
end
fun str2cmp b =
(case b of
"<" => cplexLe
| "<=" => cplexLeq
| ">" => cplexGe
| ">=" => cplexGeq
| "=" => cplexEq
| _ => raise (Load_cplexFile (b^" is no TOKEN_CMP")))
fun readConstraint () =
let
val t = readLabeledTerm ()
fun make_constraint b t1 t2 =
cplexConstr
(str2cmp b,
(t1, t2))
in
if snd t = NONE then NONE
else
let val c = readToken () in
if c = NONE orelse fst (the c) <> TOKEN_CMP
then raise (Load_cplexFile "TOKEN_CMP expected")
else
let val n = readTerm_Signed false true in
if n = NONE then
raise (Load_cplexFile "num expected")
else
SOME (fst t,
make_constraint (snd (the c))
(the (snd t))
(the n))
end
end
end
fun readST () =
let
fun readbody () =
let val t = readConstraint () in
if t = NONE then []
else if (is_normed_Constr (snd (the t))) then
(the t)::(readbody ())
else if (fst (the t) <> NONE) then
raise (Load_cplexFile
("constraint '"^(the (fst (the t)))^
"'is not normed"))
else
raise (Load_cplexFile
"constraint is not normed")
end
in
if readToken () = SOME (TOKEN_KEYWORD, "ST")
then
readbody ()
else
raise (Load_cplexFile "ST expected")
end
fun readCmp () =
let val c = readToken () in
if c = NONE then NONE
else if fst (the c) = TOKEN_CMP then
SOME (str2cmp (snd (the c)))
else (pushToken (the c); NONE)
end
fun skip_NL () =
let val c = readToken () in
if c <> NONE andalso fst (the c) = TOKEN_NL then
skip_NL ()
else
(pushToken (the c); ())
end
fun make_bounds c t1 t2 =
cplexBound (t1, c, t2)
fun readBound () =
let
val _ = skip_NL ()
val t1 = readTerm ()
in
if t1 = NONE then NONE
else
let
val c1 = readCmp ()
in
if c1 = NONE then
let
val c = readToken ()
in
if c = SOME (TOKEN_KEYWORD, "FREE") then
SOME (
cplexBounds (cplexNeg cplexInf,
cplexLeq,
the t1,
cplexLeq,
cplexInf))
else
raise (Load_cplexFile "FREE expected")
end
else
let
val t2 = readTerm ()
in
if t2 = NONE then
raise (Load_cplexFile "term expected")
else
let val c2 = readCmp () in
if c2 = NONE then
SOME (make_bounds (the c1)
(the t1)
(the t2))
else
SOME (
cplexBounds (the t1,
the c1,
the t2,
the c2,
the (readTerm())))
end
end
end
end
fun readBounds () =
let
fun makestring _ = "?"
fun readbody () =
let
val b = readBound ()
in
if b = NONE then []
else if (is_normed_Bounds (the b)) then
(the b)::(readbody())
else (
raise (Load_cplexFile
("bounds are not normed in: "^
(makestring (the b)))))
end
in
if readToken () = SOME (TOKEN_KEYWORD, "BOUNDS") then
readbody ()
else raise (Load_cplexFile "BOUNDS expected")
end
fun readEnd () =
if readToken () = SOME (TOKEN_KEYWORD, "END") then ()
else raise (Load_cplexFile "END expected")
val result_Goal = readGoal ()
val result_ST = readST ()
val _ = ignore_NL := false
val result_Bounds = readBounds ()
val _ = ignore_NL := true
val _ = readEnd ()
val _ = TextIO.closeIn f
in
cplexProg (name, result_Goal, result_ST, result_Bounds)
end
fun save_cplexFile filename (cplexProg (_, goal, constraints, bounds)) =
let
val f = TextIO.openOut filename
fun basic_write s = TextIO.output(f, s)
val linebuf = Unsynchronized.ref ""
fun buf_flushline s =
(basic_write (!linebuf);
basic_write "\n";
linebuf := s)
fun buf_add s = linebuf := (!linebuf) ^ s
fun write s =
if (String.size s) + (String.size (!linebuf)) >= 250 then
buf_flushline (" "^s)
else
buf_add s
fun writeln s = (buf_add s; buf_flushline "")
fun write_term (cplexVar x) = write x
| write_term (cplexNum x) = write x
| write_term cplexInf = write "inf"
| write_term (cplexProd (cplexNum "1", b)) = write_term b
| write_term (cplexProd (a, b)) =
(write_term a; write " "; write_term b)
| write_term (cplexNeg x) = (write " - "; write_term x)
| write_term (cplexSum ts) = write_terms ts
and write_terms [] = ()
| write_terms (t::ts) =
(if (not (is_Neg t)) then write " + " else ();
write_term t; write_terms ts)
fun write_goal (cplexMaximize term) =
(writeln "MAXIMIZE"; write_term term; writeln "")
| write_goal (cplexMinimize term) =
(writeln "MINIMIZE"; write_term term; writeln "")
fun write_cmp cplexLe = write "<"
| write_cmp cplexLeq = write "<="
| write_cmp cplexEq = write "="
| write_cmp cplexGe = write ">"
| write_cmp cplexGeq = write ">="
fun write_constr (cplexConstr (cmp, (a,b))) =
(write_term a;
write " ";
write_cmp cmp;
write " ";
write_term b)
fun write_constraints [] = ()
| write_constraints (c::cs) =
(if (fst c <> NONE)
then
(write (the (fst c)); write ": ")
else
();
write_constr (snd c);
writeln "";
write_constraints cs)
fun write_bounds [] = ()
| write_bounds ((cplexBounds (t1,c1,t2,c2,t3))::bs) =
((if t1 = cplexNeg cplexInf andalso t3 = cplexInf
andalso (c1 = cplexLeq orelse c1 = cplexLe)
andalso (c2 = cplexLeq orelse c2 = cplexLe)
then
(write_term t2; write " free")
else
(write_term t1; write " "; write_cmp c1; write " ";
write_term t2; write " "; write_cmp c2; write " ";
write_term t3)
); writeln ""; write_bounds bs)
| write_bounds ((cplexBound (t1, c, t2)) :: bs) =
(write_term t1; write " ";
write_cmp c; write " ";
write_term t2; writeln ""; write_bounds bs)
val _ = write_goal goal
val _ = (writeln ""; writeln "ST")
val _ = write_constraints constraints
val _ = (writeln ""; writeln "BOUNDS")
val _ = write_bounds bounds
val _ = (writeln ""; writeln "END")
val _ = TextIO.closeOut f
in
()
end
fun norm_Constr (constr as cplexConstr (c, (t1, t2))) =
if not (modulo_signed is_Num t2) andalso
modulo_signed is_Num t1
then
[cplexConstr (rev_cmp c, (t2, t1))]
else if (c = cplexLe orelse c = cplexLeq) andalso
(t1 = (cplexNeg cplexInf) orelse t2 = cplexInf)
then
[]
else if (c = cplexGe orelse c = cplexGeq) andalso
(t1 = cplexInf orelse t2 = cplexNeg cplexInf)
then
[]
else
[constr]
fun bound2constr (cplexBounds (t1,c1,t2,c2,t3)) =
(norm_Constr(cplexConstr (c1, (t1, t2))))
@ (norm_Constr(cplexConstr (c2, (t2, t3))))
| bound2constr (cplexBound (t1, cplexEq, t2)) =
(norm_Constr(cplexConstr (cplexLeq, (t1, t2))))
@ (norm_Constr(cplexConstr (cplexLeq, (t2, t1))))
| bound2constr (cplexBound (t1, c1, t2)) =
norm_Constr(cplexConstr (c1, (t1,t2)))
val emptyset = Symtab.empty
fun singleton v = Symtab.update (v, ()) emptyset
fun merge a b = Symtab.merge (op =) (a, b)
fun mergemap f ts = fold (fn x => fn table => merge table (f x)) ts Symtab.empty
fun diff a b = Symtab.fold (Symtab.delete_safe o fst) b a
fun collect_vars (cplexVar v) = singleton v
| collect_vars (cplexNeg t) = collect_vars t
| collect_vars (cplexProd (t1, t2)) =
merge (collect_vars t1) (collect_vars t2)
| collect_vars (cplexSum ts) = mergemap collect_vars ts
| collect_vars _ = emptyset
(* Eliminates all nonfree bounds from the linear program and produces an
equivalent program with only free bounds
IF for the input program P holds: is_normed_cplexProg P *)
fun elim_nonfree_bounds (cplexProg (name, goal, constraints, bounds)) =
let
fun collect_constr_vars (_, cplexConstr (_, (t1,_))) =
(collect_vars t1)
val cvars = merge (collect_vars (term_of_goal goal))
(mergemap collect_constr_vars constraints)
fun collect_lower_bounded_vars
(cplexBounds (_, _, cplexVar v, _, _)) =
singleton v
| collect_lower_bounded_vars
(cplexBound (_, cplexLe, cplexVar v)) =
singleton v
| collect_lower_bounded_vars
(cplexBound (_, cplexLeq, cplexVar v)) =
singleton v
| collect_lower_bounded_vars
(cplexBound (cplexVar v, cplexGe,_)) =
singleton v
| collect_lower_bounded_vars
(cplexBound (cplexVar v, cplexGeq, _)) =
singleton v
| collect_lower_bounded_vars
(cplexBound (cplexVar v, cplexEq, _)) =
singleton v
| collect_lower_bounded_vars _ = emptyset
val lvars = mergemap collect_lower_bounded_vars bounds
val positive_vars = diff cvars lvars
val zero = cplexNum "0"
fun make_pos_constr v =
(NONE, cplexConstr (cplexGeq, ((cplexVar v), zero)))
fun make_free_bound v =
cplexBounds (cplexNeg cplexInf, cplexLeq,
cplexVar v, cplexLeq,
cplexInf)
val pos_constrs = rev (Symtab.fold
(fn (k, _) => cons (make_pos_constr k))
positive_vars [])
val bound_constrs = map (pair NONE)
(maps bound2constr bounds)
val constraints' = constraints @ pos_constrs @ bound_constrs
val bounds' = rev (Symtab.fold (fn (v, _) => cons (make_free_bound v)) cvars []);
in
cplexProg (name, goal, constraints', bounds')
end
fun relax_strict_ineqs (cplexProg (name, goals, constrs, bounds)) =
let
fun relax cplexLe = cplexLeq
| relax cplexGe = cplexGeq
| relax x = x
fun relax_constr (n, cplexConstr(c, (t1, t2))) =
(n, cplexConstr(relax c, (t1, t2)))
fun relax_bounds (cplexBounds (t1, c1, t2, c2, t3)) =
cplexBounds (t1, relax c1, t2, relax c2, t3)
| relax_bounds (cplexBound (t1, c, t2)) =
cplexBound (t1, relax c, t2)
in
cplexProg (name,
goals,
map relax_constr constrs,
map relax_bounds bounds)
end
datatype cplexResult = Unbounded
| Infeasible
| Undefined
| Optimal of string * ((string * string) list)
fun is_separator x = forall (fn c => c = #"-") (String.explode x)
fun is_sign x = (x = "+" orelse x = "-")
fun is_colon x = (x = ":")
fun is_resultsymbol a =
let
val symbol_char = String.explode "!\"#$%&()/,.;?@_`'{}|~-"
fun is_symbol_char c = Char.isAlphaNum c orelse
exists (fn d => d=c) symbol_char
fun is_symbol_start c = is_symbol_char c andalso
not (Char.isDigit c) andalso
not (c= #".") andalso
not (c= #"-")
val b = String.explode a
in
b <> [] andalso is_symbol_start (hd b) andalso
forall is_symbol_char b
end
val TOKEN_SIGN = 100
val TOKEN_COLON = 101
val TOKEN_SEPARATOR = 102
fun load_glpkResult name =
let
val flist = [(is_NL, TOKEN_NL),
(is_blank, TOKEN_BLANK),
(is_num, TOKEN_NUM),
(is_sign, TOKEN_SIGN),
(is_colon, TOKEN_COLON),
(is_cmp, TOKEN_CMP),
(is_resultsymbol, TOKEN_SYMBOL),
(is_separator, TOKEN_SEPARATOR)]
val tokenize = tokenize_general flist
val f = TextIO.openIn name
val rest = Unsynchronized.ref []
fun readToken_helper () =
if length (!rest) > 0 then
let val u = hd (!rest) in
(
rest := tl (!rest);
SOME u
)
end
else
(case TextIO.inputLine f of
NONE => NONE
| SOME s => (rest := tokenize s; readToken_helper()))
fun is_tt tok ty = (tok <> NONE andalso (fst (the tok)) = ty)
fun pushToken a = if a = NONE then () else (rest := ((the a)::(!rest)))
fun readToken () =
let val t = readToken_helper () in
if is_tt t TOKEN_BLANK then
readToken ()
else if is_tt t TOKEN_NL then
let val t2 = readToken_helper () in
if is_tt t2 TOKEN_SIGN then
(pushToken (SOME (TOKEN_SEPARATOR, "-")); t)
else
(pushToken t2; t)
end
else if is_tt t TOKEN_SIGN then
let val t2 = readToken_helper () in
if is_tt t2 TOKEN_NUM then
(SOME (TOKEN_NUM, (snd (the t))^(snd (the t2))))
else
(pushToken t2; t)
end
else
t
end
fun readRestOfLine P =
let
val t = readToken ()
in
if is_tt t TOKEN_NL orelse t = NONE
then P
else readRestOfLine P
end
fun readHeader () =
let
fun readStatus () = readRestOfLine ("STATUS", snd (the (readToken ())))
fun readObjective () = readRestOfLine ("OBJECTIVE", snd (the (readToken (); readToken (); readToken ())))
val t1 = readToken ()
val t2 = readToken ()
in
if is_tt t1 TOKEN_SYMBOL andalso is_tt t2 TOKEN_COLON
then
case to_upper (snd (the t1)) of
"STATUS" => (readStatus ())::(readHeader ())
| "OBJECTIVE" => (readObjective())::(readHeader ())
| _ => (readRestOfLine (); readHeader ())
else
(pushToken t2; pushToken t1; [])
end
fun skip_until_sep () =
let val x = readToken () in
if is_tt x TOKEN_SEPARATOR then
readRestOfLine ()
else
skip_until_sep ()
end
fun load_value () =
let
val t1 = readToken ()
val t2 = readToken ()
in
if is_tt t1 TOKEN_NUM andalso is_tt t2 TOKEN_SYMBOL then
let
val t = readToken ()
val state = if is_tt t TOKEN_NL then readToken () else t
val _ = if is_tt state TOKEN_SYMBOL then () else raise (Load_cplexResult "state expected")
val k = readToken ()
in
if is_tt k TOKEN_NUM then
readRestOfLine (SOME (snd (the t2), snd (the k)))
else
raise (Load_cplexResult "number expected")
end
else
(pushToken t2; pushToken t1; NONE)
end
fun load_values () =
let val v = load_value () in
if v = NONE then [] else (the v)::(load_values ())
end
val header = readHeader ()
val result =
case AList.lookup (op =) header "STATUS" of
SOME "INFEASIBLE" => Infeasible
| SOME "UNBOUNDED" => Unbounded
| SOME "OPTIMAL" => Optimal (the (AList.lookup (op =) header "OBJECTIVE"),
(skip_until_sep ();
skip_until_sep ();
load_values ()))
| _ => Undefined
val _ = TextIO.closeIn f
in
result
end
handle (Tokenize s) => raise (Load_cplexResult ("Tokenize: "^s))
| Option.Option => raise (Load_cplexResult "Option")
fun load_cplexResult name =
let
val flist = [(is_NL, TOKEN_NL),
(is_blank, TOKEN_BLANK),
(is_num, TOKEN_NUM),
(is_sign, TOKEN_SIGN),
(is_colon, TOKEN_COLON),
(is_cmp, TOKEN_CMP),
(is_resultsymbol, TOKEN_SYMBOL)]
val tokenize = tokenize_general flist
val f = TextIO.openIn name
val rest = Unsynchronized.ref []
fun readToken_helper () =
if length (!rest) > 0 then
let val u = hd (!rest) in
(
rest := tl (!rest);
SOME u
)
end
else
(case TextIO.inputLine f of
NONE => NONE
| SOME s => (rest := tokenize s; readToken_helper()))
fun is_tt tok ty = (tok <> NONE andalso (fst (the tok)) = ty)
fun pushToken a = if a = NONE then () else (rest := ((the a)::(!rest)))
fun readToken () =
let val t = readToken_helper () in
if is_tt t TOKEN_BLANK then
readToken ()
else if is_tt t TOKEN_SIGN then
let val t2 = readToken_helper () in
if is_tt t2 TOKEN_NUM then
(SOME (TOKEN_NUM, (snd (the t))^(snd (the t2))))
else
(pushToken t2; t)
end
else
t
end
fun readRestOfLine P =
let
val t = readToken ()
in
if is_tt t TOKEN_NL orelse t = NONE
then P
else readRestOfLine P
end
fun readHeader () =
let
fun readStatus () = readRestOfLine ("STATUS", snd (the (readToken ())))
fun readObjective () =
let
val t = readToken ()
in
if is_tt t TOKEN_SYMBOL andalso to_upper (snd (the t)) = "VALUE" then
readRestOfLine ("OBJECTIVE", snd (the (readToken())))
else
readRestOfLine ("OBJECTIVE_NAME", snd (the t))
end
val t = readToken ()
in
if is_tt t TOKEN_SYMBOL then
case to_upper (snd (the t)) of
"STATUS" => (readStatus ())::(readHeader ())
| "OBJECTIVE" => (readObjective ())::(readHeader ())
| "SECTION" => (pushToken t; [])
| _ => (readRestOfLine (); readHeader ())
else
(readRestOfLine (); readHeader ())
end
fun skip_nls () =
let val x = readToken () in
if is_tt x TOKEN_NL then
skip_nls ()
else
(pushToken x; ())
end
fun skip_paragraph () =
if is_tt (readToken ()) TOKEN_NL then
(if is_tt (readToken ()) TOKEN_NL then
skip_nls ()
else
skip_paragraph ())
else
skip_paragraph ()
fun load_value () =
let
val t1 = readToken ()
val t1 = if is_tt t1 TOKEN_SYMBOL andalso snd (the t1) = "A" then readToken () else t1
in
if is_tt t1 TOKEN_NUM then
let
val name = readToken ()
val status = readToken ()
val value = readToken ()
in
if is_tt name TOKEN_SYMBOL andalso
is_tt status TOKEN_SYMBOL andalso
is_tt value TOKEN_NUM
then
readRestOfLine (SOME (snd (the name), snd (the value)))
else
raise (Load_cplexResult "column line expected")
end
else
(pushToken t1; NONE)
end
fun load_values () =
let val v = load_value () in
if v = NONE then [] else (the v)::(load_values ())
end
val header = readHeader ()
val result =
case AList.lookup (op =) header "STATUS" of
SOME "INFEASIBLE" => Infeasible
| SOME "NONOPTIMAL" => Unbounded
| SOME "OPTIMAL" => Optimal (the (AList.lookup (op =) header "OBJECTIVE"),
(skip_paragraph ();
skip_paragraph ();
skip_paragraph ();
skip_paragraph ();
skip_paragraph ();
load_values ()))
| _ => Undefined
val _ = TextIO.closeIn f
in
result
end
handle (Tokenize s) => raise (Load_cplexResult ("Tokenize: "^s))
| Option.Option => raise (Load_cplexResult "Option")
exception Execute of string;
fun tmp_file s = Path.implode (Path.expand (File.tmp_path (Path.basic s)));
fun wrap s = "\""^s^"\"";
fun solve_glpk prog =
let
val name = string_of_int (Time.toMicroseconds (Time.now ()))
val lpname = tmp_file (name^".lp")
val resultname = tmp_file (name^".txt")
val _ = save_cplexFile lpname prog
val cplex_path = getenv "GLPK_PATH"
val cplex = if cplex_path = "" then "glpsol" else cplex_path
val command = (wrap cplex)^" --lpt "^(wrap lpname)^" --output "^(wrap resultname)
val answer = #1 (Isabelle_System.bash_output command)
in
let
val result = load_glpkResult resultname
val _ = OS.FileSys.remove lpname
val _ = OS.FileSys.remove resultname
in
result
end
handle (Load_cplexResult s) => raise (Execute ("Load_cplexResult: "^s^"\nExecute: "^answer))
| exn => if Exn.is_interrupt exn then reraise exn else raise (Execute answer)
end
fun solve_cplex prog =
let
fun write_script s lp r =
let
val f = TextIO.openOut s
val _ = TextIO.output (f, "read\n"^lp^"\noptimize\nwrite\n"^r^"\nquit")
val _ = TextIO.closeOut f
in
()
end
val name = string_of_int (Time.toMicroseconds (Time.now ()))
val lpname = tmp_file (name^".lp")
val resultname = tmp_file (name^".txt")
val scriptname = tmp_file (name^".script")
val _ = save_cplexFile lpname prog
val _ = write_script scriptname lpname resultname
in
let
val result = load_cplexResult resultname
val _ = OS.FileSys.remove lpname
val _ = OS.FileSys.remove resultname
val _ = OS.FileSys.remove scriptname
in
result
end
end
fun solve prog =
case get_solver () of
SOLVER_DEFAULT =>
(case getenv "LP_SOLVER" of
"CPLEX" => solve_cplex prog
| "GLPK" => solve_glpk prog
| _ => raise (Execute ("LP_SOLVER must be set to CPLEX or to GLPK")))
| SOLVER_CPLEX => solve_cplex prog
| SOLVER_GLPK => solve_glpk prog
end;