64 val depth_limit: int Config.T |
64 val depth_limit: int Config.T |
65 val blast_tac: Proof.context -> int -> tactic |
65 val blast_tac: Proof.context -> int -> tactic |
66 val setup: theory -> theory |
66 val setup: theory -> theory |
67 (*debugging tools*) |
67 (*debugging tools*) |
68 type branch |
68 type branch |
69 val stats: bool Unsynchronized.ref |
69 val stats: bool Config.T |
70 val trace: bool Unsynchronized.ref |
70 val trace: bool Config.T |
71 val fullTrace: branch list list Unsynchronized.ref |
|
72 val fromType: (indexname * term) list Unsynchronized.ref -> Term.typ -> term |
71 val fromType: (indexname * term) list Unsynchronized.ref -> Term.typ -> term |
73 val fromTerm: theory -> Term.term -> term |
72 val fromTerm: theory -> Term.term -> term |
74 val fromSubgoal: theory -> Term.term -> term |
73 val fromSubgoal: theory -> Term.term -> term |
75 val instVars: term -> (unit -> unit) |
74 val instVars: term -> (unit -> unit) |
76 val toTerm: int -> term -> Term.term |
75 val toTerm: int -> term -> Term.term |
77 val readGoal: Proof.context -> string -> term |
76 val readGoal: Proof.context -> string -> term |
78 val tryIt: Proof.context -> int -> string -> |
77 val tryIt: Proof.context -> int -> string -> |
79 (int -> tactic) list * branch list list * (int * int * exn) list |
78 {fullTrace: branch list list, |
|
79 result: ((int -> tactic) list * branch list list * (int * int * exn) list)} |
80 val normBr: branch -> branch |
80 val normBr: branch -> branch |
81 end; |
81 end; |
82 |
82 |
83 functor Blast(Data: BLAST_DATA): BLAST = |
83 functor Blast(Data: BLAST_DATA): BLAST = |
84 struct |
84 struct |
85 |
85 |
86 structure Classical = Data.Classical; |
86 structure Classical = Data.Classical; |
87 |
87 |
88 val trace = Unsynchronized.ref false |
88 val trace = Config.bool (Config.declare "Blast.trace" (K (Config.Bool false))); |
89 and stats = Unsynchronized.ref false; (*for runtime and search statistics*) |
89 val stats = Config.bool (Config.declare "Blast.stats" (K (Config.Bool false))); |
|
90 (*for runtime and search statistics*) |
90 |
91 |
91 datatype term = |
92 datatype term = |
92 Const of string * term list (*typargs constant--as a terms!*) |
93 Const of string * term list (*typargs constant--as a terms!*) |
93 | Skolem of string * term option Unsynchronized.ref list |
94 | Skolem of string * term option Unsynchronized.ref list |
94 | Free of string |
95 | Free of string |
480 fun rot_subgoals_tac (rot, rl) = |
481 fun rot_subgoals_tac (rot, rl) = |
481 rot_tac (if rot then map nNewHyps rl else []) |
482 rot_tac (if rot then map nNewHyps rl else []) |
482 end; |
483 end; |
483 |
484 |
484 |
485 |
485 fun TRACE rl tac st i = |
486 fun TRACE ctxt rl tac i st = |
486 if !trace then (writeln (Display.string_of_thm_without_context rl); tac st i) |
487 if Config.get ctxt trace then (writeln (Display.string_of_thm ctxt rl); tac i st) |
487 else tac st i; |
488 else tac i st; |
488 |
489 |
489 (*Resolution/matching tactics: if upd then the proof state may be updated. |
490 (*Resolution/matching tactics: if upd then the proof state may be updated. |
490 Matching makes the tactics more deterministic in the presence of Vars.*) |
491 Matching makes the tactics more deterministic in the presence of Vars.*) |
491 fun emtac upd rl = TRACE rl (if upd then etac rl else ematch_tac [rl]); |
492 fun emtac ctxt upd rl = TRACE ctxt rl (if upd then etac rl else ematch_tac [rl]); |
492 fun rmtac upd rl = TRACE rl (if upd then rtac rl else match_tac [rl]); |
493 fun rmtac ctxt upd rl = TRACE ctxt rl (if upd then rtac rl else match_tac [rl]); |
493 |
494 |
494 (*Tableau rule from elimination rule. |
495 (*Tableau rule from elimination rule. |
495 Flag "upd" says that the inference updated the branch. |
496 Flag "upd" says that the inference updated the branch. |
496 Flag "dup" requests duplication of the affected formula.*) |
497 Flag "dup" requests duplication of the affected formula.*) |
497 fun fromRule ctxt vars rl = |
498 fun fromRule ctxt vars rl = |
498 let val thy = Proof_Context.theory_of ctxt |
499 let val thy = Proof_Context.theory_of ctxt |
499 val trl = rl |> Thm.prop_of |> fromTerm thy |> convertRule vars |
500 val trl = rl |> Thm.prop_of |> fromTerm thy |> convertRule vars |
500 fun tac (upd, dup,rot) i = |
501 fun tac (upd, dup,rot) i = |
501 emtac upd (if dup then rev_dup_elim rl else rl) i |
502 emtac ctxt upd (if dup then rev_dup_elim rl else rl) i |
502 THEN |
503 THEN |
503 rot_subgoals_tac (rot, #2 trl) i |
504 rot_subgoals_tac (rot, #2 trl) i |
504 in Option.SOME (trl, tac) end |
505 in Option.SOME (trl, tac) end |
505 handle |
506 handle |
506 ElimBadPrem => (*reject: prems don't preserve conclusion*) |
507 ElimBadPrem => (*reject: prems don't preserve conclusion*) |
507 (warning ("Ignoring weak elimination rule\n" ^ Display.string_of_thm ctxt rl); |
508 (warning ("Ignoring weak elimination rule\n" ^ Display.string_of_thm ctxt rl); |
508 Option.NONE) |
509 Option.NONE) |
509 | ElimBadConcl => (*ignore: conclusion is not just a variable*) |
510 | ElimBadConcl => (*ignore: conclusion is not just a variable*) |
510 (if !trace then |
511 (if Config.get ctxt trace then |
511 (warning ("Ignoring ill-formed elimination rule:\n" ^ |
512 (warning ("Ignoring ill-formed elimination rule:\n" ^ |
512 "conclusion should be a variable\n" ^ Display.string_of_thm ctxt rl)) |
513 "conclusion should be a variable\n" ^ Display.string_of_thm ctxt rl)) |
513 else (); |
514 else (); |
514 Option.NONE); |
515 Option.NONE); |
515 |
516 |
531 introduction rules.*) |
532 introduction rules.*) |
532 fun fromIntrRule ctxt vars rl = |
533 fun fromIntrRule ctxt vars rl = |
533 let val thy = Proof_Context.theory_of ctxt |
534 let val thy = Proof_Context.theory_of ctxt |
534 val trl = rl |> Thm.prop_of |> fromTerm thy |> convertIntrRule vars |
535 val trl = rl |> Thm.prop_of |> fromTerm thy |> convertIntrRule vars |
535 fun tac (upd,dup,rot) i = |
536 fun tac (upd,dup,rot) i = |
536 rmtac upd (if dup then Classical.dup_intr rl else rl) i |
537 rmtac ctxt upd (if dup then Classical.dup_intr rl else rl) i |
537 THEN |
538 THEN |
538 rot_subgoals_tac (rot, #2 trl) i |
539 rot_subgoals_tac (rot, #2 trl) i |
539 in (trl, tac) end; |
540 in (trl, tac) end; |
540 |
541 |
541 |
542 |
620 have been moved there from the literals list after substitution (equalSubst). |
621 have been moved there from the literals list after substitution (equalSubst). |
621 There can be at most one--this function could be made more efficient.*) |
622 There can be at most one--this function could be made more efficient.*) |
622 fun negOfGoals pairs = map (fn (Gs,haz) => (map negOfGoal2 Gs, haz)) pairs; |
623 fun negOfGoals pairs = map (fn (Gs,haz) => (map negOfGoal2 Gs, haz)) pairs; |
623 |
624 |
624 (*Tactic. Convert *Goal* to negated assumption in FIRST position*) |
625 (*Tactic. Convert *Goal* to negated assumption in FIRST position*) |
625 fun negOfGoal_tac i = TRACE Data.ccontr (rtac Data.ccontr) i THEN |
626 fun negOfGoal_tac ctxt i = |
626 rotate_tac ~1 i; |
627 TRACE ctxt Data.ccontr (rtac Data.ccontr) i THEN rotate_tac ~1 i; |
627 |
628 |
628 fun traceTerm ctxt t = |
629 fun traceTerm ctxt t = |
629 let val thy = Proof_Context.theory_of ctxt |
630 let val thy = Proof_Context.theory_of ctxt |
630 val t' = norm (negOfGoal t) |
631 val t' = norm (negOfGoal t) |
631 val stm = string_of ctxt 8 t' |
632 val stm = string_of ctxt 8 t' |
645 (fullTrace := brs0 :: !fullTrace; |
646 (fullTrace := brs0 :: !fullTrace; |
646 List.app (fn _ => Output.tracing "+") brs; |
647 List.app (fn _ => Output.tracing "+") brs; |
647 Output.tracing (" [" ^ string_of_int lim ^ "] "); |
648 Output.tracing (" [" ^ string_of_int lim ^ "] "); |
648 printPairs pairs; |
649 printPairs pairs; |
649 writeln"") |
650 writeln"") |
650 in if !trace then printBrs (map normBr brs) else () |
651 in if Config.get ctxt trace then printBrs (map normBr brs) else () end; |
651 end; |
652 |
652 |
653 fun traceMsg true s = writeln s |
653 fun traceMsg s = if !trace then writeln s else (); |
654 | traceMsg false _ = (); |
654 |
655 |
655 (*Tracing: variables updated in the last branch operation?*) |
656 (*Tracing: variables updated in the last branch operation?*) |
656 fun traceVars (State {ctxt, ntrail, trail, ...}) ntrl = |
657 fun traceVars (State {ctxt, ntrail, trail, ...}) ntrl = |
657 if !trace then |
658 if Config.get ctxt trace then |
658 (case !ntrail-ntrl of |
659 (case !ntrail-ntrl of |
659 0 => () |
660 0 => () |
660 | 1 => Output.tracing "\t1 variable UPDATED:" |
661 | 1 => Output.tracing "\t1 variable UPDATED:" |
661 | n => Output.tracing ("\t" ^ string_of_int n ^ " variables UPDATED:"); |
662 | n => Output.tracing ("\t" ^ string_of_int n ^ " variables UPDATED:"); |
662 (*display the instantiations themselves, though no variable names*) |
663 (*display the instantiations themselves, though no variable names*) |
664 (List.take(!trail, !ntrail-ntrl)); |
665 (List.take(!trail, !ntrail-ntrl)); |
665 writeln "") |
666 writeln "") |
666 else (); |
667 else (); |
667 |
668 |
668 (*Tracing: how many new branches are created?*) |
669 (*Tracing: how many new branches are created?*) |
669 fun traceNew prems = |
670 fun traceNew true prems = |
670 if !trace then |
671 (case length prems of |
671 case length prems of |
672 0 => Output.tracing "branch closed by rule" |
672 0 => Output.tracing "branch closed by rule" |
673 | 1 => Output.tracing "branch extended (1 new subgoal)" |
673 | 1 => Output.tracing "branch extended (1 new subgoal)" |
674 | n => Output.tracing ("branch split: "^ string_of_int n ^ " new subgoals")) |
674 | n => Output.tracing ("branch split: "^ string_of_int n ^ " new subgoals") |
675 | traceNew _ _ = (); |
675 else (); |
|
676 |
676 |
677 |
677 |
678 |
678 |
679 (*** Code for handling equality: naive substitution, like hyp_subst_tac ***) |
679 (*** Code for handling equality: naive substitution, like hyp_subst_tac ***) |
680 |
680 |
767 in if nlit aconv lit then (changed, nlit::nlits) |
767 in if nlit aconv lit then (changed, nlit::nlits) |
768 else ((nlit,true)::changed, nlits) |
768 else ((nlit,true)::changed, nlits) |
769 end |
769 end |
770 val (changed, lits') = List.foldr subLit ([], []) lits |
770 val (changed, lits') = List.foldr subLit ([], []) lits |
771 val (changed', pairs') = List.foldr subFrame (changed, []) pairs |
771 val (changed', pairs') = List.foldr subFrame (changed, []) pairs |
772 in if !trace then writeln ("Substituting " ^ traceTerm ctxt u ^ |
772 in if Config.get ctxt trace then writeln ("Substituting " ^ traceTerm ctxt u ^ |
773 " for " ^ traceTerm ctxt t ^ " in branch" ) |
773 " for " ^ traceTerm ctxt t ^ " in branch" ) |
774 else (); |
774 else (); |
775 {pairs = (changed',[])::pairs', (*affected formulas, and others*) |
775 {pairs = (changed',[])::pairs', (*affected formulas, and others*) |
776 lits = lits', (*unaffected literals*) |
776 lits = lits', (*unaffected literals*) |
777 vars = vars, |
777 vars = vars, |
785 |
785 |
786 (*Trying eq_contr_tac first INCREASES the effort, slowing reconstruction*) |
786 (*Trying eq_contr_tac first INCREASES the effort, slowing reconstruction*) |
787 val contr_tac = ematch_tac [Data.notE] THEN' |
787 val contr_tac = ematch_tac [Data.notE] THEN' |
788 (eq_assume_tac ORELSE' assume_tac); |
788 (eq_assume_tac ORELSE' assume_tac); |
789 |
789 |
790 val eContr_tac = TRACE Data.notE contr_tac; |
|
791 val eAssume_tac = TRACE asm_rl (eq_assume_tac ORELSE' assume_tac); |
|
792 |
|
793 (*Try to unify complementary literals and return the corresponding tactic. *) |
790 (*Try to unify complementary literals and return the corresponding tactic. *) |
794 fun tryClose state (G, L) = |
791 fun tryClose state (G, L) = |
795 let |
792 let |
|
793 val State {ctxt, ...} = state; |
|
794 val eContr_tac = TRACE ctxt Data.notE contr_tac; |
|
795 val eAssume_tac = TRACE ctxt asm_rl (eq_assume_tac ORELSE' assume_tac); |
796 fun close t u tac = if unify state ([], t, u) then SOME tac else NONE; |
796 fun close t u tac = if unify state ([], t, u) then SOME tac else NONE; |
797 fun arg (_ $ t) = t; |
797 fun arg (_ $ t) = t; |
798 in |
798 in |
799 if isGoal G then close (arg G) L eAssume_tac |
799 if isGoal G then close (arg G) L eAssume_tac |
800 else if isGoal L then close G (arg L) eAssume_tac |
800 else if isGoal L then close G (arg L) eAssume_tac |
830 (*nbrs = # of branches just prior to closing this one. Delete choice points |
830 (*nbrs = # of branches just prior to closing this one. Delete choice points |
831 for goals proved by the latest inference, provided NO variables in the |
831 for goals proved by the latest inference, provided NO variables in the |
832 next branch have been updated.*) |
832 next branch have been updated.*) |
833 fun prune _ (1, nxtVars, choices) = choices (*DON'T prune at very end: allow |
833 fun prune _ (1, nxtVars, choices) = choices (*DON'T prune at very end: allow |
834 backtracking over bad proofs*) |
834 backtracking over bad proofs*) |
835 | prune (State {ntrail, trail, ...}) (nbrs: int, nxtVars, choices) = |
835 | prune (State {ctxt, ntrail, trail, ...}) (nbrs: int, nxtVars, choices) = |
836 let fun traceIt last = |
836 let fun traceIt last = |
837 let val ll = length last |
837 let val ll = length last |
838 and lc = length choices |
838 and lc = length choices |
839 in if !trace andalso ll<lc then |
839 in if Config.get ctxt trace andalso ll<lc then |
840 (writeln("Pruning " ^ string_of_int(lc-ll) ^ " levels"); |
840 (writeln("Pruning " ^ string_of_int(lc-ll) ^ " levels"); |
841 last) |
841 last) |
842 else last |
842 else last |
843 end |
843 end |
844 fun pruneAux (last, _, _, []) = last |
844 fun pruneAux (last, _, _, []) = last |
854 in traceIt (pruneAux (choices, !ntrail, !trail, choices)) end; |
854 in traceIt (pruneAux (choices, !ntrail, !trail, choices)) end; |
855 |
855 |
856 fun nextVars ({pairs, lits, vars, lim} :: _) = map Var vars |
856 fun nextVars ({pairs, lits, vars, lim} :: _) = map Var vars |
857 | nextVars [] = []; |
857 | nextVars [] = []; |
858 |
858 |
859 fun backtrack (choices as (ntrl, nbrs, exn)::_) = |
859 fun backtrack trace (choices as (ntrl, nbrs, exn)::_) = |
860 (if !trace then (writeln ("Backtracking; now there are " ^ |
860 (if trace then (writeln ("Backtracking; now there are " ^ string_of_int nbrs ^ " branches")) |
861 string_of_int nbrs ^ " branches")) |
861 else (); |
862 else (); |
|
863 raise exn) |
862 raise exn) |
864 | backtrack _ = raise PROVE; |
863 | backtrack _ _ = raise PROVE; |
865 |
864 |
866 (*Add the literal G, handling *Goal* and detecting duplicates.*) |
865 (*Add the literal G, handling *Goal* and detecting duplicates.*) |
867 fun addLit (Const ("*Goal*", _) $ G, lits) = |
866 fun addLit (Const ("*Goal*", _) $ G, lits) = |
868 (*New literal is a *Goal*, so change all other Goals to Nots*) |
867 (*New literal is a *Goal*, so change all other Goals to Nots*) |
869 let fun bad (Const ("*Goal*", _) $ _) = true |
868 let fun bad (Const ("*Goal*", _) $ _) = true |
919 bound on unsafe expansions. |
918 bound on unsafe expansions. |
920 "start" is CPU time at start, for printing search time |
919 "start" is CPU time at start, for printing search time |
921 *) |
920 *) |
922 fun prove (state, start, brs, cont) = |
921 fun prove (state, start, brs, cont) = |
923 let val State {ctxt, ntrail, nclosed, ntried, ...} = state; |
922 let val State {ctxt, ntrail, nclosed, ntried, ...} = state; |
|
923 val trace = Config.get ctxt trace; |
|
924 val stats = Config.get ctxt stats; |
924 val {safe0_netpair, safep_netpair, haz_netpair, ...} = |
925 val {safe0_netpair, safep_netpair, haz_netpair, ...} = |
925 Classical.rep_cs (Classical.claset_of ctxt); |
926 Classical.rep_cs (Classical.claset_of ctxt); |
926 val safeList = [safe0_netpair, safep_netpair] |
927 val safeList = [safe0_netpair, safep_netpair] |
927 and hazList = [haz_netpair] |
928 and hazList = [haz_netpair] |
928 fun prv (tacs, trs, choices, []) = |
929 fun prv (tacs, trs, choices, []) = |
929 (printStats state (!trace orelse !stats, start, tacs); |
930 (printStats state (trace orelse stats, start, tacs); |
930 cont (tacs, trs, choices)) (*all branches closed!*) |
931 cont (tacs, trs, choices)) (*all branches closed!*) |
931 | prv (tacs, trs, choices, |
932 | prv (tacs, trs, choices, |
932 brs0 as {pairs = ((G,md)::br, haz)::pairs, |
933 brs0 as {pairs = ((G,md)::br, haz)::pairs, |
933 lits, vars, lim} :: brs) = |
934 lits, vars, lim} :: brs) = |
934 (*apply a safe rule only (possibly allowing instantiation); |
935 (*apply a safe rule only (possibly allowing instantiation); |
969 val vars' = List.foldr add_terms_vars vars prems |
970 val vars' = List.foldr add_terms_vars vars prems |
970 val choices' = (ntrl, nbrs, PRV) :: choices |
971 val choices' = (ntrl, nbrs, PRV) :: choices |
971 val tacs' = (tac(updated,false,true)) |
972 val tacs' = (tac(updated,false,true)) |
972 :: tacs (*no duplication; rotate*) |
973 :: tacs (*no duplication; rotate*) |
973 in |
974 in |
974 traceNew prems; traceVars state ntrl; |
975 traceNew trace prems; traceVars state ntrl; |
975 (if null prems then (*closed the branch: prune!*) |
976 (if null prems then (*closed the branch: prune!*) |
976 (nclosed := !nclosed + 1; |
977 (nclosed := !nclosed + 1; |
977 prv(tacs', brs0::trs, |
978 prv(tacs', brs0::trs, |
978 prune state (nbrs, nxtVars, choices'), |
979 prune state (nbrs, nxtVars, choices'), |
979 brs)) |
980 brs)) |
980 else (*prems non-null*) |
981 else (*prems non-null*) |
981 if lim'<0 (*faster to kill ALL the alternatives*) |
982 if lim'<0 (*faster to kill ALL the alternatives*) |
982 then (traceMsg"Excessive branching: KILLED"; |
983 then (traceMsg trace "Excessive branching: KILLED"; |
983 clearTo state ntrl; raise NEWBRANCHES) |
984 clearTo state ntrl; raise NEWBRANCHES) |
984 else |
985 else |
985 (ntried := !ntried + length prems - 1; |
986 (ntried := !ntried + length prems - 1; |
986 prv(tacs', brs0::trs, choices', |
987 prv(tacs', brs0::trs, choices', |
987 newBr (vars',lim') prems))) |
988 newBr (vars',lim') prems))) |
989 if updated then |
990 if updated then |
990 (*Backtrack at this level. |
991 (*Backtrack at this level. |
991 Reset Vars and try another rule*) |
992 Reset Vars and try another rule*) |
992 (clearTo state ntrl; deeper grls) |
993 (clearTo state ntrl; deeper grls) |
993 else (*backtrack to previous level*) |
994 else (*backtrack to previous level*) |
994 backtrack choices |
995 backtrack trace choices |
995 end |
996 end |
996 else deeper grls |
997 else deeper grls |
997 (*Try to close branch by unifying with head goal*) |
998 (*Try to close branch by unifying with head goal*) |
998 fun closeF [] = raise CLOSEF |
999 fun closeF [] = raise CLOSEF |
999 | closeF (L::Ls) = |
1000 | closeF (L::Ls) = |
1000 case tryClose state (G,L) of |
1001 case tryClose state (G,L) of |
1001 NONE => closeF Ls |
1002 NONE => closeF Ls |
1002 | SOME tac => |
1003 | SOME tac => |
1003 let val choices' = |
1004 let val choices' = |
1004 (if !trace then (Output.tracing "branch closed"; |
1005 (if trace then (Output.tracing "branch closed"; |
1005 traceVars state ntrl) |
1006 traceVars state ntrl) |
1006 else (); |
1007 else (); |
1007 prune state (nbrs, nxtVars, |
1008 prune state (nbrs, nxtVars, |
1008 (ntrl, nbrs, PRV) :: choices)) |
1009 (ntrl, nbrs, PRV) :: choices)) |
1009 in nclosed := !nclosed + 1; |
1010 in nclosed := !nclosed + 1; |
1018 | closeFl ((br, haz)::pairs) = |
1019 | closeFl ((br, haz)::pairs) = |
1019 closeF (map fst br) |
1020 closeF (map fst br) |
1020 handle CLOSEF => closeF (map fst haz) |
1021 handle CLOSEF => closeF (map fst haz) |
1021 handle CLOSEF => closeFl pairs |
1022 handle CLOSEF => closeFl pairs |
1022 in tracing state brs0; |
1023 in tracing state brs0; |
1023 if lim<0 then (traceMsg "Limit reached. "; backtrack choices) |
1024 if lim<0 then (traceMsg trace "Limit reached. "; backtrack trace choices) |
1024 else |
1025 else |
1025 prv (Data.hyp_subst_tac (!trace) :: tacs, |
1026 prv (Data.hyp_subst_tac trace :: tacs, |
1026 brs0::trs, choices, |
1027 brs0::trs, choices, |
1027 equalSubst ctxt |
1028 equalSubst ctxt |
1028 (G, {pairs = (br,haz)::pairs, |
1029 (G, {pairs = (br,haz)::pairs, |
1029 lits = lits, vars = vars, lim = lim}) |
1030 lits = lits, vars = vars, lim = lim}) |
1030 :: brs) |
1031 :: brs) |
1032 handle CLOSEF => closeFl ((br,haz)::pairs) |
1033 handle CLOSEF => closeFl ((br,haz)::pairs) |
1033 handle CLOSEF => deeper rules |
1034 handle CLOSEF => deeper rules |
1034 handle NEWBRANCHES => |
1035 handle NEWBRANCHES => |
1035 (case netMkRules ctxt G vars hazList of |
1036 (case netMkRules ctxt G vars hazList of |
1036 [] => (*there are no plausible haz rules*) |
1037 [] => (*there are no plausible haz rules*) |
1037 (traceMsg "moving formula to literals"; |
1038 (traceMsg trace "moving formula to literals"; |
1038 prv (tacs, brs0::trs, choices, |
1039 prv (tacs, brs0::trs, choices, |
1039 {pairs = (br,haz)::pairs, |
1040 {pairs = (br,haz)::pairs, |
1040 lits = addLit(G,lits), |
1041 lits = addLit(G,lits), |
1041 vars = vars, |
1042 vars = vars, |
1042 lim = lim} :: brs)) |
1043 lim = lim} :: brs)) |
1043 | _ => (*G admits some haz rules: try later*) |
1044 | _ => (*G admits some haz rules: try later*) |
1044 (traceMsg "moving formula to haz list"; |
1045 (traceMsg trace "moving formula to haz list"; |
1045 prv (if isGoal G then negOfGoal_tac :: tacs |
1046 prv (if isGoal G then negOfGoal_tac ctxt :: tacs |
1046 else tacs, |
1047 else tacs, |
1047 brs0::trs, |
1048 brs0::trs, |
1048 choices, |
1049 choices, |
1049 {pairs = (br, haz@[(negOfGoal G, md)])::pairs, |
1050 {pairs = (br, haz@[(negOfGoal G, md)])::pairs, |
1050 lits = lits, |
1051 lits = lits, |
1126 position*) |
1127 position*) |
1127 |
1128 |
1128 in |
1129 in |
1129 if lim'<0 andalso not (null prems) |
1130 if lim'<0 andalso not (null prems) |
1130 then (*it's faster to kill ALL the alternatives*) |
1131 then (*it's faster to kill ALL the alternatives*) |
1131 (traceMsg"Excessive branching: KILLED"; |
1132 (traceMsg trace "Excessive branching: KILLED"; |
1132 clearTo state ntrl; raise NEWBRANCHES) |
1133 clearTo state ntrl; raise NEWBRANCHES) |
1133 else |
1134 else |
1134 traceNew prems; |
1135 traceNew trace prems; |
1135 if !trace andalso dup then Output.tracing " (duplicating)" |
1136 if trace andalso dup then Output.tracing " (duplicating)" else (); |
1136 else (); |
1137 if trace andalso recur then Output.tracing " (recursive)" else (); |
1137 if !trace andalso recur then Output.tracing " (recursive)" |
|
1138 else (); |
|
1139 traceVars state ntrl; |
1138 traceVars state ntrl; |
1140 if null prems then nclosed := !nclosed + 1 |
1139 if null prems then nclosed := !nclosed + 1 |
1141 else ntried := !ntried + length prems - 1; |
1140 else ntried := !ntried + length prems - 1; |
1142 prv(tac' :: tacs, |
1141 prv(tac' :: tacs, |
1143 brs0::trs, |
1142 brs0::trs, |
1146 handle PRV => |
1145 handle PRV => |
1147 if mayUndo |
1146 if mayUndo |
1148 then (*reset Vars and try another rule*) |
1147 then (*reset Vars and try another rule*) |
1149 (clearTo state ntrl; deeper grls) |
1148 (clearTo state ntrl; deeper grls) |
1150 else (*backtrack to previous level*) |
1149 else (*backtrack to previous level*) |
1151 backtrack choices |
1150 backtrack trace choices |
1152 end |
1151 end |
1153 else deeper grls |
1152 else deeper grls |
1154 in tracing state brs0; |
1153 in tracing state brs0; |
1155 if lim<1 then (traceMsg "Limit reached. "; backtrack choices) |
1154 if lim<1 then (traceMsg trace "Limit reached. "; backtrack trace choices) |
1156 else deeper rules |
1155 else deeper rules |
1157 handle NEWBRANCHES => |
1156 handle NEWBRANCHES => |
1158 (*cannot close branch: move H to literals*) |
1157 (*cannot close branch: move H to literals*) |
1159 prv (tacs, brs0::trs, choices, |
1158 prv (tacs, brs0::trs, choices, |
1160 {pairs = [([], Hs)], |
1159 {pairs = [([], Hs)], |
1161 lits = H::lits, |
1160 lits = H::lits, |
1162 vars = vars, |
1161 vars = vars, |
1163 lim = lim} :: brs) |
1162 lim = lim} :: brs) |
1164 end |
1163 end |
1165 | prv (tacs, trs, choices, _ :: brs) = backtrack choices |
1164 | prv (tacs, trs, choices, _ :: brs) = backtrack trace choices |
1166 in prv ([], [], [(!ntrail, length brs, PROVE)], brs) end; |
1165 in prv ([], [], [(!ntrail, length brs, PROVE)], brs) end; |
1167 |
1166 |
1168 |
1167 |
1169 (*Construct an initial branch.*) |
1168 (*Construct an initial branch.*) |
1170 fun initBranch (ts,lim) = |
1169 fun initBranch (ts,lim) = |
1243 (also prints reconstruction time) |
1242 (also prints reconstruction time) |
1244 "lim" is depth limit.*) |
1243 "lim" is depth limit.*) |
1245 fun timing_depth_tac start ctxt lim i st0 = |
1244 fun timing_depth_tac start ctxt lim i st0 = |
1246 let val thy = Proof_Context.theory_of ctxt |
1245 let val thy = Proof_Context.theory_of ctxt |
1247 val state = initialize ctxt |
1246 val state = initialize ctxt |
|
1247 val trace = Config.get ctxt trace; |
|
1248 val stats = Config.get ctxt stats; |
1248 val st = st0 |
1249 val st = st0 |
1249 |> rotate_prems (i - 1) |
1250 |> rotate_prems (i - 1) |
1250 |> Conv.gconv_rule Object_Logic.atomize_prems 1 |
1251 |> Conv.gconv_rule Object_Logic.atomize_prems 1 |
1251 val skoprem = fromSubgoal thy (#1 (Logic.dest_implies (Thm.prop_of st))) |
1252 val skoprem = fromSubgoal thy (#1 (Logic.dest_implies (Thm.prop_of st))) |
1252 val hyps = strip_imp_prems skoprem |
1253 val hyps = strip_imp_prems skoprem |
1255 let val start = Timing.start () |
1256 let val start = Timing.start () |
1256 in |
1257 in |
1257 case Seq.pull(EVERY' (rev tacs) 1 st) of |
1258 case Seq.pull(EVERY' (rev tacs) 1 st) of |
1258 NONE => (writeln ("PROOF FAILED for depth " ^ |
1259 NONE => (writeln ("PROOF FAILED for depth " ^ |
1259 string_of_int lim); |
1260 string_of_int lim); |
1260 if !trace then error "************************\n" |
1261 if trace then error "************************\n" |
1261 else (); |
1262 else (); |
1262 backtrack choices) |
1263 backtrack trace choices) |
1263 | cell => (if (!trace orelse !stats) |
1264 | cell => (if (trace orelse stats) |
1264 then writeln (Timing.message (Timing.result start) ^ " for reconstruction") |
1265 then writeln (Timing.message (Timing.result start) ^ " for reconstruction") |
1265 else (); |
1266 else (); |
1266 Seq.make(fn()=> cell)) |
1267 Seq.make(fn()=> cell)) |
1267 end |
1268 end |
1268 in |
1269 in |
1278 Attrib.config_int @{binding blast_depth_limit} (K 20); |
1279 Attrib.config_int @{binding blast_depth_limit} (K 20); |
1279 |
1280 |
1280 fun blast_tac ctxt i st = |
1281 fun blast_tac ctxt i st = |
1281 ((DEEPEN (1, Config.get ctxt depth_limit) (timing_depth_tac (Timing.start ()) ctxt) 0) i |
1282 ((DEEPEN (1, Config.get ctxt depth_limit) (timing_depth_tac (Timing.start ()) ctxt) 0) i |
1282 THEN flexflex_tac) st |
1283 THEN flexflex_tac) st |
1283 handle TRANS s => (if !trace then warning ("blast: " ^ s) else (); Seq.empty); |
1284 handle TRANS s => (if Config.get ctxt trace then warning ("blast: " ^ s) else (); Seq.empty); |
1284 |
1285 |
1285 |
1286 |
1286 |
1287 |
1287 (*** For debugging: these apply the prover to a subgoal and return |
1288 (*** For debugging: these apply the prover to a subgoal and return |
1288 the resulting tactics, trace, etc. ***) |
1289 the resulting tactics, trace, etc. ***) |
1289 |
|
1290 val fullTrace = Unsynchronized.ref ([]: branch list list); |
|
1291 |
1290 |
1292 (*Read a string to make an initial, singleton branch*) |
1291 (*Read a string to make an initial, singleton branch*) |
1293 fun readGoal ctxt s = |
1292 fun readGoal ctxt s = |
1294 Syntax.read_prop ctxt s |> fromTerm (Proof_Context.theory_of ctxt) |> rand |> mkGoal; |
1293 Syntax.read_prop ctxt s |> fromTerm (Proof_Context.theory_of ctxt) |> rand |> mkGoal; |
1295 |
1294 |
1296 fun tryIt ctxt lim s = |
1295 fun tryIt ctxt lim s = |
1297 let |
1296 let |
1298 val state as State {fullTrace = ft, ...} = initialize ctxt; |
1297 val state as State {fullTrace, ...} = initialize ctxt; |
1299 val res = timeap prove (state, Timing.start (), [initBranch ([readGoal ctxt s], lim)], I); |
1298 val res = timeap prove (state, Timing.start (), [initBranch ([readGoal ctxt s], lim)], I); |
1300 val _ = fullTrace := !ft; |
1299 in {fullTrace = !fullTrace, result = res} end; |
1301 in res end; |
|
1302 |
1300 |
1303 |
1301 |
1304 (** method setup **) |
1302 (** method setup **) |
1305 |
1303 |
1306 val setup = |
1304 val setup = |