# HG changeset patch
# User boehmes
# Date 1390167497 -3600
# Node ID 327eafb594ba1524a4b8ff1c63a08d888e90c566
# Parent  acefda71629bec3b6dfe87649302f6d481aaa2ab
removed obsolete remote_cvc3 and remote_z3

diff -r acefda71629b -r 327eafb594ba NEWS
--- a/NEWS	Sun Jan 19 11:05:38 2014 +0100
+++ b/NEWS	Sun Jan 19 22:38:17 2014 +0100
@@ -196,6 +196,8 @@
 shows up as additional case in fixpoint induction proofs.
 INCOMPATIBILITY
 
+* Removed solvers remote_cvc3 and remote_z3. Use cvc3 and z3 instead.
+
 * Nitpick:
   - Fixed soundness bug whereby mutually recursive datatypes could take
     infinite values.
diff -r acefda71629b -r 327eafb594ba src/HOL/SMT.thy
--- a/src/HOL/SMT.thy	Sun Jan 19 11:05:38 2014 +0100
+++ b/src/HOL/SMT.thy	Sun Jan 19 22:38:17 2014 +0100
@@ -204,9 +204,9 @@
 options.
 *}
 
-declare [[ cvc3_options = "", remote_cvc3_options = "" ]]
+declare [[ cvc3_options = "" ]]
 declare [[ yices_options = "" ]]
-declare [[ z3_options = "", remote_z3_options = "" ]]
+declare [[ z3_options = "" ]]
 
 text {*
 Enable the following option to use built-in support for datatypes and
diff -r acefda71629b -r 327eafb594ba src/HOL/TPTP/TPTP_Parser_Example.thy
--- a/src/HOL/TPTP/TPTP_Parser_Example.thy	Sun Jan 19 11:05:38 2014 +0100
+++ b/src/HOL/TPTP/TPTP_Parser_Example.thy	Sun Jan 19 22:38:17 2014 +0100
@@ -65,9 +65,9 @@
 @{assert} (is_some (try (auto_prove @{context}) an_fmlas) = false)
 *}
 
-sledgehammer_params [provers = remote_z3, debug]
+sledgehammer_params [provers = z3, debug]
 ML {*
 @{assert} (is_some (try (sh_prove @{context}) an_fmlas) = true)
 *}
 
