diff --git a/src/HOL/SMT.thy b/src/HOL/SMT.thy --- a/src/HOL/SMT.thy +++ b/src/HOL/SMT.thy @@ -1,894 +1,895 @@ (* Title: HOL/SMT.thy Author: Sascha Boehme, TU Muenchen Author: Jasmin Blanchette, VU Amsterdam *) section \Bindings to Satisfiability Modulo Theories (SMT) solvers based on SMT-LIB 2\ theory SMT imports Divides Numeral_Simprocs keywords "smt_status" :: diag begin subsection \A skolemization tactic and proof method\ lemma choices: "\Q. \x. \y ya. Q x y ya \ \f fa. \x. Q x (f x) (fa x)" "\Q. \x. \y ya yb. Q x y ya yb \ \f fa fb. \x. Q x (f x) (fa x) (fb x)" "\Q. \x. \y ya yb yc. Q x y ya yb yc \ \f fa fb fc. \x. Q x (f x) (fa x) (fb x) (fc x)" "\Q. \x. \y ya yb yc yd. Q x y ya yb yc yd \ \f fa fb fc fd. \x. Q x (f x) (fa x) (fb x) (fc x) (fd x)" "\Q. \x. \y ya yb yc yd ye. Q x y ya yb yc yd ye \ \f fa fb fc fd fe. \x. Q x (f x) (fa x) (fb x) (fc x) (fd x) (fe x)" "\Q. \x. \y ya yb yc yd ye yf. Q x y ya yb yc yd ye yf \ \f fa fb fc fd fe ff. \x. Q x (f x) (fa x) (fb x) (fc x) (fd x) (fe x) (ff x)" "\Q. \x. \y ya yb yc yd ye yf yg. Q x y ya yb yc yd ye yf yg \ \f fa fb fc fd fe ff fg. \x. Q x (f x) (fa x) (fb x) (fc x) (fd x) (fe x) (ff x) (fg x)" by metis+ lemma bchoices: "\Q. \x \ S. \y ya. Q x y ya \ \f fa. \x \ S. Q x (f x) (fa x)" "\Q. \x \ S. \y ya yb. Q x y ya yb \ \f fa fb. \x \ S. Q x (f x) (fa x) (fb x)" "\Q. \x \ S. \y ya yb yc. Q x y ya yb yc \ \f fa fb fc. \x \ S. Q x (f x) (fa x) (fb x) (fc x)" "\Q. \x \ S. \y ya yb yc yd. Q x y ya yb yc yd \ \f fa fb fc fd. \x \ S. Q x (f x) (fa x) (fb x) (fc x) (fd x)" "\Q. \x \ S. \y ya yb yc yd ye. Q x y ya yb yc yd ye \ \f fa fb fc fd fe. \x \ S. Q x (f x) (fa x) (fb x) (fc x) (fd x) (fe x)" "\Q. \x \ S. \y ya yb yc yd ye yf. Q x y ya yb yc yd ye yf \ \f fa fb fc fd fe ff. \x \ S. Q x (f x) (fa x) (fb x) (fc x) (fd x) (fe x) (ff x)" "\Q. \x \ S. \y ya yb yc yd ye yf yg. Q x y ya yb yc yd ye yf yg \ \f fa fb fc fd fe ff fg. \x \ S. Q x (f x) (fa x) (fb x) (fc x) (fd x) (fe x) (ff x) (fg x)" by metis+ ML \ fun moura_tac ctxt = Atomize_Elim.atomize_elim_tac ctxt THEN' SELECT_GOAL (Clasimp.auto_tac (ctxt addSIs @{thms choice choices bchoice bchoices}) THEN ALLGOALS (Metis_Tactic.metis_tac (take 1 ATP_Proof_Reconstruct.partial_type_encs) ATP_Proof_Reconstruct.default_metis_lam_trans ctxt [] ORELSE' blast_tac ctxt)) \ method_setup moura = \ Scan.succeed (SIMPLE_METHOD' o moura_tac) \ "solve skolemization goals, especially those arising from Z3 proofs" hide_fact (open) choices bchoices subsection \Triggers for quantifier instantiation\ text \ Some SMT solvers support patterns as a quantifier instantiation heuristics. Patterns may either be positive terms (tagged by "pat") triggering quantifier instantiations -- when the solver finds a term matching a positive pattern, it instantiates the corresponding quantifier accordingly -- or negative terms (tagged by "nopat") inhibiting quantifier instantiations. A list of patterns of the same kind is called a multipattern, and all patterns in a multipattern are considered conjunctively for quantifier instantiation. A list of multipatterns is called a trigger, and their multipatterns act disjunctively during quantifier instantiation. Each multipattern should mention at least all quantified variables of the preceding quantifier block. \ typedecl 'a symb_list consts Symb_Nil :: "'a symb_list" Symb_Cons :: "'a \ 'a symb_list \ 'a symb_list" typedecl pattern consts pat :: "'a \ pattern" nopat :: "'a \ pattern" definition trigger :: "pattern symb_list symb_list \ bool \ bool" where "trigger _ P = P" subsection \Higher-order encoding\ text \ Application is made explicit for constants occurring with varying numbers of arguments. This is achieved by the introduction of the following constant. \ definition fun_app :: "'a \ 'a" where "fun_app f = f" text \ Some solvers support a theory of arrays which can be used to encode higher-order functions. The following set of lemmas specifies the properties of such (extensional) arrays. \ lemmas array_rules = ext fun_upd_apply fun_upd_same fun_upd_other fun_upd_upd fun_app_def subsection \Normalization\ lemma case_bool_if[abs_def]: "case_bool x y P = (if P then x else y)" by simp lemmas Ex1_def_raw = Ex1_def[abs_def] lemmas Ball_def_raw = Ball_def[abs_def] lemmas Bex_def_raw = Bex_def[abs_def] lemmas abs_if_raw = abs_if[abs_def] lemmas min_def_raw = min_def[abs_def] lemmas max_def_raw = max_def[abs_def] lemma nat_zero_as_int: "0 = nat 0" by simp lemma nat_one_as_int: "1 = nat 1" by simp lemma nat_numeral_as_int: "numeral = (\i. nat (numeral i))" by simp lemma nat_less_as_int: "(<) = (\a b. int a < int b)" by simp lemma nat_leq_as_int: "(\) = (\a b. int a \ int b)" by simp lemma Suc_as_int: "Suc = (\a. nat (int a + 1))" by (rule ext) simp lemma nat_plus_as_int: "(+) = (\a b. nat (int a + int b))" by (rule ext)+ simp lemma nat_minus_as_int: "(-) = (\a b. nat (int a - int b))" by (rule ext)+ simp lemma nat_times_as_int: "(*) = (\a b. nat (int a * int b))" by (simp add: nat_mult_distrib) lemma nat_div_as_int: "(div) = (\a b. nat (int a div int b))" by (simp add: nat_div_distrib) lemma nat_mod_as_int: "(mod) = (\a b. nat (int a mod int b))" by (simp add: nat_mod_distrib) lemma int_Suc: "int (Suc n) = int n + 1" by simp lemma int_plus: "int (n + m) = int n + int m" by (rule of_nat_add) lemma int_minus: "int (n - m) = int (nat (int n - int m))" by auto lemma nat_int_comparison: fixes a b :: nat shows "(a = b) = (int a = int b)" and "(a < b) = (int a < int b)" and "(a \ b) = (int a \ int b)" by simp_all lemma int_ops: fixes a b :: nat shows "int 0 = 0" and "int 1 = 1" and "int (numeral n) = numeral n" and "int (Suc a) = int a + 1" and "int (a + b) = int a + int b" and "int (a - b) = (if int a < int b then 0 else int a - int b)" and "int (a * b) = int a * int b" and "int (a div b) = int a div int b" and "int (a mod b) = int a mod int b" by (auto intro: zdiv_int zmod_int) lemma int_if: fixes a b :: nat shows "int (if P then a else b) = (if P then int a else int b)" by simp subsection \Integer division and modulo for Z3\ text \ The following Z3-inspired definitions are overspecified for the case where \l = 0\. This Schönheitsfehler is corrected in the \div_as_z3div\ and \mod_as_z3mod\ theorems. \ definition z3div :: "int \ int \ int" where "z3div k l = (if l \ 0 then k div l else - (k div - l))" definition z3mod :: "int \ int \ int" where "z3mod k l = k mod (if l \ 0 then l else - l)" lemma div_as_z3div: "\k l. k div l = (if l = 0 then 0 else if l > 0 then z3div k l else z3div (- k) (- l))" by (simp add: z3div_def) lemma mod_as_z3mod: "\k l. k mod l = (if l = 0 then k else if l > 0 then z3mod k l else - z3mod (- k) (- l))" by (simp add: z3mod_def) subsection \Extra theorems for veriT reconstruction\ lemma verit_sko_forall: \(\x. P x) \ P (SOME x. \P x)\ using someI[of \\x. \P x\] by auto lemma verit_sko_forall': \P (SOME x. \P x) = A \ (\x. P x) = A\ by (subst verit_sko_forall) lemma verit_sko_forall'': \B = A \ (SOME x. P x) = A \ (SOME x. P x) = B\ by auto lemma verit_sko_forall_indirect: \x = (SOME x. \P x) \ (\x. P x) \ P x\ using someI[of \\x. \P x\] by auto lemma verit_sko_forall_indirect2: \x = (SOME x. \P x) \ (\x :: 'a. (P x = P' x)) \(\x. P' x) \ P x\ using someI[of \\x. \P x\] by auto lemma verit_sko_ex: \(\x. P x) \ P (SOME x. P x)\ using someI[of \\x. P x\] by auto lemma verit_sko_ex': \P (SOME x. P x) = A \ (\x. P x) = A\ by (subst verit_sko_ex) lemma verit_sko_ex_indirect: \x = (SOME x. P x) \ (\x. P x) \ P x\ using someI[of \\x. P x\] by auto lemma verit_sko_ex_indirect2: \x = (SOME x. P x) \ (\x. P x = P' x) \ (\x. P' x) \ P x\ using someI[of \\x. P x\] by auto lemma verit_Pure_trans: \P \ Q \ Q \ P\ by auto lemma verit_if_cong: assumes \b \ c\ and \c \ x \ u\ and \\ c \ y \ v\ shows \(if b then x else y) \ (if c then u else v)\ using assms if_cong[of b c x u] by auto lemma verit_if_weak_cong': \b \ c \ (if b then x else y) \ (if c then x else y)\ by auto lemma verit_or_neg: \(A \ B) \ B \ \A\ \(\A \ B) \ B \ A\ by auto lemma verit_subst_bool: \P \ f True \ f P\ by auto lemma verit_and_pos: \(a \ \(b \ c) \ A) \ \(a \ b \ c) \ A\ \(a \ b \ A) \ \(a \ b) \ A\ \(a \ A) \ \a \ A\ \(\a \ A) \ a \ A\ by blast+ lemma verit_or_pos: \A \ A' \ (c \ A) \ (\c \ A')\ \A \ A' \ (\c \ A) \ (c \ A')\ by blast+ lemma verit_la_generic: \(a::int) \ x \ a = x \ a \ x\ by linarith lemma verit_bfun_elim: \(if b then P True else P False) = P b\ \(\b. P' b) = (P' False \ P' True)\ \(\b. P' b) = (P' False \ P' True)\ by (cases b) (auto simp: all_bool_eq ex_bool_eq) lemma verit_eq_true_simplify: \(P = True) \ P\ by auto lemma verit_and_neg: \(a \ \b \ A) \ \(a \ b) \ A\ \(a \ A) \ \a \ A\ \(\a \ A) \ a \ A\ by blast+ lemma verit_forall_inst: \A \ B \ \A \ B\ \\A \ B \ A \ B\ \A \ B \ \B \ A\ \A \ \B \ B \ A\ \A \ B \ \A \ B\ \\A \ B \ A \ B\ by blast+ lemma verit_eq_transitive: \A = B \ B = C \ A = C\ \A = B \ C = B \ A = C\ \B = A \ B = C \ A = C\ \B = A \ C = B \ A = C\ by auto lemma verit_bool_simplify: \\(P \ Q) \ P \ \Q\ \\(P \ Q) \ \P \ \Q\ \\(P \ Q) \ \P \ \Q\ \(P \ (Q \ R)) \ ((P \ Q) \ R)\ \((P \ Q) \ Q) \ P \ Q\ \(Q \ (P \ Q)) \ (P \ Q)\ \ \This rule was inverted\ \P \ (P \ Q) \ P \ Q\ \(P \ Q) \ P \ P \ Q\ (* \\Additional rules:\ * \((P \ Q) \ P) \ P\ * \((P \ Q) \ Q) \ P \ Q\ * \(P \ Q) \ P\ *) unfolding not_imp imp_conjL by auto text \We need the last equation for \<^term>\\(\a b. \P a b)\\ lemma verit_connective_def: \ \the definition of XOR is missing as the operator is not generated by Isabelle\ \(A = B) \ ((A \ B) \ (B \ A))\ \(If A B C) = ((A \ B) \ (\A \ C))\ \(\x. P x) \ \(\x. \P x)\ \\(\x. P x) \ (\x. \P x)\ by auto lemma verit_ite_simplify: \(If True B C) = B\ \(If False B C) = C\ \(If A' B B) = B\ \(If (\A') B C) = (If A' C B)\ \(If c (If c A B) C) = (If c A C)\ \(If c C (If c A B)) = (If c C B)\ \(If A' True False) = A'\ \(If A' False True) \ \A'\ \(If A' True B') \ A'\B'\ \(If A' B' False) \ A'\B'\ \(If A' False B') \ \A'\B'\ \(If A' B' True) \ \A'\B'\ \x \ True \ x\ \x \ False \ x\ for B C :: 'a and A' B' C' :: bool by auto lemma verit_and_simplify1: \True \ b \ b\ \b \ True \ b\ \False \ b \ False\ \b \ False \ False\ \(c \ \c) \ False\ \(\c \ c) \ False\ \\\a = a\ by auto lemmas verit_and_simplify = conj_ac de_Morgan_conj disj_not1 lemma verit_or_simplify_1: \False \ b \ b\ \b \ False \ b\ \b \ \b\ \\b \ b\ by auto lemmas verit_or_simplify = disj_ac lemma verit_not_simplify: \\ \b \ b\ \\True \ False\ \\False \ True\ by auto lemma verit_implies_simplify: \(\a \ \b) \ (b \ a)\ \(False \ a) \ True\ \(a \ True) \ True\ \(True \ a) \ a\ \(a \ False) \ \a\ \(a \ a) \ True\ \(\a \ a) \ a\ \(a \ \a) \ \a\ \((a \ b) \ b) \ a \ b\ by auto lemma verit_equiv_simplify: \((\a) = (\b)) \ (a = b)\ \(a = a) \ True\ \(a = (\a)) \ False\ \((\a) = a) \ False\ \(True = a) \ a\ \(a = True) \ a\ \(False = a) \ \a\ \(a = False) \ \a\ \\\a \ a\ \(\ False) = True\ for a b :: bool by auto lemmas verit_eq_simplify = semiring_char_0_class.eq_numeral_simps eq_refl zero_neq_one num.simps neg_equal_zero equal_neg_zero one_neq_zero neg_equal_iff_equal lemma verit_minus_simplify: \(a :: 'a :: cancel_comm_monoid_add) - a = 0\ \(a :: 'a :: cancel_comm_monoid_add) - 0 = a\ \0 - (b :: 'b :: {group_add}) = -b\ \- (- (b :: 'b :: group_add)) = b\ by auto lemma verit_sum_simplify: \(a :: 'a :: cancel_comm_monoid_add) + 0 = a\ by auto lemmas verit_prod_simplify = (* already included: mult_zero_class.mult_zero_right mult_zero_class.mult_zero_left *) mult_1 mult_1_right lemma verit_comp_simplify1: \(a :: 'a ::order) < a \ False\ \a \ a\ \\(b' \ a') \ (a' :: 'b :: linorder) < b'\ by auto lemmas verit_comp_simplify = verit_comp_simplify1 le_numeral_simps le_num_simps less_numeral_simps less_num_simps zero_less_one zero_le_one less_neg_numeral_simps lemma verit_la_disequality: \(a :: 'a ::linorder) = b \ \a \ b \ \b \ a\ by auto context begin text \For the reconstruction, we need to keep the order of the arguments.\ named_theorems smt_arith_multiplication \Theorems to reconstruct arithmetic theorems.\ named_theorems smt_arith_combine \Theorems to reconstruct arithmetic theorems.\ named_theorems smt_arith_simplify \Theorems to combine theorems in the LA procedure\ lemmas [smt_arith_simplify] = div_add dvd_numeral_simp divmod_steps less_num_simps le_num_simps if_True if_False divmod_cancel dvd_mult dvd_mult2 less_irrefl prod.case numeral_plus_one divmod_step_eq order.refl le_zero_eq le_numeral_simps less_numeral_simps mult.right_neutral simp_thms divides_aux_eq mult_nonneg_nonneg dvd_imp_mod_0 dvd_add zero_less_one mod_mult_self4 numeral_mod_numeral divmod_trivial prod.sel mult.left_neutral div_pos_pos_trivial arith_simps div_add div_mult_self1 add_le_cancel_left add_le_same_cancel2 not_one_le_zero le_numeral_simps add_le_same_cancel1 zero_neq_one zero_le_one le_num_simps add_Suc mod_div_trivial nat.distinct mult_minus_right add.inverse_inverse distrib_left_numeral mult_num_simps numeral_times_numeral add_num_simps divmod_steps rel_simps if_True if_False numeral_div_numeral divmod_cancel prod.case add_num_simps one_plus_numeral fst_conv divmod_step_eq arith_simps sub_num_simps dbl_inc_simps dbl_simps mult_1 add_le_cancel_right left_diff_distrib_numeral add_uminus_conv_diff zero_neq_one zero_le_one One_nat_def add_Suc mod_div_trivial nat.distinct of_int_1 numerals numeral_One of_int_numeral add_uminus_conv_diff zle_diff1_eq add_less_same_cancel2 minus_add_distrib add_uminus_conv_diff mult.left_neutral semiring_class.distrib_right add_diff_cancel_left' add_diff_eq ring_distribs mult_minus_left minus_diff_eq lemma [smt_arith_simplify]: \\ (a' :: 'a :: linorder) < b' \ b' \ a'\ \\ (a' :: 'a :: linorder) \ b' \ b' < a'\ \(c::int) mod Numeral1 = 0\ \(a::nat) mod Numeral1 = 0\ \(c::int) div Numeral1 = c\ \a div Numeral1 = a\ \(c::int) mod 1 = 0\ \a mod 1 = 0\ \(c::int) div 1 = c\ \a div 1 = a\ \\(a' \ b') \ a' = b'\ by auto lemma div_mod_decomp: "A = (A div n) * n + (A mod n)" for A :: nat by auto lemma div_less_mono: fixes A B :: nat assumes "A < B" "0 < n" and mod: "A mod n = 0""B mod n = 0" shows "(A div n) < (B div n)" proof - show ?thesis using assms(1) apply (subst (asm) div_mod_decomp[of "A" n]) apply (subst (asm) div_mod_decomp[of "B" n]) unfolding mod by (use assms(2,3) in \auto simp: ac_simps\) qed lemma verit_le_mono_div: fixes A B :: nat assumes "A < B" "0 < n" shows "(A div n) + (if B mod n = 0 then 1 else 0) \ (B div n)" by (auto simp: ac_simps Suc_leI assms less_mult_imp_div_less div_le_mono less_imp_le_nat) lemmas [smt_arith_multiplication] = verit_le_mono_div[THEN mult_le_mono1, unfolded add_mult_distrib] div_le_mono[THEN mult_le_mono2, unfolded add_mult_distrib] lemma div_mod_decomp_int: "A = (A div n) * n + (A mod n)" for A :: int by auto lemma zdiv_mono_strict: fixes A B :: int assumes "A < B" "0 < n" and mod: "A mod n = 0""B mod n = 0" shows "(A div n) < (B div n)" proof - show ?thesis using assms(1) apply (subst (asm) div_mod_decomp_int[of A n]) apply (subst (asm) div_mod_decomp_int[of B n]) unfolding mod by (use assms(2,3) in \auto simp: ac_simps\) qed lemma verit_le_mono_div_int: fixes A B :: int assumes "A < B" "0 < n" shows "(A div n) + (if B mod n = 0 then 1 else 0) \ (B div n)" proof - have f2: "B div n = A div n \ A div n < B div n" by (metis (no_types) assms less_le zdiv_mono1) have "B div n \ A div n \ B mod n \ 0" using assms(1) by (metis Groups.add_ac(2) assms(2) eucl_rel_int eucl_rel_int_iff group_cancel.rule0 le_add_same_cancel2 not_le) then have "B mod n = 0 \ A div n + (if B mod n = 0 then 1 else 0) \ B div n" using f2 by (auto dest: zless_imp_add1_zle) then show ?thesis using assms zdiv_mono1 by auto qed lemma verit_less_mono_div_int2: fixes A B :: int assumes "A \ B" "0 < -n" shows "(A div n) \ (B div n)" using assms(1) assms(2) zdiv_mono1_neg by auto lemmas [smt_arith_multiplication] = verit_le_mono_div_int[THEN mult_left_mono, unfolded int_distrib] zdiv_mono1[THEN mult_left_mono, unfolded int_distrib] lemmas [smt_arith_multiplication] = arg_cong[of _ _ \\a :: nat. a div n * p\ for n p :: nat, THEN sym] arg_cong[of _ _ \\a :: int. a div n * p\ for n p :: int, THEN sym] lemma [smt_arith_combine]: "a < b \ c < d \ a + c + 2 \ b + d" "a < b \ c \ d \ a + c + 1 \ b + d" "a \ b \ c < d \ a + c + 1 \ b + d" for a b c :: int by auto lemma [smt_arith_combine]: "a < b \ c < d \ a + c + 2 \ b + d" "a < b \ c \ d \ a + c + 1 \ b + d" "a \ b \ c < d \ a + c + 1 \ b + d" for a b c :: nat by auto lemmas [smt_arith_combine] = add_strict_mono add_less_le_mono add_mono add_le_less_mono lemma [smt_arith_combine]: \m < n \ c = d \ m + c < n + d\ \m \ n \ c = d \ m + c \ n + d\ \c = d \ m < n \ m + c < n + d\ \c = d \ m \ n \ m + c \ n + d\ for m :: \'a :: ordered_cancel_ab_semigroup_add\ by (auto intro: ordered_cancel_ab_semigroup_add_class.add_strict_right_mono ordered_ab_semigroup_add_class.add_right_mono) lemma verit_negate_coefficient: \a \ (b :: 'a :: {ordered_ab_group_add}) \ -a \ -b\ \a < b \ -a > -b\ \a = b \ -a = -b\ by auto end lemma verit_ite_intro: \(if a then P (if a then a' else b') else Q) \ (if a then P a' else Q)\ \(if a then P' else Q' (if a then a' else b')) \ (if a then P' else Q' b')\ \A = f (if a then R else S) \ (if a then A = f R else A = f S)\ by auto lemma verit_ite_if_cong: fixes x y :: bool assumes "b=c" and "c \ True \ x = u" and "c \ False \ y = v" shows "(if b then x else y) \ (if c then u else v)" proof - have H: "(if b then x else y) = (if c then u else v)" using assms by (auto split: if_splits) show "(if b then x else y) \ (if c then u else v)" by (subst H) auto qed subsection \Setup\ ML_file \Tools/SMT/smt_util.ML\ ML_file \Tools/SMT/smt_failure.ML\ ML_file \Tools/SMT/smt_config.ML\ ML_file \Tools/SMT/smt_builtin.ML\ ML_file \Tools/SMT/smt_datatypes.ML\ ML_file \Tools/SMT/smt_normalize.ML\ ML_file \Tools/SMT/smt_translate.ML\ ML_file \Tools/SMT/smtlib.ML\ ML_file \Tools/SMT/smtlib_interface.ML\ ML_file \Tools/SMT/smtlib_proof.ML\ ML_file \Tools/SMT/smtlib_isar.ML\ ML_file \Tools/SMT/z3_proof.ML\ ML_file \Tools/SMT/z3_isar.ML\ ML_file \Tools/SMT/smt_solver.ML\ ML_file \Tools/SMT/cvc4_interface.ML\ ML_file \Tools/SMT/cvc4_proof_parse.ML\ ML_file \Tools/SMT/verit_proof.ML\ ML_file \Tools/SMT/verit_isar.ML\ ML_file \Tools/SMT/verit_proof_parse.ML\ ML_file \Tools/SMT/conj_disj_perm.ML\ ML_file \Tools/SMT/smt_replay_methods.ML\ ML_file \Tools/SMT/smt_replay.ML\ ML_file \Tools/SMT/smt_replay_arith.ML\ ML_file \Tools/SMT/z3_interface.ML\ ML_file \Tools/SMT/z3_replay_rules.ML\ ML_file \Tools/SMT/z3_replay_methods.ML\ ML_file \Tools/SMT/z3_replay.ML\ ML_file \Tools/SMT/verit_replay_methods.ML\ ML_file \Tools/SMT/verit_replay.ML\ ML_file \Tools/SMT/smt_systems.ML\ subsection \Configuration\ text \ The current configuration can be printed by the command \smt_status\, which shows the values of most options. \ subsection \General configuration options\ text \ The option \smt_solver\ can be used to change the target SMT solver. The possible values can be obtained from the \smt_status\ command. \ declare [[smt_solver = z3]] text \ Since SMT solvers are potentially nonterminating, there is a timeout (given in seconds) to restrict their runtime. \ declare [[smt_timeout = 0]] text \ SMT solvers apply randomized heuristics. In case a problem is not solvable by an SMT solver, changing the following option might help. \ declare [[smt_random_seed = 1]] text \ In general, the binding to SMT solvers runs as an oracle, i.e, the SMT solvers are fully trusted without additional checks. The following option can cause the SMT solver to run in proof-producing mode, giving -a checkable certificate. This is currently only implemented for Z3. +a checkable certificate. This is currently implemented only for veriT and +Z3. \ declare [[smt_oracle = false]] text \ -Each SMT solver provides several commandline options to tweak its +Each SMT solver provides several command-line options to tweak its behaviour. They can be passed to the solver by setting the following options. \ -declare [[cvc4_options = "--full-saturate-quant --inst-when=full-last-call --inst-no-entail --term-db-mode=relevant --multi-trigger-linear"]] +declare [[cvc4_options = ""]] declare [[verit_options = ""]] declare [[z3_options = ""]] text \ The SMT method provides an inference mechanism to detect simple triggers in quantified formulas, which might increase the number of problems solvable by SMT solvers (note: triggers guide quantifier instantiations in the SMT solver). To turn it on, set the following option. \ declare [[smt_infer_triggers = false]] text \ Enable the following option to use built-in support for datatypes, codatatypes, and records in CVC4. Currently, this is implemented only in oracle mode. \ declare [[cvc4_extensions = false]] text \ Enable the following option to use built-in support for div/mod, datatypes, and records in Z3. Currently, this is implemented only in oracle mode. \ declare [[z3_extensions = false]] subsection \Certificates\ text \ By setting the option \smt_certificates\ to the name of a file, all following applications of an SMT solver a cached in that file. Any further application of the same SMT solver (using the very same configuration) re-uses the cached certificate instead of invoking the solver. An empty string disables caching certificates. The filename should be given as an explicit path. It is good practice to use the name of the current theory (with ending \.certs\ instead of \.thy\) as the certificates file. Certificate files should be used at most once in a certain theory context, to avoid race conditions with other concurrent accesses. \ declare [[smt_certificates = ""]] text \ The option \smt_read_only_certificates\ controls whether only stored certificates should be used or invocation of an SMT solver is allowed. When set to \true\, no SMT solver will ever be invoked and only the existing certificates found in the configured cache are used; when set to \false\ and there is no cached certificate for some proposition, then the configured SMT solver is invoked. \ declare [[smt_read_only_certificates = false]] subsection \Tracing\ text \ The SMT method, when applied, traces important information. To make it entirely silent, set the following option to \false\. \ declare [[smt_verbose = true]] text \ For tracing the generated problem file given to the SMT solver as well as the returned result of the solver, the option \smt_trace\ should be set to \true\. \ declare [[smt_trace = false]] subsection \Schematic rules for Z3 proof reconstruction\ text \ Several prof rules of Z3 are not very well documented. There are two lemma groups which can turn failing Z3 proof reconstruction attempts into succeeding ones: the facts in \z3_rule\ are tried prior to any implemented reconstruction procedure for all uncertain Z3 proof rules; the facts in \z3_simp\ are only fed to invocations of the simplifier when reconstructing theory-specific proof steps. \ lemmas [z3_rule] = refl eq_commute conj_commute disj_commute simp_thms nnf_simps ring_distribs field_simps times_divide_eq_right times_divide_eq_left if_True if_False not_not NO_MATCH_def lemma [z3_rule]: "(P \ Q) = (\ (\ P \ \ Q))" "(P \ Q) = (\ (\ Q \ \ P))" "(\ P \ Q) = (\ (P \ \ Q))" "(\ P \ Q) = (\ (\ Q \ P))" "(P \ \ Q) = (\ (\ P \ Q))" "(P \ \ Q) = (\ (Q \ \ P))" "(\ P \ \ Q) = (\ (P \ Q))" "(\ P \ \ Q) = (\ (Q \ P))" by auto lemma [z3_rule]: "(P \ Q) = (Q \ \ P)" "(\ P \ Q) = (P \ Q)" "(\ P \ Q) = (Q \ P)" "(True \ P) = P" "(P \ True) = True" "(False \ P) = True" "(P \ P) = True" "(\ (A \ \ B)) \ (A \ B)" by auto lemma [z3_rule]: "((P = Q) \ R) = (R \ (Q = (\ P)))" by auto lemma [z3_rule]: "(\ True) = False" "(\ False) = True" "(x = x) = True" "(P = True) = P" "(True = P) = P" "(P = False) = (\ P)" "(False = P) = (\ P)" "((\ P) = P) = False" "(P = (\ P)) = False" "((\ P) = (\ Q)) = (P = Q)" "\ (P = (\ Q)) = (P = Q)" "\ ((\ P) = Q) = (P = Q)" "(P \ Q) = (Q = (\ P))" "(P = Q) = ((\ P \ Q) \ (P \ \ Q))" "(P \ Q) = ((\ P \ \ Q) \ (P \ Q))" by auto lemma [z3_rule]: "(if P then P else \ P) = True" "(if \ P then \ P else P) = True" "(if P then True else False) = P" "(if P then False else True) = (\ P)" "(if P then Q else True) = ((\ P) \ Q)" "(if P then Q else True) = (Q \ (\ P))" "(if P then Q else \ Q) = (P = Q)" "(if P then Q else \ Q) = (Q = P)" "(if P then \ Q else Q) = (P = (\ Q))" "(if P then \ Q else Q) = ((\ Q) = P)" "(if \ P then x else y) = (if P then y else x)" "(if P then (if Q then x else y) else x) = (if P \ (\ Q) then y else x)" "(if P then (if Q then x else y) else x) = (if (\ Q) \ P then y else x)" "(if P then (if Q then x else y) else y) = (if P \ Q then x else y)" "(if P then (if Q then x else y) else y) = (if Q \ P then x else y)" "(if P then x else if P then y else z) = (if P then x else z)" "(if P then x else if Q then x else y) = (if P \ Q then x else y)" "(if P then x else if Q then x else y) = (if Q \ P then x else y)" "(if P then x = y else x = z) = (x = (if P then y else z))" "(if P then x = y else y = z) = (y = (if P then x else z))" "(if P then x = y else z = y) = (y = (if P then x else z))" by auto lemma [z3_rule]: "0 + (x::int) = x" "x + 0 = x" "x + x = 2 * x" "0 * x = 0" "1 * x = x" "x + y = y + x" by auto lemma [z3_rule]: (* for def-axiom *) "P = Q \ P \ Q" "P = Q \ \ P \ \ Q" "(\ P) = Q \ \ P \ Q" "(\ P) = Q \ P \ \ Q" "P = (\ Q) \ \ P \ Q" "P = (\ Q) \ P \ \ Q" "P \ Q \ P \ \ Q" "P \ Q \ \ P \ Q" "P \ (\ Q) \ P \ Q" "(\ P) \ Q \ P \ Q" "P \ Q \ P \ (\ Q)" "P \ Q \ (\ P) \ Q" "P \ \ Q \ P \ Q" "\ P \ Q \ P \ Q" "P \ y = (if P then x else y)" "P \ (if P then x else y) = y" "\ P \ x = (if P then x else y)" "\ P \ (if P then x else y) = x" "P \ R \ \ (if P then Q else R)" "\ P \ Q \ \ (if P then Q else R)" "\ (if P then Q else R) \ \ P \ Q" "\ (if P then Q else R) \ P \ R" "(if P then Q else R) \ \ P \ \ Q" "(if P then Q else R) \ P \ \ R" "(if P then \ Q else R) \ \ P \ Q" "(if P then Q else \ R) \ P \ R" by auto hide_type (open) symb_list pattern hide_const (open) Symb_Nil Symb_Cons trigger pat nopat fun_app z3div z3mod end diff --git a/src/HOL/Tools/SMT/smt_config.ML b/src/HOL/Tools/SMT/smt_config.ML --- a/src/HOL/Tools/SMT/smt_config.ML +++ b/src/HOL/Tools/SMT/smt_config.ML @@ -1,294 +1,294 @@ (* Title: HOL/Tools/SMT/smt_config.ML Author: Sascha Boehme, TU Muenchen Configuration options and diagnostic tools for SMT. *) signature SMT_CONFIG = sig (*solver*) type solver_info = { name: string, class: Proof.context -> SMT_Util.class, avail: unit -> bool, options: Proof.context -> string list } val add_solver: solver_info -> Context.generic -> Context.generic val set_solver_options: string * string -> Context.generic -> Context.generic val all_solvers_of: Proof.context -> string list val is_available: Proof.context -> string -> bool val available_solvers_of: Proof.context -> string list val select_solver: string -> Context.generic -> Context.generic val solver_of: Proof.context -> string val solver_class_of: Proof.context -> SMT_Util.class val solver_options_of: Proof.context -> string list (*options*) val oracle: bool Config.T val timeout: real Config.T val reconstruction_step_timeout: real Config.T val random_seed: int Config.T val read_only_certificates: bool Config.T val verbose: bool Config.T val trace: bool Config.T val statistics: bool Config.T val monomorph_limit: int Config.T val monomorph_instances: int Config.T val explicit_application: int Config.T val higher_order: bool Config.T val native_bv: bool Config.T val nat_as_int: bool Config.T val infer_triggers: bool Config.T val debug_files: string Config.T val sat_solver: string Config.T val compress_verit_proofs: Proof.context -> bool (*tools*) val get_timeout: Proof.context -> Time.time option val with_time_limit: Proof.context -> real Config.T -> ('a -> 'b) -> 'a -> 'b val with_timeout: Proof.context -> ('a -> 'b) -> 'a -> 'b (*diagnostics*) val trace_msg: Proof.context -> ('a -> string) -> 'a -> unit val verbose_msg: Proof.context -> ('a -> string) -> 'a -> unit val statistics_msg: Proof.context -> ('a -> string) -> 'a -> unit val verit_msg: Proof.context -> (unit -> 'a) -> unit val verit_arith_msg: Proof.context -> (unit -> 'a) -> unit val spy_verit: Proof.context -> bool val spy_Z3: Proof.context -> bool (*certificates*) val select_certificates: string -> Context.generic -> Context.generic val certificates_of: Proof.context -> Cache_IO.cache option (*setup*) val print_setup: Proof.context -> unit end; structure SMT_Config: SMT_CONFIG = struct (* solver *) type solver_info = { name: string, class: Proof.context -> SMT_Util.class, avail: unit -> bool, options: Proof.context -> string list} type data = { solvers: (solver_info * string list) Symtab.table, solver: string option, certs: Cache_IO.cache option} fun mk_data solvers solver certs: data = {solvers=solvers, solver=solver, certs=certs} val empty_data = mk_data Symtab.empty NONE NONE fun solvers_of ({solvers, ...}: data) = solvers fun solver_of ({solver, ...}: data) = solver fun certs_of ({certs, ...}: data) = certs fun map_solvers f ({solvers, solver, certs}: data) = mk_data (f solvers) solver certs fun map_solver f ({solvers, solver, certs}: data) = mk_data solvers (f solver) certs fun put_certs c ({solvers, solver, ...}: data) = mk_data solvers solver c fun merge_data ({solvers=ss1,solver=s1,certs=c1}: data, {solvers=ss2,solver=s2,certs=c2}: data) = mk_data (Symtab.merge (K true) (ss1, ss2)) (merge_options (s1, s2)) (merge_options (c1, c2)) structure Data = Generic_Data ( type T = data val empty = empty_data val merge = merge_data ) fun set_solver_options (name, options) = let val opts = String.tokens (Symbol.is_ascii_blank o str) options in Data.map (map_solvers (Symtab.map_entry name (apsnd (K opts)))) end fun add_solver (info as {name, ...} : solver_info) context = if Symtab.defined (solvers_of (Data.get context)) name then error ("Solver already registered: " ^ quote name) else context |> Data.map (map_solvers (Symtab.update (name, (info, [])))) |> Context.map_theory (Attrib.setup (Binding.name (name ^ "_options")) (Scan.lift (\<^keyword>\=\ |-- Args.name) >> (Thm.declaration_attribute o K o set_solver_options o pair name)) - ("additional command line options for SMT solver " ^ quote name)) + ("additional command-line options for SMT solver " ^ quote name)) fun all_solvers_of ctxt = Symtab.keys (solvers_of (Data.get (Context.Proof ctxt))) fun solver_name_of ctxt = solver_of (Data.get (Context.Proof ctxt)) fun is_available ctxt name = (case Symtab.lookup (solvers_of (Data.get (Context.Proof ctxt))) name of SOME ({avail, ...}, _) => avail () | NONE => false) fun available_solvers_of ctxt = filter (is_available ctxt) (all_solvers_of ctxt) fun warn_solver (Context.Proof ctxt) name = if Context_Position.is_visible ctxt then warning ("The SMT solver " ^ quote name ^ " is not installed") else () | warn_solver _ _ = () fun select_solver name context = let val ctxt = Context.proof_of context val upd = Data.map (map_solver (K (SOME name))) in if not (member (op =) (all_solvers_of ctxt) name) then error ("Trying to select unknown solver: " ^ quote name) else if not (is_available ctxt name) then (warn_solver context name; upd context) else upd context end fun no_solver_err () = error "No SMT solver selected" fun solver_of ctxt = (case solver_name_of ctxt of SOME name => name | NONE => no_solver_err ()) fun solver_info_of default select ctxt = (case solver_name_of ctxt of NONE => default () | SOME name => select (Symtab.lookup (solvers_of (Data.get (Context.Proof ctxt))) name)) fun solver_class_of ctxt = let fun class_of ({class, ...}: solver_info, _) = class ctxt in solver_info_of no_solver_err (class_of o the) ctxt end fun solver_options_of ctxt = let fun all_options NONE = [] | all_options (SOME ({options, ...} : solver_info, opts)) = opts @ options ctxt in solver_info_of (K []) all_options ctxt end val setup_solver = Attrib.setup \<^binding>\smt_solver\ (Scan.lift (\<^keyword>\=\ |-- Args.name) >> (Thm.declaration_attribute o K o select_solver)) "SMT solver configuration" (* options *) val oracle = Attrib.setup_config_bool \<^binding>\smt_oracle\ (K true) val timeout = Attrib.setup_config_real \<^binding>\smt_timeout\ (K 0.0) val reconstruction_step_timeout = Attrib.setup_config_real \<^binding>\smt_reconstruction_step_timeout\ (K 10.0) val random_seed = Attrib.setup_config_int \<^binding>\smt_random_seed\ (K 1) val read_only_certificates = Attrib.setup_config_bool \<^binding>\smt_read_only_certificates\ (K false) val verbose = Attrib.setup_config_bool \<^binding>\smt_verbose\ (K true) val trace = Attrib.setup_config_bool \<^binding>\smt_trace\ (K false) val trace_verit = Attrib.setup_config_bool \<^binding>\smt_debug_verit\ (K false) val spy_verit_attr = Attrib.setup_config_bool \<^binding>\smt_spy_verit\ (K false) val spy_z3 = Attrib.setup_config_bool \<^binding>\smt_spy_z3\ (K false) val trace_arith_verit = Attrib.setup_config_bool \<^binding>\smt_debug_arith_verit\ (K false) val trace_verit_compression = Attrib.setup_config_bool \<^binding>\verit_compress_proofs\ (K true) val statistics = Attrib.setup_config_bool \<^binding>\smt_statistics\ (K false) val monomorph_limit = Attrib.setup_config_int \<^binding>\smt_monomorph_limit\ (K 10) val monomorph_instances = Attrib.setup_config_int \<^binding>\smt_monomorph_instances\ (K 500) val explicit_application = Attrib.setup_config_int \<^binding>\smt_explicit_application\ (K 1) val higher_order = Attrib.setup_config_bool \<^binding>\smt_higher_order\ (K false) val native_bv = Attrib.setup_config_bool \<^binding>\native_bv\ (K true) val nat_as_int = Attrib.setup_config_bool \<^binding>\smt_nat_as_int\ (K false) val infer_triggers = Attrib.setup_config_bool \<^binding>\smt_infer_triggers\ (K false) val debug_files = Attrib.setup_config_string \<^binding>\smt_debug_files\ (K "") val sat_solver = Attrib.setup_config_string \<^binding>\smt_sat_solver\ (K "cdclite") (* diagnostics *) fun cond_trace flag f x = if flag then tracing ("SMT: " ^ f x) else () fun verbose_msg ctxt = cond_trace (Config.get ctxt verbose) fun trace_msg ctxt = cond_trace (Config.get ctxt trace) fun statistics_msg ctxt = cond_trace (Config.get ctxt statistics) fun verit_msg ctxt (x : unit -> 'a) = if (Config.get ctxt trace_verit) then ignore(x ()) else () fun verit_arith_msg ctxt (x : unit -> 'a) = if (Config.get ctxt trace_arith_verit) then ignore(x ()) else () fun spy_verit ctxt = Config.get ctxt spy_verit_attr fun spy_Z3 ctxt = Config.get ctxt spy_z3 fun compress_verit_proofs ctxt = Config.get ctxt trace_verit_compression (* tools *) fun get_timeout ctxt = let val t = seconds (Config.get ctxt timeout); in if Timeout.ignored t then NONE else SOME (Timeout.scale_time t) end; fun with_time_limit ctxt timeout_config f x = Timeout.apply (seconds (Config.get ctxt timeout_config)) f x handle Timeout.TIMEOUT _ => raise SMT_Failure.SMT SMT_Failure.Time_Out fun with_timeout ctxt = with_time_limit ctxt timeout (* certificates *) val certificates_of = certs_of o Data.get o Context.Proof val get_certificates_path = Option.map (Cache_IO.cache_path_of) o certificates_of fun select_certificates name context = context |> Data.map (put_certs ( if name = "" then NONE else (Resources.master_directory (Context.theory_of context) + Path.explode name) |> SOME o Cache_IO.unsynchronized_init)) val setup_certificates = Attrib.setup \<^binding>\smt_certificates\ (Scan.lift (\<^keyword>\=\ |-- Args.name) >> (Thm.declaration_attribute o K o select_certificates)) "SMT certificates configuration" (* setup *) val _ = Theory.setup ( setup_solver #> setup_certificates) fun print_setup ctxt = let fun string_of_bool b = if b then "true" else "false" val names = available_solvers_of ctxt val ns = if null names then ["(none)"] else sort_strings names val n = the_default "(none)" (solver_name_of ctxt) val opts = solver_options_of ctxt val t = string_of_real (Config.get ctxt timeout) val certs_filename = (case get_certificates_path ctxt of SOME path => Path.print path | NONE => "(disabled)") in Pretty.writeln (Pretty.big_list "SMT setup:" [ Pretty.str ("Current SMT solver: " ^ n), Pretty.str ("Current SMT solver options: " ^ space_implode " " opts), Pretty.str_list "Available SMT solvers: " "" ns, Pretty.str ("Current timeout: " ^ t ^ " seconds"), Pretty.str ("With proofs: " ^ string_of_bool (not (Config.get ctxt oracle))), Pretty.str ("Certificates cache: " ^ certs_filename), Pretty.str ("Fixed certificates: " ^ string_of_bool (Config.get ctxt read_only_certificates))]) end val _ = Outer_Syntax.command \<^command_keyword>\smt_status\ "show the available SMT solvers, the currently selected SMT solver, \ \and the values of SMT configuration options" (Scan.succeed (Toplevel.keep (print_setup o Toplevel.context_of))) end; diff --git a/src/HOL/Tools/SMT/smt_solver.ML b/src/HOL/Tools/SMT/smt_solver.ML --- a/src/HOL/Tools/SMT/smt_solver.ML +++ b/src/HOL/Tools/SMT/smt_solver.ML @@ -1,318 +1,318 @@ (* Title: HOL/Tools/SMT/smt_solver.ML Author: Sascha Boehme, TU Muenchen SMT solvers registry and SMT tactic. *) signature SMT_SOLVER = sig (*configuration*) datatype outcome = Unsat | Sat | Unknown | Time_Out type parsed_proof = {outcome: SMT_Failure.failure option, fact_ids: (int * ((string * ATP_Problem_Generate.stature) * thm)) list option, atp_proof: unit -> (term, string) ATP_Proof.atp_step list} type solver_config = {name: string, class: Proof.context -> SMT_Util.class, avail: unit -> bool, command: unit -> string list, options: Proof.context -> string list, smt_options: (string * string) list, - good_slices: (int * string) list, + good_slices: ((int * string) * string list) list, outcome: string -> string list -> outcome * string list, parse_proof: (Proof.context -> SMT_Translate.replay_data -> ((string * ATP_Problem_Generate.stature) * thm) list -> term list -> term -> string list -> parsed_proof) option, replay: (Proof.context -> SMT_Translate.replay_data -> string list -> thm) option} (*registry*) val add_solver: solver_config -> theory -> theory - val good_slices: Proof.context -> string -> (int * string) list + val good_slices: Proof.context -> string -> ((int * string) * string list) list (*filter*) val smt_filter: Proof.context -> thm -> ((string * ATP_Problem_Generate.stature) * thm) list -> - int -> Time.time -> parsed_proof + int -> Time.time -> string list -> parsed_proof (*tactic*) val smt_tac: Proof.context -> thm list -> int -> tactic val smt_tac': Proof.context -> thm list -> int -> tactic end; structure SMT_Solver: SMT_SOLVER = struct (* interface to external solvers *) local fun make_command command options problem_path proof_path = Bash.strings (command () @ options) ^ " " ^ File.bash_platform_path problem_path ^ " > " ^ File.bash_path proof_path ^ " 2>&1" fun with_trace ctxt msg f x = let val _ = SMT_Config.trace_msg ctxt (fn () => msg) () in f x end fun run ctxt name mk_cmd input = (case SMT_Config.certificates_of ctxt of NONE => if not (SMT_Config.is_available ctxt name) then error ("The SMT solver " ^ quote name ^ " is not installed") else if Config.get ctxt SMT_Config.debug_files = "" then with_trace ctxt ("Invoking SMT solver " ^ quote name ^ " ...") (Cache_IO.run mk_cmd) input else let val base_path = Path.explode (Config.get ctxt SMT_Config.debug_files) val in_path = Path.ext "smt_in" base_path val out_path = Path.ext "smt_out" base_path in Cache_IO.raw_run mk_cmd input in_path out_path end | SOME certs => (case Cache_IO.lookup certs input of (NONE, key) => if Config.get ctxt SMT_Config.read_only_certificates then error ("Bad certificate cache: missing certificate") else Cache_IO.run_and_cache certs key mk_cmd input | (SOME output, _) => with_trace ctxt ("Using cached certificate from " ^ Path.print (Cache_IO.cache_path_of certs) ^ " ...") I output)) (* Z3 and cvc returns 1 if "get-proof" or "get-model" fails. veriT returns 255 in that case and 14 for timeouts. *) fun normal_return_codes "z3" = [0, 1] | normal_return_codes "verit" = [0, 14, 255] | normal_return_codes _ = [0, 1] fun run_solver ctxt name mk_cmd input = let fun pretty tag lines = Pretty.string_of (Pretty.big_list tag (map Pretty.str lines)) val _ = SMT_Config.trace_msg ctxt (pretty "Problem:" o split_lines) input val ({elapsed, ...}, {redirected_output = res, output = err, return_code}) = Timing.timing (SMT_Config.with_timeout ctxt (run ctxt name mk_cmd)) input val _ = SMT_Config.trace_msg ctxt (pretty "Solver:") err val output = drop_suffix (equal "") res val _ = SMT_Config.trace_msg ctxt (pretty "Result:") output val _ = SMT_Config.trace_msg ctxt (pretty "Time:") [Value.print_time elapsed ^ "s"] val _ = SMT_Config.statistics_msg ctxt (pretty "Time:") [Value.print_time elapsed ^ "s"] val _ = member (op =) (normal_return_codes name) return_code orelse raise SMT_Failure.SMT (SMT_Failure.Abnormal_Termination return_code) in output end fun trace_assms ctxt = SMT_Config.trace_msg ctxt (Pretty.string_of o Pretty.big_list "Assertions:" o map (Thm.pretty_thm ctxt o snd)) fun trace_replay_data ({context = ctxt, typs, terms, ...} : SMT_Translate.replay_data) = let fun pretty_eq n p = Pretty.block [Pretty.str n, Pretty.str " = ", p] fun p_typ (n, T) = pretty_eq n (Syntax.pretty_typ ctxt T) fun p_term (n, t) = pretty_eq n (Syntax.pretty_term ctxt t) in SMT_Config.trace_msg ctxt (fn () => Pretty.string_of (Pretty.big_list "Names:" [ Pretty.big_list "sorts:" (map p_typ (Symtab.dest typs)), Pretty.big_list "functions:" (map p_term (Symtab.dest terms))])) () end in -fun invoke name command smt_options ithms ctxt = +fun invoke name command options smt_options ithms ctxt = let - val options = SMT_Config.solver_options_of ctxt + val options = options @ SMT_Config.solver_options_of ctxt val comments = [space_implode " " options] val (str, replay_data as {context = ctxt', ...}) = ithms |> tap (trace_assms ctxt) |> SMT_Translate.translate ctxt name smt_options comments ||> tap trace_replay_data in (run_solver ctxt' name (make_command command options) str, replay_data) end end (* configuration *) datatype outcome = Unsat | Sat | Unknown | Time_Out type parsed_proof = {outcome: SMT_Failure.failure option, fact_ids: (int * ((string * ATP_Problem_Generate.stature) * thm)) list option, atp_proof: unit -> (term, string) ATP_Proof.atp_step list} type solver_config = {name: string, class: Proof.context -> SMT_Util.class, avail: unit -> bool, command: unit -> string list, options: Proof.context -> string list, smt_options: (string * string) list, - good_slices: (int * string) list, + good_slices: ((int * string) * string list) list, outcome: string -> string list -> outcome * string list, parse_proof: (Proof.context -> SMT_Translate.replay_data -> ((string * ATP_Problem_Generate.stature) * thm) list -> term list -> term -> string list -> parsed_proof) option, replay: (Proof.context -> SMT_Translate.replay_data -> string list -> thm) option} (* check well-sortedness *) val has_topsort = Term.exists_type (Term.exists_subtype (fn TFree (_, []) => true | TVar (_, []) => true | _ => false)) (* top sorts cause problems with atomization *) fun check_topsort ctxt thm = if has_topsort (Thm.prop_of thm) then (SMT_Normalize.drop_fact_warning ctxt thm; TrueI) else thm (* registry *) type solver_info = { command: unit -> string list, smt_options: (string * string) list, - good_slices: (int * string) list, + good_slices: ((int * string) * string list) list, parse_proof: Proof.context -> SMT_Translate.replay_data -> ((string * ATP_Problem_Generate.stature) * thm) list -> term list -> term -> string list -> parsed_proof, replay: Proof.context -> SMT_Translate.replay_data -> string list -> thm} structure Solvers = Generic_Data ( type T = solver_info Symtab.table val empty = Symtab.empty fun merge data = Symtab.merge (K true) data ) local fun parse_proof outcome parse_proof0 outer_ctxt replay_data xfacts prems concl output = (case outcome output of (Unsat, lines) => (case parse_proof0 of SOME pp => pp outer_ctxt replay_data xfacts prems concl lines | NONE => {outcome = NONE, fact_ids = NONE, atp_proof = K []}) | (Time_Out, _) => raise SMT_Failure.SMT (SMT_Failure.Time_Out) | (result, _) => raise SMT_Failure.SMT (SMT_Failure.Counterexample (result = Sat))) fun replay outcome replay0 oracle outer_ctxt (replay_data as {context = ctxt, ...} : SMT_Translate.replay_data) output = (case outcome output of (Unsat, lines) => if Config.get ctxt SMT_Config.oracle then oracle () else (case replay0 of SOME replay => replay outer_ctxt replay_data lines | NONE => error "No proof reconstruction for solver -- \ \declare [[smt_oracle]] to allow oracle") | (Time_Out, _) => raise SMT_Failure.SMT (SMT_Failure.Time_Out) | (result, _) => raise SMT_Failure.SMT (SMT_Failure.Counterexample (result = Sat))) val cfalse = Thm.cterm_of \<^context> \<^prop>\False\ in fun add_solver ({name, class, avail, command, options, smt_options, good_slices, outcome, parse_proof = parse_proof0, replay = replay0} : solver_config) = let fun solver oracle = { command = command, smt_options = smt_options, good_slices = good_slices, parse_proof = parse_proof (outcome name) parse_proof0, replay = replay (outcome name) replay0 oracle} val info = {name = name, class = class, avail = avail, options = options} in Thm.add_oracle (Binding.name name, K cfalse) #-> (fn (_, oracle) => Context.theory_map (Solvers.map (Symtab.update_new (name, solver oracle)))) #> Context.theory_map (SMT_Config.add_solver info) end end fun get_info ctxt name = the (Symtab.lookup (Solvers.get (Context.Proof ctxt)) name) fun name_and_info_of ctxt = let val name = SMT_Config.solver_of ctxt in (name, get_info ctxt name) end val good_slices = #good_slices oo get_info fun apply_solver_and_replay ctxt thms0 = let val thms = map (check_topsort ctxt) thms0 val (name, {command, smt_options, replay, ...}) = name_and_info_of ctxt val (output, replay_data) = - invoke name command smt_options (SMT_Normalize.normalize ctxt thms) ctxt + invoke name command [] smt_options (SMT_Normalize.normalize ctxt thms) ctxt in replay ctxt replay_data output end (* filter (for Sledgehammer) *) -fun smt_filter ctxt0 goal xfacts i time_limit = +fun smt_filter ctxt0 goal xfacts i time_limit options = let val ctxt = ctxt0 |> Config.put SMT_Config.timeout (Time.toReal time_limit) val ({context = ctxt, prems, concl, ...}, _) = Subgoal.focus ctxt i NONE goal fun negate ct = Thm.dest_comb ct ||> Thm.apply \<^cterm>\Not\ |-> Thm.apply val cprop = (case try negate (Thm.rhs_of (SMT_Normalize.atomize_conv ctxt concl)) of SOME ct => ct | NONE => raise SMT_Failure.SMT (SMT_Failure.Other_Failure "cannot atomize goal")) val conjecture = Thm.assume cprop val facts = map snd xfacts val thms = conjecture :: prems @ facts val thms' = map (check_topsort ctxt) thms val (name, {command, smt_options, parse_proof, ...}) = name_and_info_of ctxt val (output, replay_data) = - invoke name command smt_options (SMT_Normalize.normalize ctxt thms') ctxt + invoke name command options smt_options (SMT_Normalize.normalize ctxt thms') ctxt in parse_proof ctxt replay_data xfacts (map Thm.prop_of prems) (Thm.term_of concl) output end handle SMT_Failure.SMT fail => {outcome = SOME fail, fact_ids = NONE, atp_proof = K []} (* SMT tactic *) local fun str_of ctxt fail = "Solver " ^ SMT_Config.solver_of ctxt ^ ": " ^ SMT_Failure.string_of_failure fail fun safe_solve ctxt facts = SOME (apply_solver_and_replay ctxt facts) handle SMT_Failure.SMT (fail as SMT_Failure.Counterexample _) => (SMT_Config.verbose_msg ctxt (str_of ctxt) fail; NONE) | SMT_Failure.SMT (fail as SMT_Failure.Time_Out) => (SMT_Config.verbose_msg ctxt (K ("SMT: Solver " ^ quote (SMT_Config.solver_of ctxt) ^ ": " ^ SMT_Failure.string_of_failure fail ^ " (setting the " ^ "configuration option " ^ quote (Config.name_of SMT_Config.timeout) ^ " might help)")) (); NONE) | SMT_Failure.SMT fail => error (str_of ctxt fail) fun resolve ctxt (SOME thm) = resolve_tac ctxt [thm] 1 | resolve _ NONE = no_tac fun tac prove ctxt rules = CONVERSION (SMT_Normalize.atomize_conv ctxt) THEN' resolve_tac ctxt @{thms ccontr} THEN' SUBPROOF (fn {context = ctxt', prems, ...} => resolve ctxt' (prove ctxt' (rules @ prems))) ctxt in val smt_tac = tac safe_solve val smt_tac' = tac (SOME oo apply_solver_and_replay) end end; diff --git a/src/HOL/Tools/SMT/smt_systems.ML b/src/HOL/Tools/SMT/smt_systems.ML --- a/src/HOL/Tools/SMT/smt_systems.ML +++ b/src/HOL/Tools/SMT/smt_systems.ML @@ -1,233 +1,234 @@ (* Title: HOL/Tools/SMT/smt_systems.ML Author: Sascha Boehme, TU Muenchen Setup SMT solvers. *) signature SMT_SYSTEMS = sig val cvc4_extensions: bool Config.T val z3_extensions: bool Config.T end; structure SMT_Systems: SMT_SYSTEMS = struct val mashN = "mash" val mepoN = "mepo" val meshN = "mesh" (* helper functions *) fun check_tool var () = (case getenv var of "" => NONE | s => if File.is_file (Path.variable var |> Path.expand |> Path.platform_exe) then SOME [s] else NONE); fun make_avail name () = getenv (name ^ "_SOLVER") <> "" fun make_command name () = [getenv (name ^ "_SOLVER")] fun outcome_of unsat sat unknown timeout solver_name line = if String.isPrefix unsat line then SMT_Solver.Unsat else if String.isPrefix sat line then SMT_Solver.Sat else if String.isPrefix unknown line then SMT_Solver.Unknown else if String.isPrefix timeout line then SMT_Solver.Time_Out else raise SMT_Failure.SMT (SMT_Failure.Other_Failure ("Solver " ^ quote solver_name ^ " failed -- enable tracing using the " ^ quote (Config.name_of SMT_Config.trace) ^ " option for details")) (* When used with bitvectors, CVC4 can produce error messages like: $ISABELLE_TMP_PREFIX/... No set-logic command was given before this point. These message should be ignored. *) fun is_blank_or_error_line "" = true | is_blank_or_error_line s = String.isPrefix "(error " s orelse String.isPrefix (getenv "ISABELLE_TMP_PREFIX") s fun on_first_line test_outcome solver_name lines = let val split_first = (fn [] => ("", []) | l :: ls => (l, ls)) val (l, ls) = split_first (drop_prefix is_blank_or_error_line lines) in (test_outcome solver_name l, ls) end fun on_first_non_unsupported_line test_outcome solver_name lines = on_first_line test_outcome solver_name (filter (curry (op <>) "unsupported") lines) (* CVC4 *) val cvc4_extensions = Attrib.setup_config_bool \<^binding>\cvc4_extensions\ (K false) local fun cvc4_options ctxt = ["--no-stats", "--random-seed=" ^ string_of_int (Config.get ctxt SMT_Config.random_seed), "--lang=smt2"] @ (case SMT_Config.get_timeout ctxt of NONE => [] | SOME t => ["--tlimit", string_of_int (Time.toMilliseconds t)]) fun select_class ctxt = if Config.get ctxt cvc4_extensions then if Config.get ctxt SMT_Config.higher_order then CVC4_Interface.hosmtlib_cvc4C else CVC4_Interface.smtlib_cvc4C else if Config.get ctxt SMT_Config.higher_order then SMTLIB_Interface.hosmtlibC else if Config.get ctxt SMT_Config.native_bv then SMTLIB_Interface.bvsmlibC else SMTLIB_Interface.smtlibC in val cvc4: SMT_Solver.solver_config = { name = "cvc4", class = select_class, avail = make_avail "CVC4", command = make_command "CVC4", options = cvc4_options, smt_options = [(":produce-unsat-cores", "true")], good_slices = (* FUDGE *) - [(512, meshN), - (64, meshN), - (1024, meshN), - (256, mepoN), - (32, meshN), - (128, meshN)], + [((512, meshN), ["--full-saturate-quant", "--inst-when=full-last-call", "--inst-no-entail", "--term-db-mode=relevant", "--multi-trigger-linear"]), + ((64, meshN), ["--decision=internal", "--simplification=none", "--full-saturate-quant"]), + ((1024, meshN), ["--relevant-triggers", "--full-saturate-quant"]), + ((256, mepoN), ["--trigger-sel=max", "--full-saturate-quant"]), + ((32, meshN), ["--term-db-mode=relevant", "--full-saturate-quant"]), + ((128, meshN), ["--no-e-matching", "--full-saturate-quant"]), + ((256, meshN), ["--finite-model-find", "--fmf-inst-engine"])], outcome = on_first_line (outcome_of "unsat" "sat" "unknown" "timeout"), parse_proof = SOME (K CVC4_Proof_Parse.parse_proof), replay = NONE } end (* veriT *) local fun select_class ctxt = if Config.get ctxt SMT_Config.higher_order then SMTLIB_Interface.hosmtlibC else SMTLIB_Interface.smtlibC fun veriT_options ctxt = ["--proof-with-sharing", "--proof-define-skolems", "--proof-prune", "--proof-merge", "--disable-print-success", "--disable-banner"] @ Verit_Proof.veriT_current_strategy (Context.Proof ctxt) @ (case SMT_Config.get_timeout ctxt of NONE => [] | SOME t => ["--max-time=" ^ string_of_int (Time.toMilliseconds t)]) in val veriT: SMT_Solver.solver_config = { name = "verit", class = select_class, avail = is_some o check_tool "ISABELLE_VERIT", command = the o check_tool "ISABELLE_VERIT", options = veriT_options, smt_options = [(":produce-proofs", "true")], good_slices = (* FUDGE *) - [(1024, meshN), - (512, mashN), - (64, meshN), - (128, meshN), - (256, mepoN), - (32, meshN)], + [((1024, meshN), []), + ((512, mashN), []), + ((64, meshN), []), + ((128, meshN), []), + ((256, mepoN), []), + ((32, meshN), [])], outcome = on_first_non_unsupported_line (outcome_of "unsat" "sat" "unknown" "Time limit exceeded"), parse_proof = SOME (K VeriT_Proof_Parse.parse_proof), replay = SOME Verit_Replay.replay } end (* Z3 *) val z3_extensions = Attrib.setup_config_bool \<^binding>\z3_extensions\ (K false) local fun z3_options ctxt = ["smt.random_seed=" ^ string_of_int (Config.get ctxt SMT_Config.random_seed), "smt.refine_inj_axioms=false"] @ (case SMT_Config.get_timeout ctxt of NONE => [] | SOME t => ["-T:" ^ string_of_int (Real.ceil (Time.toReal t))]) @ ["-smt2"] fun select_class ctxt = if Config.get ctxt z3_extensions then Z3_Interface.smtlib_z3C else if Config.get ctxt SMT_Config.native_bv then SMTLIB_Interface.bvsmlibC else SMTLIB_Interface.smtlibC in val z3: SMT_Solver.solver_config = { name = "z3", class = select_class, avail = make_avail "Z3", command = make_command "Z3", options = z3_options, smt_options = [(":produce-proofs", "true")], good_slices = (* FUDGE *) - [(1024, meshN), - (512, mepoN), - (64, meshN), - (256, meshN), - (128, mashN), - (32, meshN)], + [((1024, meshN), []), + ((512, mepoN), []), + ((64, meshN), []), + ((256, meshN), []), + ((128, mashN), []), + ((32, meshN), [])], outcome = on_first_line (outcome_of "unsat" "sat" "unknown" "timeout"), parse_proof = SOME Z3_Replay.parse_proof, replay = SOME Z3_Replay.replay } end (* smt tactic *) val parse_smt_options = Scan.optional (Args.parens (Args.name -- Scan.option (\<^keyword>\,\ |-- Args.name)) >> apfst SOME) (NONE, NONE) fun smt_method ((solver, stgy), thms) ctxt facts = let val default_solver = SMT_Config.solver_of ctxt val solver = the_default default_solver solver val _ = if solver = "z3" andalso stgy <> NONE then warning ("No strategy is available for z3. Ignoring " ^ quote (the stgy)) else () val ctxt = ctxt |> (if stgy <> NONE then Context.proof_map (Verit_Proof.select_veriT_stgy (the stgy)) else I) |> Context.Proof |> SMT_Config.select_solver solver |> Context.proof_of in HEADGOAL (SOLVED' (SMT_Solver.smt_tac ctxt (thms @ facts))) end val _ = Theory.setup (Method.setup \<^binding>\smt\ (Scan.lift parse_smt_options -- Attrib.thms >> (METHOD oo smt_method)) "Call to the SMT solvers veriT or z3") (* overall setup *) val _ = Theory.setup ( SMT_Solver.add_solver cvc4 #> SMT_Solver.add_solver veriT #> SMT_Solver.add_solver z3) end; diff --git a/src/HOL/Tools/Sledgehammer/sledgehammer.ML b/src/HOL/Tools/Sledgehammer/sledgehammer.ML --- a/src/HOL/Tools/Sledgehammer/sledgehammer.ML +++ b/src/HOL/Tools/Sledgehammer/sledgehammer.ML @@ -1,465 +1,467 @@ (* Title: HOL/Tools/Sledgehammer/sledgehammer.ML Author: Fabian Immler, TU Muenchen Author: Makarius Author: Jasmin Blanchette, TU Muenchen Sledgehammer's heart. *) signature SLEDGEHAMMER = sig type stature = ATP_Problem_Generate.stature type fact = Sledgehammer_Fact.fact type fact_override = Sledgehammer_Fact.fact_override type proof_method = Sledgehammer_Proof_Methods.proof_method type play_outcome = Sledgehammer_Proof_Methods.play_outcome type mode = Sledgehammer_Prover.mode type params = Sledgehammer_Prover.params type induction_rules = Sledgehammer_Prover.induction_rules type prover_problem = Sledgehammer_Prover.prover_problem type prover_result = Sledgehammer_Prover.prover_result datatype sledgehammer_outcome = SH_Some of prover_result | SH_Unknown | SH_Timeout | SH_None val short_string_of_sledgehammer_outcome : sledgehammer_outcome -> string val play_one_line_proof : bool -> Time.time -> (string * stature) list -> Proof.state -> int -> proof_method * proof_method list list -> (string * stature) list * (proof_method * play_outcome) val string_of_factss : (string * fact list) list -> string val run_sledgehammer : params -> mode -> (string -> unit) option -> int -> fact_override -> Proof.state -> bool * (sledgehammer_outcome * string) end; structure Sledgehammer : SLEDGEHAMMER = struct open ATP_Util open ATP_Problem open ATP_Proof open ATP_Problem_Generate open Sledgehammer_Util open Sledgehammer_Fact open Sledgehammer_Proof_Methods open Sledgehammer_Isar_Proof open Sledgehammer_Isar_Preplay open Sledgehammer_Isar_Minimize open Sledgehammer_ATP_Systems open Sledgehammer_Prover open Sledgehammer_Prover_ATP open Sledgehammer_Prover_Minimize open Sledgehammer_MaSh datatype sledgehammer_outcome = SH_Some of prover_result | SH_Unknown | SH_Timeout | SH_None fun short_string_of_sledgehammer_outcome (SH_Some _) = "some" | short_string_of_sledgehammer_outcome SH_Unknown = "unknown" | short_string_of_sledgehammer_outcome SH_Timeout = "timeout" | short_string_of_sledgehammer_outcome SH_None = "none" fun alternative f (SOME x) (SOME y) = SOME (f (x, y)) | alternative _ (x as SOME _) NONE = x | alternative _ NONE (y as SOME _) = y | alternative _ NONE NONE = NONE fun max_outcome outcomes = let val some = find_first (fn (SH_Some _, _) => true | _ => false) outcomes val unknown = find_first (fn (SH_Unknown, _) => true | _ => false) outcomes val timeout = find_first (fn (SH_Timeout, _) => true | _ => false) outcomes val none = find_first (fn (SH_None, _) => true | _ => false) outcomes in some |> alternative snd unknown |> alternative snd timeout |> alternative snd none |> the_default (SH_Unknown, "") end fun play_one_line_proof minimize timeout used_facts state i (preferred_meth, methss) = (if timeout = Time.zeroTime then (used_facts, (preferred_meth, Play_Timed_Out Time.zeroTime)) else let val ctxt = Proof.context_of state val fact_names = used_facts |> filter_out (fn (_, (sc, _)) => sc = Chained) |> map fst val {facts = chained, goal, ...} = Proof.goal state val goal_t = Logic.get_goal (Thm.prop_of goal) i fun try_methss [] [] = (used_facts, (preferred_meth, Play_Timed_Out Time.zeroTime)) | try_methss ress [] = (used_facts, (case AList.lookup (op =) ress preferred_meth of SOME play => (preferred_meth, play) | NONE => hd (sort (play_outcome_ord o apply2 snd) (rev ress)))) | try_methss ress (meths :: methss) = let fun mk_step fact_names meths = Prove { qualifiers = [], obtains = [], label = ("", 0), goal = goal_t, subproofs = [], facts = ([], fact_names), proof_methods = meths, comment = ""} in (case preplay_isar_step ctxt chained timeout [] (mk_step fact_names meths) of (res as (meth, Played time)) :: _ => if not minimize then (used_facts, res) else let val (time', used_names') = minimized_isar_step ctxt chained time (mk_step fact_names [meth]) ||> (facts_of_isar_step #> snd) val used_facts' = filter (member (op =) used_names' o fst) used_facts in (used_facts', (meth, Played time')) end | ress' => try_methss (ress' @ ress) methss) end in try_methss [] methss end) |> (fn (used_facts, (meth, play)) => (used_facts |> filter_out (fn (_, (sc, _)) => sc = Chained), (meth, play))) fun launch_prover (params as {verbose, spy, slices, timeout, ...}) mode learn (problem as {state, subgoal, factss, ...} : prover_problem) (slice as ((num_facts, fact_filter), _)) name = let val ctxt = Proof.context_of state val _ = spying spy (fn () => (state, subgoal, name, "Launched")) val _ = if verbose then writeln (name ^ " with " ^ string_of_int num_facts ^ " " ^ fact_filter ^ " fact" ^ plural_s num_facts ^ " for " ^ string_of_time (slice_timeout slices timeout) ^ "...") else () fun print_used_facts used_facts used_from = tag_list 1 used_from |> map (fn (j, fact) => fact |> apsnd (K j)) |> filter_used_facts false used_facts |> map (fn ((name, _), j) => name ^ "@" ^ string_of_int j) |> commas |> prefix ("Facts in " ^ name ^ " proof: ") |> writeln fun spying_str_of_res ({outcome = NONE, used_facts, used_from, ...} : prover_result) = let val num_used_facts = length used_facts fun find_indices facts = tag_list 1 facts |> map (fn (j, fact) => fact |> apsnd (K j)) |> filter_used_facts false used_facts |> distinct (eq_fst (op =)) |> map (prefix "@" o string_of_int o snd) fun filter_info (fact_filter, facts) = let val indices = find_indices facts (* "Int.max" is there for robustness *) val unknowns = replicate (Int.max (0, num_used_facts - length indices)) "?" in (commas (indices @ unknowns), fact_filter) end val filter_infos = map filter_info (("actual", used_from) :: factss) |> AList.group (op =) |> map (fn (indices, fact_filters) => commas fact_filters ^ ": " ^ indices) in "Success: Found proof with " ^ string_of_int num_used_facts ^ " fact" ^ plural_s num_used_facts ^ (if num_used_facts = 0 then "" else ": " ^ commas filter_infos) end | spying_str_of_res {outcome = SOME failure, ...} = "Failure: " ^ string_of_atp_failure failure in get_minimizing_prover ctxt mode learn name params problem slice |> verbose ? tap (fn {outcome = NONE, used_facts as _ :: _, used_from, ...} => print_used_facts used_facts used_from | _ => ()) |> spy ? tap (fn res => spying spy (fn () => (state, subgoal, name, spying_str_of_res res))) end fun preplay_prover_result ({ minimize, preplay_timeout, ...} : params) state subgoal (result as {outcome, used_facts, preferred_methss, message, ...} : prover_result) = let val output = if outcome = SOME ATP_Proof.TimedOut then SH_Timeout else if is_some outcome then SH_None else SH_Some result fun output_message () = message (fn () => play_one_line_proof minimize preplay_timeout used_facts state subgoal preferred_methss) in (output, output_message) end fun check_expected_outcome ctxt prover_name expect outcome = let val outcome_code = short_string_of_sledgehammer_outcome outcome in (* The "expect" argument is deliberately ignored if the prover is missing so that "Metis_Examples" can be processed on any machine. *) if expect = "" orelse outcome_code = expect orelse not (is_prover_installed ctxt prover_name) then () else error ("Unexpected outcome: " ^ quote outcome_code) end fun launch_prover_and_preplay (params as {debug, timeout, expect, ...}) mode writeln_result learn (problem as {state, subgoal, ...}) slice prover_name = let val ctxt = Proof.context_of state val hard_timeout = Time.scale 5.0 timeout fun really_go () = launch_prover params mode learn problem slice prover_name |> preplay_prover_result params state subgoal fun go () = if debug then really_go () else (really_go () handle ERROR msg => (SH_Unknown, fn () => "Error: " ^ msg ^ "\n") | exn => if Exn.is_interrupt exn then Exn.reraise exn else (SH_Unknown, fn () => "Internal error:\n" ^ Runtime.exn_message exn ^ "\n")) val (outcome, message) = Timeout.apply hard_timeout go () val () = check_expected_outcome ctxt prover_name expect outcome val message = message () val () = if mode = Auto_Try then () else (case outcome of SH_Some _ => the_default writeln writeln_result (prover_name ^ ": " ^ message) | _ => ()) in (outcome, message) end fun string_of_facts filter facts = "Selected " ^ string_of_int (length facts) ^ " " ^ (if filter = "" then "" else filter ^ " ") ^ "fact" ^ plural_s (length facts) ^ ": " ^ (space_implode " " (map (fst o fst) facts)) fun string_of_factss factss = if forall (null o snd) factss then "Found no relevant facts" else cat_lines (map (fn (filter, facts) => string_of_facts filter facts) factss) val default_slice_schedule = (* FUDGE (based on Seventeen evaluation) *) [cvc4N, zipperpositionN, vampireN, veritN, eN, cvc4N, zipperpositionN, cvc4N, vampireN, cvc4N, cvc4N, vampireN, cvc4N, eN, iproverN, zipperpositionN, vampireN, eN, vampireN, zipperpositionN, z3N, cvc4N, vampireN, iproverN, vampireN, zipperpositionN, z3N, z3N, cvc4N, cvc4N] fun schedule_of_provers provers num_slices = let val (known_provers, unknown_provers) = List.partition (member (op =) default_slice_schedule) provers val default_slice_schedule = filter (member (op =) known_provers) default_slice_schedule val num_default_slices = length default_slice_schedule fun round_robin _ [] = [] | round_robin 0 _ = [] | round_robin n (prover :: provers) = prover :: round_robin (n - 1) (provers @ [prover]) in if num_slices <= num_default_slices then take num_slices default_slice_schedule else default_slice_schedule @ round_robin (num_slices - num_default_slices) (unknown_provers @ known_provers) end fun prover_slices_of_schedule ctxt factss ({max_facts, fact_filter, type_enc, lam_trans, uncurried_aliases, ...} : params) schedule = let fun triplicate_slices original = let val shift = map (apfst (apsnd (fn fact_filter => if fact_filter = mashN then mepoN else if fact_filter = mepoN then meshN else mashN))) val shifted_once = shift original val shifted_twice = shift shifted_once in original @ shifted_once @ shifted_twice end - fun adjust_extra (format0, type_enc0, lam_trans0, uncurried_aliases0, extra_extra0) = - (format0, the_default type_enc0 type_enc, the_default lam_trans0 lam_trans, - the_default uncurried_aliases0 uncurried_aliases, extra_extra0) + fun adjust_extra (ATP_Slice (format0, type_enc0, lam_trans0, uncurried_aliases0, + extra_extra0)) = + ATP_Slice (format0, the_default type_enc0 type_enc, the_default lam_trans0 lam_trans, + the_default uncurried_aliases0 uncurried_aliases, extra_extra0) + | adjust_extra (extra as SMT_Slice _) = extra fun adjust_slice ((num_facts0, fact_filter0), extra) = let val fact_filter = fact_filter |> the_default fact_filter0 val max_facts = max_facts |> the_default num_facts0 val num_facts = Int.min (max_facts, length (facts_of_filter fact_filter factss)) in - ((num_facts, fact_filter), Option.map adjust_extra extra) + ((num_facts, fact_filter), adjust_extra extra) end val provers = distinct (op =) schedule val prover_slices = map (fn prover => (prover, (is_none fact_filter ? triplicate_slices) (map adjust_slice (get_slices ctxt prover)))) provers fun translate _ [] = [] | translate prover_slices (prover :: schedule) = (case AList.lookup (op =) prover_slices prover of SOME (slice :: slices) => let val prover_slices' = AList.update (op =) (prover, slices) prover_slices in (prover, slice) :: translate prover_slices' schedule end | _ => translate prover_slices schedule) in translate prover_slices schedule |> distinct (op =) end fun run_sledgehammer (params as {verbose, spy, provers, induction_rules, max_facts, max_proofs, slices, ...}) mode writeln_result i (fact_override as {only, ...}) state = if null provers then error "No prover is set" else (case subgoal_count state of 0 => (error "No subgoal!"; (false, (SH_None, ""))) | n => let val _ = Proof.assert_backward state val print = if mode = Normal andalso is_none writeln_result then writeln else K () val found_proofs = Synchronized.var "found_proofs" 0 fun found_proof prover_name = if mode = Normal then (Synchronized.change found_proofs (fn n => n + 1); (writeln_result |> the_default writeln) (prover_name ^ " found a proof...")) else () val ctxt = Proof.context_of state val inst_inducts = induction_rules = SOME Instantiate val {facts = chained_thms, goal, ...} = Proof.goal state val (_, hyp_ts, concl_t) = strip_subgoal goal i ctxt val _ = (case find_first (not o is_prover_supported ctxt) provers of SOME name => error ("No such prover: " ^ name) | NONE => ()) val _ = print "Sledgehammering..." val _ = spying spy (fn () => (state, i, "***", "Starting " ^ str_of_mode mode ^ " mode")) val ({elapsed, ...}, all_facts) = Timing.timing (nearly_all_facts_of_context ctxt inst_inducts fact_override chained_thms hyp_ts) concl_t val _ = spying spy (fn () => (state, i, "All", "Extracting " ^ string_of_int (length all_facts) ^ " facts from background theory in " ^ string_of_int (Time.toMilliseconds elapsed) ^ " ms")) val spying_str_of_factss = commas o map (fn (filter, facts) => filter ^ ": " ^ string_of_int (length facts)) fun get_factss provers = let val max_max_facts = (case max_facts of SOME n => n | NONE => fold (fn prover => fold (fn ((n, _), _) => Integer.max n) (get_slices ctxt prover)) provers 0) * 51 div 50 (* some slack to account for filtering of induction facts below *) val ({elapsed, ...}, factss) = Timing.timing (relevant_facts ctxt params (hd provers) max_max_facts fact_override hyp_ts concl_t) all_facts val induction_rules = the_default (if only then Include else Exclude) induction_rules val factss = map (apsnd (maybe_filter_out_induction_rules induction_rules)) factss val () = spying spy (fn () => (state, i, "All", "Filtering facts in " ^ string_of_int (Time.toMilliseconds elapsed) ^ " ms (MaSh algorithm: " ^ str_of_mash_algorithm (the_mash_algorithm ()) ^ ")")); val () = if verbose then print (string_of_factss factss) else () val () = spying spy (fn () => (state, i, "All", "Selected facts: " ^ spying_str_of_factss factss)) in factss end fun launch_provers () = let val factss = get_factss provers val problem = {comment = "", state = state, goal = goal, subgoal = i, subgoal_count = n, factss = factss, found_proof = found_proof} val learn = mash_learn_proof ctxt params (Thm.prop_of goal) val launch = launch_prover_and_preplay params mode writeln_result learn val schedule = if mode = Auto_Try then provers else schedule_of_provers provers slices val prover_slices = prover_slices_of_schedule ctxt factss params schedule val _ = if verbose then writeln ("Running " ^ commas (map fst prover_slices) ^ "...") else () in if mode = Auto_Try then (SH_Unknown, "") |> fold (fn (prover, slice) => fn accum as (SH_Some _, _) => accum | _ => launch problem slice prover) prover_slices else (learn chained_thms; Par_List.map (fn (prover, slice) => if Synchronized.value found_proofs < max_proofs then launch problem slice prover else (SH_None, "")) prover_slices |> max_outcome) end in (launch_provers () handle Timeout.TIMEOUT _ => (SH_Timeout, "")) |> `(fn (outcome, message) => (case outcome of SH_Some _ => (print "QED"; true) | SH_Unknown => (print message; false) | _ => (print "No proof found"; false))) end) end; diff --git a/src/HOL/Tools/Sledgehammer/sledgehammer_prover.ML b/src/HOL/Tools/Sledgehammer/sledgehammer_prover.ML --- a/src/HOL/Tools/Sledgehammer/sledgehammer_prover.ML +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_prover.ML @@ -1,255 +1,263 @@ (* Title: HOL/Tools/Sledgehammer/sledgehammer_prover.ML Author: Fabian Immler, TU Muenchen Author: Makarius Author: Jasmin Blanchette, TU Muenchen Generic prover abstraction for Sledgehammer. *) signature SLEDGEHAMMER_PROVER = sig type atp_failure = ATP_Proof.atp_failure type stature = ATP_Problem_Generate.stature type type_enc = ATP_Problem_Generate.type_enc type fact = Sledgehammer_Fact.fact type proof_method = Sledgehammer_Proof_Methods.proof_method type play_outcome = Sledgehammer_Proof_Methods.play_outcome type base_slice = Sledgehammer_ATP_Systems.base_slice type atp_slice = Sledgehammer_ATP_Systems.atp_slice datatype mode = Auto_Try | Try | Normal | Minimize | MaSh datatype induction_rules = Include | Exclude | Instantiate val induction_rules_of_string : string -> induction_rules option val maybe_filter_out_induction_rules : induction_rules -> fact list -> fact list type params = {debug : bool, verbose : bool, overlord : bool, spy : bool, provers : string list, type_enc : string option, strict : bool, lam_trans : string option, uncurried_aliases : bool option, learn : bool, fact_filter : string option, induction_rules : induction_rules option, max_facts : int option, fact_thresholds : real * real, max_mono_iters : int option, max_new_mono_instances : int option, max_proofs : int, isar_proofs : bool option, compress : real option, try0 : bool, smt_proofs : bool, minimize : bool, slices : int, timeout : Time.time, preplay_timeout : Time.time, expect : string} val string_of_params : params -> string val slice_timeout : int -> Time.time -> Time.time type prover_problem = {comment : string, state : Proof.state, goal : thm, subgoal : int, subgoal_count : int, factss : (string * fact list) list, found_proof : string -> unit} - type prover_slice = base_slice * atp_slice option + datatype prover_slice_extra = + ATP_Slice of atp_slice + | SMT_Slice of string list + + type prover_slice = base_slice * prover_slice_extra type prover_result = {outcome : atp_failure option, used_facts : (string * stature) list, used_from : fact list, preferred_methss : proof_method * proof_method list list, run_time : Time.time, message : (unit -> (string * stature) list * (proof_method * play_outcome)) -> string} type prover = params -> prover_problem -> prover_slice -> prover_result val SledgehammerN : string val str_of_mode : mode -> string val overlord_file_location_of_prover : string -> string * string val proof_banner : mode -> string -> string val is_atp : string -> bool val bunches_of_proof_methods : Proof.context -> bool -> bool -> bool -> string -> proof_method list list val facts_of_filter : string -> (string * fact list) list -> fact list val is_fact_chained : (('a * stature) * 'b) -> bool val filter_used_facts : bool -> (''a * stature) list -> ((''a * stature) * 'b) list -> ((''a * stature) * 'b) list val repair_monomorph_context : int option -> int -> int option -> int -> Proof.context -> Proof.context val supported_provers : Proof.context -> unit end; structure Sledgehammer_Prover : SLEDGEHAMMER_PROVER = struct open ATP_Proof open ATP_Util open ATP_Problem open ATP_Problem_Generate open ATP_Proof_Reconstruct open Metis_Tactic open Sledgehammer_Fact open Sledgehammer_Proof_Methods open Sledgehammer_ATP_Systems (* Identifier that distinguishes Sledgehammer from other tools that could use "Async_Manager". *) val SledgehammerN = "Sledgehammer" datatype mode = Auto_Try | Try | Normal | Minimize | MaSh fun str_of_mode Auto_Try = "Auto Try" | str_of_mode Try = "Try" | str_of_mode Normal = "Normal" | str_of_mode Minimize = "Minimize" | str_of_mode MaSh = "MaSh" datatype induction_rules = Include | Exclude | Instantiate fun induction_rules_of_string "include" = SOME Include | induction_rules_of_string "exclude" = SOME Exclude | induction_rules_of_string "instantiate" = SOME Instantiate | induction_rules_of_string _ = NONE val is_atp = member (op =) atps type params = {debug : bool, verbose : bool, overlord : bool, spy : bool, provers : string list, type_enc : string option, strict : bool, lam_trans : string option, uncurried_aliases : bool option, learn : bool, fact_filter : string option, induction_rules : induction_rules option, max_facts : int option, fact_thresholds : real * real, max_mono_iters : int option, max_new_mono_instances : int option, max_proofs : int, isar_proofs : bool option, compress : real option, try0 : bool, smt_proofs : bool, minimize : bool, slices : int, timeout : Time.time, preplay_timeout : Time.time, expect : string} fun string_of_params (params : params) = YXML.content_of (ML_Pretty.string_of_polyml (ML_system_pretty (params, 100))) fun maybe_filter_out_induction_rules induction_rules : fact list -> fact list = induction_rules = Exclude ? filter_out (fn ((_, (_, ATP_Problem_Generate.Induction)), _) => true | _ => false) fun slice_timeout slices timeout = let val max_threads = Multithreading.max_threads () val batches = (slices + max_threads - 1) div max_threads in seconds (Time.toReal timeout / Real.fromInt batches) end type prover_problem = {comment : string, state : Proof.state, goal : thm, subgoal : int, subgoal_count : int, factss : (string * fact list) list, found_proof : string -> unit} -type prover_slice = base_slice * atp_slice option +datatype prover_slice_extra = + ATP_Slice of atp_slice +| SMT_Slice of string list + +type prover_slice = base_slice * prover_slice_extra type prover_result = {outcome : atp_failure option, used_facts : (string * stature) list, used_from : fact list, preferred_methss : proof_method * proof_method list list, run_time : Time.time, message : (unit -> (string * stature) list * (proof_method * play_outcome)) -> string} type prover = params -> prover_problem -> prover_slice -> prover_result fun overlord_file_location_of_prover prover = (getenv "ISABELLE_HOME_USER", "prob_" ^ prover) fun proof_banner mode prover_name = (case mode of Auto_Try => "Auto Sledgehammer (" ^ prover_name ^ ") found a proof: " | Try => "Sledgehammer (" ^ prover_name ^ ") found a proof: " | _ => "Try this: ") fun bunches_of_proof_methods ctxt try0 smt_proofs needs_full_types desperate_lam_trans = let val try0_methodss = if try0 then [[Simp_Method, Auto_Method, Blast_Method, Linarith_Method, Meson_Method, Metis_Method (NONE, NONE), Fastforce_Method, Force_Method, Presburger_Method]] else [] val metis_methods = (if try0 then [] else [Metis_Method (NONE, NONE)]) @ Metis_Method (SOME full_typesN, NONE) :: Metis_Method (SOME really_full_type_enc, SOME desperate_lam_trans) :: (if needs_full_types then [Metis_Method (SOME really_full_type_enc, NONE), Metis_Method (SOME full_typesN, SOME desperate_lam_trans)] else [Metis_Method (SOME no_typesN, SOME desperate_lam_trans)]) val smt_methodss = if smt_proofs then [map (SMT_Method o SMT_Verit) (Verit_Proof.all_veriT_stgies (Context.Proof ctxt)), [SMT_Method SMT_Z3]] else [] in try0_methodss @ [metis_methods] @ smt_methodss end fun facts_of_filter fact_filter factss = (case AList.lookup (op =) factss fact_filter of SOME facts => facts | NONE => snd (hd factss)) fun is_fact_chained ((_, (sc, _)), _) = sc = Chained fun filter_used_facts keep_chained used = filter ((member (eq_fst (op =)) used o fst) orf (if keep_chained then is_fact_chained else K false)) val max_fact_instances = 10 (* FUDGE *) fun repair_monomorph_context max_iters best_max_iters max_new_instances best_max_new_instances = Config.put Monomorph.max_rounds (max_iters |> the_default best_max_iters) #> Config.put Monomorph.max_new_instances (max_new_instances |> the_default best_max_new_instances) #> Config.put Monomorph.max_thm_instances max_fact_instances fun supported_provers ctxt = let val local_provers = sort_strings (local_atps @ SMT_Config.available_solvers_of ctxt) val remote_provers = sort_strings remote_atps in writeln ("Supported provers: " ^ commas (local_provers @ remote_provers)) end end; diff --git a/src/HOL/Tools/Sledgehammer/sledgehammer_prover_atp.ML b/src/HOL/Tools/Sledgehammer/sledgehammer_prover_atp.ML --- a/src/HOL/Tools/Sledgehammer/sledgehammer_prover_atp.ML +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_prover_atp.ML @@ -1,349 +1,349 @@ (* Title: HOL/Tools/Sledgehammer/sledgehammer_prover_atp.ML Author: Fabian Immler, TU Muenchen Author: Makarius Author: Jasmin Blanchette, TU Muenchen ATPs as Sledgehammer provers. *) signature SLEDGEHAMMER_PROVER_ATP = sig type mode = Sledgehammer_Prover.mode type prover = Sledgehammer_Prover.prover val atp_problem_dest_dir : string Config.T val atp_proof_dest_dir : string Config.T val atp_problem_prefix : string Config.T val atp_completish : int Config.T val atp_full_names : bool Config.T val run_atp : mode -> string -> prover end; structure Sledgehammer_Prover_ATP : SLEDGEHAMMER_PROVER_ATP = struct open ATP_Util open ATP_Problem open ATP_Problem_Generate open ATP_Proof open ATP_Proof_Reconstruct open Sledgehammer_Util open Sledgehammer_Proof_Methods open Sledgehammer_Isar open Sledgehammer_ATP_Systems open Sledgehammer_Prover (* Empty string means create files in Isabelle's temporary files directory. *) val atp_problem_dest_dir = Attrib.setup_config_string \<^binding>\sledgehammer_atp_problem_dest_dir\ (K "") val atp_proof_dest_dir = Attrib.setup_config_string \<^binding>\sledgehammer_atp_proof_dest_dir\ (K "") val atp_problem_prefix = Attrib.setup_config_string \<^binding>\sledgehammer_atp_problem_prefix\ (K "prob") val atp_completish = Attrib.setup_config_int \<^binding>\sledgehammer_atp_completish\ (K 0) (* In addition to being easier to read, readable names are often much shorter, especially if types are mangled in names. This makes a difference for some provers (e.g., E). For these reason, short names are enabled by default. *) val atp_full_names = Attrib.setup_config_bool \<^binding>\sledgehammer_atp_full_names\ (K false) fun choose_type_enc strictness format good_type_enc = type_enc_of_string strictness good_type_enc |> adjust_type_enc format fun has_bound_or_var_of_type pred = exists_subterm (fn Var (_, T as Type _) => pred T | Abs (_, T as Type _, _) => pred T | _ => false) (* Unwanted equalities are those between a (bound or schematic) variable that does not properly occur in the second operand. *) val is_exhaustive_finite = let fun is_bad_equal (Var z) t = not (exists_subterm (fn Var z' => z = z' | _ => false) t) | is_bad_equal (Bound j) t = not (loose_bvar1 (t, j)) | is_bad_equal _ _ = false fun do_equals t1 t2 = is_bad_equal t1 t2 orelse is_bad_equal t2 t1 fun do_formula pos t = (case (pos, t) of (_, \<^Const_>\Trueprop for t1\) => do_formula pos t1 | (true, Const (\<^const_name>\Pure.all\, _) $ Abs (_, _, t')) => do_formula pos t' | (true, Const (\<^const_name>\All\, _) $ Abs (_, _, t')) => do_formula pos t' | (false, Const (\<^const_name>\Ex\, _) $ Abs (_, _, t')) => do_formula pos t' | (_, \<^Const_>\Pure.imp for t1 t2\) => do_formula (not pos) t1 andalso (t2 = \<^prop>\False\ orelse do_formula pos t2) | (_, \<^Const_>\implies for t1 t2\) => do_formula (not pos) t1 andalso (t2 = \<^Const>\False\ orelse do_formula pos t2) | (_, \<^Const_>\Not for t1\) => do_formula (not pos) t1 | (true, \<^Const_>\disj for t1 t2\) => forall (do_formula pos) [t1, t2] | (false, \<^Const_>\conj for t1 t2\) => forall (do_formula pos) [t1, t2] | (true, Const (\<^const_name>\HOL.eq\, _) $ t1 $ t2) => do_equals t1 t2 | (true, Const (\<^const_name>\Pure.eq\, _) $ t1 $ t2) => do_equals t1 t2 | _ => false) in do_formula true end (* Facts containing variables of finite types such as "unit" or "bool" or of the form "ALL x. x = A | x = B | x = C" are likely to lead to untypable proofs for unsound type encodings. *) fun is_dangerous_prop ctxt = transform_elim_prop #> (has_bound_or_var_of_type (is_type_surely_finite ctxt) orf is_exhaustive_finite) val mono_max_privileged_facts = 10 fun suffix_of_mode Auto_Try = "_try" | suffix_of_mode Try = "_try" | suffix_of_mode Normal = "" | suffix_of_mode MaSh = "" | suffix_of_mode Minimize = "_min" (* Important messages are important but not so important that users want to see them each time. *) val atp_important_message_keep_quotient = 25 fun run_atp mode name ({debug, verbose, overlord, strict, fact_filter, max_facts, max_mono_iters, max_new_mono_instances, isar_proofs, compress, try0, smt_proofs, minimize, slices, timeout, preplay_timeout, spy, ...} : params) ({comment, state, goal, subgoal, subgoal_count, factss, found_proof} : prover_problem) slice = let val thy = Proof.theory_of state val ctxt = Proof.context_of state - val ((good_max_facts, good_fact_filter), SOME (good_format, good_type_enc, good_lam_trans, + val ((good_max_facts, good_fact_filter), ATP_Slice (good_format, good_type_enc, good_lam_trans, good_uncurried_aliases, extra)) = slice val {exec, arguments, proof_delims, known_failures, prem_role, good_max_mono_iters, good_max_new_mono_instances, ...} = get_atp thy name () val full_proofs = isar_proofs |> the_default (mode = Minimize) val local_name = perhaps (try (unprefix remote_prefix)) name val completish = Config.get ctxt atp_completish val atp_mode = if completish > 0 then Sledgehammer_Completish completish else Sledgehammer val (_, hyp_ts, concl_t) = strip_subgoal goal subgoal ctxt val (problem_dest_dir, proof_dest_dir, problem_prefix) = if overlord then overlord_file_location_of_prover name |> (fn (dir, prefix) => (dir, dir, prefix)) else (Config.get ctxt atp_problem_dest_dir, Config.get ctxt atp_proof_dest_dir, Config.get ctxt atp_problem_prefix) val problem_file_name = Path.basic (problem_prefix ^ (if overlord then "" else serial_string ()) ^ suffix_of_mode mode ^ "_" ^ string_of_int subgoal) |> Path.ext "p" val prob_path = if problem_dest_dir = "" then File.tmp_path problem_file_name else if File.exists (Path.explode problem_dest_dir) then Path.explode problem_dest_dir + problem_file_name else error ("No such directory: " ^ quote problem_dest_dir) val executable = (case find_first (fn var => getenv var <> "") (fst exec) of SOME var => let val pref = getenv var ^ "/" val paths = map (Path.explode o prefix pref) (if ML_System.platform_is_windows then map (suffix ".exe") (snd exec) @ snd exec else snd exec); in (case find_first File.exists paths of SOME path => path | NONE => error ("Bad executable: " ^ Path.print (hd paths))) end | NONE => error ("The environment variable " ^ quote (List.last (fst exec)) ^ " is not set")) fun run () = let fun monomorphize_facts facts = let val ctxt = ctxt |> repair_monomorph_context max_mono_iters good_max_mono_iters max_new_mono_instances good_max_new_mono_instances (* pseudo-theorem involving the same constants as the subgoal *) val subgoal_th = Logic.list_implies (hyp_ts, concl_t) |> Skip_Proof.make_thm thy val rths = facts |> chop mono_max_privileged_facts |>> map (pair 1 o snd) ||> map (pair 2 o snd) |> op @ |> cons (0, subgoal_th) in Monomorph.monomorph atp_schematic_consts_of ctxt rths |> tl |> curry ListPair.zip (map fst facts) |> maps (fn (name, rths) => map (pair name o zero_var_indexes o snd) rths) end val effective_fact_filter = fact_filter |> the_default good_fact_filter val facts = facts_of_filter effective_fact_filter factss val num_facts = (case max_facts of NONE => good_max_facts | SOME max_facts => max_facts) |> Integer.min (length facts) val strictness = if strict then Strict else Non_Strict val type_enc = choose_type_enc strictness good_format good_type_enc val run_timeout = slice_timeout slices timeout val generous_run_timeout = if mode = MaSh then one_day else run_timeout val ({elapsed, ...}, atp_problem_data as (atp_problem, _, _, _)) = Timing.timing (fn () => let val sound = is_type_enc_sound type_enc val generate_info = (case good_format of DFG _ => true | _ => false) val readable_names = not (Config.get ctxt atp_full_names) in facts |> not sound ? filter_out (is_dangerous_prop ctxt o Thm.prop_of o snd) |> take num_facts |> not (is_type_enc_polymorphic type_enc) ? monomorphize_facts |> map (apsnd Thm.prop_of) |> generate_atp_problem ctxt generate_info good_format prem_role type_enc atp_mode good_lam_trans good_uncurried_aliases readable_names true hyp_ts concl_t end) () val () = spying spy (fn () => (state, subgoal, name, "Generating ATP problem in " ^ string_of_int (Time.toMilliseconds elapsed) ^ " ms")) fun sel_weights () = atp_problem_selection_weights atp_problem fun ord_info () = atp_problem_term_order_info atp_problem val ord = effective_term_order ctxt name val args = arguments ctxt full_proofs extra run_timeout prob_path (ord, ord_info, sel_weights) val command = space_implode " " (File.bash_path executable :: args) fun run_command () = if exec = isabelle_scala_function then let val {output, timing} = SystemOnTPTP.run_system_encoded args in (output, timing) end else let val res = Isabelle_System.bash_process (Bash.script command |> Bash.redirect) in (Process_Result.out res, Process_Result.timing_elapsed res) end val _ = atp_problem |> lines_of_atp_problem good_format ord ord_info |> (exec <> isabelle_scala_function) ? cons ("% " ^ command ^ "\n" ^ (if comment = "" then "" else "% " ^ comment ^ "\n")) |> File.write_list prob_path val ((output, run_time), (atp_proof, outcome)) = Timeout.apply generous_run_timeout run_command () |>> overlord ? (fn output => prefix ("% " ^ command ^ "\n% " ^ timestamp () ^ "\n") output) |> (fn accum as (output, _) => (accum, extract_tstplike_proof_and_outcome verbose proof_delims known_failures output |>> atp_proof_of_tstplike_proof (perhaps (try (unprefix remote_prefix)) name) atp_problem handle UNRECOGNIZED_ATP_PROOF () => ([], SOME ProofUnparsable))) handle Timeout.TIMEOUT _ => (("", run_timeout), ([], SOME TimedOut)) | ERROR msg => (("", Time.zeroTime), ([], SOME (UnknownError msg))) val () = spying spy (fn () => (state, subgoal, name, "Running command in " ^ string_of_int (Time.toMilliseconds run_time) ^ " ms")) val outcome = (case outcome of NONE => (case used_facts_in_unsound_atp_proof ctxt (map fst facts) atp_proof of SOME facts => let val failure = UnsoundProof (is_type_enc_sound type_enc, sort string_ord facts) in if debug then (warning (string_of_atp_failure failure); NONE) else SOME failure end | NONE => (found_proof name; NONE)) | _ => outcome) in (atp_problem_data, (output, run_time, facts, atp_proof, outcome), (good_format, type_enc)) end (* If the problem file has not been exported, remove it; otherwise, export the proof file too. *) fun clean_up () = if problem_dest_dir = "" then (try File.rm prob_path; ()) else () fun export (_, (output, _, _, _, _), _) = let val proof_dest_dir_path = Path.explode proof_dest_dir val make_export_file_name = Path.split_ext #> apfst (Path.explode o suffix "_proof" o Path.implode) #> swap #> uncurry Path.ext in if proof_dest_dir = "" then Output.system_message "don't export proof" else if File.exists proof_dest_dir_path then File.write (proof_dest_dir_path + make_export_file_name problem_file_name) output else error ("No such directory: " ^ quote proof_dest_dir) end val ((_, pool, lifted, sym_tab), (output, run_time, used_from, atp_proof, outcome), (format, type_enc)) = with_cleanup clean_up run () |> tap export val important_message = if mode = Normal andalso Random.random_range 0 (atp_important_message_keep_quotient - 1) = 0 then extract_important_message output else "" val (used_facts, preferred_methss, message) = (case outcome of NONE => let val used_facts = sort_by fst (used_facts_in_atp_proof ctxt (map fst used_from) atp_proof) val needs_full_types = is_typed_helper_used_in_atp_proof atp_proof val preferred_methss = (Metis_Method (NONE, NONE), bunches_of_proof_methods ctxt try0 smt_proofs needs_full_types (if atp_proof_prefers_lifting atp_proof then liftingN else opaque_liftingN)) in (used_facts, preferred_methss, fn preplay => let val _ = if verbose then writeln "Generating proof text..." else () fun isar_params () = let val metis_type_enc = if is_typed_helper_used_in_atp_proof atp_proof then SOME full_typesN else NONE val metis_lam_trans = if atp_proof_prefers_lifting atp_proof then SOME liftingN else NONE val atp_proof = atp_proof |> termify_atp_proof ctxt name format type_enc pool lifted sym_tab |> local_name = spassN ? introduce_spass_skolems |> factify_atp_proof (map fst used_from) hyp_ts concl_t in (verbose, (metis_type_enc, metis_lam_trans), preplay_timeout, compress, try0, minimize, atp_proof, goal) end val one_line_params = (preplay (), proof_banner mode name, subgoal, subgoal_count) val num_chained = length (#facts (Proof.goal state)) in proof_text ctxt debug isar_proofs smt_proofs isar_params num_chained one_line_params ^ (if important_message <> "" then "\n\nImportant message from Dr. Geoff Sutcliffe:\n" ^ important_message else "") end) end | SOME failure => ([], (Auto_Method (* dummy *), []), fn _ => string_of_atp_failure failure)) in {outcome = outcome, used_facts = used_facts, used_from = used_from, preferred_methss = preferred_methss, run_time = run_time, message = message} end end; diff --git a/src/HOL/Tools/Sledgehammer/sledgehammer_prover_minimize.ML b/src/HOL/Tools/Sledgehammer/sledgehammer_prover_minimize.ML --- a/src/HOL/Tools/Sledgehammer/sledgehammer_prover_minimize.ML +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_prover_minimize.ML @@ -1,269 +1,269 @@ (* Title: HOL/Tools/Sledgehammer/sledgehammer_prover_minimize.ML Author: Philipp Meyer, TU Muenchen Author: Jasmin Blanchette, TU Muenchen Minimization of fact list for Metis using external provers. *) signature SLEDGEHAMMER_PROVER_MINIMIZE = sig type stature = ATP_Problem_Generate.stature type proof_method = Sledgehammer_Proof_Methods.proof_method type play_outcome = Sledgehammer_Proof_Methods.play_outcome type mode = Sledgehammer_Prover.mode type params = Sledgehammer_Prover.params type prover = Sledgehammer_Prover.prover type prover_slice = Sledgehammer_Prover.prover_slice val is_prover_supported : Proof.context -> string -> bool val is_prover_installed : Proof.context -> string -> bool val get_prover : Proof.context -> mode -> string -> prover val get_slices : Proof.context -> string -> prover_slice list val binary_min_facts : int Config.T val minimize_facts : (thm list -> unit) -> string -> params -> bool -> int -> int -> Proof.state -> thm -> ((string * stature) * thm list) list -> ((string * stature) * thm list) list option * ((unit -> (string * stature) list * (proof_method * play_outcome)) -> string) val get_minimizing_prover : Proof.context -> mode -> (thm list -> unit) -> string -> prover end; structure Sledgehammer_Prover_Minimize : SLEDGEHAMMER_PROVER_MINIMIZE = struct open ATP_Util open ATP_Proof open ATP_Problem_Generate open ATP_Proof_Reconstruct open Sledgehammer_Util open Sledgehammer_Fact open Sledgehammer_Proof_Methods open Sledgehammer_Isar open Sledgehammer_ATP_Systems open Sledgehammer_Prover open Sledgehammer_Prover_ATP open Sledgehammer_Prover_SMT fun is_prover_supported ctxt = is_atp orf is_smt_prover ctxt fun is_prover_installed ctxt prover_name = if is_atp prover_name then let val thy = Proof_Context.theory_of ctxt in is_atp_installed thy prover_name end else is_smt_prover_installed ctxt prover_name fun get_prover ctxt mode name = if is_atp name then run_atp mode name else if is_smt_prover ctxt name then run_smt_solver mode name else error ("No such prover: " ^ name) fun get_slices ctxt name = let val thy = Proof_Context.theory_of ctxt in if is_atp name then - map (apsnd SOME) (#good_slices (get_atp thy name ()) ctxt) + map (apsnd ATP_Slice) (#good_slices (get_atp thy name ()) ctxt) else if is_smt_prover ctxt name then - map (rpair NONE) (SMT_Solver.good_slices ctxt name) + map (apsnd SMT_Slice) (SMT_Solver.good_slices ctxt name) else error ("No such prover: " ^ name) end (* wrapper for calling external prover *) fun n_facts names = let val n = length names in string_of_int n ^ " fact" ^ plural_s n ^ (if n > 0 then ": " ^ (names |> map fst |> sort string_ord |> space_implode " ") else "") end fun print silent f = if silent then () else writeln (f ()) fun test_facts ({debug, verbose, overlord, spy, provers, max_mono_iters, max_new_mono_instances, type_enc, strict, lam_trans, uncurried_aliases, isar_proofs, compress, try0, smt_proofs, minimize, preplay_timeout, induction_rules, ...} : params) slice silent (prover : prover) timeout i n state goal facts = let val _ = print silent (fn () => "Testing " ^ n_facts (map fst facts) ^ (if verbose then " (timeout: " ^ string_of_time timeout ^ ")" else "") ^ "...") val facts = facts |> maps (fn (n, ths) => map (pair n) ths) val params = {debug = debug, verbose = verbose, overlord = overlord, spy = spy, provers = provers, type_enc = type_enc, strict = strict, lam_trans = lam_trans, uncurried_aliases = uncurried_aliases, learn = false, fact_filter = NONE, induction_rules = induction_rules, max_facts = SOME (length facts), fact_thresholds = (1.01, 1.01), max_mono_iters = max_mono_iters, max_new_mono_instances = max_new_mono_instances, max_proofs = 1, isar_proofs = isar_proofs, compress = compress, try0 = try0, smt_proofs = smt_proofs, minimize = minimize, slices = 1, timeout = timeout, preplay_timeout = preplay_timeout, expect = ""} val problem = {comment = "", state = state, goal = goal, subgoal = i, subgoal_count = n, factss = [("", facts)], found_proof = K ()} val result0 as {outcome = outcome0, used_facts, used_from, preferred_methss, run_time, message} = prover params problem slice val result as {outcome, ...} = if is_none outcome0 andalso forall (member (fn ((s, _), ((s', _), _)) => s = s') used_from) used_facts then result0 else {outcome = SOME MaybeUnprovable, used_facts = [], used_from = used_from, preferred_methss = preferred_methss, run_time = run_time, message = message} in print silent (fn () => (case outcome of SOME failure => string_of_atp_failure failure | NONE => "Found proof" ^ (if length used_facts = length facts then "" else " with " ^ n_facts used_facts) ^ " (" ^ string_of_time run_time ^ ")")); result end (* minimalization of facts *) (* Give the external prover some slack. The ATP gets further slack because the Sledgehammer preprocessing time is included in the estimate below but isn't part of the timeout. *) val slack_msecs = 200 fun new_timeout timeout run_time = Int.min (Time.toMilliseconds timeout, Time.toMilliseconds run_time + slack_msecs) |> Time.fromMilliseconds (* The linear algorithm usually outperforms the binary algorithm when over 60% of the facts are actually needed. The binary algorithm is much more appropriate for provers that cannot return the list of used facts and hence returns all facts as used. Since we cannot know in advance how many facts are actually needed, we heuristically set the threshold to 10 facts. *) val binary_min_facts = Attrib.setup_config_int \<^binding>\sledgehammer_minimize_binary_min_facts\ (K 20) fun linear_minimize test timeout result xs = let fun min _ [] p = p | min timeout (x :: xs) (seen, result) = (case test timeout (xs @ seen) of result as {outcome = NONE, used_facts, run_time, ...} : prover_result => min (new_timeout timeout run_time) (filter_used_facts true used_facts xs) (filter_used_facts false used_facts seen, result) | _ => min timeout xs (x :: seen, result)) in min timeout xs ([], result) end fun binary_minimize test timeout result xs = let fun min depth (result as {run_time, ...} : prover_result) sup (xs as _ :: _ :: _) = let val (l0, r0) = chop (length xs div 2) xs (* val _ = warning (replicate_string depth " " ^ "{ " ^ "sup: " ^ n_facts (map fst sup)) val _ = warning (replicate_string depth " " ^ " " ^ "xs: " ^ n_facts (map fst xs)) val _ = warning (replicate_string depth " " ^ " " ^ "l0: " ^ n_facts (map fst l0)) val _ = warning (replicate_string depth " " ^ " " ^ "r0: " ^ n_facts (map fst r0)) *) val depth = depth + 1 val timeout = new_timeout timeout run_time in (case test timeout (sup @ l0) of result as {outcome = NONE, used_facts, ...} => min depth result (filter_used_facts true used_facts sup) (filter_used_facts true used_facts l0) | _ => (case test timeout (sup @ r0) of result as {outcome = NONE, used_facts, ...} => min depth result (filter_used_facts true used_facts sup) (filter_used_facts true used_facts r0) | _ => let val (sup_r0, (l, result)) = min depth result (sup @ r0) l0 val (sup, r0) = (sup, r0) |> apply2 (filter_used_facts true (map fst sup_r0)) val (sup_l, (r, result)) = min depth result (sup @ l) r0 val sup = sup |> filter_used_facts true (map fst sup_l) in (sup, (l @ r, result)) end)) end (* |> tap (fn _ => warning (replicate_string depth " " ^ "}")) *) | min _ result sup xs = (sup, (xs, result)) in (case snd (min 0 result [] xs) of ([x], result as {run_time, ...}) => (case test (new_timeout timeout run_time) [] of result as {outcome = NONE, ...} => ([], result) | _ => ([x], result)) | p => p) end fun minimize_facts do_learn prover_name (params as {learn, timeout, ...}) silent i n state goal facts = let val ctxt = Proof.context_of state val prover = get_prover ctxt Minimize prover_name val slice = hd (get_slices ctxt prover_name) val (chained, non_chained) = List.partition is_fact_chained facts fun test timeout non_chained = test_facts params slice silent prover timeout i n state goal (chained @ non_chained) in (print silent (fn () => "Sledgehammer minimizer: " ^ prover_name); (case test timeout non_chained of result as {outcome = NONE, used_facts, run_time, ...} => let val non_chained = filter_used_facts true used_facts non_chained val min = if length non_chained >= Config.get ctxt binary_min_facts then binary_minimize else linear_minimize val (min_facts, {message, ...}) = min test (new_timeout timeout run_time) result non_chained val min_facts_and_chained = chained @ min_facts in print silent (fn () => cat_lines ["Minimized to " ^ n_facts (map fst min_facts)] ^ (case length chained of 0 => "" | n => " (plus " ^ string_of_int n ^ " chained)")); (if learn then do_learn (maps snd min_facts_and_chained) else ()); (SOME min_facts_and_chained, message) end | {outcome = SOME TimedOut, ...} => (NONE, fn _ => "Timeout: You can increase the time limit using the \"timeout\" option (e.g., \ \timeout = " ^ string_of_int (10 + Time.toMilliseconds timeout div 1000) ^ "\")") | {message, ...} => (NONE, (prefix "Prover error: " o message)))) handle ERROR msg => (NONE, fn _ => "Error: " ^ msg) end fun maybe_minimize mode do_learn name (params as {verbose, minimize, ...}) ({state, goal, subgoal, subgoal_count, ...} : prover_problem) (result as {outcome, used_facts, used_from, preferred_methss, run_time, message} : prover_result) = if is_some outcome then result else let val (used_facts, message) = if minimize then minimize_facts do_learn name params (not verbose orelse (mode <> Normal andalso mode <> MaSh)) subgoal subgoal_count state goal (filter_used_facts true used_facts (map (apsnd single) used_from)) |>> Option.map (map fst) else (SOME used_facts, message) in (case used_facts of SOME used_facts => {outcome = NONE, used_facts = sort_by fst used_facts, used_from = used_from, preferred_methss = preferred_methss, run_time = run_time, message = message} | NONE => result) end fun get_minimizing_prover ctxt mode do_learn name params problem slice = get_prover ctxt mode name params problem slice |> maybe_minimize mode do_learn name params problem end; diff --git a/src/HOL/Tools/Sledgehammer/sledgehammer_prover_smt.ML b/src/HOL/Tools/Sledgehammer/sledgehammer_prover_smt.ML --- a/src/HOL/Tools/Sledgehammer/sledgehammer_prover_smt.ML +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_prover_smt.ML @@ -1,170 +1,170 @@ (* Title: HOL/Tools/Sledgehammer/sledgehammer_prover_smt.ML Author: Fabian Immler, TU Muenchen Author: Makarius Author: Jasmin Blanchette, TU Muenchen SMT solvers as Sledgehammer provers. *) signature SLEDGEHAMMER_PROVER_SMT = sig type stature = ATP_Problem_Generate.stature type mode = Sledgehammer_Prover.mode type prover = Sledgehammer_Prover.prover val smt_builtins : bool Config.T val smt_triggers : bool Config.T val is_smt_prover : Proof.context -> string -> bool val is_smt_prover_installed : Proof.context -> string -> bool val run_smt_solver : mode -> string -> prover val smts : Proof.context -> string list end; structure Sledgehammer_Prover_SMT : SLEDGEHAMMER_PROVER_SMT = struct open ATP_Util open ATP_Proof open ATP_Problem_Generate open ATP_Proof_Reconstruct open Sledgehammer_Util open Sledgehammer_Proof_Methods open Sledgehammer_Isar open Sledgehammer_ATP_Systems open Sledgehammer_Prover val smt_builtins = Attrib.setup_config_bool \<^binding>\sledgehammer_smt_builtins\ (K true) val smt_triggers = Attrib.setup_config_bool \<^binding>\sledgehammer_smt_triggers\ (K true) val smts = sort_strings o SMT_Config.all_solvers_of val is_smt_prover = member (op =) o smts val is_smt_prover_installed = member (op =) o SMT_Config.available_solvers_of (* "SMT_Failure.Abnormal_Termination" carries the solver's return code. Until these are sorted out properly in the SMT module, we must interpret these here. *) val z3_failures = [(101, OutOfResources), (103, MalformedInput), (110, MalformedInput), (112, TimedOut)] val unix_failures = [(134, Crashed), (138, Crashed), (139, Crashed)] val smt_failures = z3_failures @ unix_failures fun failure_of_smt_failure (SMT_Failure.Counterexample genuine) = if genuine then Unprovable else GaveUp | failure_of_smt_failure SMT_Failure.Time_Out = TimedOut | failure_of_smt_failure (SMT_Failure.Abnormal_Termination code) = (case AList.lookup (op =) smt_failures code of SOME failure => failure | NONE => UnknownError ("Abnormal termination with exit code " ^ string_of_int code)) | failure_of_smt_failure SMT_Failure.Out_Of_Memory = OutOfResources | failure_of_smt_failure (SMT_Failure.Other_Failure s) = UnknownError s val is_boring_builtin_typ = not o exists_subtype (member (op =) [\<^typ>\nat\, \<^typ>\int\, HOLogic.realT]) fun smt_filter name ({debug, overlord, max_mono_iters, max_new_mono_instances, - type_enc, slices, timeout, ...} : params) state goal i facts = + type_enc, slices, timeout, ...} : params) state goal i facts options = let val run_timeout = slice_timeout slices timeout val (higher_order, nat_as_int) = (case type_enc of SOME s => (String.isSubstring "native_higher" s, String.isSubstring "arith" s) | NONE => (false, false)) fun repair_context ctxt = ctxt |> Context.proof_map (SMT_Config.select_solver name) |> Config.put SMT_Config.higher_order higher_order |> Config.put SMT_Config.nat_as_int nat_as_int |> (if overlord then Config.put SMT_Config.debug_files (overlord_file_location_of_prover name |> (fn (path, name) => path ^ "/" ^ name)) else I) |> Config.put SMT_Config.infer_triggers (Config.get ctxt smt_triggers) |> not (Config.get ctxt smt_builtins) ? (SMT_Builtin.filter_builtins is_boring_builtin_typ #> Config.put SMT_Systems.z3_extensions false) |> repair_monomorph_context max_mono_iters default_max_mono_iters max_new_mono_instances default_max_new_mono_instances val state = Proof.map_context (repair_context) state val ctxt = Proof.context_of state val timer = Timer.startRealTimer () val birth = Timer.checkRealTimer timer val filter_result as {outcome, ...} = - SMT_Solver.smt_filter ctxt goal facts i run_timeout + SMT_Solver.smt_filter ctxt goal facts i run_timeout options handle exn => if Exn.is_interrupt exn orelse debug then Exn.reraise exn else {outcome = SOME (SMT_Failure.Other_Failure (Runtime.exn_message exn)), fact_ids = NONE, atp_proof = K []} val death = Timer.checkRealTimer timer val run_time = death - birth in {outcome = outcome, filter_result = filter_result, used_from = facts, run_time = run_time} end fun run_smt_solver mode name (params as {debug, verbose, fact_filter, isar_proofs, compress, try0, smt_proofs, minimize, preplay_timeout, ...}) ({state, goal, subgoal, subgoal_count, factss, found_proof, ...} : prover_problem) slice = let val ctxt = Proof.context_of state - val ((best_max_facts, best_fact_filter), _) = slice + val ((best_max_facts, best_fact_filter), SMT_Slice options) = slice val effective_fact_filter = fact_filter |> the_default best_fact_filter val facts = take best_max_facts (facts_of_filter effective_fact_filter factss) val {outcome, filter_result = {fact_ids, atp_proof, ...}, used_from, run_time} = - smt_filter name params state goal subgoal facts + smt_filter name params state goal subgoal facts options val used_facts = (case fact_ids of NONE => map fst used_from | SOME ids => sort_by fst (map (fst o snd) ids)) val outcome = Option.map failure_of_smt_failure outcome val (preferred_methss, message) = (case outcome of NONE => let val _ = found_proof name; val preferred = if smt_proofs then SMT_Method (if name = "verit" then SMT_Verit "default" else SMT_Z3) else Metis_Method (NONE, NONE); val methss = bunches_of_proof_methods ctxt try0 smt_proofs false liftingN; in ((preferred, methss), fn preplay => let val _ = if verbose then writeln "Generating proof text..." else () fun isar_params () = (verbose, (NONE, NONE), preplay_timeout, compress, try0, minimize, atp_proof (), goal) val one_line_params = (preplay (), proof_banner mode name, subgoal, subgoal_count) val num_chained = length (#facts (Proof.goal state)) in proof_text ctxt debug isar_proofs smt_proofs isar_params num_chained one_line_params end) end | SOME failure => ((Auto_Method (* dummy *), []), fn _ => string_of_atp_failure failure)) in {outcome = outcome, used_facts = used_facts, used_from = used_from, preferred_methss = preferred_methss, run_time = run_time, message = message} end end;