src/HOL/Matrix/cplex/Cplex_tools.ML

1. changed configuration variables for linear programming (Cplex_tools):
LP_SOLVER is either CPLEX or GLPK
CPLEX_PATH is the path to the cplex binary
GLPK_PATH is the path to the glpk binary
The change makes it possible to switch between glpk and cplex at runtime.
2. moved conflicting list theories out of Library.thy into ROOT.ML

(*  Title:      HOL/Matrix/cplex/Cplex_tools.ML
    ID:         $Id$
    Author:     Steven Obua
*)

signature CPLEX =
sig
    
    datatype cplexTerm = cplexVar of string | cplexNum of string | cplexInf 
                       | cplexNeg of cplexTerm 
                       | cplexProd of cplexTerm * cplexTerm 
                       | cplexSum of (cplexTerm list) 
    
    datatype cplexComp = cplexLe | cplexLeq | cplexEq | cplexGe | cplexGeq 
								  
    datatype cplexGoal = cplexMinimize of cplexTerm 
		       | cplexMaximize of cplexTerm
					  
    datatype cplexConstr = cplexConstr of cplexComp * 
					  (cplexTerm * cplexTerm)
					  
    datatype cplexBounds = cplexBounds of cplexTerm * cplexComp * cplexTerm 
					  * cplexComp * cplexTerm
			 | cplexBound of cplexTerm * cplexComp * cplexTerm
					 
    datatype cplexProg = cplexProg of string 
				      * cplexGoal 
				      * ((string option * cplexConstr) 
					     list) 
				      * cplexBounds list
				      
    datatype cplexResult = Unbounded 
			 | Infeasible 
			 | Undefined
			 | Optimal of string * 
				      (((* name *) string * 
					(* value *) string) list)

    datatype cplexSolver = SOLVER_DEFAULT | SOLVER_CPLEX | SOLVER_GLPK
						     
    exception Load_cplexFile of string
    exception Load_cplexResult of string
    exception Save_cplexFile of string
    exception Execute of string

    val load_cplexFile : string -> cplexProg

    val save_cplexFile : string -> cplexProg -> unit 

    val elim_nonfree_bounds : cplexProg -> cplexProg

    val relax_strict_ineqs : cplexProg -> cplexProg

    val is_normed_cplexProg : cplexProg -> bool

    val get_solver : unit -> cplexSolver
    val set_solver : cplexSolver -> unit
    val solve : cplexProg -> cplexResult
end;

structure Cplex  : CPLEX =
struct

datatype cplexSolver = SOLVER_DEFAULT | SOLVER_CPLEX | SOLVER_GLPK

val cplexsolver = ref SOLVER_DEFAULT;
fun get_solver () = !cplexsolver;
fun set_solver s = (cplexsolver := s);

exception Load_cplexFile of string;
exception Load_cplexResult of string;
exception Save_cplexFile of string;
	  
datatype cplexTerm = cplexVar of string 
		   | cplexNum of string 
		   | cplexInf 
                   | cplexNeg of cplexTerm 
                   | cplexProd of cplexTerm * cplexTerm 
                   | cplexSum of (cplexTerm list) 
datatype cplexComp = cplexLe | cplexLeq | cplexEq | cplexGe | cplexGeq 
datatype cplexGoal = cplexMinimize of cplexTerm | cplexMaximize of cplexTerm
datatype cplexConstr = cplexConstr of cplexComp * (cplexTerm * cplexTerm)
datatype cplexBounds = cplexBounds of cplexTerm * cplexComp * cplexTerm 
				      * cplexComp * cplexTerm
                     | cplexBound of cplexTerm * cplexComp * cplexTerm 
datatype cplexProg = cplexProg of string 
				  * cplexGoal 
				  * ((string option * cplexConstr) list) 
				  * cplexBounds list
				  
fun rev_cmp cplexLe = cplexGe
  | rev_cmp cplexLeq = cplexGeq
  | rev_cmp cplexGe = cplexLe
  | rev_cmp cplexGeq = cplexLeq
  | rev_cmp cplexEq = cplexEq

fun the NONE = raise (Load_cplexFile "SOME expected")
  | the (SOME x) = x; 
    
fun modulo_signed is_something (cplexNeg u) = is_something u
  | modulo_signed is_something u = is_something u

fun is_Num (cplexNum _) = true
  | is_Num _ = false

fun is_Inf cplexInf = true
  | is_Inf _ = false

fun is_Var (cplexVar _) = true
  | is_Var _ = false

fun is_Neg (cplexNeg x ) = true
  | is_Neg _ = false

fun is_normed_Prod (cplexProd (t1, t2)) = 
    (is_Num t1) andalso (is_Var t2)
  | is_normed_Prod x = is_Var x

fun is_normed_Sum (cplexSum ts) = 
    (ts <> []) andalso forall (modulo_signed is_normed_Prod) ts
  | is_normed_Sum x = modulo_signed is_normed_Prod x

fun is_normed_Constr (cplexConstr (c, (t1, t2))) = 
    (is_normed_Sum t1) andalso (modulo_signed is_Num t2)

fun is_Num_or_Inf x = is_Inf x orelse is_Num x

