src/HOL/Matrix/cplex/FloatSparseMatrixBuilder.ML
author haftmann
Sun, 13 May 2007 18:15:26 +0200
changeset 22951 dfafcd6223ad
parent 22578 b0eb5652f210
child 22964 2284e0d02e7f
permissions -rw-r--r--
whitespace 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
92ff7c903585 - added cplex package to HOL/Matrix
obua
parents:
diff changeset
     6
structure FloatSparseMatrixBuilder :
92ff7c903585 - added cplex package to HOL/Matrix
obua
parents:
diff changeset
     7
sig
92ff7c903585 - added cplex package to HOL/Matrix
obua
parents:
diff changeset
     8
    include MATRIX_BUILDER
92ff7c903585 - added cplex package to HOL/Matrix
obua
parents:
diff changeset
     9
92ff7c903585 - added cplex package to HOL/Matrix
obua
parents:
diff changeset
    10
    structure cplex : CPLEX
92ff7c903585 - added cplex package to HOL/Matrix
obua
parents:
diff changeset
    11
92ff7c903585 - added cplex package to HOL/Matrix
obua
parents:
diff changeset
    12
    type float = IntInf.int*IntInf.int
92ff7c903585 - added cplex package to HOL/Matrix
obua
parents:
diff changeset
    13
    type floatfunc = float -> float
92ff7c903585 - added cplex package to HOL/Matrix
obua
parents:
diff changeset
    14
92ff7c903585 - added cplex package to HOL/Matrix
obua
parents:
diff changeset
    15
92ff7c903585 - added cplex package to HOL/Matrix
obua
parents:
diff changeset
    16
    val float2cterm : IntInf.int * IntInf.int -> cterm
22951
dfafcd6223ad whitespace tuned
haftmann
parents: 22578
diff changeset
    17
16784
92ff7c903585 - added cplex package to HOL/Matrix
obua
parents:
diff changeset
    18
    val approx_value : int -> floatfunc -> string -> cterm * cterm
92ff7c903585 - added cplex package to HOL/Matrix
obua
parents:
diff changeset
    19
    val approx_vector : int -> floatfunc -> vector -> cterm * cterm
92ff7c903585 - added cplex package to HOL/Matrix
obua
parents:
diff changeset
    20
    val approx_matrix : int -> floatfunc -> matrix -> cterm * cterm
92ff7c903585 - added cplex package to HOL/Matrix
obua
parents:
diff changeset
    21
92ff7c903585 - added cplex package to HOL/Matrix
obua
parents:
diff changeset
    22
    val mk_spvec_entry : int -> float -> term
92ff7c903585 - added cplex package to HOL/Matrix
obua
parents:
diff changeset
    23
    val empty_spvec : term
92ff7c903585 - added cplex package to HOL/Matrix
obua
parents:
diff changeset
    24
    val cons_spvec : term -> term -> term
92ff7c903585 - added cplex package to HOL/Matrix
obua
parents:
diff changeset
    25
    val empty_spmat : term
92ff7c903585 - added cplex package to HOL/Matrix
obua
parents:
diff changeset
    26
    val mk_spmat_entry : int -> term -> term
92ff7c903585 - added cplex package to HOL/Matrix
obua
parents:
diff changeset
    27
    val cons_spmat : term -> term -> term
92ff7c903585 - added cplex package to HOL/Matrix
obua
parents:
diff changeset
    28
    val sign_term : term -> cterm
92ff7c903585 - added cplex package to HOL/Matrix
obua
parents:
diff changeset
    29
92ff7c903585 - added cplex package to HOL/Matrix
obua
parents:
diff changeset
    30
    val v_elem_at : vector -> int -> string option
92ff7c903585 - added cplex package to HOL/Matrix
obua
parents:
diff changeset
    31
    val m_elem_at : matrix -> int -> vector option
92ff7c903585 - added cplex package to HOL/Matrix
obua
parents:
diff changeset
    32
    val v_only_elem : vector -> int option
21056
2cfe839e8d58 Symtab.foldl replaced by Symtab.fold
haftmann
parents: 20485
diff changeset
    33
    val v_fold : (int * string -> 'a -> 'a) -> vector -> 'a -> 'a
2cfe839e8d58 Symtab.foldl replaced by Symtab.fold
haftmann
parents: 20485
diff changeset
    34
    val m_fold : (int * vector -> 'a -> 'a) -> matrix -> 'a -> 'a
20485
3078fd2eec7b got rid of Numeral.bin type
haftmann
parents: 17412
diff changeset
    35
16784
92ff7c903585 - added cplex package to HOL/Matrix
obua
parents:
diff changeset
    36
    val transpose_matrix : matrix -> matrix
92ff7c903585 - added cplex package to HOL/Matrix
obua
parents:
diff changeset
    37
92ff7c903585 - added cplex package to HOL/Matrix
obua
parents:
diff changeset
    38
    val cut_vector : int -> vector -> vector
92ff7c903585 - added cplex package to HOL/Matrix
obua
parents:
diff changeset
    39
    val cut_matrix : vector -> (int option) -> matrix -> matrix
22951
dfafcd6223ad whitespace tuned
haftmann
parents: 22578
diff changeset
    40
16784
92ff7c903585 - added cplex package to HOL/Matrix
obua
parents:
diff changeset
    41
    (* cplexProg c A b *)
92ff7c903585 - added cplex package to HOL/Matrix
obua
parents:
diff changeset
    42
    val cplexProg : vector -> matrix -> vector -> (cplex.cplexProg * (string -> int))
92ff7c903585 - added cplex package to HOL/Matrix
obua
parents:
diff changeset
    43
    (* dual_cplexProg c A b *)
92ff7c903585 - added cplex package to HOL/Matrix
obua
parents:
diff changeset
    44
    val dual_cplexProg : vector -> matrix -> vector -> (cplex.cplexProg * (string -> int))
