src/HOL/Matrix/cplex/Cplex_tools.ML
author haftmann
Tue Sep 20 16:17:34 2005 +0200 (2005-09-20)
changeset 17521 0f1c48de39f5
parent 17412 e26cb20ef0cc
child 21056 2cfe839e8d58
permissions -rw-r--r--
introduced AList module in favor of assoc etc.
     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)
    38 
    39     datatype cplexSolver = SOLVER_DEFAULT | SOLVER_CPLEX | SOLVER_GLPK
    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 
    56     val get_solver : unit -> cplexSolver
    57     val set_solver : cplexSolver -> unit
    58     val solve : cplexProg -> cplexResult
    59 end;
    60 
    61 structure Cplex  : CPLEX =
    62 struct
    63 
    64 datatype cplexSolver = SOLVER_DEFAULT | SOLVER_CPLEX | SOLVER_GLPK
    65 
    66 val cplexsolver = ref SOLVER_DEFAULT;
    67 fun get_solver () = !cplexsolver;
    68 fun set_solver s = (cplexsolver := s);
    69 
    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 AList.lookup (op =) header "STATUS" of
   973 		SOME "INFEASIBLE" => Infeasible
   974 	      | SOME "UNBOUNDED" => Unbounded
   975 	      | SOME "OPTIMAL" => Optimal (the (AList.lookup (op =) 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 AList.lookup (op =) header "STATUS" of
  1122 		SOME "INFEASIBLE" => Infeasible
  1123 	      | SOME "NONOPTIMAL" => Unbounded
  1124 	      | SOME "OPTIMAL" => Optimal (the (AList.lookup (op =) 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		
  1152 	val cplex_path = getenv "GLPK_PATH"
  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		
  1184 	val cplex_path = getenv "CPLEX_PATH"
  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 = 
  1201     case get_solver () of
  1202       SOLVER_DEFAULT => 
  1203         (case getenv "LP_SOLVER" of
  1204 	   "CPLEX" => solve_cplex prog
  1205          | "GLPK" => solve_glpk prog
  1206          | _ => raise (Execute ("LP_SOLVER must be set to CPLEX or to GLPK")))
  1207     | SOLVER_CPLEX => solve_cplex prog
  1208     | SOLVER_GLPK => solve_glpk prog
  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;*)