linarith counterexamples now provide only valuations for variables (which should restrict the number of linarith trace messages);
control tracing of (potentially spurious) counterexamples by the configuration option "linarith_verbose" (to disable linarith traces entirely)
--- a/src/HOL/Tools/lin_arith.ML Tue Jun 28 10:52:15 2011 +0200
+++ b/src/HOL/Tools/lin_arith.ML Wed Jun 29 11:58:35 2011 +0200
@@ -21,6 +21,7 @@
val global_setup: theory -> theory
val split_limit: int Config.T
val neq_limit: int Config.T
+ val verbose: bool Config.T
val trace: bool Unsynchronized.ref
end;
@@ -101,12 +102,14 @@
val split_limit = Attrib.setup_config_int @{binding linarith_split_limit} (K 9);
val neq_limit = Attrib.setup_config_int @{binding linarith_neq_limit} (K 9);
+val verbose = Attrib.setup_config_bool @{binding linarith_verbose} (K true);
structure LA_Data =
struct
val fast_arith_neq_limit = neq_limit;
+val fast_arith_verbose = verbose;
(* Decomposition of terms *)
--- a/src/HOL/Tools/try_methods.ML Tue Jun 28 10:52:15 2011 +0200
+++ b/src/HOL/Tools/try_methods.ML Wed Jun 29 11:58:35 2011 +0200
@@ -113,7 +113,8 @@
fun do_try_methods mode timeout_opt quad st =
let
- val st = st |> Proof.map_context (Config.put Metis_Tactics.verbose false)
+ val st = st |> Proof.map_context (Config.put Metis_Tactics.verbose false #>
+ Config.put Lin_Arith.verbose false)
in
if mode = Normal then
"Trying " ^ space_implode " " (Try.serial_commas "and"
--- a/src/Provers/Arith/fast_lin_arith.ML Tue Jun 28 10:52:15 2011 +0200
+++ b/src/Provers/Arith/fast_lin_arith.ML Wed Jun 29 11:58:35 2011 +0200
@@ -60,6 +60,9 @@
(*the limit on the number of ~= allowed; because each ~= is split
into two cases, this can lead to an explosion*)
val fast_arith_neq_limit: int Config.T
+
+ (*configures whether (potentially spurious) counterexamples are printed*)
+ val fast_arith_verbose: bool Config.T
end;
(*
decomp(`x Rel y') should yield (p,i,Rel,q,j,d)
@@ -612,11 +615,10 @@
else string_of_int p ^ "/" ^ string_of_int q
in a ^ " = " ^ s end;
-fun produce_ex sds =
- curry (op ~~) sds
- #> map print_atom
- #> commas
- #> curry (op ^) "Counterexample (possibly spurious):\n";
+fun is_variable (Free _) = true
+ | is_variable (Var _) = true
+ | is_variable (Bound _) = true
+ | is_variable _ = false
fun trace_ex ctxt params atoms discr n (hist: history) =
case hist of
@@ -628,8 +630,15 @@
val start =
if v = ~1 then (hist', findex0 discr n lineqs)
else (hist, replicate n Rat.zero)
- val ex = SOME (produce_ex (map show_term atoms ~~ discr)
- (uncurry (fold (findex1 discr)) start))
+ val produce_ex =
+ map print_atom #> commas #>
+ prefix "Counterexample (possibly spurious):\n"
+ val ex = (
+ uncurry (fold (findex1 discr)) start
+ |> map2 pair (atoms ~~ discr)
+ |> filter (fn ((t, _), _) => is_variable t)
+ |> map (apfst (apfst show_term))
+ |> (fn [] => NONE | sdss => SOME (produce_ex sdss)))
handle NoEx => NONE
in
case ex of
@@ -744,7 +753,7 @@
(trace_msg ("Contradiction! (" ^ string_of_int (length js + 1) ^ ")");
refute initemss (js @ [j]))
| Failure hist =>
- (if not show_ex then ()
+ (if not show_ex orelse not (Config.get ctxt LA_Data.fast_arith_verbose) then ()
else
let
val (param_names, ctxt') = ctxt |> Variable.variant_fixes (map fst params)