src/HOL/Matrix_LP/fspmlp.ML
author wenzelm
Wed, 26 Oct 2016 15:14:17 +0200
changeset 64406 492de9062cd2
parent 47455 26315a545e26
child 69597 ff784d5a5bfb
permissions -rw-r--r--
more specific hardware information: relevant for ultimate Mac OS X version;
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
47455
26315a545e26 updated headers;
wenzelm
parents: 46988
diff changeset
     1
(*  Title:      HOL/Matrix_LP/fspmlp.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
22951
dfafcd6223ad whitespace tuned
haftmann
parents: 21056
diff changeset
     5
signature FSPMLP =
16784
92ff7c903585 - added cplex package to HOL/Matrix
obua
parents:
diff changeset
     6
sig
92ff7c903585 - added cplex package to HOL/Matrix
obua
parents:
diff changeset
     7
    type linprog
19404
9bf2cdc9e8e8 Moved stuff from Ring_and_Field to Matrix
obua
parents: 17412
diff changeset
     8
    type vector = FloatSparseMatrixBuilder.vector
9bf2cdc9e8e8 Moved stuff from Ring_and_Field to Matrix
obua
parents: 17412
diff changeset
     9
    type matrix = FloatSparseMatrixBuilder.matrix
16784
92ff7c903585 - added cplex package to HOL/Matrix
obua
parents:
diff changeset
    10
22964
2284e0d02e7f reorganized float arithmetic
haftmann
parents: 22951
diff changeset
    11
    val y : linprog -> term
2284e0d02e7f reorganized float arithmetic
haftmann
parents: 22951
diff changeset
    12
    val A : linprog -> term * term
2284e0d02e7f reorganized float arithmetic
haftmann
parents: 22951
diff changeset
    13
    val b : linprog -> term
2284e0d02e7f reorganized float arithmetic
haftmann
parents: 22951
diff changeset
    14
    val c : linprog -> term * term
2284e0d02e7f reorganized float arithmetic
haftmann
parents: 22951
diff changeset
    15
    val r12 : linprog -> term * term
16784
92ff7c903585 - added cplex package to HOL/Matrix
obua
parents:
diff changeset
    16
92ff7c903585 - added cplex package to HOL/Matrix
obua
parents:
diff changeset
    17
    exception Load of string
22951
dfafcd6223ad whitespace tuned
haftmann
parents: 21056
diff changeset
    18
16784
92ff7c903585 - added cplex package to HOL/Matrix
obua
parents:
diff changeset
    19
    val load : string -> int -> bool -> linprog
92ff7c903585 - added cplex package to HOL/Matrix
obua
parents:
diff changeset
    20
end
92ff7c903585 - added cplex package to HOL/Matrix
obua
parents:
diff changeset
    21
22964
2284e0d02e7f reorganized float arithmetic
haftmann
parents: 22951
diff changeset
    22
structure Fspmlp : FSPMLP =
16784
92ff7c903585 - added cplex package to HOL/Matrix
obua
parents:
diff changeset
    23
struct
92ff7c903585 - added cplex package to HOL/Matrix
obua
parents:
diff changeset
    24
19404
9bf2cdc9e8e8 Moved stuff from Ring_and_Field to Matrix
obua
parents: 17412
diff changeset
    25
type vector = FloatSparseMatrixBuilder.vector
9bf2cdc9e8e8 Moved stuff from Ring_and_Field to Matrix
obua
parents: 17412
diff changeset
    26
type matrix = FloatSparseMatrixBuilder.matrix
9bf2cdc9e8e8 Moved stuff from Ring_and_Field to Matrix
obua
parents: 17412
diff changeset
    27
24302
obua
parents: 24135
diff changeset
    28
type linprog = term * (term * term) * term * (term * term) * (term * term)
16784
92ff7c903585 - added cplex package to HOL/Matrix
obua
parents:
diff changeset
    29
46533
faf233c4a404 dropped dead code
haftmann
parents: 37788
diff changeset
    30
fun y (c1, _, _, _, _) = c1
faf233c4a404 dropped dead code
haftmann
parents: 37788
diff changeset
    31
fun A (_, c2, _, _, _) = c2
faf233c4a404 dropped dead code
haftmann
parents: 37788
diff changeset
    32
fun b (_, _, c3, _, _) = c3
faf233c4a404 dropped dead code
haftmann
parents: 37788
diff changeset
    33
fun c (_, _, _, c4, _) = c4
faf233c4a404 dropped dead code
haftmann
parents: 37788
diff changeset
    34
fun r12 (_, _, _, _, c6) = c6
16784
92ff7c903585 - added cplex package to HOL/Matrix
obua
parents:
diff changeset
    35
22951
dfafcd6223ad whitespace tuned
haftmann
parents: 21056
diff changeset
    36
structure CplexFloatSparseMatrixConverter =
16784
92ff7c903585 - added cplex package to HOL/Matrix
obua
parents:
diff changeset
    37
MAKE_CPLEX_MATRIX_CONVERTER(structure cplex = Cplex and matrix_builder = FloatSparseMatrixBuilder);
92ff7c903585 - added cplex package to HOL/Matrix
obua
parents:
diff changeset
    38
92ff7c903585 - added cplex package to HOL/Matrix
obua
parents:
diff changeset
    39
datatype bound_type = LOWER | UPPER
92ff7c903585 - added cplex package to HOL/Matrix
obua
parents:
diff changeset
    40
24135
e7fb7ef2a85e added int type constraints to accomodate hacked SML/NJ;
wenzelm
parents: 23665
diff changeset
    41
fun intbound_ord ((i1: int, b1),(i2,b2)) =
16784
92ff7c903585 - added cplex package to HOL/Matrix
obua
parents:
diff changeset
    42
    if i1 < i2 then LESS
22951
dfafcd6223ad whitespace tuned
haftmann
parents: 21056
diff changeset
    43
    else if i1 = i2 then
dfafcd6223ad whitespace tuned
haftmann
parents: 21056
diff changeset
    44
        (if b1 = b2 then EQUAL else if b1=LOWER then LESS else GREATER)
16784
92ff7c903585 - added cplex package to HOL/Matrix
obua
parents:
diff changeset
    45
    else GREATER
92ff7c903585 - added cplex package to HOL/Matrix
obua
parents:
diff changeset
    46
31971
8c1b845ed105 renamed functor TableFun to Table, and GraphFun to Graph;
wenzelm
parents: 24630
diff changeset
    47
structure Inttab = Table(type key = int val ord = (rev_order o int_ord));
16784
92ff7c903585 - added cplex package to HOL/Matrix
obua
parents:
diff changeset
    48
31971
8c1b845ed105 renamed functor TableFun to Table, and GraphFun to Graph;
wenzelm
parents: 24630
diff changeset
    49
structure VarGraph = Table(type key = int*bound_type val ord = intbound_ord);
16784
92ff7c903585 - added cplex package to HOL/Matrix
obua
parents:
diff changeset
    50
(* key -> (float option) * (int -> (float * (((float * float) * key) list)))) *)
92ff7c903585 - added cplex package to HOL/Matrix
obua
parents:
diff changeset
    51
