--- a/NEWS Sun Apr 22 16:32:26 2012 +0200
+++ b/NEWS Sun Apr 22 16:33:41 2012 +0200
@@ -5283,7 +5283,7 @@
* HOL/Nat: neq0_conv no longer declared as iff. INCOMPATIBILITY.
* HOL-Word: New extensive library and type for generic, fixed size
-machine words, with arithemtic, bit-wise, shifting and rotating
+machine words, with arithmetic, bit-wise, shifting and rotating
operations, reflection into int, nat, and bool lists, automation for
linear arithmetic (by automatic reflection into nat or int), including
lemmas on overflow and monotonicity. Instantiated to all appropriate
--- a/doc-src/Sledgehammer/sledgehammer.tex Sun Apr 22 16:32:26 2012 +0200
+++ b/doc-src/Sledgehammer/sledgehammer.tex Sun Apr 22 16:33:41 2012 +0200
@@ -95,7 +95,7 @@
and satisfiability-modulo-theories (SMT) solvers on the current goal.%
\footnote{The distinction between ATPs and SMT solvers is convenient but mostly
historical. The two communities are converging, with more and more ATPs
-supporting typical SMT features such as arithemtic and sorts, and a few SMT
+supporting typical SMT features such as arithmetic and sorts, and a few SMT
solvers parsing ATP syntaxes. There is also a strong technological connection
between instantiation-based ATPs (such as iProver and iProver-Eq) and SMT
solvers.}
--- a/src/HOL/TPTP/ATP_Problem_Import.thy Sun Apr 22 16:32:26 2012 +0200
+++ b/src/HOL/TPTP/ATP_Problem_Import.thy Sun Apr 22 16:33:41 2012 +0200
@@ -9,6 +9,8 @@
uses ("atp_problem_import.ML")
begin
+declare [[show_consts]] (* for Refute *)
+
typedecl iota (* for TPTP *)
use "atp_problem_import.ML"
--- a/src/HOL/TPTP/atp_problem_import.ML Sun Apr 22 16:32:26 2012 +0200
+++ b/src/HOL/TPTP/atp_problem_import.ML Sun Apr 22 16:33:41 2012 +0200
@@ -7,10 +7,10 @@
signature ATP_PROBLEM_IMPORT =
sig
- val isabelle_tptp_file : string -> unit
- val nitpick_tptp_file : string -> unit
- val refute_tptp_file : string -> unit
- val sledgehammer_tptp_file : string -> unit
+ val isabelle_tptp_file : int -> string -> unit
+ val nitpick_tptp_file : int -> string -> unit
+ val refute_tptp_file : int -> string -> unit
+ val sledgehammer_tptp_file : int -> string -> unit
val translate_tptp_file : string -> string -> string -> unit
end;
@@ -150,12 +150,12 @@
(** Isabelle (combination of provers) **)
-fun isabelle_tptp_file file_name = ()
+fun isabelle_tptp_file timeout file_name = ()
(** Nitpick (alias Nitrox) **)
-fun nitpick_tptp_file file_name =
+fun nitpick_tptp_file timeout file_name =
let
val (falsify, ts) = read_tptp_file @{theory} file_name
val state = Proof.init @{context}
@@ -172,8 +172,7 @@
("show_consts", "true"),
("format", "1000"),
("max_potential", "0"),
- ("timeout", "none"),
- ("expect", Nitpick.genuineN)]
+ ("timeout", string_of_int timeout)]
|> Nitpick_Isar.default_params @{theory}
val i = 1
val n = 1
@@ -195,13 +194,11 @@
"Unknown")
|> writeln
-fun refute_tptp_file file_name =
+fun refute_tptp_file timeout file_name =
let
val (falsify, ts) = read_tptp_file @{theory} file_name
val params =
- [("maxtime", "10000"),
- ("assms", "true"),
- ("expect", Nitpick.genuineN)]
+ [("maxtime", string_of_int timeout)]
in
Refute.refute_term @{context} params ts @{prop False}
|> print_szs_from_outcome falsify
@@ -210,7 +207,7 @@
(** Sledgehammer **)
-fun sledgehammer_tptp_file file_name = ()
+fun sledgehammer_tptp_file timeout file_name = ()
(** Translator between TPTP(-like) file formats **)
--- a/src/HOL/TPTP/lib/Tools/tptp_isabelle Sun Apr 22 16:32:26 2012 +0200
+++ b/src/HOL/TPTP/lib/Tools/tptp_isabelle Sun Apr 22 16:33:41 2012 +0200
@@ -9,9 +9,10 @@
function usage() {
echo
- echo "Usage: isabelle $PRG FILES"
+ echo "Usage: isabelle $PRG TIMEOUT FILES"
echo
echo " Runs a combination of Isabelle tactics on TPTP problems."
+ echo " Each problem is allocated at most TIMEOUT seconds."
echo
exit 1
}
@@ -20,10 +21,13 @@
SCRATCH="Scratch_${PRG}_$$_${RANDOM}"
+TIMEOUT=$1
+shift
+
for FILE in "$@"
do
echo "theory $SCRATCH imports \"$TPTP_HOME/ATP_Problem_Import\" begin \
-ML {* ATP_Problem_Import.isabelle_tptp_file \"$FILE\" *} end;" \
+ML {* ATP_Problem_Import.isabelle_tptp_file ($TIMEOUT) \"$FILE\" *} end;" \
> /tmp/$SCRATCH.thy
"$ISABELLE_PROCESS" -e "use_thy \"/tmp/$SCRATCH\"; exit 1;"
done
--- a/src/HOL/TPTP/lib/Tools/tptp_nitpick Sun Apr 22 16:32:26 2012 +0200
+++ b/src/HOL/TPTP/lib/Tools/tptp_nitpick Sun Apr 22 16:33:41 2012 +0200
@@ -9,9 +9,10 @@
function usage() {
echo
- echo "Usage: isabelle $PRG FILES"
+ echo "Usage: isabelle $PRG TIMEOUT FILES"
echo
echo " Runs Nitpick on TPTP problems."
+ echo " Each problem is allocated at most TIMEOUT seconds."
echo
exit 1
}
@@ -20,10 +21,13 @@
SCRATCH="Scratch_${PRG}_$$_${RANDOM}"
+TIMEOUT=$1
+shift
+
for FILE in "$@"
do
echo "theory $SCRATCH imports \"$TPTP_HOME/ATP_Problem_Import\" begin \
-ML {* ATP_Problem_Import.nitpick_tptp_file \"$FILE\" *} end;" \
+ML {* ATP_Problem_Import.nitpick_tptp_file ($TIMEOUT) \"$FILE\" *} end;" \
> /tmp/$SCRATCH.thy
"$ISABELLE_PROCESS" -e "use_thy \"/tmp/$SCRATCH\"; exit 1;"
done
--- a/src/HOL/TPTP/lib/Tools/tptp_refute Sun Apr 22 16:32:26 2012 +0200
+++ b/src/HOL/TPTP/lib/Tools/tptp_refute Sun Apr 22 16:33:41 2012 +0200
@@ -9,7 +9,7 @@
function usage() {
echo
- echo "Usage: isabelle $PRG FILES"
+ echo "Usage: isabelle $PRG TIMEOUT FILES"
echo
echo " Runs Refute on TPTP problems."
echo
@@ -20,10 +20,13 @@
SCRATCH="Scratch_${PRG}_$$_${RANDOM}"
+TIMEOUT=$1
+shift
+
for FILE in "$@"
do
echo "theory $SCRATCH imports \"$TPTP_HOME/ATP_Problem_Import\" begin \
-ML {* ATP_Problem_Import.refute_tptp_file \"$FILE\" *} end;" \
+ML {* ATP_Problem_Import.refute_tptp_file ($TIMEOUT) \"$FILE\" *} end;" \
> /tmp/$SCRATCH.thy
"$ISABELLE_PROCESS" -e "use_thy \"/tmp/$SCRATCH\"; exit 1;"
done
--- a/src/HOL/TPTP/lib/Tools/tptp_sledgehammer Sun Apr 22 16:32:26 2012 +0200
+++ b/src/HOL/TPTP/lib/Tools/tptp_sledgehammer Sun Apr 22 16:33:41 2012 +0200
@@ -9,9 +9,10 @@
function usage() {
echo
- echo "Usage: isabelle $PRG FILES"
+ echo "Usage: isabelle $PRG TIMEOUT FILES"
echo
echo " Runs Sledgehammer on TPTP problems."
+ echo " Each problem is allocated at most TIMEOUT seconds."
echo
exit 1
}
@@ -20,10 +21,13 @@
SCRATCH="Scratch_${PRG}_$$_${RANDOM}"
+TIMEOUT=$1
+shift
+
for FILE in "$@"
do
echo "theory $SCRATCH imports \"$TPTP_HOME/ATP_Problem_Import\" begin \
-ML {* ATP_Problem_Import.sledgehammer_tptp_file \"$FILE\" *} end;" \
+ML {* ATP_Problem_Import.sledgehammer_tptp_file ($TIMEOUT) \"$FILE\" *} end;" \
> /tmp/$SCRATCH.thy
"$ISABELLE_PROCESS" -e "use_thy \"/tmp/$SCRATCH\"; exit 1;"
done
--- a/src/HOL/Tools/ATP/atp_systems.ML Sun Apr 22 16:32:26 2012 +0200
+++ b/src/HOL/Tools/ATP/atp_systems.ML Sun Apr 22 16:33:41 2012 +0200
@@ -595,8 +595,8 @@
fun remote_atp name system_name system_versions proof_delims known_failures
conj_sym_kind prem_kind best_slice =
(remote_prefix ^ name,
- K (remote_config system_name system_versions proof_delims known_failures
- conj_sym_kind prem_kind best_slice))
+ fn () => remote_config system_name system_versions proof_delims known_failures
+ conj_sym_kind prem_kind best_slice)
fun remotify_atp (name, config) system_name system_versions best_slice =
(remote_prefix ^ name,
remotify_config system_name system_versions best_slice o config)
--- a/src/HOL/Tools/Nitpick/nitpick.ML Sun Apr 22 16:32:26 2012 +0200
+++ b/src/HOL/Tools/Nitpick/nitpick.ML Sun Apr 22 16:33:41 2012 +0200
@@ -1048,7 +1048,10 @@
fun pick_nits_in_term state (params as {debug, timeout, expect, ...}) mode i n
step subst assm_ts orig_t =
- let val print_nt = if is_mode_nt mode then Output.urgent_message else K () in
+ let
+ val print_nt = if is_mode_nt mode then Output.urgent_message else K ()
+ val print_t = if mode = TPTP then Output.urgent_message else K ()
+ in
if getenv "KODKODI" = "" then
(* The "expect" argument is deliberately ignored if Kodkodi is missing so
that the "Nitpick_Examples" can be processed on any machine. *)
@@ -1064,14 +1067,18 @@
(pick_them_nits_in_term deadline state params mode i n step subst
assm_ts) orig_t
handle TOO_LARGE (_, details) =>
- (print_nt ("Limit reached: " ^ details ^ "."); unknown_outcome)
+ (print_t "% SZS status Unknown";
+ print_nt ("Limit reached: " ^ details ^ "."); unknown_outcome)
| TOO_SMALL (_, details) =>
- (print_nt ("Limit reached: " ^ details ^ "."); unknown_outcome)
+ (print_t "% SZS status Unknown";
+ print_nt ("Limit reached: " ^ details ^ "."); unknown_outcome)
| Kodkod.SYNTAX (_, details) =>
- (print_nt ("Malformed Kodkodi output: " ^ details ^ ".");
+ (print_t "% SZS status Unknown";
+ print_nt ("Malformed Kodkodi output: " ^ details ^ ".");
unknown_outcome)
| TimeLimit.TimeOut =>
- (print_nt "Nitpick ran out of time."; unknown_outcome)
+ (print_t "% SZS status TimedOut";
+ print_nt "Nitpick ran out of time."; unknown_outcome)
in
if expect = "" orelse outcome_code = expect then outcome
else error ("Unexpected outcome: " ^ quote outcome_code ^ ".")
--- a/src/HOL/Tools/Nitpick/nitpick_hol.ML Sun Apr 22 16:32:26 2012 +0200
+++ b/src/HOL/Tools/Nitpick/nitpick_hol.ML Sun Apr 22 16:33:41 2012 +0200
@@ -996,6 +996,7 @@
in
if k1 = max orelse k2 = max then max
else Int.min (max, reasonable_power k2 k1)
+ handle TOO_LARGE _ => max
end
| bounded_card_of_type max default_card assigns
(Type (@{type_name prod}, [T1, T2])) =
--- a/src/HOL/Tools/Nitpick/nitpick_preproc.ML Sun Apr 22 16:32:26 2012 +0200
+++ b/src/HOL/Tools/Nitpick/nitpick_preproc.ML Sun Apr 22 16:33:41 2012 +0200
@@ -867,20 +867,21 @@
fun defined_free_by_assumption t =
let
- fun do_equals x def =
- if exists_subterm (curry (op aconv) (Free x)) def then NONE else SOME x
+ fun do_equals u def =
+ if exists_subterm (curry (op aconv) u) def then NONE else SOME u
in
case t of
- Const (@{const_name "=="}, _) $ Free x $ def => do_equals x def
- | @{const Trueprop} $ (Const (@{const_name "=="}, _) $ Free x $ def) =>
- do_equals x def
+ Const (@{const_name "=="}, _) $ (u as Free _) $ def => do_equals u def
+ | @{const Trueprop}
+ $ (Const (@{const_name HOL.eq}, _) $ (u as Free _) $ def) =>
+ do_equals u def
| _ => NONE
end
fun assumption_exclusively_defines_free assm_ts t =
case defined_free_by_assumption t of
- SOME x =>
- length (filter ((fn SOME x' => x = x' | NONE => false)
+ SOME u =>
+ length (filter ((fn SOME u' => u aconv u' | NONE => false)
o defined_free_by_assumption) assm_ts) = 1
| NONE => false
@@ -994,10 +995,10 @@
(nondef_props_for_const thy false nondef_table x)
end)
|> add_axioms_for_type depth T
- | Free (x as (_, T)) =>
+ | Free (_, T) =>
(if member (op aconv) seen t then
accum
- else case AList.lookup (op =) def_assm_table x of
+ else case AList.lookup (op =) def_assm_table t of
SOME t => add_def_axiom depth t accum
| NONE => accum)
|> add_axioms_for_type depth T
--- a/src/HOL/Tools/Nitpick/nitpick_util.ML Sun Apr 22 16:32:26 2012 +0200
+++ b/src/HOL/Tools/Nitpick/nitpick_util.ML Sun Apr 22 16:33:41 2012 +0200
@@ -118,7 +118,8 @@
"negative exponent (" ^ signed_string_of_int b ^ ")")
else if b > max_exponent then
raise TOO_LARGE ("Nitpick_Util.reasonable_power",
- "too large exponent (" ^ signed_string_of_int b ^ ")")
+ "too large exponent (" ^ signed_string_of_int a ^ " ^ " ^
+ signed_string_of_int b ^ ")")
else
let val c = reasonable_power a (b div 2) in
c * c * reasonable_power a (b mod 2)