92ff7c903585 - added cplex package to HOL/Matrix
obua
parents:
diff changeset
    45
92ff7c903585 - added cplex package to HOL/Matrix
obua
parents:
diff changeset
    46
    val real_spmatT : typ
92ff7c903585 - added cplex package to HOL/Matrix
obua
parents:
diff changeset
    47
    val real_spvecT : typ
22951
dfafcd6223ad whitespace tuned
haftmann
parents: 22578
diff changeset
    48
end
dfafcd6223ad whitespace tuned
haftmann
parents: 22578
diff changeset
    49
=
16784
92ff7c903585 - added cplex package to HOL/Matrix
obua
parents:
diff changeset
    50
struct
92ff7c903585 - added cplex package to HOL/Matrix
obua
parents:
diff changeset
    51
92ff7c903585 - added cplex package to HOL/Matrix
obua
parents:
diff changeset
    52
92ff7c903585 - added cplex package to HOL/Matrix
obua
parents:
diff changeset
    53
structure Inttab = TableFun(type key = int val ord = (rev_order o int_ord));
92ff7c903585 - added cplex package to HOL/Matrix
obua
parents:
diff changeset
    54
92ff7c903585 - added cplex package to HOL/Matrix
obua
parents:
diff changeset
    55
type vector = string Inttab.table
92ff7c903585 - added cplex package to HOL/Matrix
obua
parents:
diff changeset
    56
type matrix = vector Inttab.table
92ff7c903585 - added cplex package to HOL/Matrix
obua
parents:
diff changeset
    57
type float = IntInf.int*IntInf.int
92ff7c903585 - added cplex package to HOL/Matrix
obua
parents:
diff changeset
    58
type floatfunc = float -> float
92ff7c903585 - added cplex package to HOL/Matrix
obua
parents:
diff changeset
    59
92ff7c903585 - added cplex package to HOL/Matrix
obua
parents:
diff changeset
    60
val th = theory "FloatSparseMatrix"
22951
dfafcd6223ad whitespace tuned
haftmann
parents: 22578
diff changeset
    61
22578
b0eb5652f210 removed obsolete sign_of/sign_of_thm;
wenzelm
parents: 21056
diff changeset
    62
fun readtype s = Sign.intern_type th s
b0eb5652f210 removed obsolete sign_of/sign_of_thm;
wenzelm
parents: 21056
diff changeset
    63
fun readterm s = Sign.intern_const th s
22951
dfafcd6223ad whitespace tuned
haftmann
parents: 22578
diff changeset
    64
16784
92ff7c903585 - added cplex package to HOL/Matrix
obua
parents:
diff changeset
    65
val ty_list = readtype "list"
92ff7c903585 - added cplex package to HOL/Matrix
obua
parents:
diff changeset
    66
val term_Nil = readterm "Nil"
92ff7c903585 - added cplex package to HOL/Matrix
obua
parents:
diff changeset
    67
val term_Cons = readterm "Cons"
22951
dfafcd6223ad whitespace tuned
haftmann
parents: 22578
diff changeset
    68
16784
92ff7c903585 - added cplex package to HOL/Matrix
obua
parents:
diff changeset
    69
val spvec_elemT = HOLogic.mk_prodT (HOLogic.natT, HOLogic.realT)
92ff7c903585 - added cplex package to HOL/Matrix
obua
parents:
diff changeset
    70
val spvecT = Type (ty_list, [spvec_elemT])
92ff7c903585 - added cplex package to HOL/Matrix
obua
parents:
diff changeset
    71
val spmat_elemT = HOLogic.mk_prodT (HOLogic.natT, spvecT)
92ff7c903585 - added cplex package to HOL/Matrix
obua
parents:
diff changeset
    72
val spmatT = Type (ty_list, [spmat_elemT])
92ff7c903585 - added cplex package to HOL/Matrix
obua
parents:
diff changeset
    73
92ff7c903585 - added cplex package to HOL/Matrix
obua
parents:
diff changeset
    74
val real_spmatT = spmatT
92ff7c903585 - added cplex package to HOL/Matrix
obua
parents:
diff changeset
    75
val real_spvecT = spvecT
92ff7c903585 - added cplex package to HOL/Matrix
obua
parents:
diff changeset
    76
92ff7c903585 - added cplex package to HOL/Matrix
obua
parents:
diff changeset
    77
val empty_matrix_const = Const (term_Nil, spmatT)
92ff7c903585 - added cplex package to HOL/Matrix
obua
parents:
diff changeset
    78
val empty_vector_const = Const (term_Nil, spvecT)
92ff7c903585 - added cplex package to HOL/Matrix
obua
parents:
diff changeset
    79
92ff7c903585 - added cplex package to HOL/Matrix
obua
parents:
diff changeset
    80
val Cons_spvec_const = Const (term_Cons, spvec_elemT --> spvecT --> spvecT)
22951
dfafcd6223ad whitespace tuned
haftmann
parents: 22578
diff changeset
    81
val Cons_spmat_const = Const (term_Cons, spmat_elemT --> spmatT --> spmatT)
20485
3078fd2eec7b got rid of Numeral.bin type
haftmann
parents: 17412
diff changeset
    82
16873
9ed940a1bebb proving bounds for real linear programs
obua
parents: 16784
diff changeset
    83
val float_const = Float.float_const
9ed940a1bebb proving bounds for real linear programs
obua
parents: 16784
diff changeset
    84
16784
92ff7c903585 - added cplex package to HOL/Matrix
obua
parents:
diff changeset
    85
val zero = IntInf.fromInt 0
92ff7c903585 - added cplex package to HOL/Matrix
obua
parents:
diff changeset
    86
val minus_one = IntInf.fromInt ~1
92ff7c903585 - added cplex package to HOL/Matrix
obua
parents:
diff changeset
    87
val two = IntInf.fromInt 2
20485
3078fd2eec7b got rid of Numeral.bin type
haftmann
parents: 17412
diff changeset
    88