(* dest_key -> (sure_bound * (row_index -> (row_bound * (((coeff_lower * coeff_upper) * src_key) list)))) *)
92ff7c903585 - added cplex package to HOL/Matrix
obua
parents:
diff changeset
    52
92ff7c903585 - added cplex package to HOL/Matrix
obua
parents:
diff changeset
    53
exception Internal of string;
92ff7c903585 - added cplex package to HOL/Matrix
obua
parents:
diff changeset
    54
22951
dfafcd6223ad whitespace tuned
haftmann
parents: 21056
diff changeset
    55
fun add_row_bound g dest_key row_index row_bound =
dfafcd6223ad whitespace tuned
haftmann
parents: 21056
diff changeset
    56
    let
dfafcd6223ad whitespace tuned
haftmann
parents: 21056
diff changeset
    57
        val x =
dfafcd6223ad whitespace tuned
haftmann
parents: 21056
diff changeset
    58
            case VarGraph.lookup g dest_key of
dfafcd6223ad whitespace tuned
haftmann
parents: 21056
diff changeset
    59
                NONE => (NONE, Inttab.update (row_index, (row_bound, [])) Inttab.empty)
dfafcd6223ad whitespace tuned
haftmann
parents: 21056
diff changeset
    60
              | SOME (sure_bound, f) =>
dfafcd6223ad whitespace tuned
haftmann
parents: 21056
diff changeset
    61
                (sure_bound,
dfafcd6223ad whitespace tuned
haftmann
parents: 21056
diff changeset
    62
                 case Inttab.lookup f row_index of
dfafcd6223ad whitespace tuned
haftmann
parents: 21056
diff changeset
    63
                     NONE => Inttab.update (row_index, (row_bound, [])) f
dfafcd6223ad whitespace tuned
haftmann
parents: 21056
diff changeset
    64
                   | SOME _ => raise (Internal "add_row_bound"))
16784
92ff7c903585 - added cplex package to HOL/Matrix
obua
parents:
diff changeset
    65
    in
22951
dfafcd6223ad whitespace tuned
haftmann
parents: 21056
diff changeset
    66
        VarGraph.update (dest_key, x) g
16784
92ff7c903585 - added cplex package to HOL/Matrix
obua
parents:
diff changeset
    67
    end
92ff7c903585 - added cplex package to HOL/Matrix
obua
parents:
diff changeset
    68
22951
dfafcd6223ad whitespace tuned
haftmann
parents: 21056
diff changeset
    69
fun update_sure_bound g (key as (_, btype)) bound =
dfafcd6223ad whitespace tuned
haftmann
parents: 21056
diff changeset
    70
    let
dfafcd6223ad whitespace tuned
haftmann
parents: 21056
diff changeset
    71
        val x =
dfafcd6223ad whitespace tuned
haftmann
parents: 21056
diff changeset
    72
            case VarGraph.lookup g key of
dfafcd6223ad whitespace tuned
haftmann
parents: 21056
diff changeset
    73
                NONE => (SOME bound, Inttab.empty)
dfafcd6223ad whitespace tuned
haftmann
parents: 21056
diff changeset
    74
              | SOME (NONE, f) => (SOME bound, f)
dfafcd6223ad whitespace tuned
haftmann
parents: 21056
diff changeset
    75
              | SOME (SOME old_bound, f) =>
dfafcd6223ad whitespace tuned
haftmann
parents: 21056
diff changeset
    76
                (SOME ((case btype of
22964
2284e0d02e7f reorganized float arithmetic
haftmann
parents: 22951
diff changeset
    77
                            UPPER => Float.min
2284e0d02e7f reorganized float arithmetic
haftmann
parents: 22951
diff changeset
    78
                          | LOWER => Float.max)
22951
dfafcd6223ad whitespace tuned
haftmann
parents: 21056
diff changeset
    79
                           old_bound bound), f)
