src/HOL/Matrix/cplex/FloatSparseMatrixBuilder.ML
author obua
Fri, 17 Aug 2007 09:20:45 +0200
changeset 24302 3045683749af
parent 23883 7d5aa704454e
child 24630 351a308ab58d
permissions -rw-r--r--
tuned
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
16784
92ff7c903585 - added cplex package to HOL/Matrix
obua
parents:
diff changeset
     1
(*  Title:      HOL/Matrix/cplex/FloatSparseMatrixBuilder.ML
92ff7c903585 - added cplex package to HOL/Matrix
obua
parents:
diff changeset
     2
    ID:         $Id$
92ff7c903585 - added cplex package to HOL/Matrix
obua
parents:
diff changeset
     3
    Author:     Steven Obua
92ff7c903585 - added cplex package to HOL/Matrix
obua
parents:
diff changeset
     4
*)
92ff7c903585 - added cplex package to HOL/Matrix
obua
parents:
diff changeset
     5
22964
2284e0d02e7f reorganized float arithmetic
haftmann
parents: 22951
diff changeset
     6
signature FLOAT_SPARSE_MATIRX_BUILDER =
16784
92ff7c903585 - added cplex package to HOL/Matrix
obua
parents:
diff changeset
     7
sig
22964
2284e0d02e7f reorganized float arithmetic
haftmann
parents: 22951
diff changeset
     8
  include MATRIX_BUILDER
16784
92ff7c903585 - added cplex package to HOL/Matrix
obua
parents:
diff changeset
     9
22964
2284e0d02e7f reorganized float arithmetic
haftmann
parents: 22951
diff changeset
    10
  structure cplex : CPLEX
16784
92ff7c903585 - added cplex package to HOL/Matrix
obua
parents:
diff changeset
    11
22964
2284e0d02e7f reorganized float arithmetic
haftmann
parents: 22951
diff changeset
    12
  type float = Float.float
2284e0d02e7f reorganized float arithmetic
haftmann
parents: 22951
diff changeset
    13
  val approx_value : int -> (float -> float) -> string -> term * term
2284e0d02e7f reorganized float arithmetic
haftmann
parents: 22951
diff changeset
    14
  val approx_vector : int -> (float -> float) -> vector -> term * term
2284e0d02e7f reorganized float arithmetic
haftmann
parents: 22951
diff changeset
    15
  val approx_matrix : int -> (float -> float) -> matrix -> term * term
16784
92ff7c903585 - added cplex package to HOL/Matrix
obua
parents:
diff changeset
    16
23261
85f27f79232f tuned integers
haftmann
parents: 22964
diff changeset
    17
  val mk_spvec_entry : integer -> float -> term
24302
obua
parents: 23883
diff changeset
    18
  val mk_spvec_entry' : integer -> term -> term
23261
85f27f79232f tuned integers
haftmann
parents: 22964
diff changeset
    19
  val mk_spmat_entry : integer -> term -> term
22964
2284e0d02e7f reorganized float arithmetic
haftmann
parents: 22951
diff changeset
    20
  val spvecT: typ
2284e0d02e7f reorganized float arithmetic
haftmann
parents: 22951
diff changeset
    21
  val spmatT: typ
2284e0d02e7f reorganized float arithmetic
haftmann
parents: 22951
diff changeset
    22
  
2284e0d02e7f reorganized float arithmetic
haftmann
parents: 22951
diff changeset
    23
  val v_elem_at : vector -> int -> string option
2284e0d02e7f reorganized float arithmetic
haftmann
parents: 22951
diff changeset
    24
  val m_elem_at : matrix -> int -> vector option
2284e0d02e7f reorganized float arithmetic
haftmann
parents: 22951
diff changeset
    25
  val v_only_elem : vector -> int option
2284e0d02e7f reorganized float arithmetic
haftmann
parents: 22951
diff changeset
    26
  val v_fold : (int * string -> 'a -> 'a) -> vector -> 'a -> 'a
2284e0d02e7f reorganized float arithmetic
haftmann
parents: 22951
diff changeset
    27
  val m_fold : (int * vector -> 'a -> 'a) -> matrix -> 'a -> 'a
20485
3078fd2eec7b got rid of Numeral.bin type
haftmann
parents: 17412
diff changeset
    28
22964
2284e0d02e7f reorganized float arithmetic
haftmann
parents: 22951
diff changeset
    29
  val transpose_matrix : matrix -> matrix
16784
92ff7c903585 - added cplex package to HOL/Matrix
obua
parents:
diff changeset
    30
22964
2284e0d02e7f reorganized float arithmetic
haftmann
parents: 22951
diff changeset
    31
  val cut_vector : int -> vector -> vector
2284e0d02e7f reorganized float arithmetic
haftmann
parents: 22951
diff changeset
    32
  val cut_matrix : vector -> int option -> matrix -> matrix
22951
dfafcd6223ad whitespace tuned
haftmann
parents: 22578
diff changeset
    33
