--- a/src/HOL/ATP.thy Wed Dec 16 15:44:17 2020 +0100
+++ b/src/HOL/ATP.thy Wed Dec 16 15:47:33 2020 +0100
@@ -1,6 +1,7 @@
(* Title: HOL/ATP.thy
Author: Fabian Immler, TU Muenchen
Author: Jasmin Blanchette, TU Muenchen
+ Author: Martin Desharnais, UniBw Muenchen
*)
section \<open>Automatic Theorem Provers (ATPs)\<close>
--- a/src/HOL/Data_Structures/Binomial_Heap.thy Wed Dec 16 15:44:17 2020 +0100
+++ b/src/HOL/Data_Structures/Binomial_Heap.thy Wed Dec 16 15:47:33 2020 +0100
@@ -541,15 +541,17 @@
(auto simp: T_ins_tree_length algebra_simps)
text \<open>Finally, we get the desired logarithmic bound\<close>
-lemma T_merge_bound_aux:
+lemma T_merge_bound:
fixes ts\<^sub>1 ts\<^sub>2
defines "n\<^sub>1 \<equiv> size (mset_heap ts\<^sub>1)"
defines "n\<^sub>2 \<equiv> size (mset_heap ts\<^sub>2)"
- assumes BINVARS: "invar ts\<^sub>1" "invar ts\<^sub>2"
+ assumes "invar ts\<^sub>1" "invar ts\<^sub>2"
shows "T_merge ts\<^sub>1 ts\<^sub>2 \<le> 4*log 2 (n\<^sub>1 + n\<^sub>2 + 1) + 2"
proof -
define n where "n = n\<^sub>1 + n\<^sub>2"
+ note BINVARS = \<open>invar ts\<^sub>1\<close> \<open>invar ts\<^sub>2\<close>
+
from T_merge_length[of ts\<^sub>1 ts\<^sub>2]
have "T_merge ts\<^sub>1 ts\<^sub>2 \<le> 2 * (length ts\<^sub>1 + length ts\<^sub>2) + 1" by auto
hence "(2::nat)^T_merge ts\<^sub>1 ts\<^sub>2 \<le> 2^(2 * (length ts\<^sub>1 + length ts\<^sub>2) + 1)"
@@ -575,14 +577,6 @@
thus ?thesis unfolding n_def by (auto simp: algebra_simps)
qed
-lemma T_merge_bound:
- fixes ts\<^sub>1 ts\<^sub>2
- defines "n\<^sub>1 \<equiv> size (mset_heap ts\<^sub>1)"
- defines "n\<^sub>2 \<equiv> size (mset_heap ts\<^sub>2)"
- assumes "invar ts\<^sub>1" "invar ts\<^sub>2"
- shows "T_merge ts\<^sub>1 ts\<^sub>2 \<le> 4*log 2 (n\<^sub>1 + n\<^sub>2 + 1) + 2"
-using assms T_merge_bound_aux unfolding invar_def by blast
-
subsubsection \<open>\<open>T_get_min\<close>\<close>
fun T_get_min :: "'a::linorder heap \<Rightarrow> nat" where
@@ -616,7 +610,7 @@
lemma T_get_min_rest_estimate: "ts\<noteq>[] \<Longrightarrow> T_get_min_rest ts = length ts"
by (induction ts rule: T_get_min_rest.induct) auto
-lemma T_get_min_rest_bound_aux:
+lemma T_get_min_rest_bound:
assumes "invar ts"
assumes "ts\<noteq>[]"
shows "T_get_min_rest ts \<le> log 2 (size (mset_heap ts) + 1)"
@@ -631,12 +625,6 @@
finally show ?thesis by auto
qed
-lemma T_get_min_rest_bound:
- assumes "invar ts"
- assumes "ts\<noteq>[]"
- shows "T_get_min_rest ts \<le> log 2 (size (mset_heap ts) + 1)"
-using assms T_get_min_rest_bound_aux unfolding invar_def by blast
-
text\<open>Note that although the definition of function \<^const>\<open>rev\<close> has quadratic complexity,
it can and is implemented (via suitable code lemmas) as a linear time function.
Thus the following definition is justified:\<close>
@@ -665,17 +653,17 @@
finally show ?thesis by (auto simp: algebra_simps)
qed
-lemma T_del_min_bound_aux:
+lemma T_del_min_bound:
fixes ts
defines "n \<equiv> size (mset_heap ts)"
- assumes BINVAR: "invar ts"
+ assumes "invar ts"
assumes "ts\<noteq>[]"
shows "T_del_min ts \<le> 6 * log 2 (n+1) + 3"
proof -
obtain r x ts\<^sub>1 ts\<^sub>2 where GM: "get_min_rest ts = (Node r x ts\<^sub>1, ts\<^sub>2)"
by (metis surj_pair tree.exhaust_sel)
- note BINVAR' = invar_get_min_rest[OF GM \<open>ts\<noteq>[]\<close> BINVAR]
+ note BINVAR' = invar_get_min_rest[OF GM \<open>ts\<noteq>[]\<close> \<open>invar ts\<close>]
hence BINVAR1: "invar (rev ts\<^sub>1)" by (blast intro: invar_children)
define n\<^sub>1 where "n\<^sub>1 = size (mset_heap ts\<^sub>1)"
@@ -694,11 +682,11 @@
have "T_del_min ts = T_get_min_rest ts + T_rev ts\<^sub>1 + T_merge (rev ts\<^sub>1) ts\<^sub>2"
unfolding T_del_min_def by (simp add: GM)
also have "\<dots> \<le> log 2 (n+1) + T_rev ts\<^sub>1 + T_merge (rev ts\<^sub>1) ts\<^sub>2"
- using T_get_min_rest_bound_aux[OF assms(2-)] by (auto simp: n_def)
+ using T_get_min_rest_bound[OF assms(2-)] by (auto simp: n_def)
also have "\<dots> \<le> 2*log 2 (n+1) + T_merge (rev ts\<^sub>1) ts\<^sub>2 + 1"
using T_rev_ts1_bound by auto
also have "\<dots> \<le> 2*log 2 (n+1) + 4 * log 2 (n\<^sub>1 + n\<^sub>2 + 1) + 3"
- using T_merge_bound_aux[OF \<open>invar (rev ts\<^sub>1)\<close> \<open>invar ts\<^sub>2\<close>]
+ using T_merge_bound[OF \<open>invar (rev ts\<^sub>1)\<close> \<open>invar ts\<^sub>2\<close>]
by (auto simp: n\<^sub>1_def n\<^sub>2_def algebra_simps)
also have "n\<^sub>1 + n\<^sub>2 \<le> n"
unfolding n\<^sub>1_def n\<^sub>2_def n_def
@@ -709,12 +697,4 @@
thus ?thesis by (simp add: algebra_simps)
qed
-lemma T_del_min_bound:
- fixes ts
- defines "n \<equiv> size (mset_heap ts)"
- assumes "invar ts"
- assumes "ts\<noteq>[]"
- shows "T_del_min ts \<le> 6 * log 2 (n+1) + 3"
-using assms T_del_min_bound_aux unfolding invar_def by blast
-
end
--- a/src/HOL/Data_Structures/Trie_Fun.thy Wed Dec 16 15:44:17 2020 +0100
+++ b/src/HOL/Data_Structures/Trie_Fun.thy Wed Dec 16 15:47:33 2020 +0100
@@ -17,12 +17,12 @@
"isin (Nd b m) [] = b" |
"isin (Nd b m) (k # xs) = (case m k of None \<Rightarrow> False | Some t \<Rightarrow> isin t xs)"
-fun insert :: "('a::linorder) list \<Rightarrow> 'a trie \<Rightarrow> 'a trie" where
+fun insert :: "'a list \<Rightarrow> 'a trie \<Rightarrow> 'a trie" where
"insert [] (Nd b m) = Nd True m" |
"insert (x#xs) (Nd b m) =
Nd b (m(x := Some(insert xs (case m x of None \<Rightarrow> empty | Some t \<Rightarrow> t))))"
-fun delete :: "('a::linorder) list \<Rightarrow> 'a trie \<Rightarrow> 'a trie" where
+fun delete :: "'a list \<Rightarrow> 'a trie \<Rightarrow> 'a trie" where
"delete [] (Nd b m) = Nd False m" |
"delete (x#xs) (Nd b m) = Nd b
(case m x of
--- a/src/HOL/Library/Tools/smt_word.ML Wed Dec 16 15:44:17 2020 +0100
+++ b/src/HOL/Library/Tools/smt_word.ML Wed Dec 16 15:47:33 2020 +0100
@@ -37,8 +37,17 @@
Option.map (rpair [] o index1 "BitVec") (try dest_binT T)
| word_typ _ = NONE
+ (*CVC4 does not support "_bvk T" when k does not fit in the BV of size T, so remove the bits that
+ will be ignored according to the SMT-LIB*)
fun word_num (Type (\<^type_name>\<open>word\<close>, [T])) k =
- Option.map (index1 ("bv" ^ string_of_int k)) (try dest_binT T)
+ let
+ val size = try dest_binT T
+ fun max_int size = IntInf.pow (2, size)
+ in
+ (case size of
+ NONE => NONE
+ | SOME size => SOME (index1 ("bv" ^ string_of_int (Int.rem(k, max_int size))) size))
+ end
| word_num _ _ = NONE
fun if_fixed pred m n T ts =
--- a/src/HOL/SMT_Examples/SMT_Examples_Verit.thy Wed Dec 16 15:44:17 2020 +0100
+++ b/src/HOL/SMT_Examples/SMT_Examples_Verit.thy Wed Dec 16 15:47:33 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/SMT_Examples/SMT_Word_Examples.certs Wed Dec 16 15:44:17 2020 +0100
+++ b/src/HOL/SMT_Examples/SMT_Word_Examples.certs Wed Dec 16 15:47:33 2020 +0100
@@ -1,13 +1,4 @@
-8e6fd56de8adc20c29f4bdb8c2c55e63988185a8 8 0
-unsat
-((set-logic <null>)
-(proof
-(let ((@x38 (monotonicity (rewrite (= (bvneg (_ bv5 4)) (_ bv11 4))) (= (= (_ bv11 4) (bvneg (_ bv5 4))) (= (_ bv11 4) (_ bv11 4))))))
-(let ((@x42 (trans @x38 (rewrite (= (= (_ bv11 4) (_ bv11 4)) true)) (= (= (_ bv11 4) (bvneg (_ bv5 4))) true))))
-(let ((@x49 (trans (monotonicity @x42 (= (not (= (_ bv11 4) (bvneg (_ bv5 4)))) (not true))) (rewrite (= (not true) false)) (= (not (= (_ bv11 4) (bvneg (_ bv5 4)))) false))))
-(mp (asserted (not (= (_ bv11 4) (bvneg (_ bv5 4))))) @x49 false))))))
-
-aa1cdd144e99278cb2bdb51d68a75ec8d25b433d 7 0
+152f808e76881b6ae41a49c63654f988bc675b52 7 0
unsat
((set-logic <null>)
(proof
@@ -15,372 +6,7 @@
(let ((@x39 (trans @x35 (rewrite (= (not true) false)) (= (not (= (_ bv11 4) (_ bv11 4))) false))))
(mp (asserted (not (= (_ bv11 4) (_ bv11 4)))) @x39 false)))))
-a14afea8a52a1586ff44eff03b88f1717144d17a 7 0
-unsat
-((set-logic <null>)
-(proof
-(let ((@x38 (monotonicity (rewrite (= (bvult (_ bv23 8) (_ bv27 8)) true)) (= (not (bvult (_ bv23 8) (_ bv27 8))) (not true)))))
-(let ((@x42 (trans @x38 (rewrite (= (not true) false)) (= (not (bvult (_ bv23 8) (_ bv27 8))) false))))
-(mp (asserted (not (bvult (_ bv23 8) (_ bv27 8)))) @x42 false)))))
-
-282d94be68c87485ea9ec13e80f6f2a51b18f5bd 9 0
-unsat
-((set-logic <null>)
-(proof
-(let ((@x38 (monotonicity (rewrite (= (bvadd (_ bv27 5) (_ bv11 5)) (_ bv6 5))) (= (= (bvadd (_ bv27 5) (_ bv11 5)) (_ bv6 5)) (= (_ bv6 5) (_ bv6 5))))))
-(let ((@x42 (trans @x38 (rewrite (= (= (_ bv6 5) (_ bv6 5)) true)) (= (= (bvadd (_ bv27 5) (_ bv11 5)) (_ bv6 5)) true))))
-(let ((@x45 (monotonicity @x42 (= (not (= (bvadd (_ bv27 5) (_ bv11 5)) (_ bv6 5))) (not true)))))
-(let ((@x49 (trans @x45 (rewrite (= (not true) false)) (= (not (= (bvadd (_ bv27 5) (_ bv11 5)) (_ bv6 5))) false))))
-(mp (asserted (not (= (bvadd (_ bv27 5) (_ bv11 5)) (_ bv6 5)))) @x49 false)))))))
-
-4df99826f79b2c96079a4c58ea51a58b8cc6199c 9 0
-unsat
-((set-logic <null>)
-(proof
-(let ((@x38 (monotonicity (rewrite (= (bvmul (_ bv7 8) (_ bv3 8)) (_ bv21 8))) (= (= (bvmul (_ bv7 8) (_ bv3 8)) (_ bv21 8)) (= (_ bv21 8) (_ bv21 8))))))
-(let ((@x42 (trans @x38 (rewrite (= (= (_ bv21 8) (_ bv21 8)) true)) (= (= (bvmul (_ bv7 8) (_ bv3 8)) (_ bv21 8)) true))))
-(let ((@x45 (monotonicity @x42 (= (not (= (bvmul (_ bv7 8) (_ bv3 8)) (_ bv21 8))) (not true)))))
-(let ((@x49 (trans @x45 (rewrite (= (not true) false)) (= (not (= (bvmul (_ bv7 8) (_ bv3 8)) (_ bv21 8))) false))))
-(mp (asserted (not (= (bvmul (_ bv7 8) (_ bv3 8)) (_ bv21 8)))) @x49 false)))))))
-
-45bf9e0a746f7dde46f8242e5851928c2671c7f2 9 0
-unsat
-((set-logic <null>)
-(proof
-(let ((@x43 (monotonicity (rewrite (= (bvsub (_ bv11 8) (_ bv27 8)) (_ bv240 8))) (rewrite (= (bvneg (_ bv16 8)) (_ bv240 8))) (= (= (bvsub (_ bv11 8) (_ bv27 8)) (bvneg (_ bv16 8))) (= (_ bv240 8) (_ bv240 8))))))
-(let ((@x47 (trans @x43 (rewrite (= (= (_ bv240 8) (_ bv240 8)) true)) (= (= (bvsub (_ bv11 8) (_ bv27 8)) (bvneg (_ bv16 8))) true))))
-(let ((@x50 (monotonicity @x47 (= (not (= (bvsub (_ bv11 8) (_ bv27 8)) (bvneg (_ bv16 8)))) (not true)))))
-(let ((@x54 (trans @x50 (rewrite (= (not true) false)) (= (not (= (bvsub (_ bv11 8) (_ bv27 8)) (bvneg (_ bv16 8)))) false))))
-(mp (asserted (not (= (bvsub (_ bv11 8) (_ bv27 8)) (bvneg (_ bv16 8))))) @x54 false)))))))
-
-6dd848d7b26e0521039e21a5e2bafebc1fee8c9b 7 0
-unsat
-((set-logic <null>)
-(proof
-(let ((@x35 (monotonicity (rewrite (= (= (_ bv11 5) (_ bv11 5)) true)) (= (not (= (_ bv11 5) (_ bv11 5))) (not true)))))
-(let ((@x39 (trans @x35 (rewrite (= (not true) false)) (= (not (= (_ bv11 5) (_ bv11 5))) false))))
-(mp (asserted (not (= (_ bv11 5) (_ bv11 5)))) @x39 false)))))
-
-00a7ff287d9c23d984163ea8e0cac8ac61008afd 11 0
-unsat
-((set-logic <null>)
-(proof
-(let ((@x42 (monotonicity (rewrite (= (bvneg (_ bv40 7)) (_ bv88 7))) (= (bvadd (bvneg (_ bv40 7)) (_ bv1 7)) (bvadd (_ bv88 7) (_ bv1 7))))))
-(let ((@x47 (trans @x42 (rewrite (= (bvadd (_ bv88 7) (_ bv1 7)) (_ bv89 7))) (= (bvadd (bvneg (_ bv40 7)) (_ bv1 7)) (_ bv89 7)))))
-(let ((@x52 (monotonicity @x47 (rewrite (= (bvneg (_ bv39 7)) (_ bv89 7))) (= (= (bvadd (bvneg (_ bv40 7)) (_ bv1 7)) (bvneg (_ bv39 7))) (= (_ bv89 7) (_ bv89 7))))))
-(let ((@x56 (trans @x52 (rewrite (= (= (_ bv89 7) (_ bv89 7)) true)) (= (= (bvadd (bvneg (_ bv40 7)) (_ bv1 7)) (bvneg (_ bv39 7))) true))))
-(let ((@x59 (monotonicity @x56 (= (not (= (bvadd (bvneg (_ bv40 7)) (_ bv1 7)) (bvneg (_ bv39 7)))) (not true)))))
-(let ((@x63 (trans @x59 (rewrite (= (not true) false)) (= (not (= (bvadd (bvneg (_ bv40 7)) (_ bv1 7)) (bvneg (_ bv39 7)))) false))))
-(mp (asserted (not (= (bvadd (bvneg (_ bv40 7)) (_ bv1 7)) (bvneg (_ bv39 7))))) @x63 false)))))))))
-
-9673ca576ccae343db48aa68f876fd3a2515cc33 19 0
-unsat
-((set-logic <null>)
-(proof
-(let ((?x35 (bvadd b$ c$)))
-(let ((?x36 (bvadd ?x35 a$)))
-(let ((?x30 (bvmul (_ bv2 32) b$)))
-(let ((?x31 (bvadd a$ ?x30)))
-(let ((?x33 (bvadd ?x31 c$)))
-(let ((?x34 (bvsub ?x33 b$)))
-(let (($x37 (= ?x34 ?x36)))
-(let (($x38 (not $x37)))
-(let ((@x58 (rewrite (= (= (bvadd a$ b$ c$) (bvadd a$ b$ c$)) true))))
-(let ((@x48 (rewrite (= (bvsub (bvadd a$ ?x30 c$) b$) (bvadd a$ b$ c$)))))
-(let ((@x46 (monotonicity (rewrite (= ?x33 (bvadd a$ ?x30 c$))) (= ?x34 (bvsub (bvadd a$ ?x30 c$) b$)))))
-(let ((@x56 (monotonicity (trans @x46 @x48 (= ?x34 (bvadd a$ b$ c$))) (rewrite (= ?x36 (bvadd a$ b$ c$))) (= $x37 (= (bvadd a$ b$ c$) (bvadd a$ b$ c$))))))
-(let ((@x63 (monotonicity (trans @x56 @x58 (= $x37 true)) (= $x38 (not true)))))
-(let ((@x67 (trans @x63 (rewrite (= (not true) false)) (= $x38 false))))
-(mp (asserted $x38) @x67 false)))))))))))))))))
-
-b4600e6d14c88b633ac7bcc5b2e24af8539b0218 18 0
-unsat
-((set-logic <null>)
-(proof
-(let ((?x31 (bvmul (_ bv4 4) x$)))
-(let (($x32 (= ?x31 (_ bv4 4))))
-(let (($x43 (= (_ bv5 4) x$)))
-(let (($x56 (not (or (not $x43) (= (_ bv4 4) ?x31)))))
-(let ((@x48 (monotonicity (rewrite (= (= x$ (_ bv5 4)) $x43)) (= (not (= x$ (_ bv5 4))) (not $x43)))))
-(let ((@x55 (monotonicity @x48 (rewrite (= $x32 (= (_ bv4 4) ?x31))) (= (or (not (= x$ (_ bv5 4))) $x32) (or (not $x43) (= (_ bv4 4) ?x31))))))
-(let (($x34 (not (=> (= x$ (_ bv5 4)) $x32))))
-(let ((@x39 (rewrite (= (=> (= x$ (_ bv5 4)) $x32) (or (not (= x$ (_ bv5 4))) $x32)))))
-(let ((@x60 (trans (monotonicity @x39 (= $x34 (not (or (not (= x$ (_ bv5 4))) $x32)))) (monotonicity @x55 (= (not (or (not (= x$ (_ bv5 4))) $x32)) $x56)) (= $x34 $x56))))
-(let ((@x67 (monotonicity (not-or-elim (mp (asserted $x34) @x60 $x56) $x43) (= ?x31 (bvmul (_ bv4 4) (_ bv5 4))))))
-(let ((@x73 (monotonicity (trans @x67 (rewrite (= (bvmul (_ bv4 4) (_ bv5 4)) (_ bv4 4))) $x32) (= (= (_ bv4 4) ?x31) (= (_ bv4 4) (_ bv4 4))))))
-(let ((@x77 (trans @x73 (rewrite (= (= (_ bv4 4) (_ bv4 4)) true)) (= (= (_ bv4 4) ?x31) true))))
-(let ((@x84 (trans (monotonicity @x77 (= (not (= (_ bv4 4) ?x31)) (not true))) (rewrite (= (not true) false)) (= (not (= (_ bv4 4) ?x31)) false))))
-(mp (not-or-elim (mp (asserted $x34) @x60 $x56) (not (= (_ bv4 4) ?x31))) @x84 false))))))))))))))))
-
-d150015a66b6757a72346710966844993c0f3c27 9 0
-unsat
-((set-logic <null>)
-(proof
-(let ((@x37 (monotonicity (rewrite (= (bvand (_ bv6 32) (_ bv5 32)) (_ bv4 32))) (= (= (bvand (_ bv6 32) (_ bv5 32)) (_ bv4 32)) (= (_ bv4 32) (_ bv4 32))))))
-(let ((@x41 (trans @x37 (rewrite (= (= (_ bv4 32) (_ bv4 32)) true)) (= (= (bvand (_ bv6 32) (_ bv5 32)) (_ bv4 32)) true))))
-(let ((@x44 (monotonicity @x41 (= (not (= (bvand (_ bv6 32) (_ bv5 32)) (_ bv4 32))) (not true)))))
-(let ((@x48 (trans @x44 (rewrite (= (not true) false)) (= (not (= (bvand (_ bv6 32) (_ bv5 32)) (_ bv4 32))) false))))
-(mp (asserted (not (= (bvand (_ bv6 32) (_ bv5 32)) (_ bv4 32)))) @x48 false)))))))
-
-200e29aa9f19844d244c5c9755155eb956c5cf7c 9 0
-unsat
-((set-logic <null>)
-(proof
-(let ((@x37 (monotonicity (rewrite (= (bvor (_ bv6 8) (_ bv3 8)) (_ bv7 8))) (= (= (bvor (_ bv6 8) (_ bv3 8)) (_ bv7 8)) (= (_ bv7 8) (_ bv7 8))))))
-(let ((@x41 (trans @x37 (rewrite (= (= (_ bv7 8) (_ bv7 8)) true)) (= (= (bvor (_ bv6 8) (_ bv3 8)) (_ bv7 8)) true))))
-(let ((@x44 (monotonicity @x41 (= (not (= (bvor (_ bv6 8) (_ bv3 8)) (_ bv7 8))) (not true)))))
-(let ((@x48 (trans @x44 (rewrite (= (not true) false)) (= (not (= (bvor (_ bv6 8) (_ bv3 8)) (_ bv7 8))) false))))
-(mp (asserted (not (= (bvor (_ bv6 8) (_ bv3 8)) (_ bv7 8)))) @x48 false)))))))
-
-d7cc0827eb340c29b0f489145022e4b3e3610818 9 0
-unsat
-((set-logic <null>)
-(proof
-(let ((@x37 (monotonicity (rewrite (= (bvxor (_ bv240 8) (_ bv255 8)) (_ bv15 8))) (= (= (bvxor (_ bv240 8) (_ bv255 8)) (_ bv15 8)) (= (_ bv15 8) (_ bv15 8))))))
-(let ((@x41 (trans @x37 (rewrite (= (= (_ bv15 8) (_ bv15 8)) true)) (= (= (bvxor (_ bv240 8) (_ bv255 8)) (_ bv15 8)) true))))
-(let ((@x44 (monotonicity @x41 (= (not (= (bvxor (_ bv240 8) (_ bv255 8)) (_ bv15 8))) (not true)))))
-(let ((@x48 (trans @x44 (rewrite (= (not true) false)) (= (not (= (bvxor (_ bv240 8) (_ bv255 8)) (_ bv15 8))) false))))
-(mp (asserted (not (= (bvxor (_ bv240 8) (_ bv255 8)) (_ bv15 8)))) @x48 false)))))))
-
-3838eb33edcd292c3a0ecbf1662b54af3940189f 8 0
-unsat
-((set-logic <null>)
-(proof
-(let ((@x36 (monotonicity (rewrite (= (bvnot (_ bv240 16)) (_ bv65295 16))) (= (= (bvnot (_ bv240 16)) (_ bv65295 16)) (= (_ bv65295 16) (_ bv65295 16))))))
-(let ((@x40 (trans @x36 (rewrite (= (= (_ bv65295 16) (_ bv65295 16)) true)) (= (= (bvnot (_ bv240 16)) (_ bv65295 16)) true))))
-(let ((@x47 (trans (monotonicity @x40 (= (not (= (bvnot (_ bv240 16)) (_ bv65295 16))) (not true))) (rewrite (= (not true) false)) (= (not (= (bvnot (_ bv240 16)) (_ bv65295 16))) false))))
-(mp (asserted (not (= (bvnot (_ bv240 16)) (_ bv65295 16)))) @x47 false))))))
-
-14431ccb33137348161eb6ca6cfb2e57942c3f9d 9 0
-unsat
-((set-logic <null>)
-(proof
-(let ((@x37 (monotonicity (rewrite (= (concat (_ bv11 4) (_ bv27 8)) (_ bv2843 12))) (= (= (concat (_ bv11 4) (_ bv27 8)) (_ bv2843 12)) (= (_ bv2843 12) (_ bv2843 12))))))
-(let ((@x41 (trans @x37 (rewrite (= (= (_ bv2843 12) (_ bv2843 12)) true)) (= (= (concat (_ bv11 4) (_ bv27 8)) (_ bv2843 12)) true))))
-(let ((@x44 (monotonicity @x41 (= (not (= (concat (_ bv11 4) (_ bv27 8)) (_ bv2843 12))) (not true)))))
-(let ((@x48 (trans @x44 (rewrite (= (not true) false)) (= (not (= (concat (_ bv11 4) (_ bv27 8)) (_ bv2843 12))) false))))
-(mp (asserted (not (= (concat (_ bv11 4) (_ bv27 8)) (_ bv2843 12)))) @x48 false)))))))
-
-880bee16a8f6469b14122277b92e87533ef6a071 9 0
-unsat
-((set-logic <null>)
-(proof
-(let ((@x37 (monotonicity (rewrite (= (concat (_ bv3 4) (_ bv15 6)) (_ bv207 10))) (= (= (concat (_ bv3 4) (_ bv15 6)) (_ bv207 10)) (= (_ bv207 10) (_ bv207 10))))))
-(let ((@x41 (trans @x37 (rewrite (= (= (_ bv207 10) (_ bv207 10)) true)) (= (= (concat (_ bv3 4) (_ bv15 6)) (_ bv207 10)) true))))
-(let ((@x44 (monotonicity @x41 (= (not (= (concat (_ bv3 4) (_ bv15 6)) (_ bv207 10))) (not true)))))
-(let ((@x48 (trans @x44 (rewrite (= (not true) false)) (= (not (= (concat (_ bv3 4) (_ bv15 6)) (_ bv207 10))) false))))
-(mp (asserted (not (= (concat (_ bv3 4) (_ bv15 6)) (_ bv207 10)))) @x48 false)))))))
-
-b48f55cefc567df166d8e9967c53372c30620183 8 0
-unsat
-((set-logic <null>)
-(proof
-(let ((@x36 (monotonicity (rewrite (= ((_ extract 2 1) (_ bv6 4)) (_ bv3 2))) (= (= ((_ extract 2 1) (_ bv6 4)) (_ bv3 2)) (= (_ bv3 2) (_ bv3 2))))))
-(let ((@x40 (trans @x36 (rewrite (= (= (_ bv3 2) (_ bv3 2)) true)) (= (= ((_ extract 2 1) (_ bv6 4)) (_ bv3 2)) true))))
-(let ((@x47 (trans (monotonicity @x40 (= (not (= ((_ extract 2 1) (_ bv6 4)) (_ bv3 2))) (not true))) (rewrite (= (not true) false)) (= (not (= ((_ extract 2 1) (_ bv6 4)) (_ bv3 2))) false))))
-(mp (asserted (not (= ((_ extract 2 1) (_ bv6 4)) (_ bv3 2)))) @x47 false))))))
-
-446b3cb9d63aa1f488dc092ed3fb111d2ad50b4e 9 0
-unsat
-((set-logic <null>)
-(proof
-(let ((@x36 (monotonicity (rewrite (= ((_ zero_extend 6) (_ bv10 4)) (_ bv10 10))) (= (= ((_ zero_extend 6) (_ bv10 4)) (_ bv10 10)) (= (_ bv10 10) (_ bv10 10))))))
-(let ((@x40 (trans @x36 (rewrite (= (= (_ bv10 10) (_ bv10 10)) true)) (= (= ((_ zero_extend 6) (_ bv10 4)) (_ bv10 10)) true))))
-(let ((@x43 (monotonicity @x40 (= (not (= ((_ zero_extend 6) (_ bv10 4)) (_ bv10 10))) (not true)))))
-(let ((@x47 (trans @x43 (rewrite (= (not true) false)) (= (not (= ((_ zero_extend 6) (_ bv10 4)) (_ bv10 10))) false))))
-(mp (asserted (not (= ((_ zero_extend 6) (_ bv10 4)) (_ bv10 10)))) @x47 false)))))))
-
-956d8b6229140c8c4aa869ab0f3765697ab8ff25 9 0
-unsat
-((set-logic <null>)
-(proof
-(let ((@x36 (monotonicity (rewrite (= ((_ sign_extend 2) (_ bv10 4)) (_ bv58 6))) (= (= ((_ sign_extend 2) (_ bv10 4)) (_ bv58 6)) (= (_ bv58 6) (_ bv58 6))))))
-(let ((@x40 (trans @x36 (rewrite (= (= (_ bv58 6) (_ bv58 6)) true)) (= (= ((_ sign_extend 2) (_ bv10 4)) (_ bv58 6)) true))))
-(let ((@x43 (monotonicity @x40 (= (not (= ((_ sign_extend 2) (_ bv10 4)) (_ bv58 6))) (not true)))))
-(let ((@x47 (trans @x43 (rewrite (= (not true) false)) (= (not (= ((_ sign_extend 2) (_ bv10 4)) (_ bv58 6))) false))))
-(mp (asserted (not (= ((_ sign_extend 2) (_ bv10 4)) (_ bv58 6)))) @x47 false)))))))
-
-24e98aaba1a95c03812c938201b3faa04d97c341 9 0
-unsat
-((set-logic <null>)
-(proof
-(let ((@x37 (monotonicity (rewrite (= (bvshl (_ bv19 8) (_ bv2 8)) (_ bv76 8))) (= (= (bvshl (_ bv19 8) (_ bv2 8)) (_ bv76 8)) (= (_ bv76 8) (_ bv76 8))))))
-(let ((@x41 (trans @x37 (rewrite (= (= (_ bv76 8) (_ bv76 8)) true)) (= (= (bvshl (_ bv19 8) (_ bv2 8)) (_ bv76 8)) true))))
-(let ((@x44 (monotonicity @x41 (= (not (= (bvshl (_ bv19 8) (_ bv2 8)) (_ bv76 8))) (not true)))))
-(let ((@x48 (trans @x44 (rewrite (= (not true) false)) (= (not (= (bvshl (_ bv19 8) (_ bv2 8)) (_ bv76 8))) false))))
-(mp (asserted (not (= (bvshl (_ bv19 8) (_ bv2 8)) (_ bv76 8)))) @x48 false)))))))
-
-c13d08f3c98afca39a5c9317ed8ca7b7d4e35b5a 9 0
-unsat
-((set-logic <null>)
-(proof
-(let ((@x37 (monotonicity (rewrite (= (bvlshr (_ bv25 8) (_ bv2 8)) (_ bv6 8))) (= (= (bvlshr (_ bv25 8) (_ bv2 8)) (_ bv6 8)) (= (_ bv6 8) (_ bv6 8))))))
-(let ((@x41 (trans @x37 (rewrite (= (= (_ bv6 8) (_ bv6 8)) true)) (= (= (bvlshr (_ bv25 8) (_ bv2 8)) (_ bv6 8)) true))))
-(let ((@x44 (monotonicity @x41 (= (not (= (bvlshr (_ bv25 8) (_ bv2 8)) (_ bv6 8))) (not true)))))
-(let ((@x48 (trans @x44 (rewrite (= (not true) false)) (= (not (= (bvlshr (_ bv25 8) (_ bv2 8)) (_ bv6 8))) false))))
-(mp (asserted (not (= (bvlshr (_ bv25 8) (_ bv2 8)) (_ bv6 8)))) @x48 false)))))))
-
-053f04ff749dbee44bfba8828181ab0a78473f75 9 0
-unsat
-((set-logic <null>)
-(proof
-(let ((@x37 (monotonicity (rewrite (= (bvashr (_ bv19 8) (_ bv2 8)) (_ bv4 8))) (= (= (bvashr (_ bv19 8) (_ bv2 8)) (_ bv4 8)) (= (_ bv4 8) (_ bv4 8))))))
-(let ((@x41 (trans @x37 (rewrite (= (= (_ bv4 8) (_ bv4 8)) true)) (= (= (bvashr (_ bv19 8) (_ bv2 8)) (_ bv4 8)) true))))
-(let ((@x44 (monotonicity @x41 (= (not (= (bvashr (_ bv19 8) (_ bv2 8)) (_ bv4 8))) (not true)))))
-(let ((@x48 (trans @x44 (rewrite (= (not true) false)) (= (not (= (bvashr (_ bv19 8) (_ bv2 8)) (_ bv4 8))) false))))
-(mp (asserted (not (= (bvashr (_ bv19 8) (_ bv2 8)) (_ bv4 8)))) @x48 false)))))))
-
-42de7906f9755bf3d790213172b0ec7fab46237c 9 0
-unsat
-((set-logic <null>)
-(proof
-(let ((@x36 (monotonicity (rewrite (= ((_ rotate_right 2) (_ bv6 4)) (_ bv9 4))) (= (= ((_ rotate_right 2) (_ bv6 4)) (_ bv9 4)) (= (_ bv9 4) (_ bv9 4))))))
-(let ((@x40 (trans @x36 (rewrite (= (= (_ bv9 4) (_ bv9 4)) true)) (= (= ((_ rotate_right 2) (_ bv6 4)) (_ bv9 4)) true))))
-(let ((@x43 (monotonicity @x40 (= (not (= ((_ rotate_right 2) (_ bv6 4)) (_ bv9 4))) (not true)))))
-(let ((@x47 (trans @x43 (rewrite (= (not true) false)) (= (not (= ((_ rotate_right 2) (_ bv6 4)) (_ bv9 4))) false))))
-(mp (asserted (not (= ((_ rotate_right 2) (_ bv6 4)) (_ bv9 4)))) @x47 false)))))))
-
-6b83b0b418738896f8c64ad12f5670cb5bf96e0f 9 0
-unsat
-((set-logic <null>)
-(proof
-(let ((@x36 (monotonicity (rewrite (= ((_ rotate_left 1) (_ bv14 4)) (_ bv13 4))) (= (= ((_ rotate_left 1) (_ bv14 4)) (_ bv13 4)) (= (_ bv13 4) (_ bv13 4))))))
-(let ((@x40 (trans @x36 (rewrite (= (= (_ bv13 4) (_ bv13 4)) true)) (= (= ((_ rotate_left 1) (_ bv14 4)) (_ bv13 4)) true))))
-(let ((@x43 (monotonicity @x40 (= (not (= ((_ rotate_left 1) (_ bv14 4)) (_ bv13 4))) (not true)))))
-(let ((@x47 (trans @x43 (rewrite (= (not true) false)) (= (not (= ((_ rotate_left 1) (_ bv14 4)) (_ bv13 4))) false))))
-(mp (asserted (not (= ((_ rotate_left 1) (_ bv14 4)) (_ bv13 4)))) @x47 false)))))))
-
-5c4e275bed2d91897e820ccd6744b0a775a6e26e 17 0
-unsat
-((set-logic <null>)
-(proof
-(let ((?x31 (bvand x$ (_ bv255 16))))
-(let ((?x29 (bvand x$ (_ bv65280 16))))
-(let ((?x32 (bvor ?x29 ?x31)))
-(let (($x33 (= ?x32 x$)))
-(let (($x34 (not $x33)))
-(let ((@x59 (symm (commutativity (= (= x$ ?x32) $x33)) (= $x33 (= x$ ?x32)))))
-(let ((@x35 (asserted $x34)))
-(let ((@x63 (mp @x35 (monotonicity @x59 (= $x34 (not (= x$ ?x32)))) (not (= x$ ?x32)))))
-(let (($x52 (= x$ ?x32)))
-(let ((@x26 (true-axiom true)))
-(let (($x53 (or $x52 false false false false false false false false false false false false false false false false)))
-(let ((@x55 (unit-resolution ((_ th-lemma bv) $x53) @x26 @x26 @x26 @x26 @x26 @x26 @x26 @x26 @x26 @x26 @x26 @x26 @x26 @x26 @x26 @x26 $x52)))
-(unit-resolution @x55 @x63 false)))))))))))))))
-
-1d4a0e2a4449a8adbcf5a134bf7f2b0ee940d954 51 0
-unsat
-((set-logic <null>)
-(proof
-(let ((?x31 (bvand w$ (_ bv255 16))))
-(let (($x32 (= ?x31 w$)))
-(let (($x64 (not $x32)))
-(let ((@x318 (symm (commutativity (= (= w$ ?x31) $x32)) (= $x32 (= w$ ?x31)))))
-(let (($x57 (not (or (bvule (_ bv256 16) w$) $x32))))
-(let ((@x49 (monotonicity (rewrite (= (bvult w$ (_ bv256 16)) (not (bvule (_ bv256 16) w$)))) (= (not (bvult w$ (_ bv256 16))) (not (not (bvule (_ bv256 16) w$)))))))
-(let ((@x53 (trans @x49 (rewrite (= (not (not (bvule (_ bv256 16) w$))) (bvule (_ bv256 16) w$))) (= (not (bvult w$ (_ bv256 16))) (bvule (_ bv256 16) w$)))))
-(let ((@x56 (monotonicity @x53 (= (or (not (bvult w$ (_ bv256 16))) $x32) (or (bvule (_ bv256 16) w$) $x32)))))
-(let ((@x59 (monotonicity @x56 (= (not (or (not (bvult w$ (_ bv256 16))) $x32)) $x57))))
-(let (($x34 (not (=> (bvult w$ (_ bv256 16)) $x32))))
-(let ((@x39 (rewrite (= (=> (bvult w$ (_ bv256 16)) $x32) (or (not (bvult w$ (_ bv256 16))) $x32)))))
-(let ((@x42 (monotonicity @x39 (= $x34 (not (or (not (bvult w$ (_ bv256 16))) $x32))))))
-(let ((@x65 (not-or-elim (mp (asserted $x34) (trans @x42 @x59 (= $x34 $x57)) $x57) $x64)))
-(let ((@x322 (mp @x65 (monotonicity @x318 (= $x64 (not (= w$ ?x31)))) (not (= w$ ?x31)))))
-(let (($x300 (= w$ ?x31)))
-(let (($x81 (= ((_ extract 15 15) w$) (_ bv1 1))))
-(let (($x264 (not $x81)))
-(let (($x74 (= ((_ extract 8 8) w$) (_ bv1 1))))
-(let (($x75 (= ((_ extract 9 9) w$) (_ bv1 1))))
-(let (($x82 (and $x75 $x74)))
-(let (($x83 (or $x75 $x74 $x82)))
-(let (($x76 (= ((_ extract 10 10) w$) (_ bv1 1))))
-(let (($x84 (and $x76 $x83)))
-(let (($x85 (or $x76 $x75 $x74 $x82 $x84)))
-(let (($x77 (= ((_ extract 11 11) w$) (_ bv1 1))))
-(let (($x86 (and $x77 $x85)))
-(let (($x87 (or $x77 $x76 $x75 $x74 $x82 $x84 $x86)))
-(let (($x78 (= ((_ extract 12 12) w$) (_ bv1 1))))
-(let (($x88 (and $x78 $x87)))
-(let (($x89 (or $x78 $x77 $x76 $x75 $x74 $x82 $x84 $x86 $x88)))
-(let (($x79 (= ((_ extract 13 13) w$) (_ bv1 1))))
-(let (($x90 (and $x79 $x89)))
-(let (($x91 (or $x79 $x78 $x77 $x76 $x75 $x74 $x82 $x84 $x86 $x88 $x90)))
-(let (($x80 (= ((_ extract 14 14) w$) (_ bv1 1))))
-(let (($x92 (and $x80 $x91)))
-(let (($x93 (or $x80 $x79 $x78 $x77 $x76 $x75 $x74 $x82 $x84 $x86 $x88 $x90 $x92)))
-(let (($x94 (and $x81 $x93)))
-(let (($x95 (or $x81 $x80 $x79 $x78 $x77 $x76 $x75 $x74 $x82 $x84 $x86 $x88 $x90 $x92 $x94)))
-(let (($x297 (not $x95)))
-(let (($x43 (bvule (_ bv256 16) w$)))
-(let (($x44 (not $x43)))
-(let ((@x63 (not-or-elim (mp (asserted $x34) (trans @x42 @x59 (= $x34 $x57)) $x57) $x44)))
-(let ((@x303 (unit-resolution ((_ th-lemma bv) (or $x43 $x297)) @x63 $x297)))
-(let ((@x26 (true-axiom true)))
-(let (($x312 (or $x300 false false false false false false false false $x74 $x75 $x76 $x77 $x78 $x79 $x80 $x81)))
-(let ((@x314 (unit-resolution ((_ th-lemma bv) $x312) @x26 @x26 @x26 @x26 @x26 @x26 @x26 @x26 (unit-resolution (def-axiom (or $x95 (not $x74))) @x303 (not $x74)) (unit-resolution (def-axiom (or $x95 (not $x75))) @x303 (not $x75)) (unit-resolution (def-axiom (or $x95 (not $x76))) @x303 (not $x76)) (unit-resolution (def-axiom (or $x95 (not $x77))) @x303 (not $x77)) (unit-resolution (def-axiom (or $x95 (not $x78))) @x303 (not $x78)) (unit-resolution (def-axiom (or $x95 (not $x79))) @x303 (not $x79)) (unit-resolution (def-axiom (or $x95 (not $x80))) @x303 (not $x80)) (unit-resolution (def-axiom (or $x95 $x264)) @x303 $x264) $x300)))
-(unit-resolution @x314 @x322 false)))))))))))))))))))))))))))))))))))))))))))))))))
-
-115ab22c9945d493b971e69a38d9e608c5b40a71 29 0
-unsat
-((set-logic <null>)
-(proof
-(let ((?x28 (bv2int$ (_ bv0 2))))
-(let (($x183 (<= ?x28 0)))
-(let (($x184 (not $x183)))
-(let (($x175 (forall ((?v0 (_ BitVec 2)) )(! (let ((?x47 (bv2int$ ?v0)))
-(let (($x53 (<= ?x47 0)))
-(not $x53))) :pattern ( (bv2int$ ?v0) ) :qid k!9))
-))
-(let (($x57 (forall ((?v0 (_ BitVec 2)) )(! (let ((?x47 (bv2int$ ?v0)))
-(let (($x53 (<= ?x47 0)))
-(not $x53))) :qid k!9))
-))
-(let ((@x177 (refl (= (not (<= (bv2int$ ?0) 0)) (not (<= (bv2int$ ?0) 0))))))
-(let ((@x112 (refl (~ (not (<= (bv2int$ ?0) 0)) (not (<= (bv2int$ ?0) 0))))))
-(let (($x49 (forall ((?v0 (_ BitVec 2)) )(! (let ((?x47 (bv2int$ ?v0)))
-(< 0 ?x47)) :qid k!9))
-))
-(let ((@x56 (rewrite (= (< 0 (bv2int$ ?0)) (not (<= (bv2int$ ?0) 0))))))
-(let ((@x115 (mp~ (mp (asserted $x49) (quant-intro @x56 (= $x49 $x57)) $x57) (nnf-pos @x112 (~ $x57 $x57)) $x57)))
-(let ((@x180 (mp @x115 (quant-intro @x177 (= $x57 $x175)) $x175)))
-(let (($x187 (not $x175)))
-(let (($x188 (or $x187 $x184)))
-(let ((@x189 ((_ quant-inst (_ bv0 2)) $x188)))
-(let (($x29 (= ?x28 0)))
-(let ((@x30 (asserted $x29)))
-(unit-resolution ((_ th-lemma arith triangle-eq) (or (not $x29) $x183)) @x30 (unit-resolution @x189 @x180 $x184) false)))))))))))))))))))
-
-d14e7b8f0d1858316e700b4eb09e7d03e57cf9c3 16 0
-unsat
-((set-logic <null>)
-(proof
-(let ((?x32 (p$ true)))
-(let (($x29 (bvule (_ bv0 4) a$)))
-(let (($x30 (ite $x29 true false)))
-(let ((?x31 (p$ $x30)))
-(let (($x33 (= ?x31 ?x32)))
-(let (($x34 (not $x33)))
-(let ((@x52 (monotonicity (monotonicity (rewrite (= $x29 true)) (= (p$ $x29) ?x32)) (= (= (p$ $x29) ?x32) (= ?x32 ?x32)))))
-(let ((@x56 (trans @x52 (rewrite (= (= ?x32 ?x32) true)) (= (= (p$ $x29) ?x32) true))))
-(let ((@x63 (trans (monotonicity @x56 (= (not (= (p$ $x29) ?x32)) (not true))) (rewrite (= (not true) false)) (= (not (= (p$ $x29) ?x32)) false))))
-(let ((@x43 (monotonicity (monotonicity (rewrite (= $x30 $x29)) (= ?x31 (p$ $x29))) (= $x33 (= (p$ $x29) ?x32)))))
-(let ((@x46 (monotonicity @x43 (= $x34 (not (= (p$ $x29) ?x32))))))
-(mp (asserted $x34) (trans @x46 @x63 (= $x34 false)) false))))))))))))))
-
-6182523304a5597432fa1bb8dd16e804ddd8d7ee 12 0
-unsat
-((set-logic <null>)
-(proof
-(let ((?x31 (p$ true)))
-(let (($x29 (bvule (_ bv0 4) a$)))
-(let ((?x30 (p$ $x29)))
-(let (($x32 (= ?x30 ?x31)))
-(let ((@x42 (monotonicity (monotonicity (rewrite (= $x29 true)) $x32) (= $x32 (= ?x31 ?x31)))))
-(let ((@x49 (monotonicity (trans @x42 (rewrite (= (= ?x31 ?x31) true)) (= $x32 true)) (= (not $x32) (not true)))))
-(let ((@x53 (trans @x49 (rewrite (= (not true) false)) (= (not $x32) false))))
-(mp (asserted (not $x32)) @x53 false))))))))))
-
-9f7a96d88c6326ad836384c37d13934828ff726d 8 0
+9fbec967ab26119b905e134e9f6da22a94ff68aa 8 0
unsat
((set-logic <null>)
(proof
@@ -389,14 +15,6 @@
(let ((@x49 (trans (monotonicity @x42 (= (not (= (_ bv11 4) (bvneg (_ bv5 4)))) (not true))) (rewrite (= (not true) false)) (= (not (= (_ bv11 4) (bvneg (_ bv5 4)))) false))))
(mp (asserted (not (= (_ bv11 4) (bvneg (_ bv5 4))))) @x49 false))))))
-6cad4ca9b92628993328e0c9cd5982fe4690567b 7 0
-unsat
-((set-logic <null>)
-(proof
-(let ((@x35 (monotonicity (rewrite (= (= (_ bv11 4) (_ bv11 4)) true)) (= (not (= (_ bv11 4) (_ bv11 4))) (not true)))))
-(let ((@x39 (trans @x35 (rewrite (= (not true) false)) (= (not (= (_ bv11 4) (_ bv11 4))) false))))
-(mp (asserted (not (= (_ bv11 4) (_ bv11 4)))) @x39 false)))))
-
55b7bec34258b475381a754439390616488c924c 7 0
unsat
((set-logic <null>)
@@ -533,7 +151,7 @@
(let ((@x47 (trans (monotonicity @x40 (= (not (= (bvnot (_ bv240 16)) (_ bv65295 16))) (not true))) (rewrite (= (not true) false)) (= (not (= (bvnot (_ bv240 16)) (_ bv65295 16))) false))))
(mp (asserted (not (= (bvnot (_ bv240 16)) (_ bv65295 16)))) @x47 false))))))
-f40271ef9e5c8b600036568090a9c30a30fba3c1 9 0
+88af7aeb0e9a24cb60cf70ebed32fe4a6b94a809 9 0
unsat
((set-logic <null>)
(proof
@@ -553,15 +171,6 @@
(let ((@x48 (trans @x44 (rewrite (= (not true) false)) (= (not (= (concat (_ bv3 4) (_ bv15 6)) (_ bv207 10))) false))))
(mp (asserted (not (= (concat (_ bv3 4) (_ bv15 6)) (_ bv207 10)))) @x48 false)))))))
-f5796d75c7b1d8ea9a2c70c40ab57315660fbcf3 8 0
-unsat
-((set-logic <null>)
-(proof
-(let ((@x36 (monotonicity (rewrite (= ((_ extract 2 1) (_ bv6 4)) (_ bv3 2))) (= (= ((_ extract 2 1) (_ bv6 4)) (_ bv3 2)) (= (_ bv3 2) (_ bv3 2))))))
-(let ((@x40 (trans @x36 (rewrite (= (= (_ bv3 2) (_ bv3 2)) true)) (= (= ((_ extract 2 1) (_ bv6 4)) (_ bv3 2)) true))))
-(let ((@x47 (trans (monotonicity @x40 (= (not (= ((_ extract 2 1) (_ bv6 4)) (_ bv3 2))) (not true))) (rewrite (= (not true) false)) (= (not (= ((_ extract 2 1) (_ bv6 4)) (_ bv3 2))) false))))
-(mp (asserted (not (= ((_ extract 2 1) (_ bv6 4)) (_ bv3 2)))) @x47 false))))))
-
44630a6139544aa8cc936f2dcdd464d5967b2876 9 0
unsat
((set-logic <null>)
@@ -572,6 +181,15 @@
(let ((@x47 (trans @x43 (rewrite (= (not true) false)) (= (not (= ((_ zero_extend 6) (_ bv10 4)) (_ bv10 10))) false))))
(mp (asserted (not (= ((_ zero_extend 6) (_ bv10 4)) (_ bv10 10)))) @x47 false)))))))
+36033c98ec9d88c28e82a4d5b423281f56a42859 8 0
+unsat
+((set-logic <null>)
+(proof
+(let ((@x36 (monotonicity (rewrite (= ((_ extract 2 1) (_ bv6 4)) (_ bv3 2))) (= (= ((_ extract 2 1) (_ bv6 4)) (_ bv3 2)) (= (_ bv3 2) (_ bv3 2))))))
+(let ((@x40 (trans @x36 (rewrite (= (= (_ bv3 2) (_ bv3 2)) true)) (= (= ((_ extract 2 1) (_ bv6 4)) (_ bv3 2)) true))))
+(let ((@x47 (trans (monotonicity @x40 (= (not (= ((_ extract 2 1) (_ bv6 4)) (_ bv3 2))) (not true))) (rewrite (= (not true) false)) (= (not (= ((_ extract 2 1) (_ bv6 4)) (_ bv3 2))) false))))
+(mp (asserted (not (= ((_ extract 2 1) (_ bv6 4)) (_ bv3 2)))) @x47 false))))))
+
2b91c33c03a89b80ac6fb984f384bd9814c2b51d 9 0
unsat
((set-logic <null>)
@@ -602,6 +220,16 @@
(let ((@x48 (trans @x44 (rewrite (= (not true) false)) (= (not (= (bvlshr (_ bv25 8) (_ bv2 8)) (_ bv6 8))) false))))
(mp (asserted (not (= (bvlshr (_ bv25 8) (_ bv2 8)) (_ bv6 8)))) @x48 false)))))))
+d1e9761fb935892f82a21268d39aac76f75ee282 9 0
+unsat
+((set-logic <null>)
+(proof
+(let ((@x37 (monotonicity (rewrite (= (bvashr (_ bv19 8) (_ bv2 8)) (_ bv4 8))) (= (= (bvashr (_ bv19 8) (_ bv2 8)) (_ bv4 8)) (= (_ bv4 8) (_ bv4 8))))))
+(let ((@x41 (trans @x37 (rewrite (= (= (_ bv4 8) (_ bv4 8)) true)) (= (= (bvashr (_ bv19 8) (_ bv2 8)) (_ bv4 8)) true))))
+(let ((@x44 (monotonicity @x41 (= (not (= (bvashr (_ bv19 8) (_ bv2 8)) (_ bv4 8))) (not true)))))
+(let ((@x48 (trans @x44 (rewrite (= (not true) false)) (= (not (= (bvashr (_ bv19 8) (_ bv2 8)) (_ bv4 8))) false))))
+(mp (asserted (not (= (bvashr (_ bv19 8) (_ bv2 8)) (_ bv4 8)))) @x48 false)))))))
+
1b01af1c33961b4a329d46a526471313f71130ca 9 0
unsat
((set-logic <null>)
@@ -612,16 +240,6 @@
(let ((@x47 (trans @x43 (rewrite (= (not true) false)) (= (not (= ((_ rotate_right 2) (_ bv6 4)) (_ bv9 4))) false))))
(mp (asserted (not (= ((_ rotate_right 2) (_ bv6 4)) (_ bv9 4)))) @x47 false)))))))
-d1e9761fb935892f82a21268d39aac76f75ee282 9 0
-unsat
-((set-logic <null>)
-(proof
-(let ((@x37 (monotonicity (rewrite (= (bvashr (_ bv19 8) (_ bv2 8)) (_ bv4 8))) (= (= (bvashr (_ bv19 8) (_ bv2 8)) (_ bv4 8)) (= (_ bv4 8) (_ bv4 8))))))
-(let ((@x41 (trans @x37 (rewrite (= (= (_ bv4 8) (_ bv4 8)) true)) (= (= (bvashr (_ bv19 8) (_ bv2 8)) (_ bv4 8)) true))))
-(let ((@x44 (monotonicity @x41 (= (not (= (bvashr (_ bv19 8) (_ bv2 8)) (_ bv4 8))) (not true)))))
-(let ((@x48 (trans @x44 (rewrite (= (not true) false)) (= (not (= (bvashr (_ bv19 8) (_ bv2 8)) (_ bv4 8))) false))))
-(mp (asserted (not (= (bvashr (_ bv19 8) (_ bv2 8)) (_ bv4 8)))) @x48 false)))))))
-
a14e30a88e731b5e605d4726dbb1f583497ab894 9 0
unsat
((set-logic <null>)
--- a/src/HOL/Tools/ATP/atp_problem.ML Wed Dec 16 15:44:17 2020 +0100
+++ b/src/HOL/Tools/ATP/atp_problem.ML Wed Dec 16 15:47:33 2020 +0100
@@ -33,7 +33,7 @@
datatype fool = Without_FOOL | With_FOOL
datatype polymorphism = Monomorphic | Polymorphic
- datatype thf_flavor = THF_Lambda_Bool_Free | THF_Without_Choice | THF_With_Choice
+ datatype thf_flavor = THF_Lambda_Free | THF_Without_Choice | THF_With_Choice
datatype atp_format =
CNF |
@@ -97,6 +97,8 @@
val tptp_true : string
val tptp_lambda : string
val tptp_empty_list : string
+ val tptp_unary_builtins : string list
+ val tptp_binary_builtins : string list
val dfg_individual_type : string
val isabelle_info_prefix : string
val isabelle_info : bool -> string -> int -> (string, 'a) atp_term list
@@ -191,7 +193,7 @@
datatype fool = Without_FOOL | With_FOOL
datatype polymorphism = Monomorphic | Polymorphic
-datatype thf_flavor = THF_Lambda_Bool_Free | THF_Without_Choice | THF_With_Choice
+datatype thf_flavor = THF_Lambda_Free | THF_Without_Choice | THF_With_Choice
datatype atp_format =
CNF |
@@ -257,6 +259,10 @@
val tptp_lambda = "^"
val tptp_empty_list = "[]"
+val tptp_unary_builtins = [tptp_not]
+val tptp_binary_builtins =
+ [tptp_and, tptp_or, tptp_implies, tptp_if, tptp_iff, tptp_not_iff, tptp_equal]
+
val dfg_individual_type = "iii" (* cannot clash *)
val isabelle_info_prefix = "isabelle_"
@@ -455,7 +461,8 @@
else
"")
-fun tptp_string_of_term _ (ATerm ((s, []), [])) = s
+fun tptp_string_of_term _ (ATerm ((s, []), [])) =
+ s |> member (op =) (tptp_unary_builtins @ tptp_binary_builtins) s ? parens
| tptp_string_of_term format (ATerm ((s, tys), ts)) =
let
val of_type = string_of_type format
@@ -473,8 +480,8 @@
else if s = tptp_ho_forall orelse s = tptp_ho_exists then
(case ts of
[AAbs (((s', ty), tm), [])] =>
- (* Use syntactic sugar "!" and "?" instead of "!!" and "??" whenever
- possible, to work around LEO-II 1.2.8 parser limitation. *)
+ (* Use syntactic sugar "!" and "?" instead of "!!" and "??" whenever possible, to work
+ around LEO-II, Leo-III, and Satallax parser limitation. *)
tptp_string_of_formula format
(AQuant (if s = tptp_ho_forall then AForall else AExists,
[(s', SOME ty)], AAtom tm))
@@ -482,19 +489,18 @@
else if s = tptp_choice then
(case ts of
[AAbs (((s', ty), tm), args)] =>
- (* There is code in "ATP_Problem_Generate" to ensure that "Eps" is
- always applied to an abstraction. *)
+ (* There is code in "ATP_Problem_Generate" to ensure that "Eps" is always applied to an
+ abstraction. *)
tptp_string_of_app format
(tptp_choice ^ "[" ^ s' ^ " : " ^ of_type ty ^
"]: " ^ of_term tm ^ ""
|> parens) (map of_term args)
| _ => app ())
- else if s = tptp_not then
- (* agsyHOL doesn't like negations applied like this: "~ @ t". *)
- (case ts of [t] => s ^ " " ^ (of_term t |> parens) |> parens | _ => s)
- else if member (op =) [tptp_and, tptp_or, tptp_implies, tptp_if, tptp_iff,
- tptp_not_iff, tptp_equal] s then
- (* agsyHOL doesn't like connectives applied like this: "& @ t1 @ t2". *)
+ else if member (op =) tptp_unary_builtins s then
+ (* generate e.g. "~ t" instead of "~ @ t". *)
+ (case ts of [t] => s ^ " " ^ (of_term t |> parens) |> parens)
+ else if member (op =) tptp_binary_builtins s then
+ (* generate e.g. "t1 & t2" instead of "& @ t1 @ t2". *)
(case ts of
[t1, t2] => (of_term t1 |> parens) ^ " " ^ s ^ " " ^ (of_term t2 |> parens) |> parens
| _ => app ())
--- a/src/HOL/Tools/ATP/atp_problem_generate.ML Wed Dec 16 15:44:17 2020 +0100
+++ b/src/HOL/Tools/ATP/atp_problem_generate.ML Wed Dec 16 15:47:33 2020 +0100
@@ -2,6 +2,7 @@
Author: Fabian Immler, TU Muenchen
Author: Makarius
Author: Jasmin Blanchette, TU Muenchen
+ Author: Martin Desharnais, UniBw Muenchen
Translation of HOL to FOL for Metis and Sledgehammer.
*)
@@ -99,7 +100,7 @@
val is_type_enc_sound : type_enc -> bool
val type_enc_of_string : strictness -> string -> type_enc
val adjust_type_enc : atp_format -> type_enc -> type_enc
- val is_lambda_free : term -> bool
+ val is_first_order_lambda_free : term -> bool
val do_cheaply_conceal_lambdas : typ list -> term -> term
val mk_aconns :
atp_connective -> ('a, 'b, 'c, 'd) atp_formula list
@@ -162,7 +163,7 @@
fun is_type_enc_native (Native _) = true
| is_type_enc_native _ = false
-fun is_type_enc_full_higher_order (Native (Higher_Order THF_Lambda_Bool_Free, _, _, _)) = false
+fun is_type_enc_full_higher_order (Native (Higher_Order THF_Lambda_Free, _, _, _)) = false
| is_type_enc_full_higher_order (Native (Higher_Order _, _, _, _)) = true
| is_type_enc_full_higher_order _ = false
fun is_type_enc_fool (Native (_, With_FOOL, _, _)) = true
@@ -654,11 +655,11 @@
| (_, Undercover_Types) => raise Same.SAME
| (Mangled_Monomorphic, _) =>
if is_type_level_uniform level then
- Native (Higher_Order THF_With_Choice, Without_FOOL, Mangled_Monomorphic, level)
+ Native (Higher_Order THF_With_Choice, fool, Mangled_Monomorphic, level)
else
raise Same.SAME
| (poly as Raw_Polymorphic _, All_Types) =>
- Native (Higher_Order THF_With_Choice, Without_FOOL, poly, All_Types)
+ Native (Higher_Order THF_With_Choice, fool, poly, All_Types)
| _ => raise Same.SAME))
end
@@ -695,8 +696,8 @@
end
handle Same.SAME => error ("Unknown type encoding: " ^ quote s)
-fun min_hologic THF_Lambda_Bool_Free _ = THF_Lambda_Bool_Free
- | min_hologic _ THF_Lambda_Bool_Free = THF_Lambda_Bool_Free
+fun min_hologic THF_Lambda_Free _ = THF_Lambda_Free
+ | min_hologic _ THF_Lambda_Free = THF_Lambda_Free
| min_hologic THF_Without_Choice _ = THF_Without_Choice
| min_hologic _ THF_Without_Choice = THF_Without_Choice
| min_hologic _ _ = THF_With_Choice
@@ -728,42 +729,62 @@
(if is_type_enc_sound type_enc then Tags else Guards) stuff
| adjust_type_enc _ type_enc = type_enc
-fun is_lambda_free t =
+fun is_first_order_lambda_free t =
(case t of
- \<^const>\<open>Not\<close> $ t1 => is_lambda_free t1
- | Const (\<^const_name>\<open>All\<close>, _) $ Abs (_, _, t') => is_lambda_free t'
- | Const (\<^const_name>\<open>All\<close>, _) $ t1 => is_lambda_free t1
- | Const (\<^const_name>\<open>Ex\<close>, _) $ Abs (_, _, t') => is_lambda_free t'
- | Const (\<^const_name>\<open>Ex\<close>, _) $ t1 => is_lambda_free t1
- | \<^const>\<open>HOL.conj\<close> $ t1 $ t2 => is_lambda_free t1 andalso is_lambda_free t2
- | \<^const>\<open>HOL.disj\<close> $ t1 $ t2 => is_lambda_free t1 andalso is_lambda_free t2
- | \<^const>\<open>HOL.implies\<close> $ t1 $ t2 => is_lambda_free t1 andalso is_lambda_free t2
+ \<^const>\<open>Not\<close> $ t1 => is_first_order_lambda_free t1
+ | Const (\<^const_name>\<open>All\<close>, _) $ Abs (_, _, t') => is_first_order_lambda_free t'
+ | Const (\<^const_name>\<open>All\<close>, _) $ t1 => is_first_order_lambda_free t1
+ | Const (\<^const_name>\<open>Ex\<close>, _) $ Abs (_, _, t') => is_first_order_lambda_free t'
+ | Const (\<^const_name>\<open>Ex\<close>, _) $ t1 => is_first_order_lambda_free t1
+ | \<^const>\<open>HOL.conj\<close> $ t1 $ t2 => is_first_order_lambda_free t1 andalso is_first_order_lambda_free t2
+ | \<^const>\<open>HOL.disj\<close> $ t1 $ t2 => is_first_order_lambda_free t1 andalso is_first_order_lambda_free t2
+ | \<^const>\<open>HOL.implies\<close> $ t1 $ t2 =>
+ is_first_order_lambda_free t1 andalso is_first_order_lambda_free t2
| Const (\<^const_name>\<open>HOL.eq\<close>, Type (_, [\<^typ>\<open>bool\<close>, _])) $ t1 $ t2 =>
- is_lambda_free t1 andalso is_lambda_free t2
+ is_first_order_lambda_free t1 andalso is_first_order_lambda_free t2
| _ => not (exists_subterm (fn Abs _ => true | _ => false) t))
-fun simple_translate_lambdas do_lambdas ctxt t =
- if is_lambda_free t then
+fun simple_translate_lambdas do_lambdas ctxt type_enc t =
+ if is_first_order_lambda_free t then
t
else
let
- fun trans Ts t =
+ fun trans_first_order Ts t =
(case t of
- \<^const>\<open>Not\<close> $ t1 => \<^const>\<open>Not\<close> $ trans Ts t1
+ \<^const>\<open>Not\<close> $ t1 => \<^const>\<open>Not\<close> $ trans_first_order Ts t1
| (t0 as Const (\<^const_name>\<open>All\<close>, _)) $ Abs (s, T, t') =>
- t0 $ Abs (s, T, trans (T :: Ts) t')
- | (t0 as Const (\<^const_name>\<open>All\<close>, _)) $ t1 => trans Ts (t0 $ eta_expand Ts t1 1)
+ t0 $ Abs (s, T, trans_first_order (T :: Ts) t')
+ | (t0 as Const (\<^const_name>\<open>All\<close>, _)) $ t1 =>
+ trans_first_order Ts (t0 $ eta_expand Ts t1 1)
| (t0 as Const (\<^const_name>\<open>Ex\<close>, _)) $ Abs (s, T, t') =>
- t0 $ Abs (s, T, trans (T :: Ts) t')
- | (t0 as Const (\<^const_name>\<open>Ex\<close>, _)) $ t1 => trans Ts (t0 $ eta_expand Ts t1 1)
- | (t0 as \<^const>\<open>HOL.conj\<close>) $ t1 $ t2 => t0 $ trans Ts t1 $ trans Ts t2
- | (t0 as \<^const>\<open>HOL.disj\<close>) $ t1 $ t2 => t0 $ trans Ts t1 $ trans Ts t2
- | (t0 as \<^const>\<open>HOL.implies\<close>) $ t1 $ t2 => t0 $ trans Ts t1 $ trans Ts t2
+ t0 $ Abs (s, T, trans_first_order (T :: Ts) t')
+ | (t0 as Const (\<^const_name>\<open>Ex\<close>, _)) $ t1 =>
+ trans_first_order Ts (t0 $ eta_expand Ts t1 1)
+ | (t0 as \<^const>\<open>HOL.conj\<close>) $ t1 $ t2 =>
+ t0 $ trans_first_order Ts t1 $ trans_first_order Ts t2
+ | (t0 as \<^const>\<open>HOL.disj\<close>) $ t1 $ t2 =>
+ t0 $ trans_first_order Ts t1 $ trans_first_order Ts t2
+ | (t0 as \<^const>\<open>HOL.implies\<close>) $ t1 $ t2 =>
+ t0 $ trans_first_order Ts t1 $ trans_first_order Ts t2
| (t0 as Const (\<^const_name>\<open>HOL.eq\<close>, Type (_, [\<^typ>\<open>bool\<close>, _]))) $ t1 $ t2 =>
- t0 $ trans Ts t1 $ trans Ts t2
+ t0 $ trans_first_order Ts t1 $ trans_first_order Ts t2
| _ =>
if not (exists_subterm (fn Abs _ => true | _ => false) t) then t
else t |> Envir.eta_contract |> do_lambdas ctxt Ts)
+
+ fun trans_fool Ts t =
+ (case t of
+ (t0 as Const (\<^const_name>\<open>All\<close>, _)) $ Abs (s, T, t') =>
+ t0 $ Abs (s, T, trans_fool (T :: Ts) t')
+ | (t0 as Const (\<^const_name>\<open>All\<close>, _)) $ t1 => trans_fool Ts (t0 $ eta_expand Ts t1 1)
+ | (t0 as Const (\<^const_name>\<open>Ex\<close>, _)) $ Abs (s, T, t') =>
+ t0 $ Abs (s, T, trans_fool (T :: Ts) t')
+ | (t0 as Const (\<^const_name>\<open>Ex\<close>, _)) $ t1 => trans_fool Ts (t0 $ eta_expand Ts t1 1)
+ | t1 $ t2 => trans_fool Ts t1 $ trans_fool Ts t2
+ | Abs _ => t |> Envir.eta_contract |> do_lambdas ctxt Ts
+ | _ => t)
+
+ val trans = if is_type_enc_fool type_enc then trans_fool else trans_first_order
val (t, ctxt') = yield_singleton (Variable.import_terms true) t ctxt
in t |> trans [] |> singleton (Variable.export_terms ctxt' ctxt) end
@@ -809,18 +830,18 @@
Lambda_Lifting.is_quantifier
#> fst
-fun lift_lams_part_2 ctxt (facts, lifted) =
+fun lift_lams_part_2 ctxt type_enc (facts, lifted) =
(facts, lifted)
(* Lambda-lifting sometimes leaves some lambdas around; we need some way to
get rid of them *)
- |> apply2 (map (introduce_combinators ctxt))
+ |> apply2 (map (introduce_combinators ctxt type_enc))
|> apply2 (map constify_lifted)
(* Requires bound variables not to clash with any schematic variables (as
should be the case right after lambda-lifting). *)
|>> map (hol_open_form (unprefix hol_close_form_prefix))
||> map (hol_open_form I)
-fun lift_lams ctxt = lift_lams_part_2 ctxt oo lift_lams_part_1 ctxt
+fun lift_lams ctxt type_enc = lift_lams_part_2 ctxt type_enc o lift_lams_part_1 ctxt type_enc
fun intentionalize_def (Const (\<^const_name>\<open>All\<close>, _) $ Abs (_, _, t)) =
intentionalize_def t
@@ -1103,67 +1124,121 @@
val unmangled_invert_const = invert_const o hd o unmangled_const_name
+fun vars_of_iterm vars (IConst ((s, _), _, _)) = insert (op =) s vars
+ | vars_of_iterm vars (IVar ((s, _), _)) = insert (op =) s vars
+ | vars_of_iterm vars (IApp (tm1, tm2)) = union (op =) (vars_of_iterm vars tm1) (vars_of_iterm vars tm2)
+ | vars_of_iterm vars (IAbs (_, tm)) = vars_of_iterm vars tm
+
+fun generate_unique_name gen unique n =
+ let val x = gen n in
+ if unique x then x else generate_unique_name gen unique (n + 1)
+ end
+
+fun eta_expand_quantifier_body (tm as IAbs _) = tm
+ | eta_expand_quantifier_body tm =
+ let
+ (* We accumulate all variables because E 2.5 does not support variable shadowing. *)
+ val vars = vars_of_iterm [] tm
+ val x = generate_unique_name
+ (fn n => "X" ^ (if n = 0 then "" else string_of_int n))
+ (fn name => not (exists (equal name) vars)) 0
+ val T = domain_type (ityp_of tm)
+ in
+ IAbs ((`I x, T), IApp (tm, IConst (`I x, T, [])))
+ end
+
fun introduce_proxies_in_iterm type_enc =
let
- fun tweak_ho_quant ho_quant T [IAbs _] = IConst (`I ho_quant, T, [])
- | tweak_ho_quant ho_quant (T as Type (_, [p_T as Type (_, [x_T, _]), _])) _ =
- (* Eta-expand "!!" and "??", to work around LEO-II 1.2.8 parser
- limitation. This works in conjuction with special code in
- "ATP_Problem" that uses the syntactic sugar "!" and "?" whenever
- possible. *)
+ fun tweak_ho_quant ho_quant (T as Type (_, [p_T as Type (_, [x_T, _]), _])) [] =
+ (* Eta-expand "!!" and "??", to work around LEO-II, Leo-III, and Satallax parser
+ limitations. This works in conjunction with special code in "ATP_Problem" that uses the
+ syntactic sugar "!" and "?" whenever possible. *)
IAbs ((`I "P", p_T),
IApp (IConst (`I ho_quant, T, []),
IAbs ((`I "X", x_T),
IApp (IConst (`I "P", p_T, []),
IConst (`I "X", x_T, [])))))
- | tweak_ho_quant _ _ _ = raise Fail "unexpected type for quantifier"
+ | tweak_ho_quant ho_quant T _ = IConst (`I ho_quant, T, [])
+ fun tweak_ho_equal T argc =
+ if argc = 2 then
+ IConst (`I tptp_equal, T, [])
+ else
+ (* Eta-expand partially applied THF equality, because the LEO-II and Satallax parsers
+ complain about not being able to infer the type of "=". *)
+ let val i_T = domain_type T in
+ IAbs ((`I "Y", i_T),
+ IAbs ((`I "Z", i_T),
+ IApp (IApp (IConst (`I tptp_equal, T, []),
+ IConst (`I "Y", i_T, [])),
+ IConst (`I "Z", i_T, []))))
+ end
fun intro top_level args (IApp (tm1, tm2)) =
- IApp (intro top_level (tm2 :: args) tm1, intro false [] tm2)
+ let
+ val tm1' = intro top_level (tm2 :: args) tm1
+ val tm2' = intro false [] tm2
+ val tm2'' =
+ (case tm1' of
+ IConst ((s, _), _, _) =>
+ if s = tptp_ho_forall orelse s = tptp_ho_exists then
+ eta_expand_quantifier_body tm2'
+ else
+ tm2'
+ | _ => tm2')
+ in
+ IApp (tm1', tm2'')
+ end
| intro top_level args (IConst (name as (s, _), T, T_args)) =
(case proxify_const s of
SOME proxy_base =>
let
val argc = length args
- val plain_const = IConst (name, T, [])
+ fun plain_const () = IConst (name, T, [])
fun proxy_const () = IConst (proxy_base |>> prefix const_prefix, T, T_args)
- val is_fool = is_type_enc_fool type_enc
- fun if_card_matches card x = if not is_fool orelse card = argc then x else plain_const
+ fun handle_fool card x = if card = argc then x else proxy_const ()
in
- if top_level orelse is_fool orelse is_type_enc_full_higher_order type_enc then
- (case (top_level, s) of
- (_, "c_False") => IConst (`I tptp_false, T, [])
- | (_, "c_True") => IConst (`I tptp_true, T, [])
- | (false, "c_Not") => if_card_matches 1 (IConst (`I tptp_not, T, []))
- | (false, "c_conj") => if_card_matches 2 (IConst (`I tptp_and, T, []))
- | (false, "c_disj") => if_card_matches 2 (IConst (`I tptp_or, T, []))
- | (false, "c_implies") => if_card_matches 2 (IConst (`I tptp_implies, T, []))
- | (false, "c_All") => if_card_matches 1 (tweak_ho_quant tptp_ho_forall T args)
- | (false, "c_Ex") => if_card_matches 1 (tweak_ho_quant tptp_ho_exists T args)
- | (false, s) =>
+ if top_level then
+ (case s of
+ "c_False" => IConst (`I tptp_false, T, [])
+ | "c_True" => IConst (`I tptp_true, T, [])
+ | _ => plain_const ())
+ else if is_type_enc_full_higher_order type_enc then
+ (case s of
+ "c_False" => IConst (`I tptp_false, T, [])
+ | "c_True" => IConst (`I tptp_true, T, [])
+ | "c_Not" => IConst (`I tptp_not, T, [])
+ | "c_conj" => IConst (`I tptp_and, T, [])
+ | "c_disj" => IConst (`I tptp_or, T, [])
+ | "c_implies" => IConst (`I tptp_implies, T, [])
+ | "c_All" => tweak_ho_quant tptp_ho_forall T args
+ | "c_Ex" => tweak_ho_quant tptp_ho_exists T args
+ | s =>
if is_tptp_equal s then
- if argc = 2 then
- IConst (`I tptp_equal, T, [])
- else if is_fool then
- proxy_const ()
- else
- (* Eta-expand partially applied THF equality, because the
- LEO-II and Satallax parsers complain about not being able to
- infer the type of "=". *)
- let val i_T = domain_type T in
- IAbs ((`I "Y", i_T),
- IAbs ((`I "Z", i_T),
- IApp (IApp (IConst (`I tptp_equal, T, []),
- IConst (`I "Y", i_T, [])),
- IConst (`I "Z", i_T, []))))
- end
+ tweak_ho_equal T argc
else
- plain_const
- | _ => plain_const)
+ plain_const ())
+ else if is_type_enc_fool type_enc then
+ (case s of
+ "c_False" => IConst (`I tptp_false, T, [])
+ | "c_True" => IConst (`I tptp_true, T, [])
+ | "c_Not" => handle_fool 1 (IConst (`I tptp_not, T, []))
+ | "c_conj" => handle_fool 2 (IConst (`I tptp_and, T, []))
+ | "c_disj" => handle_fool 2 (IConst (`I tptp_or, T, []))
+ | "c_implies" => handle_fool 2 (IConst (`I tptp_implies, T, []))
+ | "c_All" => handle_fool 1 (tweak_ho_quant tptp_ho_forall T args)
+ | "c_Ex" => handle_fool 1 (tweak_ho_quant tptp_ho_exists T args)
+ | s =>
+ if is_tptp_equal s then
+ handle_fool 2 (IConst (`I tptp_equal, T, []))
+ else
+ plain_const ())
else
- IConst (proxy_base |>> prefix const_prefix, T, T_args)
+ proxy_const ()
end
- | NONE => if s = tptp_choice then tweak_ho_quant tptp_choice T args
- else IConst (name, T, T_args))
+ | NONE =>
+ if s = tptp_choice then
+ tweak_ho_quant tptp_choice T args
+ else
+ IConst (name, T, T_args))
| intro _ _ (IAbs (bound, tm)) = IAbs (bound, intro false [] tm)
| intro _ _ tm = tm
in intro true [] end
@@ -1423,20 +1498,20 @@
(** predicators and application operators **)
-type sym_info =
- {pred_sym : bool, min_ary : int, max_ary : int, types : typ list,
- in_conj : bool}
+type sym_info = {pred_sym : bool, min_ary : int, max_ary : int, types : typ list, in_conj : bool}
fun default_sym_tab_entries type_enc =
- (make_fixed_const NONE \<^const_name>\<open>undefined\<close>,
- {pred_sym = false, min_ary = 0, max_ary = 0, types = [], in_conj = false}) ::
- ([tptp_false, tptp_true]
- |> map (rpair {pred_sym = true, min_ary = 0, max_ary = 0, types = [], in_conj = false})) @
- ([tptp_equal, tptp_old_equal]
- |> map (rpair {pred_sym = true, min_ary = 2, max_ary = 2, types = [], in_conj = false}))
- |> not (is_type_enc_fool type_enc orelse is_type_enc_full_higher_order type_enc)
- ? cons (prefixed_predicator_name,
- {pred_sym = true, min_ary = 1, max_ary = 1, types = [], in_conj = false})
+ let
+ fun mk_sym_info pred n =
+ {pred_sym = pred, min_ary = n, max_ary = n, types = [], in_conj = false}
+ in
+ (make_fixed_const NONE \<^const_name>\<open>undefined\<close>, mk_sym_info false 0) ::
+ (map (rpair (mk_sym_info true 0)) [tptp_false, tptp_true]) @
+ (map (rpair (mk_sym_info true 1)) tptp_unary_builtins) @
+ (map (rpair (mk_sym_info true 2)) (tptp_old_equal :: tptp_binary_builtins))
+ |> not (is_type_enc_fool type_enc orelse is_type_enc_full_higher_order type_enc)
+ ? cons (prefixed_predicator_name, mk_sym_info true 1)
+ end
datatype app_op_level =
Min_App_Op |
@@ -1833,17 +1908,17 @@
else if lam_trans = liftingN orelse lam_trans = lam_liftingN then
lift_lams ctxt type_enc
else if lam_trans = combsN then
- map (introduce_combinators ctxt) #> rpair []
+ map (introduce_combinators ctxt type_enc) #> rpair []
else if lam_trans = combs_and_liftingN then
lift_lams_part_1 ctxt type_enc
- ##> maps (fn t => [t, introduce_combinators ctxt (intentionalize_def t)])
- #> lift_lams_part_2 ctxt
+ ##> maps (fn t => [t, introduce_combinators ctxt type_enc (intentionalize_def t)])
+ #> lift_lams_part_2 ctxt type_enc
else if lam_trans = combs_or_liftingN then
lift_lams_part_1 ctxt type_enc
##> map (fn t => (case head_of (strip_qnt_body \<^const_name>\<open>All\<close> t) of
\<^term>\<open>(=) ::bool => bool => bool\<close> => t
- | _ => introduce_combinators ctxt (intentionalize_def t)))
- #> lift_lams_part_2 ctxt
+ | _ => introduce_combinators ctxt type_enc (intentionalize_def t)))
+ #> lift_lams_part_2 ctxt type_enc
else if lam_trans = keep_lamsN then
map (Envir.eta_contract) #> rpair []
else
--- a/src/HOL/Tools/SMT/smt_config.ML Wed Dec 16 15:44:17 2020 +0100
+++ b/src/HOL/Tools/SMT/smt_config.ML Wed Dec 16 15:47:33 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 Wed Dec 16 15:44:17 2020 +0100
+++ b/src/HOL/Tools/SMT/verit_proof.ML Wed Dec 16 15:47:33 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 Wed Dec 16 15:44:17 2020 +0100
+++ b/src/HOL/Tools/SMT/verit_replay_methods.ML Wed Dec 16 15:47:33 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
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_atp_systems.ML Wed Dec 16 15:44:17 2020 +0100
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_atp_systems.ML Wed Dec 16 15:47:33 2020 +0100
@@ -296,7 +296,7 @@
val modern = string_ord (getenv "E_VERSION", "2.3") <> LESS
val (format, enc) =
if modern then
- (THF (With_FOOL, Monomorphic, THF_Lambda_Bool_Free), "mono_native_higher")
+ (THF (With_FOOL, Monomorphic, THF_Lambda_Free), "mono_native_higher_fool")
else
(TFF (Without_FOOL, Monomorphic), "mono_native")
in