--- a/src/HOL/SMT_Examples/SMT_Examples_Verit.thy Sun Dec 13 23:11:41 2020 +0100
+++ b/src/HOL/SMT_Examples/SMT_Examples_Verit.thy Mon Dec 14 21:02:57 2020 +0100
@@ -647,7 +647,7 @@
lemma
fixes clock :: \<open>'astate \<Rightarrow> nat\<close> and
-fun_evaluate_match :: \<open>'astate \<Rightarrow> 'vsemv_env \<Rightarrow> _ \<Rightarrow> ('pat \<times> 'exp0) list \<Rightarrow> _ \<Rightarrow>
+ fun_evaluate_match :: \<open>'astate \<Rightarrow> 'vsemv_env \<Rightarrow> _ \<Rightarrow> ('pat \<times> 'exp0) list \<Rightarrow> _ \<Rightarrow>
'astate*((('v)list),('v))result\<close>
assumes
" fix_clock (st::'astate) (fun_evaluate st (env::'vsemv_env) [e::'exp0]) =
--- a/src/HOL/Tools/SMT/smt_config.ML Sun Dec 13 23:11:41 2020 +0100
+++ b/src/HOL/Tools/SMT/smt_config.ML Mon Dec 14 21:02:57 2020 +0100
@@ -188,7 +188,7 @@
val spy_verit_attr = Attrib.setup_config_bool \<^binding>\<open>smt_spy_verit\<close> (K false)
val spy_z3 = Attrib.setup_config_bool \<^binding>\<open>smt_spy_z3\<close> (K false)
val trace_arith_verit = Attrib.setup_config_bool \<^binding>\<open>smt_debug_arith_verit\<close> (K false)
-val trace_verit_compression = Attrib.setup_config_bool \<^binding>\<open>verit_compress_proofs\<close> (K false)
+val trace_verit_compression = Attrib.setup_config_bool \<^binding>\<open>verit_compress_proofs\<close> (K true)
val statistics = Attrib.setup_config_bool \<^binding>\<open>smt_statistics\<close> (K false)
val monomorph_limit = Attrib.setup_config_int \<^binding>\<open>smt_monomorph_limit\<close> (K 10)
val monomorph_instances = Attrib.setup_config_int \<^binding>\<open>smt_monomorph_instances\<close> (K 500)
--- a/src/HOL/Tools/SMT/verit_proof.ML Sun Dec 13 23:11:41 2020 +0100
+++ b/src/HOL/Tools/SMT/verit_proof.ML Mon Dec 14 21:02:57 2020 +0100
@@ -52,6 +52,9 @@
val eq_congruent_rule : string
val eq_congruent_pred_rule : string
val skolemization_steps : string list
+ val theory_resolution2_rule: string
+ val equiv_pos2_rule: string
+ val th_resolution_rule: string
val is_skolemization: string -> bool
val is_skolemization_step: veriT_replay_node -> bool
@@ -151,7 +154,7 @@
let
val {default_strategy,strategies} = Data.get context
in
- Data.map
+ Data.map
(K (mk_verit_strategy default_strategy (AList.update (op =) stgy strategies)))
context
end
@@ -160,7 +163,7 @@
let
val {default_strategy,strategies} = Data.get context
in
- Data.map
+ Data.map
(K (mk_verit_strategy default_strategy (AList.delete (op =) stgy strategies)))
context
end
@@ -242,6 +245,9 @@
val eq_congruent_rule = "eq_congruent"
val ite_intro_rule = "ite_intro"
val default_skolem_rule = "sko_forall" (*arbitrary, but must be one of the skolems*)
+val theory_resolution2_rule = "__theory_resolution2" (*arbitrary*)
+val equiv_pos2_rule = "equiv_pos2"
+val th_resolution_rule = "th_resolution"
val skolemization_steps = ["sko_forall", "sko_ex"]
val is_skolemization = member (op =) skolemization_steps
@@ -682,7 +688,39 @@
in
postprocess step (cx, [])
|> (fn (step, (cx, _)) => (step, cx))
- end
+ end
+
+fun combine_proof_steps ((step1 : veriT_replay_node) :: step2 :: steps) =
+ let
+ val (VeriT_Replay_Node {id = id1, rule = rule1, args = args1, prems = prems1,
+ proof_ctxt = proof_ctxt1, concl = concl1, bounds = bounds1, insts = insts1,
+ declarations = declarations1,
+ subproof = (bound_sub1, assms_sub1, assms_extra1, subproof1)}) = step1
+ val (VeriT_Replay_Node {id = id2, rule = rule2, args = args2, prems = prems2,
+ proof_ctxt = proof_ctxt2, concl = concl2, bounds = bounds2, insts = insts2,
+ declarations = declarations2,
+ subproof = (bound_sub2, assms_sub2, assms_extra2, subproof2)}) = step2
+ val goals1 =
+ (case concl1 of
+ _ $ (Const (\<^const_name>\<open>HOL.disj\<close>, _) $ _ $
+ (Const (\<^const_name>\<open>HOL.disj\<close>, _) $ (Const (\<^const_name>\<open>HOL.Not\<close>, _) $a) $ b)) => [a,b]
+ | _ => [])
+ val goal2 = (case concl2 of _ $ a => a)
+ in
+ if rule1 = equiv_pos2_rule andalso rule2 = th_resolution_rule andalso member (op =) prems2 id1
+ andalso member (op =) goals1 goal2
+ then
+ mk_replay_node id2 theory_resolution2_rule args2 (filter_out (curry (op =) id1) prems2)
+ proof_ctxt2 concl2 bounds2 insts2 declarations2
+ (bound_sub2, assms_sub2, assms_extra2, combine_proof_steps subproof2) ::
+ combine_proof_steps steps
+ else
+ mk_replay_node id1 rule1 args1 prems1
+ proof_ctxt1 concl1 bounds1 insts1 declarations1
+ (bound_sub1, assms_sub1, assms_extra1, combine_proof_steps subproof1) ::
+ combine_proof_steps (step2 :: steps)
+ end
+ | combine_proof_steps steps = steps
val linearize_proof =
@@ -749,7 +787,7 @@
B. Skolems in subproofs
Supporting this is more or less hopeless as long as the Isar reconstruction of Sledgehammer
does not support more features like definitions. veriT is able to generate proofs with skolemization
-happening in subproofs inside the formula.
+happening in subproofs inside the formula.
(assume "A \<or> P"
...
P \<longleftrightarrow> Q :skolemization in the subproof
@@ -781,7 +819,7 @@
val promote_to_skolem = exists (fn t => member (op =) skolems t) prems
val promote_from_assms = fold has_skolem_substep subproof NONE <> NONE
val promote_step = promote_to_skolem orelse promote_from_assms
- val skolem_step_to_skip = is_skolemization rule orelse
+ val skolem_step_to_skip = is_skolemization rule orelse
(promote_from_assms andalso length prems > 1)
val is_skolem = is_skolemization rule orelse promote_step
val prems = prems
@@ -820,9 +858,9 @@
|> map single
|> map SMTLIB.parse
|> map remove_all_qm2
- val (raw_steps, _, _) =
+ val (raw_steps, _, _) =
parse_raw_proof_steps NONE smtlib_lines_without_qm SMTLIB_Proof.empty_name_binding
-
+
fun process step (cx, cx') =
let fun postprocess step (cx, cx') =
let val (step, cx) = postprocess_proof compress ctxt step cx
@@ -832,6 +870,7 @@
(empty_context ctxt typs funs, [])
|> fold_map process raw_steps
|> (fn (steps, (cx, _)) => (flat steps, cx))
+ |> compress? apfst combine_proof_steps
in step end
in
--- a/src/HOL/Tools/SMT/verit_replay_methods.ML Sun Dec 13 23:11:41 2020 +0100
+++ b/src/HOL/Tools/SMT/verit_replay_methods.ML Mon Dec 14 21:02:57 2020 +0100
@@ -73,7 +73,9 @@
Eq_Simplify | ITE_Simplify | Sum_Simplify | Prod_Simplify |
Qnt_Simplify | Not_Not | Tautological_Clause | Duplicate_Literals |
(*Unsupported rule*)
- Unsupported
+ Unsupported |
+ (*For compression*)
+ Theory_Resolution2
fun verit_rule_of "bind" = Bind
@@ -82,13 +84,12 @@
| verit_rule_of "equiv1" = Equiv1
| verit_rule_of "equiv2" = Equiv2
| verit_rule_of "equiv_pos1" = Equiv_pos1
- | verit_rule_of "equiv_pos2" = Equiv_pos2
+ (*Equiv_pos2 covered below*)
| verit_rule_of "equiv_neg1" = Equiv_neg1
| verit_rule_of "equiv_neg2" = Equiv_neg2
| verit_rule_of "sko_forall" = Skolem_Forall
| verit_rule_of "sko_ex" = Skolem_Ex
| verit_rule_of "eq_reflexive" = Eq_Reflexive
- | verit_rule_of "th_resolution" = Theory_Resolution
| verit_rule_of "forall_inst" = Forall_Inst
| verit_rule_of "implies_pos" = Implies_Pos
| verit_rule_of "or" = Or
@@ -156,6 +157,9 @@
else if r = Verit_Proof.ite_intro_rule then ITE_Intro
else if r = Verit_Proof.eq_congruent_rule then Eq_Congruent
else if r = Verit_Proof.eq_congruent_pred_rule then Eq_Congruent_Pred
+ else if r = Verit_Proof.theory_resolution2_rule then Theory_Resolution2
+ else if r = Verit_Proof.th_resolution_rule then Theory_Resolution
+ else if r = Verit_Proof.equiv_pos2_rule then Equiv_pos2
else (@{print} ("Unsupport rule", r); Unsupported)
fun string_of_verit_rule Bind = "Bind"
@@ -171,6 +175,7 @@
| string_of_verit_rule Skolem_Ex = "Skolem_Ex"
| string_of_verit_rule Eq_Reflexive = "Eq_Reflexive"
| string_of_verit_rule Theory_Resolution = "Theory_Resolution"
+ | string_of_verit_rule Theory_Resolution2 = "Theory_Resolution2"
| string_of_verit_rule Forall_Inst = "forall_inst"
| string_of_verit_rule Or = "Or"
| string_of_verit_rule Not_Or = "Not_Or"
@@ -536,6 +541,8 @@
match_tac ctxt @{thms verit_or_neg}
THEN' K (unfold_tac ctxt @{thms not_not disj_assoc[symmetric]})
THEN' TRY' (match_tac ctxt @{thms notE} THEN_ALL_NEW assume_tac ctxt)
+
+ val theory_resolution2_lemma = @{lemma \<open>a \<Longrightarrow> a = b \<Longrightarrow> b\<close> by blast}
in
fun prove_abstract abstracter tac ctxt thms t =
@@ -561,6 +568,10 @@
val unit_res = prove_abstract SMT_Replay_Methods.abstract_bool_shallow SMT_Replay_Methods.prop_tac
+(*match_instantiate does not work*)
+fun theory_resolution2 ctxt prems t =
+ SMT_Replay_Methods.prove ctxt t (fn _ => match_tac ctxt [theory_resolution2_lemma OF prems])
+
end
@@ -1145,6 +1156,7 @@
| choose Or_Neg = ignore_args or_neg_rule
| choose Or_Pos = ignore_args or_pos_rule
| choose Or_Simplify = ignore_args rewrite_or_simplify
+ | choose Theory_Resolution2 = ignore_args theory_resolution2
| choose Prod_Simplify = ignore_args prod_simplify
| choose Qnt_Join = ignore_args qnt_join
| choose Qnt_Rm_Unused = ignore_args qnt_rm_unused