src/HOL/Matrix/fspmlp.ML
author skalberg
Thu, 03 Mar 2005 12:43:01 +0100
changeset 15570 8d8c70b41bab
parent 15531 08c8dad8e399
permissions -rw-r--r--
Move towards standard functions.
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
15178
5f621aa35c25 Matrix theory, linear programming
obua
parents:
diff changeset
     1
signature FSPMLP = 
5f621aa35c25 Matrix theory, linear programming
obua
parents:
diff changeset
     2
sig
5f621aa35c25 Matrix theory, linear programming
obua
parents:
diff changeset
     3
    type linprog
5f621aa35c25 Matrix theory, linear programming
obua
parents:
diff changeset
     4
5f621aa35c25 Matrix theory, linear programming
obua
parents:
diff changeset
     5
    val y : linprog -> cterm
5f621aa35c25 Matrix theory, linear programming
obua
parents:
diff changeset
     6
    val A : linprog -> cterm * cterm
5f621aa35c25 Matrix theory, linear programming
obua
parents:
diff changeset
     7
    val b : linprog -> cterm
5f621aa35c25 Matrix theory, linear programming
obua
parents:
diff changeset
     8
    val c : linprog -> cterm * cterm
5f621aa35c25 Matrix theory, linear programming
obua
parents:
diff changeset
     9
    val r : linprog -> cterm
5f621aa35c25 Matrix theory, linear programming
obua
parents:
diff changeset
    10
5f621aa35c25 Matrix theory, linear programming
obua
parents:
diff changeset
    11
    exception Load of string
5f621aa35c25 Matrix theory, linear programming
obua
parents:
diff changeset
    12
		       
5f621aa35c25 Matrix theory, linear programming
obua
parents:
diff changeset
    13
    val load : string -> int -> bool -> linprog
5f621aa35c25 Matrix theory, linear programming
obua
parents:
diff changeset
    14
end
5f621aa35c25 Matrix theory, linear programming
obua
parents:
diff changeset
    15
5f621aa35c25 Matrix theory, linear programming
obua
parents:
diff changeset
    16
structure fspmlp : FSPMLP = 
5f621aa35c25 Matrix theory, linear programming
obua
parents:
diff changeset
    17
struct
5f621aa35c25 Matrix theory, linear programming
obua
parents:
diff changeset
    18
5f621aa35c25 Matrix theory, linear programming
obua
parents:
diff changeset
    19
type linprog = cterm * (cterm * cterm) * cterm * (cterm * cterm) * cterm 
5f621aa35c25 Matrix theory, linear programming
obua
parents:
diff changeset
    20
5f621aa35c25 Matrix theory, linear programming
obua
parents:
diff changeset
    21
fun y (c1, c2, c3, c4, c5) = c1
5f621aa35c25 Matrix theory, linear programming
obua
parents:
diff changeset
    22
fun A (c1, c2, c3, c4, c5) = c2
5f621aa35c25 Matrix theory, linear programming
obua
parents:
diff changeset
    23
fun b (c1, c2, c3, c4, c5) = c3
5f621aa35c25 Matrix theory, linear programming
obua
parents:
diff changeset
    24
fun c (c1, c2, c3, c4, c5) = c4
5f621aa35c25 Matrix theory, linear programming
obua
parents:
diff changeset
    25
fun r (c1, c2, c3, c4, c5) = c5
5f621aa35c25 Matrix theory, linear programming
obua
parents:
diff changeset
    26
5f621aa35c25 Matrix theory, linear programming
obua
parents:
diff changeset
    27
structure CplexFloatSparseMatrixConverter = 
5f621aa35c25 Matrix theory, linear programming
obua
parents:
diff changeset
    28
MAKE_CPLEX_MATRIX_CONVERTER(structure cplex = Cplex and matrix_builder = FloatSparseMatrixBuilder);
5f621aa35c25 Matrix theory, linear programming
obua
parents:
diff changeset
    29
5f621aa35c25 Matrix theory, linear programming
obua
parents:
diff changeset
    30
datatype bound_type = LOWER | UPPER
5f621aa35c25 Matrix theory, linear programming
obua
parents:
diff changeset
    31
5f621aa35c25 Matrix theory, linear programming
obua
parents:
diff changeset
    32
fun intbound_ord ((i1, b1),(i2,b2)) = 
5f621aa35c25 Matrix theory, linear programming
obua
parents:
diff changeset
    33
    if i1 < i2 then LESS
5f621aa35c25 Matrix theory, linear programming
obua
parents:
diff changeset
    34
    else if i1 = i2 then 
5f621aa35c25 Matrix theory, linear programming
obua
parents:
diff changeset
    35
	(if b1 = b2 then EQUAL else if b1=LOWER then LESS else GREATER)
5f621aa35c25 Matrix theory, linear programming
obua
parents:
diff changeset
    36
    else GREATER
5f621aa35c25 Matrix theory, linear programming
obua
parents:
diff changeset
    37
5f621aa35c25 Matrix theory, linear programming
obua
parents:
diff changeset
    38
structure Inttab = TableFun(type key = int val ord = (rev_order o int_ord));
5f621aa35c25 Matrix theory, linear programming
obua
parents:
diff changeset
    39