dfafcd6223ad whitespace tuned
haftmann
parents: 21056
diff changeset
    80
    in
dfafcd6223ad whitespace tuned
haftmann
parents: 21056
diff changeset
    81
        VarGraph.update (key, x) g
dfafcd6223ad whitespace tuned
haftmann
parents: 21056
diff changeset
    82
    end
dfafcd6223ad whitespace tuned
haftmann
parents: 21056
diff changeset
    83
dfafcd6223ad whitespace tuned
haftmann
parents: 21056
diff changeset
    84
fun get_sure_bound g key =
dfafcd6223ad whitespace tuned
haftmann
parents: 21056
diff changeset
    85
    case VarGraph.lookup g key of
dfafcd6223ad whitespace tuned
haftmann
parents: 21056
diff changeset
    86
        NONE => NONE
16784
92ff7c903585 - added cplex package to HOL/Matrix
obua
parents:
diff changeset
    87
      | SOME (sure_bound, _) => sure_bound
92ff7c903585 - added cplex package to HOL/Matrix
obua
parents:
diff changeset
    88
22951
dfafcd6223ad whitespace tuned
haftmann
parents: 21056
diff changeset
    89
(*fun get_row_bound g key row_index =
17412
e26cb20ef0cc TableFun/Symtab: curried lookup and update;
wenzelm
parents: 17261
diff changeset
    90
    case VarGraph.lookup g key of
22951
dfafcd6223ad whitespace tuned
haftmann
parents: 21056
diff changeset
    91
        NONE => NONE
16784
92ff7c903585 - added cplex package to HOL/Matrix
obua
parents:
diff changeset
    92
      | SOME (sure_bound, f) =>
22951
dfafcd6223ad whitespace tuned
haftmann
parents: 21056
diff changeset
    93
        (case Inttab.lookup f row_index of
dfafcd6223ad whitespace tuned
haftmann
parents: 21056
diff changeset
    94
             NONE => NONE
dfafcd6223ad whitespace tuned
haftmann
parents: 21056
diff changeset
    95
           | SOME (row_bound, _) => (sure_bound, row_bound))*)
dfafcd6223ad whitespace tuned
haftmann
parents: 21056
diff changeset
    96
dfafcd6223ad whitespace tuned
haftmann
parents: 21056
diff changeset
    97
fun add_edge g src_key dest_key row_index coeff =
17412
e26cb20ef0cc TableFun/Symtab: curried lookup and update;
wenzelm
parents: 17261
diff changeset
    98
    case VarGraph.lookup g dest_key of
22951
dfafcd6223ad whitespace tuned
haftmann
parents: 21056
diff changeset
    99
        NONE => raise (Internal "add_edge: dest_key not found")
16784
92ff7c903585 - added cplex package to HOL/Matrix
obua
parents:
diff changeset
   100
      | SOME (sure_bound, f) =>
22951
dfafcd6223ad whitespace tuned
haftmann
parents: 21056
diff changeset
   101
        (case Inttab.lookup f row_index of
dfafcd6223ad whitespace tuned
haftmann
parents: 21056
diff changeset
   102
             NONE => raise (Internal "add_edge: row_index not found")
dfafcd6223ad whitespace tuned
haftmann
parents: 21056
diff changeset
   103
           | SOME (row_bound, sources) =>
dfafcd6223ad whitespace tuned
haftmann
parents: 21056
diff changeset
   104
             VarGraph.update (dest_key, (sure_bound, Inttab.update (row_index, (row_bound, (coeff, src_key) :: sources)) f)) g)
16784
92ff7c903585 - added cplex package to HOL/Matrix
obua
parents:
diff changeset
   105
22951
dfafcd6223ad whitespace tuned
haftmann
parents: 21056
diff changeset
   106
fun split_graph g =
21056
2cfe839e8d58 Symtab.foldl replaced by Symtab.fold
haftmann
parents: 19404
diff changeset
   107
  let
2cfe839e8d58 Symtab.foldl replaced by Symtab.fold
haftmann
parents: 19404
diff changeset
   108
    fun split (key, (sure_bound, _)) (r1, r2) = case sure_bound
2cfe839e8d58 Symtab.foldl replaced by Symtab.fold
haftmann
parents: 19404
diff changeset
   109
     of NONE => (r1, r2)
2cfe839e8d58 Symtab.foldl replaced by Symtab.fold
haftmann
parents: 19404
diff changeset
   110
      | SOME bound =>  (case key
2cfe839e8d58 Symtab.foldl replaced by Symtab.fold
haftmann
parents: 19404
diff changeset
   111
         of (u, UPPER) => (r1, Inttab.update (u, bound) r2)
2cfe839e8d58 Symtab.foldl replaced by Symtab.fold
haftmann
parents: 19404
diff changeset
   112
          | (u, LOWER) => (Inttab.update (u, bound) r1, r2))
2cfe839e8d58 Symtab.foldl replaced by Symtab.fold
haftmann
parents: 19404
diff changeset
   113
  in VarGraph.fold split g (Inttab.empty, Inttab.empty) end
16784
92ff7c903585 - added cplex package to HOL/Matrix
obua
parents:
diff changeset
   114
92ff7c903585 - added cplex package to HOL/Matrix
obua
parents:
diff changeset
   115
