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.
obua@16784
     1
(*  Title:      HOL/Matrix/cplex/Cplex_tools.ML
obua@16784
     2
    ID:         $Id$
obua@16784
     3
    Author:     Steven Obua
obua@16784
     4
*)
obua@16784
     5
obua@16784
     6
signature CPLEX =
obua@16784
     7
sig
obua@16784
     8
    
obua@16784
     9
    datatype cplexTerm = cplexVar of string | cplexNum of string | cplexInf 
obua@16784
    10
                       | cplexNeg of cplexTerm 
obua@16784
    11
                       | cplexProd of cplexTerm * cplexTerm 
obua@16784
    12
                       | cplexSum of (cplexTerm list) 
obua@16784
    13
    
obua@16784
    14
    datatype cplexComp = cplexLe | cplexLeq | cplexEq | cplexGe | cplexGeq 
obua@16784
    15
								  
obua@16784
    16
    datatype cplexGoal = cplexMinimize of cplexTerm 
obua@16784
    17
		       | cplexMaximize of cplexTerm
obua@16784
    18
					  
obua@16784
    19
    datatype cplexConstr = cplexConstr of cplexComp * 
obua@16784
    20
					  (cplexTerm * cplexTerm)
obua@16784
    21
					  
obua@16784
    22
    datatype cplexBounds = cplexBounds of cplexTerm * cplexComp * cplexTerm 
obua@16784
    23
					  * cplexComp * cplexTerm
obua@16784
    24
			 | cplexBound of cplexTerm * cplexComp * cplexTerm
obua@16784
    25
					 
obua@16784
    26
    datatype cplexProg = cplexProg of string 
obua@16784
    27
				      * cplexGoal 
obua@16784
    28
				      * ((string option * cplexConstr) 
obua@16784
    29
					     list) 
obua@16784
    30
				      * cplexBounds list
obua@16784
    31
				      
obua@16784
    32
    datatype cplexResult = Unbounded 
obua@16784
    33
			 | Infeasible 
obua@16784
    34
			 | Undefined
obua@16784
    35
			 | Optimal of string * 
obua@16784
    36
				      (((* name *) string * 
obua@16784
    37
					(* value *) string) list)
obua@16966
    38
obua@16966
    39
    datatype cplexSolver = SOLVER_DEFAULT | SOLVER_CPLEX | SOLVER_GLPK
obua@16784
    40
						     
obua@16784
    41
    exception Load_cplexFile of string
obua@16784
    42
    exception Load_cplexResult of string
obua@16784
    43
    exception Save_cplexFile of string
obua@16784
    44
    exception Execute of string
obua@16784
    45
obua@16784
    46
    val load_cplexFile : string -> cplexProg
obua@16784
    47
obua@16784
    48
    val save_cplexFile : string -> cplexProg -> unit 
obua@16784
    49
obua@16784
    50
    val elim_nonfree_bounds : cplexProg -> cplexProg
obua@16784
    51
obua@16784
    52
    val relax_strict_ineqs : cplexProg -> cplexProg
obua@16784
    53
obua@16784
    54
    val is_normed_cplexProg : cplexProg -> bool
obua@16784
    55
obua@16966
    56
    val get_solver : unit -> cplexSolver
obua@16966
    57
    val set_solver : cplexSolver -> unit
obua@16784
    58
    val solve : cplexProg -> cplexResult
obua@16784
    59
end;
obua@16784
    60
obua@16784
    61
structure Cplex  : CPLEX =
obua@16784
    62
struct
obua@16784
    63
obua@16966
    64
datatype cplexSolver = SOLVER_DEFAULT | SOLVER_CPLEX | SOLVER_GLPK
obua@16966
    65
obua@16966
    66
val cplexsolver = ref SOLVER_DEFAULT;
obua@16966
    67
fun get_solver () = !cplexsolver;
obua@16966
    68
fun set_solver s = (cplexsolver := s);
obua@16966
    69
obua@16784
    70
exception Load_cplexFile of string;
obua@16784
    71
exception Load_cplexResult of string;
obua@16784
    72
exception Save_cplexFile of string;
obua@16784
    73
	  
obua@16784
    74
datatype cplexTerm = cplexVar of string 
obua@16784
    75
		   | cplexNum of string 
obua@16784
    76
		   | cplexInf 
obua@16784
    77
                   | cplexNeg of cplexTerm 
obua@16784
    78
                   | cplexProd of cplexTerm * cplexTerm 
obua@16784
    79
                   | cplexSum of (cplexTerm list) 
obua@16784
    80
datatype cplexComp = cplexLe | cplexLeq | cplexEq | cplexGe | cplexGeq 
obua@16784
    81
datatype cplexGoal = cplexMinimize of cplexTerm | cplexMaximize of cplexTerm
obua@16784
    82
datatype cplexConstr = cplexConstr of cplexComp * (cplexTerm * cplexTerm)
obua@16784
    83
datatype cplexBounds = cplexBounds of cplexTerm * cplexComp * cplexTerm 
obua@16784
    84
				      * cplexComp * cplexTerm
obua@16784
    85
                     | cplexBound of cplexTerm * cplexComp * cplexTerm 
obua@16784
    86
datatype cplexProg = cplexProg of string 
obua@16784
    87
				  * cplexGoal 
obua@16784
    88
				  * ((string option * cplexConstr) list) 
obua@16784
    89
				  * cplexBounds list
obua@16784
    90
				  
obua@16784
    91
fun rev_cmp cplexLe = cplexGe
obua@16784
    92
  | rev_cmp cplexLeq = cplexGeq
obua@16784
    93
  | rev_cmp cplexGe = cplexLe
obua@16784
    94
  | rev_cmp cplexGeq = cplexLeq
obua@16784
    95
  | rev_cmp cplexEq = cplexEq
obua@16784
    96
obua@16784
    97
fun the NONE = raise (Load_cplexFile "SOME expected")
obua@16784
    98
  | the (SOME x) = x; 
obua@16784
    99
    
obua@16784
   100
fun modulo_signed is_something (cplexNeg u) = is_something u
obua@16784
   101
  | modulo_signed is_something u = is_something u
obua@16784
   102
obua@16784
   103
fun is_Num (cplexNum _) = true
obua@16784
   104
  | is_Num _ = false
obua@16784
   105
obua@16784
   106
fun is_Inf cplexInf = true
obua@16784
   107
  | is_Inf _ = false
obua@16784
   108
obua@16784
   109
fun is_Var (cplexVar _) = true
obua@16784
   110
  | is_Var _ = false
obua@16784
   111
obua@16784
   112
fun is_Neg (cplexNeg x ) = true
obua@16784
   113
  | is_Neg _ = false
obua@16784
   114
obua@16784
   115
fun is_normed_Prod (cplexProd (t1, t2)) = 
obua@16784
   116
    (is_Num t1) andalso (is_Var t2)
obua@16784
   117
  | is_normed_Prod x = is_Var x
obua@16784
   118
obua@16784
   119
fun is_normed_Sum (cplexSum ts) = 
obua@16784
   120
    (ts <> []) andalso forall (modulo_signed is_normed_Prod) ts
obua@16784
   121
  | is_normed_Sum x = modulo_signed is_normed_Prod x
obua@16784
   122
obua@16784
   123
fun is_normed_Constr (cplexConstr (c, (t1, t2))) = 
obua@16784
   124
    (is_normed_Sum t1) andalso (modulo_signed is_Num t2)
obua@16784
   125
obua@16784
   126
fun is_Num_or_Inf x = is_Inf x orelse is_Num x
obua@16784
   127
obua@16784
   128
fun is_normed_Bounds (cplexBounds (t1, c1, t2, c2, t3)) =
obua@16784
   129
    (c1 = cplexLe orelse c1 = cplexLeq) andalso 
obua@16784
   130
    (c2 = cplexLe orelse c2 = cplexLeq) andalso
obua@16784
   131
    is_Var t2 andalso
obua@16784
   132
    modulo_signed is_Num_or_Inf t1 andalso
obua@16784
   133
    modulo_signed is_Num_or_Inf t3
obua@16784
   134
  | is_normed_Bounds (cplexBound (t1, c, t2)) =
obua@16784
   135
    (is_Var t1 andalso (modulo_signed is_Num_or_Inf t2)) 
obua@16784
   136
    orelse
obua@16784
   137
    (c <> cplexEq andalso 
obua@16784
   138
     is_Var t2 andalso (modulo_signed is_Num_or_Inf t1))
obua@16784
   139
	             		
obua@16784
   140
fun term_of_goal (cplexMinimize x) = x
obua@16784
   141
  | term_of_goal (cplexMaximize x) = x
obua@16784
   142
obua@16784
   143
fun is_normed_cplexProg (cplexProg (name, goal, constraints, bounds)) = 
obua@16784
   144
    is_normed_Sum (term_of_goal goal) andalso