5f621aa35c25 Matrix theory, linear programming
obua
parents:
diff changeset
    40
structure VarGraph = TableFun(type key = int*bound_type val ord = intbound_ord);
5f621aa35c25 Matrix theory, linear programming
obua
parents:
diff changeset
    41
(* key -> (float option) * (int -> (float * (((float * float) * key) list)))) *)
5f621aa35c25 Matrix theory, linear programming
obua
parents:
diff changeset
    42
(* dest_key -> (sure_bound * (row_index -> (row_bound * (((coeff_lower * coeff_upper) * src_key) list)))) *)
5f621aa35c25 Matrix theory, linear programming
obua
parents:
diff changeset
    43
5f621aa35c25 Matrix theory, linear programming
obua
parents:
diff changeset
    44
exception Internal of string;
5f621aa35c25 Matrix theory, linear programming
obua
parents:
diff changeset
    45
5f621aa35c25 Matrix theory, linear programming
obua
parents:
diff changeset
    46
fun add_row_bound g dest_key row_index row_bound = 
5f621aa35c25 Matrix theory, linear programming
obua
parents:
diff changeset
    47
    let 
5f621aa35c25 Matrix theory, linear programming
obua
parents:
diff changeset
    48
	val x = 
5f621aa35c25 Matrix theory, linear programming
obua
parents:
diff changeset
    49
	    case VarGraph.lookup (g, dest_key) of
15531
08c8dad8e399 Deleted Library.option type.
skalberg
parents: 15178
diff changeset
    50
		NONE => (NONE, Inttab.update ((row_index, (row_bound, [])), Inttab.empty))
08c8dad8e399 Deleted Library.option type.
skalberg
parents: 15178
diff changeset
    51
	      | SOME (sure_bound, f) =>
15178
5f621aa35c25 Matrix theory, linear programming
obua
parents:
diff changeset
    52
		(sure_bound,
5f621aa35c25 Matrix theory, linear programming
obua
parents:
diff changeset
    53
		 case Inttab.lookup (f, row_index) of
15531
08c8dad8e399 Deleted Library.option type.
skalberg
parents: 15178
diff changeset
    54
		     NONE => Inttab.update ((row_index, (row_bound, [])), f)
08c8dad8e399 Deleted Library.option type.
skalberg
parents: 15178
diff changeset
    55
		   | SOME _ => raise (Internal "add_row_bound"))				     
15178
5f621aa35c25 Matrix theory, linear programming
obua
parents:
diff changeset
    56
    in
5f621aa35c25 Matrix theory, linear programming
obua
parents:
diff changeset
    57
	VarGraph.update ((dest_key, x), g)
5f621aa35c25 Matrix theory, linear programming
obua
parents:
diff changeset
    58
    end    
5f621aa35c25 Matrix theory, linear programming
obua
parents:
diff changeset
    59
5f621aa35c25 Matrix theory, linear programming
obua
parents:
diff changeset
    60
fun update_sure_bound g (key as (_, btype)) bound = 
5f621aa35c25 Matrix theory, linear programming
obua
parents:
diff changeset
    61
    let
5f621aa35c25 Matrix theory, linear programming
obua
parents:
diff changeset
    62
	val x = 
5f621aa35c25 Matrix theory, linear programming
obua
parents:
diff changeset
    63
	    case VarGraph.lookup (g, key) of
15531
08c8dad8e399 Deleted Library.option type.
skalberg
parents: 15178
diff changeset
    64
		NONE => (SOME bound, Inttab.empty)
08c8dad8e399 Deleted Library.option type.
skalberg
parents: 15178
diff changeset
    65
	      | SOME (NONE, f) => (SOME bound, f)
08c8dad8e399 Deleted Library.option type.
skalberg
parents: 15178
diff changeset
    66
	      | SOME (SOME old_bound, f) => 
08c8dad8e399 Deleted Library.option type.
skalberg
parents: 15178
diff changeset
    67
		(SOME ((case btype of 
15178
5f621aa35c25 Matrix theory, linear programming
obua
parents:
diff changeset
    68
			    UPPER => FloatArith.min 
5f621aa35c25 Matrix theory, linear programming
obua
parents:
diff changeset
    69
			  | LOWER => FloatArith.max) 
5f621aa35c25 Matrix theory, linear programming
obua
parents:
diff changeset
    70
			   old_bound bound), f)
5f621aa35c25 Matrix theory, linear programming
obua
parents:
diff changeset
    71
    in
5f621aa35c25 Matrix theory, linear programming
obua
parents:
diff changeset
    72
	VarGraph.update ((key, x), g)
5f621aa35c25 Matrix theory, linear programming
obua
parents:
diff changeset
    73
    end
5f621aa35c25 Matrix theory, linear programming
obua
parents:
diff changeset
    74
5f621aa35c25 Matrix theory, linear programming
obua
parents:
diff changeset
    75
fun get_sure_bound g key = 
5f621aa35c25 Matrix theory, linear programming
obua
parents:
diff changeset
    76
    case VarGraph.lookup (g, key) of 
15531
08c8dad8e399 Deleted Library.option type.
skalberg
parents: 15178
diff changeset
    77
	NONE => NONE