(* If safe is true, termination is guaranteed, but the sure bounds may be not optimal (relative to the algorithm).
92ff7c903585 - added cplex package to HOL/Matrix
obua
parents:
diff changeset
   116
   If safe is false, termination is not guaranteed, but on termination the sure bounds are optimal (relative to the algorithm) *)
22951
dfafcd6223ad whitespace tuned
haftmann
parents: 21056
diff changeset
   117
fun propagate_sure_bounds safe names g =
dfafcd6223ad whitespace tuned
haftmann
parents: 21056
diff changeset
   118
    let
dfafcd6223ad whitespace tuned
haftmann
parents: 21056
diff changeset
   119
        (* returns NONE if no new sure bound could be calculated, otherwise the new sure bound is returned *)
dfafcd6223ad whitespace tuned
haftmann
parents: 21056
diff changeset
   120
        fun calc_sure_bound_from_sources g (key as (_, btype)) =
dfafcd6223ad whitespace tuned
haftmann
parents: 21056
diff changeset
   121
            let
dfafcd6223ad whitespace tuned
haftmann
parents: 21056
diff changeset
   122
                fun mult_upper x (lower, upper) =
23520
483fe92f00c1 tuned arithmetic modules
haftmann
parents: 23297
diff changeset
   123
                    if Float.sign x = LESS then
22964
2284e0d02e7f reorganized float arithmetic
haftmann
parents: 22951
diff changeset
   124
                        Float.mult x lower
22951
dfafcd6223ad whitespace tuned
haftmann
parents: 21056
diff changeset
   125
                    else
22964
2284e0d02e7f reorganized float arithmetic
haftmann
parents: 22951
diff changeset
   126
                        Float.mult x upper
16784
92ff7c903585 - added cplex package to HOL/Matrix
obua
parents:
diff changeset
   127
22951
dfafcd6223ad whitespace tuned
haftmann
parents: 21056
diff changeset
   128
                fun mult_lower x (lower, upper) =
23520
483fe92f00c1 tuned arithmetic modules
haftmann
parents: 23297
diff changeset
   129
                    if Float.sign x = LESS then
22964
2284e0d02e7f reorganized float arithmetic
haftmann
parents: 22951
diff changeset
   130
                        Float.mult x upper
22951
dfafcd6223ad whitespace tuned
haftmann
parents: 21056
diff changeset
   131
                    else
22964
2284e0d02e7f reorganized float arithmetic
haftmann
parents: 22951
diff changeset
   132
                        Float.mult x lower
22951
dfafcd6223ad whitespace tuned
haftmann
parents: 21056
diff changeset
   133
dfafcd6223ad whitespace tuned
haftmann
parents: 21056
diff changeset
   134
                val mult_btype = case btype of UPPER => mult_upper | LOWER => mult_lower
16784
92ff7c903585 - added cplex package to HOL/Matrix
obua
parents:
diff changeset
   135
46533
faf233c4a404 dropped dead code
haftmann
parents: 37788
diff changeset
   136
                fun calc_sure_bound (_, (row_bound, sources)) sure_bound =
22951
dfafcd6223ad whitespace tuned
haftmann
parents: 21056
diff changeset
   137
                    let
dfafcd6223ad whitespace tuned
haftmann
parents: 21056
diff changeset
   138
                        fun add_src_bound (coeff, src_key) sum =
dfafcd6223ad whitespace tuned
haftmann
parents: 21056
diff changeset
   139
                            case sum of
dfafcd6223ad whitespace tuned
haftmann
parents: 21056
diff changeset
   140
                                NONE => NONE
dfafcd6223ad whitespace tuned
haftmann
parents: 21056
diff changeset
   141
                              | SOME x =>
dfafcd6223ad whitespace tuned
haftmann
parents: 21056
diff changeset
   142
                                (case get_sure_bound g src_key of
dfafcd6223ad whitespace tuned
haftmann
parents: 21056
diff changeset
   143
                                     NONE => NONE
22964
2284e0d02e7f reorganized float arithmetic
haftmann
parents: 22951
diff changeset
   144
                                   | SOME src_sure_bound => SOME (Float.add x (mult_btype src_sure_bound coeff)))
22951
dfafcd6223ad whitespace tuned
haftmann
parents: 21056
diff changeset
   145
                    in
dfafcd6223ad whitespace tuned
haftmann
parents: 21056
diff changeset
   146
                        case fold add_src_bound sources (SOME row_bound) of
dfafcd6223ad whitespace tuned
haftmann
parents: 21056
diff changeset
   147
                            NONE => sure_bound
dfafcd6223ad whitespace tuned
haftmann
parents: 21056
diff changeset
   148
                          | new_sure_bound as (SOME new_bound) =>
dfafcd6223ad whitespace tuned
haftmann
parents: 21056
diff changeset
   149
                            (case sure_bound of
dfafcd6223ad whitespace tuned
haftmann
parents: 21056
diff changeset
   150
                                 NONE => new_sure_bound
dfafcd6223ad whitespace tuned
haftmann
parents: 21056
diff changeset
   151
                               | SOME old_bound =>
dfafcd6223ad whitespace tuned
haftmann
parents: 21056
diff changeset
   152
                                 SOME (case btype of
22964
2284e0d02e7f reorganized float arithmetic
haftmann
parents: 22951
diff changeset
   153
                                           UPPER => Float.min old_bound new_bound
2284e0d02e7f reorganized float arithmetic
haftmann
parents: 22951
diff changeset
   154
                                         | LOWER => Float.max old_bound new_bound))
