# HG changeset patch
# User boehmes
# Date 1309341515 -7200
# Node ID 119767e1ccb4b42d236081e819067ea086b65356
# Parent  d4cbd6feffdf25affca29e241cf499d351f69063
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)

diff -r d4cbd6feffdf -r 119767e1ccb4 src/HOL/Tools/lin_arith.ML
--- 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 *)
diff -r d4cbd6feffdf -r 119767e1ccb4 src/HOL/Tools/try_methods.ML
--- 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"
diff -r d4cbd6feffdf -r 119767e1ccb4 src/Provers/Arith/fast_lin_arith.ML
--- 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)