08c8dad8e399 Deleted Library.option type.
skalberg
parents: 15178
diff changeset
    78
      | SOME (sure_bound, _) => sure_bound
15178
5f621aa35c25 Matrix theory, linear programming
obua
parents:
diff changeset
    79
5f621aa35c25 Matrix theory, linear programming
obua
parents:
diff changeset
    80
(*fun get_row_bound g key row_index = 
5f621aa35c25 Matrix theory, linear programming
obua
parents:
diff changeset
    81
    case VarGraph.lookup (g, key) of
15531
08c8dad8e399 Deleted Library.option type.
skalberg
parents: 15178
diff changeset
    82
	NONE => NONE
08c8dad8e399 Deleted Library.option type.
skalberg
parents: 15178
diff changeset
    83
      | SOME (sure_bound, f) =>
15178
5f621aa35c25 Matrix theory, linear programming
obua
parents:
diff changeset
    84
	(case Inttab.lookup (f, row_index) of 
15531
08c8dad8e399 Deleted Library.option type.
skalberg
parents: 15178
diff changeset
    85
	     NONE => NONE
08c8dad8e399 Deleted Library.option type.
skalberg
parents: 15178
diff changeset
    86
	   | SOME (row_bound, _) => (sure_bound, row_bound))*)
15178
5f621aa35c25 Matrix theory, linear programming
obua
parents:
diff changeset
    87
    
5f621aa35c25 Matrix theory, linear programming
obua
parents:
diff changeset
    88
fun add_edge g src_key dest_key row_index coeff = 
5f621aa35c25 Matrix theory, linear programming
obua
parents:
diff changeset
    89
    case VarGraph.lookup (g, dest_key) of
15531
08c8dad8e399 Deleted Library.option type.
skalberg
parents: 15178
diff changeset
    90
	NONE => raise (Internal "add_edge: dest_key not found")
08c8dad8e399 Deleted Library.option type.
skalberg
parents: 15178
diff changeset
    91
      | SOME (sure_bound, f) =>
15178
5f621aa35c25 Matrix theory, linear programming
obua
parents:
diff changeset
    92
	(case Inttab.lookup (f, row_index) of
15531
08c8dad8e399 Deleted Library.option type.
skalberg
parents: 15178
diff changeset
    93
	     NONE => raise (Internal "add_edge: row_index not found")
08c8dad8e399 Deleted Library.option type.
skalberg
parents: 15178
diff changeset
    94
	   | SOME (row_bound, sources) => 
15178
5f621aa35c25 Matrix theory, linear programming
obua
parents:
diff changeset
    95
	     VarGraph.update ((dest_key, (sure_bound, Inttab.update ((row_index, (row_bound, (coeff, src_key) :: sources)), f))), g))
5f621aa35c25 Matrix theory, linear programming
obua
parents:
diff changeset
    96
5f621aa35c25 Matrix theory, linear programming
obua
parents:
diff changeset
    97
fun split_graph g = 
5f621aa35c25 Matrix theory, linear programming
obua
parents:
diff changeset
    98
    let
5f621aa35c25 Matrix theory, linear programming
obua
parents:
diff changeset
    99
	fun split ((r1, r2), (key, (sure_bound, _))) = 
5f621aa35c25 Matrix theory, linear programming
obua
parents:
diff changeset
   100
	    case sure_bound of
15531
08c8dad8e399 Deleted Library.option type.
skalberg
parents: 15178
diff changeset
   101
		NONE => (r1, r2)
08c8dad8e399 Deleted Library.option type.
skalberg
parents: 15178
diff changeset
   102
	      | SOME bound => 
15178
5f621aa35c25 Matrix theory, linear programming
obua
parents:
diff changeset
   103
		(case key of
5f621aa35c25 Matrix theory, linear programming
obua
parents:
diff changeset
   104
		     (u, UPPER) => (r1, Inttab.update ((u, bound), r2))
5f621aa35c25 Matrix theory, linear programming
obua
parents:
diff changeset
   105
		   | (u, LOWER) => (Inttab.update ((u, bound), r1), r2))
5f621aa35c25 Matrix theory, linear programming
obua
parents:
diff changeset
   106
    in
5f621aa35c25 Matrix theory, linear programming
obua
parents:
diff changeset
   107
	VarGraph.foldl split ((Inttab.empty, Inttab.empty), g)
5f621aa35c25 Matrix theory, linear programming
obua
parents:
diff changeset
   108
    end
5f621aa35c25 Matrix theory, linear programming
obua
parents:
diff changeset
   109
5f621aa35c25 Matrix theory, linear programming
obua
parents:
diff changeset
   110
fun it2list t = 
5f621aa35c25 Matrix theory, linear programming
obua
parents:
diff changeset
   111
    let
5f621aa35c25 Matrix theory, linear programming
obua
parents:
diff changeset
   112
	fun tolist (l, a) = a::l
5f621aa35c25 Matrix theory, linear programming
obua
parents:
diff changeset
   113
    in
5f621aa35c25 Matrix theory, linear programming
obua
parents:
diff changeset
   114
	Inttab.foldl tolist ([], t)
5f621aa35c25 Matrix theory, linear programming
obua
parents:
diff changeset
   115
    end