22951
dfafcd6223ad whitespace tuned
haftmann
parents: 21056
diff changeset
   155
                    end
dfafcd6223ad whitespace tuned
haftmann
parents: 21056
diff changeset
   156
            in
dfafcd6223ad whitespace tuned
haftmann
parents: 21056
diff changeset
   157
                case VarGraph.lookup g key of
dfafcd6223ad whitespace tuned
haftmann
parents: 21056
diff changeset
   158
                    NONE => NONE
dfafcd6223ad whitespace tuned
haftmann
parents: 21056
diff changeset
   159
                  | SOME (sure_bound, f) =>
dfafcd6223ad whitespace tuned
haftmann
parents: 21056
diff changeset
   160
                    let
dfafcd6223ad whitespace tuned
haftmann
parents: 21056
diff changeset
   161
                        val x = Inttab.fold calc_sure_bound f sure_bound
dfafcd6223ad whitespace tuned
haftmann
parents: 21056
diff changeset
   162
                    in
dfafcd6223ad whitespace tuned
haftmann
parents: 21056
diff changeset
   163
                        if x = sure_bound then NONE else x
dfafcd6223ad whitespace tuned
haftmann
parents: 21056
diff changeset
   164
                    end
dfafcd6223ad whitespace tuned
haftmann
parents: 21056
diff changeset
   165
                end
16784
92ff7c903585 - added cplex package to HOL/Matrix
obua
parents:
diff changeset
   166
22951
dfafcd6223ad whitespace tuned
haftmann
parents: 21056
diff changeset
   167
        fun propagate (key, _) (g, b) =
dfafcd6223ad whitespace tuned
haftmann
parents: 21056
diff changeset
   168
            case calc_sure_bound_from_sources g key of
dfafcd6223ad whitespace tuned
haftmann
parents: 21056
diff changeset
   169
                NONE => (g,b)
dfafcd6223ad whitespace tuned
haftmann
parents: 21056
diff changeset
   170
              | SOME bound => (update_sure_bound g key bound,
dfafcd6223ad whitespace tuned
haftmann
parents: 21056
diff changeset
   171
                               if safe then
dfafcd6223ad whitespace tuned
haftmann
parents: 21056
diff changeset
   172
                                   case get_sure_bound g key of
dfafcd6223ad whitespace tuned
haftmann
parents: 21056
diff changeset
   173
                                       NONE => true
dfafcd6223ad whitespace tuned
haftmann
parents: 21056
diff changeset
   174
                                     | _ => b
dfafcd6223ad whitespace tuned
haftmann
parents: 21056
diff changeset
   175
                               else
dfafcd6223ad whitespace tuned
haftmann
parents: 21056
diff changeset
   176
                                   true)
16784
92ff7c903585 - added cplex package to HOL/Matrix
obua
parents:
diff changeset
   177
22951
dfafcd6223ad whitespace tuned
haftmann
parents: 21056
diff changeset
   178
        val (g, b) = VarGraph.fold propagate g (g, false)
16784
92ff7c903585 - added cplex package to HOL/Matrix
obua
parents:
diff changeset
   179
    in
22951
dfafcd6223ad whitespace tuned
haftmann
parents: 21056
diff changeset
   180
        if b then propagate_sure_bounds safe names g else g
dfafcd6223ad whitespace tuned
haftmann
parents: 21056
diff changeset
   181
    end
dfafcd6223ad whitespace tuned
haftmann
parents: 21056
diff changeset
   182
16784
92ff7c903585 - added cplex package to HOL/Matrix
obua
parents:
diff changeset
   183
exception Load of string;
92ff7c903585 - added cplex package to HOL/Matrix
obua
parents:
diff changeset
   184
23665
825bea0266db adopted to new computing oracle and fixed bugs introduced by tuning
obua
parents: 23520
diff changeset
   185
val empty_spvec = @{term "Nil :: real spvec"};
825bea0266db adopted to new computing oracle and fixed bugs introduced by tuning
obua
parents: 23520
diff changeset
   186
fun cons_spvec x xs = @{term "Cons :: nat * real => real spvec => real spvec"} $ x $ xs;
825bea0266db adopted to new computing oracle and fixed bugs introduced by tuning
obua
parents: 23520
diff changeset
   187
val empty_spmat = @{term "Nil :: real spmat"};
825bea0266db adopted to new computing oracle and fixed bugs introduced by tuning
obua
parents: 23520
diff changeset
   188
fun cons_spmat x xs = @{term "Cons :: nat * real spvec => real spmat => real spmat"} $ x $ xs;
22964
2284e0d02e7f reorganized float arithmetic
haftmann
parents: 22951
diff changeset
   189
22951
dfafcd6223ad whitespace tuned
haftmann
parents: 21056
diff changeset
   190
fun calcr safe_propagation xlen names prec A b =
16784
92ff7c903585 - added cplex package to HOL/Matrix
obua
parents:
diff changeset
   191
    let
22951
dfafcd6223ad whitespace tuned
haftmann
parents: 21056
diff changeset
   192
        fun test_1 (lower, upper) =
dfafcd6223ad whitespace tuned
haftmann
parents: 21056
diff changeset
   193
            if lower = upper then
23297
06f108974fa1 simplified type integer;
wenzelm
parents: 23261
diff changeset
   194
                (if Float.eq (lower, (~1, 0)) then ~1
06f108974fa1 simplified type integer;
wenzelm
parents: 23261
diff changeset
   195
                 else if Float.eq (lower, (1, 0)) then 1
22951
dfafcd6223ad whitespace tuned
haftmann
parents: 21056
diff changeset
   196
                 else 0)
