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