5f621aa35c25 Matrix theory, linear programming
obua
parents:
diff changeset
   116
5f621aa35c25 Matrix theory, linear programming
obua
parents:
diff changeset
   117
(* If safe is true, termination is guaranteed, but the sure bounds may be not optimal (relative to the algorithm).
5f621aa35c25 Matrix theory, linear programming
obua
parents:
diff changeset
   118
   If safe is false, termination is not guaranteed, but on termination the sure bounds are optimal (relative to the algorithm) *)
5f621aa35c25 Matrix theory, linear programming
obua
parents:
diff changeset
   119
fun propagate_sure_bounds safe names g = 
5f621aa35c25 Matrix theory, linear programming
obua
parents:
diff changeset
   120
    let		 	    	
15531
08c8dad8e399 Deleted Library.option type.
skalberg
parents: 15178
diff changeset
   121
	(* returns NONE if no new sure bound could be calculated, otherwise the new sure bound is returned *)
15178
5f621aa35c25 Matrix theory, linear programming
obua
parents:
diff changeset
   122
	fun calc_sure_bound_from_sources g (key as (_, btype)) = 
5f621aa35c25 Matrix theory, linear programming
obua
parents:
diff changeset
   123
	    let		
5f621aa35c25 Matrix theory, linear programming
obua
parents:
diff changeset
   124
		fun mult_upper x (lower, upper) = 
5f621aa35c25 Matrix theory, linear programming
obua
parents:
diff changeset
   125
		    if FloatArith.is_negative x then
5f621aa35c25 Matrix theory, linear programming
obua
parents:
diff changeset
   126
			FloatArith.mul x lower
5f621aa35c25 Matrix theory, linear programming
obua
parents:
diff changeset
   127
		    else
5f621aa35c25 Matrix theory, linear programming
obua
parents:
diff changeset
   128
			FloatArith.mul x upper
5f621aa35c25 Matrix theory, linear programming
obua
parents:
diff changeset
   129
			
5f621aa35c25 Matrix theory, linear programming
obua
parents:
diff changeset
   130
		fun mult_lower x (lower, upper) = 
5f621aa35c25 Matrix theory, linear programming
obua
parents:
diff changeset
   131
		    if FloatArith.is_negative x then
5f621aa35c25 Matrix theory, linear programming
obua
parents:
diff changeset
   132
			FloatArith.mul x upper
5f621aa35c25 Matrix theory, linear programming
obua
parents:
diff changeset
   133
		    else
5f621aa35c25 Matrix theory, linear programming
obua
parents:
diff changeset
   134
			FloatArith.mul x lower
5f621aa35c25 Matrix theory, linear programming
obua
parents:
diff changeset
   135
5f621aa35c25 Matrix theory, linear programming
obua
parents:
diff changeset
   136
		val mult_btype = case btype of UPPER => mult_upper | LOWER => mult_lower
5f621aa35c25 Matrix theory, linear programming
obua
parents:
diff changeset
   137
5f621aa35c25 Matrix theory, linear programming
obua
parents:
diff changeset
   138
		fun calc_sure_bound (sure_bound, (row_index, (row_bound, sources))) = 
5f621aa35c25 Matrix theory, linear programming
obua
parents:
diff changeset
   139
		    let
5f621aa35c25 Matrix theory, linear programming
obua
parents:
diff changeset
   140
			fun add_src_bound (sum, (coeff, src_key)) = 
5f621aa35c25 Matrix theory, linear programming
obua
parents:
diff changeset
   141
			    case sum of 
15531
08c8dad8e399 Deleted Library.option type.
skalberg
parents: 15178
diff changeset
   142
				NONE => NONE
08c8dad8e399 Deleted Library.option type.
skalberg
parents: 15178
diff changeset
   143
			      | SOME x => 
15178
5f621aa35c25 Matrix theory, linear programming
obua
parents:
diff changeset
   144
				(case get_sure_bound g src_key of
15531
08c8dad8e399 Deleted Library.option type.
skalberg
parents: 15178
diff changeset
   145
				     NONE => NONE
08c8dad8e399 Deleted Library.option type.
skalberg
parents: 15178
diff changeset
   146
				   | SOME src_sure_bound => SOME (FloatArith.add x (mult_btype src_sure_bound coeff)))
15178
5f621aa35c25 Matrix theory, linear programming
obua
parents:
diff changeset
   147
		    in
15570
8d8c70b41bab Move towards standard functions.
skalberg
parents: 15531
diff changeset
   148
			case Library.foldl add_src_bound (SOME row_bound, sources) of
15531
08c8dad8e399 Deleted Library.option type.
skalberg
parents: 15178
diff changeset
   149
			    NONE => sure_bound
08c8dad8e399 Deleted Library.option type.
skalberg
parents: 15178
diff changeset
   150
			  | new_sure_bound as (SOME new_bound) => 