-end
\ No newline at end of file
+end
diff -r acefda71629b -r 327eafb594ba src/HOL/Tools/SMT/lib/scripts/remote_smt
--- a/src/HOL/Tools/SMT/lib/scripts/remote_smt	Sun Jan 19 11:05:38 2014 +0100
+++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
@@ -1,32 +0,0 @@
-#!/usr/bin/env perl
-#
-# Author: Sascha Boehme, TU Muenchen
-#
-# Invoke remote SMT solvers.
-
-use strict;
-use warnings;
-use LWP;
-
-
-# arguments
-
-my $solver = $ARGV[0];
-my @options = @ARGV[1 .. ($#ARGV - 1)];
-my $problem_file = $ARGV[-1];
-
-
-# call solver
-
-my $agent = LWP::UserAgent->new;
-$agent->env_proxy;
-$agent->agent("SMT-Request");
-$agent->timeout(180);
-my $response = $agent->post($ENV{"ISABELLE_SMT_REMOTE_URL"}, [
-  "Solver" => $solver,
-  "Options" => join(" ", @options),
-  "Problem" => [$problem_file] ],
-  "Content_Type" => "form-data");
-if (not $response->is_success) { die "HTTP error: " . $response->message; }
-else { print $response->content; }
-
diff -r acefda71629b -r 327eafb594ba src/HOL/Tools/SMT/smt_setup_solvers.ML
--- a/src/HOL/Tools/SMT/smt_setup_solvers.ML	Sun Jan 19 11:05:38 2014 +0100
+++ b/src/HOL/Tools/SMT/smt_setup_solvers.ML	Sun Jan 19 22:38:17 2014 +0100
@@ -20,23 +20,9 @@
 
 (* helper functions *)
 
-val remote_prefix = "remote_"
-fun make_name is_remote name = name |> is_remote ? prefix remote_prefix
-
-fun make_local_avail name () = getenv (name ^ "_SOLVER") <> ""
-fun make_remote_avail name () = getenv (name ^ "_REMOTE_SOLVER") <> ""
-fun make_avail is_remote name =
-  if is_remote then make_remote_avail name
-  else make_local_avail name orf make_remote_avail name
+fun make_avail name () = getenv (name ^ "_SOLVER") <> ""
 
-fun make_local_command name () = [getenv (name ^ "_SOLVER")]
-fun make_remote_command name () =
-  [getenv "ISABELLE_SMT_REMOTE", getenv (name ^ "_REMOTE_SOLVER")]
-fun make_command is_remote name =
-  if is_remote then make_remote_command name
-  else (fn () =>
-    if make_local_avail name () then make_local_command name ()
-    else make_remote_command name ())
+fun make_command name () = [getenv (name ^ "_SOLVER")]
 
 fun outcome_of unsat sat unknown solver_name line =
   if String.isPrefix unsat line then SMT_Solver.Unsat
@@ -62,34 +48,31 @@
     "-seed", string_of_int (Config.get ctxt SMT_Config.random_seed),
     "-lang", "smtlib", "-output-lang", "presentation",
     "-timeout", string_of_int (Real.ceil (Config.get ctxt SMT_Config.timeout))]
-
-  fun mk is_remote = {
-    name = make_name is_remote "cvc3",
-    class = K SMTLIB_Interface.smtlibC,
-    avail = make_avail is_remote "CVC3",
-    command = make_command is_remote "CVC3",
-    options = cvc3_options,
-    default_max_relevant = 400 (* FUDGE *),
-    supports_filter = false,
-    outcome =
-      on_first_line (outcome_of "Unsatisfiable." "Satisfiable." "Unknown."),
-    cex_parser = NONE,
-    reconstruct = NONE }
 in
 
-fun cvc3 () = mk false
-fun remote_cvc3 () = mk true
+val cvc3: SMT_Solver.solver_config = {
+  name = "cvc3",
+  class = K SMTLIB_Interface.smtlibC,
+  avail = make_avail "CVC3",
+  command = make_command "CVC3",
+  options = cvc3_options,
+  default_max_relevant = 400 (* FUDGE *),
+  supports_filter = false,
+  outcome =
+    on_first_line (outcome_of "Unsatisfiable." "Satisfiable." "Unknown."),
+  cex_parser = NONE,
+  reconstruct = NONE }
 
 end
 
 
 (* Yices *)
 
-fun yices () = {
+val yices: SMT_Solver.solver_config = {
   name = "yices",
   class = K SMTLIB_Interface.smtlibC,
-  avail = make_local_avail "YICES",
-  command = make_local_command "YICES",
+  avail = make_avail "YICES",
+  command = make_command "YICES",
   options = (fn ctxt => [
     "--rand-seed=" ^ string_of_int (Config.get ctxt SMT_Config.random_seed),
     "--timeout=" ^
@@ -146,8 +129,7 @@
   Attrib.setup_config_bool @{binding z3_with_extensions} (K false)
 
 local
-  fun z3_make_command is_remote name () =
-    if_z3_non_commercial (make_command is_remote name)
+  fun z3_make_command name () = if_z3_non_commercial (make_command name)
 
   fun z3_options ctxt =
     ["-rs:" ^ string_of_int (Config.get ctxt SMT_Config.random_seed),
@@ -181,22 +163,19 @@
   fun select_class ctxt =
     if Config.get ctxt z3_with_extensions then Z3_Interface.smtlib_z3C
     else SMTLIB_Interface.smtlibC
-
-  fun mk is_remote = {
-    name = make_name is_remote "z3",
-    class = select_class,
-    avail = make_avail is_remote "Z3",
-    command = z3_make_command is_remote "Z3",
-    options = z3_options,
-    default_max_relevant = 350 (* FUDGE *),
-    supports_filter = true,
-    outcome = z3_on_first_or_last_line,
-    cex_parser = SOME Z3_Model.parse_counterex,
-    reconstruct = SOME Z3_Proof_Reconstruction.reconstruct }
 in
 
-fun z3 () = mk false
-fun remote_z3 () = mk true
+val z3: SMT_Solver.solver_config = {
+  name = "z3",
+  class = select_class,
+  avail = make_avail "Z3",
+  command = z3_make_command "Z3",
+  options = z3_options,
+  default_max_relevant = 350 (* FUDGE *),
+  supports_filter = true,
+  outcome = z3_on_first_or_last_line,
+  cex_parser = SOME Z3_Model.parse_counterex,
+  reconstruct = SOME Z3_Proof_Reconstruction.reconstruct }
 
 end
 
@@ -204,10 +183,8 @@
 (* overall setup *)
 
 val setup =
-  SMT_Solver.add_solver (cvc3 ()) #>
-  SMT_Solver.add_solver (remote_cvc3 ()) #>
-  SMT_Solver.add_solver (yices ()) #>
-  SMT_Solver.add_solver (z3 ()) #>
-  SMT_Solver.add_solver (remote_z3 ())
+  SMT_Solver.add_solver cvc3 #>
+  SMT_Solver.add_solver yices #>
+  SMT_Solver.add_solver z3
 
 end
diff -r acefda71629b -r 327eafb594ba src/HOL/Tools/etc/settings
--- a/src/HOL/Tools/etc/settings	Sun Jan 19 11:05:38 2014 +0100
+++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
@@ -1,5 +0,0 @@
-# -*- shell-script -*- :mode=shellscript:
-
-ISABELLE_SMT_REMOTE="$ISABELLE_HOME/src/HOL/Tools/SMT/lib/scripts/remote_smt"
-ISABELLE_SMT_REMOTE_URL="http://smt.in.tum.de/smt"
-