src/HOL/Matrix/Cplex_tools.ML
author haftmann
Tue, 13 Jul 2010 11:38:04 +0200
changeset 37788 261c61fabc98
parent 37764 3489daf839d5
child 40299 132e2349694b
permissions -rw-r--r--
corrected title
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
92ff7c903585 - added cplex package to HOL/Matrix
obua
parents:
diff changeset
   111
fun is_Neg (cplexNeg x ) = true
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
22951
dfafcd6223ad whitespace tuned
haftmann
parents: 21858
diff changeset
   122
fun is_normed_Constr (cplexConstr (c, (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
22951
dfafcd6223ad whitespace tuned
haftmann
parents: 21858
diff changeset
   142
fun is_normed_cplexProg (cplexProg (name, 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)]
dfafcd6223ad whitespace tuned
haftmann
parents: 21858
diff changeset
   247
    fun match_helper [] s = (fn x => false, TOKEN_ERROR)
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 is_var (cplexVar _) = true
dfafcd6223ad whitespace tuned
haftmann
parents: 21858
diff changeset
   520
      | is_var _ = false
dfafcd6223ad whitespace tuned
haftmann
parents: 21858
diff changeset
   521
dfafcd6223ad whitespace tuned
haftmann
parents: 21858
diff changeset
   522
    fun make_bounds c t1 t2 =
dfafcd6223ad whitespace tuned
haftmann
parents: 21858
diff changeset
   523
        cplexBound (t1, c, t2)
16784
92ff7c903585 - added cplex package to HOL/Matrix
obua
parents:
diff changeset
   524
22951
dfafcd6223ad whitespace tuned
haftmann
parents: 21858
diff changeset
   525
    fun readBound () =
dfafcd6223ad whitespace tuned
haftmann
parents: 21858
diff changeset
   526
        let
dfafcd6223ad whitespace tuned
haftmann
parents: 21858
diff changeset
   527
        val _ = skip_NL ()
dfafcd6223ad whitespace tuned
haftmann
parents: 21858
diff changeset
   528
        val t1 = readTerm ()
dfafcd6223ad whitespace tuned
haftmann
parents: 21858
diff changeset
   529
        in
dfafcd6223ad whitespace tuned
haftmann
parents: 21858
diff changeset
   530
        if t1 = NONE then NONE
dfafcd6223ad whitespace tuned
haftmann
parents: 21858
diff changeset
   531
        else
dfafcd6223ad whitespace tuned
haftmann
parents: 21858
diff changeset
   532
            let
dfafcd6223ad whitespace tuned
haftmann
parents: 21858
diff changeset
   533
            val c1 = readCmp ()
dfafcd6223ad whitespace tuned
haftmann
parents: 21858
diff changeset
   534
            in
dfafcd6223ad whitespace tuned
haftmann
parents: 21858
diff changeset
   535
            if c1 = NONE then
dfafcd6223ad whitespace tuned
haftmann
parents: 21858
diff changeset
   536
                let
dfafcd6223ad whitespace tuned
haftmann
parents: 21858
diff changeset
   537
                val c = readToken ()
dfafcd6223ad whitespace tuned
haftmann
parents: 21858
diff changeset
   538
                in
dfafcd6223ad whitespace tuned
haftmann
parents: 21858
diff changeset
   539
                if c = SOME (TOKEN_KEYWORD, "FREE") then
dfafcd6223ad whitespace tuned
haftmann
parents: 21858
diff changeset
   540
                    SOME (
dfafcd6223ad whitespace tuned
haftmann
parents: 21858
diff changeset
   541
                    cplexBounds (cplexNeg cplexInf,
dfafcd6223ad whitespace tuned
haftmann
parents: 21858
diff changeset
   542
                         cplexLeq,
dfafcd6223ad whitespace tuned
haftmann
parents: 21858
diff changeset
   543
                         the t1,
dfafcd6223ad whitespace tuned
haftmann
parents: 21858
diff changeset
   544
                         cplexLeq,
dfafcd6223ad whitespace tuned
haftmann
parents: 21858
diff changeset
   545
                         cplexInf))
dfafcd6223ad whitespace tuned
haftmann
parents: 21858
diff changeset
   546
                else
dfafcd6223ad whitespace tuned
haftmann
parents: 21858
diff changeset
   547
                    raise (Load_cplexFile "FREE expected")
dfafcd6223ad whitespace tuned
haftmann
parents: 21858
diff changeset
   548
                end
dfafcd6223ad whitespace tuned
haftmann
parents: 21858
diff changeset
   549
            else
dfafcd6223ad whitespace tuned
haftmann
parents: 21858
diff changeset
   550
                let
dfafcd6223ad whitespace tuned
haftmann
parents: 21858
diff changeset
   551
                val t2 = readTerm ()
dfafcd6223ad whitespace tuned
haftmann
parents: 21858
diff changeset
   552
                in
dfafcd6223ad whitespace tuned
haftmann
parents: 21858
diff changeset
   553
                if t2 = NONE then
dfafcd6223ad whitespace tuned
haftmann
parents: 21858
diff changeset
   554
                    raise (Load_cplexFile "term expected")
dfafcd6223ad whitespace tuned
haftmann
parents: 21858
diff changeset
   555
                else
dfafcd6223ad whitespace tuned
haftmann
parents: 21858
diff changeset
   556
                    let val c2 = readCmp () in
dfafcd6223ad whitespace tuned
haftmann
parents: 21858
diff changeset
   557
                    if c2 = NONE then
dfafcd6223ad whitespace tuned
haftmann
parents: 21858
diff changeset
   558
                        SOME (make_bounds (the c1)
dfafcd6223ad whitespace tuned
haftmann
parents: 21858
diff changeset
   559
                                  (the t1)
dfafcd6223ad whitespace tuned
haftmann
parents: 21858
diff changeset
   560
                                  (the t2))
dfafcd6223ad whitespace tuned
haftmann
parents: 21858
diff changeset
   561
                    else
dfafcd6223ad whitespace tuned
haftmann
parents: 21858
diff changeset
   562
                        SOME (
dfafcd6223ad whitespace tuned
haftmann
parents: 21858
diff changeset
   563
                        cplexBounds (the t1,
dfafcd6223ad whitespace tuned
haftmann
parents: 21858
diff changeset
   564
                             the c1,
dfafcd6223ad whitespace tuned
haftmann
parents: 21858
diff changeset
   565
                             the t2,
dfafcd6223ad whitespace tuned
haftmann
parents: 21858
diff changeset
   566
                             the c2,
dfafcd6223ad whitespace tuned
haftmann
parents: 21858
diff changeset
   567
                             the (readTerm())))
dfafcd6223ad whitespace tuned
haftmann
parents: 21858
diff changeset
   568
                    end
dfafcd6223ad whitespace tuned
haftmann
parents: 21858
diff changeset
   569
                end
dfafcd6223ad whitespace tuned
haftmann
parents: 21858
diff changeset
   570
            end
dfafcd6223ad whitespace tuned
haftmann
parents: 21858
diff changeset
   571
        end
16784
92ff7c903585 - added cplex package to HOL/Matrix
obua
parents:
diff changeset
   572
22951
dfafcd6223ad whitespace tuned
haftmann
parents: 21858
diff changeset
   573
    fun readBounds () =
dfafcd6223ad whitespace tuned
haftmann
parents: 21858
diff changeset
   574
        let
dfafcd6223ad whitespace tuned
haftmann
parents: 21858
diff changeset
   575
        fun makestring b = "?"
dfafcd6223ad whitespace tuned
haftmann
parents: 21858
diff changeset
   576
        fun readbody () =
dfafcd6223ad whitespace tuned
haftmann
parents: 21858
diff changeset
   577
            let
dfafcd6223ad whitespace tuned
haftmann
parents: 21858
diff changeset
   578
            val b = readBound ()
dfafcd6223ad whitespace tuned
haftmann
parents: 21858
diff changeset
   579
            in
dfafcd6223ad whitespace tuned
haftmann
parents: 21858
diff changeset
   580
            if b = NONE then []
dfafcd6223ad whitespace tuned
haftmann
parents: 21858
diff changeset
   581
            else if (is_normed_Bounds (the b)) then
dfafcd6223ad whitespace tuned
haftmann
parents: 21858
diff changeset
   582
                (the b)::(readbody())
dfafcd6223ad whitespace tuned
haftmann
parents: 21858
diff changeset
   583
            else (
dfafcd6223ad whitespace tuned
haftmann
parents: 21858
diff changeset
   584
                raise (Load_cplexFile
dfafcd6223ad whitespace tuned
haftmann
parents: 21858
diff changeset
   585
                       ("bounds are not normed in: "^
dfafcd6223ad whitespace tuned
haftmann
parents: 21858
diff changeset
   586
                    (makestring (the b)))))
dfafcd6223ad whitespace tuned
haftmann
parents: 21858
diff changeset
   587
            end
dfafcd6223ad whitespace tuned
haftmann
parents: 21858
diff changeset
   588
        in
dfafcd6223ad whitespace tuned
haftmann
parents: 21858
diff changeset
   589
        if readToken () = SOME (TOKEN_KEYWORD, "BOUNDS") then
dfafcd6223ad whitespace tuned
haftmann
parents: 21858
diff changeset
   590
            readbody ()
dfafcd6223ad whitespace tuned
haftmann
parents: 21858
diff changeset
   591
        else raise (Load_cplexFile "BOUNDS expected")
dfafcd6223ad whitespace tuned
haftmann
parents: 21858
diff changeset
   592
        end
dfafcd6223ad whitespace tuned
haftmann
parents: 21858
diff changeset
   593
dfafcd6223ad whitespace tuned
haftmann
parents: 21858
diff changeset
   594
        fun readEnd () =
dfafcd6223ad whitespace tuned
haftmann
parents: 21858
diff changeset
   595
        if readToken () = SOME (TOKEN_KEYWORD, "END") then ()
dfafcd6223ad whitespace tuned
haftmann
parents: 21858
diff changeset
   596
        else raise (Load_cplexFile "END expected")
dfafcd6223ad whitespace tuned
haftmann
parents: 21858
diff changeset
   597
dfafcd6223ad whitespace tuned
haftmann
parents: 21858
diff changeset
   598
    val result_Goal = readGoal ()
dfafcd6223ad whitespace tuned
haftmann
parents: 21858
diff changeset
   599
    val result_ST = readST ()
dfafcd6223ad whitespace tuned
haftmann
parents: 21858
diff changeset
   600
    val _ =    ignore_NL := false
16784
92ff7c903585 - added cplex package to HOL/Matrix
obua
parents:
diff changeset
   601
        val result_Bounds = readBounds ()
92ff7c903585 - added cplex package to HOL/Matrix
obua
parents:
diff changeset
   602
        val _ = ignore_NL := true
92ff7c903585 - added cplex package to HOL/Matrix
obua
parents:
diff changeset
   603
        val _ = readEnd ()
22951
dfafcd6223ad whitespace tuned
haftmann
parents: 21858
diff changeset
   604
    val _ = TextIO.closeIn f
16784
92ff7c903585 - added cplex package to HOL/Matrix
obua
parents:
diff changeset
   605
    in
22951
dfafcd6223ad whitespace tuned
haftmann
parents: 21858
diff changeset
   606
    cplexProg (name, result_Goal, result_ST, result_Bounds)
16784
92ff7c903585 - added cplex package to HOL/Matrix
obua
parents:
diff changeset
   607
    end
92ff7c903585 - added cplex package to HOL/Matrix
obua
parents:
diff changeset
   608
92ff7c903585 - added cplex package to HOL/Matrix
obua
parents:
diff changeset
   609
fun save_cplexFile filename (cplexProg (name, goal, constraints, bounds)) =
92ff7c903585 - added cplex package to HOL/Matrix
obua
parents:
diff changeset
   610
    let
22951
dfafcd6223ad whitespace tuned
haftmann
parents: 21858
diff changeset
   611
    val f = TextIO.openOut filename
dfafcd6223ad whitespace tuned
haftmann
parents: 21858
diff changeset
   612
dfafcd6223ad whitespace tuned
haftmann
parents: 21858
diff changeset
   613
    fun basic_write s = TextIO.output(f, s)
16784
92ff7c903585 - added cplex package to HOL/Matrix
obua
parents:
diff changeset
   614
32740
9dd0a2f83429 explicit indication of Unsynchronized.ref;
wenzelm
parents: 32491
diff changeset
   615
    val linebuf = Unsynchronized.ref ""
22951
dfafcd6223ad whitespace tuned
haftmann
parents: 21858
diff changeset
   616
    fun buf_flushline s =
dfafcd6223ad whitespace tuned
haftmann
parents: 21858
diff changeset
   617
        (basic_write (!linebuf);
dfafcd6223ad whitespace tuned
haftmann
parents: 21858
diff changeset
   618
         basic_write "\n";
dfafcd6223ad whitespace tuned
haftmann
parents: 21858
diff changeset
   619
         linebuf := s)
dfafcd6223ad whitespace tuned
haftmann
parents: 21858
diff changeset
   620
    fun buf_add s = linebuf := (!linebuf) ^ s
16784
92ff7c903585 - added cplex package to HOL/Matrix
obua
parents:
diff changeset
   621
22951
dfafcd6223ad whitespace tuned
haftmann
parents: 21858
diff changeset
   622
    fun write s =
dfafcd6223ad whitespace tuned
haftmann
parents: 21858
diff changeset
   623
        if (String.size s) + (String.size (!linebuf)) >= 250 then
dfafcd6223ad whitespace tuned
haftmann
parents: 21858
diff changeset
   624
        buf_flushline ("    "^s)
dfafcd6223ad whitespace tuned
haftmann
parents: 21858
diff changeset
   625
        else
dfafcd6223ad whitespace tuned
haftmann
parents: 21858
diff changeset
   626
        buf_add s
16784
92ff7c903585 - added cplex package to HOL/Matrix
obua
parents:
diff changeset
   627
92ff7c903585 - added cplex package to HOL/Matrix
obua
parents:
diff changeset
   628
        fun writeln s = (buf_add s; buf_flushline "")
22951
dfafcd6223ad whitespace tuned
haftmann
parents: 21858
diff changeset
   629
dfafcd6223ad whitespace tuned
haftmann
parents: 21858
diff changeset
   630
    fun write_term (cplexVar x) = write x
dfafcd6223ad whitespace tuned
haftmann
parents: 21858
diff changeset
   631
      | write_term (cplexNum x) = write x
dfafcd6223ad whitespace tuned
haftmann
parents: 21858
diff changeset
   632
      | write_term cplexInf = write "inf"
dfafcd6223ad whitespace tuned
haftmann
parents: 21858
diff changeset
   633
      | write_term (cplexProd (cplexNum "1", b)) = write_term b
dfafcd6223ad whitespace tuned
haftmann
parents: 21858
diff changeset
   634
      | write_term (cplexProd (a, b)) =
dfafcd6223ad whitespace tuned
haftmann
parents: 21858
diff changeset
   635
        (write_term a; write " "; write_term b)
16784
92ff7c903585 - added cplex package to HOL/Matrix
obua
parents:
diff changeset
   636
          | write_term (cplexNeg x) = (write " - "; write_term x)
92ff7c903585 - added cplex package to HOL/Matrix
obua
parents:
diff changeset
   637
          | write_term (cplexSum ts) = write_terms ts
22951
dfafcd6223ad whitespace tuned
haftmann
parents: 21858
diff changeset
   638
    and write_terms [] = ()
dfafcd6223ad whitespace tuned
haftmann
parents: 21858
diff changeset
   639
      | write_terms (t::ts) =
dfafcd6223ad whitespace tuned
haftmann
parents: 21858
diff changeset
   640
        (if (not (is_Neg t)) then write " + " else ();
dfafcd6223ad whitespace tuned
haftmann
parents: 21858
diff changeset
   641
         write_term t; write_terms ts)
dfafcd6223ad whitespace tuned
haftmann
parents: 21858
diff changeset
   642
dfafcd6223ad whitespace tuned
haftmann
parents: 21858
diff changeset
   643
    fun write_goal (cplexMaximize term) =
dfafcd6223ad whitespace tuned
haftmann
parents: 21858
diff changeset
   644
        (writeln "MAXIMIZE"; write_term term; writeln "")
dfafcd6223ad whitespace tuned
haftmann
parents: 21858
diff changeset
   645
      | write_goal (cplexMinimize term) =
dfafcd6223ad whitespace tuned
haftmann
parents: 21858
diff changeset
   646
        (writeln "MINIMIZE"; write_term term; writeln "")
16784
92ff7c903585 - added cplex package to HOL/Matrix
obua
parents:
diff changeset
   647
22951
dfafcd6223ad whitespace tuned
haftmann
parents: 21858
diff changeset
   648
    fun write_cmp cplexLe = write "<"
dfafcd6223ad whitespace tuned
haftmann
parents: 21858
diff changeset
   649
      | write_cmp cplexLeq = write "<="
dfafcd6223ad whitespace tuned
haftmann
parents: 21858
diff changeset
   650
      | write_cmp cplexEq = write "="
dfafcd6223ad whitespace tuned
haftmann
parents: 21858
diff changeset
   651
      | write_cmp cplexGe = write ">"
dfafcd6223ad whitespace tuned
haftmann
parents: 21858
diff changeset
   652
      | write_cmp cplexGeq = write ">="
dfafcd6223ad whitespace tuned
haftmann
parents: 21858
diff changeset
   653
dfafcd6223ad whitespace tuned
haftmann
parents: 21858
diff changeset
   654
    fun write_constr (cplexConstr (cmp, (a,b))) =
dfafcd6223ad whitespace tuned
haftmann
parents: 21858
diff changeset
   655
        (write_term a;
dfafcd6223ad whitespace tuned
haftmann
parents: 21858
diff changeset
   656
         write " ";
dfafcd6223ad whitespace tuned
haftmann
parents: 21858
diff changeset
   657
         write_cmp cmp;
dfafcd6223ad whitespace tuned
haftmann
parents: 21858
diff changeset
   658
         write " ";
dfafcd6223ad whitespace tuned
haftmann
parents: 21858
diff changeset
   659
         write_term b)
16784
92ff7c903585 - added cplex package to HOL/Matrix
obua
parents:
diff changeset
   660
22951
dfafcd6223ad whitespace tuned
haftmann
parents: 21858
diff changeset
   661
    fun write_constraints [] = ()
dfafcd6223ad whitespace tuned
haftmann
parents: 21858
diff changeset
   662
      | write_constraints (c::cs) =
dfafcd6223ad whitespace tuned
haftmann
parents: 21858
diff changeset
   663
        (if (fst c <> NONE)
dfafcd6223ad whitespace tuned
haftmann
parents: 21858
diff changeset
   664
         then
dfafcd6223ad whitespace tuned
haftmann
parents: 21858
diff changeset
   665
         (write (the (fst c)); write ": ")
dfafcd6223ad whitespace tuned
haftmann
parents: 21858
diff changeset
   666
         else
dfafcd6223ad whitespace tuned
haftmann
parents: 21858
diff changeset
   667
         ();
dfafcd6223ad whitespace tuned
haftmann
parents: 21858
diff changeset
   668
         write_constr (snd c);
dfafcd6223ad whitespace tuned
haftmann
parents: 21858
diff changeset
   669
         writeln "";
dfafcd6223ad whitespace tuned
haftmann
parents: 21858
diff changeset
   670
         write_constraints cs)
16784
92ff7c903585 - added cplex package to HOL/Matrix
obua
parents:
diff changeset
   671
22951
dfafcd6223ad whitespace tuned
haftmann
parents: 21858
diff changeset
   672
    fun write_bounds [] = ()
dfafcd6223ad whitespace tuned
haftmann
parents: 21858
diff changeset
   673
      | write_bounds ((cplexBounds (t1,c1,t2,c2,t3))::bs) =
dfafcd6223ad whitespace tuned
haftmann
parents: 21858
diff changeset
   674
        ((if t1 = cplexNeg cplexInf andalso t3 = cplexInf
dfafcd6223ad whitespace tuned
haftmann
parents: 21858
diff changeset
   675
         andalso (c1 = cplexLeq orelse c1 = cplexLe)
dfafcd6223ad whitespace tuned
haftmann
parents: 21858
diff changeset
   676
         andalso (c2 = cplexLeq orelse c2 = cplexLe)
dfafcd6223ad whitespace tuned
haftmann
parents: 21858
diff changeset
   677
          then
dfafcd6223ad whitespace tuned
haftmann
parents: 21858
diff changeset
   678
          (write_term t2; write " free")
dfafcd6223ad whitespace tuned
haftmann
parents: 21858
diff changeset
   679
          else
dfafcd6223ad whitespace tuned
haftmann
parents: 21858
diff changeset
   680
          (write_term t1; write " "; write_cmp c1; write " ";
dfafcd6223ad whitespace tuned
haftmann
parents: 21858
diff changeset
   681
           write_term t2; write " "; write_cmp c2; write " ";
dfafcd6223ad whitespace tuned
haftmann
parents: 21858
diff changeset
   682
           write_term t3)
dfafcd6223ad whitespace tuned
haftmann
parents: 21858
diff changeset
   683
         ); writeln ""; write_bounds bs)
dfafcd6223ad whitespace tuned
haftmann
parents: 21858
diff changeset
   684
      | write_bounds ((cplexBound (t1, c, t2)) :: bs) =
dfafcd6223ad whitespace tuned
haftmann
parents: 21858
diff changeset
   685
        (write_term t1; write " ";
dfafcd6223ad whitespace tuned
haftmann
parents: 21858
diff changeset
   686
         write_cmp c; write " ";
dfafcd6223ad whitespace tuned
haftmann
parents: 21858
diff changeset
   687
         write_term t2; writeln ""; write_bounds bs)
dfafcd6223ad whitespace tuned
haftmann
parents: 21858
diff changeset
   688
dfafcd6223ad whitespace tuned
haftmann
parents: 21858
diff changeset
   689
    val _ = write_goal goal
16784
92ff7c903585 - added cplex package to HOL/Matrix
obua
parents:
diff changeset
   690
        val _ = (writeln ""; writeln "ST")
22951
dfafcd6223ad whitespace tuned
haftmann
parents: 21858
diff changeset
   691
    val _ = write_constraints constraints
16784
92ff7c903585 - added cplex package to HOL/Matrix
obua
parents:
diff changeset
   692
        val _ = (writeln ""; writeln "BOUNDS")
22951
dfafcd6223ad whitespace tuned
haftmann
parents: 21858
diff changeset
   693
    val _ = write_bounds bounds
dfafcd6223ad whitespace tuned
haftmann
parents: 21858
diff changeset
   694
        val _ = (writeln ""; writeln "END")
16784
92ff7c903585 - added cplex package to HOL/Matrix
obua
parents:
diff changeset
   695
        val _ = TextIO.closeOut f
92ff7c903585 - added cplex package to HOL/Matrix
obua
parents:
diff changeset
   696
    in
22951
dfafcd6223ad whitespace tuned
haftmann
parents: 21858
diff changeset
   697
    ()
16784
92ff7c903585 - added cplex package to HOL/Matrix
obua
parents:
diff changeset
   698
    end
92ff7c903585 - added cplex package to HOL/Matrix
obua
parents:
diff changeset
   699
22951
dfafcd6223ad whitespace tuned
haftmann
parents: 21858
diff changeset
   700
fun norm_Constr (constr as cplexConstr (c, (t1, t2))) =
dfafcd6223ad whitespace tuned
haftmann
parents: 21858
diff changeset
   701
    if not (modulo_signed is_Num t2) andalso
dfafcd6223ad whitespace tuned
haftmann
parents: 21858
diff changeset
   702
       modulo_signed is_Num t1
16784
92ff7c903585 - added cplex package to HOL/Matrix
obua
parents:
diff changeset
   703
    then
22951
dfafcd6223ad whitespace tuned
haftmann
parents: 21858
diff changeset
   704
    [cplexConstr (rev_cmp c, (t2, t1))]
16784
92ff7c903585 - added cplex package to HOL/Matrix
obua
parents:
diff changeset
   705
    else if (c = cplexLe orelse c = cplexLeq) andalso
22951
dfafcd6223ad whitespace tuned
haftmann
parents: 21858
diff changeset
   706
        (t1 = (cplexNeg cplexInf) orelse t2 = cplexInf)
dfafcd6223ad whitespace tuned
haftmann
parents: 21858
diff changeset
   707
    then
dfafcd6223ad whitespace tuned
haftmann
parents: 21858
diff changeset
   708
    []
16784
92ff7c903585 - added cplex package to HOL/Matrix
obua
parents:
diff changeset
   709
    else if (c = cplexGe orelse c = cplexGeq) andalso
22951
dfafcd6223ad whitespace tuned
haftmann
parents: 21858
diff changeset
   710
        (t1 = cplexInf orelse t2 = cplexNeg cplexInf)
16784
92ff7c903585 - added cplex package to HOL/Matrix
obua
parents:
diff changeset
   711
    then
22951
dfafcd6223ad whitespace tuned
haftmann
parents: 21858
diff changeset
   712
    []
16784
92ff7c903585 - added cplex package to HOL/Matrix
obua
parents:
diff changeset
   713
    else
22951
dfafcd6223ad whitespace tuned
haftmann
parents: 21858
diff changeset
   714
    [constr]
16784
92ff7c903585 - added cplex package to HOL/Matrix
obua
parents:
diff changeset
   715
92ff7c903585 - added cplex package to HOL/Matrix
obua
parents:
diff changeset
   716
fun bound2constr (cplexBounds (t1,c1,t2,c2,t3)) =
92ff7c903585 - added cplex package to HOL/Matrix
obua
parents:
diff changeset
   717
    (norm_Constr(cplexConstr (c1, (t1, t2))))
92ff7c903585 - added cplex package to HOL/Matrix
obua
parents:
diff changeset
   718
    @ (norm_Constr(cplexConstr (c2, (t2, t3))))
92ff7c903585 - added cplex package to HOL/Matrix
obua
parents:
diff changeset
   719
  | bound2constr (cplexBound (t1, cplexEq, t2)) =
92ff7c903585 - added cplex package to HOL/Matrix
obua
parents:
diff changeset
   720
    (norm_Constr(cplexConstr (cplexLeq, (t1, t2))))
92ff7c903585 - added cplex package to HOL/Matrix
obua
parents:
diff changeset
   721
    @ (norm_Constr(cplexConstr (cplexLeq, (t2, t1))))
22951
dfafcd6223ad whitespace tuned
haftmann
parents: 21858
diff changeset
   722
  | bound2constr (cplexBound (t1, c1, t2)) =
16784
92ff7c903585 - added cplex package to HOL/Matrix
obua
parents:
diff changeset
   723
    norm_Constr(cplexConstr (c1, (t1,t2)))
92ff7c903585 - added cplex package to HOL/Matrix
obua
parents:
diff changeset
   724
92ff7c903585 - added cplex package to HOL/Matrix
obua
parents:
diff changeset
   725
val emptyset = Symtab.empty
92ff7c903585 - added cplex package to HOL/Matrix
obua
parents:
diff changeset
   726
17412
e26cb20ef0cc TableFun/Symtab: curried lookup and update;
wenzelm
parents: 16966
diff changeset
   727
fun singleton v = Symtab.update (v, ()) emptyset
16784
92ff7c903585 - added cplex package to HOL/Matrix
obua
parents:
diff changeset
   728
92ff7c903585 - added cplex package to HOL/Matrix
obua
parents:
diff changeset
   729
fun merge a b = Symtab.merge (op =) (a, b)
92ff7c903585 - added cplex package to HOL/Matrix
obua
parents:
diff changeset
   730
21056
2cfe839e8d58 Symtab.foldl replaced by Symtab.fold
haftmann
parents: 17521
diff changeset
   731
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
   732
37116
e32cc5958282 tuned -- avoid catch-all exception pattern;
wenzelm
parents: 35010
diff changeset
   733
fun diff a b = Symtab.fold (Symtab.delete_safe o fst) b a
22951
dfafcd6223ad whitespace tuned
haftmann
parents: 21858
diff changeset
   734
16784
92ff7c903585 - added cplex package to HOL/Matrix
obua
parents:
diff changeset
   735
fun collect_vars (cplexVar v) = singleton v
92ff7c903585 - added cplex package to HOL/Matrix
obua
parents:
diff changeset
   736
  | collect_vars (cplexNeg t) = collect_vars t
22951
dfafcd6223ad whitespace tuned
haftmann
parents: 21858
diff changeset
   737
  | collect_vars (cplexProd (t1, t2)) =
16784
92ff7c903585 - added cplex package to HOL/Matrix
obua
parents:
diff changeset
   738
    merge (collect_vars t1) (collect_vars t2)
92ff7c903585 - added cplex package to HOL/Matrix
obua
parents:
diff changeset
   739
  | collect_vars (cplexSum ts) = mergemap collect_vars ts
92ff7c903585 - added cplex package to HOL/Matrix
obua
parents:
diff changeset
   740
  | collect_vars _ = emptyset
92ff7c903585 - added cplex package to HOL/Matrix
obua
parents:
diff changeset
   741
92ff7c903585 - added cplex package to HOL/Matrix
obua
parents:
diff changeset
   742
(* Eliminates all nonfree bounds from the linear program and produces an
22951
dfafcd6223ad whitespace tuned
haftmann
parents: 21858
diff changeset
   743
   equivalent program with only free bounds
16784
92ff7c903585 - added cplex package to HOL/Matrix
obua
parents:
diff changeset
   744
   IF for the input program P holds: is_normed_cplexProg P *)
92ff7c903585 - added cplex package to HOL/Matrix
obua
parents:
diff changeset
   745
fun elim_nonfree_bounds (cplexProg (name, goal, constraints, bounds)) =
92ff7c903585 - added cplex package to HOL/Matrix
obua
parents:
diff changeset
   746
    let
22951
dfafcd6223ad whitespace tuned
haftmann
parents: 21858
diff changeset
   747
    fun collect_constr_vars (_, cplexConstr (c, (t1,_))) =
dfafcd6223ad whitespace tuned
haftmann
parents: 21858
diff changeset
   748
        (collect_vars t1)
dfafcd6223ad whitespace tuned
haftmann
parents: 21858
diff changeset
   749
dfafcd6223ad whitespace tuned
haftmann
parents: 21858
diff changeset
   750
    val cvars = merge (collect_vars (term_of_goal goal))
dfafcd6223ad whitespace tuned
haftmann
parents: 21858
diff changeset
   751
              (mergemap collect_constr_vars constraints)
dfafcd6223ad whitespace tuned
haftmann
parents: 21858
diff changeset
   752
dfafcd6223ad whitespace tuned
haftmann
parents: 21858
diff changeset
   753
    fun collect_lower_bounded_vars
dfafcd6223ad whitespace tuned
haftmann
parents: 21858
diff changeset
   754
        (cplexBounds (t1, c1, cplexVar v, c2, t3)) =
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 (_, cplexLe, 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 (_, cplexLeq, cplexVar v)) =
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, cplexGe,_)) =
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, cplexGeq, _)) =
dfafcd6223ad whitespace tuned
haftmann
parents: 21858
diff changeset
   767
         singleton v
