--- 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.
--- 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
--- 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
--- 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; }
-
--- 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
--- 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"
-