15178
5f621aa35c25 Matrix theory, linear programming
obua
parents:
diff changeset
   151
			    (case sure_bound of 
15531
08c8dad8e399 Deleted Library.option type.
skalberg
parents: 15178
diff changeset
   152
				 NONE => new_sure_bound
08c8dad8e399 Deleted Library.option type.
skalberg
parents: 15178
diff changeset
   153
			       | SOME old_bound => 
08c8dad8e399 Deleted Library.option type.
skalberg
parents: 15178
diff changeset
   154
				 SOME (case btype of 
15178
5f621aa35c25 Matrix theory, linear programming
obua
parents:
diff changeset
   155
					   UPPER => FloatArith.min old_bound new_bound
5f621aa35c25 Matrix theory, linear programming
obua
parents:
diff changeset
   156
					 | LOWER => FloatArith.max old_bound new_bound))				 
5f621aa35c25 Matrix theory, linear programming
obua
parents:
diff changeset
   157
		    end		
5f621aa35c25 Matrix theory, linear programming
obua
parents:
diff changeset
   158
	    in
5f621aa35c25 Matrix theory, linear programming
obua
parents:
diff changeset
   159
		case VarGraph.lookup (g, key) of
15531
08c8dad8e399 Deleted Library.option type.
skalberg
parents: 15178
diff changeset
   160
		    NONE => NONE
08c8dad8e399 Deleted Library.option type.
skalberg
parents: 15178
diff changeset
   161
		  | SOME (sure_bound, f) =>
15178
5f621aa35c25 Matrix theory, linear programming
obua
parents:
diff changeset
   162
		    let
5f621aa35c25 Matrix theory, linear programming
obua
parents:
diff changeset
   163
			val x = Inttab.foldl calc_sure_bound (sure_bound, f) 
5f621aa35c25 Matrix theory, linear programming
obua
parents:
diff changeset
   164
		    in
15531
08c8dad8e399 Deleted Library.option type.
skalberg
parents: 15178
diff changeset
   165
			if x = sure_bound then NONE else x
15178
5f621aa35c25 Matrix theory, linear programming
obua
parents:
diff changeset
   166
		    end		
5f621aa35c25 Matrix theory, linear programming
obua
parents:
diff changeset
   167
    	    end
5f621aa35c25 Matrix theory, linear programming
obua
parents:
diff changeset
   168
5f621aa35c25 Matrix theory, linear programming
obua
parents:
diff changeset
   169
	fun propagate ((g, b), (key, _)) = 
5f621aa35c25 Matrix theory, linear programming
obua
parents:
diff changeset
   170
	    case calc_sure_bound_from_sources g key of 
15531
08c8dad8e399 Deleted Library.option type.
skalberg
parents: 15178
diff changeset
   171
		NONE => (g,b)
08c8dad8e399 Deleted Library.option type.
skalberg
parents: 15178
diff changeset
   172
	      | SOME bound => (update_sure_bound g key bound, 
15178
5f621aa35c25 Matrix theory, linear programming
obua
parents:
diff changeset
   173
			       if safe then 
5f621aa35c25 Matrix theory, linear programming
obua
parents:
diff changeset
   174
				   case get_sure_bound g key of
15531
08c8dad8e399 Deleted Library.option type.
skalberg
parents: 15178
diff changeset
   175
				       NONE => true
15178
5f621aa35c25 Matrix theory, linear programming
obua
parents:
diff changeset
   176
				     | _ => b
5f621aa35c25 Matrix theory, linear programming
obua
parents:
diff changeset
   177
			       else
5f621aa35c25 Matrix theory, linear programming
obua
parents:
diff changeset
   178
				   true)
5f621aa35c25 Matrix theory, linear programming
obua
parents:
diff changeset
   179
5f621aa35c25 Matrix theory, linear programming
obua
parents:
diff changeset
   180
	val (g, b) = VarGraph.foldl propagate ((g, false), g) 
5f621aa35c25 Matrix theory, linear programming
obua
parents:
diff changeset
   181
    in
5f621aa35c25 Matrix theory, linear programming
obua
parents:
diff changeset
   182
	if b then propagate_sure_bounds safe names g else g	
5f621aa35c25 Matrix theory, linear programming
obua
parents:
diff changeset
   183
    end	    
5f621aa35c25 Matrix theory, linear programming
obua
parents:
diff changeset
   184
    		
5f621aa35c25 Matrix theory, linear programming
obua
parents:
diff changeset
   185
exception Load of string;
5f621aa35c25 Matrix theory, linear programming
obua
parents:
diff changeset
   186
5f621aa35c25 Matrix theory, linear programming
obua
parents:
diff changeset
   187
fun calcr safe_propagation xlen names prec A b = 
5f621aa35c25 Matrix theory, linear programming
obua
parents:
diff changeset
   188
    let
5f621aa35c25 Matrix theory, linear programming
obua
parents:
diff changeset
   189
	val empty = Inttab.empty
5f621aa35c25 Matrix theory, linear programming
obua
parents:
diff changeset
   190
5f621aa35c25 Matrix theory, linear programming
obua
parents:
diff changeset
   191
	fun instab t i x = Inttab.update ((i,x), t)
5f621aa35c25 Matrix theory, linear programming
obua
parents:
diff changeset
   192
5f621aa35c25 Matrix theory, linear programming
obua
parents:
diff changeset
   193
	fun isnegstr x = String.isPrefix "-" x
5f621aa35c25 Matrix theory, linear programming
obua
parents:
diff changeset
   194
	fun negstr x = if isnegstr x then String.extract (x, 1, NONE) else "-"^x