16873
9ed940a1bebb proving bounds for real linear programs
obua
parents: 16784
diff changeset
    89
val mk_intinf = Float.mk_intinf
16784
92ff7c903585 - added cplex package to HOL/Matrix
obua
parents:
diff changeset
    90
22951
dfafcd6223ad whitespace tuned
haftmann
parents: 22578
diff changeset
    91
val mk_float  = Float.mk_float
16784
92ff7c903585 - added cplex package to HOL/Matrix
obua
parents:
diff changeset
    92
22578
b0eb5652f210 removed obsolete sign_of/sign_of_thm;
wenzelm
parents: 21056
diff changeset
    93
fun float2cterm (a,b) = cterm_of th (mk_float (a,b))
16784
92ff7c903585 - added cplex package to HOL/Matrix
obua
parents:
diff changeset
    94
16873
9ed940a1bebb proving bounds for real linear programs
obua
parents: 16784
diff changeset
    95
fun approx_value_term prec f = Float.approx_float prec (fn (x, y) => (f x, f y))
16784
92ff7c903585 - added cplex package to HOL/Matrix
obua
parents:
diff changeset
    96
22951
dfafcd6223ad whitespace tuned
haftmann
parents: 22578
diff changeset
    97
fun approx_value prec pprt value =
20485
3078fd2eec7b got rid of Numeral.bin type
haftmann
parents: 17412
diff changeset
    98
  let
3078fd2eec7b got rid of Numeral.bin type
haftmann
parents: 17412
diff changeset
    99
    val (flower, fupper) = approx_value_term prec pprt value
3078fd2eec7b got rid of Numeral.bin type
haftmann
parents: 17412
diff changeset
   100
  in
22578
b0eb5652f210 removed obsolete sign_of/sign_of_thm;
wenzelm
parents: 21056
diff changeset
   101
    (cterm_of th flower, cterm_of th fupper)
20485
3078fd2eec7b got rid of Numeral.bin type
haftmann
parents: 17412
diff changeset
   102
  end
16784
92ff7c903585 - added cplex package to HOL/Matrix
obua
parents:
diff changeset
   103
22578
b0eb5652f210 removed obsolete sign_of/sign_of_thm;
wenzelm
parents: 21056
diff changeset
   104
fun sign_term t = cterm_of th t
16784
92ff7c903585 - added cplex package to HOL/Matrix
obua
parents:
diff changeset
   105
92ff7c903585 - added cplex package to HOL/Matrix
obua
parents:
diff changeset
   106
val empty_spvec = empty_vector_const
92ff7c903585 - added cplex package to HOL/Matrix
obua
parents:
diff changeset
   107
92ff7c903585 - added cplex package to HOL/Matrix
obua
parents:
diff changeset
   108
val empty_spmat = empty_matrix_const
92ff7c903585 - added cplex package to HOL/Matrix
obua
parents:
diff changeset
   109
22951
dfafcd6223ad whitespace tuned
haftmann
parents: 22578
diff changeset
   110
fun mk_spvec_entry i f =
16784
92ff7c903585 - added cplex package to HOL/Matrix
obua
parents:
diff changeset
   111
    let
22951
dfafcd6223ad whitespace tuned
haftmann
parents: 22578
diff changeset
   112
        val term_i = mk_intinf HOLogic.natT (IntInf.fromInt i)
dfafcd6223ad whitespace tuned
haftmann
parents: 22578
diff changeset
   113
        val term_f = mk_float f
dfafcd6223ad whitespace tuned
haftmann
parents: 22578
diff changeset
   114
    in
dfafcd6223ad whitespace tuned
haftmann
parents: 22578
diff changeset
   115
        HOLogic.mk_prod (term_i, term_f)
16784
92ff7c903585 - added cplex package to HOL/Matrix
obua
parents:
diff changeset
   116
    end
92ff7c903585 - added cplex package to HOL/Matrix
obua
parents:
diff changeset
   117
22951
dfafcd6223ad whitespace tuned
haftmann
parents: 22578
diff changeset
   118
fun mk_spmat_entry i e =
16784
92ff7c903585 - added cplex package to HOL/Matrix
obua
parents:
diff changeset
   119
    let
22951
dfafcd6223ad whitespace tuned
haftmann
parents: 22578
diff changeset
   120
        val term_i = mk_intinf HOLogic.natT (IntInf.fromInt i)
16784
92ff7c903585 - added cplex package to HOL/Matrix
obua
parents:
diff changeset
   121
    in
22951
dfafcd6223ad whitespace tuned
haftmann
parents: 22578
diff changeset
   122
        HOLogic.mk_prod (term_i, e)
16784
92ff7c903585 - added cplex package to HOL/Matrix
obua
parents:
diff changeset
   123
    end
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 cons_spvec h t = Cons_spvec_const $ h $ t
92ff7c903585 - added cplex package to HOL/Matrix
obua
parents:
diff changeset
   126
22951
dfafcd6223ad whitespace tuned
haftmann
parents: 22578
diff changeset
   127
fun cons_spmat h t = Cons_spmat_const $ h $ t
16784
92ff7c903585 - added cplex package to HOL/Matrix
obua
parents:
diff changeset
   128
22951
dfafcd6223ad whitespace tuned
haftmann
parents: 22578
diff changeset
   129
fun approx_vector_term prec pprt vector =
dfafcd6223ad whitespace tuned
haftmann
parents: 22578
diff changeset
   130
    let
dfafcd6223ad whitespace tuned
haftmann
parents: 22578
diff changeset
   131
        fun app (index, s) (vlower, vupper) =
dfafcd6223ad whitespace tuned
haftmann
parents: 22578
diff changeset
   132
            let
dfafcd6223ad whitespace tuned
haftmann
parents: 22578
diff changeset
   133
                val (flower, fupper) = approx_value_term prec pprt s