dfafcd6223ad whitespace tuned
haftmann
parents: 21858
diff changeset
   768
      | collect_lower_bounded_vars
dfafcd6223ad whitespace tuned
haftmann
parents: 21858
diff changeset
   769
        (cplexBound (cplexVar v, cplexEq, _)) =
dfafcd6223ad whitespace tuned
haftmann
parents: 21858
diff changeset
   770
        singleton v
dfafcd6223ad whitespace tuned
haftmann
parents: 21858
diff changeset
   771
      |  collect_lower_bounded_vars _ = emptyset
dfafcd6223ad whitespace tuned
haftmann
parents: 21858
diff changeset
   772
dfafcd6223ad whitespace tuned
haftmann
parents: 21858
diff changeset
   773
    val lvars = mergemap collect_lower_bounded_vars bounds
dfafcd6223ad whitespace tuned
haftmann
parents: 21858
diff changeset
   774
    val positive_vars = diff cvars lvars
dfafcd6223ad whitespace tuned
haftmann
parents: 21858
diff changeset
   775
    val zero = cplexNum "0"
dfafcd6223ad whitespace tuned
haftmann
parents: 21858
diff changeset
   776
dfafcd6223ad whitespace tuned
haftmann
parents: 21858
diff changeset
   777
    fun make_pos_constr v =