23883
7d5aa704454e new functions cut_matrix', etc.
obua
parents: 23665
diff changeset
    34
  val delete_matrix : int list -> matrix -> matrix
7d5aa704454e new functions cut_matrix', etc.
obua
parents: 23665
diff changeset
    35
  val cut_matrix' : int list -> matrix -> matrix 
7d5aa704454e new functions cut_matrix', etc.
obua
parents: 23665
diff changeset
    36
  val delete_vector : int list -> vector -> vector
7d5aa704454e new functions cut_matrix', etc.
obua
parents: 23665
diff changeset
    37
  val cut_vector' : int list -> vector -> vector
7d5aa704454e new functions cut_matrix', etc.
obua
parents: 23665
diff changeset
    38
7d5aa704454e new functions cut_matrix', etc.
obua
parents: 23665
diff changeset
    39
  val indices_of_matrix : matrix -> int list
7d5aa704454e new functions cut_matrix', etc.
obua
parents: 23665
diff changeset
    40
  val indices_of_vector : vector -> int list
7d5aa704454e new functions cut_matrix', etc.
obua
parents: 23665
diff changeset
    41
22964
2284e0d02e7f reorganized float arithmetic
haftmann
parents: 22951
diff changeset
    42
  (* cplexProg c A b *)
2284e0d02e7f reorganized float arithmetic
haftmann
parents: 22951
diff changeset
    43
  val cplexProg : vector -> matrix -> vector -> cplex.cplexProg * (string -> int)
2284e0d02e7f reorganized float arithmetic
haftmann
parents: 22951
diff changeset
    44
  (* dual_cplexProg c A b *)
2284e0d02e7f reorganized float arithmetic
haftmann
parents: 22951
diff changeset
    45
  val dual_cplexProg : vector -> matrix -> vector -> cplex.cplexProg * (string -> int)
2284e0d02e7f reorganized float arithmetic
haftmann
parents: 22951
diff changeset
    46
end;
16784
92ff7c903585 - added cplex package to HOL/Matrix
obua
parents:
diff changeset
    47
22964
2284e0d02e7f reorganized float arithmetic
haftmann
parents: 22951
diff changeset
    48
structure FloatSparseMatrixBuilder : FLOAT_SPARSE_MATIRX_BUILDER =
16784
92ff7c903585 - added cplex package to HOL/Matrix
obua
parents:
diff changeset
    49
struct
92ff7c903585 - added cplex package to HOL/Matrix
obua
parents:
diff changeset
    50
22964
2284e0d02e7f reorganized float arithmetic
haftmann
parents: 22951
diff changeset
    51
type float = Float.float
2284e0d02e7f reorganized float arithmetic
haftmann
parents: 22951
diff changeset
    52
structure Inttab = TableFun(type key = int val ord = rev_order o int_ord);
16784
92ff7c903585 - added cplex package to HOL/Matrix
obua
parents:
diff changeset
    53
92ff7c903585 - added cplex package to HOL/Matrix
obua
parents:
diff changeset
    54
type vector = string Inttab.table
92ff7c903585 - added cplex package to HOL/Matrix
obua
parents:
diff changeset
    55
type matrix = vector Inttab.table
20485
3078fd2eec7b got rid of Numeral.bin type
haftmann
parents: 17412
diff changeset
    56
22964
2284e0d02e7f reorganized float arithmetic
haftmann
parents: 22951
diff changeset
    57
val spvec_elemT = HOLogic.mk_prodT (HOLogic.natT, HOLogic.realT);
2284e0d02e7f reorganized float arithmetic
haftmann
parents: 22951
diff changeset
    58
val spvecT = HOLogic.listT spvec_elemT;
2284e0d02e7f reorganized float arithmetic
haftmann
parents: 22951
diff changeset
    59
val spmat_elemT = HOLogic.mk_prodT (HOLogic.natT, spvecT);
2284e0d02e7f reorganized float arithmetic
haftmann
parents: 22951
diff changeset
    60
val spmatT = HOLogic.listT spmat_elemT;
16784
92ff7c903585 - added cplex package to HOL/Matrix
obua
parents:
diff changeset
    61
22964
2284e0d02e7f reorganized float arithmetic
haftmann
parents: 22951
diff changeset
    62
fun approx_value prec f =
2284e0d02e7f reorganized float arithmetic
haftmann
parents: 22951
diff changeset
    63
  FloatArith.approx_float prec (fn (x, y) => (f x, f y));
16784
92ff7c903585 - added cplex package to HOL/Matrix
obua
parents:
diff changeset
    64
22951
dfafcd6223ad whitespace tuned
haftmann
parents: 22578
diff changeset
    65
fun mk_spvec_entry i f =
22964
2284e0d02e7f reorganized float arithmetic
haftmann
parents: 22951
diff changeset
    66
  HOLogic.mk_prod (HOLogic.mk_number HOLogic.natT i, FloatArith.mk_float f);
16784
92ff7c903585 - added cplex package to HOL/Matrix
obua
parents:
diff changeset
    67
24302
obua
parents: 23883
diff changeset
    68
