--- a/src/HOL/Library/Tools/smt_word.ML Tue Dec 15 17:22:27 2020 +0000
+++ b/src/HOL/Library/Tools/smt_word.ML Tue Dec 15 17:22:40 2020 +0000
@@ -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 Tue Dec 15 17:22:27 2020 +0000
+++ b/src/HOL/SMT_Examples/SMT_Examples_Verit.thy Tue Dec 15 17:22:40 2020 +0000
@@ -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 Tue Dec 15 17:22:27 2020 +0000
+++ b/src/HOL/SMT_Examples/SMT_Word_Examples.certs Tue Dec 15 17:22:40 2020 +0000
@@ -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/SMT/smt_config.ML Tue Dec 15 17:22:27 2020 +0000
+++ b/src/HOL/Tools/SMT/smt_config.ML Tue Dec 15 17:22:40 2020 +0000
@@ -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 Tue Dec 15 17:22:27 2020 +0000
+++ b/src/HOL/Tools/SMT/verit_proof.ML Tue Dec 15 17:22:40 2020 +0000
@@ -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 Tue Dec 15 17:22:27 2020 +0000
+++ b/src/HOL/Tools/SMT/verit_replay_methods.ML Tue Dec 15 17:22:40 2020 +0000
@@ -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