dfafcd6223ad whitespace tuned
haftmann
parents: 21858
diff changeset
   778
        (NONE, cplexConstr (cplexGeq, ((cplexVar v), zero)))
dfafcd6223ad whitespace tuned
haftmann
parents: 21858
diff changeset
   779
dfafcd6223ad whitespace tuned
haftmann
parents: 21858
diff changeset
   780
    fun make_free_bound v =
dfafcd6223ad whitespace tuned
haftmann
parents: 21858
diff changeset
   781
        cplexBounds (cplexNeg cplexInf, cplexLeq,
dfafcd6223ad whitespace tuned
haftmann
parents: 21858
diff changeset
   782
             cplexVar v, cplexLeq,
dfafcd6223ad whitespace tuned
haftmann
parents: 21858
diff changeset
   783
             cplexInf)
dfafcd6223ad whitespace tuned
haftmann
parents: 21858
diff changeset
   784
dfafcd6223ad whitespace tuned
haftmann
parents: 21858
diff changeset
   785
    val pos_constrs = rev (Symtab.fold
dfafcd6223ad whitespace tuned
haftmann
parents: 21858
diff changeset
   786
                  (fn (k, v) => cons (make_pos_constr k))
dfafcd6223ad whitespace tuned
haftmann
parents: 21858
diff changeset
   787
                  positive_vars [])