5f621aa35c25 Matrix theory, linear programming
obua
parents:
diff changeset
   195
5f621aa35c25 Matrix theory, linear programming
obua
parents:
diff changeset
   196
	fun test_1 (lower, upper) = 
5f621aa35c25 Matrix theory, linear programming
obua
parents:
diff changeset
   197
	    if lower = upper then
5f621aa35c25 Matrix theory, linear programming
obua
parents:
diff changeset
   198
		(if FloatArith.is_equal lower (IntInf.fromInt ~1, FloatArith.izero) then ~1 
5f621aa35c25 Matrix theory, linear programming
obua
parents:
diff changeset
   199
		 else if FloatArith.is_equal lower (IntInf.fromInt 1, FloatArith.izero) then 1
5f621aa35c25 Matrix theory, linear programming
obua
parents:
diff changeset
   200
		 else 0)
5f621aa35c25 Matrix theory, linear programming
obua
parents:
diff changeset
   201
	    else 0	
5f621aa35c25 Matrix theory, linear programming
obua
parents:
diff changeset
   202
5f621aa35c25 Matrix theory, linear programming
obua
parents:
diff changeset
   203
	fun calcr (g, (row_index, a)) = 
5f621aa35c25 Matrix theory, linear programming
obua
parents:
diff changeset
   204
	    let				
5f621aa35c25 Matrix theory, linear programming
obua
parents:
diff changeset
   205
		val b =  FloatSparseMatrixBuilder.v_elem_at b row_index
15531
08c8dad8e399 Deleted Library.option type.
skalberg
parents: 15178
diff changeset
   206
		val (_, b2) = ExactFloatingPoint.approx_decstr_by_bin prec (case b of NONE => "0" | SOME b => b)
15178
5f621aa35c25 Matrix theory, linear programming
obua
parents:
diff changeset
   207
		val approx_a = FloatSparseMatrixBuilder.v_fold (fn (l, (i,s)) => 
5f621aa35c25 Matrix theory, linear programming
obua
parents:
diff changeset
   208
								   (i, ExactFloatingPoint.approx_decstr_by_bin prec s)::l) [] a
5f621aa35c25 Matrix theory, linear programming
obua
parents:
diff changeset
   209
			       
5f621aa35c25 Matrix theory, linear programming
obua
parents:
diff changeset
   210
		fun fold_dest_nodes (g, (dest_index, dest_value)) = 
5f621aa35c25 Matrix theory, linear programming
obua
parents:
diff changeset
   211
		    let		
5f621aa35c25 Matrix theory, linear programming
obua
parents:
diff changeset
   212
			val dest_test = test_1 dest_value
5f621aa35c25 Matrix theory, linear programming
obua
parents:
diff changeset
   213
		    in
5f621aa35c25 Matrix theory, linear programming
obua
parents:
diff changeset
   214
			if dest_test = 0 then
5f621aa35c25 Matrix theory, linear programming
obua
parents:
diff changeset
   215
			    g
5f621aa35c25 Matrix theory, linear programming
obua
parents:
diff changeset
   216
			else let
5f621aa35c25 Matrix theory, linear programming
obua
parents:
diff changeset
   217
				val (dest_key as (_, dest_btype), row_bound) = 
5f621aa35c25 Matrix theory, linear programming
obua
parents:
diff changeset
   218
				    if dest_test = ~1 then 
5f621aa35c25 Matrix theory, linear programming
obua
parents:
diff changeset
   219
					((dest_index, LOWER), FloatArith.neg b2)
5f621aa35c25 Matrix theory, linear programming
obua
parents:
diff changeset
   220
				    else
5f621aa35c25 Matrix theory, linear programming
obua
parents:
diff changeset
   221
					((dest_index, UPPER), b2)
5f621aa35c25 Matrix theory, linear programming
obua
parents:
diff changeset
   222
					
5f621aa35c25 Matrix theory, linear programming
obua
parents:
diff changeset
   223
				fun fold_src_nodes (g, (src_index, src_value as (src_lower, src_upper))) = 
5f621aa35c25 Matrix theory, linear programming
obua
parents:
diff changeset
   224
				    if src_index = dest_index then g
5f621aa35c25 Matrix theory, linear programming
obua
parents:
diff changeset
   225
				    else
5f621aa35c25 Matrix theory, linear programming
obua
parents:
diff changeset
   226
					let
5f621aa35c25 Matrix theory, linear programming
obua
parents:
diff changeset
   227
					    val coeff = case dest_btype of 
5f621aa35c25 Matrix theory, linear programming
obua
parents:
diff changeset
   228
							    UPPER => (FloatArith.neg src_upper, FloatArith.neg src_lower)
5f621aa35c25 Matrix theory, linear programming
obua
parents:
diff changeset
   229
							  | LOWER => src_value
5f621aa35c25 Matrix theory, linear programming
obua
parents:
diff changeset
   230
					in
5f621aa35c25 Matrix theory, linear programming
obua
parents:
diff changeset
   231
					    if FloatArith.is_negative src_lower then
5f621aa35c25 Matrix theory, linear programming
obua
parents:
diff changeset
   232
						add_edge g (src_index, UPPER) dest_key row_index coeff