dfafcd6223ad whitespace tuned
haftmann
parents: 22578
diff changeset
   134
                val index = mk_intinf HOLogic.natT (IntInf.fromInt index)
dfafcd6223ad whitespace tuned
haftmann
parents: 22578
diff changeset
   135
                val elower = HOLogic.mk_prod (index, flower)
dfafcd6223ad whitespace tuned
haftmann
parents: 22578
diff changeset
   136
                val eupper = HOLogic.mk_prod (index, fupper)
dfafcd6223ad whitespace tuned
haftmann
parents: 22578
diff changeset
   137
            in
dfafcd6223ad whitespace tuned
haftmann
parents: 22578
diff changeset
   138
                (Cons_spvec_const $ elower $ vlower,
dfafcd6223ad whitespace tuned
haftmann
parents: 22578
diff changeset
   139
                 Cons_spvec_const $ eupper $ vupper)
dfafcd6223ad whitespace tuned
haftmann
parents: 22578
diff changeset
   140
            end
16784
92ff7c903585 - added cplex package to HOL/Matrix
obua
parents:
diff changeset
   141
    in
22951
dfafcd6223ad whitespace tuned
haftmann
parents: 22578
diff changeset
   142
        Inttab.fold app vector (empty_vector_const, empty_vector_const)
16784
92ff7c903585 - added cplex package to HOL/Matrix
obua
parents:
diff changeset
   143
    end
92ff7c903585 - added cplex package to HOL/Matrix
obua
parents:
diff changeset
   144
92ff7c903585 - added cplex package to HOL/Matrix
obua
parents:
diff changeset
   145
fun approx_matrix_term prec pprt matrix =
21056
2cfe839e8d58 Symtab.foldl replaced by Symtab.fold
haftmann
parents: 20485
diff changeset
   146
  let
2cfe839e8d58 Symtab.foldl replaced by Symtab.fold
haftmann
parents: 20485
diff changeset
   147
    fun app (index, vector) (mlower, mupper) =
2cfe839e8d58 Symtab.foldl replaced by Symtab.fold
haftmann
parents: 20485
diff changeset
   148
      let
22951
dfafcd6223ad whitespace tuned
haftmann
parents: 22578
diff changeset
   149
        val (vlower, vupper) = approx_vector_term prec pprt vector
21056
2cfe839e8d58 Symtab.foldl replaced by Symtab.fold
haftmann
parents: 20485
diff changeset
   150
        val index = mk_intinf HOLogic.natT (IntInf.fromInt index)
2cfe839e8d58 Symtab.foldl replaced by Symtab.fold
haftmann
parents: 20485
diff changeset
   151
        val elower = HOLogic.mk_prod (index, vlower)
2cfe839e8d58 Symtab.foldl replaced by Symtab.fold
haftmann
parents: 20485
diff changeset
   152
        val eupper = HOLogic.mk_prod (index, vupper)
2cfe839e8d58 Symtab.foldl replaced by Symtab.fold
haftmann
parents: 20485
diff changeset
   153
      in
2cfe839e8d58 Symtab.foldl replaced by Symtab.fold
haftmann
parents: 20485
diff changeset
   154
        (Cons_spmat_const $ elower $ mlower, Cons_spmat_const $ eupper $ mupper)
2cfe839e8d58 Symtab.foldl replaced by Symtab.fold
haftmann
parents: 20485
diff changeset
   155
      end
2cfe839e8d58 Symtab.foldl replaced by Symtab.fold
haftmann
parents: 20485
diff changeset
   156
    val (mlower, mupper) = Inttab.fold app matrix (empty_matrix_const, empty_matrix_const)
2cfe839e8d58 Symtab.foldl replaced by Symtab.fold
haftmann
parents: 20485
diff changeset
   157
  in Inttab.fold app matrix (empty_matrix_const, empty_matrix_const) end;
16784
92ff7c903585 - added cplex package to HOL/Matrix
obua
parents:
diff changeset
   158
92ff7c903585 - added cplex package to HOL/Matrix
obua
parents:
diff changeset
   159
fun approx_vector prec pprt vector =
92ff7c903585 - added cplex package to HOL/Matrix
obua
parents:
diff changeset
   160
    let
22951
dfafcd6223ad whitespace tuned
haftmann
parents: 22578
diff changeset
   161
        val (l, u) = approx_vector_term prec pprt vector
16784
92ff7c903585 - added cplex package to HOL/Matrix
obua
parents:
diff changeset
   162
    in
22951
dfafcd6223ad whitespace tuned
haftmann
parents: 22578
diff changeset
   163
        (cterm_of th l, cterm_of th u)
16784
92ff7c903585 - added cplex package to HOL/Matrix
obua
parents:
diff changeset
   164
    end
92ff7c903585 - added cplex package to HOL/Matrix
obua
parents:
diff changeset
   165
22951
dfafcd6223ad whitespace tuned
haftmann
parents: 22578
diff changeset
   166
fun approx_matrix prec pprt matrix =
16784
92ff7c903585 - added cplex package to HOL/Matrix
obua
parents:
diff changeset
   167
    let
22951
dfafcd6223ad whitespace tuned
haftmann
parents: 22578
diff changeset
   168
        val (l, u) = approx_matrix_term prec pprt matrix
16784
92ff7c903585 - added cplex package to HOL/Matrix
obua
parents:
diff changeset
   169
    in
22951
dfafcd6223ad whitespace tuned
haftmann
parents: 22578
diff changeset
   170
        (cterm_of th l, cterm_of th u)
16784
92ff7c903585 - added cplex package to HOL/Matrix
obua
parents:
diff changeset
   171
    end
92ff7c903585 - added cplex package to HOL/Matrix
obua
parents:
diff changeset
   172
92ff7c903585 - added cplex package to HOL/Matrix
obua
parents:
diff changeset
   173
