src/HOL/Matrix_LP/Cplex_tools.ML
author wenzelm
Sat May 11 16:57:18 2013 +0200 (2013-05-11)
changeset 51930 52fd62618631
parent 50902 cb2b940e2fdf
child 51940 958d439b3013
permissions -rw-r--r--
prefer explicitly qualified exceptions, which is particular important for robust handlers;
     1 (*  Title:      HOL/Matrix_LP/Cplex_tools.ML
     2     Author:     Steven Obua
     3 *)
     4 
     5 signature CPLEX =
     6 sig
     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)
    37 
    38     datatype cplexSolver = SOLVER_DEFAULT | SOLVER_CPLEX | SOLVER_GLPK
    39 
    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 
    47     val save_cplexFile : string -> cplexProg -> unit
    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 
    55     val get_solver : unit -> cplexSolver
    56     val set_solver : cplexSolver -> unit
    57     val solve : cplexProg -> cplexResult
    58 end;
    59 
    60 structure Cplex  : CPLEX =
    61 struct
    62 
    63 datatype cplexSolver = SOLVER_DEFAULT | SOLVER_CPLEX | SOLVER_GLPK
    64 
    65 val cplexsolver = Unsynchronized.ref SOLVER_DEFAULT;
    66 fun get_solver () = !cplexsolver;
    67 fun set_solver s = (cplexsolver := s);
    68 
    69 exception Load_cplexFile of string;
    70 exception Load_cplexResult of string;
    71 exception Save_cplexFile of string;
    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
    80 datatype cplexGoal = cplexMinimize of cplexTerm | cplexMaximize of cplexTerm
    81 datatype cplexConstr = cplexConstr of cplexComp * (cplexTerm * cplexTerm)
    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 
    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")
    97   | the (SOME x) = x;
    98 
    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 _) = true
   112   | is_Neg _ = false
   113 
   114 fun is_normed_Prod (cplexProd (t1, t2)) =
   115     (is_Num t1) andalso (is_Var t2)
   116   | is_normed_Prod x = is_Var x
   117 
   118 fun is_normed_Sum (cplexSum ts) =
   119     (ts <> []) andalso forall (modulo_signed is_normed_Prod) ts
   120   | is_normed_Sum x = modulo_signed is_normed_Prod x
   121 
   122 fun is_normed_Constr (cplexConstr (_, (t1, t2))) =
   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)) =
   128     (c1 = cplexLe orelse c1 = cplexLeq) andalso
   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)) =
   134     (is_Var t1 andalso (modulo_signed is_Num_or_Inf t2))
   135     orelse
   136     (c <> cplexEq andalso
   137      is_Var t2 andalso (modulo_signed is_Num_or_Inf t1))
   138 
   139 fun term_of_goal (cplexMinimize x) = x
   140   | term_of_goal (cplexMaximize x) = x
   141 
   142 fun is_normed_cplexProg (cplexProg (_, goal, constraints, bounds)) =
   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)
   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
   174     in
   175     num b
   176     end
   177 
   178 fun is_delimiter s = s = "+" orelse s = "-" orelse s = ":"
   179 
   180 fun is_cmp s = s = "<" orelse s = ">" orelse s = "<="
   181              orelse s = ">=" orelse s = "="
   182 
   183 fun is_symbol a =
   184     let
   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
   192     in
   193     b <> [] andalso is_symbol_start (hd b) andalso
   194     forall is_symbol_char b
   195     end
   196 
   197 fun to_upper s = String.implode (map Char.toUpper (String.explode s))
   198 
   199 fun keyword x =
   200     let
   201     val a = to_upper x
   202     in
   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
   223     end
   224 
   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
   234 
   235 (* tokenize takes a list of chars as argument and returns a list of
   236    int * string pairs, each string representing a "cplex token",
   237    and each int being one of TOKEN_NUM, TOKEN_DELIMITER, TOKEN_CMP
   238    or TOKEN_SYMBOL *)
   239 fun tokenize s =
   240     let
   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 _ => 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
   275     in
   276     tok s
   277     end
   278 
   279 exception Tokenize of string;
   280 
   281 fun tokenize_general flist s =
   282     let
   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
   301     in
   302     tok s
   303     end
   304 
   305 fun load_cplexFile name =
   306     let
   307     val f = TextIO.openIn name
   308         val ignore_NL = Unsynchronized.ref true
   309     val rest = Unsynchronized.ref []
   310 
   311     fun is_symbol s c = (fst c) = TOKEN_SYMBOL andalso (to_upper (snd c)) = s
   312 
   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
   322           (case TextIO.inputLine f of
   323             NONE => NONE
   324           | SOME s =>
   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 
   339     fun readToken_helper2 () =
   340         let val c = readToken_helper () in
   341             if c = NONE then NONE
   342                     else if !ignore_NL andalso fst (the c) = TOKEN_NL then
   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")
   366 
   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
   451                | "=" => cplexEq
   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
   479 
   480         fun readST () =
   481         let
   482         fun readbody () =
   483             let val t = readConstraint () in
   484             if t = NONE then []
   485             else if (is_normed_Constr (snd (the t))) then
   486                 (the t)::(readbody ())
   487             else if (fst (the t) <> NONE) then
   488                 raise (Load_cplexFile
   489                        ("constraint '"^(the (fst (the t)))^
   490                     "'is not normed"))
   491             else
   492                 raise (Load_cplexFile
   493                        "constraint is not normed")
   494             end
   495         in
   496         if readToken () = SOME (TOKEN_KEYWORD, "ST")
   497         then
   498             readbody ()
   499         else
   500             raise (Load_cplexFile "ST expected")
   501         end
   502 
   503     fun readCmp () =
   504         let val c = readToken () in
   505         if c = NONE then NONE
   506         else if fst (the c) = TOKEN_CMP then
   507             SOME (str2cmp (snd (the c)))
   508         else (pushToken (the c); NONE)
   509         end
   510 
   511     fun skip_NL () =
   512         let val c = readToken () in
   513         if c <> NONE andalso fst (the c) = TOKEN_NL then
   514             skip_NL ()
   515         else
   516             (pushToken (the c); ())
   517         end
   518 
   519     fun make_bounds c t1 t2 =
   520         cplexBound (t1, c, t2)
   521 
   522     fun readBound () =
   523         let
   524         val _ = skip_NL ()
   525         val t1 = readTerm ()
   526         in
   527         if t1 = NONE then NONE
   528         else
   529             let
   530             val c1 = readCmp ()
   531             in
   532             if c1 = NONE then
   533                 let
   534                 val c = readToken ()
   535                 in
   536                 if c = SOME (TOKEN_KEYWORD, "FREE") then
   537                     SOME (
   538                     cplexBounds (cplexNeg cplexInf,
   539                          cplexLeq,
   540                          the t1,
   541                          cplexLeq,
   542                          cplexInf))
   543                 else
   544                     raise (Load_cplexFile "FREE expected")
   545                 end
   546             else
   547                 let
   548                 val t2 = readTerm ()
   549                 in
   550                 if t2 = NONE then
   551                     raise (Load_cplexFile "term expected")
   552                 else
   553                     let val c2 = readCmp () in
   554                     if c2 = NONE then
   555                         SOME (make_bounds (the c1)
   556                                   (the t1)
   557                                   (the t2))
   558                     else
   559                         SOME (
   560                         cplexBounds (the t1,
   561                              the c1,
   562                              the t2,
   563                              the c2,
   564                              the (readTerm())))
   565                     end
   566                 end
   567             end
   568         end
   569 
   570     fun readBounds () =
   571         let
   572         fun makestring _ = "?"
   573         fun readbody () =
   574             let
   575             val b = readBound ()
   576             in
   577             if b = NONE then []
   578             else if (is_normed_Bounds (the b)) then
   579                 (the b)::(readbody())
   580             else (
   581                 raise (Load_cplexFile
   582                        ("bounds are not normed in: "^
   583                     (makestring (the b)))))
   584             end
   585         in
   586         if readToken () = SOME (TOKEN_KEYWORD, "BOUNDS") then
   587             readbody ()
   588         else raise (Load_cplexFile "BOUNDS expected")
   589         end
   590 
   591         fun readEnd () =
   592         if readToken () = SOME (TOKEN_KEYWORD, "END") then ()
   593         else raise (Load_cplexFile "END expected")
   594 
   595     val result_Goal = readGoal ()
   596     val result_ST = readST ()
   597     val _ =    ignore_NL := false
   598         val result_Bounds = readBounds ()
   599         val _ = ignore_NL := true
   600         val _ = readEnd ()
   601     val _ = TextIO.closeIn f
   602     in
   603     cplexProg (name, result_Goal, result_ST, result_Bounds)
   604     end
   605 
   606 fun save_cplexFile filename (cplexProg (_, goal, constraints, bounds)) =
   607     let
   608     val f = TextIO.openOut filename
   609 
   610     fun basic_write s = TextIO.output(f, s)
   611 
   612     val linebuf = Unsynchronized.ref ""
   613     fun buf_flushline s =
   614         (basic_write (!linebuf);
   615          basic_write "\n";
   616          linebuf := s)
   617     fun buf_add s = linebuf := (!linebuf) ^ s
   618 
   619     fun write s =
   620         if (String.size s) + (String.size (!linebuf)) >= 250 then
   621         buf_flushline ("    "^s)
   622         else
   623         buf_add s
   624 
   625         fun writeln s = (buf_add s; buf_flushline "")
   626 
   627     fun write_term (cplexVar x) = write x
   628       | write_term (cplexNum x) = write x
   629       | write_term cplexInf = write "inf"
   630       | write_term (cplexProd (cplexNum "1", b)) = write_term b
   631       | write_term (cplexProd (a, b)) =
   632         (write_term a; write " "; write_term b)
   633           | write_term (cplexNeg x) = (write " - "; write_term x)
   634           | write_term (cplexSum ts) = write_terms ts
   635     and write_terms [] = ()
   636       | write_terms (t::ts) =
   637         (if (not (is_Neg t)) then write " + " else ();
   638          write_term t; write_terms ts)
   639 
   640     fun write_goal (cplexMaximize term) =
   641         (writeln "MAXIMIZE"; write_term term; writeln "")
   642       | write_goal (cplexMinimize term) =
   643         (writeln "MINIMIZE"; write_term term; writeln "")
   644 
   645     fun write_cmp cplexLe = write "<"
   646       | write_cmp cplexLeq = write "<="
   647       | write_cmp cplexEq = write "="
   648       | write_cmp cplexGe = write ">"
   649       | write_cmp cplexGeq = write ">="
   650 
   651     fun write_constr (cplexConstr (cmp, (a,b))) =
   652         (write_term a;
   653          write " ";
   654          write_cmp cmp;
   655          write " ";
   656          write_term b)
   657 
   658     fun write_constraints [] = ()
   659       | write_constraints (c::cs) =
   660         (if (fst c <> NONE)
   661          then
   662          (write (the (fst c)); write ": ")
   663          else
   664          ();
   665          write_constr (snd c);
   666          writeln "";
   667          write_constraints cs)
   668 
   669     fun write_bounds [] = ()
   670       | write_bounds ((cplexBounds (t1,c1,t2,c2,t3))::bs) =
   671         ((if t1 = cplexNeg cplexInf andalso t3 = cplexInf
   672          andalso (c1 = cplexLeq orelse c1 = cplexLe)
   673          andalso (c2 = cplexLeq orelse c2 = cplexLe)
   674           then
   675           (write_term t2; write " free")
   676           else
   677           (write_term t1; write " "; write_cmp c1; write " ";
   678            write_term t2; write " "; write_cmp c2; write " ";
   679            write_term t3)
   680          ); writeln ""; write_bounds bs)
   681       | write_bounds ((cplexBound (t1, c, t2)) :: bs) =
   682         (write_term t1; write " ";
   683          write_cmp c; write " ";
   684          write_term t2; writeln ""; write_bounds bs)
   685 
   686     val _ = write_goal goal
   687         val _ = (writeln ""; writeln "ST")
   688     val _ = write_constraints constraints
   689         val _ = (writeln ""; writeln "BOUNDS")
   690     val _ = write_bounds bounds
   691         val _ = (writeln ""; writeln "END")
   692         val _ = TextIO.closeOut f
   693     in
   694     ()
   695     end
   696 
   697 fun norm_Constr (constr as cplexConstr (c, (t1, t2))) =
   698     if not (modulo_signed is_Num t2) andalso
   699        modulo_signed is_Num t1
   700     then
   701     [cplexConstr (rev_cmp c, (t2, t1))]
   702     else if (c = cplexLe orelse c = cplexLeq) andalso
   703         (t1 = (cplexNeg cplexInf) orelse t2 = cplexInf)
   704     then
   705     []
   706     else if (c = cplexGe orelse c = cplexGeq) andalso
   707         (t1 = cplexInf orelse t2 = cplexNeg cplexInf)
   708     then
   709     []
   710     else
   711     [constr]
   712 
   713 fun bound2constr (cplexBounds (t1,c1,t2,c2,t3)) =
   714     (norm_Constr(cplexConstr (c1, (t1, t2))))
   715     @ (norm_Constr(cplexConstr (c2, (t2, t3))))
   716   | bound2constr (cplexBound (t1, cplexEq, t2)) =
   717     (norm_Constr(cplexConstr (cplexLeq, (t1, t2))))
   718     @ (norm_Constr(cplexConstr (cplexLeq, (t2, t1))))
   719   | bound2constr (cplexBound (t1, c1, t2)) =
   720     norm_Constr(cplexConstr (c1, (t1,t2)))
   721 
   722 val emptyset = Symtab.empty
   723 
   724 fun singleton v = Symtab.update (v, ()) emptyset
   725 
   726 fun merge a b = Symtab.merge (op =) (a, b)
   727 
   728 fun mergemap f ts = fold (fn x => fn table => merge table (f x)) ts Symtab.empty
   729 
   730 fun diff a b = Symtab.fold (Symtab.delete_safe o fst) b a
   731 
   732 fun collect_vars (cplexVar v) = singleton v
   733   | collect_vars (cplexNeg t) = collect_vars t
   734   | collect_vars (cplexProd (t1, t2)) =
   735     merge (collect_vars t1) (collect_vars t2)
   736   | collect_vars (cplexSum ts) = mergemap collect_vars ts
   737   | collect_vars _ = emptyset
   738 
   739 (* Eliminates all nonfree bounds from the linear program and produces an
   740    equivalent program with only free bounds
   741    IF for the input program P holds: is_normed_cplexProg P *)
   742 fun elim_nonfree_bounds (cplexProg (name, goal, constraints, bounds)) =
   743     let
   744     fun collect_constr_vars (_, cplexConstr (_, (t1,_))) =
   745         (collect_vars t1)
   746 
   747     val cvars = merge (collect_vars (term_of_goal goal))
   748               (mergemap collect_constr_vars constraints)
   749 
   750     fun collect_lower_bounded_vars
   751         (cplexBounds (_, _, cplexVar v, _, _)) =
   752         singleton v
   753       |  collect_lower_bounded_vars
   754          (cplexBound (_, cplexLe, cplexVar v)) =
   755          singleton v
   756       |  collect_lower_bounded_vars
   757          (cplexBound (_, cplexLeq, cplexVar v)) =
   758          singleton v
   759       |  collect_lower_bounded_vars
   760          (cplexBound (cplexVar v, cplexGe,_)) =
   761          singleton v
   762       |  collect_lower_bounded_vars
   763          (cplexBound (cplexVar v, cplexGeq, _)) =
   764          singleton v
   765       | collect_lower_bounded_vars
   766         (cplexBound (cplexVar v, cplexEq, _)) =
   767         singleton v
   768       |  collect_lower_bounded_vars _ = emptyset
   769 
   770     val lvars = mergemap collect_lower_bounded_vars bounds
   771     val positive_vars = diff cvars lvars
   772     val zero = cplexNum "0"
   773 
   774     fun make_pos_constr v =
   775         (NONE, cplexConstr (cplexGeq, ((cplexVar v), zero)))
   776 
   777     fun make_free_bound v =
   778         cplexBounds (cplexNeg cplexInf, cplexLeq,
   779              cplexVar v, cplexLeq,
   780              cplexInf)
   781 
   782     val pos_constrs = rev (Symtab.fold
   783                   (fn (k, _) => cons (make_pos_constr k))
   784                   positive_vars [])
   785         val bound_constrs = map (pair NONE)
   786                 (maps bound2constr bounds)
   787     val constraints' = constraints @ pos_constrs @ bound_constrs
   788     val bounds' = rev (Symtab.fold (fn (v, _) => cons (make_free_bound v)) cvars []);
   789     in
   790     cplexProg (name, goal, constraints', bounds')
   791     end
   792 
   793 fun relax_strict_ineqs (cplexProg (name, goals, constrs, bounds)) =
   794     let
   795     fun relax cplexLe = cplexLeq
   796       | relax cplexGe = cplexGeq
   797       | relax x = x
   798 
   799     fun relax_constr (n, cplexConstr(c, (t1, t2))) =
   800         (n, cplexConstr(relax c, (t1, t2)))
   801 
   802     fun relax_bounds (cplexBounds (t1, c1, t2, c2, t3)) =
   803         cplexBounds (t1, relax c1, t2, relax c2, t3)
   804       | relax_bounds (cplexBound (t1, c, t2)) =
   805         cplexBound (t1, relax c, t2)
   806     in
   807     cplexProg (name,
   808            goals,
   809            map relax_constr constrs,
   810            map relax_bounds bounds)
   811     end
   812 
   813 datatype cplexResult = Unbounded
   814              | Infeasible
   815              | Undefined
   816              | Optimal of string * ((string * string) list)
   817 
   818 fun is_separator x = forall (fn c => c = #"-") (String.explode x)
   819 
   820 fun is_sign x = (x = "+" orelse x = "-")
   821 
   822 fun is_colon x = (x = ":")
   823 
   824 fun is_resultsymbol a =
   825     let
   826     val symbol_char = String.explode "!\"#$%&()/,.;?@_`'{}|~-"
   827     fun is_symbol_char c = Char.isAlphaNum c orelse
   828                    exists (fn d => d=c) symbol_char
   829     fun is_symbol_start c = is_symbol_char c andalso
   830                 not (Char.isDigit c) andalso
   831                 not (c= #".") andalso
   832                 not (c= #"-")
   833     val b = String.explode a
   834     in
   835     b <> [] andalso is_symbol_start (hd b) andalso
   836     forall is_symbol_char b
   837     end
   838 
   839 val TOKEN_SIGN = 100
   840 val TOKEN_COLON = 101
   841 val TOKEN_SEPARATOR = 102
   842 
   843 fun load_glpkResult name =
   844     let
   845     val flist = [(is_NL, TOKEN_NL),
   846              (is_blank, TOKEN_BLANK),
   847              (is_num, TOKEN_NUM),
   848              (is_sign, TOKEN_SIGN),
   849                      (is_colon, TOKEN_COLON),
   850              (is_cmp, TOKEN_CMP),
   851              (is_resultsymbol, TOKEN_SYMBOL),
   852              (is_separator, TOKEN_SEPARATOR)]
   853 
   854     val tokenize = tokenize_general flist
   855 
   856     val f = TextIO.openIn name
   857 
   858     val rest = Unsynchronized.ref []
   859 
   860     fun readToken_helper () =
   861         if length (!rest) > 0 then
   862         let val u = hd (!rest) in
   863             (
   864              rest := tl (!rest);
   865              SOME u
   866             )
   867         end
   868         else
   869         (case TextIO.inputLine f of
   870           NONE => NONE
   871         | SOME s => (rest := tokenize s; readToken_helper()))
   872 
   873     fun is_tt tok ty = (tok <> NONE andalso (fst (the tok)) = ty)
   874 
   875     fun pushToken a = if a = NONE then () else (rest := ((the a)::(!rest)))
   876 
   877     fun readToken () =
   878         let val t = readToken_helper () in
   879         if is_tt t TOKEN_BLANK then
   880             readToken ()
   881         else if is_tt t TOKEN_NL then
   882             let val t2 = readToken_helper () in
   883             if is_tt t2 TOKEN_SIGN then
   884                 (pushToken (SOME (TOKEN_SEPARATOR, "-")); t)
   885             else
   886                 (pushToken t2; t)
   887             end
   888         else if is_tt t TOKEN_SIGN then
   889             let val t2 = readToken_helper () in
   890             if is_tt t2 TOKEN_NUM then
   891                 (SOME (TOKEN_NUM, (snd (the t))^(snd (the t2))))
   892             else
   893                 (pushToken t2; t)
   894             end
   895         else
   896             t
   897         end
   898 
   899         fun readRestOfLine P =
   900         let
   901         val t = readToken ()
   902         in
   903         if is_tt t TOKEN_NL orelse t = NONE
   904         then P
   905         else readRestOfLine P
   906         end
   907 
   908     fun readHeader () =
   909         let
   910         fun readStatus () = readRestOfLine ("STATUS", snd (the (readToken ())))
   911         fun readObjective () = readRestOfLine ("OBJECTIVE", snd (the (readToken (); readToken (); readToken ())))
   912         val t1 = readToken ()
   913         val t2 = readToken ()
   914         in
   915         if is_tt t1 TOKEN_SYMBOL andalso is_tt t2 TOKEN_COLON
   916         then
   917             case to_upper (snd (the t1)) of
   918             "STATUS" => (readStatus ())::(readHeader ())
   919               | "OBJECTIVE" => (readObjective())::(readHeader ())
   920               | _ => (readRestOfLine (); readHeader ())
   921         else
   922             (pushToken t2; pushToken t1; [])
   923         end
   924 
   925     fun skip_until_sep () =
   926         let val x = readToken () in
   927         if is_tt x TOKEN_SEPARATOR then
   928             readRestOfLine ()
   929         else
   930             skip_until_sep ()
   931         end
   932 
   933     fun load_value () =
   934         let
   935         val t1 = readToken ()
   936         val t2 = readToken ()
   937         in
   938         if is_tt t1 TOKEN_NUM andalso is_tt t2 TOKEN_SYMBOL then
   939             let
   940             val t = readToken ()
   941             val state = if is_tt t TOKEN_NL then readToken () else t
   942             val _ = if is_tt state TOKEN_SYMBOL then () else raise (Load_cplexResult "state expected")
   943             val k = readToken ()
   944             in
   945             if is_tt k TOKEN_NUM then
   946                 readRestOfLine (SOME (snd (the t2), snd (the k)))
   947             else
   948                 raise (Load_cplexResult "number expected")
   949             end
   950         else
   951             (pushToken t2; pushToken t1; NONE)
   952         end
   953 
   954     fun load_values () =
   955         let val v = load_value () in
   956         if v = NONE then [] else (the v)::(load_values ())
   957         end
   958 
   959     val header = readHeader ()
   960 
   961     val result =
   962         case AList.lookup (op =) header "STATUS" of
   963         SOME "INFEASIBLE" => Infeasible
   964           | SOME "UNBOUNDED" => Unbounded
   965           | SOME "OPTIMAL" => Optimal (the (AList.lookup (op =) header "OBJECTIVE"),
   966                        (skip_until_sep ();
   967                         skip_until_sep ();
   968                         load_values ()))
   969           | _ => Undefined
   970 
   971     val _ = TextIO.closeIn f
   972     in
   973     result
   974     end
   975     handle (Tokenize s) => raise (Load_cplexResult ("Tokenize: "^s))
   976      | Option.Option => raise (Load_cplexResult "Option")
   977 
   978 fun load_cplexResult name =
   979     let
   980     val flist = [(is_NL, TOKEN_NL),
   981              (is_blank, TOKEN_BLANK),
   982              (is_num, TOKEN_NUM),
   983              (is_sign, TOKEN_SIGN),
   984                      (is_colon, TOKEN_COLON),
   985              (is_cmp, TOKEN_CMP),
   986              (is_resultsymbol, TOKEN_SYMBOL)]
   987 
   988     val tokenize = tokenize_general flist
   989 
   990     val f = TextIO.openIn name
   991 
   992     val rest = Unsynchronized.ref []
   993 
   994     fun readToken_helper () =
   995         if length (!rest) > 0 then
   996         let val u = hd (!rest) in
   997             (
   998              rest := tl (!rest);
   999              SOME u
  1000             )
  1001         end
  1002         else
  1003         (case TextIO.inputLine f of
  1004           NONE => NONE
  1005         | SOME s => (rest := tokenize s; readToken_helper()))
  1006 
  1007     fun is_tt tok ty = (tok <> NONE andalso (fst (the tok)) = ty)
  1008 
  1009     fun pushToken a = if a = NONE then () else (rest := ((the a)::(!rest)))
  1010 
  1011     fun readToken () =
  1012         let val t = readToken_helper () in
  1013         if is_tt t TOKEN_BLANK then
  1014             readToken ()
  1015         else if is_tt t TOKEN_SIGN then
  1016             let val t2 = readToken_helper () in
  1017             if is_tt t2 TOKEN_NUM then
  1018                 (SOME (TOKEN_NUM, (snd (the t))^(snd (the t2))))
  1019             else
  1020                 (pushToken t2; t)
  1021             end
  1022         else
  1023             t
  1024         end
  1025 
  1026         fun readRestOfLine P =
  1027         let
  1028         val t = readToken ()
  1029         in
  1030         if is_tt t TOKEN_NL orelse t = NONE
  1031         then P
  1032         else readRestOfLine P
  1033         end
  1034 
  1035     fun readHeader () =
  1036         let
  1037         fun readStatus () = readRestOfLine ("STATUS", snd (the (readToken ())))
  1038         fun readObjective () =
  1039             let
  1040             val t = readToken ()
  1041             in
  1042             if is_tt t TOKEN_SYMBOL andalso to_upper (snd (the t)) = "VALUE" then
  1043                 readRestOfLine ("OBJECTIVE", snd (the (readToken())))
  1044             else
  1045                 readRestOfLine ("OBJECTIVE_NAME", snd (the t))
  1046             end
  1047 
  1048         val t = readToken ()
  1049         in
  1050         if is_tt t TOKEN_SYMBOL then
  1051             case to_upper (snd (the t)) of
  1052             "STATUS" => (readStatus ())::(readHeader ())
  1053               | "OBJECTIVE" => (readObjective ())::(readHeader ())
  1054               | "SECTION" => (pushToken t; [])
  1055               | _ => (readRestOfLine (); readHeader ())
  1056         else
  1057             (readRestOfLine (); readHeader ())
  1058         end
  1059 
  1060     fun skip_nls () =
  1061         let val x = readToken () in
  1062         if is_tt x TOKEN_NL then
  1063             skip_nls ()
  1064         else
  1065             (pushToken x; ())
  1066         end
  1067 
  1068     fun skip_paragraph () =
  1069         if is_tt (readToken ()) TOKEN_NL then
  1070         (if is_tt (readToken ()) TOKEN_NL then
  1071              skip_nls ()
  1072          else
  1073              skip_paragraph ())
  1074         else
  1075         skip_paragraph ()
  1076 
  1077     fun load_value () =
  1078         let
  1079         val t1 = readToken ()
  1080         val t1 = if is_tt t1 TOKEN_SYMBOL andalso snd (the t1) = "A" then readToken () else t1
  1081         in
  1082         if is_tt t1 TOKEN_NUM then
  1083             let
  1084             val name = readToken ()
  1085             val status = readToken ()
  1086             val value = readToken ()
  1087             in
  1088             if is_tt name TOKEN_SYMBOL andalso
  1089                is_tt status TOKEN_SYMBOL andalso
  1090                is_tt value TOKEN_NUM
  1091             then
  1092                 readRestOfLine (SOME (snd (the name), snd (the value)))
  1093             else
  1094                 raise (Load_cplexResult "column line expected")
  1095             end
  1096         else
  1097             (pushToken t1; NONE)
  1098         end
  1099 
  1100     fun load_values () =
  1101         let val v = load_value () in
  1102         if v = NONE then [] else (the v)::(load_values ())
  1103         end
  1104 
  1105     val header = readHeader ()
  1106 
  1107     val result =
  1108         case AList.lookup (op =) header "STATUS" of
  1109         SOME "INFEASIBLE" => Infeasible
  1110           | SOME "NONOPTIMAL" => Unbounded
  1111           | SOME "OPTIMAL" => Optimal (the (AList.lookup (op =) header "OBJECTIVE"),
  1112                        (skip_paragraph ();
  1113                         skip_paragraph ();
  1114                         skip_paragraph ();
  1115                         skip_paragraph ();
  1116                         skip_paragraph ();
  1117                         load_values ()))
  1118           | _ => Undefined
  1119 
  1120     val _ = TextIO.closeIn f
  1121     in
  1122     result
  1123     end
  1124     handle (Tokenize s) => raise (Load_cplexResult ("Tokenize: "^s))
  1125      | Option.Option => raise (Load_cplexResult "Option")
  1126 
  1127 exception Execute of string;
  1128 
  1129 fun tmp_file s = Path.implode (Path.expand (File.tmp_path (Path.basic s)));
  1130 fun wrap s = "\""^s^"\"";
  1131 
  1132 fun solve_glpk prog =
  1133     let
  1134     val name = string_of_int (Time.toMicroseconds (Time.now ()))
  1135     val lpname = tmp_file (name^".lp")
  1136     val resultname = tmp_file (name^".txt")
  1137     val _ = save_cplexFile lpname prog
  1138     val cplex_path = getenv "GLPK_PATH"
  1139     val cplex = if cplex_path = "" then "glpsol" else cplex_path
  1140     val command = (wrap cplex)^" --lpt "^(wrap lpname)^" --output "^(wrap resultname)
  1141     val answer = #1 (Isabelle_System.bash_output command)
  1142     in
  1143     let
  1144         val result = load_glpkResult resultname
  1145         val _ = OS.FileSys.remove lpname
  1146         val _ = OS.FileSys.remove resultname
  1147     in
  1148         result
  1149     end
  1150     handle (Load_cplexResult s) => raise (Execute ("Load_cplexResult: "^s^"\nExecute: "^answer))
  1151          | exn => if Exn.is_interrupt exn then reraise exn else raise (Execute answer)
  1152     end
  1153 
  1154 fun solve_cplex prog =
  1155     let
  1156     fun write_script s lp r =
  1157         let
  1158         val f = TextIO.openOut s
  1159         val _ = TextIO.output (f, "read\n"^lp^"\noptimize\nwrite\n"^r^"\nquit")
  1160         val _ = TextIO.closeOut f
  1161         in
  1162         ()
  1163         end
  1164 
  1165     val name = string_of_int (Time.toMicroseconds (Time.now ()))
  1166     val lpname = tmp_file (name^".lp")
  1167     val resultname = tmp_file (name^".txt")
  1168     val scriptname = tmp_file (name^".script")
  1169     val _ = save_cplexFile lpname prog
  1170     val _ = write_script scriptname lpname resultname
  1171     in
  1172     let
  1173         val result = load_cplexResult resultname
  1174         val _ = OS.FileSys.remove lpname
  1175         val _ = OS.FileSys.remove resultname
  1176         val _ = OS.FileSys.remove scriptname
  1177     in
  1178         result
  1179     end
  1180     end
  1181 
  1182 fun solve prog =
  1183     case get_solver () of
  1184       SOLVER_DEFAULT =>
  1185         (case getenv "LP_SOLVER" of
  1186        "CPLEX" => solve_cplex prog
  1187          | "GLPK" => solve_glpk prog
  1188          | _ => raise (Execute ("LP_SOLVER must be set to CPLEX or to GLPK")))
  1189     | SOLVER_CPLEX => solve_cplex prog
  1190     | SOLVER_GLPK => solve_glpk prog
  1191 
  1192 end;