fun mk_spvec_entry' i x =
obua
parents: 23883
diff changeset
    69
  HOLogic.mk_prod (HOLogic.mk_number HOLogic.natT i, x);
obua
parents: 23883
diff changeset
    70
22951
dfafcd6223ad whitespace tuned
haftmann
parents: 22578
diff changeset
    71
fun mk_spmat_entry i e =
22964
2284e0d02e7f reorganized float arithmetic
haftmann
parents: 22951
diff changeset
    72
  HOLogic.mk_prod (HOLogic.mk_number HOLogic.natT i, e);
16784
92ff7c903585 - added cplex package to HOL/Matrix
obua
parents:
diff changeset
    73
92ff7c903585 - added cplex package to HOL/Matrix
obua
parents:
diff changeset
    74
fun approx_vector prec pprt vector =
22964
2284e0d02e7f reorganized float arithmetic
haftmann
parents: 22951
diff changeset
    75
  let
2284e0d02e7f reorganized float arithmetic
haftmann
parents: 22951
diff changeset
    76
    fun app (index, s) (lower, upper) =
2284e0d02e7f reorganized float arithmetic
haftmann
parents: 22951
diff changeset
    77
      let
2284e0d02e7f reorganized float arithmetic
haftmann
parents: 22951
diff changeset
    78
        val (flower, fupper) = approx_value prec pprt s
23261
85f27f79232f tuned integers
haftmann
parents: 22964
diff changeset
    79
        val index = HOLogic.mk_number HOLogic.natT (Integer.int index)
22964
2284e0d02e7f reorganized float arithmetic
haftmann
parents: 22951
diff changeset
    80
        val elower = HOLogic.mk_prod (index, flower)
2284e0d02e7f reorganized float arithmetic
haftmann
parents: 22951
diff changeset
    81
        val eupper = HOLogic.mk_prod (index, fupper)
2284e0d02e7f reorganized float arithmetic
haftmann
parents: 22951
diff changeset
    82
      in (elower :: lower, eupper :: upper) end;
2284e0d02e7f reorganized float arithmetic
haftmann
parents: 22951
diff changeset
    83
  in
23665
825bea0266db adopted to new computing oracle and fixed bugs introduced by tuning
obua
parents: 23261
diff changeset
    84
    pairself (HOLogic.mk_list spvec_elemT) (Inttab.fold app vector ([], []))
22964
2284e0d02e7f reorganized float arithmetic
haftmann
parents: 22951
diff changeset
    85
  end;
16784
92ff7c903585 - added cplex package to HOL/Matrix
obua
parents:
diff changeset
    86
22964
2284e0d02e7f reorganized float arithmetic
haftmann
parents: 22951
diff changeset
    87
fun approx_matrix prec pprt vector =
2284e0d02e7f reorganized float arithmetic
haftmann
parents: 22951
diff changeset
    88
  let
2284e0d02e7f reorganized float arithmetic
haftmann
parents: 22951
diff changeset
    89
    fun app (index, v) (lower, upper) =
2284e0d02e7f reorganized float arithmetic
haftmann
parents: 22951
diff changeset
    90
      let
2284e0d02e7f reorganized float arithmetic
haftmann
parents: 22951
diff changeset
    91
        val (flower, fupper) = approx_vector prec pprt v
23261
85f27f79232f tuned integers
haftmann
parents: 22964
diff changeset
    92
        val index = HOLogic.mk_number HOLogic.natT (Integer.int index)
22964
2284e0d02e7f reorganized float arithmetic
haftmann
parents: 22951
diff changeset
    93
        val elower = HOLogic.mk_prod (index, flower)
2284e0d02e7f reorganized float arithmetic
haftmann
parents: 22951
diff changeset
    94
        val eupper = HOLogic.mk_prod (index, fupper)
2284e0d02e7f reorganized float arithmetic
haftmann
parents: 22951
diff changeset
    95
      in (elower :: lower, eupper :: upper) end;
2284e0d02e7f reorganized float arithmetic
haftmann
parents: 22951
diff changeset
    96
  in
23665
825bea0266db adopted to new computing oracle and fixed bugs introduced by tuning
obua
parents: 23261
diff changeset
    97
    pairself (HOLogic.mk_list spmat_elemT) (Inttab.fold app vector ([], []))
22964
2284e0d02e7f reorganized float arithmetic
haftmann
parents: 22951
diff changeset
    98
  end;
16784
92ff7c903585 - added cplex package to HOL/Matrix
obua
parents:
diff changeset
    99
92ff7c903585 - added cplex package to HOL/Matrix
obua
parents:
diff changeset
   100
exception Nat_expected of int;
92ff7c903585 - added cplex package to HOL/Matrix
obua
parents:
diff changeset
   101
22964
2284e0d02e7f reorganized float arithmetic
haftmann
parents: 22951
diff changeset
   102
val zero_interval = approx_value 1 I "0"
16784
92ff7c903585 - added cplex package to HOL/Matrix
obua
parents:
diff changeset
   103
