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