equal
deleted
inserted
replaced
58 val pre_tac: simpset -> int -> tactic |
58 val pre_tac: simpset -> int -> tactic |
59 |
59 |
60 (*the limit on the number of ~= allowed; because each ~= is split |
60 (*the limit on the number of ~= allowed; because each ~= is split |
61 into two cases, this can lead to an explosion*) |
61 into two cases, this can lead to an explosion*) |
62 val fast_arith_neq_limit: int Config.T |
62 val fast_arith_neq_limit: int Config.T |
|
63 |
|
64 (*configures whether (potentially spurious) counterexamples are printed*) |
|
65 val fast_arith_verbose: bool Config.T |
63 end; |
66 end; |
64 (* |
67 (* |
65 decomp(`x Rel y') should yield (p,i,Rel,q,j,d) |
68 decomp(`x Rel y') should yield (p,i,Rel,q,j,d) |
66 where Rel is one of "<", "~<", "<=", "~<=" and "=" and |
69 where Rel is one of "<", "~<", "<=", "~<=" and "=" and |
67 p (q, respectively) is the decomposition of the sum term x |
70 p (q, respectively) is the decomposition of the sum term x |
610 val s = if d then string_of_int p else |
613 val s = if d then string_of_int p else |
611 if p = 0 then "0" |
614 if p = 0 then "0" |
612 else string_of_int p ^ "/" ^ string_of_int q |
615 else string_of_int p ^ "/" ^ string_of_int q |
613 in a ^ " = " ^ s end; |
616 in a ^ " = " ^ s end; |
614 |
617 |
615 fun produce_ex sds = |
618 fun is_variable (Free _) = true |
616 curry (op ~~) sds |
619 | is_variable (Var _) = true |
617 #> map print_atom |
620 | is_variable (Bound _) = true |
618 #> commas |
621 | is_variable _ = false |
619 #> curry (op ^) "Counterexample (possibly spurious):\n"; |
|
620 |
622 |
621 fun trace_ex ctxt params atoms discr n (hist: history) = |
623 fun trace_ex ctxt params atoms discr n (hist: history) = |
622 case hist of |
624 case hist of |
623 [] => () |
625 [] => () |
624 | (v, lineqs) :: hist' => |
626 | (v, lineqs) :: hist' => |
626 val frees = map Free params |
628 val frees = map Free params |
627 fun show_term t = Syntax.string_of_term ctxt (subst_bounds (frees, t)) |
629 fun show_term t = Syntax.string_of_term ctxt (subst_bounds (frees, t)) |
628 val start = |
630 val start = |
629 if v = ~1 then (hist', findex0 discr n lineqs) |
631 if v = ~1 then (hist', findex0 discr n lineqs) |
630 else (hist, replicate n Rat.zero) |
632 else (hist, replicate n Rat.zero) |
631 val ex = SOME (produce_ex (map show_term atoms ~~ discr) |
633 val produce_ex = |
632 (uncurry (fold (findex1 discr)) start)) |
634 map print_atom #> commas #> |
|
635 prefix "Counterexample (possibly spurious):\n" |
|
636 val ex = ( |
|
637 uncurry (fold (findex1 discr)) start |
|
638 |> map2 pair (atoms ~~ discr) |
|
639 |> filter (fn ((t, _), _) => is_variable t) |
|
640 |> map (apfst (apfst show_term)) |
|
641 |> (fn [] => NONE | sdss => SOME (produce_ex sdss))) |
633 handle NoEx => NONE |
642 handle NoEx => NONE |
634 in |
643 in |
635 case ex of |
644 case ex of |
636 SOME s => (warning "Linear arithmetic failed - see trace for a (potentially spurious) counterexample."; tracing s) |
645 SOME s => (warning "Linear arithmetic failed - see trace for a (potentially spurious) counterexample."; tracing s) |
637 | NONE => warning "Linear arithmetic failed" |
646 | NONE => warning "Linear arithmetic failed" |
742 in case elim (ineqs, []) of |
751 in case elim (ineqs, []) of |
743 Success j => |
752 Success j => |
744 (trace_msg ("Contradiction! (" ^ string_of_int (length js + 1) ^ ")"); |
753 (trace_msg ("Contradiction! (" ^ string_of_int (length js + 1) ^ ")"); |
745 refute initemss (js @ [j])) |
754 refute initemss (js @ [j])) |
746 | Failure hist => |
755 | Failure hist => |
747 (if not show_ex then () |
756 (if not show_ex orelse not (Config.get ctxt LA_Data.fast_arith_verbose) then () |
748 else |
757 else |
749 let |
758 let |
750 val (param_names, ctxt') = ctxt |> Variable.variant_fixes (map fst params) |
759 val (param_names, ctxt') = ctxt |> Variable.variant_fixes (map fst params) |
751 val (more_names, ctxt'') = ctxt' |> Variable.variant_fixes |
760 val (more_names, ctxt'') = ctxt' |> Variable.variant_fixes |
752 (Name.invent (Variable.names_of ctxt') Name.uu (length Ts - length params)) |
761 (Name.invent (Variable.names_of ctxt') Name.uu (length Ts - length params)) |