22951
dfafcd6223ad whitespace tuned
haftmann
parents: 22578
diff changeset
   104
fun set_elem vector index str =
dfafcd6223ad whitespace tuned
haftmann
parents: 22578
diff changeset
   105
    if index < 0 then
dfafcd6223ad whitespace tuned
haftmann
parents: 22578
diff changeset
   106
        raise (Nat_expected index)
22964
2284e0d02e7f reorganized float arithmetic
haftmann
parents: 22951
diff changeset
   107
    else if (approx_value 1 I str) = zero_interval then
22951
dfafcd6223ad whitespace tuned
haftmann
parents: 22578
diff changeset
   108
        vector
dfafcd6223ad whitespace tuned
haftmann
parents: 22578
diff changeset
   109
    else
dfafcd6223ad whitespace tuned
haftmann
parents: 22578
diff changeset
   110
        Inttab.update (index, str) vector
16784
92ff7c903585 - added cplex package to HOL/Matrix
obua
parents:
diff changeset
   111
22951
dfafcd6223ad whitespace tuned
haftmann
parents: 22578
diff changeset
   112
fun set_vector matrix index vector =
16784
92ff7c903585 - added cplex package to HOL/Matrix
obua
parents:
diff changeset
   113
    if index < 0 then
22951
dfafcd6223ad whitespace tuned
haftmann
parents: 22578
diff changeset
   114
        raise (Nat_expected index)
16784
92ff7c903585 - added cplex package to HOL/Matrix
obua
parents:
diff changeset
   115
    else if Inttab.is_empty vector then
22951
dfafcd6223ad whitespace tuned
haftmann
parents: 22578
diff changeset
   116
        matrix
16784
92ff7c903585 - added cplex package to HOL/Matrix
obua
parents:
diff changeset
   117
    else
22951
dfafcd6223ad whitespace tuned
haftmann
parents: 22578
diff changeset
   118
        Inttab.update (index, vector) matrix
16784
92ff7c903585 - added cplex package to HOL/Matrix
obua
parents:
diff changeset
   119
92ff7c903585 - added cplex package to HOL/Matrix
obua
parents:
diff changeset
   120
val empty_matrix = Inttab.empty
92ff7c903585 - added cplex package to HOL/Matrix
obua
parents:
diff changeset
   121
val empty_vector = Inttab.empty
92ff7c903585 - added cplex package to HOL/Matrix
obua
parents:
diff changeset
   122
92ff7c903585 - added cplex package to HOL/Matrix
obua
parents:
diff changeset
   123
(* dual stuff *)
92ff7c903585 - added cplex package to HOL/Matrix
obua
parents:
diff changeset
   124
92ff7c903585 - added cplex package to HOL/Matrix
obua
parents:
diff changeset
   125
structure cplex = Cplex
92ff7c903585 - added cplex package to HOL/Matrix
obua
parents:
diff changeset
   126
22951
dfafcd6223ad whitespace tuned
haftmann
parents: 22578
diff changeset
   127
fun transpose_matrix matrix =
21056
2cfe839e8d58 Symtab.foldl replaced by Symtab.fold
haftmann
parents: 20485
diff changeset
   128
  let
2cfe839e8d58 Symtab.foldl replaced by Symtab.fold
haftmann
parents: 20485
diff changeset
   129
    fun upd j (i, s) =
2cfe839e8d58 Symtab.foldl replaced by Symtab.fold
haftmann
parents: 20485
diff changeset
   130
      Inttab.map_default (i, Inttab.empty) (Inttab.update (j, s));
2cfe839e8d58 Symtab.foldl replaced by Symtab.fold
haftmann
parents: 20485
diff changeset
   131
    fun updm (j, v) = Inttab.fold (upd j) v;
2cfe839e8d58 Symtab.foldl replaced by Symtab.fold
haftmann
parents: 20485
diff changeset
   132
  in Inttab.fold updm matrix empty_matrix end;
16784
92ff7c903585 - added cplex package to HOL/Matrix
obua
parents:
diff changeset
   133
92ff7c903585 - added cplex package to HOL/Matrix
obua
parents:
diff changeset
   134
exception No_name of string;
92ff7c903585 - added cplex package to HOL/Matrix
obua
parents:
diff changeset
   135
92ff7c903585 - added cplex package to HOL/Matrix
obua
parents:
diff changeset
   136
exception Superfluous_constr_right_hand_sides
92ff7c903585 - added cplex package to HOL/Matrix
obua
parents:
diff changeset
   137
22951
dfafcd6223ad whitespace tuned
haftmann
parents: 22578
diff changeset
   138
fun cplexProg c A b =
16784
92ff7c903585 - added cplex package to HOL/Matrix
obua
parents:
diff changeset
   139
    let
22951
dfafcd6223ad whitespace tuned
haftmann
parents: 22578
diff changeset
   140
        val ytable = ref Inttab.empty
dfafcd6223ad whitespace tuned
haftmann
parents: 22578
diff changeset
   141
        fun indexof s =