obua@16784
   145
    forall (fn (_,x) => is_normed_Constr x) constraints andalso
obua@16784
   146
    forall is_normed_Bounds bounds
obua@16784
   147
obua@16784
   148
fun is_NL s = s = "\n"
obua@16784
   149
obua@16784
   150
fun is_blank s = forall (fn c => c <> #"\n" andalso Char.isSpace c) (String.explode s)
obua@16784
   151
		 
obua@16784
   152
fun is_num a = 
obua@16784
   153
    let 
obua@16784
   154
	val b = String.explode a 
obua@16784
   155
	fun num4 cs = forall Char.isDigit cs		      
obua@16784
   156
	fun num3 [] = true
obua@16784
   157
	  | num3 (ds as (c::cs)) = 
obua@16784
   158
	    if c = #"+" orelse c = #"-" then
obua@16784
   159
		num4 cs
obua@16784
   160
	    else 
obua@16784
   161
		num4 ds		    
obua@16784
   162
	fun num2 [] = true
obua@16784
   163
	  | num2 (c::cs) =
obua@16784
   164
	    if c = #"e" orelse c = #"E" then num3 cs
obua@16784
   165
	    else (Char.isDigit c) andalso num2 cs			 
obua@16784
   166
	fun num1 [] = true
obua@16784
   167
	  | num1 (c::cs) = 
obua@16784
   168
	    if c = #"." then num2 cs 
obua@16784
   169
	    else if c = #"e" orelse c = #"E" then num3 cs 
obua@16784
   170
	    else (Char.isDigit c) andalso num1 cs
obua@16784
   171
	fun num [] = true
obua@16784
   172
	  | num (c::cs) = 
obua@16784
   173
	    if c = #"." then num2 cs 
obua@16784
   174
	    else (Char.isDigit c) andalso num1 cs
obua@16784
   175
    in
obua@16784
   176
	num b
obua@16784
   177
    end  
obua@16784
   178
obua@16784
   179
fun is_delimiter s = s = "+" orelse s = "-" orelse s = ":"
obua@16784
   180
		    
obua@16784
   181
fun is_cmp s = s = "<" orelse s = ">" orelse s = "<=" 
obua@16784
   182
		     orelse s = ">=" orelse s = "="
obua@16784
   183
obua@16784
   184
fun is_symbol a = 
obua@16784
   185
    let
obua@16784
   186
	val symbol_char = String.explode "!\"#$%&()/,.;?@_`'{}|~"
obua@16784
   187
	fun is_symbol_char c = Char.isAlphaNum c orelse 
obua@16784
   188
			       exists (fn d => d=c) symbol_char
obua@16784
   189
	fun is_symbol_start c = is_symbol_char c andalso 
obua@16784
   190
				not (Char.isDigit c) andalso 
obua@16784
   191
				not (c= #".")
obua@16784
   192
	val b = String.explode a
obua@16784
   193
    in
obua@16784
   194
	b <> [] andalso is_symbol_start (hd b) andalso 
obua@16784
   195
	forall is_symbol_char b
obua@16784
   196
    end
obua@16784
   197
obua@16784
   198
fun to_upper s = String.implode (map Char.toUpper (String.explode s))
obua@16784
   199
obua@16784
   200
fun keyword x = 
obua@16784
   201
    let 	
obua@16784
   202
	val a = to_upper x 
obua@16784
   203
    in
obua@16784
   204
	if a = "BOUNDS" orelse a = "BOUND" then
obua@16784
   205
	    SOME "BOUNDS"
obua@16784
   206
	else if a = "MINIMIZE" orelse a = "MINIMUM" orelse a = "MIN" then
obua@16784
   207
	    SOME "MINIMIZE"
obua@16784
   208
	else if a = "MAXIMIZE" orelse a = "MAXIMUM" orelse a = "MAX" then
obua@16784
   209
	    SOME "MAXIMIZE"
obua@16784
   210
	else if a = "ST" orelse a = "S.T." orelse a = "ST." then
obua@16784
   211
	    SOME "ST"
obua@16784
   212
	else if a = "FREE" orelse a = "END" then
obua@16784
   213
	    SOME a
obua@16784
   214
	else if a = "GENERAL" orelse a = "GENERALS" orelse a = "GEN" then
obua@16784
   215
	    SOME "GENERAL"
obua@16784
   216
	else if a = "INTEGER" orelse a = "INTEGERS" orelse a = "INT" then
obua@16784
   217
	    SOME "INTEGER"
obua@16784
   218
	else if a = "BINARY" orelse a = "BINARIES" orelse a = "BIN" then
obua@16784
   219
	    SOME "BINARY"
obua@16784
   220
	else if a = "INF" orelse a = "INFINITY" then
obua@16784
   221
	    SOME "INF"
obua@16784
   222
	else								   
obua@16784
   223
	    NONE
obua@16784
   224
    end
obua@16784
   225
	        
obua@16784
   226
val TOKEN_ERROR = ~1
obua@16784
   227
val TOKEN_BLANK = 0
obua@16784
   228
val TOKEN_NUM = 1
obua@16784
   229
val TOKEN_DELIMITER = 2
obua@16784
   230
val TOKEN_SYMBOL = 3
obua@16784
   231
val TOKEN_LABEL = 4
obua@16784
   232
val TOKEN_CMP = 5
obua@16784
   233
val TOKEN_KEYWORD = 6
obua@16784
   234
val TOKEN_NL = 7
obua@16784
   235
		      
obua@16784
   236
(* tokenize takes a list of chars as argument and returns a list of
obua@16784
   237
   int * string pairs, each string representing a "cplex token", 
obua@16784
   238
   and each int being one of TOKEN_NUM, TOKEN_DELIMITER, TOKEN_CMP
obua@16784
   239
   or TOKEN_SYMBOL *)
obua@16784
   240
fun tokenize s = 
obua@16784
   241
    let
obua@16784
   242
	val flist = [(is_NL, TOKEN_NL), 
obua@16784
   243
		     (is_blank, TOKEN_BLANK), 
obua@16784
   244
		     (is_num, TOKEN_NUM),  
obua@16784
   245
                     (is_delimiter, TOKEN_DELIMITER), 
obua@16784
   246
		     (is_cmp, TOKEN_CMP), 
obua@16784
   247
		     (is_symbol, TOKEN_SYMBOL)]  
obua@16784
   248
	fun match_helper [] s = (fn x => false, TOKEN_ERROR)
obua@16784
   249
	  | match_helper (f::fs) s = 
obua@16784
   250
	    if ((fst f) s) then f else match_helper fs s   
obua@16784
   251
	fun match s = match_helper flist s
obua@16784
   252
	fun tok s = 
obua@16784
   253
	    if s = "" then [] else       
obua@16784
   254
	    let 
obua@16784
   255
		val h = String.substring (s,0,1) 
obua@16784
   256
		val (f, j) = match h
obua@16784
   257
		fun len i = 
obua@16784
   258
		    if size s = i then i 
obua@16784
   259
		    else if f (String.substring (s,0,i+1)) then 
obua@16784
   260
			len (i+1) 
obua@16784
   261
		    else i 
obua@16784
   262
	    in
obua@16784
   263
		if j < 0 then 
obua@16784
   264
		    (if h = "\\" then [] 
obua@16784
   265
		     else raise (Load_cplexFile ("token expected, found: "
obua@16784
   266
						 ^s)))
obua@16784
   267
		else 
obua@16784
   268
		    let 
obua@16784
   269
			val l = len 1 
obua@16784
   270
			val u = String.substring (s,0,l)
obua@16784
   271
			val v = String.extract (s,l,NONE)
obua@16784
   272
		    in
obua@16784
   273
			if j = 0 then tok v else (j, u) :: tok v
obua@16784
   274
		    end
obua@16784
   275
	    end                
obua@16784
   276
    in
obua@16784
   277
	tok s     
obua@16784
   278
    end
obua@16784
   279
obua@16784
   280
exception Tokenize of string;
obua@16784
   281
obua@16784
   282
fun tokenize_general flist s = 
obua@16784
   283
    let
obua@16784
   284
	fun match_helper [] s = raise (Tokenize s)
obua@16784
   285
	  | match_helper (f::fs) s = 
obua@16784
   286
	    if ((fst f) s) then f else match_helper fs s   
obua@16784
   287
	fun match s = match_helper flist s
obua@16784
   288
	fun tok s = 
obua@16784
   289
	    if s = "" then [] else       
obua@16784
   290
	    let 
obua@16784
   291
		val h = String.substring (s,0,1) 
obua@16784
   292
		val (f, j) = match h
obua@16784
   293
		fun len i = 
obua@16784
   294
		    if size s = i then i 
obua@16784
   295
		    else if f (String.substring (s,0,i+1)) then 
obua@16784
   296
			len (i+1) 
obua@16784
   297
		    else i 
obua@16784
   298
		val l = len 1
obua@16784
   299
	    in
obua@16784
   300
		(j, String.substring (s,0,l)) :: tok (String.extract (s,l,NONE))
obua@16784
   301
	    end
obua@16784
   302
    in
obua@16784
   303
	tok s     
obua@16784
   304
    end
obua@16784
   305
obua@16784
   306
fun load_cplexFile name = 
obua@16784
   307
    let 
obua@16784
   308
	val f = TextIO.openIn name  
obua@16784
   309
        val ignore_NL = ref true  
obua@16784
   310
	val rest = ref []
obua@16784
   311
obua@16784
   312
	fun is_symbol s c = (fst c) = TOKEN_SYMBOL andalso (to_upper (snd c)) = s 
obua@16784
   313
		   
obua@16784
   314
	fun readToken_helper () =
obua@16784
   315
	    if length (!rest) > 0 then  
obua@16784
   316
		let val u = hd (!rest) in 
obua@16784
   317
		    (
obua@16784
   318
		     rest := tl (!rest); 
obua@16784
   319
		     SOME u
obua@16784
   320
		    ) 
obua@16784
   321
		end
obua@16784
   322
	    else 
obua@16784
   323
		let val s = TextIO.inputLine f in
obua@16784
   324
		    if s = "" then NONE else
obua@16784
   325
		    let val t = tokenize s in
obua@16784
   326
			if (length t >= 2 andalso 
obua@16784
   327
			    snd(hd (tl t)) = ":") 
obua@16784
   328
			then 
obua@16784
   329
			    rest := (TOKEN_LABEL, snd (hd t)) :: (tl (tl t))
obua@16784
   330
			else if (length t >= 2) andalso is_symbol "SUBJECT" (hd (t)) 
obua@16784
   331
				andalso is_symbol "TO" (hd (tl t)) 
obua@16784
   332
			then
obua@16784
   333
			    rest := (TOKEN_SYMBOL, "ST") :: (tl (tl t))
obua@16784
   334
			else
obua@16784
   335
			    rest := t;
obua@16784
   336
			readToken_helper ()  
obua@16784
   337
		    end
obua@16784
   338
		end           
obua@16784
   339
	
obua@16784
   340
	fun readToken_helper2 () = 
obua@16784
   341
		let val c = readToken_helper () in
obua@16784
   342
		    if c = NONE then NONE
obua@16784
   343
                    else if !ignore_NL andalso fst (the c) = TOKEN_NL then
obua@16784
   344
			readToken_helper2 ()
obua@16784
   345
		    else if fst (the c) = TOKEN_SYMBOL 
obua@16784
   346
			    andalso keyword (snd (the c)) <> NONE
obua@16784
   347
		    then SOME (TOKEN_KEYWORD, the (keyword (snd (the c))))
obua@16784
   348
		    else c
obua@16784
   349
		end
obua@16784
   350
		
obua@16784
   351
	fun readToken () = readToken_helper2 ()
obua@16784
   352
	    			   
obua@16784
   353
	fun pushToken a = rest := (a::(!rest))
obua@16784
   354
	    
obua@16784
   355
	fun is_value token = 
obua@16784
   356
	    fst token = TOKEN_NUM orelse (fst token = TOKEN_KEYWORD 
obua@16784
   357
					  andalso snd token = "INF")	
obua@16784
   358
obua@16784
   359
        fun get_value token = 
obua@16784
   360
	    if fst token = TOKEN_NUM then
obua@16784
   361
		cplexNum (snd token)
obua@16784
   362
	    else if fst token = TOKEN_KEYWORD andalso snd token = "INF" 
obua@16784
   363
	    then
obua@16784
   364
		cplexInf
obua@16784
   365
	    else
obua@16784
   366
		raise (Load_cplexFile "num expected")
obua@16784
   367
					    
obua@16784
   368
	fun readTerm_Product only_num = 
obua@16784
   369
	    let val c = readToken () in
obua@16784
   370
		if c = NONE then NONE
obua@16784
   371
		else if fst (the c) = TOKEN_SYMBOL 
obua@16784
   372
		then (
obua@16784
   373
		    if only_num then (pushToken (the c); NONE) 
obua@16784
   374
		    else SOME (cplexVar (snd (the c)))
obua@16784
   375
		    ) 
obua@16784
   376
		else if only_num andalso is_value (the c) then
obua@16784
   377
		    SOME (get_value (the c))
obua@16784
   378
		else if is_value (the c) then  
obua@16784
   379
		    let val t1 = get_value (the c) 
obua@16784
   380
			val d = readToken () 
obua@16784
   381
		    in
obua@16784
   382
			if d = NONE then SOME t1 
obua@16784
   383
			else if fst (the d) = TOKEN_SYMBOL then 
obua@16784
   384
			    SOME (cplexProd (t1, cplexVar (snd (the d))))
obua@16784
   385
			else
obua@16784
   386
			    (pushToken (the d); SOME t1)
obua@16784
   387
		    end
obua@16784
   388
		else (pushToken (the c); NONE)
obua@16784
   389
	    end
obua@16784
   390
	    
obua@16784
   391
	fun readTerm_Signed only_signed only_num = 
obua@16784
   392
	    let
obua@16784
   393
		val c = readToken ()
obua@16784
   394
	    in
obua@16784
   395
		if c = NONE then NONE 
obua@16784
   396
		else 
obua@16784
   397
		    let val d = the c in 
obua@16784
   398
			if d = (TOKEN_DELIMITER, "+") then 
obua@16784
   399
			    readTerm_Product only_num
obua@16784
   400
			 else if d = (TOKEN_DELIMITER, "-") then 
obua@16784
   401
			     SOME (cplexNeg (the (readTerm_Product 
obua@16784
   402
						      only_num)))
obua@16784
   403
			 else (pushToken d; 
obua@16784
   404
			       if only_signed then NONE 
obua@16784
   405
			       else readTerm_Product only_num)
obua@16784
   406
		    end
obua@16784
   407
	    end
obua@16784
   408
    
obua@16784
   409
	fun readTerm_Sum first_signed = 
obua@16784
   410
	    let val c = readTerm_Signed first_signed false in
obua@16784
   411
		if c = NONE then [] else (the c)::(readTerm_Sum true)
obua@16784
   412
	    end
obua@16784
   413
	    
obua@16784
   414
	fun readTerm () = 
obua@16784
   415
	    let val c = readTerm_Sum false in
obua@16784
   416
		if c = [] then NONE 
obua@16784
   417
		else if tl c = [] then SOME (hd c)
obua@16784
   418
		else SOME (cplexSum c) 
obua@16784
   419
	    end
obua@16784
   420
	    
obua@16784
   421
	fun readLabeledTerm () = 
obua@16784
   422
	    let val c = readToken () in
obua@16784
   423
		if c = NONE then (NONE, NONE) 
obua@16784
   424
		else if fst (the c) = TOKEN_LABEL then 
obua@16784
   425
		    let val t = readTerm () in
obua@16784
   426
			if t = NONE then 
obua@16784
   427
			    raise (Load_cplexFile ("term after label "^
obua@16784
   428
						   (snd (the c))^
obua@16784
   429
						   " expected"))
obua@16784
   430
			else (SOME (snd (the c)), t)
obua@16784
   431
		    end
obua@16784
   432
		else (pushToken (the c); (NONE, readTerm ()))
obua@16784
   433
	    end
obua@16784
   434
            
obua@16784
   435
	fun readGoal () = 
obua@16784
   436
	    let 
obua@16784
   437
		val g = readToken ()
obua@16784
   438
	    in
obua@16784
   439
    		if g = SOME (TOKEN_KEYWORD, "MAXIMIZE") then 
obua@16784
   440
		    cplexMaximize (the (snd (readLabeledTerm ()))) 
obua@16784
   441
		else if g = SOME (TOKEN_KEYWORD, "MINIMIZE") then 
obua@16784
   442
		    cplexMinimize (the (snd (readLabeledTerm ())))
obua@16784
   443
		else raise (Load_cplexFile "MAXIMIZE or MINIMIZE expected")
obua@16784
   444
	    end
obua@16784
   445
	    
obua@16784
   446
	fun str2cmp b = 
obua@16784
   447
	    (case b of 
obua@16784
   448
		 "<" => cplexLe 
obua@16784
   449
	       | "<=" => cplexLeq 
obua@16784
   450
	       | ">" => cplexGe 
obua@16784
   451
	       | ">=" => cplexGeq 
obua@16784
   452
               | "=" => cplexEq
obua@16784
   453
	       | _ => raise (Load_cplexFile (b^" is no TOKEN_CMP")))
obua@16784
   454
			    
obua@16784
   455
	fun readConstraint () = 
obua@16784
   456
            let 
obua@16784
   457
		val t = readLabeledTerm () 
obua@16784
   458
		fun make_constraint b t1 t2 =
obua@16784
   459
                    cplexConstr 
obua@16784
   460
			(str2cmp b,
obua@16784
   461
			 (t1, t2))		
obua@16784
   462
	    in
obua@16784
   463
		if snd t = NONE then NONE
obua@16784
   464
		else 
obua@16784
   465
		    let val c = readToken () in
obua@16784
   466
			if c = NONE orelse fst (the c) <> TOKEN_CMP 
obua@16784
   467
			then raise (Load_cplexFile "TOKEN_CMP expected")
obua@16784
   468
			else 
obua@16784
   469
			    let val n = readTerm_Signed false true in
obua@16784
   470
				if n = NONE then 
obua@16784
   471
				    raise (Load_cplexFile "num expected")
obua@16784
   472
				else
obua@16784
   473
				    SOME (fst t,
obua@16784
   474
					  make_constraint (snd (the c)) 
obua@16784
   475
							  (the (snd t)) 
obua@16784
   476
							  (the n))
obua@16784
   477
			    end
obua@16784
   478
		    end            
obua@16784
   479
	    end
obua@16784
   480
        
obua@16784
   481
        fun readST () = 
obua@16784
   482
	    let 
obua@16784
   483
		fun readbody () = 
obua@16784
   484
		    let val t = readConstraint () in
obua@16784
   485
			if t = NONE then []
obua@16784
   486
			else if (is_normed_Constr (snd (the t))) then
obua@16784
   487
			    (the t)::(readbody ())
obua@16784
   488
			else if (fst (the t) <> NONE) then 
obua@16784
   489
			    raise (Load_cplexFile 
obua@16784
   490
				       ("constraint '"^(the (fst (the t)))^ 
obua@16784
   491
					"'is not normed"))
obua@16784
   492
			else
obua@16784
   493
			    raise (Load_cplexFile 
obua@16784
   494
				       "constraint is not normed")
obua@16784
   495
		    end
obua@16784
   496
	    in    		
obua@16784
   497
		if readToken () = SOME (TOKEN_KEYWORD, "ST") 
obua@16784
   498
		then 
obua@16784
   499
		    readbody ()
obua@16784
   500
		else 
obua@16784
   501
		    raise (Load_cplexFile "ST expected")
obua@16784
   502
	    end
obua@16784
   503
	    
obua@16784
   504
	fun readCmp () = 
obua@16784
   505
	    let val c = readToken () in
obua@16784
   506
		if c = NONE then NONE
obua@16784
   507
		else if fst (the c) = TOKEN_CMP then 
obua@16784
   508
		    SOME (str2cmp (snd (the c)))
obua@16784
   509
		else (pushToken (the c); NONE)
obua@16784
   510
	    end
obua@16784
   511
	    
obua@16784
   512
	fun skip_NL () =
obua@16784
   513
	    let val c = readToken () in
obua@16784
   514
		if c <> NONE andalso fst (the c) = TOKEN_NL then
obua@16784
   515
		    skip_NL ()
obua@16784
   516
		else
obua@16784
   517
		    (pushToken (the c); ())
obua@16784
   518
	    end
obua@16784
   519
obua@16784
   520
	fun is_var (cplexVar _) = true
obua@16784
   521
	  | is_var _ = false
obua@16784
   522
	    
obua@16784
   523
	fun make_bounds c t1 t2 = 
obua@16784
   524
	    cplexBound (t1, c, t2)
obua@16784
   525
obua@16784
   526
	fun readBound () = 	    
obua@16784
   527
	    let 		
obua@16784
   528
		val _ = skip_NL ()
obua@16784
   529
		val t1 = readTerm ()
obua@16784
   530
	    in
obua@16784
   531
		if t1 = NONE then NONE 
obua@16784
   532
		else 
obua@16784
   533
		    let 
obua@16784
   534
			val c1 = readCmp () 
obua@16784
   535
		    in
obua@16784
   536
			if c1 = NONE then
obua@16784
   537
			    let 
obua@16784
   538
				val c = readToken () 
obua@16784
   539
			    in
obua@16784
   540
				if c = SOME (TOKEN_KEYWORD, "FREE") then
obua@16784
   541
				    SOME (
obua@16784
   542
				    cplexBounds (cplexNeg cplexInf,
obua@16784
   543
						 cplexLeq,
obua@16784
   544
						 the t1,
obua@16784
   545
						 cplexLeq,
obua@16784
   546
						 cplexInf))
obua@16784
   547
				else
obua@16784
   548
				    raise (Load_cplexFile "FREE expected")
obua@16784
   549
			    end
obua@16784
   550
			else
obua@16784
   551
			    let 
obua@16784
   552
				val t2 = readTerm () 
obua@16784
   553
			    in
obua@16784
   554
				if t2 = NONE then
obua@16784
   555
				    raise (Load_cplexFile "term expected")
obua@16784
   556
				else
obua@16784
   557
				    let val c2 = readCmp () in
obua@16784
   558
					if c2 = NONE then
obua@16784
   559
					    SOME (make_bounds (the c1) 
obua@16784
   560
							      (the t1)
obua@16784
   561
							      (the t2))
obua@16784
   562
					else
obua@16784
   563
					    SOME (
obua@16784
   564
					    cplexBounds (the t1,
obua@16784
   565
							 the c1,
obua@16784
   566
							 the t2,
obua@16784
   567
							 the c2,
obua@16784
   568
							 the (readTerm())))
obua@16784
   569
				    end
obua@16784
   570
			    end
obua@16784
   571
		    end
obua@16784
   572
	    end
obua@16784
   573
	    
obua@16784
   574
	fun readBounds () =
obua@16784
   575
	    let 
obua@16784
   576
		fun makestring b = "?"
obua@16784
   577
		fun readbody () = 
obua@16784
   578
		    let 
obua@16784
   579
			val b = readBound ()
obua@16784
   580
		    in
obua@16784
   581
			if b = NONE then []
obua@16784
   582
			else if (is_normed_Bounds (the b)) then
obua@16784
   583
			    (the b)::(readbody())
obua@16784
   584
			else (
obua@16784
   585
			    raise (Load_cplexFile 
obua@16784
   586
				       ("bounds are not normed in: "^
obua@16784
   587
					(makestring (the b)))))
obua@16784
   588
		    end
obua@16784
   589
	    in
obua@16784
   590
		if readToken () = SOME (TOKEN_KEYWORD, "BOUNDS") then 
obua@16784
   591
		    readbody ()
obua@16784
   592
		else raise (Load_cplexFile "BOUNDS expected")
obua@16784
   593
	    end
obua@16784
   594
obua@16784
   595
        fun readEnd () = 
obua@16784
   596
	    if readToken () = SOME (TOKEN_KEYWORD, "END") then ()
obua@16784
   597
	    else raise (Load_cplexFile "END expected")
obua@16784
   598
		    
obua@16784
   599
	val result_Goal = readGoal ()  
obua@16784
   600
	val result_ST = readST ()  
obua@16784
   601
	val _ =	ignore_NL := false 
obua@16784
   602
        val result_Bounds = readBounds ()
obua@16784
   603
        val _ = ignore_NL := true
obua@16784
   604
        val _ = readEnd ()
obua@16784
   605
	val _ = TextIO.closeIn f
obua@16784
   606
    in
obua@16784
   607
	cplexProg (name, result_Goal, result_ST, result_Bounds)
obua@16784
   608
    end
obua@16784
   609
obua@16784
   610
fun save_cplexFile filename (cplexProg (name, goal, constraints, bounds)) =
obua@16784
   611
    let
obua@16784
   612
	val f = TextIO.openOut filename
obua@16784
   613
	
obua@16784
   614
	fun basic_write s = TextIO.output(f, s)
obua@16784
   615
obua@16784
   616
	val linebuf = ref ""
obua@16784
   617
	fun buf_flushline s = 
obua@16784
   618
	    (basic_write (!linebuf); 
obua@16784
   619
	     basic_write "\n";
obua@16784
   620
	     linebuf := s)
obua@16784
   621
	fun buf_add s = linebuf := (!linebuf) ^ s
obua@16784
   622
obua@16784
   623
	fun write s = 
obua@16784
   624
	    if (String.size s) + (String.size (!linebuf)) >= 250 then 
obua@16784
   625
		buf_flushline ("    "^s)
obua@16784
   626
	    else 
obua@16784
   627
		buf_add s
obua@16784
   628
obua@16784
   629
        fun writeln s = (buf_add s; buf_flushline "")
obua@16784
   630
        
obua@16784
   631
	fun write_term (cplexVar x) = write x
obua@16784
   632
	  | write_term (cplexNum x) = write x
obua@16784
   633
	  | write_term cplexInf = write "inf"
obua@16784
   634
	  | write_term (cplexProd (cplexNum "1", b)) = write_term b
obua@16784
   635
	  | write_term (cplexProd (a, b)) = 
obua@16784
   636
	    (write_term a; write " "; write_term b)
obua@16784
   637
          | write_term (cplexNeg x) = (write " - "; write_term x)
obua@16784
   638
          | write_term (cplexSum ts) = write_terms ts
obua@16784
   639
	and write_terms [] = ()
obua@16784
   640
	  | write_terms (t::ts) = 
obua@16784
   641
	    (if (not (is_Neg t)) then write " + " else (); 
obua@16784
   642
	     write_term t; write_terms ts)
obua@16784
   643
obua@16784
   644
	fun write_goal (cplexMaximize term) = 
obua@16784
   645
	    (writeln "MAXIMIZE"; write_term term; writeln "")
obua@16784
   646
	  | write_goal (cplexMinimize term) = 
obua@16784
   647
	    (writeln "MINIMIZE"; write_term term; writeln "")
obua@16784
   648
obua@16784
   649
	fun write_cmp cplexLe = write "<"
obua@16784
   650
	  | write_cmp cplexLeq = write "<="
obua@16784
   651
	  | write_cmp cplexEq = write "="
obua@16784
   652
	  | write_cmp cplexGe = write ">"
obua@16784
   653
	  | write_cmp cplexGeq = write ">="
obua@16784
   654
        
obua@16784
   655
	fun write_constr (cplexConstr (cmp, (a,b))) = 
obua@16784
   656
	    (write_term a;
obua@16784
   657
	     write " ";
obua@16784
   658
	     write_cmp cmp;
obua@16784
   659
	     write " ";
obua@16784
   660
	     write_term b)
obua@16784
   661
        
obua@16784
   662
	fun write_constraints [] = ()
obua@16784
   663
	  | write_constraints (c::cs) = 
obua@16784
   664
	    (if (fst c <> NONE) 
obua@16784
   665
	     then 
obua@16784
   666
		 (write (the (fst c)); write ": ") 
obua@16784
   667
	     else 
obua@16784
   668
		 ();
obua@16784
   669
	     write_constr (snd c);
obua@16784
   670
	     writeln "";
obua@16784
   671
	     write_constraints cs)
obua@16784
   672
obua@16784
   673
	fun write_bounds [] = ()
obua@16784
   674
	  | write_bounds ((cplexBounds (t1,c1,t2,c2,t3))::bs) =
obua@16784
   675
	    ((if t1 = cplexNeg cplexInf andalso t3 = cplexInf
obua@16784
   676
		 andalso (c1 = cplexLeq orelse c1 = cplexLe) 
obua@16784
   677
		 andalso (c2 = cplexLeq orelse c2 = cplexLe) 
obua@16784
   678
	      then
obua@16784
   679
		  (write_term t2; write " free")
obua@16784
   680
	      else		 		 
obua@16784
   681
		  (write_term t1; write " "; write_cmp c1; write " ";
obua@16784
   682
		   write_term t2; write " "; write_cmp c2; write " ";
obua@16784
   683
		   write_term t3)
obua@16784
   684
	     ); writeln ""; write_bounds bs)
obua@16784
   685
	  | write_bounds ((cplexBound (t1, c, t2)) :: bs) = 
obua@16784
   686
	    (write_term t1; write " "; 
obua@16784
   687
	     write_cmp c; write " ";
obua@16784
   688
	     write_term t2; writeln ""; write_bounds bs)
obua@16784
   689
	     
obua@16784
   690
	val _ = write_goal goal
obua@16784
   691
        val _ = (writeln ""; writeln "ST")
obua@16784
   692
	val _ = write_constraints constraints
obua@16784
   693
        val _ = (writeln ""; writeln "BOUNDS")
obua@16784
   694
	val _ = write_bounds bounds
obua@16784
   695
        val _ = (writeln ""; writeln "END") 
obua@16784
   696
        val _ = TextIO.closeOut f
obua@16784
   697
    in
obua@16784
   698
	()
obua@16784
   699
    end
obua@16784
   700
obua@16784
   701
fun norm_Constr (constr as cplexConstr (c, (t1, t2))) = 
obua@16784
   702
    if not (modulo_signed is_Num t2) andalso  
obua@16784
   703
       modulo_signed is_Num t1 
obua@16784
   704
    then
obua@16784
   705
	[cplexConstr (rev_cmp c, (t2, t1))]
obua@16784
   706
    else if (c = cplexLe orelse c = cplexLeq) andalso
obua@16784
   707
	    (t1 = (cplexNeg cplexInf) orelse t2 = cplexInf)	    
obua@16784
   708
    then 
obua@16784
   709
	[]
obua@16784
   710
    else if (c = cplexGe orelse c = cplexGeq) andalso
obua@16784
   711
	    (t1 = cplexInf orelse t2 = cplexNeg cplexInf)
obua@16784
   712
    then
obua@16784
   713
	[]
obua@16784
   714
    else
obua@16784
   715
	[constr]
obua@16784
   716
obua@16784
   717
fun bound2constr (cplexBounds (t1,c1,t2,c2,t3)) =
obua@16784
   718
    (norm_Constr(cplexConstr (c1, (t1, t2))))
obua@16784
   719
    @ (norm_Constr(cplexConstr (c2, (t2, t3))))
obua@16784
   720
  | bound2constr (cplexBound (t1, cplexEq, t2)) =
obua@16784
   721
    (norm_Constr(cplexConstr (cplexLeq, (t1, t2))))
obua@16784
   722
    @ (norm_Constr(cplexConstr (cplexLeq, (t2, t1))))
obua@16784
   723
  | bound2constr (cplexBound (t1, c1, t2)) = 
obua@16784
   724
    norm_Constr(cplexConstr (c1, (t1,t2)))
obua@16784
   725
obua@16784
   726
val emptyset = Symtab.empty
obua@16784
   727
wenzelm@17412
   728
fun singleton v = Symtab.update (v, ()) emptyset
obua@16784
   729
obua@16784
   730
fun merge a b = Symtab.merge (op =) (a, b)
obua@16784
   731
obua@16784
   732
fun mergemap f ts = Library.foldl
obua@16784
   733
			(fn (table, x) => merge table (f x))
obua@16784
   734
			(Symtab.empty, ts)
obua@16784
   735
obua@16784
   736
fun diff a b = Symtab.foldl (fn (a, (k,v)) => 
obua@16784
   737
			 (Symtab.delete k a) handle UNDEF => a) 
obua@16784
   738
		     (a, b)
obua@16784
   739
		    
obua@16784
   740
fun collect_vars (cplexVar v) = singleton v
obua@16784
   741
  | collect_vars (cplexNeg t) = collect_vars t
obua@16784
   742
  | collect_vars (cplexProd (t1, t2)) = 
obua@16784
   743
    merge (collect_vars t1) (collect_vars t2)
obua@16784
   744
  | collect_vars (cplexSum ts) = mergemap collect_vars ts
obua@16784
   745
  | collect_vars _ = emptyset
obua@16784
   746
obua@16784
   747
(* Eliminates all nonfree bounds from the linear program and produces an
obua@16784
   748
   equivalent program with only free bounds 
obua@16784
   749
   IF for the input program P holds: is_normed_cplexProg P *)
obua@16784
   750
fun elim_nonfree_bounds (cplexProg (name, goal, constraints, bounds)) =
obua@16784
   751
    let
obua@16784
   752
	fun collect_constr_vars (_, cplexConstr (c, (t1,_))) =
obua@16784
   753
	    (collect_vars t1)   
obua@16784
   754
	
obua@16784
   755
	val cvars = merge (collect_vars (term_of_goal goal)) 
obua@16784
   756
			  (mergemap collect_constr_vars constraints)         
obua@16784
   757
		    
obua@16784
   758
	fun collect_lower_bounded_vars 
obua@16784
   759
	    (cplexBounds (t1, c1, cplexVar v, c2, t3)) =
obua@16784
   760
	    singleton v
obua@16784
   761
	  |  collect_lower_bounded_vars 
obua@16784
   762
		 (cplexBound (_, cplexLe, cplexVar v)) =
obua@16784
   763
	     singleton v
obua@16784
   764
	  |  collect_lower_bounded_vars 
obua@16784
   765
		 (cplexBound (_, cplexLeq, cplexVar v)) = 
obua@16784
   766
	     singleton v
obua@16784
   767
	  |  collect_lower_bounded_vars 
obua@16784
   768
		 (cplexBound (cplexVar v, cplexGe,_)) = 
obua@16784
   769
	     singleton v
obua@16784
   770
	  |  collect_lower_bounded_vars 
obua@16784
   771
		 (cplexBound (cplexVar v, cplexGeq, _)) = 
obua@16784
   772
	     singleton v
obua@16784
   773
	  | collect_lower_bounded_vars
obua@16784
   774
	    (cplexBound (cplexVar v, cplexEq, _)) = 
obua@16784
   775
	    singleton v
obua@16784
   776
	  |  collect_lower_bounded_vars _ = emptyset
obua@16784
   777
	
obua@16784
   778
	val lvars = mergemap collect_lower_bounded_vars bounds        
obua@16784
   779
	val positive_vars = diff cvars lvars			   
obua@16784
   780
	val zero = cplexNum "0"
obua@16784
   781
	
obua@16784
   782
	fun make_pos_constr v = 
obua@16784
   783
	    (NONE, cplexConstr (cplexGeq, ((cplexVar v), zero)))
obua@16784
   784
	
obua@16784
   785
	fun make_free_bound v = 
obua@16784
   786
	    cplexBounds (cplexNeg cplexInf, cplexLeq, 
obua@16784
   787
			 cplexVar v, cplexLeq,
obua@16784
   788
			 cplexInf)
obua@16784
   789
	
obua@16784
   790
	val pos_constrs = rev(Symtab.foldl 
obua@16784
   791
			      (fn (l, (k,v)) => (make_pos_constr k) :: l)
obua@16784
   792
			      ([], positive_vars))
obua@16784
   793
        val bound_constrs = map (fn x => (NONE, x)) 
obua@16784
   794
				(Library.flat (map bound2constr bounds))
obua@16784
   795
	val constraints' = constraints @ pos_constrs @ bound_constrs	   
obua@16784
   796
	val bounds' = rev(Symtab.foldl (fn (l, (v,_)) => 
obua@16784
   797
					   (make_free_bound v)::l)
obua@16784
   798
				       ([], cvars))			  
