# File Cplex_tools.ML

    (*  Title:      HOL/Matrix/cplex/Cplex_tools.ML
        ID:         $Id: Cplex_tools.ML,v 1.5 2005/09/20 14:18:15 haftmann Exp $
        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 AList.lookup (op =) header "STATUS" of
    		SOME "INFEASIBLE" => Infeasible
    	      | SOME "UNBOUNDED" => Unbounded
    	      | SOME "OPTIMAL" => Optimal (the (AList.lookup (op =) 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 AList.lookup (op =) header "STATUS" of
    		SOME "INFEASIBLE" => Infeasible
    	      | SOME "NONOPTIMAL" => Unbounded
    	      | SOME "OPTIMAL" => Optimal (the (AList.lookup (op =) 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;*)