dfafcd6223ad whitespace tuned
haftmann
parents: 22578
diff changeset
   142
            if String.size s = 0 then raise (No_name s)
dfafcd6223ad whitespace tuned
haftmann
parents: 22578
diff changeset
   143
            else case Int.fromString (String.extract(s, 1, NONE)) of
dfafcd6223ad whitespace tuned
haftmann
parents: 22578
diff changeset
   144
                     SOME i => i | NONE => raise (No_name s)
16784
92ff7c903585 - added cplex package to HOL/Matrix
obua
parents:
diff changeset
   145
22951
dfafcd6223ad whitespace tuned
haftmann
parents: 22578
diff changeset
   146
        fun nameof i =
dfafcd6223ad whitespace tuned
haftmann
parents: 22578
diff changeset
   147
            let
dfafcd6223ad whitespace tuned
haftmann
parents: 22578
diff changeset
   148
                val s = "x"^(Int.toString i)
dfafcd6223ad whitespace tuned
haftmann
parents: 22578
diff changeset
   149
                val _ = change ytable (Inttab.update (i, s))
dfafcd6223ad whitespace tuned
haftmann
parents: 22578
diff changeset
   150
            in
dfafcd6223ad whitespace tuned
haftmann
parents: 22578
diff changeset
   151
                s
dfafcd6223ad whitespace tuned
haftmann
parents: 22578
diff changeset
   152
            end
dfafcd6223ad whitespace tuned
haftmann
parents: 22578
diff changeset
   153
dfafcd6223ad whitespace tuned
haftmann
parents: 22578
diff changeset
   154
        fun split_numstr s =
dfafcd6223ad whitespace tuned
haftmann
parents: 22578
diff changeset
   155
            if String.isPrefix "-" s then (false,String.extract(s, 1, NONE))
dfafcd6223ad whitespace tuned
haftmann
parents: 22578
diff changeset
   156
            else if String.isPrefix "+" s then (true, String.extract(s, 1, NONE))
dfafcd6223ad whitespace tuned
haftmann
parents: 22578
diff changeset
   157
            else (true, s)
dfafcd6223ad whitespace tuned
haftmann
parents: 22578
diff changeset
   158
dfafcd6223ad whitespace tuned
haftmann
parents: 22578
diff changeset
   159
        fun mk_term index s =
dfafcd6223ad whitespace tuned
haftmann
parents: 22578
diff changeset
   160
            let
dfafcd6223ad whitespace tuned
haftmann
parents: 22578
diff changeset
   161
                val (p, s) = split_numstr s
dfafcd6223ad whitespace tuned
haftmann
parents: 22578
diff changeset
   162
                val prod = cplex.cplexProd (cplex.cplexNum s, cplex.cplexVar (nameof index))
dfafcd6223ad whitespace tuned
haftmann
parents: 22578
diff changeset
   163
            in
dfafcd6223ad whitespace tuned
haftmann
parents: 22578
diff changeset
   164
                if p then prod else cplex.cplexNeg prod
dfafcd6223ad whitespace tuned
haftmann
parents: 22578
diff changeset
   165
            end
16784
92ff7c903585 - added cplex package to HOL/Matrix
obua
parents:
diff changeset
   166
22951
dfafcd6223ad whitespace tuned
haftmann
parents: 22578
diff changeset
   167
        fun vec2sum vector =
dfafcd6223ad whitespace tuned
haftmann
parents: 22578
diff changeset
   168
            cplex.cplexSum (Inttab.fold (fn (index, s) => fn list => (mk_term index s) :: list) vector [])
16784
92ff7c903585 - added cplex package to HOL/Matrix
obua
parents:
diff changeset
   169
22951
dfafcd6223ad whitespace tuned
haftmann
parents: 22578
diff changeset
   170
        fun mk_constr index vector c =
dfafcd6223ad whitespace tuned
haftmann
parents: 22578
diff changeset
   171
            let
dfafcd6223ad whitespace tuned
haftmann
parents: 22578
diff changeset
   172
                val s = case Inttab.lookup c index of SOME s => s | NONE => "0"
dfafcd6223ad whitespace tuned
haftmann
parents: 22578
diff changeset
   173
                val (p, s) = split_numstr s
dfafcd6223ad whitespace tuned
haftmann
parents: 22578
diff changeset
   174
                val num = if p then cplex.cplexNum s else cplex.cplexNeg (cplex.cplexNum s)
dfafcd6223ad whitespace tuned
haftmann
parents: 22578
diff changeset
   175
            in
dfafcd6223ad whitespace tuned
haftmann
parents: 22578
diff changeset
   176
                (NONE, cplex.cplexConstr (cplex.cplexLeq, (vec2sum vector, num)))
dfafcd6223ad whitespace tuned
haftmann
parents: 22578
diff changeset
   177
            end
dfafcd6223ad whitespace tuned
haftmann
parents: 22578
diff changeset
   178
dfafcd6223ad whitespace tuned
haftmann
parents: 22578
diff changeset
   179
        fun delete index c = Inttab.delete index c handle Inttab.UNDEF _ => c
