removed obsolete remote_cvc3 and remote_z3
authorboehmes
Sun Jan 19 22:38:17 2014 +0100 (2014-01-19)
changeset 55049327eafb594ba
parent 55043 acefda71629b
child 55050 de68c9c3e454
removed obsolete remote_cvc3 and remote_z3
NEWS
src/HOL/SMT.thy
src/HOL/TPTP/TPTP_Parser_Example.thy
src/HOL/Tools/SMT/lib/scripts/remote_smt
src/HOL/Tools/SMT/smt_setup_solvers.ML
src/HOL/Tools/etc/settings
     1.1 --- a/NEWS	Sun Jan 19 11:05:38 2014 +0100
     1.2 +++ b/NEWS	Sun Jan 19 22:38:17 2014 +0100
     1.3 @@ -196,6 +196,8 @@
     1.4  shows up as additional case in fixpoint induction proofs.
     1.5  INCOMPATIBILITY
     1.6  
     1.7 +* Removed solvers remote_cvc3 and remote_z3. Use cvc3 and z3 instead.
     1.8 +
     1.9  * Nitpick:
    1.10    - Fixed soundness bug whereby mutually recursive datatypes could take
    1.11      infinite values.
     2.1 --- a/src/HOL/SMT.thy	Sun Jan 19 11:05:38 2014 +0100
     2.2 +++ b/src/HOL/SMT.thy	Sun Jan 19 22:38:17 2014 +0100
     2.3 @@ -204,9 +204,9 @@
     2.4  options.
     2.5  *}
     2.6  
     2.7 -declare [[ cvc3_options = "", remote_cvc3_options = "" ]]
     2.8 +declare [[ cvc3_options = "" ]]
     2.9  declare [[ yices_options = "" ]]
    2.10 -declare [[ z3_options = "", remote_z3_options = "" ]]
    2.11 +declare [[ z3_options = "" ]]
    2.12  
    2.13  text {*
    2.14  Enable the following option to use built-in support for datatypes and
     3.1 --- a/src/HOL/TPTP/TPTP_Parser_Example.thy	Sun Jan 19 11:05:38 2014 +0100
     3.2 +++ b/src/HOL/TPTP/TPTP_Parser_Example.thy	Sun Jan 19 22:38:17 2014 +0100
     3.3 @@ -65,9 +65,9 @@
     3.4  @{assert} (is_some (try (auto_prove @{context}) an_fmlas) = false)
     3.5  *}
     3.6  
     3.7 -sledgehammer_params [provers = remote_z3, debug]
     3.8 +sledgehammer_params [provers = z3, debug]
     3.9  ML {*
    3.10  @{assert} (is_some (try (sh_prove @{context}) an_fmlas) = true)
    3.11  *}
    3.12  
    3.13 -end
    3.14 \ No newline at end of file
    3.15 +end
     4.1 --- a/src/HOL/Tools/SMT/lib/scripts/remote_smt	Sun Jan 19 11:05:38 2014 +0100
     4.2 +++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
     4.3 @@ -1,32 +0,0 @@
     4.4 -#!/usr/bin/env perl
     4.5 -#
     4.6 -# Author: Sascha Boehme, TU Muenchen
     4.7 -#
     4.8 -# Invoke remote SMT solvers.
     4.9 -
    4.10 -use strict;
    4.11 -use warnings;
    4.12 -use LWP;
    4.13 -
    4.14 -
    4.15 -# arguments
    4.16 -
    4.17 -my $solver = $ARGV[0];
    4.18 -my @options = @ARGV[1 .. ($#ARGV - 1)];
    4.19 -my $problem_file = $ARGV[-1];
    4.20 -
    4.21 -
    4.22 -# call solver
    4.23 -
    4.24 -my $agent = LWP::UserAgent->new;
    4.25 -$agent->env_proxy;
    4.26 -$agent->agent("SMT-Request");
    4.27 -$agent->timeout(180);
    4.28 -my $response = $agent->post($ENV{"ISABELLE_SMT_REMOTE_URL"}, [
    4.29 -  "Solver" => $solver,
    4.30 -  "Options" => join(" ", @options),
    4.31 -  "Problem" => [$problem_file] ],
    4.32 -  "Content_Type" => "form-data");
    4.33 -if (not $response->is_success) { die "HTTP error: " . $response->message; }
    4.34 -else { print $response->content; }
    4.35 -
     5.1 --- a/src/HOL/Tools/SMT/smt_setup_solvers.ML	Sun Jan 19 11:05:38 2014 +0100
     5.2 +++ b/src/HOL/Tools/SMT/smt_setup_solvers.ML	Sun Jan 19 22:38:17 2014 +0100
     5.3 @@ -20,23 +20,9 @@
     5.4  
     5.5  (* helper functions *)
     5.6  
     5.7 -val remote_prefix = "remote_"
     5.8 -fun make_name is_remote name = name |> is_remote ? prefix remote_prefix
     5.9 -
    5.10 -fun make_local_avail name () = getenv (name ^ "_SOLVER") <> ""
    5.11 -fun make_remote_avail name () = getenv (name ^ "_REMOTE_SOLVER") <> ""
    5.12 -fun make_avail is_remote name =
    5.13 -  if is_remote then make_remote_avail name
    5.14 -  else make_local_avail name orf make_remote_avail name
    5.15 +fun make_avail name () = getenv (name ^ "_SOLVER") <> ""
    5.16  
    5.17 -fun make_local_command name () = [getenv (name ^ "_SOLVER")]
    5.18 -fun make_remote_command name () =
    5.19 -  [getenv "ISABELLE_SMT_REMOTE", getenv (name ^ "_REMOTE_SOLVER")]
    5.20 -fun make_command is_remote name =
    5.21 -  if is_remote then make_remote_command name
    5.22 -  else (fn () =>
    5.23 -    if make_local_avail name () then make_local_command name ()
    5.24 -    else make_remote_command name ())
    5.25 +fun make_command name () = [getenv (name ^ "_SOLVER")]
    5.26  
    5.27  fun outcome_of unsat sat unknown solver_name line =
    5.28    if String.isPrefix unsat line then SMT_Solver.Unsat
    5.29 @@ -62,34 +48,31 @@
    5.30      "-seed", string_of_int (Config.get ctxt SMT_Config.random_seed),
    5.31      "-lang", "smtlib", "-output-lang", "presentation",
    5.32      "-timeout", string_of_int (Real.ceil (Config.get ctxt SMT_Config.timeout))]
    5.33 -
    5.34 -  fun mk is_remote = {
    5.35 -    name = make_name is_remote "cvc3",
    5.36 -    class = K SMTLIB_Interface.smtlibC,
    5.37 -    avail = make_avail is_remote "CVC3",
    5.38 -    command = make_command is_remote "CVC3",
    5.39 -    options = cvc3_options,
    5.40 -    default_max_relevant = 400 (* FUDGE *),
    5.41 -    supports_filter = false,
    5.42 -    outcome =
    5.43 -      on_first_line (outcome_of "Unsatisfiable." "Satisfiable." "Unknown."),
    5.44 -    cex_parser = NONE,
    5.45 -    reconstruct = NONE }
    5.46  in
    5.47  
    5.48 -fun cvc3 () = mk false
    5.49 -fun remote_cvc3 () = mk true
    5.50 +val cvc3: SMT_Solver.solver_config = {
    5.51 +  name = "cvc3",
    5.52 +  class = K SMTLIB_Interface.smtlibC,
    5.53 +  avail = make_avail "CVC3",
    5.54 +  command = make_command "CVC3",
    5.55 +  options = cvc3_options,
    5.56 +  default_max_relevant = 400 (* FUDGE *),
    5.57 +  supports_filter = false,
    5.58 +  outcome =
    5.59 +    on_first_line (outcome_of "Unsatisfiable." "Satisfiable." "Unknown."),
    5.60 +  cex_parser = NONE,
    5.61 +  reconstruct = NONE }
    5.62  
    5.63  end
    5.64  
    5.65  
    5.66  (* Yices *)
    5.67  
    5.68 -fun yices () = {
    5.69 +val yices: SMT_Solver.solver_config = {
    5.70    name = "yices",
    5.71    class = K SMTLIB_Interface.smtlibC,
    5.72 -  avail = make_local_avail "YICES",
    5.73 -  command = make_local_command "YICES",
    5.74 +  avail = make_avail "YICES",
    5.75 +  command = make_command "YICES",
    5.76    options = (fn ctxt => [
    5.77      "--rand-seed=" ^ string_of_int (Config.get ctxt SMT_Config.random_seed),
    5.78      "--timeout=" ^
    5.79 @@ -146,8 +129,7 @@
    5.80    Attrib.setup_config_bool @{binding z3_with_extensions} (K false)
    5.81  
    5.82  local
    5.83 -  fun z3_make_command is_remote name () =
    5.84 -    if_z3_non_commercial (make_command is_remote name)
    5.85 +  fun z3_make_command name () = if_z3_non_commercial (make_command name)
    5.86  
    5.87    fun z3_options ctxt =
    5.88      ["-rs:" ^ string_of_int (Config.get ctxt SMT_Config.random_seed),
    5.89 @@ -181,22 +163,19 @@
    5.90    fun select_class ctxt =
    5.91      if Config.get ctxt z3_with_extensions then Z3_Interface.smtlib_z3C
    5.92      else SMTLIB_Interface.smtlibC
    5.93 -
    5.94 -  fun mk is_remote = {
    5.95 -    name = make_name is_remote "z3",
    5.96 -    class = select_class,
    5.97 -    avail = make_avail is_remote "Z3",
    5.98 -    command = z3_make_command is_remote "Z3",
    5.99 -    options = z3_options,
   5.100 -    default_max_relevant = 350 (* FUDGE *),
   5.101 -    supports_filter = true,
   5.102 -    outcome = z3_on_first_or_last_line,
   5.103 -    cex_parser = SOME Z3_Model.parse_counterex,
   5.104 -    reconstruct = SOME Z3_Proof_Reconstruction.reconstruct }
   5.105  in
   5.106  
   5.107 -fun z3 () = mk false
   5.108 -fun remote_z3 () = mk true
   5.109 +val z3: SMT_Solver.solver_config = {
   5.110 +  name = "z3",
   5.111 +  class = select_class,
   5.112 +  avail = make_avail "Z3",
   5.113 +  command = z3_make_command "Z3",
   5.114 +  options = z3_options,
   5.115 +  default_max_relevant = 350 (* FUDGE *),
   5.116 +  supports_filter = true,
   5.117 +  outcome = z3_on_first_or_last_line,
   5.118 +  cex_parser = SOME Z3_Model.parse_counterex,
   5.119 +  reconstruct = SOME Z3_Proof_Reconstruction.reconstruct }
   5.120  
   5.121  end
   5.122  
   5.123 @@ -204,10 +183,8 @@
   5.124  (* overall setup *)
   5.125  
   5.126  val setup =
   5.127 -  SMT_Solver.add_solver (cvc3 ()) #>
   5.128 -  SMT_Solver.add_solver (remote_cvc3 ()) #>
   5.129 -  SMT_Solver.add_solver (yices ()) #>
   5.130 -  SMT_Solver.add_solver (z3 ()) #>
   5.131 -  SMT_Solver.add_solver (remote_z3 ())
   5.132 +  SMT_Solver.add_solver cvc3 #>
   5.133 +  SMT_Solver.add_solver yices #>
   5.134 +  SMT_Solver.add_solver z3
   5.135  
   5.136  end
     6.1 --- a/src/HOL/Tools/etc/settings	Sun Jan 19 11:05:38 2014 +0100
     6.2 +++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
     6.3 @@ -1,5 +0,0 @@
     6.4 -# -*- shell-script -*- :mode=shellscript:
     6.5 -
     6.6 -ISABELLE_SMT_REMOTE="$ISABELLE_HOME/src/HOL/Tools/SMT/lib/scripts/remote_smt"
     6.7 -ISABELLE_SMT_REMOTE_URL="http://smt.in.tum.de/smt"
     6.8 -