obua@16784
   799
    in
obua@16784
   800
	cplexProg (name, goal, constraints', bounds')
obua@16784
   801
    end
obua@16784
   802
obua@16784
   803
fun relax_strict_ineqs (cplexProg (name, goals, constrs, bounds)) = 
obua@16784
   804
    let
obua@16784
   805
	fun relax cplexLe = cplexLeq
obua@16784
   806
	  | relax cplexGe = cplexGeq
obua@16784
   807
	  | relax x = x
obua@16784
   808
	
obua@16784
   809
	fun relax_constr (n, cplexConstr(c, (t1, t2))) = 
obua@16784
   810
	    (n, cplexConstr(relax c, (t1, t2)))
obua@16784
   811
	    
obua@16784
   812
	fun relax_bounds (cplexBounds (t1, c1, t2, c2, t3)) = 
obua@16784
   813
	    cplexBounds (t1, relax c1, t2, relax c2, t3)
obua@16784
   814
	  | relax_bounds (cplexBound (t1, c, t2)) = 
obua@16784
   815
	    cplexBound (t1, relax c, t2)
obua@16784
   816
    in
obua@16784
   817
	cplexProg (name, 
obua@16784
   818
		   goals, 
obua@16784
   819
		   map relax_constr constrs, 
obua@16784
   820
		   map relax_bounds bounds)