16784
92ff7c903585 - added cplex package to HOL/Matrix
obua
parents:
diff changeset
   180
22951
dfafcd6223ad whitespace tuned
haftmann
parents: 22578
diff changeset
   181
        val (list, b) = Inttab.fold
dfafcd6223ad whitespace tuned
haftmann
parents: 22578
diff changeset
   182
                            (fn (index, v) => fn (list, c) => ((mk_constr index v c)::list, delete index c))
dfafcd6223ad whitespace tuned
haftmann
parents: 22578
diff changeset
   183
                            A ([], b)
dfafcd6223ad whitespace tuned
haftmann
parents: 22578
diff changeset
   184
        val _ = if Inttab.is_empty b then () else raise Superfluous_constr_right_hand_sides
16784
92ff7c903585 - added cplex package to HOL/Matrix
obua
parents:
diff changeset
   185
22951
dfafcd6223ad whitespace tuned
haftmann
parents: 22578
diff changeset
   186
        fun mk_free y = cplex.cplexBounds (cplex.cplexNeg cplex.cplexInf, cplex.cplexLeq,
dfafcd6223ad whitespace tuned
haftmann
parents: 22578
diff changeset
   187
                                           cplex.cplexVar y, cplex.cplexLeq,
dfafcd6223ad whitespace tuned
haftmann
parents: 22578
diff changeset
   188
                                           cplex.cplexInf)
16784
92ff7c903585 - added cplex package to HOL/Matrix
obua
parents:
diff changeset
   189
22951
dfafcd6223ad whitespace tuned
haftmann
parents: 22578
diff changeset
   190
        val yvars = Inttab.fold (fn (i, y) => fn l => (mk_free y)::l) (!ytable) []
16784
92ff7c903585 - added cplex package to HOL/Matrix
obua
parents:
diff changeset
   191
22951
dfafcd6223ad whitespace tuned
haftmann
parents: 22578
diff changeset
   192
        val prog = cplex.cplexProg ("original", cplex.cplexMaximize (vec2sum c), list, yvars)
16784
92ff7c903585 - added cplex package to HOL/Matrix
obua
parents:
diff changeset
   193
    in
22951
dfafcd6223ad whitespace tuned
haftmann
parents: 22578
diff changeset
   194
        (prog, indexof)
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
22951
dfafcd6223ad whitespace tuned
haftmann
parents: 22578
diff changeset
   198
fun dual_cplexProg c A b =
16784
92ff7c903585 - added cplex package to HOL/Matrix
obua
parents:
diff changeset
   199
    let
22951
dfafcd6223ad whitespace tuned
haftmann
parents: 22578
diff changeset
   200
        fun indexof s =
dfafcd6223ad whitespace tuned
haftmann
parents: 22578
diff changeset
   201
            if String.size s = 0 then raise (No_name s)
dfafcd6223ad whitespace tuned
haftmann
parents: 22578
diff changeset
   202
            else case Int.fromString (String.extract(s, 1, NONE)) of
dfafcd6223ad whitespace tuned
haftmann
parents: 22578
diff changeset
   203
                     SOME i => i | NONE => raise (No_name s)
dfafcd6223ad whitespace tuned
haftmann
parents: 22578
diff changeset
   204
dfafcd6223ad whitespace tuned
haftmann
parents: 22578
diff changeset
   205
        fun nameof i = "y"^(Int.toString i)
16784
92ff7c903585 - added cplex package to HOL/Matrix
obua
parents:
diff changeset
   206
22951
dfafcd6223ad whitespace tuned
haftmann
parents: 22578
diff changeset
   207
        fun split_numstr s =
dfafcd6223ad whitespace tuned
haftmann
parents: 22578
diff changeset
   208
            if String.isPrefix "-" s then (false,String.extract(s, 1, NONE))
dfafcd6223ad whitespace tuned
haftmann
parents: 22578
diff changeset
   209
            else if String.isPrefix "+" s then (true, String.extract(s, 1, NONE))
dfafcd6223ad whitespace tuned
haftmann
parents: 22578
diff changeset
   210
            else (true, s)
dfafcd6223ad whitespace tuned
haftmann
parents: 22578
diff changeset
   211
dfafcd6223ad whitespace tuned
haftmann
parents: 22578
diff changeset
   212
        fun mk_term index s =
dfafcd6223ad whitespace tuned
haftmann
parents: 22578
diff changeset
   213
            let
dfafcd6223ad whitespace tuned
haftmann
parents: 22578
diff changeset
   214
                val (p, s) = split_numstr s
dfafcd6223ad whitespace tuned
haftmann
parents: 22578
diff changeset
   215
                val prod = cplex.cplexProd (cplex.cplexNum s, cplex.cplexVar (nameof index))
dfafcd6223ad whitespace tuned
haftmann
parents: 22578
diff changeset
   216
            in
dfafcd6223ad whitespace tuned
haftmann
parents: 22578
diff changeset
   217
                if p then prod else cplex.cplexNeg prod
dfafcd6223ad whitespace tuned
haftmann
parents: 22578
diff changeset
   218
            end