fun is_normed_Bounds (cplexBounds (t1, c1, t2, c2, t3)) =
    (c1 = cplexLe orelse c1 = cplexLeq) andalso 
    (c2 = cplexLe orelse c2 = cplexLeq) andalso
    is_Var t2 andalso
    modulo_signed is_Num_or_Inf t1 andalso
    modulo_signed is_Num_or_Inf t3
  | is_normed_Bounds (cplexBound (t1, c, t2)) =
    (is_Var t1 andalso (modulo_signed is_Num_or_Inf t2)) 
    orelse
    (c <> cplexEq andalso 
     is_Var t2 andalso (modulo_signed is_Num_or_Inf t1))
	             		
fun term_of_goal (cplexMinimize x) = x
  | term_of_goal (cplexMaximize x) = x

fun is_normed_cplexProg (cplexProg (name, goal, constraints, bounds)) = 
    is_normed_Sum (term_of_goal goal) andalso
    forall (fn (_,x) => is_normed_Constr x) constraints andalso
    forall is_normed_Bounds bounds

fun is_NL s = s = "\n"

fun is_blank s = forall (fn c => c <> #"\n" andalso Char.isSpace c) (String.explode s)
		 
fun is_num a = 
    let 
	val b = String.explode a 
	fun num4 cs = forall Char.isDigit cs		      
	fun num3 [] = true
	  | num3 (ds as (c::cs)) = 
	    if c = #"+" orelse c = #"-" then
		num4 cs
	    else 
		num4 ds		    
	fun num2 [] = true
	  | num2 (c::cs) =
	    if c = #"e" orelse c = #"E" then num3 cs
	    else (Char.isDigit c) andalso num2 cs			 
	fun num1 [] = true
	  | num1 (c::cs) = 
	    if c = #"." then num2 cs 
	    else if c = #"e" orelse c = #"E" then num3 cs 
	    else (Char.isDigit c) andalso num1 cs
	fun num [] = true
	  | num (c::cs) = 
	    if c = #"." then num2 cs 
	    else (Char.isDigit c) andalso num1 cs
    in
	num b
    end  

fun is_delimiter s = s = "+" orelse s = "-" orelse s = ":"
		    
fun is_cmp s = s = "<" orelse s = ">" orelse s = "<=" 
		     orelse s = ">=" orelse s = "="

fun is_symbol a = 
    let
	val symbol_char = String.explode "!\"#$%&()/,.;?@_`'{}|~"
	fun is_symbol_char c = Char.isAlphaNum c orelse 
			       exists (fn d => d=c) symbol_char
	fun is_symbol_start c = is_symbol_char c andalso 
				not (Char.isDigit c) andalso 
				not (c= #".")
	val b = String.explode a
    in
	b <> [] andalso is_symbol_start (hd b) andalso 
	forall is_symbol_char b
    end

fun to_upper s = String.implode (map Char.toUpper (String.explode s))

fun keyword x = 
    let 	
	val a = to_upper x 
    in
	if a = "BOUNDS" orelse a = "BOUND" then
	    SOME "BOUNDS"
	else if a = "MINIMIZE" orelse a = "MINIMUM" orelse a = "MIN" then
	    SOME "MINIMIZE"
	else if a = "MAXIMIZE" orelse a = "MAXIMUM" orelse a = "MAX" then
	    SOME "MAXIMIZE"
	else if a = "ST" orelse a = "S.T." orelse a = "ST." then
	    SOME "ST"
	else if a = "FREE" orelse a = "END" then
	    SOME a
	else if a = "GENERAL" orelse a = "GENERALS" orelse a = "GEN" then
	    SOME "GENERAL"
	else if a = "INTEGER" orelse a = "INTEGERS" orelse a = "INT" then
	    SOME "INTEGER"
	else if a = "BINARY" orelse a = "BINARIES" orelse a = "BIN" then
	    SOME "BINARY"
	else if a = "INF" orelse a = "INFINITY" then
	    SOME "INF"
	else								   
	    NONE
    end
	        
val TOKEN_ERROR = ~1
val TOKEN_BLANK = 0
val TOKEN_NUM = 1
val TOKEN_DELIMITER = 2
val TOKEN_SYMBOL = 3
val TOKEN_LABEL = 4
val TOKEN_CMP = 5
val TOKEN_KEYWORD = 6
val TOKEN_NL = 7
		      
(* tokenize takes a list of chars as argument and returns a list of
   int * string pairs, each string representing a "cplex token", 
   and each int being one of TOKEN_NUM, TOKEN_DELIMITER, TOKEN_CMP
   or TOKEN_SYMBOL *)
fun tokenize s = 
    let
	val flist = [(is_NL, TOKEN_NL), 
		     (is_blank, TOKEN_BLANK), 
		     (is_num, TOKEN_NUM),  
                     (is_delimiter, TOKEN_DELIMITER), 
		     (is_cmp, TOKEN_CMP), 
		     (is_symbol, TOKEN_SYMBOL)]  
	fun match_helper [] s = (fn x => false, TOKEN_ERROR)
	  | match_helper (f::fs) s = 
	    if ((fst f) s) then f else match_helper fs s   
	fun match s = match_helper flist s
	fun tok s = 
	    if s = "" then [] else       
	    let 
		val h = String.substring (s,0,1) 
		val (f, j) = match h
		fun len i = 
		    if size s = i then i 
		    else if f (String.substring (s,0,i+1)) then 
			len (i+1) 
		    else i 
	    in
		if j < 0 then 
		    (if h = "\\" then [] 
		     else raise (Load_cplexFile ("token expected, found: "
						 ^s)))
		else 
		    let 
			val l = len 1 
			val u = String.substring (s,0,l)
			val v = String.extract (s,l,NONE)
		    in
			if j = 0 then tok v else (j, u) :: tok v
		    end
	    end                
    in
	tok s     
    end

exception Tokenize of string;

fun tokenize_general flist s = 
    let
	fun match_helper [] s = raise (Tokenize s)
	  | match_helper (f::fs) s = 
	    if ((fst f) s) then f else match_helper fs s   
	fun match s = match_helper flist s
	fun tok s = 
	    if s = "" then [] else       
	    let 
		val h = String.substring (s,0,1) 
		val (f, j) = match h
		fun len i = 
		    if size s = i then i 
		    else if f (String.substring (s,0,i+1)) then 
			len (i+1) 
		    else i 
		val l = len 1
	    in
		(j, String.substring (s,0,l)) :: tok (String.extract (s,l,NONE))
	    end
    in
	tok s     
    end

fun load_cplexFile name = 
    let 
	val f = TextIO.openIn name  
        val ignore_NL = ref true  
	val rest = ref []

	fun is_symbol s c = (fst c) = TOKEN_SYMBOL andalso (to_upper (snd c)) = s 
		   
	fun readToken_helper () =
	    if length (!rest) > 0 then  
		let val u = hd (!rest) in 
		    (
		     rest := tl (!rest); 
		     SOME u
		    ) 
		end
	    else 
		let val s = TextIO.inputLine f in
		    if s = "" then NONE else
		    let val t = tokenize s in
			if (length t >= 2 andalso 
			    snd(hd (tl t)) = ":") 
			then 
			    rest := (TOKEN_LABEL, snd (hd t)) :: (tl (tl t))
			else if (length t >= 2) andalso is_symbol "SUBJECT" (hd (t)) 
				andalso is_symbol "TO" (hd (tl t)) 
			then
			    rest := (TOKEN_SYMBOL, "ST") :: (tl (tl t))
			else
			    rest := t;
			readToken_helper ()  
		    end
		end           
	
	fun readToken_helper2 () = 
		let val c = readToken_helper () in
		    if c = NONE then NONE
                    else if !ignore_NL andalso fst (the c) = TOKEN_NL then
			readToken_helper2 ()
		    else if fst (the c) = TOKEN_SYMBOL 
			    andalso keyword (snd (the c)) <> NONE
		    then SOME (TOKEN_KEYWORD, the (keyword (snd (the c))))
		    else c
		end
		
	fun readToken () = readToken_helper2 ()
	    			   
	fun pushToken a = rest := (a::(!rest))
	    
	fun is_value token = 
	    fst token = TOKEN_NUM orelse (fst token = TOKEN_KEYWORD 
					  andalso snd token = "INF")	

        fun get_value token = 
	    if fst token = TOKEN_NUM then
		cplexNum (snd token)
	    else if fst token = TOKEN_KEYWORD andalso snd token = "INF" 
	    then
		cplexInf
	    else
		raise (Load_cplexFile "num expected")
					    
	fun readTerm_Product only_num = 
	    let val c = readToken () in
		if c = NONE then NONE
		else if fst (the c) = TOKEN_SYMBOL 
		then (
		    if only_num then (pushToken (the c); NONE) 
		    else SOME (cplexVar (snd (the c)))
		    ) 
		else if only_num andalso is_value (the c) then
		    SOME (get_value (the c))
		else if is_value (the c) then  
		    let val t1 = get_value (the c) 
			val d = readToken () 
		    in
			if d = NONE then SOME t1 
			else if fst (the d) = TOKEN_SYMBOL then 
			    SOME (cplexProd (t1, cplexVar (snd (the d))))
			else
			    (pushToken (the d); SOME t1)
		    end
		else (pushToken (the c); NONE)
	    end
	    
	fun readTerm_Signed only_signed only_num = 
	    let
		val c = readToken ()
	    in
		if c = NONE then NONE 
		else 
		    let val d = the c in 
			if d = (TOKEN_DELIMITER, "+") then 
			    readTerm_Product only_num
			 else if d = (TOKEN_DELIMITER, "-") then 
			     SOME (cplexNeg (the (readTerm_Product 
						      only_num)))
			 else (pushToken d; 
			       if only_signed then NONE 
			       else readTerm_Product only_num)
		    end
	    end
    
	fun readTerm_Sum first_signed = 
	    let val c = readTerm_Signed first_signed false in
		if c = NONE then [] else (the c)::(readTerm_Sum true)
	    end
	    
	fun readTerm () = 
	    let val c = readTerm_Sum false in
		if c = [] then NONE 
		else if tl c = [] then SOME (hd c)
		else SOME (cplexSum c) 
	    end
	    
	fun readLabeledTerm () = 
	    let val c = readToken () in
		if c = NONE then (NONE, NONE) 
		else if fst (the c) = TOKEN_LABEL then 
		    let val t = readTerm () in
			if t = NONE then 
			    raise (Load_cplexFile ("term after label "^
						   (snd (the c))^
						   " expected"))
			else (SOME (snd (the c)), t)
		    end
		else (pushToken (the c); (NONE, readTerm ()))
	    end
            
	fun readGoal () = 
	    let 
		val g = readToken ()
	    in
    		if g = SOME (TOKEN_KEYWORD, "MAXIMIZE") then 
		    cplexMaximize (the (snd (readLabeledTerm ()))) 
		else if g = SOME (TOKEN_KEYWORD, "MINIMIZE") then 
		    cplexMinimize (the (snd (readLabeledTerm ())))
		else raise (Load_cplexFile "MAXIMIZE or MINIMIZE expected")
	    end
	    
	fun str2cmp b = 
	    (case b of 
		 "<" => cplexLe 
	       | "<=" => cplexLeq 
	       | ">" => cplexGe 
	       | ">=" => cplexGeq 
               | "=" => cplexEq
	       | _ => raise (Load_cplexFile (b^" is no TOKEN_CMP")))
			    
	fun readConstraint () = 
            let 
		val t = readLabeledTerm () 
		fun make_constraint b t1 t2 =
                    cplexConstr 
			(str2cmp b,
			 (t1, t2))		
	    in
		if snd t = NONE then NONE
		else 
		    let val c = readToken () in
			if c = NONE orelse fst (the c) <> TOKEN_CMP 
			then raise (Load_cplexFile "TOKEN_CMP expected")
			else 
			    let val n = readTerm_Signed false true in
				if n = NONE then 
				    raise (Load_cplexFile "num expected")
				else
				    SOME (fst t,
					  make_constraint (snd (the c)) 
							  (the (snd t)) 
							  (the n))
			    end
		    end            
	    end
        
        fun readST () = 
	    let 
		fun readbody () = 
		    let val t = readConstraint () in
			if t = NONE then []
			else if (is_normed_Constr (snd (the t))) then
			    (the t)::(readbody ())
			else if (fst (the t) <> NONE) then 
			    raise (Load_cplexFile 
				       ("constraint '"^(the (fst (the t)))^ 
					"'is not normed"))
			else
			    raise (Load_cplexFile 
				       "constraint is not normed")
		    end
	    in    		
		if readToken () = SOME (TOKEN_KEYWORD, "ST") 
		then 
		    readbody ()
		else 
		    raise (Load_cplexFile "ST expected")
	    end
	    
	fun readCmp () = 
	    let val c = readToken () in
		if c = NONE then NONE
		else if fst (the c) = TOKEN_CMP then 
		    SOME (str2cmp (snd (the c)))
		else (pushToken (the c); NONE)
	    end
	    
	fun skip_NL () =
	    let val c = readToken () in
		if c <> NONE andalso fst (the c) = TOKEN_NL then
		    skip_NL ()
		else
		    (pushToken (the c); ())
	    end

	fun is_var (cplexVar _) = true
	  | is_var _ = false
	    
	fun make_bounds c t1 t2 = 
	    cplexBound (t1, c, t2)

	fun readBound () = 	    
	    let 		
		val _ = skip_NL ()
		val t1 = readTerm ()
	    in
		if t1 = NONE then NONE 
		else 
		    let 
			val c1 = readCmp () 
		    in
			if c1 = NONE then
			    let 
				val c = readToken () 
			    in
				if c = SOME (TOKEN_KEYWORD, "FREE") then
				    SOME (
				    cplexBounds (cplexNeg cplexInf,
						 cplexLeq,
						 the t1,
						 cplexLeq,
						 cplexInf))
				else
				    raise (Load_cplexFile "FREE expected")
			    end
			else
			    let 
				val t2 = readTerm () 
			    in
				if t2 = NONE then
				    raise (Load_cplexFile "term expected")
				else
				    let val c2 = readCmp () in
					if c2 = NONE then
					    SOME (make_bounds (the c1) 
							      (the t1)
							      (the t2))
					else
					    SOME (
					    cplexBounds (the t1,
							 the c1,
							 the t2,
							 the c2,
							 the (readTerm())))
				    end
			    end
		    end
	    end
	    
	fun readBounds () =
	    let 
		fun makestring b = "?"
		fun readbody () = 
		    let 
			val b = readBound ()
		    in
			if b = NONE then []
			else if (is_normed_Bounds (the b)) then
			    (the b)::(readbody())
			else (
			    raise (Load_cplexFile 
				       ("bounds are not normed in: "^
					(makestring (the b)))))
		    end
	    in
		if readToken () = SOME (TOKEN_KEYWORD, "BOUNDS") then 
		    readbody ()
		else raise (Load_cplexFile "BOUNDS expected")
	    end

        fun readEnd () = 
	    if readToken () = SOME (TOKEN_KEYWORD, "END") then ()
	    else raise (Load_cplexFile "END expected")
		    
	val result_Goal = readGoal ()  
	val result_ST = readST ()  
	val _ =	ignore_NL := false 
        val result_Bounds = readBounds ()
        val _ = ignore_NL := true
        val _ = readEnd ()
	val _ = TextIO.closeIn f
    in
	cplexProg (name, result_Goal, result_ST, result_Bounds)
    end

fun save_cplexFile filename (cplexProg (name, goal, constraints, bounds)) =
    let
	val f = TextIO.openOut filename
	
	fun basic_write s = TextIO.output(f, s)

	val linebuf = ref ""
	fun buf_flushline s = 
	    (basic_write (!linebuf); 
	     basic_write "\n";
	     linebuf := s)
	fun buf_add s = linebuf := (!linebuf) ^ s

	fun write s = 
	    if (String.size s) + (String.size (!linebuf)) >= 250 then 
		buf_flushline ("    "^s)
	    else 
		buf_add s

        fun writeln s = (buf_add s; buf_flushline "")
        
	fun write_term (cplexVar x) = write x
	  | write_term (cplexNum x) = write x
	  | write_term cplexInf = write "inf"
	  | write_term (cplexProd (cplexNum "1", b)) = write_term b
	  | write_term (cplexProd (a, b)) = 
	    (write_term a; write " "; write_term b)
          | write_term (cplexNeg x) = (write " - "; write_term x)
          | write_term (cplexSum ts) = write_terms ts
	and write_terms [] = ()
	  | write_terms (t::ts) = 
	    (if (not (is_Neg t)) then write " + " else (); 
	     write_term t; write_terms ts)

	fun write_goal (cplexMaximize term) = 
	    (writeln "MAXIMIZE"; write_term term; writeln "")
	  | write_goal (cplexMinimize term) = 
	    (writeln "MINIMIZE"; write_term term; writeln "")

	fun write_cmp cplexLe = write "<"
	  | write_cmp cplexLeq = write "<="
	  | write_cmp cplexEq = write "="
	  | write_cmp cplexGe = write ">"
	  | write_cmp cplexGeq = write ">="
        
	fun write_constr (cplexConstr (cmp, (a,b))) = 
	    (write_term a;
	     write " ";
	     write_cmp cmp;
	     write " ";
	     write_term b)
        
	fun write_constraints [] = ()
	  | write_constraints (c::cs) = 
	    (if (fst c <> NONE) 
	     then 
		 (write (the (fst c)); write ": ") 
	     else 
		 ();
	     write_constr (snd c);
	     writeln "";
	     write_constraints cs)

	fun write_bounds [] = ()
	  | write_bounds ((cplexBounds (t1,c1,t2,c2,t3))::bs) =
	    ((if t1 = cplexNeg cplexInf andalso t3 = cplexInf
		 andalso (c1 = cplexLeq orelse c1 = cplexLe) 
		 andalso (c2 = cplexLeq orelse c2 = cplexLe) 
	      then
		  (write_term t2; write " free")
	      else		 		 
		  (write_term t1; write " "; write_cmp c1; write " ";
		   write_term t2; write " "; write_cmp c2; write " ";
		   write_term t3)
	     ); writeln ""; write_bounds bs)
	  | write_bounds ((cplexBound (t1, c, t2)) :: bs) = 
	    (write_term t1; write " "; 
	     write_cmp c; write " ";
	     write_term t2; writeln ""; write_bounds bs)
	     
	val _ = write_goal goal
        val _ = (writeln ""; writeln "ST")
	val _ = write_constraints constraints
        val _ = (writeln ""; writeln "BOUNDS")
	val _ = write_bounds bounds
        val _ = (writeln ""; writeln "END") 
        val _ = TextIO.closeOut f
    in
	()
    end

fun norm_Constr (constr as cplexConstr (c, (t1, t2))) = 
    if not (modulo_signed is_Num t2) andalso  
       modulo_signed is_Num t1 
    then
	[cplexConstr (rev_cmp c, (t2, t1))]
    else if (c = cplexLe orelse c = cplexLeq) andalso
	    (t1 = (cplexNeg cplexInf) orelse t2 = cplexInf)	    
    then 
	[]
    else if (c = cplexGe orelse c = cplexGeq) andalso
	    (t1 = cplexInf orelse t2 = cplexNeg cplexInf)
    then
	[]
    else
	[constr]

fun bound2constr (cplexBounds (t1,c1,t2,c2,t3)) =
    (norm_Constr(cplexConstr (c1, (t1, t2))))
    @ (norm_Constr(cplexConstr (c2, (t2, t3))))
  | bound2constr (cplexBound (t1, cplexEq, t2)) =
    (norm_Constr(cplexConstr (cplexLeq, (t1, t2))))
    @ (norm_Constr(cplexConstr (cplexLeq, (t2, t1))))
  | bound2constr (cplexBound (t1, c1, t2)) = 
    norm_Constr(cplexConstr (c1, (t1,t2)))

val emptyset = Symtab.empty

fun singleton v = Symtab.update ((v, ()), emptyset)

fun merge a b = Symtab.merge (op =) (a, b)

fun mergemap f ts = Library.foldl
			(fn (table, x) => merge table (f x))
			(Symtab.empty, ts)

fun diff a b = Symtab.foldl (fn (a, (k,v)) => 
			 (Symtab.delete k a) handle UNDEF => a) 
		     (a, b)
		    
fun collect_vars (cplexVar v) = singleton v
  | collect_vars (cplexNeg t) = collect_vars t
  | collect_vars (cplexProd (t1, t2)) = 
    merge (collect_vars t1) (collect_vars t2)
  | collect_vars (cplexSum ts) = mergemap collect_vars ts
  | collect_vars _ = emptyset

(* Eliminates all nonfree bounds from the linear program and produces an
   equivalent program with only free bounds 
   IF for the input program P holds: is_normed_cplexProg P *)
fun elim_nonfree_bounds (cplexProg (name, goal, constraints, bounds)) =
    let
	fun collect_constr_vars (_, cplexConstr (c, (t1,_))) =
	    (collect_vars t1)   
	
	val cvars = merge (collect_vars (term_of_goal goal)) 
			  (mergemap collect_constr_vars constraints)         
		    
	fun collect_lower_bounded_vars 
	    (cplexBounds (t1, c1, cplexVar v, c2, t3)) =
	    singleton v
	  |  collect_lower_bounded_vars 
		 (cplexBound (_, cplexLe, cplexVar v)) =
	     singleton v
	  |  collect_lower_bounded_vars 
		 (cplexBound (_, cplexLeq, cplexVar v)) = 
	     singleton v
	  |  collect_lower_bounded_vars 
		 (cplexBound (cplexVar v, cplexGe,_)) = 
	     singleton v
	  |  collect_lower_bounded_vars 
		 (cplexBound (cplexVar v, cplexGeq, _)) = 
	     singleton v
	  | collect_lower_bounded_vars
	    (cplexBound (cplexVar v, cplexEq, _)) = 
	    singleton v
	  |  collect_lower_bounded_vars _ = emptyset
	
	val lvars = mergemap collect_lower_bounded_vars bounds        
	val positive_vars = diff cvars lvars			   
	val zero = cplexNum "0"
	
	fun make_pos_constr v = 
	    (NONE, cplexConstr (cplexGeq, ((cplexVar v), zero)))
	
	fun make_free_bound v = 
	    cplexBounds (cplexNeg cplexInf, cplexLeq, 
			 cplexVar v, cplexLeq,
			 cplexInf)
	
	val pos_constrs = rev(Symtab.foldl 
			      (fn (l, (k,v)) => (make_pos_constr k) :: l)
			      ([], positive_vars))
        val bound_constrs = map (fn x => (NONE, x)) 
				(Library.flat (map bound2constr bounds))
	val constraints' = constraints @ pos_constrs @ bound_constrs	   
	val bounds' = rev(Symtab.foldl (fn (l, (v,_)) => 
					   (make_free_bound v)::l)
				       ([], cvars))			  
    in
	cplexProg (name, goal, constraints', bounds')
    end

