src/HOL/Matrix/Cplex.ML
changeset 15178 5f621aa35c25
child 15531 08c8dad8e399
     1.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     1.2 +++ b/src/HOL/Matrix/Cplex.ML	Fri Sep 03 17:10:36 2004 +0200
     1.3 @@ -0,0 +1,1027 @@
     1.4 +signature CPLEX =
     1.5 +sig
     1.6 +    
     1.7 +    datatype cplexTerm = cplexVar of string | cplexNum of string | cplexInf 
     1.8 +                       | cplexNeg of cplexTerm 
     1.9 +                       | cplexProd of cplexTerm * cplexTerm 
    1.10 +                       | cplexSum of (cplexTerm list) 
    1.11 +    
    1.12 +    datatype cplexComp = cplexLe | cplexLeq | cplexEq | cplexGe | cplexGeq 
    1.13 +								  
    1.14 +    datatype cplexGoal = cplexMinimize of cplexTerm 
    1.15 +		       | cplexMaximize of cplexTerm
    1.16 +					  
    1.17 +    datatype cplexConstr = cplexConstr of cplexComp * 
    1.18 +					  (cplexTerm * cplexTerm)
    1.19 +					  
    1.20 +    datatype cplexBounds = cplexBounds of cplexTerm * cplexComp * cplexTerm 
    1.21 +					  * cplexComp * cplexTerm
    1.22 +			 | cplexBound of cplexTerm * cplexComp * cplexTerm
    1.23 +					 
    1.24 +    datatype cplexProg = cplexProg of string 
    1.25 +				      * cplexGoal 
    1.26 +				      * ((string option * cplexConstr) 
    1.27 +					     list) 
    1.28 +				      * cplexBounds list
    1.29 +				      
    1.30 +    datatype cplexResult = Unbounded 
    1.31 +			 | Infeasible 
    1.32 +			 | Undefined
    1.33 +			 | Optimal of string * 
    1.34 +				      (((* name *) string * 
    1.35 +					(* value *) string) list)
    1.36 +						     
    1.37 +    exception Load_cplexFile of string
    1.38 +    exception Load_cplexResult of string
    1.39 +    exception Save_cplexFile of string
    1.40 +    exception Execute of string
    1.41 +
    1.42 +    val load_cplexFile : string -> cplexProg
    1.43 +
    1.44 +    val save_cplexFile : string -> cplexProg -> unit 
    1.45 +
    1.46 +    val elim_nonfree_bounds : cplexProg -> cplexProg
    1.47 +
    1.48 +    val relax_strict_ineqs : cplexProg -> cplexProg
    1.49 +
    1.50 +    val is_normed_cplexProg : cplexProg -> bool
    1.51 +
    1.52 +    val load_cplexResult : string -> cplexResult
    1.53 +
    1.54 +    val solve : cplexProg -> cplexResult
    1.55 +end;
    1.56 +
    1.57 +structure Cplex : CPLEX =
    1.58 +struct
    1.59 +
    1.60 +exception Load_cplexFile of string;
    1.61 +exception Load_cplexResult of string;
    1.62 +exception Save_cplexFile of string;
    1.63 +	  
    1.64 +datatype cplexTerm = cplexVar of string 
    1.65 +		   | cplexNum of string 
    1.66 +		   | cplexInf 
    1.67 +                   | cplexNeg of cplexTerm 
    1.68 +                   | cplexProd of cplexTerm * cplexTerm 
    1.69 +                   | cplexSum of (cplexTerm list) 
    1.70 +datatype cplexComp = cplexLe | cplexLeq | cplexEq | cplexGe | cplexGeq 
    1.71 +datatype cplexGoal = cplexMinimize of cplexTerm | cplexMaximize of cplexTerm
    1.72 +datatype cplexConstr = cplexConstr of cplexComp * (cplexTerm * cplexTerm)
    1.73 +datatype cplexBounds = cplexBounds of cplexTerm * cplexComp * cplexTerm 
    1.74 +				      * cplexComp * cplexTerm
    1.75 +                     | cplexBound of cplexTerm * cplexComp * cplexTerm 
    1.76 +datatype cplexProg = cplexProg of string 
    1.77 +				  * cplexGoal 
    1.78 +				  * ((string option * cplexConstr) list) 
    1.79 +				  * cplexBounds list
    1.80 +				  
    1.81 +fun rev_cmp cplexLe = cplexGe
    1.82 +  | rev_cmp cplexLeq = cplexGeq
    1.83 +  | rev_cmp cplexGe = cplexLe
    1.84 +  | rev_cmp cplexGeq = cplexLeq
    1.85 +  | rev_cmp cplexEq = cplexEq
    1.86 +
    1.87 +fun the None = raise (Load_cplexFile "Some expected")
    1.88 +  | the (Some x) = x; 
    1.89 +    
    1.90 +fun modulo_signed is_something (cplexNeg u) = is_something u
    1.91 +  | modulo_signed is_something u = is_something u
    1.92 +
    1.93 +fun is_Num (cplexNum _) = true
    1.94 +  | is_Num _ = false
    1.95 +
    1.96 +fun is_Inf cplexInf = true
    1.97 +  | is_Inf _ = false
    1.98 +
    1.99 +fun is_Var (cplexVar _) = true
   1.100 +  | is_Var _ = false
   1.101 +
   1.102 +fun is_Neg (cplexNeg x ) = true
   1.103 +  | is_Neg _ = false
   1.104 +
   1.105 +fun is_normed_Prod (cplexProd (t1, t2)) = 
   1.106 +    (is_Num t1) andalso (is_Var t2)
   1.107 +  | is_normed_Prod x = is_Var x
   1.108 +
   1.109 +fun is_normed_Sum (cplexSum ts) = 
   1.110 +    (ts <> []) andalso forall (modulo_signed is_normed_Prod) ts
   1.111 +  | is_normed_Sum x = modulo_signed is_normed_Prod x
   1.112 +
   1.113 +fun is_normed_Constr (cplexConstr (c, (t1, t2))) = 
   1.114 +    (is_normed_Sum t1) andalso (modulo_signed is_Num t2)
   1.115 +
   1.116 +fun is_Num_or_Inf x = is_Inf x orelse is_Num x
   1.117 +
   1.118 +fun is_normed_Bounds (cplexBounds (t1, c1, t2, c2, t3)) =
   1.119 +    (c1 = cplexLe orelse c1 = cplexLeq) andalso 
   1.120 +    (c2 = cplexLe orelse c2 = cplexLeq) andalso
   1.121 +    is_Var t2 andalso
   1.122 +    modulo_signed is_Num_or_Inf t1 andalso
   1.123 +    modulo_signed is_Num_or_Inf t3
   1.124 +  | is_normed_Bounds (cplexBound (t1, c, t2)) =
   1.125 +    (is_Var t1 andalso (modulo_signed is_Num_or_Inf t2)) 
   1.126 +    orelse
   1.127 +    (c <> cplexEq andalso 
   1.128 +     is_Var t2 andalso (modulo_signed is_Num_or_Inf t1))
   1.129 +	             		
   1.130 +fun term_of_goal (cplexMinimize x) = x
   1.131 +  | term_of_goal (cplexMaximize x) = x
   1.132 +
   1.133 +fun is_normed_cplexProg (cplexProg (name, goal, constraints, bounds)) = 
   1.134 +    is_normed_Sum (term_of_goal goal) andalso
   1.135 +    forall (fn (_,x) => is_normed_Constr x) constraints andalso
   1.136 +    forall is_normed_Bounds bounds
   1.137 +
   1.138 +fun is_NL s = s = "\n"
   1.139 +
   1.140 +fun is_blank s = forall (fn c => c <> #"\n" andalso Char.isSpace c) (String.explode s)
   1.141 +		 
   1.142 +fun is_num a = 
   1.143 +    let 
   1.144 +	val b = String.explode a 
   1.145 +	fun num4 cs = forall Char.isDigit cs		      
   1.146 +	fun num3 [] = true
   1.147 +	  | num3 (ds as (c::cs)) = 
   1.148 +	    if c = #"+" orelse c = #"-" then
   1.149 +		num4 cs
   1.150 +	    else 
   1.151 +		num4 ds		    
   1.152 +	fun num2 [] = true
   1.153 +	  | num2 (c::cs) =
   1.154 +	    if c = #"e" orelse c = #"E" then num3 cs
   1.155 +	    else (Char.isDigit c) andalso num2 cs			 
   1.156 +	fun num1 [] = true
   1.157 +	  | num1 (c::cs) = 
   1.158 +	    if c = #"." then num2 cs 
   1.159 +	    else if c = #"e" orelse c = #"E" then num3 cs 
   1.160 +	    else (Char.isDigit c) andalso num1 cs
   1.161 +	fun num [] = true
   1.162 +	  | num (c::cs) = 
   1.163 +	    if c = #"." then num2 cs 
   1.164 +	    else (Char.isDigit c) andalso num1 cs
   1.165 +    in
   1.166 +	num b
   1.167 +    end  
   1.168 +
   1.169 +fun is_delimiter s = s = "+" orelse s = "-" orelse s = ":"
   1.170 +		    
   1.171 +fun is_cmp s = s = "<" orelse s = ">" orelse s = "<=" 
   1.172 +		     orelse s = ">=" orelse s = "="
   1.173 +
   1.174 +fun is_symbol a = 
   1.175 +    let
   1.176 +	val symbol_char = String.explode "!\"#$%&()/,.;?@_`'{}|~"
   1.177 +	fun is_symbol_char c = Char.isAlphaNum c orelse 
   1.178 +			       exists (fn d => d=c) symbol_char
   1.179 +	fun is_symbol_start c = is_symbol_char c andalso 
   1.180 +				not (Char.isDigit c) andalso 
   1.181 +				not (c= #".")
   1.182 +	val b = String.explode a
   1.183 +    in
   1.184 +	b <> [] andalso is_symbol_start (hd b) andalso 
   1.185 +	forall is_symbol_char b
   1.186 +    end
   1.187 +
   1.188 +fun to_upper s = String.implode (map Char.toUpper (String.explode s))
   1.189 +
   1.190 +fun keyword x = 
   1.191 +    let 	
   1.192 +	val a = to_upper x 
   1.193 +    in
   1.194 +	if a = "BOUNDS" orelse a = "BOUND" then
   1.195 +	    Some "BOUNDS"
   1.196 +	else if a = "MINIMIZE" orelse a = "MINIMUM" orelse a = "MIN" then
   1.197 +	    Some "MINIMIZE"
   1.198 +	else if a = "MAXIMIZE" orelse a = "MAXIMUM" orelse a = "MAX" then
   1.199 +	    Some "MAXIMIZE"
   1.200 +	else if a = "ST" orelse a = "S.T." orelse a = "ST." then
   1.201 +	    Some "ST"
   1.202 +	else if a = "FREE" orelse a = "END" then
   1.203 +	    Some a
   1.204 +	else if a = "GENERAL" orelse a = "GENERALS" orelse a = "GEN" then
   1.205 +	    Some "GENERAL"
   1.206 +	else if a = "INTEGER" orelse a = "INTEGERS" orelse a = "INT" then
   1.207 +	    Some "INTEGER"
   1.208 +	else if a = "BINARY" orelse a = "BINARIES" orelse a = "BIN" then
   1.209 +	    Some "BINARY"
   1.210 +	else if a = "INF" orelse a = "INFINITY" then
   1.211 +	    Some "INF"
   1.212 +	else								   
   1.213 +	    None
   1.214 +    end
   1.215 +	        
   1.216 +val TOKEN_ERROR = ~1
   1.217 +val TOKEN_BLANK = 0
   1.218 +val TOKEN_NUM = 1
   1.219 +val TOKEN_DELIMITER = 2
   1.220 +val TOKEN_SYMBOL = 3
   1.221 +val TOKEN_LABEL = 4
   1.222 +val TOKEN_CMP = 5
   1.223 +val TOKEN_KEYWORD = 6
   1.224 +val TOKEN_NL = 7
   1.225 +		      
   1.226 +(* tokenize takes a list of chars as argument and returns a list of
   1.227 +   int * string pairs, each string representing a "cplex token", 
   1.228 +   and each int being one of TOKEN_NUM, TOKEN_DELIMITER, TOKEN_CMP
   1.229 +   or TOKEN_SYMBOL *)
   1.230 +fun tokenize s = 
   1.231 +    let
   1.232 +	val flist = [(is_NL, TOKEN_NL), 
   1.233 +		     (is_blank, TOKEN_BLANK), 
   1.234 +		     (is_num, TOKEN_NUM),  
   1.235 +                     (is_delimiter, TOKEN_DELIMITER), 
   1.236 +		     (is_cmp, TOKEN_CMP), 
   1.237 +		     (is_symbol, TOKEN_SYMBOL)]  
   1.238 +	fun match_helper [] s = (fn x => false, TOKEN_ERROR)
   1.239 +	  | match_helper (f::fs) s = 
   1.240 +	    if ((fst f) s) then f else match_helper fs s   
   1.241 +	fun match s = match_helper flist s
   1.242 +	fun tok s = 
   1.243 +	    if s = "" then [] else       
   1.244 +	    let 
   1.245 +		val h = String.substring (s,0,1) 
   1.246 +		val (f, j) = match h
   1.247 +		fun len i = 
   1.248 +		    if size s = i then i 
   1.249 +		    else if f (String.substring (s,0,i+1)) then 
   1.250 +			len (i+1) 
   1.251 +		    else i 
   1.252 +	    in
   1.253 +		if j < 0 then 
   1.254 +		    (if h = "\\" then [] 
   1.255 +		     else raise (Load_cplexFile ("token expected, found: "
   1.256 +						 ^s)))
   1.257 +		else 
   1.258 +		    let 
   1.259 +			val l = len 1 
   1.260 +			val u = String.substring (s,0,l)
   1.261 +			val v = String.extract (s,l,NONE)
   1.262 +		    in
   1.263 +			if j = 0 then tok v else (j, u) :: tok v
   1.264 +		    end
   1.265 +	    end                
   1.266 +    in
   1.267 +	tok s     
   1.268 +    end
   1.269 +
   1.270 +exception Tokenize of string;
   1.271 +
   1.272 +fun tokenize_general flist s = 
   1.273 +    let
   1.274 +	fun match_helper [] s = raise (Tokenize s)
   1.275 +	  | match_helper (f::fs) s = 
   1.276 +	    if ((fst f) s) then f else match_helper fs s   
   1.277 +	fun match s = match_helper flist s
   1.278 +	fun tok s = 
   1.279 +	    if s = "" then [] else       
   1.280 +	    let 
   1.281 +		val h = String.substring (s,0,1) 
   1.282 +		val (f, j) = match h
   1.283 +		fun len i = 
   1.284 +		    if size s = i then i 
   1.285 +		    else if f (String.substring (s,0,i+1)) then 
   1.286 +			len (i+1) 
   1.287 +		    else i 
   1.288 +		val l = len 1
   1.289 +	    in
   1.290 +		(j, String.substring (s,0,l)) :: tok (String.extract (s,l,NONE))
   1.291 +	    end
   1.292 +    in
   1.293 +	tok s     
   1.294 +    end
   1.295 +
   1.296 +fun load_cplexFile name = 
   1.297 +    let 
   1.298 +	val f = TextIO.openIn name  
   1.299 +        val ignore_NL = ref true  
   1.300 +	val rest = ref []
   1.301 +
   1.302 +	fun is_symbol s c = (fst c) = TOKEN_SYMBOL andalso (to_upper (snd c)) = s 
   1.303 +		   
   1.304 +	fun readToken_helper () =
   1.305 +	    if length (!rest) > 0 then  
   1.306 +		let val u = hd (!rest) in 
   1.307 +		    (
   1.308 +		     rest := tl (!rest); 
   1.309 +		     Some u
   1.310 +		    ) 
   1.311 +		end
   1.312 +	    else 
   1.313 +		let val s = TextIO.inputLine f in
   1.314 +		    if s = "" then None else
   1.315 +		    let val t = tokenize s in
   1.316 +			if (length t >= 2 andalso 
   1.317 +			    snd(hd (tl t)) = ":") 
   1.318 +			then 
   1.319 +			    rest := (TOKEN_LABEL, snd (hd t)) :: (tl (tl t))
   1.320 +			else if (length t >= 2) andalso is_symbol "SUBJECT" (hd (t)) 
   1.321 +				andalso is_symbol "TO" (hd (tl t)) 
   1.322 +			then
   1.323 +			    rest := (TOKEN_SYMBOL, "ST") :: (tl (tl t))
   1.324 +			else
   1.325 +			    rest := t;
   1.326 +			readToken_helper ()  
   1.327 +		    end
   1.328 +		end           
   1.329 +	
   1.330 +	fun readToken_helper2 () = 
   1.331 +		let val c = readToken_helper () in
   1.332 +		    if c = None then None
   1.333 +                    else if !ignore_NL andalso fst (the c) = TOKEN_NL then
   1.334 +			readToken_helper2 ()
   1.335 +		    else if fst (the c) = TOKEN_SYMBOL 
   1.336 +			    andalso keyword (snd (the c)) <> None
   1.337 +		    then Some (TOKEN_KEYWORD, the (keyword (snd (the c))))
   1.338 +		    else c
   1.339 +		end
   1.340 +		
   1.341 +	fun readToken () = readToken_helper2 ()
   1.342 +	    			   
   1.343 +	fun pushToken a = rest := (a::(!rest))
   1.344 +	    
   1.345 +	fun is_value token = 
   1.346 +	    fst token = TOKEN_NUM orelse (fst token = TOKEN_KEYWORD 
   1.347 +					  andalso snd token = "INF")	
   1.348 +
   1.349 +        fun get_value token = 
   1.350 +	    if fst token = TOKEN_NUM then
   1.351 +		cplexNum (snd token)
   1.352 +	    else if fst token = TOKEN_KEYWORD andalso snd token = "INF" 
   1.353 +	    then
   1.354 +		cplexInf
   1.355 +	    else
   1.356 +		raise (Load_cplexFile "num expected")
   1.357 +					    
   1.358 +	fun readTerm_Product only_num = 
   1.359 +	    let val c = readToken () in
   1.360 +		if c = None then None
   1.361 +		else if fst (the c) = TOKEN_SYMBOL 
   1.362 +		then (
   1.363 +		    if only_num then (pushToken (the c); None) 
   1.364 +		    else Some (cplexVar (snd (the c)))
   1.365 +		    ) 
   1.366 +		else if only_num andalso is_value (the c) then
   1.367 +		    Some (get_value (the c))
   1.368 +		else if is_value (the c) then  
   1.369 +		    let val t1 = get_value (the c) 
   1.370 +			val d = readToken () 
   1.371 +		    in
   1.372 +			if d = None then Some t1 
   1.373 +			else if fst (the d) = TOKEN_SYMBOL then 
   1.374 +			    Some (cplexProd (t1, cplexVar (snd (the d))))
   1.375 +			else
   1.376 +			    (pushToken (the d); Some t1)
   1.377 +		    end
   1.378 +		else (pushToken (the c); None)
   1.379 +	    end
   1.380 +	    
   1.381 +	fun readTerm_Signed only_signed only_num = 
   1.382 +	    let
   1.383 +		val c = readToken ()
   1.384 +	    in
   1.385 +		if c = None then None 
   1.386 +		else 
   1.387 +		    let val d = the c in 
   1.388 +			if d = (TOKEN_DELIMITER, "+") then 
   1.389 +			    readTerm_Product only_num
   1.390 +			 else if d = (TOKEN_DELIMITER, "-") then 
   1.391 +			     Some (cplexNeg (the (readTerm_Product 
   1.392 +						      only_num)))
   1.393 +			 else (pushToken d; 
   1.394 +			       if only_signed then None 
   1.395 +			       else readTerm_Product only_num)
   1.396 +		    end
   1.397 +	    end
   1.398 +    
   1.399 +	fun readTerm_Sum first_signed = 
   1.400 +	    let val c = readTerm_Signed first_signed false in
   1.401 +		if c = None then [] else (the c)::(readTerm_Sum true)
   1.402 +	    end
   1.403 +	    
   1.404 +	fun readTerm () = 
   1.405 +	    let val c = readTerm_Sum false in
   1.406 +		if c = [] then None 
   1.407 +		else if tl c = [] then Some (hd c)
   1.408 +		else Some (cplexSum c) 
   1.409 +	    end
   1.410 +	    
   1.411 +	fun readLabeledTerm () = 
   1.412 +	    let val c = readToken () in
   1.413 +		if c = None then (None, None) 
   1.414 +		else if fst (the c) = TOKEN_LABEL then 
   1.415 +		    let val t = readTerm () in
   1.416 +			if t = None then 
   1.417 +			    raise (Load_cplexFile ("term after label "^
   1.418 +						   (snd (the c))^
   1.419 +						   " expected"))
   1.420 +			else (Some (snd (the c)), t)
   1.421 +		    end
   1.422 +		else (pushToken (the c); (None, readTerm ()))
   1.423 +	    end
   1.424 +            
   1.425 +	fun readGoal () = 
   1.426 +	    let 
   1.427 +		val g = readToken ()
   1.428 +	    in
   1.429 +    		if g = Some (TOKEN_KEYWORD, "MAXIMIZE") then 
   1.430 +		    cplexMaximize (the (snd (readLabeledTerm ()))) 
   1.431 +		else if g = Some (TOKEN_KEYWORD, "MINIMIZE") then 
   1.432 +		    cplexMinimize (the (snd (readLabeledTerm ())))
   1.433 +		else raise (Load_cplexFile "MAXIMIZE or MINIMIZE expected")
   1.434 +	    end
   1.435 +	    
   1.436 +	fun str2cmp b = 
   1.437 +	    (case b of 
   1.438 +		 "<" => cplexLe 
   1.439 +	       | "<=" => cplexLeq 
   1.440 +	       | ">" => cplexGe 
   1.441 +	       | ">=" => cplexGeq 
   1.442 +               | "=" => cplexEq
   1.443 +	       | _ => raise (Load_cplexFile (b^" is no TOKEN_CMP")))
   1.444 +			    
   1.445 +	fun readConstraint () = 
   1.446 +            let 
   1.447 +		val t = readLabeledTerm () 
   1.448 +		fun make_constraint b t1 t2 =
   1.449 +                    cplexConstr 
   1.450 +			(str2cmp b,
   1.451 +			 (t1, t2))		
   1.452 +	    in
   1.453 +		if snd t = None then None
   1.454 +		else 
   1.455 +		    let val c = readToken () in
   1.456 +			if c = None orelse fst (the c) <> TOKEN_CMP 
   1.457 +			then raise (Load_cplexFile "TOKEN_CMP expected")
   1.458 +			else 
   1.459 +			    let val n = readTerm_Signed false true in
   1.460 +				if n = None then 
   1.461 +				    raise (Load_cplexFile "num expected")
   1.462 +				else
   1.463 +				    Some (fst t,
   1.464 +					  make_constraint (snd (the c)) 
   1.465 +							  (the (snd t)) 
   1.466 +							  (the n))
   1.467 +			    end
   1.468 +		    end            
   1.469 +	    end
   1.470 +        
   1.471 +        fun readST () = 
   1.472 +	    let 
   1.473 +		fun readbody () = 
   1.474 +		    let val t = readConstraint () in
   1.475 +			if t = None then []
   1.476 +			else if (is_normed_Constr (snd (the t))) then
   1.477 +			    (the t)::(readbody ())
   1.478 +			else if (fst (the t) <> None) then 
   1.479 +			    raise (Load_cplexFile 
   1.480 +				       ("constraint '"^(the (fst (the t)))^ 
   1.481 +					"'is not normed"))
   1.482 +			else
   1.483 +			    raise (Load_cplexFile 
   1.484 +				       "constraint is not normed")
   1.485 +		    end
   1.486 +	    in    		
   1.487 +		if readToken () = Some (TOKEN_KEYWORD, "ST") 
   1.488 +		then 
   1.489 +		    readbody ()
   1.490 +		else 
   1.491 +		    raise (Load_cplexFile "ST expected")
   1.492 +	    end
   1.493 +	    
   1.494 +	fun readCmp () = 
   1.495 +	    let val c = readToken () in
   1.496 +		if c = None then None
   1.497 +		else if fst (the c) = TOKEN_CMP then 
   1.498 +		    Some (str2cmp (snd (the c)))
   1.499 +		else (pushToken (the c); None)
   1.500 +	    end
   1.501 +	    
   1.502 +	fun skip_NL () =
   1.503 +	    let val c = readToken () in
   1.504 +		if c <> None andalso fst (the c) = TOKEN_NL then
   1.505 +		    skip_NL ()
   1.506 +		else
   1.507 +		    (pushToken (the c); ())
   1.508 +	    end
   1.509 +
   1.510 +	fun is_var (cplexVar _) = true
   1.511 +	  | is_var _ = false
   1.512 +	    
   1.513 +	fun make_bounds c t1 t2 = 
   1.514 +	    cplexBound (t1, c, t2)
   1.515 +
   1.516 +	fun readBound () = 	    
   1.517 +	    let 		
   1.518 +		val _ = skip_NL ()
   1.519 +		val t1 = readTerm ()
   1.520 +	    in
   1.521 +		if t1 = None then None 
   1.522 +		else 
   1.523 +		    let 
   1.524 +			val c1 = readCmp () 
   1.525 +		    in
   1.526 +			if c1 = None then
   1.527 +			    let 
   1.528 +				val c = readToken () 
   1.529 +			    in
   1.530 +				if c = Some (TOKEN_KEYWORD, "FREE") then
   1.531 +				    Some (
   1.532 +				    cplexBounds (cplexNeg cplexInf,
   1.533 +						 cplexLeq,
   1.534 +						 the t1,
   1.535 +						 cplexLeq,
   1.536 +						 cplexInf))
   1.537 +				else
   1.538 +				    raise (Load_cplexFile "FREE expected")
   1.539 +			    end
   1.540 +			else
   1.541 +			    let 
   1.542 +				val t2 = readTerm () 
   1.543 +			    in
   1.544 +				if t2 = None then
   1.545 +				    raise (Load_cplexFile "term expected")
   1.546 +				else
   1.547 +				    let val c2 = readCmp () in
   1.548 +					if c2 = None then
   1.549 +					    Some (make_bounds (the c1) 
   1.550 +							      (the t1)
   1.551 +							      (the t2))
   1.552 +					else
   1.553 +					    Some (
   1.554 +					    cplexBounds (the t1,
   1.555 +							 the c1,
   1.556 +							 the t2,
   1.557 +							 the c2,
   1.558 +							 the (readTerm())))
   1.559 +				    end
   1.560 +			    end
   1.561 +		    end
   1.562 +	    end
   1.563 +	    
   1.564 +	fun readBounds () =
   1.565 +	    let 
   1.566 +		fun makestring b = "?"
   1.567 +		fun readbody () = 
   1.568 +		    let 
   1.569 +			val b = readBound ()
   1.570 +		    in
   1.571 +			if b = None then []
   1.572 +			else if (is_normed_Bounds (the b)) then
   1.573 +			    (the b)::(readbody())
   1.574 +			else (
   1.575 +			    raise (Load_cplexFile 
   1.576 +				       ("bounds are not normed in: "^
   1.577 +					(makestring (the b)))))
   1.578 +		    end
   1.579 +	    in
   1.580 +		if readToken () = Some (TOKEN_KEYWORD, "BOUNDS") then 
   1.581 +		    readbody ()
   1.582 +		else raise (Load_cplexFile "BOUNDS expected")
   1.583 +	    end
   1.584 +
   1.585 +        fun readEnd () = 
   1.586 +	    if readToken () = Some (TOKEN_KEYWORD, "END") then ()
   1.587 +	    else raise (Load_cplexFile "END expected")
   1.588 +		    
   1.589 +	val result_Goal = readGoal ()  
   1.590 +	val result_ST = readST ()  
   1.591 +	val _ =	ignore_NL := false 
   1.592 +        val result_Bounds = readBounds ()
   1.593 +        val _ = ignore_NL := true
   1.594 +        val _ = readEnd ()
   1.595 +	val _ = TextIO.closeIn f
   1.596 +    in
   1.597 +	cplexProg (name, result_Goal, result_ST, result_Bounds)
   1.598 +    end
   1.599 +
   1.600 +fun save_cplexFile filename (cplexProg (name, goal, constraints, bounds)) =
   1.601 +    let
   1.602 +	val f = TextIO.openOut filename
   1.603 +	
   1.604 +	fun basic_write s = TextIO.output(f, s)
   1.605 +
   1.606 +	val linebuf = ref ""
   1.607 +	fun buf_flushline s = 
   1.608 +	    (basic_write (!linebuf); 
   1.609 +	     basic_write "\n";
   1.610 +	     linebuf := s)
   1.611 +	fun buf_add s = linebuf := (!linebuf) ^ s
   1.612 +
   1.613 +	fun write s = 
   1.614 +	    if (String.size s) + (String.size (!linebuf)) >= 250 then 
   1.615 +		buf_flushline ("    "^s)
   1.616 +	    else 
   1.617 +		buf_add s
   1.618 +
   1.619 +        fun writeln s = (buf_add s; buf_flushline "")
   1.620 +        
   1.621 +	fun write_term (cplexVar x) = write x
   1.622 +	  | write_term (cplexNum x) = write x
   1.623 +	  | write_term cplexInf = write "inf"
   1.624 +	  | write_term (cplexProd (cplexNum "1", b)) = write_term b
   1.625 +	  | write_term (cplexProd (a, b)) = 
   1.626 +	    (write_term a; write " "; write_term b)
   1.627 +          | write_term (cplexNeg x) = (write " - "; write_term x)
   1.628 +          | write_term (cplexSum ts) = write_terms ts
   1.629 +	and write_terms [] = ()
   1.630 +	  | write_terms (t::ts) = 
   1.631 +	    (if (not (is_Neg t)) then write " + " else (); 
   1.632 +	     write_term t; write_terms ts)
   1.633 +
   1.634 +	fun write_goal (cplexMaximize term) = 
   1.635 +	    (writeln "MAXIMIZE"; write_term term; writeln "")
   1.636 +	  | write_goal (cplexMinimize term) = 
   1.637 +	    (writeln "MINIMIZE"; write_term term; writeln "")
   1.638 +
   1.639 +	fun write_cmp cplexLe = write "<"
   1.640 +	  | write_cmp cplexLeq = write "<="
   1.641 +	  | write_cmp cplexEq = write "="
   1.642 +	  | write_cmp cplexGe = write ">"
   1.643 +	  | write_cmp cplexGeq = write ">="
   1.644 +        
   1.645 +	fun write_constr (cplexConstr (cmp, (a,b))) = 
   1.646 +	    (write_term a;
   1.647 +	     write " ";
   1.648 +	     write_cmp cmp;
   1.649 +	     write " ";
   1.650 +	     write_term b)
   1.651 +        
   1.652 +	fun write_constraints [] = ()
   1.653 +	  | write_constraints (c::cs) = 
   1.654 +	    (if (fst c <> None) 
   1.655 +	     then 
   1.656 +		 (write (the (fst c)); write ": ") 
   1.657 +	     else 
   1.658 +		 ();
   1.659 +	     write_constr (snd c);
   1.660 +	     writeln "";
   1.661 +	     write_constraints cs)
   1.662 +
   1.663 +	fun write_bounds [] = ()
   1.664 +	  | write_bounds ((cplexBounds (t1,c1,t2,c2,t3))::bs) =
   1.665 +	    ((if t1 = cplexNeg cplexInf andalso t3 = cplexInf
   1.666 +		 andalso (c1 = cplexLeq orelse c1 = cplexLe) 
   1.667 +		 andalso (c2 = cplexLeq orelse c2 = cplexLe) 
   1.668 +	      then
   1.669 +		  (write_term t2; write " free")
   1.670 +	      else		 		 
   1.671 +		  (write_term t1; write " "; write_cmp c1; write " ";
   1.672 +		   write_term t2; write " "; write_cmp c2; write " ";
   1.673 +		   write_term t3)
   1.674 +	     ); writeln ""; write_bounds bs)
   1.675 +	  | write_bounds ((cplexBound (t1, c, t2)) :: bs) = 
   1.676 +	    (write_term t1; write " "; 
   1.677 +	     write_cmp c; write " ";
   1.678 +	     write_term t2; writeln ""; write_bounds bs)
   1.679 +	     
   1.680 +	val _ = write_goal goal
   1.681 +        val _ = (writeln ""; writeln "ST")
   1.682 +	val _ = write_constraints constraints
   1.683 +        val _ = (writeln ""; writeln "BOUNDS")
   1.684 +	val _ = write_bounds bounds
   1.685 +        val _ = (writeln ""; writeln "END") 
   1.686 +        val _ = TextIO.closeOut f
   1.687 +    in
   1.688 +	()
   1.689 +    end
   1.690 +
   1.691 +fun norm_Constr (constr as cplexConstr (c, (t1, t2))) = 
   1.692 +    if not (modulo_signed is_Num t2) andalso  
   1.693 +       modulo_signed is_Num t1 
   1.694 +    then
   1.695 +	[cplexConstr (rev_cmp c, (t2, t1))]
   1.696 +    else if (c = cplexLe orelse c = cplexLeq) andalso
   1.697 +	    (t1 = (cplexNeg cplexInf) orelse t2 = cplexInf)	    
   1.698 +    then 
   1.699 +	[]
   1.700 +    else if (c = cplexGe orelse c = cplexGeq) andalso
   1.701 +	    (t1 = cplexInf orelse t2 = cplexNeg cplexInf)
   1.702 +    then
   1.703 +	[]
   1.704 +    else
   1.705 +	[constr]
   1.706 +
   1.707 +fun bound2constr (cplexBounds (t1,c1,t2,c2,t3)) =
   1.708 +    (norm_Constr(cplexConstr (c1, (t1, t2))))
   1.709 +    @ (norm_Constr(cplexConstr (c2, (t2, t3))))
   1.710 +  | bound2constr (cplexBound (t1, cplexEq, t2)) =
   1.711 +    (norm_Constr(cplexConstr (cplexLeq, (t1, t2))))
   1.712 +    @ (norm_Constr(cplexConstr (cplexLeq, (t2, t1))))
   1.713 +  | bound2constr (cplexBound (t1, c1, t2)) = 
   1.714 +    norm_Constr(cplexConstr (c1, (t1,t2)))
   1.715 +
   1.716 +val emptyset = Symtab.empty
   1.717 +
   1.718 +fun singleton v = Symtab.update ((v, ()), emptyset)
   1.719 +
   1.720 +fun merge a b = Symtab.merge (op =) (a, b)
   1.721 +
   1.722 +fun mergemap f ts = foldl
   1.723 +			(fn (table, x) => merge table (f x))
   1.724 +			(Symtab.empty, ts)
   1.725 +
   1.726 +fun diff a b = Symtab.foldl (fn (a, (k,v)) => 
   1.727 +			 (Symtab.delete k a) handle UNDEF => a) 
   1.728 +		     (a, b)
   1.729 +		    
   1.730 +fun collect_vars (cplexVar v) = singleton v
   1.731 +  | collect_vars (cplexNeg t) = collect_vars t
   1.732 +  | collect_vars (cplexProd (t1, t2)) = 
   1.733 +    merge (collect_vars t1) (collect_vars t2)
   1.734 +  | collect_vars (cplexSum ts) = mergemap collect_vars ts
   1.735 +  | collect_vars _ = emptyset
   1.736 +
   1.737 +(* Eliminates all nonfree bounds from the linear program and produces an
   1.738 +   equivalent program with only free bounds 
   1.739 +   IF for the input program P holds: is_normed_cplexProg P *)
   1.740 +fun elim_nonfree_bounds (cplexProg (name, goal, constraints, bounds)) =
   1.741 +    let
   1.742 +	fun collect_constr_vars (_, cplexConstr (c, (t1,_))) =
   1.743 +	    (collect_vars t1)   
   1.744 +	
   1.745 +	val cvars = merge (collect_vars (term_of_goal goal)) 
   1.746 +			  (mergemap collect_constr_vars constraints)         
   1.747 +		    
   1.748 +	fun collect_lower_bounded_vars 
   1.749 +	    (cplexBounds (t1, c1, cplexVar v, c2, t3)) =
   1.750 +	    singleton v
   1.751 +	  |  collect_lower_bounded_vars 
   1.752 +		 (cplexBound (_, cplexLe, cplexVar v)) =
   1.753 +	     singleton v
   1.754 +	  |  collect_lower_bounded_vars 
   1.755 +		 (cplexBound (_, cplexLeq, cplexVar v)) = 
   1.756 +	     singleton v
   1.757 +	  |  collect_lower_bounded_vars 
   1.758 +		 (cplexBound (cplexVar v, cplexGe,_)) = 
   1.759 +	     singleton v
   1.760 +	  |  collect_lower_bounded_vars 
   1.761 +		 (cplexBound (cplexVar v, cplexGeq, _)) = 
   1.762 +	     singleton v
   1.763 +	  | collect_lower_bounded_vars
   1.764 +	    (cplexBound (cplexVar v, cplexEq, _)) = 
   1.765 +	    singleton v
   1.766 +	  |  collect_lower_bounded_vars _ = emptyset
   1.767 +	
   1.768 +	val lvars = mergemap collect_lower_bounded_vars bounds        
   1.769 +	val positive_vars = diff cvars lvars			   
   1.770 +	val zero = cplexNum "0"
   1.771 +	
   1.772 +	fun make_pos_constr v = 
   1.773 +	    (None, cplexConstr (cplexGeq, ((cplexVar v), zero)))
   1.774 +	
   1.775 +	fun make_free_bound v = 
   1.776 +	    cplexBounds (cplexNeg cplexInf, cplexLeq, 
   1.777 +			 cplexVar v, cplexLeq,
   1.778 +			 cplexInf)
   1.779 +	
   1.780 +	val pos_constrs = rev(Symtab.foldl 
   1.781 +			      (fn (l, (k,v)) => (make_pos_constr k) :: l)
   1.782 +			      ([], positive_vars))
   1.783 +        val bound_constrs = map (fn x => (None, x)) 
   1.784 +				(flat (map bound2constr bounds))
   1.785 +	val constraints' = constraints @ pos_constrs @ bound_constrs	   
   1.786 +	val bounds' = rev(Symtab.foldl (fn (l, (v,_)) => 
   1.787 +					   (make_free_bound v)::l)
   1.788 +				       ([], cvars))			  
   1.789 +    in
   1.790 +	cplexProg (name, goal, constraints', bounds')
   1.791 +    end
   1.792 +
   1.793 +fun relax_strict_ineqs (cplexProg (name, goals, constrs, bounds)) = 
   1.794 +    let
   1.795 +	fun relax cplexLe = cplexLeq
   1.796 +	  | relax cplexGe = cplexGeq
   1.797 +	  | relax x = x
   1.798 +	
   1.799 +	fun relax_constr (n, cplexConstr(c, (t1, t2))) = 
   1.800 +	    (n, cplexConstr(relax c, (t1, t2)))
   1.801 +	    
   1.802 +	fun relax_bounds (cplexBounds (t1, c1, t2, c2, t3)) = 
   1.803 +	    cplexBounds (t1, relax c1, t2, relax c2, t3)
   1.804 +	  | relax_bounds (cplexBound (t1, c, t2)) = 
   1.805 +	    cplexBound (t1, relax c, t2)
   1.806 +    in
   1.807 +	cplexProg (name, 
   1.808 +		   goals, 
   1.809 +		   map relax_constr constrs, 
   1.810 +		   map relax_bounds bounds)
   1.811 +    end
   1.812 +
   1.813 +datatype cplexResult = Unbounded 
   1.814 +		     | Infeasible 
   1.815 +		     | Undefined
   1.816 +		     | Optimal of string * ((string * string) list)
   1.817 +
   1.818 +fun is_separator x = forall (fn c => c = #"-") (String.explode x)
   1.819 +
   1.820 +fun is_sign x = (x = "+" orelse x = "-")
   1.821 +
   1.822 +fun is_colon x = (x = ":")
   1.823 +
   1.824 +fun is_resultsymbol a = 
   1.825 +    let
   1.826 +	val symbol_char = String.explode "!\"#$%&()/,.;?@_`'{}|~-"
   1.827 +	fun is_symbol_char c = Char.isAlphaNum c orelse 
   1.828 +			       exists (fn d => d=c) symbol_char
   1.829 +	fun is_symbol_start c = is_symbol_char c andalso 
   1.830 +				not (Char.isDigit c) andalso 
   1.831 +				not (c= #".") andalso
   1.832 +				not (c= #"-")
   1.833 +	val b = String.explode a
   1.834 +    in
   1.835 +	b <> [] andalso is_symbol_start (hd b) andalso 
   1.836 +	forall is_symbol_char b
   1.837 +    end
   1.838 +
   1.839 +val TOKEN_SIGN = 100
   1.840 +val TOKEN_COLON = 101
   1.841 +val TOKEN_SEPARATOR = 102
   1.842 +
   1.843 +fun load_cplexResult name = 
   1.844 +    let
   1.845 +	val flist = [(is_NL, TOKEN_NL), 
   1.846 +		     (is_blank, TOKEN_BLANK),
   1.847 +		     (is_num, TOKEN_NUM),
   1.848 +		     (is_sign, TOKEN_SIGN),
   1.849 +                     (is_colon, TOKEN_COLON),
   1.850 +		     (is_cmp, TOKEN_CMP),
   1.851 +		     (is_resultsymbol, TOKEN_SYMBOL),
   1.852 +		     (is_separator, TOKEN_SEPARATOR)]
   1.853 +
   1.854 +	val tokenize = tokenize_general flist
   1.855 +
   1.856 +	val f = TextIO.openIn name  
   1.857 +
   1.858 +	val rest = ref []
   1.859 +		   
   1.860 +	fun readToken_helper () =
   1.861 +	    if length (!rest) > 0 then  
   1.862 +		let val u = hd (!rest) in 
   1.863 +		    (
   1.864 +		     rest := tl (!rest); 
   1.865 +		     Some u
   1.866 +		    ) 
   1.867 +		end
   1.868 +	    else 
   1.869 +		let val s = TextIO.inputLine f in
   1.870 +		    if s = "" then None else (rest := tokenize s; readToken_helper())					     
   1.871 +		end           
   1.872 +		
   1.873 +	fun is_tt tok ty = (tok <> None andalso (fst (the tok)) = ty)
   1.874 +
   1.875 +	fun pushToken a = if a = None then () else (rest := ((the a)::(!rest)))
   1.876 +	
   1.877 +	fun readToken () =
   1.878 +	    let val t = readToken_helper () in
   1.879 +		if is_tt t TOKEN_BLANK then 
   1.880 +		    readToken ()
   1.881 +		else if is_tt t TOKEN_NL then 
   1.882 +		    let val t2 = readToken_helper () in
   1.883 +			if is_tt t2 TOKEN_SIGN then 
   1.884 +			    (pushToken (Some (TOKEN_SEPARATOR, "-")); t)
   1.885 +			else 
   1.886 +			    (pushToken t2; t)
   1.887 +		    end
   1.888 +		else if is_tt t TOKEN_SIGN then
   1.889 +		    let val t2 = readToken_helper () in
   1.890 +			if is_tt t2 TOKEN_NUM then
   1.891 +			    (Some (TOKEN_NUM, (snd (the t))^(snd (the t2))))
   1.892 +			else
   1.893 +			    (pushToken t2; t)
   1.894 +		    end
   1.895 +		else
   1.896 +		    t
   1.897 +	    end	    		
   1.898 +
   1.899 +        fun readRestOfLine P = 
   1.900 +	    let 
   1.901 +		val t = readToken ()
   1.902 +	    in
   1.903 +		if is_tt t TOKEN_NL orelse t = None 
   1.904 +		then P
   1.905 +		else readRestOfLine P
   1.906 +	    end			
   1.907 +							 
   1.908 +	fun readHeader () = 
   1.909 +	    let
   1.910 +		fun readStatus () = readRestOfLine ("STATUS", snd (the (readToken ())))
   1.911 +		fun readObjective () = readRestOfLine ("OBJECTIVE", snd (the (readToken (); readToken (); readToken ())))
   1.912 +		val t1 = readToken ()
   1.913 +		val t2 = readToken ()
   1.914 +	    in
   1.915 +		if is_tt t1 TOKEN_SYMBOL andalso is_tt t2 TOKEN_COLON 
   1.916 +		then
   1.917 +		    case to_upper (snd (the t1)) of
   1.918 +			"STATUS" => (readStatus ())::(readHeader ())
   1.919 +		      | "OBJECTIVE" => (readObjective())::(readHeader ())
   1.920 +		      | _ => (readRestOfLine (); readHeader ())
   1.921 +		else
   1.922 +		    (pushToken t2; pushToken t1; [])
   1.923 +	    end
   1.924 +
   1.925 +	fun skip_until_sep () = 
   1.926 +	    let val x = readToken () in
   1.927 +		if is_tt x TOKEN_SEPARATOR then
   1.928 +		    readRestOfLine ()
   1.929 +		else 
   1.930 +		    skip_until_sep ()
   1.931 +	    end
   1.932 +
   1.933 +	fun load_value () =
   1.934 +	    let 
   1.935 +		val t1 = readToken ()
   1.936 +		val t2 = readToken ()
   1.937 +	    in
   1.938 +		if is_tt t1 TOKEN_NUM andalso is_tt t2 TOKEN_SYMBOL then
   1.939 +		    let 
   1.940 +			val t = readToken ()
   1.941 +			val state = if is_tt t TOKEN_NL then readToken () else t
   1.942 +			val _ = if is_tt state TOKEN_SYMBOL then () else raise (Load_cplexResult "state expected")
   1.943 +			val k = readToken ()
   1.944 +		    in
   1.945 +			if is_tt k TOKEN_NUM then
   1.946 +			    readRestOfLine (Some (snd (the t2), snd (the k)))
   1.947 +			else
   1.948 +			    raise (Load_cplexResult "number expected")
   1.949 +		    end				
   1.950 +		else
   1.951 +		    (pushToken t2; pushToken t1; None)
   1.952 +	    end
   1.953 +
   1.954 +	fun load_values () = 
   1.955 +	    let val v = load_value () in
   1.956 +		if v = None then [] else (the v)::(load_values ())
   1.957 +	    end
   1.958 +	
   1.959 +	val header = readHeader () 
   1.960 +
   1.961 +	val result = 
   1.962 +	    case assoc (header, "STATUS") of
   1.963 +		Some "INFEASIBLE" => Infeasible
   1.964 +	      | Some "UNBOUNDED" => Unbounded
   1.965 +	      | Some "OPTIMAL" => Optimal (the (assoc (header, "OBJECTIVE")), 
   1.966 +					   (skip_until_sep (); 
   1.967 +					    skip_until_sep ();
   1.968 +					    load_values ()))
   1.969 +	      | _ => Undefined
   1.970 +
   1.971 +	val _ = TextIO.closeIn f
   1.972 +    in
   1.973 +	result
   1.974 +    end
   1.975 +    handle (Tokenize s) => raise (Load_cplexResult ("Tokenize: "^s))
   1.976 +	 | OPTION => raise (Load_cplexResult "OPTION")
   1.977 +	 | x => raise x
   1.978 +
   1.979 +exception Execute of string;
   1.980 +
   1.981 +fun execute_cplex lpname resultname = 
   1.982 +let
   1.983 +    fun wrap s = "\""^s^"\""
   1.984 +    val cplex_path = getenv "CPLEX"
   1.985 +    val cplex = if cplex_path = "" then "glpsol" else cplex_path
   1.986 +    val command = (wrap cplex)^" --lpt "^(wrap lpname)^" --output "^(wrap resultname)
   1.987 +in
   1.988 +    execute command
   1.989 +end
   1.990 +
   1.991 +fun tmp_file s = Path.pack (Path.expand (File.tmp_path (Path.make [s])))
   1.992 +
   1.993 +fun solve prog =
   1.994 +    let 
   1.995 +	val name = LargeInt.toString (Time.toMicroseconds (Time.now ()))
   1.996 +	val lpname = tmp_file (name^".lp")
   1.997 +	val resultname = tmp_file (name^".result")
   1.998 +	val _ = save_cplexFile lpname prog
   1.999 +	val answer = execute_cplex lpname resultname
  1.1000 +    in
  1.1001 +	let
  1.1002 +	    val result = load_cplexResult resultname
  1.1003 +	    val _ = OS.FileSys.remove lpname
  1.1004 +	    val _ = OS.FileSys.remove resultname
  1.1005 +	in
  1.1006 +	    result
  1.1007 +	end 
  1.1008 +	handle (Load_cplexResult s) => raise (Execute ("Load_cplexResult: "^s^"\nExecute: "^answer))
  1.1009 +	     | _ => raise (Execute answer)
  1.1010 +    end			     
  1.1011 +end;
  1.1012 +
  1.1013 +val demofile = "/home/obua/flyspeck/kepler/LP/cplexPent2.lp45"
  1.1014 +val demoout = "/home/obua/flyspeck/kepler/LP/test.out"
  1.1015 +val demoresult = "/home/obua/flyspeck/kepler/LP/try/test2.sol"
  1.1016 +	   
  1.1017 +fun loadcplex () = Cplex.relax_strict_ineqs 
  1.1018 +		   (Cplex.load_cplexFile demofile)
  1.1019 +
  1.1020 +fun writecplex lp = Cplex.save_cplexFile demoout lp
  1.1021 +
  1.1022 +fun test () = 
  1.1023 +    let
  1.1024 +	val lp = loadcplex ()
  1.1025 +	val lp2 = Cplex.elim_nonfree_bounds lp
  1.1026 +    in
  1.1027 +	writecplex lp2
  1.1028 +    end
  1.1029 +
  1.1030 +fun loadresult () = Cplex.load_cplexResult demoresult;