92ff7c903585 - added cplex package to HOL/Matrix
obua
parents:
diff changeset
   174
exception Nat_expected of int;
92ff7c903585 - added cplex package to HOL/Matrix
obua
parents:
diff changeset
   175
92ff7c903585 - added cplex package to HOL/Matrix
obua
parents:
diff changeset
   176
val zero_interval = approx_value_term 1 I "0"
92ff7c903585 - added cplex package to HOL/Matrix
obua
parents:
diff changeset
   177
22951
dfafcd6223ad whitespace tuned
haftmann
parents: 22578
diff changeset
   178
fun set_elem vector index str =
dfafcd6223ad whitespace tuned
haftmann
parents: 22578
diff changeset
   179
    if index < 0 then
dfafcd6223ad whitespace tuned
haftmann
parents: 22578
diff changeset
   180
        raise (Nat_expected index)
dfafcd6223ad whitespace tuned
haftmann
parents: 22578
diff changeset
   181
    else if (approx_value_term 1 I str) = zero_interval then
dfafcd6223ad whitespace tuned
haftmann
parents: 22578
diff changeset
   182
        vector
dfafcd6223ad whitespace tuned
haftmann
parents: 22578
diff changeset
   183
    else
dfafcd6223ad whitespace tuned
haftmann
parents: 22578
diff changeset
   184
        Inttab.update (index, str) vector
16784
92ff7c903585 - added cplex package to HOL/Matrix
obua
parents:
diff changeset
   185
22951
dfafcd6223ad whitespace tuned
haftmann
parents: 22578
diff changeset
   186
fun set_vector matrix index vector =
16784
92ff7c903585 - added cplex package to HOL/Matrix
obua
parents:
diff changeset
   187
    if index < 0 then
22951
dfafcd6223ad whitespace tuned
haftmann
parents: 22578
diff changeset
   188
        raise (Nat_expected index)
16784
92ff7c903585 - added cplex package to HOL/Matrix
obua
parents:
diff changeset
   189
    else if Inttab.is_empty vector then
22951
dfafcd6223ad whitespace tuned
haftmann
parents: 22578
diff changeset
   190
        matrix
16784
92ff7c903585 - added cplex package to HOL/Matrix
obua
parents:
diff changeset
   191
    else
22951
dfafcd6223ad whitespace tuned
haftmann
parents: 22578
diff changeset
   192
        Inttab.update (index, vector) matrix
16784
92ff7c903585 - added cplex package to HOL/Matrix
obua
parents:
diff changeset
   193
92ff7c903585 - added cplex package to HOL/Matrix
obua
parents:
diff changeset
   194
val empty_matrix = Inttab.empty
92ff7c903585 - added cplex package to HOL/Matrix
obua
parents:
diff changeset
   195
val empty_vector = Inttab.empty
92ff7c903585 - added cplex package to HOL/Matrix
obua
parents:
diff changeset
   196
92ff7c903585 - added cplex package to HOL/Matrix
obua
parents:
diff changeset
   197
(* dual stuff *)
92ff7c903585 - added cplex package to HOL/Matrix
obua
parents:
diff changeset
   198
92ff7c903585 - added cplex package to HOL/Matrix
obua
parents:
diff changeset
   199
structure cplex = Cplex
92ff7c903585 - added cplex package to HOL/Matrix
obua
parents:
diff changeset
   200
22951
dfafcd6223ad whitespace tuned
haftmann
parents: 22578
diff changeset
   201
fun transpose_matrix matrix =
21056
2cfe839e8d58 Symtab.foldl replaced by Symtab.fold
haftmann
parents: 20485
diff changeset
   202
  let
2cfe839e8d58 Symtab.foldl replaced by Symtab.fold
haftmann
parents: 20485
diff changeset
   203
    fun upd j (i, s) =
2cfe839e8d58 Symtab.foldl replaced by Symtab.fold
haftmann
parents: 20485
diff changeset
   204
      Inttab.map_default (i, Inttab.empty) (Inttab.update (j, s));
2cfe839e8d58 Symtab.foldl replaced by Symtab.fold
haftmann
parents: 20485
diff changeset
   205
    fun updm (j, v) = Inttab.fold (upd j) v;
2cfe839e8d58 Symtab.foldl replaced by Symtab.fold
haftmann
parents: 20485
diff changeset
   206
  in Inttab.fold updm matrix empty_matrix end;
16784
92ff7c903585 - added cplex package to HOL/Matrix
obua
parents:
diff changeset
   207
92ff7c903585 - added cplex package to HOL/Matrix
obua
parents:
diff changeset
   208
exception No_name of string;
92ff7c903585 - added cplex package to HOL/Matrix
obua
parents:
diff changeset
   209
92ff7c903585 - added cplex package to HOL/Matrix
obua
parents:
diff changeset
   210
exception Superfluous_constr_right_hand_sides
92ff7c903585 - added cplex package to HOL/Matrix
obua
parents:
diff changeset
   211
22951
dfafcd6223ad whitespace tuned
haftmann
parents: 22578
diff changeset
   212
fun cplexProg c A b =
16784
92ff7c903585 - added cplex package to HOL/Matrix
obua
parents:
diff changeset
   213
    let
22951
dfafcd6223ad whitespace tuned
haftmann
parents: 22578
diff changeset
   214
        val ytable = ref Inttab.empty
dfafcd6223ad whitespace tuned
haftmann
parents: 22578
diff changeset
   215
        fun indexof s =
dfafcd6223ad whitespace tuned
haftmann
parents: 22578
diff changeset
   216
            if String.size s = 0 then raise (No_name s)
dfafcd6223ad whitespace tuned
haftmann
parents: 22578
diff changeset
   217
            else case Int.fromString (String.extract(s, 1, NONE)) of
dfafcd6223ad whitespace tuned
haftmann
parents: 22578
diff changeset
   218
                     SOME i => i | NONE => raise (No_name s)