16784
92ff7c903585 - added cplex package to HOL/Matrix
obua
parents:
diff changeset
   219
22951
dfafcd6223ad whitespace tuned
haftmann
parents: 22578
diff changeset
   220
        fun vec2sum vector =
dfafcd6223ad whitespace tuned
haftmann
parents: 22578
diff changeset
   221
            cplex.cplexSum (Inttab.fold (fn (index, s) => fn list => (mk_term index s)::list) vector [])
16784
92ff7c903585 - added cplex package to HOL/Matrix
obua
parents:
diff changeset
   222
22951
dfafcd6223ad whitespace tuned
haftmann
parents: 22578
diff changeset
   223
        fun mk_constr index vector c =
dfafcd6223ad whitespace tuned
haftmann
parents: 22578
diff changeset
   224
            let
dfafcd6223ad whitespace tuned
haftmann
parents: 22578
diff changeset
   225
                val s = case Inttab.lookup c index of SOME s => s | NONE => "0"
dfafcd6223ad whitespace tuned
haftmann
parents: 22578
diff changeset
   226
                val (p, s) = split_numstr s
dfafcd6223ad whitespace tuned
haftmann
parents: 22578
diff changeset
   227
                val num = if p then cplex.cplexNum s else cplex.cplexNeg (cplex.cplexNum s)
dfafcd6223ad whitespace tuned
haftmann
parents: 22578
diff changeset
   228
            in
dfafcd6223ad whitespace tuned
haftmann
parents: 22578
diff changeset
   229
                (NONE, cplex.cplexConstr (cplex.cplexEq, (vec2sum vector, num)))
dfafcd6223ad whitespace tuned
haftmann
parents: 22578
diff changeset
   230
            end
16784
92ff7c903585 - added cplex package to HOL/Matrix
obua
parents:
diff changeset
   231
22951
dfafcd6223ad whitespace tuned
haftmann
parents: 22578
diff changeset
   232
        fun delete index c = Inttab.delete index c handle Inttab.UNDEF _ => c
16784
92ff7c903585 - added cplex package to HOL/Matrix
obua
parents:
diff changeset
   233
22951
dfafcd6223ad whitespace tuned
haftmann
parents: 22578
diff changeset
   234
        val (list, c) = Inttab.fold
dfafcd6223ad whitespace tuned
haftmann
parents: 22578
diff changeset
   235
                            (fn (index, v) => fn (list, c) => ((mk_constr index v c)::list, delete index c))
dfafcd6223ad whitespace tuned
haftmann
parents: 22578
diff changeset
   236
                            (transpose_matrix A) ([], c)
dfafcd6223ad whitespace tuned
haftmann
parents: 22578
diff changeset
   237
        val _ = if Inttab.is_empty c then () else raise Superfluous_constr_right_hand_sides
dfafcd6223ad whitespace tuned
haftmann
parents: 22578
diff changeset
   238
dfafcd6223ad whitespace tuned
haftmann
parents: 22578
diff changeset
   239
        val prog = cplex.cplexProg ("dual", cplex.cplexMinimize (vec2sum b), list, [])
16784
92ff7c903585 - added cplex package to HOL/Matrix
obua
parents:
diff changeset
   240
    in
22951
dfafcd6223ad whitespace tuned
haftmann
parents: 22578
diff changeset
   241
        (prog, indexof)
16784
92ff7c903585 - added cplex package to HOL/Matrix
obua
parents:
diff changeset
   242
    end
92ff7c903585 - added cplex package to HOL/Matrix
obua
parents:
diff changeset
   243
22951
dfafcd6223ad whitespace tuned
haftmann
parents: 22578
diff changeset
   244
fun cut_vector size v =
21056
2cfe839e8d58 Symtab.foldl replaced by Symtab.fold
haftmann
parents: 20485
diff changeset
   245
  let
2cfe839e8d58 Symtab.foldl replaced by Symtab.fold
haftmann
parents: 20485
diff changeset
   246
    val count = ref 0;
2cfe839e8d58 Symtab.foldl replaced by Symtab.fold
haftmann
parents: 20485
diff changeset
   247
    fun app (i, s) =  if (!count < size) then
2cfe839e8d58 Symtab.foldl replaced by Symtab.fold
haftmann
parents: 20485
diff changeset
   248
        (count := !count +1 ; Inttab.update (i, s))
2cfe839e8d58 Symtab.foldl replaced by Symtab.fold
haftmann
parents: 20485
diff changeset
   249
      else I
2cfe839e8d58 Symtab.foldl replaced by Symtab.fold
haftmann
parents: 20485
diff changeset
   250
  in
2cfe839e8d58 Symtab.foldl replaced by Symtab.fold
haftmann
parents: 20485
diff changeset
   251
    Inttab.fold app v empty_vector
2cfe839e8d58 Symtab.foldl replaced by Symtab.fold
haftmann
parents: 20485
diff changeset
   252
  end
16784
92ff7c903585 - added cplex package to HOL/Matrix
obua
parents:
diff changeset
   253
