1. changed configuration variables for linear programming (Cplex_tools):
LP_SOLVER is either CPLEX or GLPK
CPLEX_PATH is the path to the cplex binary
GLPK_PATH is the path to the glpk binary
The change makes it possible to switch between glpk and cplex at runtime.
2. moved conflicting list theories out of Library.thy into ROOT.ML
--- a/etc/settings Mon Aug 01 11:24:19 2005 +0200
+++ b/etc/settings Mon Aug 01 11:39:33 2005 +0200
@@ -219,9 +219,13 @@
HOL4_PROOFS="$PROOF_DIRS:$ISABELLE_HOME_USER/proofs:$ISABELLE_HOME/proofs"
# For configuring HOL/Matrix/cplex
+# LP_SOLVER is the default solver. It can be changed during runtime via Cplex.set_solver.
# First option: use the commercial cplex solver
-#LP_SOLVER_NAME=CPLEX
-#LP_SOLVER_PATH=cplex
+# LP_SOLVER=CPLEX
+# CPLEX_PATH=cplex
# Second option: use the open source glpk solver
-#LP_SOLVER_NAME=GLPK
-#LP_SOLVER_PATH=glpsol
+# LP_SOLVER=GLPK
+# GLPK_PATH=glpsol
+
+# toogles the detail of the error message in case of a cyclic definition
+DEFS_CHAIN_HISTORY=ON
--- a/src/HOL/Library/Library.thy Mon Aug 01 11:24:19 2005 +0200
+++ b/src/HOL/Library/Library.thy Mon Aug 01 11:39:33 2005 +0200
@@ -17,9 +17,7 @@
While_Combinator
Word
Zorn
- (*List_Prefix*)
Char_ord
- List_lexord
begin
end
(*>*)
--- a/src/HOL/Library/Library/ROOT.ML Mon Aug 01 11:24:19 2005 +0200
+++ b/src/HOL/Library/Library/ROOT.ML Mon Aug 01 11:39:33 2005 +0200
@@ -1,1 +1,3 @@
use_thy "Library";
+use_thy "List_Prefix";
+use_thy "List_lexord";
--- a/src/HOL/Matrix/cplex/Cplex_tools.ML Mon Aug 01 11:24:19 2005 +0200
+++ b/src/HOL/Matrix/cplex/Cplex_tools.ML Mon Aug 01 11:39:33 2005 +0200
@@ -35,6 +35,8 @@
| Optimal of string *
(((* name *) string *
(* value *) string) list)
+
+ datatype cplexSolver = SOLVER_DEFAULT | SOLVER_CPLEX | SOLVER_GLPK
exception Load_cplexFile of string
exception Load_cplexResult of string
@@ -51,12 +53,20 @@
val is_normed_cplexProg : cplexProg -> bool
+ val get_solver : unit -> cplexSolver
+ val set_solver : cplexSolver -> unit
val solve : cplexProg -> cplexResult
end;
structure Cplex : CPLEX =
struct
+datatype cplexSolver = SOLVER_DEFAULT | SOLVER_CPLEX | SOLVER_GLPK
+
+val cplexsolver = ref SOLVER_DEFAULT;
+fun get_solver () = !cplexsolver;
+fun set_solver s = (cplexsolver := s);
+
exception Load_cplexFile of string;
exception Load_cplexResult of string;
exception Save_cplexFile of string;
@@ -1139,7 +1149,7 @@
val lpname = tmp_file (name^".lp")
val resultname = tmp_file (name^".txt")
val _ = save_cplexFile lpname prog
- val cplex_path = getenv "LP_SOLVER_PATH"
+ val cplex_path = getenv "GLPK_PATH"
val cplex = if cplex_path = "" then "glpsol" else cplex_path
val command = (wrap cplex)^" --lpt "^(wrap lpname)^" --output "^(wrap resultname)
val answer = execute command
@@ -1171,7 +1181,7 @@
val resultname = tmp_file (name^".txt")
val scriptname = tmp_file (name^".script")
val _ = save_cplexFile lpname prog
- val cplex_path = getenv "LP_SOLVER_PATH"
+ val cplex_path = getenv "CPLEX_PATH"
val cplex = if cplex_path = "" then "cplex" else cplex_path
val _ = write_script scriptname lpname resultname
val command = (wrap cplex)^" < "^(wrap scriptname)^" > /dev/null"
@@ -1188,10 +1198,14 @@
end
fun solve prog =
- case getenv "LP_SOLVER_NAME" of
- "CPLEX" => solve_cplex prog
- | "GLPK" => solve_glpk prog
- | _ => raise (Execute ("LP_SOLVER_NAME must be set to CPLEX or to GLPK"));
+ case get_solver () of
+ SOLVER_DEFAULT =>
+ (case getenv "LP_SOLVER" of
+ "CPLEX" => solve_cplex prog
+ | "GLPK" => solve_glpk prog
+ | _ => raise (Execute ("LP_SOLVER must be set to CPLEX or to GLPK")))
+ | SOLVER_CPLEX => solve_cplex prog
+ | SOLVER_GLPK => solve_glpk prog
end;