5f621aa35c25 Matrix theory, linear programming
obua
parents:
diff changeset
   233
					    else
5f621aa35c25 Matrix theory, linear programming
obua
parents:
diff changeset
   234
						add_edge g (src_index, LOWER) dest_key row_index coeff
5f621aa35c25 Matrix theory, linear programming
obua
parents:
diff changeset
   235
					end
5f621aa35c25 Matrix theory, linear programming
obua
parents:
diff changeset
   236
			    in	    
15570
8d8c70b41bab Move towards standard functions.
skalberg
parents: 15531
diff changeset
   237
				Library.foldl fold_src_nodes ((add_row_bound g dest_key row_index row_bound), approx_a)
15178
5f621aa35c25 Matrix theory, linear programming
obua
parents:
diff changeset
   238
			    end
5f621aa35c25 Matrix theory, linear programming
obua
parents:
diff changeset
   239
		    end
5f621aa35c25 Matrix theory, linear programming
obua
parents:
diff changeset
   240
	    in
5f621aa35c25 Matrix theory, linear programming
obua
parents:
diff changeset
   241
		case approx_a of
5f621aa35c25 Matrix theory, linear programming
obua
parents:
diff changeset
   242
		    [] => g
5f621aa35c25 Matrix theory, linear programming
obua
parents:
diff changeset
   243
		  | [(u, a)] => 
5f621aa35c25 Matrix theory, linear programming
obua
parents:
diff changeset
   244
		    let
5f621aa35c25 Matrix theory, linear programming
obua
parents:
diff changeset
   245
			val atest = test_1 a
5f621aa35c25 Matrix theory, linear programming
obua
parents:
diff changeset
   246
		    in
5f621aa35c25 Matrix theory, linear programming
obua
parents:
diff changeset
   247
			if atest = ~1 then 			  
5f621aa35c25 Matrix theory, linear programming
obua
parents:
diff changeset
   248
			    update_sure_bound g (u, LOWER) (FloatArith.neg b2)
5f621aa35c25 Matrix theory, linear programming
obua
parents:
diff changeset
   249
			else if atest = 1 then
5f621aa35c25 Matrix theory, linear programming
obua
parents:
diff changeset
   250
			    update_sure_bound g (u, UPPER) b2
5f621aa35c25 Matrix theory, linear programming
obua
parents:
diff changeset
   251
			else
5f621aa35c25 Matrix theory, linear programming
obua
parents:
diff changeset
   252
			    g
5f621aa35c25 Matrix theory, linear programming
obua
parents:
diff changeset
   253
		    end
15570
8d8c70b41bab Move towards standard functions.
skalberg
parents: 15531
diff changeset
   254
		  | _ => Library.foldl fold_dest_nodes (g, approx_a)
15178
5f621aa35c25 Matrix theory, linear programming
obua
parents:
diff changeset
   255
	    end
5f621aa35c25 Matrix theory, linear programming
obua
parents:
diff changeset
   256
	
5f621aa35c25 Matrix theory, linear programming
obua
parents:
diff changeset
   257
	val g = FloatSparseMatrixBuilder.m_fold calcr VarGraph.empty A
5f621aa35c25 Matrix theory, linear programming
obua
parents:
diff changeset
   258
	val g = propagate_sure_bounds safe_propagation names g
5f621aa35c25 Matrix theory, linear programming
obua
parents:
diff changeset
   259
5f621aa35c25 Matrix theory, linear programming
obua
parents:
diff changeset
   260
	val (r1, r2) = split_graph g
5f621aa35c25 Matrix theory, linear programming
obua
parents:
diff changeset
   261
	
5f621aa35c25 Matrix theory, linear programming
obua
parents:
diff changeset
   262
	fun abs_estimate i r1 r2 = 
5f621aa35c25 Matrix theory, linear programming
obua
parents:
diff changeset
   263
	    if i = 0 then FloatSparseMatrixBuilder.empty_spmat
5f621aa35c25 Matrix theory, linear programming
obua
parents:
diff changeset
   264
	    else
5f621aa35c25 Matrix theory, linear programming
obua
parents:
diff changeset
   265
		let
5f621aa35c25 Matrix theory, linear programming
obua
parents:
diff changeset
   266
		    val index = xlen-i
5f621aa35c25 Matrix theory, linear programming
obua
parents:
diff changeset
   267
		    val r = abs_estimate (i-1) r1 r2 
15531
08c8dad8e399 Deleted Library.option type.
skalberg
parents: 15178
diff changeset
   268
		    val b1 = case Inttab.lookup (r1, index) of NONE => raise (Load ("x-value not bounded from below: "^(names index))) | SOME x => x
08c8dad8e399 Deleted Library.option type.
skalberg
parents: 15178
diff changeset
   269
		    val b2 = case Inttab.lookup (r2, index) of NONE => raise (Load ("x-value not bounded from above: "^(names index))) | SOME x => x
15178
5f621aa35c25 Matrix theory, linear programming
obua
parents:
diff changeset
   270
		    val abs_max = FloatArith.max (FloatArith.neg (FloatArith.negative_part b1)) (FloatArith.positive_part b2)    
