1. changed configuration variables for linear programming (Cplex_tools):
authorobua
Mon Aug 01 11:39:33 2005 +0200 (2005-08-01)
changeset 1696637e34f315057
parent 16965 46697fa536ab
child 16967 40759607c590
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
etc/settings
src/HOL/Library/Library.thy
src/HOL/Library/Library/ROOT.ML
src/HOL/Matrix/cplex/Cplex_tools.ML
     1.1 --- a/etc/settings	Mon Aug 01 11:24:19 2005 +0200
     1.2 +++ b/etc/settings	Mon Aug 01 11:39:33 2005 +0200
     1.3 @@ -219,9 +219,13 @@
     1.4  HOL4_PROOFS="$PROOF_DIRS:$ISABELLE_HOME_USER/proofs:$ISABELLE_HOME/proofs"
     1.5  
     1.6  # For configuring HOL/Matrix/cplex
     1.7 +# LP_SOLVER is the default solver. It can be changed during runtime via Cplex.set_solver.
     1.8  # First option: use the commercial cplex solver
     1.9 -#LP_SOLVER_NAME=CPLEX
    1.10 -#LP_SOLVER_PATH=cplex
    1.11 +# LP_SOLVER=CPLEX
    1.12 +# CPLEX_PATH=cplex
    1.13  # Second option: use the open source glpk solver
    1.14 -#LP_SOLVER_NAME=GLPK
    1.15 -#LP_SOLVER_PATH=glpsol
    1.16 +# LP_SOLVER=GLPK
    1.17 +# GLPK_PATH=glpsol
    1.18 +
    1.19 +# toogles the detail of the error message in case of a cyclic definition
    1.20 +DEFS_CHAIN_HISTORY=ON
     2.1 --- a/src/HOL/Library/Library.thy	Mon Aug 01 11:24:19 2005 +0200
     2.2 +++ b/src/HOL/Library/Library.thy	Mon Aug 01 11:39:33 2005 +0200
     2.3 @@ -17,9 +17,7 @@
     2.4    While_Combinator
     2.5    Word
     2.6    Zorn
     2.7 -  (*List_Prefix*)
     2.8    Char_ord
     2.9 -  List_lexord
    2.10  begin
    2.11  end
    2.12  (*>*)
     3.1 --- a/src/HOL/Library/Library/ROOT.ML	Mon Aug 01 11:24:19 2005 +0200
     3.2 +++ b/src/HOL/Library/Library/ROOT.ML	Mon Aug 01 11:39:33 2005 +0200
     3.3 @@ -1,1 +1,3 @@
     3.4  use_thy "Library";
     3.5 +use_thy "List_Prefix";
     3.6 +use_thy "List_lexord";
     4.1 --- a/src/HOL/Matrix/cplex/Cplex_tools.ML	Mon Aug 01 11:24:19 2005 +0200
     4.2 +++ b/src/HOL/Matrix/cplex/Cplex_tools.ML	Mon Aug 01 11:39:33 2005 +0200
     4.3 @@ -35,6 +35,8 @@
     4.4  			 | Optimal of string * 
     4.5  				      (((* name *) string * 
     4.6  					(* value *) string) list)
     4.7 +
     4.8 +    datatype cplexSolver = SOLVER_DEFAULT | SOLVER_CPLEX | SOLVER_GLPK
     4.9  						     
    4.10      exception Load_cplexFile of string
    4.11      exception Load_cplexResult of string
    4.12 @@ -51,12 +53,20 @@
    4.13  
    4.14      val is_normed_cplexProg : cplexProg -> bool
    4.15  
    4.16 +    val get_solver : unit -> cplexSolver
    4.17 +    val set_solver : cplexSolver -> unit
    4.18      val solve : cplexProg -> cplexResult
    4.19  end;
    4.20  
    4.21  structure Cplex  : CPLEX =
    4.22  struct
    4.23  
    4.24 +datatype cplexSolver = SOLVER_DEFAULT | SOLVER_CPLEX | SOLVER_GLPK
    4.25 +
    4.26 +val cplexsolver = ref SOLVER_DEFAULT;
    4.27 +fun get_solver () = !cplexsolver;
    4.28 +fun set_solver s = (cplexsolver := s);
    4.29 +
    4.30  exception Load_cplexFile of string;
    4.31  exception Load_cplexResult of string;
    4.32  exception Save_cplexFile of string;
    4.33 @@ -1139,7 +1149,7 @@
    4.34  	val lpname = tmp_file (name^".lp")
    4.35  	val resultname = tmp_file (name^".txt")
    4.36  	val _ = save_cplexFile lpname prog		
    4.37 -	val cplex_path = getenv "LP_SOLVER_PATH"
    4.38 +	val cplex_path = getenv "GLPK_PATH"
    4.39  	val cplex = if cplex_path = "" then "glpsol" else cplex_path
    4.40  	val command = (wrap cplex)^" --lpt "^(wrap lpname)^" --output "^(wrap resultname)
    4.41  	val answer = execute command
    4.42 @@ -1171,7 +1181,7 @@
    4.43  	val resultname = tmp_file (name^".txt")
    4.44  	val scriptname = tmp_file (name^".script")
    4.45  	val _ = save_cplexFile lpname prog		
    4.46 -	val cplex_path = getenv "LP_SOLVER_PATH"
    4.47 +	val cplex_path = getenv "CPLEX_PATH"
    4.48  	val cplex = if cplex_path = "" then "cplex" else cplex_path
    4.49  	val _ = write_script scriptname lpname resultname
    4.50  	val command = (wrap cplex)^" < "^(wrap scriptname)^" > /dev/null"
    4.51 @@ -1188,10 +1198,14 @@
    4.52      end
    4.53  
    4.54  fun solve prog = 
    4.55 -    case getenv "LP_SOLVER_NAME" of
    4.56 -	"CPLEX" => solve_cplex prog
    4.57 -      | "GLPK" => solve_glpk prog
    4.58 -      | _ => raise (Execute ("LP_SOLVER_NAME must be set to CPLEX or to GLPK"));
    4.59 +    case get_solver () of
    4.60 +      SOLVER_DEFAULT => 
    4.61 +        (case getenv "LP_SOLVER" of
    4.62 +	   "CPLEX" => solve_cplex prog
    4.63 +         | "GLPK" => solve_glpk prog
    4.64 +         | _ => raise (Execute ("LP_SOLVER must be set to CPLEX or to GLPK")))
    4.65 +    | SOLVER_CPLEX => solve_cplex prog
    4.66 +    | SOLVER_GLPK => solve_glpk prog
    4.67  		   
    4.68  end;
    4.69