--- a/NEWS Sun Mar 15 16:02:22 2009 +0100
+++ b/NEWS Sun Mar 15 16:59:17 2009 +0100
@@ -335,10 +335,9 @@
commands are covered in the isar-ref manual.
* Wrapper scripts for remote SystemOnTPTP service allows to use
-sledgehammer without local ATP installation (Vampire etc.). See also
-ISABELLE_HOME/contrib/SystemOnTPTP and the VAMPIRE_HOME setting
-variable. Other provers may be included via suitable ML wrappers, see
-also src/HOL/ATP_Linkup.thy.
+sledgehammer without local ATP installation (Vampire etc.). Other
+provers may be included via suitable ML wrappers, see also
+src/HOL/ATP_Linkup.thy.
* Normalization by evaluation now allows non-leftlinear equations.
Declare with attribute [code nbe].
--- a/contrib/SystemOnTPTP/remote Sun Mar 15 16:02:22 2009 +0100
+++ b/contrib/SystemOnTPTP/remote Sun Mar 15 16:59:17 2009 +0100
@@ -21,16 +21,6 @@
"ProblemSource" => "UPLOAD",
);
-# check connection
-my $TestAgent = LWP::UserAgent->new;
-$TestAgent->timeout(5);
-my $TestRequest = GET($SystemOnTPTPFormReplyURL);
-my $TestResponse = $TestAgent->request($TestRequest);
-if(! $TestResponse->is_success) {
- print "HTTP-Error: " . $TestResponse->message . "\n";
- exit(-1);
-}
-
#----Get format and transform options if specified
my %Options;
getopts("hws:t:c:",\%Options);
@@ -85,7 +75,7 @@
my $Agent = LWP::UserAgent->new;
if (exists($Options{'t'})) {
# give server more time to respond
- $Agent->timeout($Options{'t'} * 2 + 10);
+ $Agent->timeout($Options{'t'} + 10);
}
my $Request = POST($SystemOnTPTPFormReplyURL,
Content_Type => 'form-data',Content => \%URLParameters);
@@ -93,17 +83,13 @@
#catch errors / failure
if(! $Response->is_success){
- print "HTTP-Error: " . $Response->message . "\n";
- exit(-1);
+ print "HTTP-Error: " . $Response->message . "\n";
+ exit(-1);
} elsif (exists($Options{'w'})) {
print $Response->content;
exit (0);
} elsif ($Response->content =~ /NO SOLUTION OUTPUT BY SYSTEM/){
- if ($Response->content =~ /%\s*Result\s*:(.*)\n%\s*Output\s*:(.*)\n%/) {
- print "No Solution Output\nResult: $1\nOutput: $2\n";
- } else {
- print "No Solution Output\n";
- }
+ print "No Solution Output by System\n";
exit(-1);
} elsif ($Response->content =~ /ERROR: Could not form TPTP format derivation/) {
print "Could not form TPTP format derivation\n";
--- a/src/HOL/Tools/atp_manager.ML Sun Mar 15 16:02:22 2009 +0100
+++ b/src/HOL/Tools/atp_manager.ML Sun Mar 15 16:59:17 2009 +0100
@@ -19,7 +19,7 @@
val kill: unit -> unit
val info: unit -> unit
val messages: int option -> unit
- type prover = int -> int -> Proof.state -> bool * string
+ type prover = int -> int -> Proof.context * (thm list * thm) -> bool * string
val add_prover: string -> prover -> theory -> theory
val print_provers: theory -> unit
val sledgehammer: string list -> Proof.state -> unit
@@ -271,7 +271,7 @@
(* named provers *)
-type prover = int -> int -> Proof.state -> bool * string;
+type prover = int -> int -> Proof.context * (thm list * thm) -> bool * string;
fun err_dup_prover name = error ("Duplicate prover: " ^ quote name);
@@ -307,7 +307,7 @@
val _ = SimpleThread.fork true (fn () =>
let
val _ = register birthtime deadtime (Thread.self (), desc)
- val result = prover (get_timeout ()) i proof_state
+ val result = prover (get_timeout ()) i (Proof.get_goal proof_state)
handle ResHolClause.TOO_TRIVIAL
=> (true, "Empty clause: Try this command: " ^ Markup.markup Markup.sendback "apply metis")
| ERROR msg
@@ -360,3 +360,4 @@
end;
end;
+
--- a/src/HOL/Tools/atp_wrapper.ML Sun Mar 15 16:02:22 2009 +0100
+++ b/src/HOL/Tools/atp_wrapper.ML Sun Mar 15 16:59:17 2009 +0100
@@ -10,9 +10,9 @@
val destdir: string ref
val problem_name: string ref
val external_prover:
- ((int -> Path.T) -> Proof.context * thm list * thm -> string list * ResHolClause.axiom_name Vector.vector list) ->
- Path.T * string ->
- (string -> string option) ->
+ (thm * (string * int)) list ->
+ (Path.T -> thm -> int -> (thm * (string * int)) list -> theory -> string vector) ->
+ Path.T * string -> (string -> string option) ->
(string * string vector * Proof.context * thm * int -> string) ->
AtpManager.prover
val tptp_prover_opts_full: int -> bool -> bool -> Path.T * string -> AtpManager.prover
@@ -47,7 +47,7 @@
(* basic template *)
-fun external_prover write_problem_files (cmd, args) find_failure produce_answer timeout subgoalno state =
+fun external_prover axiom_clauses write_problem_file (cmd, args) find_failure produce_answer timeout subgoalno goal =
let
(* path to unique problem file *)
val destdir' = ! destdir
@@ -61,25 +61,28 @@
end
(* write out problem file and call prover *)
- val (ctxt, (chain_ths, goal)) = Proof.get_goal state
+ val (ctxt, (chain_ths, th)) = goal
+ val thy = ProofContext.theory_of ctxt
val chain_ths = map (Thm.put_name_hint ResReconstruct.chained_hint) chain_ths
- val (filenames, thm_names_list) = write_problem_files prob_pathname (ctxt, chain_ths, goal)
- val thm_names = nth thm_names_list (subgoalno - 1)
-
+ val probfile = prob_pathname subgoalno
+ val fname = File.platform_path probfile
+ val thm_names = write_problem_file probfile th subgoalno axiom_clauses thy
val cmdline =
if File.exists cmd then File.shell_path cmd ^ " " ^ args
else error ("Bad executable: " ^ Path.implode cmd)
- val (proof, rc) = system_out (cmdline ^ " " ^ nth filenames (subgoalno - 1))
+ val (proof, rc) = system_out (cmdline ^ " " ^ fname)
(* remove *temporary* files *)
- val _ = if destdir' = "" then List.app OS.FileSys.remove filenames else ()
+ val _ = if destdir' = "" then OS.FileSys.remove fname else ()
(* check for success and print out some information on failure *)
val failure = find_failure proof
val success = rc = 0 andalso is_none failure
val message =
- if success then "Try this command: " ^ produce_answer (proof, thm_names, ctxt, goal, subgoalno)
- else "Could not prove goal."
+ if isSome failure then "Proof attempt failed."
+ else if rc <> 0 then "Proof attempt failed: " ^ proof
+ else "Try this command: " ^ produce_answer (proof, thm_names, ctxt, th, subgoalno)
+
val _ = if isSome failure
then Output.debug (fn () => "Sledgehammer failure: " ^ the failure ^ "\nOutput: " ^ proof)
else ()
@@ -94,12 +97,14 @@
(* generic TPTP-based provers *)
-fun tptp_prover_opts_full max_new theory_const full command =
+fun tptp_prover_opts_full max_new theory_const full command timeout n goal =
external_prover
- (ResAtp.write_problem_files false max_new theory_const)
+ (ResAtp.get_relevant max_new theory_const goal n)
+ (ResAtp.write_problem_file false)
command
ResReconstruct.find_failure_e_vamp_spass
- (if full then ResReconstruct.structured_proof else ResReconstruct.lemma_list_tstp);
+ (if full then ResReconstruct.structured_proof else ResReconstruct.lemma_list_tstp)
+ timeout n goal;
(*arbitrary ATP with TPTP input/output and problemfile as last argument*)
fun tptp_prover_opts max_new theory_const =
@@ -137,26 +142,33 @@
(* E prover *)
-fun eprover_opts max_new theory_const = tptp_prover_opts
+fun eprover_opts max_new theory_const timeout = tptp_prover_opts
max_new theory_const
- (Path.explode "$E_HOME/eproof", "--tstp-in --tstp-out -l5 -xAutoDev -tAutoDev --silent");
+ (Path.explode "$E_HOME/eproof",
+ "--tstp-in --tstp-out -l5 -xAutoDev -tAutoDev --silent --cpu-limit=" ^ string_of_int timeout)
+ timeout;
val eprover = eprover_opts 100 false;
-fun eprover_opts_full max_new theory_const = full_prover_opts
+fun eprover_opts_full max_new theory_const timeout = full_prover_opts
max_new theory_const
- (Path.explode "$E_HOME/eproof", "--tstp-in --tstp-out -l5 -xAutoDev -tAutoDev --silent");
+ (Path.explode "$E_HOME/eproof",
+ "--tstp-in --tstp-out -l5 -xAutoDev -tAutoDev --silent --cpu-limit=" ^ string_of_int timeout)
+ timeout;
val eprover_full = eprover_opts_full 100 false;
(* SPASS *)
-fun spass_opts max_new theory_const = external_prover
- (ResAtp.write_problem_files true max_new theory_const)
- (Path.explode "$SPASS_HOME/SPASS", "-Auto -SOS=1 -PGiven=0 -PProblem=0 -Splits=0 -FullRed=0 -DocProof")
+fun spass_opts max_new theory_const timeout n goal = external_prover
+ (ResAtp.get_relevant max_new theory_const goal n)
+ (ResAtp.write_problem_file true)
+ (Path.explode "$SPASS_HOME/SPASS",
+ "-Auto -SOS=1 -PGiven=0 -PProblem=0 -Splits=0 -FullRed=0 -DocProof -TimeLimit=" ^ string_of_int timeout)
ResReconstruct.find_failure_e_vamp_spass
- ResReconstruct.lemma_list_dfg;
+ ResReconstruct.lemma_list_dfg
+ timeout n goal;
val spass = spass_opts 40 true;
@@ -165,9 +177,11 @@
fun remote_prover_opts max_new theory_const args timeout =
tptp_prover_opts max_new theory_const
- (Path.explode "$ISABELLE_HOME/contrib/SystemOnTPTP/remote", args ^ " -t " ^ string_of_int timeout)
+ (Path.explode "$ISABELLE_HOME/contrib/SystemOnTPTP/remote", args ^ " -t " ^ string_of_int (timeout - 10))
timeout;
val remote_prover = remote_prover_opts 60 false;
end;
+
+
--- a/src/HOL/Tools/res_atp.ML Sun Mar 15 16:02:22 2009 +0100
+++ b/src/HOL/Tools/res_atp.ML Sun Mar 15 16:59:17 2009 +0100
@@ -6,9 +6,10 @@
val tvar_classes_of_terms : term list -> string list
val tfree_classes_of_terms : term list -> string list
val type_consts_of_terms : theory -> term list -> string list
- val write_problem_files : bool -> int -> bool
- -> (int -> Path.T) -> Proof.context * thm list * thm
- -> string list * ResHolClause.axiom_name Vector.vector list
+ val get_relevant : int -> bool -> Proof.context * (thm list * thm) -> int
+ -> (thm * (string * int)) list
+ val write_problem_file : bool -> Path.T -> thm -> int -> (thm * (string * int)) list -> theory
+ -> string vector
end;
structure ResAtp: RES_ATP =
@@ -510,54 +511,51 @@
likely to lead to unsound proofs.*)
fun remove_unwanted_clauses cls = filter (not o unwanted o prop_of o fst) cls;
-(* TODO: problem file for *one* subgoal would be sufficient *)
-(*Write out problem files for each subgoal.
- Argument probfile generates filenames from subgoal-number
- Arguments max_new and theory_const are booleans controlling relevance_filter
- (necessary for different provers)
-*)
-fun write_problem_files dfg max_new theory_const probfile (ctxt, chain_ths, th) =
- let val goals = Thm.prems_of th
- val thy = ProofContext.theory_of ctxt
- fun get_neg_subgoals [] _ = []
- | get_neg_subgoals (gl::gls) n = #1 (ResAxioms.neg_conjecture_clauses th n) ::
- get_neg_subgoals gls (n+1)
- val goal_cls = get_neg_subgoals goals 1
- handle THM ("assume: variables", _, _) =>
- error "Sledgehammer: Goal contains type variables (TVars)"
- val isFO = case linkup_logic_mode of
- Auto => forall (Meson.is_fol_term thy) (map prop_of (List.concat goal_cls))
- | Fol => true
- | Hol => false
- val (included_thms,white_thms) = get_clasimp_atp_lemmas ctxt chain_ths
- val included_cls = included_thms |> ResAxioms.cnf_rules_pairs thy |> make_unique
- |> restrict_to_logic thy isFO
- |> remove_unwanted_clauses
- val white_cls = ResAxioms.cnf_rules_pairs thy white_thms
- (*clauses relevant to goal gl*)
- val axcls_list = map (fn ngcls => white_cls @ relevance_filter max_new theory_const thy included_cls (map prop_of ngcls)) goal_cls
- val writer = if dfg then ResHolClause.dfg_write_file else ResHolClause.tptp_write_file
- fun write_all [] [] _ = []
- | write_all (ccls::ccls_list) (axcls::axcls_list) k =
- let val fname = File.platform_path (probfile k)
- val axcls = make_unique axcls
- val _ = app (fn th => Output.debug (fn _ => Display.string_of_thm th)) ccls
- val ccls = subtract_cls ccls axcls
- val _ = app (fn th => Output.debug (fn _ => Display.string_of_thm th)) ccls
- val ccltms = map prop_of ccls
- and axtms = map (prop_of o #1) axcls
- val subs = tfree_classes_of_terms ccltms
- and supers = tvar_classes_of_terms axtms
- and tycons = type_consts_of_terms thy (ccltms@axtms)
- (*TFrees in conjecture clauses; TVars in axiom clauses*)
- val (supers',arity_clauses) = ResClause.make_arity_clauses_dfg dfg thy tycons supers
- val classrel_clauses = ResClause.make_classrel_clauses thy subs supers'
- val clnames = writer thy isFO ccls fname (axcls,classrel_clauses,arity_clauses) []
- val thm_names = Vector.fromList clnames
- in (thm_names,fname) :: write_all ccls_list axcls_list (k+1) end
- val (thm_names_list, filenames) = ListPair.unzip (write_all goal_cls axcls_list 1)
+fun isFO thy goal_cls = case linkup_logic_mode of
+ Auto => forall (Meson.is_fol_term thy) (map prop_of goal_cls)
+ | Fol => true
+ | Hol => false
+
+fun get_relevant max_new theory_const (ctxt, (chain_ths, th)) n =
+ let
+ val thy = ProofContext.theory_of ctxt
+ val goal_cls = #1 (ResAxioms.neg_conjecture_clauses th n)
+ handle THM ("assume: variables", _, _) =>
+ error "Sledgehammer: Goal contains type variables (TVars)"
+ val (included_thms,white_thms) = get_clasimp_atp_lemmas ctxt chain_ths
+ val included_cls = included_thms |> ResAxioms.cnf_rules_pairs thy |> make_unique
+ |> restrict_to_logic thy (isFO thy goal_cls)
+ |> remove_unwanted_clauses
+ val white_cls = ResAxioms.cnf_rules_pairs thy white_thms
+ (*clauses relevant to goal gl*)
in
- (filenames, thm_names_list)
+ white_cls @ relevance_filter max_new theory_const thy included_cls (map prop_of goal_cls)
+ end;
+
+(* Write out problem file *)
+fun write_problem_file dfg probfile goal n axcls thy =
+ let val writer = if dfg then ResHolClause.dfg_write_file else ResHolClause.tptp_write_file
+ val fname = File.platform_path probfile
+ val axcls = make_unique axcls
+ val goal_cls = #1 (ResAxioms.neg_conjecture_clauses goal n)
+ handle THM ("assume: variables", _, _) =>
+ error "Sledgehammer: Goal contains type variables (TVars)"
+ val _ = app (fn th => Output.debug (fn _ => Display.string_of_thm th)) goal_cls
+ val ccls = subtract_cls goal_cls axcls
+ val _ = app (fn th => Output.debug (fn _ => Display.string_of_thm th)) ccls
+ val ccltms = map prop_of ccls
+ and axtms = map (prop_of o #1) axcls
+ val subs = tfree_classes_of_terms ccltms
+ and supers = tvar_classes_of_terms axtms
+ and tycons = type_consts_of_terms thy (ccltms@axtms)
+ (*TFrees in conjecture clauses; TVars in axiom clauses*)
+ val (supers',arity_clauses) = ResClause.make_arity_clauses_dfg dfg thy tycons supers
+ val classrel_clauses = ResClause.make_classrel_clauses thy subs supers'
+ val clnames = writer thy (isFO thy goal_cls) ccls fname (axcls,classrel_clauses,arity_clauses) []
+ in
+ Vector.fromList clnames
end;
end;
+
+