# HG changeset patch # User obua # Date 1183995595 -7200 # Node ID 825bea0266dbfcc5fa6b9019040ff43e37b3b3e5 # Parent 9c486517354a0ac4c343cfd9153c3f6459d4e2e2 adopted to new computing oracle and fixed bugs introduced by tuning diff -r 9c486517354a -r 825bea0266db src/HOL/Matrix/cplex/Cplex.thy --- a/src/HOL/Matrix/cplex/Cplex.thy Mon Jul 09 17:38:40 2007 +0200 +++ b/src/HOL/Matrix/cplex/Cplex.thy Mon Jul 09 17:39:55 2007 +0200 @@ -4,7 +4,7 @@ *) theory Cplex -imports FloatSparseMatrix +imports FloatSparseMatrix "~~/src/HOL/Tools/ComputeNumeral" uses "Cplex_tools.ML" "CplexMatrixConverter.ML" "FloatSparseMatrixBuilder.ML" "fspmlp.ML" begin diff -r 9c486517354a -r 825bea0266db src/HOL/Matrix/cplex/FloatSparseMatrixBuilder.ML --- a/src/HOL/Matrix/cplex/FloatSparseMatrixBuilder.ML Mon Jul 09 17:38:40 2007 +0200 +++ b/src/HOL/Matrix/cplex/FloatSparseMatrixBuilder.ML Mon Jul 09 17:39:55 2007 +0200 @@ -69,7 +69,7 @@ val eupper = HOLogic.mk_prod (index, fupper) in (elower :: lower, eupper :: upper) end; in - pairself (HOLogic.mk_list spvecT) (Inttab.fold app vector ([], [])) + pairself (HOLogic.mk_list spvec_elemT) (Inttab.fold app vector ([], [])) end; fun approx_matrix prec pprt vector = @@ -82,7 +82,7 @@ val eupper = HOLogic.mk_prod (index, fupper) in (elower :: lower, eupper :: upper) end; in - pairself (HOLogic.mk_list spmatT) (Inttab.fold app vector ([], [])) + pairself (HOLogic.mk_list spmat_elemT) (Inttab.fold app vector ([], [])) end; exception Nat_expected of int; diff -r 9c486517354a -r 825bea0266db src/HOL/Matrix/cplex/MatrixLP.thy --- a/src/HOL/Matrix/cplex/MatrixLP.thy Mon Jul 09 17:38:40 2007 +0200 +++ b/src/HOL/Matrix/cplex/MatrixLP.thy Mon Jul 09 17:39:55 2007 +0200 @@ -4,65 +4,7 @@ *) theory MatrixLP -imports Cplex "~~/src/Tools/Compute_Oracle/Compute_Oracle" -uses ("matrixlp.ML") +imports Cplex +uses "matrixlp.ML" begin - -constdefs - list_case_compute :: "'b list \ 'a \ ('b \ 'b list \ 'a) \ 'a" - "list_case_compute l a f == list_case a f l" - -lemma list_case_compute: "list_case = (\ (a::'a) f (l::'b list). list_case_compute l a f)" - apply (rule ext)+ - apply (simp add: list_case_compute_def) - done - -lemma list_case_compute_empty: "list_case_compute ([]::'b list) = (\ (a::'a) f. a)" - apply (rule ext)+ - apply (simp add: list_case_compute_def) - done - -lemma list_case_compute_cons: "list_case_compute (u#v) = (\ (a::'a) f. (f (u::'b) v))" - apply (rule ext)+ - apply (simp add: list_case_compute_def) - done - -lemma If_True: "(If True) = (\ x y. x)" - apply (rule ext)+ - apply auto - done - -lemma If_False: "(If False) = (\ x y. y)" - apply (rule ext)+ - apply auto - done - -lemma Let_compute: "Let (x::'a) f = ((f x)::'b)" - by (simp add: Let_def) - -lemma fst_compute: "fst (a::'a, b::'b) = a" - by auto - -lemma snd_compute: "snd (a::'a, b::'b) = b" - by auto - -lemma bool1: "(\ True) = False" by blast -lemma bool2: "(\ False) = True" by blast -lemma bool3: "((P\bool) \ True) = P" by blast -lemma bool4: "(True \ (P\bool)) = P" by blast -lemma bool5: "((P\bool) \ False) = False" by blast -lemma bool6: "(False \ (P\bool)) = False" by blast -lemma bool7: "((P\bool) \ True) = True" by blast -lemma bool8: "(True \ (P\bool)) = True" by blast -lemma bool9: "((P\bool) \ False) = P" by blast -lemma bool10: "(False \ (P\bool)) = P" by blast -lemmas boolarith = bool1 bool2 bool3 bool4 bool5 bool6 bool7 bool8 bool9 bool10 - -lemmas float_arith = Float.arith -lemmas sparse_row_matrix_arith_simps = SparseMatrix.sparse_row_matrix_arith_simps -lemmas sorted_sp_simps = SparseMatrix.sorted_sp_simps -lemmas fst_snd_conv = Product_Type.fst_conv Product_Type.snd_conv - -use "matrixlp.ML" - end diff -r 9c486517354a -r 825bea0266db src/HOL/Matrix/cplex/fspmlp.ML --- a/src/HOL/Matrix/cplex/fspmlp.ML Mon Jul 09 17:38:40 2007 +0200 +++ b/src/HOL/Matrix/cplex/fspmlp.ML Mon Jul 09 17:39:55 2007 +0200 @@ -187,14 +187,10 @@ exception Load of string; -(*val empty_spvec = @ {term "Nil :: (nat * real) list"}; -fun cons_spvec x xs = @ {term "Cons :: nat * real => nat * real => (nat * real) list"} $ x $ xs; -val empty_spmat = @ {term "Nil :: (nat * (nat * real) list) list"}; -fun cons_spmat x xs = @ {term "Cons :: nat * (nat * real) list => (nat * (nat * real) list) list => (nat * (nat * real) list) list"} $ x $ xs;*) -val empty_spvec = Bound 0 -fun cons_spvec x xs = Bound 0 -val empty_spmat = Bound 0 -fun cons_spmat x xs = Bound 0 +val empty_spvec = @{term "Nil :: real spvec"}; +fun cons_spvec x xs = @{term "Cons :: nat * real => real spvec => real spvec"} $ x $ xs; +val empty_spmat = @{term "Nil :: real spmat"}; +fun cons_spmat x xs = @{term "Cons :: nat * real spvec => real spmat => real spmat"} $ x $ xs; fun calcr safe_propagation xlen names prec A b = let @@ -267,9 +263,10 @@ end val g = FloatSparseMatrixBuilder.m_fold calcr A VarGraph.empty + val g = propagate_sure_bounds safe_propagation names g - val (r1, r2) = split_graph g + val (r1, r2) = split_graph g fun add_row_entry m index value = let @@ -292,7 +289,9 @@ in (add_row_entry r i' abs_max, (add_row_entry r12_1 i' b1, add_row_entry r12_2 i' b2)) end + val (r, (r1, r2)) = abs_estimate xlen r1 r2 + in (r, (r1, r2)) end @@ -302,7 +301,7 @@ val prog = Cplex.load_cplexFile filename val prog = Cplex.elim_nonfree_bounds prog val prog = Cplex.relax_strict_ineqs prog - val (maximize, c, A, b, (xlen, names, _)) = CplexFloatSparseMatrixConverter.convert_prog prog + val (maximize, c, A, b, (xlen, names, _)) = CplexFloatSparseMatrixConverter.convert_prog prog val (r, (r1, r2)) = calcr safe_propagation xlen names prec A b val _ = if maximize then () else raise Load "sorry, cannot handle minimization problems" val (dualprog, indexof) = FloatSparseMatrixBuilder.dual_cplexProg c A b diff -r 9c486517354a -r 825bea0266db src/HOL/Matrix/cplex/matrixlp.ML --- a/src/HOL/Matrix/cplex/matrixlp.ML Mon Jul 09 17:38:40 2007 +0200 +++ b/src/HOL/Matrix/cplex/matrixlp.ML Mon Jul 09 17:39:55 2007 +0200 @@ -23,12 +23,15 @@ ([(certT (TVar (hd (term_tvars (prop_of thm)))), certT HOLogic.realT)], []) thm) end -val spm_mult_le_dual_prts_no_let = thm "SparseMatrix.spm_mult_le_dual_prts_no_let"; -val cert = cterm_of (Thm.theory_of_thm spm_mult_le_dual_prts_no_let); +local + +val cert = cterm_of @{theory "Cplex"} + +in fun lp_dual_estimate_prt_primitive (y, (A1, A2), (c1, c2), b, (r1, r2)) = let - val th = inst_real spm_mult_le_dual_prts_no_let + val th = inst_real @{thm "SparseMatrix.spm_mult_le_dual_prts_no_let"} fun var s x = (cert (Var ((s,0), FloatSparseMatrixBuilder.spmatT)), x) val th = Thm.instantiate ([], [var "A1" A1, var "A2" A2, var "y" y, var "c1" c1, var "c2" c2, var "r1" r1, var "r2" r2, var "b" b]) th @@ -41,21 +44,15 @@ open Fspmlp val l = load lptfile prec false in - (y l |> cert, A l |> pairself cert, c l |> pairself cert, b l |> cert, r12 l |> pairself cert) + (y l |> cert, A l |> pairself cert, c l |> pairself cert, b l |> cert, r12 l |> pairself cert) end in lp_dual_estimate_prt_primitive certificate end -fun is_meta_eq th = - let - fun check ((Const ("==", _)) $ _ $ _) = true - | check _ = false - in - check (concl_of th) - end +end -fun prep ths = filter is_meta_eq ths @ map (standard o mk_meta_eq) (filter_out is_meta_eq ths) +fun prep ths = ComputeHOL.prep_thms ths fun inst_tvar ty thm = let @@ -69,38 +66,27 @@ fun inst_tvars [] thms = thms | inst_tvars (ty::tys) thms = inst_tvars tys (map (inst_tvar ty) thms) -val matrix_compute = - let - val spvecT = FloatSparseMatrixBuilder.spvecT - val spmatT = FloatSparseMatrixBuilder.spmatT - val spvecT_elem = HOLogic.mk_prodT (HOLogic.natT, HOLogic.realT) - val spmatT_elem = HOLogic.mk_prodT (HOLogic.natT, spvecT) - val case_compute = map thm ["list_case_compute", "list_case_compute_empty", "list_case_compute_cons"] - val ths = - prep ( - (inst_tvars [HOLogic.intT, HOLogic.natT] (thms "Let_compute")) - @ (inst_tvars [HOLogic.intT, HOLogic.intT] (thms "Let_compute")) - @ (map (fn t => inst_tvar t (thm "If_True")) [HOLogic.intT, HOLogic.natT, HOLogic.realT, spvecT, spmatT, HOLogic.boolT]) - @ (map (fn t => inst_tvar t (thm "If_False")) [HOLogic.intT, HOLogic.natT, HOLogic.realT, spvecT, spmatT, HOLogic.boolT]) - @ (thms "MatrixLP.float_arith") - @ (map (inst_tvar HOLogic.realT) (thms "MatrixLP.sparse_row_matrix_arith_simps")) - @ (thms "MatrixLP.boolarith") - @ (inst_tvars [HOLogic.natT, HOLogic.realT] [thm "fst_compute", thm "snd_compute"]) - @ (inst_tvars [HOLogic.natT, FloatSparseMatrixBuilder.spvecT] [thm "fst_compute", thm "snd_compute"]) - @ (inst_tvars [HOLogic.boolT, spmatT_elem] case_compute) - @ (inst_tvars [HOLogic.boolT, spvecT_elem] case_compute) - @ (inst_tvars [HOLogic.boolT, HOLogic.realT] case_compute) - @ (inst_tvars [spvecT] (thms "MatrixLP.sorted_sp_simps")) - @ (inst_tvars [HOLogic.realT] (thms "MatrixLP.sorted_sp_simps")) - @ [thm "zero_eq_Numeral0_nat", thm "one_eq_Numeral1_nat"] - @ (inst_tvars [HOLogic.intT] [thm "zero_eq_Numeral0_nring", thm "one_eq_Numeral1_nring"]) - @ (inst_tvars [HOLogic.realT] [thm "zero_eq_Numeral0_nring", thm "one_eq_Numeral1_nring"])) +local + val matrix_lemmas = [ + "ComputeHOL.compute_list_case", + "ComputeHOL.compute_let", + "ComputeHOL.compute_if", + "Float.arith", + "SparseMatrix.sparse_row_matrix_arith_simps", + "ComputeHOL.compute_bool", + "ComputeHOL.compute_pair", + "SparseMatrix.sorted_sp_simps", + "ComputeNumeral.number_norm", + "ComputeNumeral.natnorm"] + fun get_thms n = ComputeHOL.prep_thms (PureThy.get_thms @{theory "Cplex"} (Name n)) + val ths = List.concat (map get_thms matrix_lemmas) + val computer = PCompute.make Compute.SML @{theory "Cplex"} ths [] +in - val c = Compute.basic_make (the_context ()) ths - in - Compute.rewrite c - end +fun matrix_compute c = hd (PCompute.rewrite computer [c]) +end + fun matrix_simplify th = let val simp_th = matrix_compute (cprop_of th)