isabelle: src/HOL/Tools/SMT2/smt2_failure.ML@276befcd90d9 (annotated)

56078 624faeda77b5 moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle blanchet parents: diff changeset	1	(* Title: HOL/Tools/SMT2/smt2_failure.ML
624faeda77b5 moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle blanchet parents: diff changeset	2	Author: Sascha Boehme, TU Muenchen
624faeda77b5 moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle blanchet parents: diff changeset	3
624faeda77b5 moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle blanchet parents: diff changeset	4	Failures and exception of SMT.
624faeda77b5 moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle blanchet parents: diff changeset	5	*)
624faeda77b5 moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle blanchet parents: diff changeset	6
624faeda77b5 moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle blanchet parents: diff changeset	7	signature SMT2_FAILURE =
624faeda77b5 moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle blanchet parents: diff changeset	8	sig
624faeda77b5 moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle blanchet parents: diff changeset	9	datatype failure =
57158 f028d93798e6 simplified counterexample handling blanchet parents: 56078 diff changeset	10	Counterexample of bool \|
56078 624faeda77b5 moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle blanchet parents: diff changeset	11	Time_Out \|
624faeda77b5 moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle blanchet parents: diff changeset	12	Out_Of_Memory \|
624faeda77b5 moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle blanchet parents: diff changeset	13	Abnormal_Termination of int \|
624faeda77b5 moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle blanchet parents: diff changeset	14	Other_Failure of string
57158 f028d93798e6 simplified counterexample handling blanchet parents: 56078 diff changeset	15	val string_of_failure: failure -> string
56078 624faeda77b5 moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle blanchet parents: diff changeset	16	exception SMT of failure
624faeda77b5 moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle blanchet parents: diff changeset	17	end
624faeda77b5 moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle blanchet parents: diff changeset	18
624faeda77b5 moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle blanchet parents: diff changeset	19	structure SMT2_Failure: SMT2_FAILURE =
624faeda77b5 moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle blanchet parents: diff changeset	20	struct
624faeda77b5 moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle blanchet parents: diff changeset	21
624faeda77b5 moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle blanchet parents: diff changeset	22	datatype failure =
57158 f028d93798e6 simplified counterexample handling blanchet parents: 56078 diff changeset	23	Counterexample of bool \|
56078 624faeda77b5 moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle blanchet parents: diff changeset	24	Time_Out \|
624faeda77b5 moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle blanchet parents: diff changeset	25	Out_Of_Memory \|
624faeda77b5 moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle blanchet parents: diff changeset	26	Abnormal_Termination of int \|
624faeda77b5 moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle blanchet parents: diff changeset	27	Other_Failure of string
624faeda77b5 moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle blanchet parents: diff changeset	28
57158 f028d93798e6 simplified counterexample handling blanchet parents: 56078 diff changeset	29	fun string_of_failure (Counterexample genuine) =
f028d93798e6 simplified counterexample handling blanchet parents: 56078 diff changeset	30	if genuine then "Counterexample found (possibly spurious)"
56078 624faeda77b5 moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle blanchet parents: diff changeset	31	else "Potential counterexample found"
57158 f028d93798e6 simplified counterexample handling blanchet parents: 56078 diff changeset	32	\| string_of_failure Time_Out = "Timed out"
f028d93798e6 simplified counterexample handling blanchet parents: 56078 diff changeset	33	\| string_of_failure Out_Of_Memory = "Ran out of memory"
f028d93798e6 simplified counterexample handling blanchet parents: 56078 diff changeset	34	\| string_of_failure (Abnormal_Termination err) =
56078 624faeda77b5 moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle blanchet parents: diff changeset	35	"Solver terminated abnormally with error code " ^ string_of_int err
57158 f028d93798e6 simplified counterexample handling blanchet parents: 56078 diff changeset	36	\| string_of_failure (Other_Failure msg) = msg
56078 624faeda77b5 moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle blanchet parents: diff changeset	37
624faeda77b5 moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle blanchet parents: diff changeset	38	exception SMT of failure
624faeda77b5 moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle blanchet parents: diff changeset	39
624faeda77b5 moved 'SMT2' (SMT-LIB-2-based SMT module) into Isabelle blanchet parents: diff changeset	40	end

author	nipkow
	Fri, 06 Jun 2014 10:53:33 +0200
changeset 57178	276befcd90d9
parent 57158	f028d93798e6
child 57229	489083abce44
permissions	-rw-r--r--