dfafcd6223ad whitespace tuned
haftmann
parents: 21056
diff changeset
   197
            else 0
16784
92ff7c903585 - added cplex package to HOL/Matrix
obua
parents:
diff changeset
   198
22951
dfafcd6223ad whitespace tuned
haftmann
parents: 21056
diff changeset
   199
        fun calcr (row_index, a) g =
dfafcd6223ad whitespace tuned
haftmann
parents: 21056
diff changeset
   200
            let
dfafcd6223ad whitespace tuned
haftmann
parents: 21056
diff changeset
   201
                val b =  FloatSparseMatrixBuilder.v_elem_at b row_index
22964
2284e0d02e7f reorganized float arithmetic
haftmann
parents: 22951
diff changeset
   202
                val (_, b2) = FloatArith.approx_decstr_by_bin prec (case b of NONE => "0" | SOME b => b)
22951
dfafcd6223ad whitespace tuned
haftmann
parents: 21056
diff changeset
   203
                val approx_a = FloatSparseMatrixBuilder.v_fold (fn (i, s) => fn l =>
22964
2284e0d02e7f reorganized float arithmetic
haftmann
parents: 22951
diff changeset
   204
                                                                   (i, FloatArith.approx_decstr_by_bin prec s)::l) a []
16784
92ff7c903585 - added cplex package to HOL/Matrix
obua
parents:
diff changeset
   205
22951
dfafcd6223ad whitespace tuned
haftmann
parents: 21056
diff changeset
   206
                fun fold_dest_nodes (dest_index, dest_value) g =
dfafcd6223ad whitespace tuned
haftmann
parents: 21056
diff changeset
   207
                    let
dfafcd6223ad whitespace tuned
haftmann
parents: 21056
diff changeset
   208
                        val dest_test = test_1 dest_value
dfafcd6223ad whitespace tuned
haftmann
parents: 21056
diff changeset
   209
                    in
dfafcd6223ad whitespace tuned
haftmann
parents: 21056
diff changeset
   210
                        if dest_test = 0 then
dfafcd6223ad whitespace tuned
haftmann
parents: 21056
diff changeset
   211
                            g
dfafcd6223ad whitespace tuned
haftmann
parents: 21056
diff changeset
   212
                        else let
dfafcd6223ad whitespace tuned
haftmann
parents: 21056
diff changeset
   213
                                val (dest_key as (_, dest_btype), row_bound) =
dfafcd6223ad whitespace tuned
haftmann
parents: 21056
diff changeset
   214
                                    if dest_test = ~1 then
22964
2284e0d02e7f reorganized float arithmetic
haftmann
parents: 22951
diff changeset
   215
                                        ((dest_index, LOWER), Float.neg b2)
22951
dfafcd6223ad whitespace tuned
haftmann
parents: 21056
diff changeset
   216
                                    else
dfafcd6223ad whitespace tuned
haftmann
parents: 21056
diff changeset
   217
                                        ((dest_index, UPPER), b2)
16784
92ff7c903585 - added cplex package to HOL/Matrix
obua
parents:
diff changeset
   218
22951
dfafcd6223ad whitespace tuned
haftmann
parents: 21056
diff changeset
   219
                                fun fold_src_nodes (src_index, src_value as (src_lower, src_upper)) g =
dfafcd6223ad whitespace tuned
haftmann
parents: 21056
diff changeset
   220
                                    if src_index = dest_index then g
dfafcd6223ad whitespace tuned
haftmann
parents: 21056
diff changeset
   221
                                    else
dfafcd6223ad whitespace tuned
haftmann
parents: 21056
diff changeset
   222
                                        let
dfafcd6223ad whitespace tuned
haftmann
parents: 21056
diff changeset
   223
                                            val coeff = case dest_btype of
22964
2284e0d02e7f reorganized float arithmetic
haftmann
parents: 22951
diff changeset
   224
                                                            UPPER => (Float.neg src_upper, Float.neg src_lower)
22951
dfafcd6223ad whitespace tuned
haftmann
parents: 21056
diff changeset
   225
                                                          | LOWER => src_value
dfafcd6223ad whitespace tuned
haftmann
parents: 21056
diff changeset
   226
                                        in
23520
483fe92f00c1 tuned arithmetic modules
haftmann
parents: 23297
diff changeset
   227
                                            if Float.sign src_lower = LESS then
22951
dfafcd6223ad whitespace tuned
haftmann
parents: 21056
diff changeset
   228
                                                add_edge g (src_index, UPPER) dest_key row_index coeff
dfafcd6223ad whitespace tuned
haftmann
parents: 21056
diff changeset
   229
                                            else
dfafcd6223ad whitespace tuned
haftmann
parents: 21056
diff changeset
   230
                                                add_edge g (src_index, LOWER) dest_key row_index coeff
dfafcd6223ad whitespace tuned
haftmann
parents: 21056
diff changeset
   231
                                        end
dfafcd6223ad whitespace tuned
haftmann
parents: 21056
diff changeset
   232
                            in
dfafcd6223ad whitespace tuned
haftmann
parents: 21056
diff changeset
   233
                                fold fold_src_nodes approx_a (add_row_bound g dest_key row_index row_bound)
dfafcd6223ad whitespace tuned
haftmann
parents: 21056
diff changeset
   234
                            end