fun relax_strict_ineqs (cplexProg (name, goals, constrs, bounds)) = 
    let
	fun relax cplexLe = cplexLeq
	  | relax cplexGe = cplexGeq
	  | relax x = x
	
	fun relax_constr (n, cplexConstr(c, (t1, t2))) = 
	    (n, cplexConstr(relax c, (t1, t2)))
	    
	fun relax_bounds (cplexBounds (t1, c1, t2, c2, t3)) = 
	    cplexBounds (t1, relax c1, t2, relax c2, t3)
	  | relax_bounds (cplexBound (t1, c, t2)) = 
	    cplexBound (t1, relax c, t2)
    in
	cplexProg (name, 
		   goals, 
		   map relax_constr constrs, 
		   map relax_bounds bounds)
    end

datatype cplexResult = Unbounded 
		     | Infeasible 
		     | Undefined
		     | Optimal of string * ((string * string) list)

fun is_separator x = forall (fn c => c = #"-") (String.explode x)

fun is_sign x = (x = "+" orelse x = "-")

fun is_colon x = (x = ":")

fun is_resultsymbol a = 
    let
	val symbol_char = String.explode "!\"#$%&()/,.;?@_`'{}|~-"
	fun is_symbol_char c = Char.isAlphaNum c orelse 
			       exists (fn d => d=c) symbol_char
	fun is_symbol_start c = is_symbol_char c andalso 
				not (Char.isDigit c) andalso 
				not (c= #".") andalso
				not (c= #"-")
	val b = String.explode a
    in
	b <> [] andalso is_symbol_start (hd b) andalso 
	forall is_symbol_char b
    end

val TOKEN_SIGN = 100
val TOKEN_COLON = 101
val TOKEN_SEPARATOR = 102

fun load_glpkResult name = 
    let
	val flist = [(is_NL, TOKEN_NL), 
		     (is_blank, TOKEN_BLANK),
		     (is_num, TOKEN_NUM),
		     (is_sign, TOKEN_SIGN),
                     (is_colon, TOKEN_COLON),
		     (is_cmp, TOKEN_CMP),
		     (is_resultsymbol, TOKEN_SYMBOL),
		     (is_separator, TOKEN_SEPARATOR)]

	val tokenize = tokenize_general flist

	val f = TextIO.openIn name  

	val rest = ref []
		   
	fun readToken_helper () =
	    if length (!rest) > 0 then  
		let val u = hd (!rest) in 
		    (
		     rest := tl (!rest); 
		     SOME u
		    ) 
		end
	    else 
		let val s = TextIO.inputLine f in
		    if s = "" then NONE else (rest := tokenize s; readToken_helper())					     
		end           
		
	fun is_tt tok ty = (tok <> NONE andalso (fst (the tok)) = ty)

	fun pushToken a = if a = NONE then () else (rest := ((the a)::(!rest)))
	
	fun readToken () =
	    let val t = readToken_helper () in
		if is_tt t TOKEN_BLANK then 
		    readToken ()
		else if is_tt t TOKEN_NL then 
		    let val t2 = readToken_helper () in
			if is_tt t2 TOKEN_SIGN then 
			    (pushToken (SOME (TOKEN_SEPARATOR, "-")); t)
			else 
			    (pushToken t2; t)
		    end
		else if is_tt t TOKEN_SIGN then
		    let val t2 = readToken_helper () in
			if is_tt t2 TOKEN_NUM then
			    (SOME (TOKEN_NUM, (snd (the t))^(snd (the t2))))
			else
			    (pushToken t2; t)
		    end
		else
		    t
	    end	    		

        fun readRestOfLine P = 
	    let 
		val t = readToken ()
	    in
		if is_tt t TOKEN_NL orelse t = NONE 
		then P
		else readRestOfLine P
	    end			
							 
	fun readHeader () = 
	    let
		fun readStatus () = readRestOfLine ("STATUS", snd (the (readToken ())))
		fun readObjective () = readRestOfLine ("OBJECTIVE", snd (the (readToken (); readToken (); readToken ())))
		val t1 = readToken ()
		val t2 = readToken ()
	    in
		if is_tt t1 TOKEN_SYMBOL andalso is_tt t2 TOKEN_COLON 
		then
		    case to_upper (snd (the t1)) of
			"STATUS" => (readStatus ())::(readHeader ())
		      | "OBJECTIVE" => (readObjective())::(readHeader ())
		      | _ => (readRestOfLine (); readHeader ())
		else
		    (pushToken t2; pushToken t1; [])
	    end

	fun skip_until_sep () = 
	    let val x = readToken () in
		if is_tt x TOKEN_SEPARATOR then
		    readRestOfLine ()
		else 
		    skip_until_sep ()
	    end

	fun load_value () =
	    let 
		val t1 = readToken ()
		val t2 = readToken ()
	    in
		if is_tt t1 TOKEN_NUM andalso is_tt t2 TOKEN_SYMBOL then
		    let 
			val t = readToken ()
			val state = if is_tt t TOKEN_NL then readToken () else t
			val _ = if is_tt state TOKEN_SYMBOL then () else raise (Load_cplexResult "state expected")
			val k = readToken ()
		    in
			if is_tt k TOKEN_NUM then
			    readRestOfLine (SOME (snd (the t2), snd (the k)))
			else
			    raise (Load_cplexResult "number expected")
		    end				
		else
		    (pushToken t2; pushToken t1; NONE)
	    end

	fun load_values () = 
	    let val v = load_value () in
		if v = NONE then [] else (the v)::(load_values ())
	    end
	
	val header = readHeader () 

	val result = 
	    case assoc (header, "STATUS") of
		SOME "INFEASIBLE" => Infeasible
	      | SOME "UNBOUNDED" => Unbounded
	      | SOME "OPTIMAL" => Optimal (the (assoc (header, "OBJECTIVE")), 
					   (skip_until_sep (); 
					    skip_until_sep ();
					    load_values ()))
	      | _ => Undefined

	val _ = TextIO.closeIn f
    in
	result
    end
    handle (Tokenize s) => raise (Load_cplexResult ("Tokenize: "^s))
	 | Option => raise (Load_cplexResult "Option")
	 | x => raise x

fun load_cplexResult name = 
    let
	val flist = [(is_NL, TOKEN_NL), 
		     (is_blank, TOKEN_BLANK),
		     (is_num, TOKEN_NUM),
		     (is_sign, TOKEN_SIGN),
                     (is_colon, TOKEN_COLON),
		     (is_cmp, TOKEN_CMP),
		     (is_resultsymbol, TOKEN_SYMBOL)]

	val tokenize = tokenize_general flist

	val f = TextIO.openIn name  

	val rest = ref []
		   
	fun readToken_helper () =
	    if length (!rest) > 0 then  
		let val u = hd (!rest) in 
		    (
		     rest := tl (!rest); 
		     SOME u
		    ) 
		end
	    else 
		let 
		    val s = TextIO.inputLine f 
		in		    
		    if s = "" then NONE else (rest := tokenize s; readToken_helper())					     
		end           
		
	fun is_tt tok ty = (tok <> NONE andalso (fst (the tok)) = ty)

	fun pushToken a = if a = NONE then () else (rest := ((the a)::(!rest)))
	
	fun readToken () =
	    let val t = readToken_helper () in
		if is_tt t TOKEN_BLANK then 
		    readToken ()
		else if is_tt t TOKEN_SIGN then
		    let val t2 = readToken_helper () in
			if is_tt t2 TOKEN_NUM then
			    (SOME (TOKEN_NUM, (snd (the t))^(snd (the t2))))
			else
			    (pushToken t2; t)
		    end
		else
		    t
	    end	    		

        fun readRestOfLine P = 
	    let 
		val t = readToken ()
	    in
		if is_tt t TOKEN_NL orelse t = NONE 
		then P
		else readRestOfLine P
	    end			

	fun readHeader () = 
	    let
		fun readStatus () = readRestOfLine ("STATUS", snd (the (readToken ())))
		fun readObjective () = 
		    let
			val t = readToken ()
		    in
			if is_tt t TOKEN_SYMBOL andalso to_upper (snd (the t)) = "VALUE" then 
			    readRestOfLine ("OBJECTIVE", snd (the (readToken())))
			else
			    readRestOfLine ("OBJECTIVE_NAME", snd (the t))
		    end
		  
		val t = readToken ()
	    in
		if is_tt t TOKEN_SYMBOL then
		    case to_upper (snd (the t)) of 
			"STATUS" => (readStatus ())::(readHeader ())
		      | "OBJECTIVE" => (readObjective ())::(readHeader ())
		      | "SECTION" => (pushToken t; [])
		      | _ => (readRestOfLine (); readHeader ())
		else
		    (readRestOfLine (); readHeader ())
	    end

	fun skip_nls () = 
	    let val x = readToken () in
		if is_tt x TOKEN_NL then 
		    skip_nls () 
		else 
		    (pushToken x; ())
	    end

	fun skip_paragraph () = 
	    if is_tt (readToken ()) TOKEN_NL then
		(if is_tt (readToken ()) TOKEN_NL then
		     skip_nls ()
		 else
		     skip_paragraph ())
	    else			
		skip_paragraph ()	

	fun load_value () =
	    let 
		val t1 = readToken ()
		val t1 = if is_tt t1 TOKEN_SYMBOL andalso snd (the t1) = "A" then readToken () else t1
	    in
		if is_tt t1 TOKEN_NUM then
		    let 
			val name = readToken ()
			val status = readToken ()
			val value = readToken ()
		    in
			if is_tt name TOKEN_SYMBOL andalso
			   is_tt status TOKEN_SYMBOL andalso
			   is_tt value TOKEN_NUM 
			then
			    readRestOfLine (SOME (snd (the name), snd (the value)))
			else
			    raise (Load_cplexResult "column line expected")
		    end
		else 
		    (pushToken t1; NONE)
	    end

	fun load_values () = 
	    let val v = load_value () in
		if v = NONE then [] else (the v)::(load_values ())
	    end
	
	val header = readHeader ()

	val result = 
	    case assoc (header, "STATUS") of
		SOME "INFEASIBLE" => Infeasible
	      | SOME "NONOPTIMAL" => Unbounded
	      | SOME "OPTIMAL" => Optimal (the (assoc (header, "OBJECTIVE")), 
					   (skip_paragraph (); 
					    skip_paragraph (); 
					    skip_paragraph (); 
					    skip_paragraph (); 
					    skip_paragraph ();
					    load_values ()))
	      | _ => Undefined

	val _ = TextIO.closeIn f
    in
	result
    end
    handle (Tokenize s) => raise (Load_cplexResult ("Tokenize: "^s))
	 | Option => raise (Load_cplexResult "Option")
	 | x => raise x

exception Execute of string;

fun tmp_file s = Path.pack (Path.expand (File.tmp_path (Path.make [s])));
fun wrap s = "\""^s^"\"";

fun solve_glpk prog =
    let 
	val name = LargeInt.toString (Time.toMicroseconds (Time.now ()))	
	val lpname = tmp_file (name^".lp")
	val resultname = tmp_file (name^".txt")
	val _ = save_cplexFile lpname prog		
	val cplex_path = getenv "GLPK_PATH"
	val cplex = if cplex_path = "" then "glpsol" else cplex_path
	val command = (wrap cplex)^" --lpt "^(wrap lpname)^" --output "^(wrap resultname)
	val answer = execute command
    in
	let
	    val result = load_glpkResult resultname
	    val _ = OS.FileSys.remove lpname
	    val _ = OS.FileSys.remove resultname
	in
	    result
	end 
	handle (Load_cplexResult s) => raise (Execute ("Load_cplexResult: "^s^"\nExecute: "^answer))
	     | _ => raise (Execute answer)
    end		     
    
fun solve_cplex prog =
    let 
	fun write_script s lp r =
	    let
		val f = TextIO.openOut s
		val _ = TextIO.output (f, "read\n"^lp^"\noptimize\nwrite\n"^r^"\nquit")
		val _ = TextIO.closeOut f
	    in 
		() 
	    end 
	    
	val name = LargeInt.toString (Time.toMicroseconds (Time.now ()))	
	val lpname = tmp_file (name^".lp")
	val resultname = tmp_file (name^".txt")
	val scriptname = tmp_file (name^".script")
	val _ = save_cplexFile lpname prog		
	val cplex_path = getenv "CPLEX_PATH"
	val cplex = if cplex_path = "" then "cplex" else cplex_path
	val _ = write_script scriptname lpname resultname
	val command = (wrap cplex)^" < "^(wrap scriptname)^" > /dev/null"
	val answer = "return code "^(Int.toString (system command))
    in
	let
	    val result = load_cplexResult resultname
	    val _ = OS.FileSys.remove lpname
	    val _ = OS.FileSys.remove resultname
	    val _ = OS.FileSys.remove scriptname
	in
	    result
	end 
    end

fun solve prog = 
    case get_solver () of
      SOLVER_DEFAULT => 
        (case getenv "LP_SOLVER" of
	   "CPLEX" => solve_cplex prog
         | "GLPK" => solve_glpk prog
         | _ => raise (Execute ("LP_SOLVER must be set to CPLEX or to GLPK")))
    | SOLVER_CPLEX => solve_cplex prog
    | SOLVER_GLPK => solve_glpk prog
		   
end;

(*
val demofile = "/home/obua/flyspeck/kepler/LP/cplexPent2.lp45"
val demoout = "/home/obua/flyspeck/kepler/LP/test.out"
val demoresult = "/home/obua/flyspeck/kepler/LP/try/test2.sol"
	   
fun loadcplex () = Cplex.relax_strict_ineqs 
		   (Cplex.load_cplexFile demofile)

fun writecplex lp = Cplex.save_cplexFile demoout lp

fun test () = 
    let
	val lp = loadcplex ()
	val lp2 = Cplex.elim_nonfree_bounds lp
    in
	writecplex lp2
    end

fun loadresult () = Cplex.load_cplexResult demoresult;
*)

(*val prog = Cplex.load_cplexFile "/home/obua/tmp/pent/graph_0.lpt";
val _ = Cplex.solve prog;*)