21056
2cfe839e8d58 Symtab.foldl replaced by Symtab.fold
haftmann
parents: 17521
diff changeset
   788
        val bound_constrs = map (pair NONE)
22951
dfafcd6223ad whitespace tuned
haftmann
parents: 21858
diff changeset
   789
                (maps bound2constr bounds)
dfafcd6223ad whitespace tuned
haftmann
parents: 21858
diff changeset
   790
    val constraints' = constraints @ pos_constrs @ bound_constrs
dfafcd6223ad whitespace tuned
haftmann
parents: 21858
diff changeset
   791
    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
   792
    in
22951
dfafcd6223ad whitespace tuned
haftmann
parents: 21858
diff changeset
   793
    cplexProg (name, goal, constraints', bounds')
16784
92ff7c903585 - added cplex package to HOL/Matrix
obua
parents:
diff changeset
   794
    end
92ff7c903585 - added cplex package to HOL/Matrix
obua
parents:
diff changeset
   795
22951
dfafcd6223ad whitespace tuned
haftmann
parents: 21858
diff changeset
   796
fun relax_strict_ineqs (cplexProg (name, goals, constrs, bounds)) =
16784
92ff7c903585 - added cplex package to HOL/Matrix
obua
parents:
diff changeset
   797
    let
22951
dfafcd6223ad whitespace tuned
haftmann
parents: 21858
diff changeset
   798
    fun relax cplexLe = cplexLeq
dfafcd6223ad whitespace tuned
haftmann
parents: 21858
diff changeset
   799
      | relax cplexGe = cplexGeq
dfafcd6223ad whitespace tuned
haftmann
parents: 21858
diff changeset
   800
      | relax x = x
dfafcd6223ad whitespace tuned
haftmann
parents: 21858
diff changeset
   801
dfafcd6223ad whitespace tuned
haftmann
parents: 21858
diff changeset
   802
    fun relax_constr (n, cplexConstr(c, (t1, t2))) =
dfafcd6223ad whitespace tuned
haftmann
parents: 21858
diff changeset
   803
        (n, cplexConstr(relax c, (t1, t2)))
dfafcd6223ad whitespace tuned
haftmann
parents: 21858
diff changeset
   804
dfafcd6223ad whitespace tuned
haftmann
parents: 21858
diff changeset
   805
    fun relax_bounds (cplexBounds (t1, c1, t2, c2, t3)) =
dfafcd6223ad whitespace tuned
haftmann
parents: 21858
diff changeset
   806
        cplexBounds (t1, relax c1, t2, relax c2, t3)
dfafcd6223ad whitespace tuned
haftmann
parents: 21858
diff changeset
   807
      | relax_bounds (cplexBound (t1, c, t2)) =
dfafcd6223ad whitespace tuned
haftmann
parents: 21858
diff changeset
   808
        cplexBound (t1, relax c, t2)
16784
92ff7c903585 - added cplex package to HOL/Matrix
obua
parents:
diff changeset
   809
    in
22951
dfafcd6223ad whitespace tuned
haftmann
parents: 21858
diff changeset
   810
    cplexProg (name,
dfafcd6223ad whitespace tuned
haftmann
parents: 21858
diff changeset
   811
           goals,
dfafcd6223ad whitespace tuned
haftmann
parents: 21858
diff changeset
   812
           map relax_constr constrs,
dfafcd6223ad whitespace tuned
haftmann
parents: 21858
diff changeset
   813
           map relax_bounds bounds)
16784
92ff7c903585 - added cplex package to HOL/Matrix
obua
parents:
diff changeset
   814
    end
92ff7c903585 - added cplex package to HOL/Matrix
obua
parents:
diff changeset
   815
22951
dfafcd6223ad whitespace tuned
haftmann
parents: 21858
diff changeset
   816
datatype cplexResult = Unbounded
dfafcd6223ad whitespace tuned
haftmann
parents: 21858
diff changeset
   817
             | Infeasible
dfafcd6223ad whitespace tuned
haftmann
parents: 21858
diff changeset
   818
             | Undefined
dfafcd6223ad whitespace tuned
haftmann
parents: 21858
diff changeset
   819
             | Optimal of string * ((string * string) list)
16784
92ff7c903585 - added cplex package to HOL/Matrix
obua
parents:
diff changeset
   820
92ff7c903585 - added cplex package to HOL/Matrix
obua
parents:
diff changeset
   821