dfafcd6223ad whitespace tuned
haftmann
parents: 21056
diff changeset
   235
                    end
dfafcd6223ad whitespace tuned
haftmann
parents: 21056
diff changeset
   236
            in
dfafcd6223ad whitespace tuned
haftmann
parents: 21056
diff changeset
   237
                case approx_a of
dfafcd6223ad whitespace tuned
haftmann
parents: 21056
diff changeset
   238
                    [] => g
dfafcd6223ad whitespace tuned
haftmann
parents: 21056
diff changeset
   239
                  | [(u, a)] =>
dfafcd6223ad whitespace tuned
haftmann
parents: 21056
diff changeset
   240
                    let
dfafcd6223ad whitespace tuned
haftmann
parents: 21056
diff changeset
   241
                        val atest = test_1 a
dfafcd6223ad whitespace tuned
haftmann
parents: 21056
diff changeset
   242
                    in
dfafcd6223ad whitespace tuned
haftmann
parents: 21056
diff changeset
   243
                        if atest = ~1 then
22964
2284e0d02e7f reorganized float arithmetic
haftmann
parents: 22951
diff changeset
   244
                            update_sure_bound g (u, LOWER) (Float.neg b2)
22951
dfafcd6223ad whitespace tuned
haftmann
parents: 21056
diff changeset
   245
                        else if atest = 1 then
dfafcd6223ad whitespace tuned
haftmann
parents: 21056
diff changeset
   246
                            update_sure_bound g (u, UPPER) b2
dfafcd6223ad whitespace tuned
haftmann
parents: 21056
diff changeset
   247
                        else
dfafcd6223ad whitespace tuned
haftmann
parents: 21056
diff changeset
   248
                            g
dfafcd6223ad whitespace tuned
haftmann
parents: 21056
diff changeset
   249
                    end
dfafcd6223ad whitespace tuned
haftmann
parents: 21056
diff changeset
   250
                  | _ => fold fold_dest_nodes approx_a g
dfafcd6223ad whitespace tuned
haftmann
parents: 21056
diff changeset
   251
            end
16784
92ff7c903585 - added cplex package to HOL/Matrix
obua
parents:
diff changeset
   252
22951
dfafcd6223ad whitespace tuned
haftmann
parents: 21056
diff changeset
   253
        val g = FloatSparseMatrixBuilder.m_fold calcr A VarGraph.empty
23665
825bea0266db adopted to new computing oracle and fixed bugs introduced by tuning
obua
parents: 23520
diff changeset
   254
22951
dfafcd6223ad whitespace tuned
haftmann
parents: 21056
diff changeset
   255
        val g = propagate_sure_bounds safe_propagation names g
dfafcd6223ad whitespace tuned
haftmann
parents: 21056
diff changeset
   256
32960
69916a850301 eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents: 31971
diff changeset
   257
        val (r1, r2) = split_graph g
22951
dfafcd6223ad whitespace tuned
haftmann
parents: 21056
diff changeset
   258
24302
obua
parents: 24135
diff changeset
   259
        fun add_row_entry m index f vname value =
22951
dfafcd6223ad whitespace tuned
haftmann
parents: 21056
diff changeset
   260
            let