16784
92ff7c903585 - added cplex package to HOL/Matrix
obua
parents:
diff changeset
   219
22951
dfafcd6223ad whitespace tuned
haftmann
parents: 22578
diff changeset
   220
        fun nameof i =
dfafcd6223ad whitespace tuned
haftmann
parents: 22578
diff changeset
   221
            let
dfafcd6223ad whitespace tuned
haftmann
parents: 22578
diff changeset
   222
                val s = "x"^(Int.toString i)
dfafcd6223ad whitespace tuned
haftmann
parents: 22578
diff changeset
   223
                val _ = change ytable (Inttab.update (i, s))
dfafcd6223ad whitespace tuned
haftmann
parents: 22578
diff changeset
   224
            in
dfafcd6223ad whitespace tuned
haftmann
parents: 22578
diff changeset
   225
                s
dfafcd6223ad whitespace tuned
haftmann
parents: 22578
diff changeset
   226
            end
dfafcd6223ad whitespace tuned
haftmann
parents: 22578
diff changeset
   227
dfafcd6223ad whitespace tuned
haftmann
parents: 22578
diff changeset
   228
        fun split_numstr s =
dfafcd6223ad whitespace tuned
haftmann
parents: 22578
diff changeset
   229
            if String.isPrefix "-" s then (false,String.extract(s, 1, NONE))
dfafcd6223ad whitespace tuned
haftmann
parents: 22578
diff changeset
   230
            else if String.isPrefix "+" s then (true, String.extract(s, 1, NONE))
dfafcd6223ad whitespace tuned
haftmann
parents: 22578
diff changeset
   231
            else (true, s)
dfafcd6223ad whitespace tuned
haftmann
parents: 22578
diff changeset
   232
dfafcd6223ad whitespace tuned
haftmann
parents: 22578
diff changeset
   233
        fun mk_term index s =
dfafcd6223ad whitespace tuned
haftmann
parents: 22578
diff changeset
   234
            let
dfafcd6223ad whitespace tuned
haftmann
parents: 22578
diff changeset
   235
                val (p, s) = split_numstr s
dfafcd6223ad whitespace tuned
haftmann
parents: 22578
diff changeset
   236
                val prod = cplex.cplexProd (cplex.cplexNum s, cplex.cplexVar (nameof index))
dfafcd6223ad whitespace tuned
haftmann
parents: 22578
diff changeset
   237
            in
dfafcd6223ad whitespace tuned
haftmann
parents: 22578
diff changeset
   238
                if p then prod else cplex.cplexNeg prod
dfafcd6223ad whitespace tuned
haftmann
parents: 22578
diff changeset
   239
            end
16784
92ff7c903585 - added cplex package to HOL/Matrix
obua
parents:
diff changeset
   240
22951
dfafcd6223ad whitespace tuned
haftmann
parents: 22578
diff changeset
   241
        fun vec2sum vector =
dfafcd6223ad whitespace tuned
haftmann
parents: 22578
diff changeset
   242
            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
   243
22951
dfafcd6223ad whitespace tuned
haftmann
parents: 22578
diff changeset
   244
        fun mk_constr index vector c =
dfafcd6223ad whitespace tuned
haftmann
parents: 22578
diff changeset
   245
            let
dfafcd6223ad whitespace tuned
haftmann
parents: 22578
diff changeset
   246
                val s = case Inttab.lookup c index of SOME s => s | NONE => "0"
dfafcd6223ad whitespace tuned
haftmann
parents: 22578
diff changeset
   247
                val (p, s) = split_numstr s
dfafcd6223ad whitespace tuned
haftmann
parents: 22578
diff changeset
   248
                val num = if p then cplex.cplexNum s else cplex.cplexNeg (cplex.cplexNum s)
dfafcd6223ad whitespace tuned
haftmann
parents: 22578
diff changeset
   249
            in
dfafcd6223ad whitespace tuned
haftmann
parents: 22578
diff changeset
   250
                (NONE, cplex.cplexConstr (cplex.cplexLeq, (vec2sum vector, num)))
dfafcd6223ad whitespace tuned
haftmann
parents: 22578
diff changeset
   251
            end
dfafcd6223ad whitespace tuned
haftmann
parents: 22578
diff changeset
   252
dfafcd6223ad whitespace tuned
haftmann
parents: 22578
diff changeset
   253
        fun delete index c = Inttab.delete index c handle Inttab.UNDEF _ => c
16784
92ff7c903585 - added cplex package to HOL/Matrix
obua
parents:
diff changeset
   254
22951
dfafcd6223ad whitespace tuned
haftmann
parents: 22578
diff changeset
   255
        val (list, b) = Inttab.fold
dfafcd6223ad whitespace tuned
haftmann
parents: 22578
diff changeset
   256
                            (fn (index, v) => fn (list, c) => ((mk_constr index v c)::list, delete index c))
dfafcd6223ad whitespace tuned
haftmann
parents: 22578
diff changeset
   257
                            A ([], b)
dfafcd6223ad whitespace tuned
haftmann
parents: 22578
diff changeset
   258
        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
   259
22951
dfafcd6223ad whitespace tuned
haftmann
parents: 22578
diff changeset
   260
        fun mk_free y = cplex.cplexBounds (cplex.cplexNeg cplex.cplexInf, cplex.cplexLeq,
dfafcd6223ad whitespace tuned
haftmann
parents: 22578
diff changeset
   261
                                           cplex.cplexVar y, cplex.cplexLeq,
dfafcd6223ad whitespace tuned
haftmann
parents: 22578
diff changeset
   262
                                           cplex.cplexInf)
16784
92ff7c903585 - added cplex package to HOL/Matrix
obua
parents:
diff changeset
   263
22951
dfafcd6223ad whitespace tuned
haftmann
parents: 22578
diff changeset
   264
        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
   265