fun is_separator x = forall (fn c => c = #"-") (String.explode x)
92ff7c903585 - added cplex package to HOL/Matrix
obua
parents:
diff changeset
   822
92ff7c903585 - added cplex package to HOL/Matrix
obua
parents:
diff changeset
   823
fun is_sign x = (x = "+" orelse x = "-")
92ff7c903585 - added cplex package to HOL/Matrix
obua
parents:
diff changeset
   824
92ff7c903585 - added cplex package to HOL/Matrix
obua
parents:
diff changeset
   825
fun is_colon x = (x = ":")
92ff7c903585 - added cplex package to HOL/Matrix
obua
parents:
diff changeset
   826
22951
dfafcd6223ad whitespace tuned
haftmann
parents: 21858
diff changeset
   827
fun is_resultsymbol a =
16784
92ff7c903585 - added cplex package to HOL/Matrix
obua
parents:
diff changeset
   828
    let
22951
dfafcd6223ad whitespace tuned
haftmann
parents: 21858
diff changeset
   829
    val symbol_char = String.explode "!\"#$%&()/,.;?@_`'{}|~-"
dfafcd6223ad whitespace tuned
haftmann
parents: 21858
diff changeset
   830
    fun is_symbol_char c = Char.isAlphaNum c orelse
dfafcd6223ad whitespace tuned
haftmann
parents: 21858
diff changeset
   831
                   exists (fn d => d=c) symbol_char
dfafcd6223ad whitespace tuned
haftmann
parents: 21858
diff changeset
   832
    fun is_symbol_start c = is_symbol_char c andalso
dfafcd6223ad whitespace tuned
haftmann
parents: 21858
diff changeset
   833
                not (Char.isDigit c) andalso
dfafcd6223ad whitespace tuned
haftmann
parents: 21858
diff changeset
   834
                not (c= #".") andalso
dfafcd6223ad whitespace tuned
haftmann
parents: 21858
diff changeset
   835
                not (c= #"-")
dfafcd6223ad whitespace tuned
haftmann
parents: 21858
diff changeset
   836
    val b = String.explode a
16784
92ff7c903585 - added cplex package to HOL/Matrix
obua
parents:
diff changeset
   837
    in
22951
dfafcd6223ad whitespace tuned
haftmann
parents: 21858
diff changeset
   838
    b <> [] andalso is_symbol_start (hd b) andalso
dfafcd6223ad whitespace tuned
haftmann
parents: 21858
diff changeset
   839
    forall is_symbol_char b
16784
92ff7c903585 - added cplex package to HOL/Matrix
obua
parents:
diff changeset
   840
    end
92ff7c903585 - added cplex package to HOL/Matrix
obua
parents:
diff changeset
   841
92ff7c903585 - added cplex package to HOL/Matrix
obua
parents:
diff changeset
   842
val TOKEN_SIGN = 100
92ff7c903585 - added cplex package to HOL/Matrix
obua
parents:
diff changeset
   843
val TOKEN_COLON = 101
92ff7c903585 - added cplex package to HOL/Matrix
obua
parents:
diff changeset
   844
val TOKEN_SEPARATOR = 102
92ff7c903585 - added cplex package to HOL/Matrix
obua
parents:
diff changeset
   845
22951
dfafcd6223ad whitespace tuned
haftmann
parents: 21858
diff changeset
   846
fun load_glpkResult name =
16784
92ff7c903585 - added cplex package to HOL/Matrix
obua
parents:
diff changeset
   847
    let
22951
dfafcd6223ad whitespace tuned
haftmann
parents: 21858
diff changeset
   848
    val flist = [(is_NL, TOKEN_NL),
dfafcd6223ad whitespace tuned
haftmann
parents: 21858
diff changeset
   849
             (is_blank, TOKEN_BLANK),
dfafcd6223ad whitespace tuned
haftmann
parents: 21858
diff changeset
   850
             (is_num, TOKEN_NUM),
dfafcd6223ad whitespace tuned
haftmann
parents: 21858
diff changeset
   851
             (is_sign, TOKEN_SIGN),
16784
92ff7c903585 - added cplex package to HOL/Matrix
obua
parents:
diff changeset
   852
                     (is_colon, TOKEN_COLON),
22951
dfafcd6223ad whitespace tuned
haftmann
parents: 21858
diff changeset
   853
             (is_cmp, TOKEN_CMP),
dfafcd6223ad whitespace tuned
haftmann
parents: 21858
diff changeset
   854
             (is_resultsymbol, TOKEN_SYMBOL),
dfafcd6223ad whitespace tuned
haftmann
parents: 21858
diff changeset
   855
             (is_separator, TOKEN_SEPARATOR)]
dfafcd6223ad whitespace tuned
haftmann
parents: 21858
diff changeset
   856
dfafcd6223ad whitespace tuned
haftmann
parents: 21858
diff changeset
   857
    val tokenize = tokenize_general flist
dfafcd6223ad whitespace tuned
haftmann
parents: 21858
diff changeset
   858
dfafcd6223ad whitespace tuned
haftmann
parents: 21858
diff changeset
   859
    val f = TextIO.openIn name
dfafcd6223ad whitespace tuned
haftmann
parents: 21858
diff changeset
   860
32740
9dd0a2f83429 explicit indication of Unsynchronized.ref;
wenzelm
parents: 32491
diff changeset
   861
    val rest = Unsynchronized.ref []
16784
92ff7c903585 - added cplex package to HOL/Matrix
obua
parents:
diff changeset
   862
22951
dfafcd6223ad whitespace tuned
haftmann
parents: 21858
diff changeset
   863
    fun readToken_helper () =
dfafcd6223ad whitespace tuned
haftmann
parents: 21858
diff changeset
   864
        if length (!rest) > 0 then
dfafcd6223ad whitespace tuned
haftmann
parents: 21858
diff changeset
   865
        let val u = hd (!rest) in
dfafcd6223ad whitespace tuned
haftmann
parents: 21858
diff changeset
   866
            (
dfafcd6223ad whitespace tuned
haftmann
parents: 21858
diff changeset
   867
             rest := tl (!rest);
dfafcd6223ad whitespace tuned
haftmann
parents: 21858
diff changeset
   868
             SOME u
dfafcd6223ad whitespace tuned
haftmann
parents: 21858
diff changeset
   869
            )
dfafcd6223ad whitespace tuned
haftmann
parents: 21858
diff changeset
   870
        end
dfafcd6223ad whitespace tuned
haftmann
parents: 21858
diff changeset
   871
        else
23139
aa899bce7c3b TextIO.inputLine: use present SML B library version;
wenzelm
parents: 22951
diff changeset
   872
        (case TextIO.inputLine f of
aa899bce7c3b TextIO.inputLine: use present SML B library version;
wenzelm
parents: 22951
diff changeset
   873
          NONE => NONE
aa899bce7c3b TextIO.inputLine: use present SML B library version;
wenzelm
parents: 22951
diff changeset
   874
        | SOME s => (rest := tokenize s; readToken_helper()))
16784
92ff7c903585 - added cplex package to HOL/Matrix
obua
parents:
diff changeset
   875
22951
dfafcd6223ad whitespace tuned
haftmann
parents: 21858
diff changeset
   876
    fun is_tt tok ty = (tok <> NONE andalso (fst (the tok)) = ty)
16784
92ff7c903585 - added cplex package to HOL/Matrix
obua
parents:
diff changeset
   877
22951
dfafcd6223ad whitespace tuned
haftmann
parents: 21858
diff changeset
   878
    fun pushToken a = if a = NONE then () else (rest := ((the a)::(!rest)))
16784
92ff7c903585 - added cplex package to HOL/Matrix
obua
parents:
diff changeset
   879
22951
dfafcd6223ad whitespace tuned
haftmann
parents: 21858
diff changeset
   880
    fun readToken () =
dfafcd6223ad whitespace tuned
haftmann
parents: 21858
diff changeset
   881
        let val t = readToken_helper () in
dfafcd6223ad whitespace tuned
haftmann
parents: 21858
diff changeset
   882
        if is_tt t TOKEN_BLANK then
dfafcd6223ad whitespace tuned
haftmann
parents: 21858
diff changeset
   883
            readToken ()
dfafcd6223ad whitespace tuned
haftmann
parents: 21858
diff changeset
   884
        else if is_tt t TOKEN_NL then
dfafcd6223ad whitespace tuned
haftmann
parents: 21858
diff changeset
   885
            let val t2 = readToken_helper () in
dfafcd6223ad whitespace tuned
haftmann
parents: 21858
diff changeset
   886
            if is_tt t2 TOKEN_SIGN then
dfafcd6223ad whitespace tuned
haftmann
parents: 21858
diff changeset
   887
                (pushToken (SOME (TOKEN_SEPARATOR, "-")); t)
dfafcd6223ad whitespace tuned
haftmann
parents: 21858
diff changeset
   888
            else
dfafcd6223ad whitespace tuned
haftmann
parents: 21858
diff changeset
   889
                (pushToken t2; t)
dfafcd6223ad whitespace tuned
haftmann
parents: 21858
diff changeset
   890
            end
dfafcd6223ad whitespace tuned
haftmann
parents: 21858
diff changeset
   891
        else if is_tt t TOKEN_SIGN then
dfafcd6223ad whitespace tuned
haftmann
parents: 21858
diff changeset
   892
            let val t2 = readToken_helper () in
dfafcd6223ad whitespace tuned
haftmann
parents: 21858
diff changeset
   893
            if is_tt t2 TOKEN_NUM then
dfafcd6223ad whitespace tuned
haftmann
parents: 21858
diff changeset
   894
                (SOME (TOKEN_NUM, (snd (the t))^(snd (the t2))))
dfafcd6223ad whitespace tuned
haftmann
parents: 21858
diff changeset
   895
            else
dfafcd6223ad whitespace tuned
haftmann
parents: 21858
diff changeset
   896
                (pushToken t2; t)
dfafcd6223ad whitespace tuned
haftmann
parents: 21858
diff changeset
   897
            end
dfafcd6223ad whitespace tuned
haftmann
parents: 21858
diff changeset
   898
        else
dfafcd6223ad whitespace tuned
haftmann
parents: 21858
diff changeset
   899
            t
dfafcd6223ad whitespace tuned
haftmann
parents: 21858
diff changeset
   900
        end
dfafcd6223ad whitespace tuned
haftmann
parents: 21858
diff changeset
   901
dfafcd6223ad whitespace tuned
haftmann
parents: 21858
diff changeset
   902
        fun readRestOfLine P =
dfafcd6223ad whitespace tuned
haftmann
parents: 21858
diff changeset
   903
        let
dfafcd6223ad whitespace tuned
haftmann
parents: 21858
diff changeset
   904
        val t = readToken ()
dfafcd6223ad whitespace tuned
haftmann
parents: 21858
diff changeset
   905
        in
dfafcd6223ad whitespace tuned
haftmann
parents: 21858
diff changeset
   906
        if is_tt t TOKEN_NL orelse t = NONE
dfafcd6223ad whitespace tuned
haftmann
parents: 21858
diff changeset
   907
        then P
dfafcd6223ad whitespace tuned
haftmann
parents: 21858
diff changeset
   908
        else readRestOfLine P
dfafcd6223ad whitespace tuned
haftmann
parents: 21858
diff changeset
   909
        end
16784
92ff7c903585 - added cplex package to HOL/Matrix
obua
parents:
diff changeset
   910
22951
dfafcd6223ad whitespace tuned
haftmann
parents: 21858
diff changeset
   911
    fun readHeader () =
dfafcd6223ad whitespace tuned
haftmann
parents: 21858
diff changeset
   912
        let
dfafcd6223ad whitespace tuned
haftmann
parents: 21858
diff changeset
   913
        fun readStatus () = readRestOfLine ("STATUS", snd (the (readToken ())))
dfafcd6223ad whitespace tuned
haftmann
parents: 21858
diff changeset
   914
        fun readObjective () = readRestOfLine ("OBJECTIVE", snd (the (readToken (); readToken (); readToken ())))
dfafcd6223ad whitespace tuned
haftmann
parents: 21858
diff changeset
   915
        val t1 = readToken ()
dfafcd6223ad whitespace tuned
haftmann
parents: 21858
diff changeset
   916
        val t2 = readToken ()
dfafcd6223ad whitespace tuned
haftmann
parents: 21858
diff changeset
   917
        in
dfafcd6223ad whitespace tuned
haftmann
parents: 21858
diff changeset
   918
        if is_tt t1 TOKEN_SYMBOL andalso is_tt t2 TOKEN_COLON
dfafcd6223ad whitespace tuned
haftmann
parents: 21858
diff changeset
   919
        then
dfafcd6223ad whitespace tuned
haftmann
parents: 21858
diff changeset
   920
            case to_upper (snd (the t1)) of
dfafcd6223ad whitespace tuned
haftmann
parents: 21858
diff changeset
   921
            "STATUS" => (readStatus ())::(readHeader ())
dfafcd6223ad whitespace tuned
haftmann
parents: 21858
diff changeset
   922
              | "OBJECTIVE" => (readObjective())::(readHeader ())
dfafcd6223ad whitespace tuned
haftmann
parents: 21858
diff changeset
   923
              | _ => (readRestOfLine (); readHeader ())
dfafcd6223ad whitespace tuned
haftmann
parents: 21858
diff changeset
   924
        else
dfafcd6223ad whitespace tuned
haftmann
parents: 21858
diff changeset
   925
            (pushToken t2; pushToken t1; [])
dfafcd6223ad whitespace tuned
haftmann
parents: 21858
diff changeset
   926
        end
16784
92ff7c903585 - added cplex package to HOL/Matrix
obua
parents:
diff changeset
   927
22951
dfafcd6223ad whitespace tuned
haftmann
parents: 21858
diff changeset
   928
    fun skip_until_sep () =
dfafcd6223ad whitespace tuned
haftmann
parents: 21858
diff changeset
   929
        let val x = readToken () in
dfafcd6223ad whitespace tuned
haftmann
parents: 21858
diff changeset
   930
        if is_tt x TOKEN_SEPARATOR then
dfafcd6223ad whitespace tuned
haftmann
parents: 21858
diff changeset
   931
            readRestOfLine ()
dfafcd6223ad whitespace tuned
haftmann
parents: 21858
diff changeset
   932
        else
dfafcd6223ad whitespace tuned
haftmann
parents: 21858
diff changeset
   933
            skip_until_sep ()
dfafcd6223ad whitespace tuned
haftmann
parents: 21858
diff changeset
   934
        end
16784
92ff7c903585 - added cplex package to HOL/Matrix
obua
parents:
diff changeset
   935
22951
dfafcd6223ad whitespace tuned
haftmann
parents: 21858
diff changeset
   936
    fun load_value () =
dfafcd6223ad whitespace tuned
haftmann
parents: 21858
diff changeset
   937
        let
dfafcd6223ad whitespace tuned
haftmann
parents: 21858
diff changeset
   938
        val t1 = readToken ()
dfafcd6223ad whitespace tuned
haftmann
parents: 21858
diff changeset
   939
        val t2 = readToken ()
dfafcd6223ad whitespace tuned
haftmann
parents: 21858
diff changeset
   940
        in
dfafcd6223ad whitespace tuned
haftmann
parents: 21858
diff changeset
   941
        if is_tt t1 TOKEN_NUM andalso is_tt t2 TOKEN_SYMBOL then
dfafcd6223ad whitespace tuned
haftmann
parents: 21858
diff changeset
   942
            let
dfafcd6223ad whitespace tuned
haftmann
parents: 21858
diff changeset
   943
            val t = readToken ()
dfafcd6223ad whitespace tuned
haftmann
parents: 21858
diff changeset
   944
            val state = if is_tt t TOKEN_NL then readToken () else t
dfafcd6223ad whitespace tuned
haftmann
parents: 21858
diff changeset
   945
            val _ = if is_tt state TOKEN_SYMBOL then () else raise (Load_cplexResult "state expected")
dfafcd6223ad whitespace tuned
haftmann
parents: 21858
diff changeset
   946
            val k = readToken ()
dfafcd6223ad whitespace tuned
haftmann
parents: 21858
diff changeset
   947
            in
dfafcd6223ad whitespace tuned
haftmann
parents: 21858
diff changeset
   948
            if is_tt k TOKEN_NUM then
dfafcd6223ad whitespace tuned
haftmann
parents: 21858
diff changeset
   949
                readRestOfLine (SOME (snd (the t2), snd (the k)))
dfafcd6223ad whitespace tuned
haftmann
parents: 21858
diff changeset
   950
            else
dfafcd6223ad whitespace tuned
haftmann
parents: 21858
diff changeset
   951
                raise (Load_cplexResult "number expected")
dfafcd6223ad whitespace tuned
haftmann
parents: 21858
diff changeset
   952
            end
dfafcd6223ad whitespace tuned
haftmann
parents: 21858
diff changeset
   953
        else
dfafcd6223ad whitespace tuned
haftmann
parents: 21858
diff changeset
   954
            (pushToken t2; pushToken t1; NONE)
dfafcd6223ad whitespace tuned
haftmann
parents: 21858
diff changeset
   955
        end
16784
92ff7c903585 - added cplex package to HOL/Matrix
obua
parents:
diff changeset
   956
22951
dfafcd6223ad whitespace tuned
haftmann
parents: 21858
diff changeset
   957
    fun load_values () =
dfafcd6223ad whitespace tuned
haftmann
parents: 21858
diff changeset
   958
        let val v = load_value () in
dfafcd6223ad whitespace tuned
haftmann
parents: 21858
diff changeset
   959
        if v = NONE then [] else (the v)::(load_values ())
dfafcd6223ad whitespace tuned
haftmann
parents: 21858
diff changeset
   960
        end
dfafcd6223ad whitespace tuned
haftmann
parents: 21858
diff changeset
   961
dfafcd6223ad whitespace tuned
haftmann
parents: 21858
diff changeset
   962
    val header = readHeader ()
16784
92ff7c903585 - added cplex package to HOL/Matrix
obua
parents:
diff changeset
   963
22951
dfafcd6223ad whitespace tuned
haftmann
parents: 21858
diff changeset
   964
    val result =
dfafcd6223ad whitespace tuned
haftmann
parents: 21858
diff changeset
   965
        case AList.lookup (op =) header "STATUS" of
dfafcd6223ad whitespace tuned
haftmann
parents: 21858
diff changeset
   966
        SOME "INFEASIBLE" => Infeasible
dfafcd6223ad whitespace tuned
haftmann
parents: 21858
diff changeset
   967
          | SOME "UNBOUNDED" => Unbounded
dfafcd6223ad whitespace tuned
haftmann
parents: 21858
diff changeset
   968
          | SOME "OPTIMAL" => Optimal (the (AList.lookup (op =) header "OBJECTIVE"),
dfafcd6223ad whitespace tuned
haftmann
parents: 21858
diff changeset
   969
                       (skip_until_sep ();
dfafcd6223ad whitespace tuned
haftmann
parents: 21858
diff changeset
   970
                        skip_until_sep ();
dfafcd6223ad whitespace tuned
haftmann
parents: 21858
diff changeset
   971
                        load_values ()))
dfafcd6223ad whitespace tuned
haftmann
parents: 21858
diff changeset
   972
          | _ => Undefined
16784
92ff7c903585 - added cplex package to HOL/Matrix
obua
parents:
diff changeset
   973
22951
dfafcd6223ad whitespace tuned
haftmann
parents: 21858
diff changeset
   974
    val _ = TextIO.closeIn f
16784
92ff7c903585 - added cplex package to HOL/Matrix
obua
parents:
diff changeset
   975
    in
22951
dfafcd6223ad whitespace tuned
haftmann
parents: 21858
diff changeset
   976
    result
16784
92ff7c903585 - added cplex package to HOL/Matrix
obua
parents:
diff changeset
   977
    end
92ff7c903585 - added cplex package to HOL/Matrix
obua
parents:
diff changeset
   978
    handle (Tokenize s) => raise (Load_cplexResult ("Tokenize: "^s))
22951
dfafcd6223ad whitespace tuned
haftmann
parents: 21858
diff changeset
   979
     | Option => raise (Load_cplexResult "Option")
dfafcd6223ad whitespace tuned
haftmann
parents: 21858
diff changeset
   980
     | x => raise x
16784
92ff7c903585 - added cplex package to HOL/Matrix
obua
parents:
diff changeset
   981
22951
dfafcd6223ad whitespace tuned
haftmann
parents: 21858
diff changeset
   982
fun load_cplexResult name =
16784
92ff7c903585 - added cplex package to HOL/Matrix
obua
parents:
diff changeset
   983
    let
22951
dfafcd6223ad whitespace tuned
haftmann
parents: 21858
diff changeset
   984
    val flist = [(is_NL, TOKEN_NL),
dfafcd6223ad whitespace tuned
haftmann
parents: 21858
diff changeset
   985
             (is_blank, TOKEN_BLANK),
dfafcd6223ad whitespace tuned
haftmann
parents: 21858
diff changeset
   986
             (is_num, TOKEN_NUM),
dfafcd6223ad whitespace tuned
haftmann
parents: 21858
diff changeset
   987
             (is_sign, TOKEN_SIGN),
16784
92ff7c903585 - added cplex package to HOL/Matrix
obua
parents:
diff changeset
   988
                     (is_colon, TOKEN_COLON),
22951
dfafcd6223ad whitespace tuned
haftmann
parents: 21858
diff changeset
   989
             (is_cmp, TOKEN_CMP),
dfafcd6223ad whitespace tuned
haftmann
parents: 21858
diff changeset
   990
             (is_resultsymbol, TOKEN_SYMBOL)]
dfafcd6223ad whitespace tuned
haftmann
parents: 21858
diff changeset
   991
dfafcd6223ad whitespace tuned
haftmann
parents: 21858
diff changeset
   992
    val tokenize = tokenize_general flist
dfafcd6223ad whitespace tuned
haftmann
parents: 21858
diff changeset
   993
dfafcd6223ad whitespace tuned
haftmann
parents: 21858
diff changeset
   994
    val f = TextIO.openIn name
dfafcd6223ad whitespace tuned
haftmann
parents: 21858
diff changeset
   995
32740
9dd0a2f83429 explicit indication of Unsynchronized.ref;
wenzelm
parents: 32491
diff changeset
   996
    val rest = Unsynchronized.ref []
16784
92ff7c903585 - added cplex package to HOL/Matrix
obua
parents:
diff changeset
   997
22951
dfafcd6223ad whitespace tuned
haftmann
parents: 21858
diff changeset
   998
    fun readToken_helper () =
dfafcd6223ad whitespace tuned
haftmann
parents: 21858
diff changeset
   999
        if length (!rest) > 0 then
dfafcd6223ad whitespace tuned
haftmann
parents: 21858
diff changeset
  1000
        let val u = hd (!rest) in
dfafcd6223ad whitespace tuned
haftmann
parents: 21858
diff changeset
  1001
            (
dfafcd6223ad whitespace tuned
haftmann
parents: 21858
diff changeset
  1002
             rest := tl (!rest);
dfafcd6223ad whitespace tuned
haftmann
parents: 21858
diff changeset
  1003
             SOME u
dfafcd6223ad whitespace tuned
haftmann
parents: 21858
diff changeset
  1004
            )
dfafcd6223ad whitespace tuned
haftmann
parents: 21858
diff changeset
  1005
        end
dfafcd6223ad whitespace tuned
haftmann
parents: 21858
diff changeset
  1006
        else
23139
aa899bce7c3b TextIO.inputLine: use present SML B library version;
wenzelm
parents: 22951
diff changeset
  1007
        (case TextIO.inputLine f of
aa899bce7c3b TextIO.inputLine: use present SML B library version;
wenzelm
parents: 22951
diff changeset
  1008
          NONE => NONE
aa899bce7c3b TextIO.inputLine: use present SML B library version;
wenzelm
parents: 22951
diff changeset
  1009
        | SOME s => (rest := tokenize s; readToken_helper()))
16784
92ff7c903585 - added cplex package to HOL/Matrix
obua
parents:
diff changeset
  1010
22951
dfafcd6223ad whitespace tuned
haftmann
parents: 21858
diff changeset
  1011
    fun is_tt tok ty = (tok <> NONE andalso (fst (the tok)) = ty)
16784
92ff7c903585 - added cplex package to HOL/Matrix
obua
parents:
diff changeset
  1012
22951
dfafcd6223ad whitespace tuned
haftmann
parents: 21858
diff changeset
  1013
    fun pushToken a = if a = NONE then () else (rest := ((the a)::(!rest)))
dfafcd6223ad whitespace tuned
haftmann
parents: 21858
diff changeset
  1014
dfafcd6223ad whitespace tuned
haftmann
parents: 21858
diff changeset
  1015
    fun readToken () =
dfafcd6223ad whitespace tuned
haftmann
parents: 21858
diff changeset
  1016
        let val t = readToken_helper () in
dfafcd6223ad whitespace tuned
haftmann
parents: 21858
diff changeset
  1017
        if is_tt t TOKEN_BLANK then
dfafcd6223ad whitespace tuned
haftmann
parents: 21858
diff changeset
  1018
            readToken ()
dfafcd6223ad whitespace tuned
haftmann
parents: 21858
diff changeset
  1019
        else if is_tt t TOKEN_SIGN then
dfafcd6223ad whitespace tuned
haftmann
parents: 21858
diff changeset
  1020
            let val t2 = readToken_helper () in
dfafcd6223ad whitespace tuned
haftmann
parents: 21858
diff changeset
  1021
            if is_tt t2 TOKEN_NUM then
dfafcd6223ad whitespace tuned
haftmann
parents: 21858
diff changeset
  1022
                (SOME (TOKEN_NUM, (snd (the t))^(snd (the t2))))
dfafcd6223ad whitespace tuned
haftmann
parents: 21858
diff changeset
  1023
            else
dfafcd6223ad whitespace tuned
haftmann
parents: 21858
diff changeset
  1024
                (pushToken t2; t)
dfafcd6223ad whitespace tuned
haftmann
parents: 21858
diff changeset
  1025
            end
dfafcd6223ad whitespace tuned
haftmann
parents: 21858
diff changeset
  1026
        else
dfafcd6223ad whitespace tuned
haftmann
parents: 21858
diff changeset
  1027
            t
dfafcd6223ad whitespace tuned
haftmann
parents: 21858
diff changeset
  1028
        end
16784
92ff7c903585 - added cplex package to HOL/Matrix
obua
parents:
diff changeset
  1029
22951
dfafcd6223ad whitespace tuned
haftmann
parents: 21858
diff changeset
  1030
        fun readRestOfLine P =
dfafcd6223ad whitespace tuned
haftmann
parents: 21858
diff changeset
  1031
        let
dfafcd6223ad whitespace tuned
haftmann
parents: 21858
diff changeset
  1032
        val t = readToken ()
dfafcd6223ad whitespace tuned
haftmann
parents: 21858
diff changeset
  1033
        in
dfafcd6223ad whitespace tuned
haftmann
parents: 21858
diff changeset
  1034
        if is_tt t TOKEN_NL orelse t = NONE
dfafcd6223ad whitespace tuned
haftmann
parents: 21858
diff changeset
  1035
        then P
dfafcd6223ad whitespace tuned
haftmann
parents: 21858
diff changeset
  1036
        else readRestOfLine P
dfafcd6223ad whitespace tuned
haftmann
parents: 21858
diff changeset
  1037
        end
16784
92ff7c903585 - added cplex package to HOL/Matrix
obua
parents:
diff changeset
  1038
22951
dfafcd6223ad whitespace tuned
haftmann
parents: 21858
diff changeset
  1039
    fun readHeader () =
dfafcd6223ad whitespace tuned
haftmann
parents: 21858
diff changeset
  1040
        let
dfafcd6223ad whitespace tuned
haftmann
parents: 21858
diff changeset
  1041
        fun readStatus () = readRestOfLine ("STATUS", snd (the (readToken ())))
dfafcd6223ad whitespace tuned
haftmann
parents: 21858
diff changeset
  1042
        fun readObjective () =
dfafcd6223ad whitespace tuned
haftmann
parents: 21858
diff changeset
  1043
            let
dfafcd6223ad whitespace tuned
haftmann
parents: 21858
diff changeset
  1044
            val t = readToken ()
dfafcd6223ad whitespace tuned
haftmann
parents: 21858
diff changeset
  1045
            in
dfafcd6223ad whitespace tuned
haftmann
parents: 21858
diff changeset
  1046
            if is_tt t TOKEN_SYMBOL andalso to_upper (snd (the t)) = "VALUE" then
dfafcd6223ad whitespace tuned
haftmann
parents: 21858
diff changeset
  1047
                readRestOfLine ("OBJECTIVE", snd (the (readToken())))
dfafcd6223ad whitespace tuned
haftmann
parents: 21858
diff changeset
  1048
            else
dfafcd6223ad whitespace tuned
haftmann
parents: 21858
diff changeset
  1049
                readRestOfLine ("OBJECTIVE_NAME", snd (the t))
dfafcd6223ad whitespace tuned
haftmann
parents: 21858
diff changeset
  1050
            end
16784
92ff7c903585 - added cplex package to HOL/Matrix
obua
parents:
diff changeset
  1051
22951
dfafcd6223ad whitespace tuned
haftmann
parents: 21858
diff changeset
  1052
        val t = readToken ()
dfafcd6223ad whitespace tuned
haftmann
parents: 21858
diff changeset
  1053
        in
dfafcd6223ad whitespace tuned
haftmann
parents: 21858
diff changeset
  1054
        if is_tt t TOKEN_SYMBOL then
dfafcd6223ad whitespace tuned
haftmann
parents: 21858
diff changeset
  1055
            case to_upper (snd (the t)) of
dfafcd6223ad whitespace tuned
haftmann
parents: 21858
diff changeset
  1056
            "STATUS" => (readStatus ())::(readHeader ())
dfafcd6223ad whitespace tuned
haftmann
parents: 21858
diff changeset
  1057
              | "OBJECTIVE" => (readObjective ())::(readHeader ())
dfafcd6223ad whitespace tuned
haftmann
parents: 21858
diff changeset
  1058
              | "SECTION" => (pushToken t; [])
dfafcd6223ad whitespace tuned
haftmann
parents: 21858
diff changeset
  1059
              | _ => (readRestOfLine (); readHeader ())
dfafcd6223ad whitespace tuned
haftmann
parents: 21858
diff changeset
  1060
        else
dfafcd6223ad whitespace tuned
haftmann
parents: 21858
diff changeset
  1061
            (readRestOfLine (); readHeader ())
dfafcd6223ad whitespace tuned
haftmann
parents: 21858
diff changeset
  1062
        end
16784
92ff7c903585 - added cplex package to HOL/Matrix
obua
parents:
diff changeset
  1063
22951
dfafcd6223ad whitespace tuned
haftmann
parents: 21858
diff changeset
  1064
    fun skip_nls () =
dfafcd6223ad whitespace tuned
haftmann
parents: 21858
diff changeset
  1065
        let val x = readToken () in
dfafcd6223ad whitespace tuned
haftmann
parents: 21858
diff changeset
  1066
        if is_tt x TOKEN_NL then
dfafcd6223ad whitespace tuned
haftmann
parents: 21858
diff changeset
  1067
            skip_nls ()
dfafcd6223ad whitespace tuned
haftmann
parents: 21858
diff changeset
  1068
        else
dfafcd6223ad whitespace tuned
haftmann
parents: 21858
diff changeset
  1069
            (pushToken x; ())
dfafcd6223ad whitespace tuned
haftmann
parents: 21858
diff changeset
  1070
        end
16784
92ff7c903585 - added cplex package to HOL/Matrix
obua
parents:
diff changeset
  1071
22951
dfafcd6223ad whitespace tuned
haftmann
parents: 21858
diff changeset
  1072
    fun skip_paragraph () =
dfafcd6223ad whitespace tuned
haftmann
parents: 21858
diff changeset
  1073
        if is_tt (readToken ()) TOKEN_NL then
dfafcd6223ad whitespace tuned
haftmann
parents: 21858
diff changeset
  1074
        (if is_tt (readToken ()) TOKEN_NL then
dfafcd6223ad whitespace tuned
haftmann
parents: 21858
diff changeset
  1075
             skip_nls ()
dfafcd6223ad whitespace tuned
haftmann
parents: 21858
diff changeset
  1076
         else
dfafcd6223ad whitespace tuned
haftmann
parents: 21858
diff changeset
  1077
             skip_paragraph ())
dfafcd6223ad whitespace tuned
haftmann
parents: 21858
diff changeset
  1078
        else
dfafcd6223ad whitespace tuned
haftmann
parents: 21858
diff changeset
  1079
        skip_paragraph ()
16784
92ff7c903585 - added cplex package to HOL/Matrix
obua
parents:
diff changeset
  1080
22951
dfafcd6223ad whitespace tuned
haftmann
parents: 21858
diff changeset
  1081
    fun load_value () =
dfafcd6223ad whitespace tuned
haftmann
parents: 21858
diff changeset
  1082
        let
dfafcd6223ad whitespace tuned
haftmann
parents: 21858
diff changeset
  1083
        val t1 = readToken ()
dfafcd6223ad whitespace tuned
haftmann
parents: 21858
diff changeset
  1084
        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
  1085
        in
dfafcd6223ad whitespace tuned
haftmann
parents: 21858
diff changeset
  1086
        if is_tt t1 TOKEN_NUM then
dfafcd6223ad whitespace tuned
haftmann
parents: 21858
diff changeset
  1087
            let
dfafcd6223ad whitespace tuned
haftmann
parents: 21858
diff changeset
  1088
            val name = readToken ()
dfafcd6223ad whitespace tuned
haftmann
parents: 21858
diff changeset
  1089
            val status = readToken ()
dfafcd6223ad whitespace tuned
haftmann
parents: 21858
diff changeset
  1090
            val value = readToken ()
dfafcd6223ad whitespace tuned
haftmann
parents: 21858
diff changeset
  1091
            in
dfafcd6223ad whitespace tuned
haftmann
parents: 21858
diff changeset
  1092
            if is_tt name TOKEN_SYMBOL andalso
dfafcd6223ad whitespace tuned
haftmann
parents: 21858
diff changeset
  1093
               is_tt status TOKEN_SYMBOL andalso
dfafcd6223ad whitespace tuned
haftmann
parents: 21858
diff changeset
  1094
               is_tt value TOKEN_NUM
dfafcd6223ad whitespace tuned
haftmann
parents: 21858
diff changeset
  1095
            then
dfafcd6223ad whitespace tuned
haftmann
parents: 21858
diff changeset
  1096
                readRestOfLine (SOME (snd (the name), snd (the value)))
dfafcd6223ad whitespace tuned
haftmann
parents: 21858
diff changeset
  1097
            else
dfafcd6223ad whitespace tuned
haftmann
parents: 21858
diff changeset
  1098
                raise (Load_cplexResult "column line expected")
dfafcd6223ad whitespace tuned
haftmann
parents: 21858
diff changeset
  1099
            end
dfafcd6223ad whitespace tuned
haftmann
parents: 21858
diff changeset
  1100
        else
dfafcd6223ad whitespace tuned
haftmann
parents: 21858
diff changeset
  1101
            (pushToken t1; NONE)
dfafcd6223ad whitespace tuned
haftmann
parents: 21858
diff changeset
  1102
        end
16784
92ff7c903585 - added cplex package to HOL/Matrix
obua
parents:
diff changeset
  1103
22951
dfafcd6223ad whitespace tuned
haftmann
parents: 21858
diff changeset
  1104
    fun load_values () =
dfafcd6223ad whitespace tuned
haftmann
parents: 21858
diff changeset
  1105
        let val v = load_value () in
dfafcd6223ad whitespace tuned
haftmann
parents: 21858
diff changeset
  1106
        if v = NONE then [] else (the v)::(load_values ())
dfafcd6223ad whitespace tuned
haftmann
parents: 21858
diff changeset
  1107
        end
dfafcd6223ad whitespace tuned
haftmann
parents: 21858
diff changeset
  1108
dfafcd6223ad whitespace tuned
haftmann
parents: 21858
diff changeset
  1109
    val header = readHeader ()
16784
92ff7c903585 - added cplex package to HOL/Matrix
obua
parents:
diff changeset
  1110
22951
dfafcd6223ad whitespace tuned
haftmann
parents: 21858
diff changeset
  1111
    val result =
dfafcd6223ad whitespace tuned
haftmann
parents: 21858
diff changeset
  1112
        case AList.lookup (op =) header "STATUS" of
dfafcd6223ad whitespace tuned
haftmann
parents: 21858
diff changeset
  1113
        SOME "INFEASIBLE" => Infeasible
dfafcd6223ad whitespace tuned
haftmann
parents: 21858
diff changeset
  1114
          | SOME "NONOPTIMAL" => Unbounded
dfafcd6223ad whitespace tuned
haftmann
parents: 21858
diff changeset
  1115
          | SOME "OPTIMAL" => Optimal (the (AList.lookup (op =) header "OBJECTIVE"),
dfafcd6223ad whitespace tuned
haftmann
parents: 21858
diff changeset
  1116
                       (skip_paragraph ();
dfafcd6223ad whitespace tuned
haftmann
parents: 21858
diff changeset
  1117
                        skip_paragraph ();
dfafcd6223ad whitespace tuned
haftmann
parents: 21858
diff changeset
  1118
                        skip_paragraph ();
dfafcd6223ad whitespace tuned
haftmann
parents: 21858
diff changeset
  1119
                        skip_paragraph ();
dfafcd6223ad whitespace tuned
haftmann
parents: 21858
diff changeset
  1120
                        skip_paragraph ();
dfafcd6223ad whitespace tuned
haftmann
parents: 21858
diff changeset
  1121
                        load_values ()))
dfafcd6223ad whitespace tuned
haftmann
parents: 21858
diff changeset
  1122
          | _ => Undefined
16784
92ff7c903585 - added cplex package to HOL/Matrix
obua
parents:
diff changeset
  1123
22951
dfafcd6223ad whitespace tuned
haftmann
parents: 21858
diff changeset
  1124
    val _ = TextIO.closeIn f
16784
92ff7c903585 - added cplex package to HOL/Matrix
obua
parents:
diff changeset
  1125
    in
22951
dfafcd6223ad whitespace tuned
haftmann
parents: 21858
diff changeset
  1126
    result
16784
92ff7c903585 - added cplex package to HOL/Matrix
obua
parents:
diff changeset
  1127
    end
92ff7c903585 - added cplex package to HOL/Matrix
obua
parents:
diff changeset
  1128
    handle (Tokenize s) => raise (Load_cplexResult ("Tokenize: "^s))
22951
dfafcd6223ad whitespace tuned
haftmann
parents: 21858
diff changeset
  1129
     | Option => raise (Load_cplexResult "Option")
dfafcd6223ad whitespace tuned
haftmann
parents: 21858
diff changeset
  1130
     | x => raise x
16784
92ff7c903585 - added cplex package to HOL/Matrix
obua
parents:
diff changeset
  1131
92ff7c903585 - added cplex package to HOL/Matrix
obua
parents:
diff changeset
  1132
exception Execute of string;
92ff7c903585 - added cplex package to HOL/Matrix
obua
parents:
diff changeset
  1133
21858
05f57309170c avoid conflict with Alice keywords: renamed pack -> implode, unpack -> explode, any -> many, avoided assert;
wenzelm
parents: 21056
diff changeset
  1134
fun tmp_file s = Path.implode (Path.expand (File.tmp_path (Path.make [s])));
16784
92ff7c903585 - added cplex package to HOL/Matrix
obua
parents:
diff changeset
  1135
fun wrap s = "\""^s^"\"";
92ff7c903585 - added cplex package to HOL/Matrix
obua
parents:
diff changeset
  1136
92ff7c903585 - added cplex package to HOL/Matrix
obua
parents:
diff changeset
  1137
fun solve_glpk prog =
22951
dfafcd6223ad whitespace tuned
haftmann
parents: 21858
diff changeset
  1138
    let
dfafcd6223ad whitespace tuned
haftmann
parents: 21858
diff changeset
  1139
    val name = LargeInt.toString (Time.toMicroseconds (Time.now ()))
dfafcd6223ad whitespace tuned
haftmann
parents: 21858
diff changeset
  1140
    val lpname = tmp_file (name^".lp")
dfafcd6223ad whitespace tuned
haftmann
parents: 21858
diff changeset
  1141
    val resultname = tmp_file (name^".txt")
dfafcd6223ad whitespace tuned
haftmann
parents: 21858
diff changeset
  1142
    val _ = save_cplexFile lpname prog
dfafcd6223ad whitespace tuned
haftmann
parents: 21858
diff changeset
  1143
    val cplex_path = getenv "GLPK_PATH"
dfafcd6223ad whitespace tuned
haftmann
parents: 21858
diff changeset
  1144
    val cplex = if cplex_path = "" then "glpsol" else cplex_path
dfafcd6223ad whitespace tuned
haftmann
parents: 21858
diff changeset
  1145
    val command = (wrap cplex)^" --lpt "^(wrap lpname)^" --output "^(wrap resultname)
35010
d6e492cea6e4 renamed system/system_out to bash/bash_output -- to emphasized that this is really GNU bash, not some undefined POSIX sh;
wenzelm
parents: 32740
diff changeset
  1146
    val answer = #1 (bash_output command)
16784
92ff7c903585 - added cplex package to HOL/Matrix
obua
parents:
diff changeset
  1147
    in
22951
dfafcd6223ad whitespace tuned
haftmann
parents: 21858
diff changeset
  1148
    let
dfafcd6223ad whitespace tuned
haftmann
parents: 21858
diff changeset
  1149
        val result = load_glpkResult resultname
dfafcd6223ad whitespace tuned
haftmann
parents: 21858
diff changeset
  1150
        val _ = OS.FileSys.remove lpname
dfafcd6223ad whitespace tuned
haftmann
parents: 21858
diff changeset
  1151
        val _ = OS.FileSys.remove resultname
16784
92ff7c903585 - added cplex package to HOL/Matrix
obua
parents:
diff changeset
  1152
    in
22951
dfafcd6223ad whitespace tuned
haftmann
parents: 21858
diff changeset
  1153
        result
dfafcd6223ad whitespace tuned
haftmann
parents: 21858
diff changeset
  1154
    end
dfafcd6223ad whitespace tuned
haftmann
parents: 21858
diff changeset
  1155
    handle (Load_cplexResult s) => raise (Execute ("Load_cplexResult: "^s^"\nExecute: "^answer))
dfafcd6223ad whitespace tuned
haftmann
parents: 21858
diff changeset
  1156
         | _ => raise (Execute answer)
16784
92ff7c903585 - added cplex package to HOL/Matrix
obua
parents:
diff changeset
  1157
    end
92ff7c903585 - added cplex package to HOL/Matrix
obua
parents:
diff changeset
  1158
22951
dfafcd6223ad whitespace tuned
haftmann
parents: 21858
diff changeset
  1159
fun solve_cplex prog =
dfafcd6223ad whitespace tuned
haftmann
parents: 21858
diff changeset
  1160
    let
dfafcd6223ad whitespace tuned
haftmann
parents: 21858
diff changeset
  1161
    fun write_script s lp r =
dfafcd6223ad whitespace tuned
haftmann
parents: 21858
diff changeset
  1162
        let
dfafcd6223ad whitespace tuned
haftmann
parents: 21858
diff changeset
  1163
        val f = TextIO.openOut s
dfafcd6223ad whitespace tuned
haftmann
parents: 21858
diff changeset
  1164
        val _ = TextIO.output (f, "read\n"^lp^"\noptimize\nwrite\n"^r^"\nquit")
dfafcd6223ad whitespace tuned
haftmann
parents: 21858
diff changeset
  1165
        val _ = TextIO.closeOut f
dfafcd6223ad whitespace tuned
haftmann
parents: 21858
diff changeset
  1166
        in
dfafcd6223ad whitespace tuned
haftmann
parents: 21858
diff changeset
  1167
        ()
dfafcd6223ad whitespace tuned
haftmann
parents: 21858
diff changeset
  1168
        end
dfafcd6223ad whitespace tuned
haftmann
parents: 21858
diff changeset
  1169
dfafcd6223ad whitespace tuned
haftmann
parents: 21858
diff changeset
  1170
    val name = LargeInt.toString (Time.toMicroseconds (Time.now ()))
dfafcd6223ad whitespace tuned
haftmann
parents: 21858
diff changeset
  1171
    val lpname = tmp_file (name^".lp")
dfafcd6223ad whitespace tuned
haftmann
parents: 21858
diff changeset
  1172
    val resultname = tmp_file (name^".txt")
dfafcd6223ad whitespace tuned
haftmann
parents: 21858
diff changeset
  1173
    val scriptname = tmp_file (name^".script")
dfafcd6223ad whitespace tuned
haftmann
parents: 21858
diff changeset
  1174
    val _ = save_cplexFile lpname prog
dfafcd6223ad whitespace tuned
haftmann
parents: 21858
diff changeset
  1175
    val cplex_path = getenv "CPLEX_PATH"
dfafcd6223ad whitespace tuned
haftmann
parents: 21858
diff changeset
  1176
    val cplex = if cplex_path = "" then "cplex" else cplex_path
dfafcd6223ad whitespace tuned
haftmann
parents: 21858
diff changeset
  1177
    val _ = write_script scriptname lpname resultname
dfafcd6223ad whitespace tuned
haftmann
parents: 21858
diff changeset
  1178
    val command = (wrap cplex)^" < "^(wrap scriptname)^" > /dev/null"
35010
d6e492cea6e4 renamed system/system_out to bash/bash_output -- to emphasized that this is really GNU bash, not some undefined POSIX sh;
wenzelm
parents: 32740
diff changeset
  1179
    val answer = "return code "^(Int.toString (bash command))
22951
dfafcd6223ad whitespace tuned
haftmann
parents: 21858
diff changeset
  1180
    in
dfafcd6223ad whitespace tuned
haftmann
parents: 21858
diff changeset
  1181
    let
dfafcd6223ad whitespace tuned
haftmann
parents: 21858
diff changeset
  1182
        val result = load_cplexResult resultname
dfafcd6223ad whitespace tuned
haftmann
parents: 21858
diff changeset
  1183
        val _ = OS.FileSys.remove lpname
dfafcd6223ad whitespace tuned
haftmann
parents: 21858
diff changeset
  1184
        val _ = OS.FileSys.remove resultname
dfafcd6223ad whitespace tuned
haftmann
parents: 21858
diff changeset
  1185
        val _ = OS.FileSys.remove scriptname
dfafcd6223ad whitespace tuned
haftmann
parents: 21858
diff changeset
  1186
    in
dfafcd6223ad whitespace tuned
haftmann
parents: 21858
diff changeset
  1187
        result
dfafcd6223ad whitespace tuned
haftmann
parents: 21858
diff changeset
  1188
    end
dfafcd6223ad whitespace tuned
haftmann
parents: 21858
diff changeset
  1189
    end
dfafcd6223ad whitespace tuned
haftmann
parents: 21858
diff changeset
  1190
dfafcd6223ad whitespace tuned
haftmann
parents: 21858
diff changeset
  1191
fun solve prog =
16966
37e34f315057 1. changed configuration variables for linear programming (Cplex_tools):
obua
parents: 16873
diff changeset
  1192
    case get_solver () of
22951
dfafcd6223ad whitespace tuned
haftmann
parents: 21858
diff changeset
  1193
      SOLVER_DEFAULT =>
16966
37e34f315057 1. changed configuration variables for linear programming (Cplex_tools):
obua
parents: 16873
diff changeset
  1194
        (case getenv "LP_SOLVER" of
22951
dfafcd6223ad whitespace tuned
haftmann
parents: 21858
diff changeset
  1195
       "CPLEX" => solve_cplex prog
16966
37e34f315057 1. changed configuration variables for linear programming (Cplex_tools):
obua
parents: 16873
diff changeset
  1196
         | "GLPK" => solve_glpk prog
37e34f315057 1. changed configuration variables for linear programming (Cplex_tools):
obua
parents: 16873
diff changeset
  1197
         | _ => 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
  1198
    | SOLVER_CPLEX => solve_cplex prog
37e34f315057 1. changed configuration variables for linear programming (Cplex_tools):
obua
parents: 16873
diff changeset
  1199
    | SOLVER_GLPK => solve_glpk prog
22951
dfafcd6223ad whitespace tuned
haftmann
parents: 21858
diff changeset
  1200
16784
92ff7c903585 - added cplex package to HOL/Matrix
obua
parents:
diff changeset
  1201
end;
92ff7c903585 - added cplex package to HOL/Matrix
obua
parents:
diff changeset
  1202
92ff7c903585 - added cplex package to HOL/Matrix
obua
parents:
diff changeset
  1203
(*
92ff7c903585 - added cplex package to HOL/Matrix
obua
parents:
diff changeset
  1204
val demofile = "/home/obua/flyspeck/kepler/LP/cplexPent2.lp45"
92ff7c903585 - added cplex package to HOL/Matrix
obua
parents:
diff changeset
  1205
val demoout = "/home/obua/flyspeck/kepler/LP/test.out"
92ff7c903585 - added cplex package to HOL/Matrix
obua
parents:
diff changeset
  1206
val demoresult = "/home/obua/flyspeck/kepler/LP/try/test2.sol"
22951
dfafcd6223ad whitespace tuned
haftmann
parents: 21858
diff changeset
  1207
dfafcd6223ad whitespace tuned
haftmann
parents: 21858
diff changeset
  1208
fun loadcplex () = Cplex.relax_strict_ineqs
dfafcd6223ad whitespace tuned
haftmann
parents: 21858
diff changeset
  1209
           (Cplex.load_cplexFile demofile)
16784
92ff7c903585 - added cplex package to HOL/Matrix
obua
parents:
diff changeset
  1210
92ff7c903585 - added cplex package to HOL/Matrix
obua
parents:
diff changeset
  1211
fun writecplex lp = Cplex.save_cplexFile demoout lp
92ff7c903585 - added cplex package to HOL/Matrix
obua
parents:
diff changeset
  1212
22951
dfafcd6223ad whitespace tuned
haftmann
parents: 21858
diff changeset
  1213
fun test () =
16784
92ff7c903585 - added cplex package to HOL/Matrix
obua
parents:
diff changeset
  1214
    let
22951
dfafcd6223ad whitespace tuned
haftmann
parents: 21858
diff changeset
  1215
    val lp = loadcplex ()
dfafcd6223ad whitespace tuned
haftmann
parents: 21858
diff changeset
  1216
    val lp2 = Cplex.elim_nonfree_bounds lp
16784
92ff7c903585 - added cplex package to HOL/Matrix
obua
parents:
diff changeset
  1217
    in
22951
dfafcd6223ad whitespace tuned
haftmann
parents: 21858
diff changeset
  1218
    writecplex lp2
16784
92ff7c903585 - added cplex package to HOL/Matrix
obua
parents:
diff changeset
  1219
    end
92ff7c903585 - added cplex package to HOL/Matrix
obua
parents:
diff changeset
  1220
92ff7c903585 - added cplex package to HOL/Matrix
obua
parents:
diff changeset
  1221
fun loadresult () = Cplex.load_cplexResult demoresult;
92ff7c903585 - added cplex package to HOL/Matrix
obua
parents:
diff changeset
  1222
*)
92ff7c903585 - added cplex package to HOL/Matrix
obua
parents:
diff changeset
  1223
92ff7c903585 - added cplex package to HOL/Matrix
obua
parents:
diff changeset
  1224
(*val prog = Cplex.load_cplexFile "/home/obua/tmp/pent/graph_0.lpt";
92ff7c903585 - added cplex package to HOL/Matrix
obua
parents:
diff changeset
  1225
val _ = Cplex.solve prog;*)