isabelle: src/HOL/Tools/Sledgehammer/sledgehammer_reconstructor.ML@a510fc40559c (annotated)

52590 02713cd2c2cd tuned smolkas parents: 52555 diff changeset	1	(* Title: HOL/Tools/Sledgehammer/sledgehammer_reconstructor.ML
52555 6811291d1869 moved code -> easier debugging smolkas parents: diff changeset	2	Author: Jasmin Blanchette, TU Muenchen
6811291d1869 moved code -> easier debugging smolkas parents: diff changeset	3	Author: Steffen Juilf Smolka, TU Muenchen
6811291d1869 moved code -> easier debugging smolkas parents: diff changeset	4
6811291d1869 moved code -> easier debugging smolkas parents: diff changeset	5	Reconstructors.
6811291d1869 moved code -> easier debugging smolkas parents: diff changeset	6	*)
6811291d1869 moved code -> easier debugging smolkas parents: diff changeset	7
6811291d1869 moved code -> easier debugging smolkas parents: diff changeset	8	signature SLEDGEHAMMER_RECONSTRUCTOR =
6811291d1869 moved code -> easier debugging smolkas parents: diff changeset	9	sig
6811291d1869 moved code -> easier debugging smolkas parents: diff changeset	10	type stature = ATP_Problem_Generate.stature
6811291d1869 moved code -> easier debugging smolkas parents: diff changeset	11
6811291d1869 moved code -> easier debugging smolkas parents: diff changeset	12	datatype reconstructor =
6811291d1869 moved code -> easier debugging smolkas parents: diff changeset	13	Metis of string * string \|
6811291d1869 moved code -> easier debugging smolkas parents: diff changeset	14	SMT
6811291d1869 moved code -> easier debugging smolkas parents: diff changeset	15
6811291d1869 moved code -> easier debugging smolkas parents: diff changeset	16	datatype play =
6811291d1869 moved code -> easier debugging smolkas parents: diff changeset	17	Played of reconstructor * Time.time \|
54823 a510fc40559c distinguish not preplayed & timed out blanchet parents: 54815 diff changeset	18	Not_Played of reconstructor \|
54815 4f6ec8754bf5 simplified data structure blanchet parents: 54813 diff changeset	19	Play_Timed_Out of reconstructor * Time.time \|
54813 c8b04da1bd01 tuning blanchet parents: 54772 diff changeset	20	Play_Failed of reconstructor
52555 6811291d1869 moved code -> easier debugging smolkas parents: diff changeset	21
6811291d1869 moved code -> easier debugging smolkas parents: diff changeset	22	type minimize_command = string list -> string
54772 f5fd4a34b0e8 handle Skolems gracefully for SPASS as well blanchet parents: 54495 diff changeset	23	type one_line_params = play * string * (string * stature) list * minimize_command * int * int
52555 6811291d1869 moved code -> easier debugging smolkas parents: diff changeset	24
6811291d1869 moved code -> easier debugging smolkas parents: diff changeset	25	val smtN : string
54495 237d5be57277 refactored blanchet parents: 52590 diff changeset	26	end;
52555 6811291d1869 moved code -> easier debugging smolkas parents: diff changeset	27
6811291d1869 moved code -> easier debugging smolkas parents: diff changeset	28	structure Sledgehammer_Reconstructor : SLEDGEHAMMER_RECONSTRUCTOR =
6811291d1869 moved code -> easier debugging smolkas parents: diff changeset	29	struct
6811291d1869 moved code -> easier debugging smolkas parents: diff changeset	30
6811291d1869 moved code -> easier debugging smolkas parents: diff changeset	31	open ATP_Problem_Generate
6811291d1869 moved code -> easier debugging smolkas parents: diff changeset	32
6811291d1869 moved code -> easier debugging smolkas parents: diff changeset	33	datatype reconstructor =
6811291d1869 moved code -> easier debugging smolkas parents: diff changeset	34	Metis of string * string \|
6811291d1869 moved code -> easier debugging smolkas parents: diff changeset	35	SMT
6811291d1869 moved code -> easier debugging smolkas parents: diff changeset	36
6811291d1869 moved code -> easier debugging smolkas parents: diff changeset	37	datatype play =
6811291d1869 moved code -> easier debugging smolkas parents: diff changeset	38	Played of reconstructor * Time.time \|
54823 a510fc40559c distinguish not preplayed & timed out blanchet parents: 54815 diff changeset	39	Not_Played of reconstructor \|
54815 4f6ec8754bf5 simplified data structure blanchet parents: 54813 diff changeset	40	Play_Timed_Out of reconstructor * Time.time \|
54813 c8b04da1bd01 tuning blanchet parents: 54772 diff changeset	41	Play_Failed of reconstructor
52555 6811291d1869 moved code -> easier debugging smolkas parents: diff changeset	42
6811291d1869 moved code -> easier debugging smolkas parents: diff changeset	43	type minimize_command = string list -> string
54772 f5fd4a34b0e8 handle Skolems gracefully for SPASS as well blanchet parents: 54495 diff changeset	44	type one_line_params = play * string * (string * stature) list * minimize_command * int * int
52555 6811291d1869 moved code -> easier debugging smolkas parents: diff changeset	45
6811291d1869 moved code -> easier debugging smolkas parents: diff changeset	46	val smtN = "smt"
6811291d1869 moved code -> easier debugging smolkas parents: diff changeset	47
54495 237d5be57277 refactored blanchet parents: 52590 diff changeset	48	end;

author	blanchet
	Thu, 19 Dec 2013 17:24:17 +0100
changeset 54823	a510fc40559c
parent 54815	4f6ec8754bf5
child 54824	4e58a38b330b
permissions	-rw-r--r--