obua@16784
   821
    end
obua@16784
   822
obua@16784
   823
datatype cplexResult = Unbounded 
obua@16784
   824
		     | Infeasible 
obua@16784
   825
		     | Undefined
obua@16784
   826
		     | Optimal of string * ((string * string) list)
obua@16784
   827
obua@16784
   828
fun is_separator x = forall (fn c => c = #"-") (String.explode x)
obua@16784
   829
obua@16784
   830
fun is_sign x = (x = "+" orelse x = "-")
obua@16784
   831
obua@16784
   832
fun is_colon x = (x = ":")
obua@16784
   833
obua@16784
   834
fun is_resultsymbol a = 
obua@16784
   835
    let
obua@16784
   836
	val symbol_char = String.explode "!\"#$%&()/,.;?@_`'{}|~-"
obua@16784
   837
	fun is_symbol_char c = Char.isAlphaNum c orelse 
obua@16784
   838
			       exists (fn d => d=c) symbol_char
obua@16784
   839
	fun is_symbol_start c = is_symbol_char c andalso 
obua@16784
   840
				not (Char.isDigit c) andalso 
obua@16784
   841
				not (c= #".") andalso
obua@16784
   842
				not (c= #"-")
obua@16784
   843
	val b = String.explode a
obua@16784
   844
    in
obua@16784
   845
	b <> [] andalso is_symbol_start (hd b) andalso 
obua@16784
   846
	forall is_symbol_char b
obua@16784
   847
    end
obua@16784
   848
obua@16784
   849
val TOKEN_SIGN = 100
obua@16784
   850
val TOKEN_COLON = 101
obua@16784
   851
val TOKEN_SEPARATOR = 102
obua@16784
   852
obua@16784
   853
fun load_glpkResult name = 
obua@16784
   854
    let
obua@16784
   855
	val flist = [(is_NL, TOKEN_NL), 
obua@16784
   856
		     (is_blank, TOKEN_BLANK),
obua@16784
   857
		     (is_num, TOKEN_NUM),
obua@16784
   858
		     (is_sign, TOKEN_SIGN),
obua@16784
   859
                     (is_colon, TOKEN_COLON),
obua@16784
   860
		     (is_cmp, TOKEN_CMP),
obua@16784
   861
		     (is_resultsymbol, TOKEN_SYMBOL),
obua@16784
   862
		     (is_separator, TOKEN_SEPARATOR)]
obua@16784
   863
obua@16784
   864
	val tokenize = tokenize_general flist
obua@16784
   865
obua@16784
   866
	val f = TextIO.openIn name  
obua@16784
   867
obua@16784
   868
	val rest = ref []
obua@16784
   869
		   
obua@16784
   870
	fun readToken_helper () =
obua@16784
   871
	    if length (!rest) > 0 then  
obua@16784
   872
		let val u = hd (!rest) in 
obua@16784
   873
		    (
obua@16784
   874
		     rest := tl (!rest); 
obua@16784
   875
		     SOME u
obua@16784
   876
		    ) 
obua@16784
   877
		end
obua@16784
   878
	    else 
obua@16784
   879
		let val s = TextIO.inputLine f in
obua@16784
   880
		    if s = "" then NONE else (rest := tokenize s; readToken_helper())					     
obua@16784
   881
		end           
obua@16784
   882
		
obua@16784
   883
	fun is_tt tok ty = (tok <> NONE andalso (fst (the tok)) = ty)
obua@16784
   884
obua@16784
   885
	fun pushToken a = if a = NONE then () else (rest := ((the a)::(!rest)))
obua@16784
   886
	
obua@16784
   887
	fun readToken () =
obua@16784
   888
	    let val t = readToken_helper () in
obua@16784
   889
		if is_tt t TOKEN_BLANK then 
obua@16784
   890
		    readToken ()
obua@16784
   891
		else if is_tt t TOKEN_NL then 
obua@16784
   892
		    let val t2 = readToken_helper () in
obua@16784
   893
			if is_tt t2 TOKEN_SIGN then 
obua@16784
   894
			    (pushToken (SOME (TOKEN_SEPARATOR, "-")); t)
obua@16784
   895
			else 
obua@16784
   896
			    (pushToken t2; t)
obua@16784
   897
		    end
obua@16784
   898
		else if is_tt t TOKEN_SIGN then
obua@16784
   899
		    let val t2 = readToken_helper () in
obua@16784
   900
			if is_tt t2 TOKEN_NUM then
obua@16784
   901
			    (SOME (TOKEN_NUM, (snd (the t))^(snd (the t2))))
obua@16784
   902
			else
obua@16784
   903
			    (pushToken t2; t)
obua@16784
   904
		    end
obua@16784
   905
		else
obua@16784
   906
		    t
obua@16784
   907
	    end	    		
obua@16784
   908
obua@16784
   909
        fun readRestOfLine P = 
obua@16784
   910
	    let 
obua@16784
   911
		val t = readToken ()
obua@16784
   912
	    in
obua@16784
   913
		if is_tt t TOKEN_NL orelse t = NONE 
obua@16784
   914
		then P
obua@16784
   915
		else readRestOfLine P
obua@16784
   916
	    end			
obua@16784
   917
							 
obua@16784
   918
	fun readHeader () = 
obua@16784
   919
	    let
obua@16784
   920
		fun readStatus () = readRestOfLine ("STATUS", snd (the (readToken ())))
obua@16784
   921
		fun readObjective () = readRestOfLine ("OBJECTIVE", snd (the (readToken (); readToken (); readToken ())))
obua@16784
   922
		val t1 = readToken ()
obua@16784
   923
		val t2 = readToken ()
obua@16784
   924
	    in
obua@16784
   925
		if is_tt t1 TOKEN_SYMBOL andalso is_tt t2 TOKEN_COLON 
obua@16784
   926
		then
obua@16784
   927
		    case to_upper (snd (the t1)) of
obua@16784
   928
			"STATUS" => (readStatus ())::(readHeader ())
obua@16784
   929
		      | "OBJECTIVE" => (readObjective())::(readHeader ())
obua@16784
   930
		      | _ => (readRestOfLine (); readHeader ())
obua@16784
   931
		else
obua@16784
   932
		    (pushToken t2; pushToken t1; [])
obua@16784
   933
	    end
obua@16784
   934
obua@16784
   935
	fun skip_until_sep () = 
obua@16784
   936
	    let val x = readToken () in
obua@16784
   937
		if is_tt x TOKEN_SEPARATOR then
obua@16784
   938
		    readRestOfLine ()
obua@16784
   939
		else 
obua@16784
   940
		    skip_until_sep ()
obua@16784
   941
	    end
obua@16784
   942
obua@16784
   943
	fun load_value () =
obua@16784
   944
	    let 
obua@16784
   945
		val t1 = readToken ()
obua@16784
   946
		val t2 = readToken ()
obua@16784
   947
	    in
obua@16784
   948
		if is_tt t1 TOKEN_NUM andalso is_tt t2 TOKEN_SYMBOL then
obua@16784
   949
		    let 
obua@16784
   950
			val t = readToken ()
obua@16784
   951
			val state = if is_tt t TOKEN_NL then readToken () else t
obua@16784
   952
			val _ = if is_tt state TOKEN_SYMBOL then () else raise (Load_cplexResult "state expected")
obua@16784
   953
			val k = readToken ()
obua@16784
   954
		    in
obua@16784
   955
			if is_tt k TOKEN_NUM then
obua@16784
   956
			    readRestOfLine (SOME (snd (the t2), snd (the k)))
obua@16784
   957
			else
obua@16784
   958
			    raise (Load_cplexResult "number expected")
obua@16784
   959
		    end				
obua@16784
   960
		else
obua@16784
   961
		    (pushToken t2; pushToken t1; NONE)
obua@16784
   962
	    end
obua@16784
   963
obua@16784
   964
	fun load_values () = 
obua@16784
   965
	    let val v = load_value () in
obua@16784
   966
		if v = NONE then [] else (the v)::(load_values ())
obua@16784
   967
	    end
obua@16784
   968
	
obua@16784
   969
	val header = readHeader () 
obua@16784
   970
obua@16784
   971
	val result = 
haftmann@17521
   972
	    case AList.lookup (op =) header "STATUS" of
obua@16784
   973
		SOME "INFEASIBLE" => Infeasible
obua@16784
   974
	      | SOME "UNBOUNDED" => Unbounded
haftmann@17521
   975
	      | SOME "OPTIMAL" => Optimal (the (AList.lookup (op =) header "OBJECTIVE"), 
obua@16784
   976
					   (skip_until_sep (); 
obua@16784
   977
					    skip_until_sep ();
obua@16784
   978
					    load_values ()))
obua@16784
   979
	      | _ => Undefined
obua@16784
   980
obua@16784
   981
	val _ = TextIO.closeIn f
obua@16784
   982
    in
obua@16784
   983
	result
obua@16784
   984
    end
obua@16784
   985
    handle (Tokenize s) => raise (Load_cplexResult ("Tokenize: "^s))
obua@16784
   986
	 | Option => raise (Load_cplexResult "Option")
obua@16784
   987
	 | x => raise x
obua@16784
   988
obua@16784
   989
fun load_cplexResult name = 
obua@16784
   990
    let
obua@16784
   991
	val flist = [(is_NL, TOKEN_NL), 
obua@16784
   992
		     (is_blank, TOKEN_BLANK),
obua@16784
   993
		     (is_num, TOKEN_NUM),
obua@16784
   994
		     (is_sign, TOKEN_SIGN),
obua@16784
   995
                     (is_colon, TOKEN_COLON),
obua@16784
   996
		     (is_cmp, TOKEN_CMP),
obua@16784
   997
		     (is_resultsymbol, TOKEN_SYMBOL)]
obua@16784
   998
obua@16784
   999
	val tokenize = tokenize_general flist
obua@16784
  1000
obua@16784
  1001
	val f = TextIO.openIn name  
obua@16784
  1002
obua@16784
  1003
	val rest = ref []
obua@16784
  1004
		   
obua@16784
  1005
	fun readToken_helper () =
obua@16784
  1006
	    if length (!rest) > 0 then  
obua@16784
  1007
		let val u = hd (!rest) in 
obua@16784
  1008
		    (
obua@16784
  1009
		     rest := tl (!rest); 
obua@16784
  1010
		     SOME u
obua@16784
  1011
		    ) 
obua@16784
  1012
		end
obua@16784
  1013
	    else 
obua@16784
  1014
		let 
obua@16784
  1015
		    val s = TextIO.inputLine f 
obua@16784
  1016
		in		    
obua@16784
  1017
		    if s = "" then NONE else (rest := tokenize s; readToken_helper())					     
obua@16784
  1018
		end           
obua@16784
  1019
		
obua@16784
  1020
	fun is_tt tok ty = (tok <> NONE andalso (fst (the tok)) = ty)
obua@16784
  1021
obua@16784
  1022
	fun pushToken a = if a = NONE then () else (rest := ((the a)::(!rest)))
obua@16784
  1023
	
obua@16784
  1024
	fun readToken () =
obua@16784
  1025
	    let val t = readToken_helper () in
obua@16784
  1026
		if is_tt t TOKEN_BLANK then 
obua@16784
  1027
		    readToken ()
obua@16784
  1028
		else if is_tt t TOKEN_SIGN then
obua@16784
  1029
		    let val t2 = readToken_helper () in
obua@16784
  1030
			if is_tt t2 TOKEN_NUM then
obua@16784
  1031
			    (SOME (TOKEN_NUM, (snd (the t))^(snd (the t2))))
obua@16784
  1032
			else
obua@16784
  1033
			    (pushToken t2; t)
obua@16784
  1034
		    end
obua@16784
  1035
		else
obua@16784
  1036
		    t
obua@16784
  1037
	    end	    		
obua@16784
  1038
obua@16784
  1039
        fun readRestOfLine P = 
obua@16784
  1040
	    let 
obua@16784
  1041
		val t = readToken ()
obua@16784
  1042
	    in
obua@16784
  1043
		if is_tt t TOKEN_NL orelse t = NONE 
obua@16784
  1044
		then P
obua@16784
  1045
		else readRestOfLine P
obua@16784
  1046
	    end			
obua@16784
  1047
obua@16784
  1048
	fun readHeader () = 
obua@16784
  1049
	    let
obua@16784
  1050
		fun readStatus () = readRestOfLine ("STATUS", snd (the (readToken ())))
obua@16784
  1051
		fun readObjective () = 
obua@16784
  1052
		    let
obua@16784
  1053
			val t = readToken ()
obua@16784
  1054
		    in
obua@16784
  1055
			if is_tt t TOKEN_SYMBOL andalso to_upper (snd (the t)) = "VALUE" then 
obua@16784
  1056
			    readRestOfLine ("OBJECTIVE", snd (the (readToken())))
obua@16784
  1057
			else
obua@16784
  1058
			    readRestOfLine ("OBJECTIVE_NAME", snd (the t))
obua@16784
  1059
		    end
obua@16784
  1060
		  
obua@16784
  1061
		val t = readToken ()
obua@16784
  1062
	    in
obua@16784
  1063
		if is_tt t TOKEN_SYMBOL then
obua@16784
  1064
		    case to_upper (snd (the t)) of 
obua@16784
  1065
			"STATUS" => (readStatus ())::(readHeader ())
obua@16784
  1066
		      | "OBJECTIVE" => (readObjective ())::(readHeader ())
obua@16784
  1067
		      | "SECTION" => (pushToken t; [])
obua@16784
  1068
		      | _ => (readRestOfLine (); readHeader ())
obua@16784
  1069
		else
obua@16784
  1070
		    (readRestOfLine (); readHeader ())
obua@16784
  1071
	    end
obua@16784
  1072
obua@16784
  1073
	fun skip_nls () = 
obua@16784
  1074
	    let val x = readToken () in
obua@16784
  1075
		if is_tt x TOKEN_NL then 
obua@16784
  1076
		    skip_nls () 
obua@16784
  1077
		else 
obua@16784
  1078
		    (pushToken x; ())
obua@16784
  1079
	    end
obua@16784
  1080
obua@16784
  1081
	fun skip_paragraph () = 
obua@16784
  1082
	    if is_tt (readToken ()) TOKEN_NL then
obua@16784
  1083
		(if is_tt (readToken ()) TOKEN_NL then
obua@16784
  1084
		     skip_nls ()
obua@16784
  1085
		 else
obua@16784
  1086
		     skip_paragraph ())
obua@16784
  1087
	    else			
obua@16784
  1088
		skip_paragraph ()	
obua@16784
  1089
obua@16784
  1090
	fun load_value () =
obua@16784
  1091
	    let 
obua@16784
  1092
		val t1 = readToken ()
obua@16784
  1093
		val t1 = if is_tt t1 TOKEN_SYMBOL andalso snd (the t1) = "A" then readToken () else t1
obua@16784
  1094
	    in
obua@16784
  1095
		if is_tt t1 TOKEN_NUM then
obua@16784
  1096
		    let 
obua@16784
  1097
			val name = readToken ()
obua@16784
  1098
			val status = readToken ()
obua@16784
  1099
			val value = readToken ()
obua@16784
  1100
		    in
obua@16784
  1101
			if is_tt name TOKEN_SYMBOL andalso
obua@16784
  1102
			   is_tt status TOKEN_SYMBOL andalso
obua@16784
  1103
			   is_tt value TOKEN_NUM 
obua@16784
  1104
			then
obua@16784
  1105
			    readRestOfLine (SOME (snd (the name), snd (the value)))
obua@16784
  1106
			else
obua@16784
  1107
			    raise (Load_cplexResult "column line expected")
obua@16784
  1108
		    end
obua@16784
  1109
		else 
obua@16784
  1110
		    (pushToken t1; NONE)
obua@16784
  1111
	    end
obua@16784
  1112
obua@16784
  1113
	fun load_values () = 
obua@16784
  1114
	    let val v = load_value () in
obua@16784
  1115
		if v = NONE then [] else (the v)::(load_values ())
obua@16784
  1116
	    end
obua@16784
  1117
	
obua@16784
  1118
	val header = readHeader ()
obua@16784
  1119
obua@16784
  1120
	val result = 
haftmann@17521
  1121
	    case AList.lookup (op =) header "STATUS" of
obua@16784
  1122
		SOME "INFEASIBLE" => Infeasible
obua@16784
  1123
	      | SOME "NONOPTIMAL" => Unbounded
haftmann@17521
  1124
	      | SOME "OPTIMAL" => Optimal (the (AList.lookup (op =) header "OBJECTIVE"), 
obua@16784
  1125
					   (skip_paragraph (); 
obua@16784
  1126
					    skip_paragraph (); 
obua@16784
  1127
					    skip_paragraph (); 
obua@16784
  1128
					    skip_paragraph (); 
obua@16784
  1129
					    skip_paragraph ();
obua@16784
  1130
					    load_values ()))
obua@16784
  1131
	      | _ => Undefined
obua@16784
  1132
obua@16784
  1133
	val _ = TextIO.closeIn f
obua@16784
  1134
    in
obua@16784
  1135
	result
obua@16784
  1136
    end
obua@16784
  1137
    handle (Tokenize s) => raise (Load_cplexResult ("Tokenize: "^s))
obua@16784
  1138
	 | Option => raise (Load_cplexResult "Option")
obua@16784
  1139
	 | x => raise x
obua@16784
  1140
obua@16784
  1141
exception Execute of string;
obua@16784
  1142
obua@16784
  1143
fun tmp_file s = Path.pack (Path.expand (File.tmp_path (Path.make [s])));
obua@16784
  1144
fun wrap s = "\""^s^"\"";
obua@16784
  1145
obua@16784
  1146
fun solve_glpk prog =
obua@16784
  1147
    let 
obua@16784
  1148
	val name = LargeInt.toString (Time.toMicroseconds (Time.now ()))	
obua@16784
  1149
	val lpname = tmp_file (name^".lp")
obua@16784
  1150
	val resultname = tmp_file (name^".txt")
obua@16784
  1151
	val _ = save_cplexFile lpname prog		
obua@16966
  1152
	val cplex_path = getenv "GLPK_PATH"
obua@16784
  1153
	val cplex = if cplex_path = "" then "glpsol" else cplex_path
obua@16784
  1154
	val command = (wrap cplex)^" --lpt "^(wrap lpname)^" --output "^(wrap resultname)
obua@16784
  1155
	val answer = execute command
obua@16784
  1156
    in
obua@16784
  1157
	let
obua@16784
  1158
	    val result = load_glpkResult resultname
obua@16784
  1159
	    val _ = OS.FileSys.remove lpname
obua@16784
  1160
	    val _ = OS.FileSys.remove resultname
obua@16784
  1161
	in
obua@16784
  1162
	    result
obua@16784
  1163
	end 
obua@16784
  1164
	handle (Load_cplexResult s) => raise (Execute ("Load_cplexResult: "^s^"\nExecute: "^answer))
obua@16784
  1165
	     | _ => raise (Execute answer)
obua@16784
  1166
    end		     
obua@16784
  1167
    
obua@16784
  1168
fun solve_cplex prog =
obua@16784
  1169
    let 
obua@16784
  1170
	fun write_script s lp r =
obua@16784
  1171
	    let
obua@16784
  1172
		val f = TextIO.openOut s
obua@16784
  1173
		val _ = TextIO.output (f, "read\n"^lp^"\noptimize\nwrite\n"^r^"\nquit")
obua@16784
  1174
		val _ = TextIO.closeOut f
obua@16784
  1175
	    in 
obua@16784
  1176
		() 
obua@16784
  1177
	    end 
obua@16784
  1178
	    
obua@16784
  1179
	val name = LargeInt.toString (Time.toMicroseconds (Time.now ()))	
obua@16784
  1180
	val lpname = tmp_file (name^".lp")
obua@16784
  1181
	val resultname = tmp_file (name^".txt")
obua@16784
  1182
	val scriptname = tmp_file (name^".script")
obua@16784
  1183
	val _ = save_cplexFile lpname prog		
obua@16966
  1184
	val cplex_path = getenv "CPLEX_PATH"
obua@16784
  1185
	val cplex = if cplex_path = "" then "cplex" else cplex_path
obua@16784
  1186
	val _ = write_script scriptname lpname resultname
obua@16784
  1187
	val command = (wrap cplex)^" < "^(wrap scriptname)^" > /dev/null"
obua@16784
  1188
	val answer = "return code "^(Int.toString (system command))
obua@16784
  1189
    in
obua@16784
  1190
	let
obua@16784
  1191
	    val result = load_cplexResult resultname
obua@16784
  1192
	    val _ = OS.FileSys.remove lpname
obua@16784
  1193
	    val _ = OS.FileSys.remove resultname
obua@16784
  1194
	    val _ = OS.FileSys.remove scriptname
obua@16784
  1195
	in
obua@16784
  1196
	    result
obua@16784
  1197
	end 
obua@16784
  1198
    end
obua@16784
  1199
obua@16784
  1200
fun solve prog = 
obua@16966
  1201
    case get_solver () of
obua@16966
  1202
      SOLVER_DEFAULT => 
obua@16966
  1203
        (case getenv "LP_SOLVER" of
obua@16966
  1204
	   "CPLEX" => solve_cplex prog
obua@16966
  1205
         | "GLPK" => solve_glpk prog
obua@16966
  1206
         | _ => raise (Execute ("LP_SOLVER must be set to CPLEX or to GLPK")))
obua@16966
  1207
    | SOLVER_CPLEX => solve_cplex prog
obua@16966
  1208
    | SOLVER_GLPK => solve_glpk prog
obua@16784
  1209
		   
obua@16784
  1210
end;
obua@16784
  1211
obua@16784
  1212
(*
obua@16784
  1213
val demofile = "/home/obua/flyspeck/kepler/LP/cplexPent2.lp45"
obua@16784
  1214
val demoout = "/home/obua/flyspeck/kepler/LP/test.out"
obua@16784
  1215
val demoresult = "/home/obua/flyspeck/kepler/LP/try/test2.sol"
obua@16784
  1216
	   
obua@16784
  1217
fun loadcplex () = Cplex.relax_strict_ineqs 
obua@16784
  1218
		   (Cplex.load_cplexFile demofile)
obua@16784
  1219
obua@16784
  1220
fun writecplex lp = Cplex.save_cplexFile demoout lp
obua@16784
  1221
obua@16784
  1222
fun test () = 
obua@16784
  1223
    let
obua@16784
  1224
	val lp = loadcplex ()
obua@16784
  1225
	val lp2 = Cplex.elim_nonfree_bounds lp
obua@16784
  1226
    in
obua@16784
  1227
	writecplex lp2
obua@16784
  1228
    end
obua@16784
  1229
obua@16784
  1230
fun loadresult () = Cplex.load_cplexResult demoresult;
obua@16784
  1231
*)
obua@16784
  1232
obua@16784
  1233
(*val prog = Cplex.load_cplexFile "/home/obua/tmp/pent/graph_0.lpt";
obua@16784
  1234
val _ = Cplex.solve prog;*)