22951
dfafcd6223ad whitespace tuned
haftmann
parents: 22578
diff changeset
   254
fun cut_matrix vfilter vsize m =
21056
2cfe839e8d58 Symtab.foldl replaced by Symtab.fold
haftmann
parents: 20485
diff changeset
   255
  let
22951
dfafcd6223ad whitespace tuned
haftmann
parents: 22578
diff changeset
   256
    fun app (i, v) =
21056
2cfe839e8d58 Symtab.foldl replaced by Symtab.fold
haftmann
parents: 20485
diff changeset
   257
      if is_none (Inttab.lookup vfilter i) then I
2cfe839e8d58 Symtab.foldl replaced by Symtab.fold
haftmann
parents: 20485
diff changeset
   258
      else case vsize
2cfe839e8d58 Symtab.foldl replaced by Symtab.fold
haftmann
parents: 20485
diff changeset
   259
       of NONE => Inttab.update (i, v)
2cfe839e8d58 Symtab.foldl replaced by Symtab.fold
haftmann
parents: 20485
diff changeset
   260
        | SOME s => Inttab.update (i, cut_vector s v)
2cfe839e8d58 Symtab.foldl replaced by Symtab.fold
haftmann
parents: 20485
diff changeset
   261
  in Inttab.fold app m empty_matrix end
2cfe839e8d58 Symtab.foldl replaced by Symtab.fold
haftmann
parents: 20485
diff changeset
   262
17412
e26cb20ef0cc TableFun/Symtab: curried lookup and update;
wenzelm
parents: 17261
diff changeset
   263
fun v_elem_at v i = Inttab.lookup v i
e26cb20ef0cc TableFun/Symtab: curried lookup and update;
wenzelm
parents: 17261
diff changeset
   264
fun m_elem_at m i = Inttab.lookup m i
16784
92ff7c903585 - added cplex package to HOL/Matrix
obua
parents:
diff changeset
   265
22951
dfafcd6223ad whitespace tuned
haftmann
parents: 22578
diff changeset
   266
fun v_only_elem v =
16784
92ff7c903585 - added cplex package to HOL/Matrix
obua
parents:
diff changeset
   267
    case Inttab.min_key v of
22951
dfafcd6223ad whitespace tuned
haftmann
parents: 22578
diff changeset
   268
        NONE => NONE
16784
92ff7c903585 - added cplex package to HOL/Matrix
obua
parents:
diff changeset
   269
      | SOME vmin => (case Inttab.max_key v of
22951
dfafcd6223ad whitespace tuned
haftmann
parents: 22578
diff changeset
   270
                          NONE => SOME vmin
dfafcd6223ad whitespace tuned
haftmann
parents: 22578
diff changeset
   271
                        | SOME vmax => if vmin = vmax then SOME vmin else NONE)
16784
92ff7c903585 - added cplex package to HOL/Matrix
obua
parents:
diff changeset
   272
21056
2cfe839e8d58 Symtab.foldl replaced by Symtab.fold
haftmann
parents: 20485
diff changeset
   273
fun v_fold f = Inttab.fold f;
2cfe839e8d58 Symtab.foldl replaced by Symtab.fold
haftmann
parents: 20485
diff changeset
   274
fun m_fold f = Inttab.fold f;
16784
92ff7c903585 - added cplex package to HOL/Matrix
obua
parents:
diff changeset
   275
23883
7d5aa704454e new functions cut_matrix', etc.
obua
parents: 23665
diff changeset
   276
fun indices_of_vector v = Inttab.keys v
7d5aa704454e new functions cut_matrix', etc.
obua
parents: 23665
diff changeset
   277
fun indices_of_matrix m = Inttab.keys m
7d5aa704454e new functions cut_matrix', etc.
obua
parents: 23665
diff changeset
   278
fun delete_vector indices v = fold Inttab.delete indices v
7d5aa704454e new functions cut_matrix', etc.
obua
parents: 23665
diff changeset
   279
fun delete_matrix indices m = fold Inttab.delete indices m
7d5aa704454e new functions cut_matrix', etc.
obua
parents: 23665
diff changeset
   280
fun cut_matrix' indices m = fold (fn i => fn m => (case Inttab.lookup m i of NONE => m | SOME v => Inttab.update (i, v) m))  indices Inttab.empty
7d5aa704454e new functions cut_matrix', etc.
obua
parents: 23665
diff changeset
   281
fun cut_vector' indices v = fold (fn i => fn v => (case Inttab.lookup v i of NONE => v | SOME x => Inttab.update (i, x) v))  indices Inttab.empty
7d5aa704454e new functions cut_matrix', etc.
obua
parents: 23665
diff changeset
   282
7d5aa704454e new functions cut_matrix', etc.
obua
parents: 23665
diff changeset
   283
7d5aa704454e new functions cut_matrix', etc.
obua
parents: 23665
diff changeset
   284
16784
92ff7c903585 - added cplex package to HOL/Matrix
obua
parents:
diff changeset
   285
end;