22951
dfafcd6223ad whitespace tuned
haftmann
parents: 22578
diff changeset
   266
        val prog = cplex.cplexProg ("original", cplex.cplexMaximize (vec2sum c), list, yvars)
16784
92ff7c903585 - added cplex package to HOL/Matrix
obua
parents:
diff changeset
   267
    in
22951
dfafcd6223ad whitespace tuned
haftmann
parents: 22578
diff changeset
   268
        (prog, indexof)
16784
92ff7c903585 - added cplex package to HOL/Matrix
obua
parents:
diff changeset
   269
    end
92ff7c903585 - added cplex package to HOL/Matrix
obua
parents:
diff changeset
   270
92ff7c903585 - added cplex package to HOL/Matrix
obua
parents:
diff changeset
   271
22951
dfafcd6223ad whitespace tuned
haftmann
parents: 22578
diff changeset
   272
fun dual_cplexProg c A b =
16784
92ff7c903585 - added cplex package to HOL/Matrix
obua
parents:
diff changeset
   273
    let
22951
dfafcd6223ad whitespace tuned
haftmann
parents: 22578
diff changeset
   274
        fun indexof s =
dfafcd6223ad whitespace tuned
haftmann
parents: 22578
diff changeset
   275
            if String.size s = 0 then raise (No_name s)
dfafcd6223ad whitespace tuned
haftmann
parents: 22578
diff changeset
   276
            else case Int.fromString (String.extract(s, 1, NONE)) of
dfafcd6223ad whitespace tuned
haftmann
parents: 22578
diff changeset
   277
                     SOME i => i | NONE => raise (No_name s)
dfafcd6223ad whitespace tuned
haftmann
parents: 22578
diff changeset
   278
dfafcd6223ad whitespace tuned
haftmann
parents: 22578
diff changeset
   279
        fun nameof i = "y"^(Int.toString i)
16784
92ff7c903585 - added cplex package to HOL/Matrix
obua
parents:
diff changeset
   280
22951
dfafcd6223ad whitespace tuned
haftmann
parents: 22578
diff changeset
   281
        fun split_numstr s =
dfafcd6223ad whitespace tuned
haftmann
parents: 22578
diff changeset
   282
            if String.isPrefix "-" s then (false,String.extract(s, 1, NONE))
dfafcd6223ad whitespace tuned
haftmann
parents: 22578
diff changeset
   283
            else if String.isPrefix "+" s then (true, String.extract(s, 1, NONE))
dfafcd6223ad whitespace tuned
haftmann
parents: 22578
diff changeset
   284
            else (true, s)
dfafcd6223ad whitespace tuned
haftmann
parents: 22578
diff changeset
   285
dfafcd6223ad whitespace tuned
haftmann
parents: 22578
diff changeset
   286
        fun mk_term index s =
dfafcd6223ad whitespace tuned
haftmann
parents: 22578
diff changeset
   287
            let
dfafcd6223ad whitespace tuned
haftmann
parents: 22578
diff changeset
   288
                val (p, s) = split_numstr s
dfafcd6223ad whitespace tuned
haftmann
parents: 22578
diff changeset
   289
                val prod = cplex.cplexProd (cplex.cplexNum s, cplex.cplexVar (nameof index))
dfafcd6223ad whitespace tuned
haftmann
parents: 22578
diff changeset
   290
            in
dfafcd6223ad whitespace tuned
haftmann
parents: 22578
diff changeset
   291
                if p then prod else cplex.cplexNeg prod
dfafcd6223ad whitespace tuned
haftmann
parents: 22578
diff changeset
   292
            end
16784
92ff7c903585 - added cplex package to HOL/Matrix
obua
parents:
diff changeset
   293
22951
dfafcd6223ad whitespace tuned
haftmann
parents: 22578
diff changeset
   294
        fun vec2sum vector =
dfafcd6223ad whitespace tuned
haftmann
parents: 22578
diff changeset
   295
            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
   296
22951
dfafcd6223ad whitespace tuned
haftmann
parents: 22578
diff changeset
   297
        fun mk_constr index vector c =
dfafcd6223ad whitespace tuned
haftmann
parents: 22578
diff changeset
   298
            let
dfafcd6223ad whitespace tuned
haftmann
parents: 22578
diff changeset
   299
                val s = case Inttab.lookup c index of SOME s => s | NONE => "0"
dfafcd6223ad whitespace tuned
haftmann
parents: 22578
diff changeset
   300
                val (p, s) = split_numstr s
dfafcd6223ad whitespace tuned
haftmann
parents: 22578
diff changeset
   301
                val num = if p then cplex.cplexNum s else cplex.cplexNeg (cplex.cplexNum s)
dfafcd6223ad whitespace tuned
haftmann
parents: 22578
diff changeset
   302
            in
dfafcd6223ad whitespace tuned
haftmann
parents: 22578
diff changeset
   303
                (NONE, cplex.cplexConstr (cplex.cplexEq, (vec2sum vector, num)))
dfafcd6223ad whitespace tuned
haftmann
parents: 22578
diff changeset
   304
            end
16784
92ff7c903585 - added cplex package to HOL/Matrix
obua
parents:
diff changeset
   305
22951
dfafcd6223ad whitespace tuned
haftmann
parents: 22578
diff changeset
   306
        fun delete index c = Inttab.delete index c handle Inttab.UNDEF _ => c
16784
92ff7c903585 - added cplex package to HOL/Matrix
obua
parents:
diff changeset
   307
22951
dfafcd6223ad whitespace tuned
haftmann
parents: 22578
diff changeset
   308
        val (list, c) = Inttab.fold
dfafcd6223ad whitespace tuned
haftmann
parents: 22578
diff changeset
   309
                            (fn (index, v) => fn (list, c) => ((mk_constr index v c)::list, delete index c))
dfafcd6223ad whitespace tuned
haftmann
parents: 22578
diff changeset
   310
                            (transpose_matrix A) ([], c)