5f621aa35c25 Matrix theory, linear programming
obua
parents:
diff changeset
   271
		    val vec = FloatSparseMatrixBuilder.cons_spvec (FloatSparseMatrixBuilder.mk_spvec_entry 0 abs_max) FloatSparseMatrixBuilder.empty_spvec
5f621aa35c25 Matrix theory, linear programming
obua
parents:
diff changeset
   272
		in
5f621aa35c25 Matrix theory, linear programming
obua
parents:
diff changeset
   273
		    FloatSparseMatrixBuilder.cons_spmat (FloatSparseMatrixBuilder.mk_spmat_entry index vec) r
5f621aa35c25 Matrix theory, linear programming
obua
parents:
diff changeset
   274
		end		    		    
5f621aa35c25 Matrix theory, linear programming
obua
parents:
diff changeset
   275
    in
5f621aa35c25 Matrix theory, linear programming
obua
parents:
diff changeset
   276
	FloatSparseMatrixBuilder.sign_term (abs_estimate xlen r1 r2)
5f621aa35c25 Matrix theory, linear programming
obua
parents:
diff changeset
   277
    end
5f621aa35c25 Matrix theory, linear programming
obua
parents:
diff changeset
   278
	    
5f621aa35c25 Matrix theory, linear programming
obua
parents:
diff changeset
   279
fun load filename prec safe_propagation =
5f621aa35c25 Matrix theory, linear programming
obua
parents:
diff changeset
   280
    let
5f621aa35c25 Matrix theory, linear programming
obua
parents:
diff changeset
   281
	val prog = Cplex.load_cplexFile filename
5f621aa35c25 Matrix theory, linear programming
obua
parents:
diff changeset
   282
	val prog = Cplex.elim_nonfree_bounds prog
5f621aa35c25 Matrix theory, linear programming
obua
parents:
diff changeset
   283
	val prog = Cplex.relax_strict_ineqs prog
5f621aa35c25 Matrix theory, linear programming
obua
parents:
diff changeset
   284
	val (maximize, c, A, b, (xlen, names, _)) = CplexFloatSparseMatrixConverter.convert_prog prog
5f621aa35c25 Matrix theory, linear programming
obua
parents:
diff changeset
   285
	val r = calcr safe_propagation xlen names prec A b
5f621aa35c25 Matrix theory, linear programming
obua
parents:
diff changeset
   286
	val _ = if maximize then () else raise Load "sorry, cannot handle minimization problems"			
5f621aa35c25 Matrix theory, linear programming
obua
parents:
diff changeset
   287
	val (dualprog, indexof) = FloatSparseMatrixBuilder.dual_cplexProg c A b
5f621aa35c25 Matrix theory, linear programming
obua
parents:
diff changeset
   288
	val results = Cplex.solve dualprog
5f621aa35c25 Matrix theory, linear programming
obua
parents:
diff changeset
   289
	val (optimal,v) = CplexFloatSparseMatrixConverter.convert_results results indexof
15531
08c8dad8e399 Deleted Library.option type.
skalberg
parents: 15178
diff changeset
   290
	val A = FloatSparseMatrixBuilder.cut_matrix v NONE A
15178
5f621aa35c25 Matrix theory, linear programming
obua
parents:
diff changeset
   291
	fun id x = x
5f621aa35c25 Matrix theory, linear programming
obua
parents:
diff changeset
   292
	val v = FloatSparseMatrixBuilder.set_vector FloatSparseMatrixBuilder.empty_matrix 0 v
5f621aa35c25 Matrix theory, linear programming
obua
parents:
diff changeset
   293
	val b = FloatSparseMatrixBuilder.transpose_matrix (FloatSparseMatrixBuilder.set_vector FloatSparseMatrixBuilder.empty_matrix 0 b)
5f621aa35c25 Matrix theory, linear programming
obua
parents:
diff changeset
   294
	val c = FloatSparseMatrixBuilder.set_vector FloatSparseMatrixBuilder.empty_matrix 0 c
5f621aa35c25 Matrix theory, linear programming
obua
parents:
diff changeset
   295
	val (y1, _) = FloatSparseMatrixBuilder.approx_matrix prec FloatArith.positive_part v
5f621aa35c25 Matrix theory, linear programming
obua
parents:
diff changeset
   296
	val A = FloatSparseMatrixBuilder.approx_matrix prec id A
5f621aa35c25 Matrix theory, linear programming
obua
parents:
diff changeset
   297
	val (_,b2) = FloatSparseMatrixBuilder.approx_matrix prec id b
5f621aa35c25 Matrix theory, linear programming
obua
parents:
diff changeset
   298
	val c = FloatSparseMatrixBuilder.approx_matrix prec id c
5f621aa35c25 Matrix theory, linear programming
obua
parents:
diff changeset
   299
    in
5f621aa35c25 Matrix theory, linear programming
obua
parents:
diff changeset
   300
	(y1, A, b2, c, r)
5f621aa35c25 Matrix theory, linear programming
obua
parents:
diff changeset
   301
    end handle CplexFloatSparseMatrixConverter.Converter s => (raise (Load ("Converter: "^s)))
5f621aa35c25 Matrix theory, linear programming
obua
parents:
diff changeset
   302
5f621aa35c25 Matrix theory, linear programming
obua
parents:
diff changeset
   303
end