32960
69916a850301 eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents: 31971
diff changeset
   261
                val v = (case value of 
69916a850301 eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents: 31971
diff changeset
   262
                             SOME value => FloatSparseMatrixBuilder.mk_spvec_entry 0 value
69916a850301 eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents: 31971
diff changeset
   263
                           | NONE => FloatSparseMatrixBuilder.mk_spvec_entry' 0 (f $ (Var ((vname,0), HOLogic.realT))))
24302
obua
parents: 24135
diff changeset
   264
                val vec = cons_spvec v empty_spvec
22951
dfafcd6223ad whitespace tuned
haftmann
parents: 21056
diff changeset
   265
            in
22964
2284e0d02e7f reorganized float arithmetic
haftmann
parents: 22951
diff changeset
   266
                cons_spmat (FloatSparseMatrixBuilder.mk_spmat_entry index vec) m
22951
dfafcd6223ad whitespace tuned
haftmann
parents: 21056
diff changeset
   267
            end
16784
92ff7c903585 - added cplex package to HOL/Matrix
obua
parents:
diff changeset
   268
22951
dfafcd6223ad whitespace tuned
haftmann
parents: 21056
diff changeset
   269
        fun abs_estimate i r1 r2 =
dfafcd6223ad whitespace tuned
haftmann
parents: 21056
diff changeset
   270
            if i = 0 then
24302
obua
parents: 24135
diff changeset
   271
                let val e = empty_spmat in (e, e) end
22951
dfafcd6223ad whitespace tuned
haftmann
parents: 21056
diff changeset
   272
            else
dfafcd6223ad whitespace tuned
haftmann
parents: 21056
diff changeset
   273
                let
dfafcd6223ad whitespace tuned
haftmann
parents: 21056
diff changeset
   274
                    val index = xlen-i
24302
obua
parents: 24135
diff changeset
   275
                    val (r12_1, r12_2) = abs_estimate (i-1) r1 r2
obua
parents: 24135
diff changeset
   276
                    val b1 = Inttab.lookup r1 index
24630
351a308ab58d simplified type int (eliminated IntInf.int, integer);
wenzelm
parents: 24302
diff changeset
   277
                    val b2 = Inttab.lookup r2 index
22951
dfafcd6223ad whitespace tuned
haftmann
parents: 21056
diff changeset
   278
                in
24630
351a308ab58d simplified type int (eliminated IntInf.int, integer);
wenzelm
parents: 24302
diff changeset
   279
                    (add_row_entry r12_1 index @{term "lbound :: real => real"} ((names index)^"l") b1, 
32960
69916a850301 eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents: 31971
diff changeset
   280
                     add_row_entry r12_2 index @{term "ubound :: real => real"} ((names index)^"u") b2)
22951
dfafcd6223ad whitespace tuned
haftmann
parents: 21056
diff changeset
   281
                end
23665
825bea0266db adopted to new computing oracle and fixed bugs introduced by tuning
obua
parents: 23520
diff changeset
   282
24302
obua
parents: 24135
diff changeset
   283
        val (r1, r2) = abs_estimate xlen r1 r2
23665
825bea0266db adopted to new computing oracle and fixed bugs introduced by tuning
obua
parents: 23520
diff changeset
   284
16784
92ff7c903585 - added cplex package to HOL/Matrix
obua
parents:
diff changeset
   285
    in
24302
obua
parents: 24135
diff changeset
   286
        (r1, r2)
16784
92ff7c903585 - added cplex package to HOL/Matrix
obua
parents:
diff changeset
   287
    end
22951
dfafcd6223ad whitespace tuned
haftmann
parents: 21056
diff changeset
   288
16784
92ff7c903585 - added cplex package to HOL/Matrix
obua
parents:
diff changeset
   289
fun load filename prec safe_propagation =
92ff7c903585 - added cplex package to HOL/Matrix
obua
parents:
diff changeset
   290
    let
22951
dfafcd6223ad whitespace tuned
haftmann
parents: 21056
diff changeset
   291
        val prog = Cplex.load_cplexFile filename
dfafcd6223ad whitespace tuned
haftmann
parents: 21056
diff changeset
   292
        val prog = Cplex.elim_nonfree_bounds prog
dfafcd6223ad whitespace tuned
haftmann
parents: 21056
diff changeset
   293
        val prog = Cplex.relax_strict_ineqs prog
32960
69916a850301 eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents: 31971
diff changeset
   294
        val (maximize, c, A, b, (xlen, names, _)) = CplexFloatSparseMatrixConverter.convert_prog prog                       
24302
obua
parents: 24135
diff changeset
   295
        val (r1, r2) = calcr safe_propagation xlen names prec A b
22951
dfafcd6223ad whitespace tuned
haftmann
parents: 21056
diff changeset
   296
        val _ = if maximize then () else raise Load "sorry, cannot handle minimization problems"
dfafcd6223ad whitespace tuned
haftmann
parents: 21056
diff changeset
   297
        val (dualprog, indexof) = FloatSparseMatrixBuilder.dual_cplexProg c A b
dfafcd6223ad whitespace tuned
haftmann
parents: 21056
diff changeset
   298
        val results = Cplex.solve dualprog
46533
faf233c4a404 dropped dead code
haftmann
parents: 37788
diff changeset
   299
        val (_, v) = CplexFloatSparseMatrixConverter.convert_results results indexof
24302
obua
parents: 24135
diff changeset
   300
        (*val A = FloatSparseMatrixBuilder.cut_matrix v NONE A*)
22951
dfafcd6223ad whitespace tuned
haftmann
parents: 21056
diff changeset
   301
        fun id x = x
dfafcd6223ad whitespace tuned
haftmann
parents: 21056
diff changeset
   302
        val v = FloatSparseMatrixBuilder.set_vector FloatSparseMatrixBuilder.empty_matrix 0 v
dfafcd6223ad whitespace tuned
haftmann
parents: 21056
diff changeset
   303
        val b = FloatSparseMatrixBuilder.transpose_matrix (FloatSparseMatrixBuilder.set_vector FloatSparseMatrixBuilder.empty_matrix 0 b)
dfafcd6223ad whitespace tuned
haftmann
parents: 21056
diff changeset
   304
        val c = FloatSparseMatrixBuilder.set_vector FloatSparseMatrixBuilder.empty_matrix 0 c
22964
2284e0d02e7f reorganized float arithmetic
haftmann
parents: 22951
diff changeset
   305
        val (y1, _) = FloatSparseMatrixBuilder.approx_matrix prec Float.positive_part v
22951
dfafcd6223ad whitespace tuned
haftmann
parents: 21056
diff changeset
   306
        val A = FloatSparseMatrixBuilder.approx_matrix prec id A
dfafcd6223ad whitespace tuned
haftmann
parents: 21056
diff changeset
   307
        val (_,b2) = FloatSparseMatrixBuilder.approx_matrix prec id b
dfafcd6223ad whitespace tuned
haftmann
parents: 21056
diff changeset
   308
        val c = FloatSparseMatrixBuilder.approx_matrix prec id c
16784
92ff7c903585 - added cplex package to HOL/Matrix
obua
parents:
diff changeset
   309
    in
24302
obua
parents: 24135
diff changeset
   310
        (y1, A, b2, c, (r1, r2))
22951
dfafcd6223ad whitespace tuned
haftmann
parents: 21056
diff changeset
   311
    end handle CplexFloatSparseMatrixConverter.Converter s => (raise (Load ("Converter: "^s)))
16784
92ff7c903585 - added cplex package to HOL/Matrix
obua
parents:
diff changeset
   312
92ff7c903585 - added cplex package to HOL/Matrix
obua
parents:
diff changeset
   313
end