dfafcd6223ad whitespace tuned
haftmann
parents: 22578
diff changeset
   311
        val _ = if Inttab.is_empty c then () else raise Superfluous_constr_right_hand_sides
dfafcd6223ad whitespace tuned
haftmann
parents: 22578
diff changeset
   312
dfafcd6223ad whitespace tuned
haftmann
parents: 22578
diff changeset
   313
        val prog = cplex.cplexProg ("dual", cplex.cplexMinimize (vec2sum b), list, [])
16784
92ff7c903585 - added cplex package to HOL/Matrix
obua
parents:
diff changeset
   314
    in
22951
dfafcd6223ad whitespace tuned
haftmann
parents: 22578
diff changeset
   315
        (prog, indexof)
16784
92ff7c903585 - added cplex package to HOL/Matrix
obua
parents:
diff changeset
   316
    end
92ff7c903585 - added cplex package to HOL/Matrix
obua
parents:
diff changeset
   317
22951
dfafcd6223ad whitespace tuned
haftmann
parents: 22578
diff changeset
   318
fun cut_vector size v =
21056
2cfe839e8d58 Symtab.foldl replaced by Symtab.fold
haftmann
parents: 20485
diff changeset
   319
  let
2cfe839e8d58 Symtab.foldl replaced by Symtab.fold
haftmann
parents: 20485
diff changeset
   320
    val count = ref 0;
2cfe839e8d58 Symtab.foldl replaced by Symtab.fold
haftmann
parents: 20485
diff changeset
   321
    fun app (i, s) =  if (!count < size) then
2cfe839e8d58 Symtab.foldl replaced by Symtab.fold
haftmann
parents: 20485
diff changeset
   322
        (count := !count +1 ; Inttab.update (i, s))
2cfe839e8d58 Symtab.foldl replaced by Symtab.fold
haftmann
parents: 20485
diff changeset
   323
      else I
2cfe839e8d58 Symtab.foldl replaced by Symtab.fold
haftmann
parents: 20485
diff changeset
   324
  in
2cfe839e8d58 Symtab.foldl replaced by Symtab.fold
haftmann
parents: 20485
diff changeset
   325
    Inttab.fold app v empty_vector
2cfe839e8d58 Symtab.foldl replaced by Symtab.fold
haftmann
parents: 20485
diff changeset
   326
  end
16784
92ff7c903585 - added cplex package to HOL/Matrix
obua
parents:
diff changeset
   327
22951
dfafcd6223ad whitespace tuned
haftmann
parents: 22578
diff changeset
   328
fun cut_matrix vfilter vsize m =
21056
2cfe839e8d58 Symtab.foldl replaced by Symtab.fold
haftmann
parents: 20485
diff changeset
   329
  let
22951
dfafcd6223ad whitespace tuned
haftmann
parents: 22578
diff changeset
   330
    fun app (i, v) =
21056
2cfe839e8d58 Symtab.foldl replaced by Symtab.fold
haftmann
parents: 20485
diff changeset
   331
      if is_none (Inttab.lookup vfilter i) then I
2cfe839e8d58 Symtab.foldl replaced by Symtab.fold
haftmann
parents: 20485
diff changeset
   332
      else case vsize
2cfe839e8d58 Symtab.foldl replaced by Symtab.fold
haftmann
parents: 20485
diff changeset
   333
       of NONE => Inttab.update (i, v)
2cfe839e8d58 Symtab.foldl replaced by Symtab.fold
haftmann
parents: 20485
diff changeset
   334
        | SOME s => Inttab.update (i, cut_vector s v)
2cfe839e8d58 Symtab.foldl replaced by Symtab.fold
haftmann
parents: 20485
diff changeset
   335
  in Inttab.fold app m empty_matrix end
2cfe839e8d58 Symtab.foldl replaced by Symtab.fold
haftmann
parents: 20485
diff changeset
   336
17412
e26cb20ef0cc TableFun/Symtab: curried lookup and update;
wenzelm
parents: 17261
diff changeset
   337
fun v_elem_at v i = Inttab.lookup v i
e26cb20ef0cc TableFun/Symtab: curried lookup and update;
wenzelm
parents: 17261
diff changeset
   338
fun m_elem_at m i = Inttab.lookup m i
16784
92ff7c903585 - added cplex package to HOL/Matrix
obua
parents:
diff changeset
   339
22951
dfafcd6223ad whitespace tuned
haftmann
parents: 22578
diff changeset
   340
fun v_only_elem v =
16784
92ff7c903585 - added cplex package to HOL/Matrix
obua
parents:
diff changeset
   341
    case Inttab.min_key v of
22951
dfafcd6223ad whitespace tuned
haftmann
parents: 22578
diff changeset
   342
        NONE => NONE
16784
92ff7c903585 - added cplex package to HOL/Matrix
obua
parents:
diff changeset
   343
      | SOME vmin => (case Inttab.max_key v of
22951
dfafcd6223ad whitespace tuned
haftmann
parents: 22578
diff changeset
   344
                          NONE => SOME vmin
dfafcd6223ad whitespace tuned
haftmann
parents: 22578
diff changeset
   345
                        | SOME vmax => if vmin = vmax then SOME vmin else NONE)
16784
92ff7c903585 - added cplex package to HOL/Matrix
obua
parents:
diff changeset
   346
21056
2cfe839e8d58 Symtab.foldl replaced by Symtab.fold
haftmann
parents: 20485
diff changeset
   347
fun v_fold f = Inttab.fold f;
2cfe839e8d58 Symtab.foldl replaced by Symtab.fold
haftmann
parents: 20485
diff changeset
   348
fun m_fold f = Inttab.fold f;
16784
92ff7c903585 - added cplex package to HOL/Matrix
obua
parents:
diff changeset
   349
92ff7c903585 - added cplex package to HOL/Matrix
obua
parents:
diff changeset
   350
end;