blob: 58494e7930e556ce9975c1975c68a96ad988fe08 (
plain)
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
|
; (a = b) ^ (a = b & 00000) ^ (b = 11111) is UNSAT
(check
(% a var_bv
(% b var_bv
(% f1 (th_holds (= (BitVec 4) (a_var_bv _ a) (a_var_bv _ b)))
(% f2 (th_holds (= (BitVec 4) (a_var_bv _ a) (bvand 4 (a_var_bv 4 b) (a_bv _ (bvc b0 (bvc b0 (bvc b0 (bvc b0 (bvc b0 bvn)))))))))
(% f3 (th_holds (= (BitVec 4) (a_var_bv _ b) (a_bv _ (bvc b1 (bvc b1 (bvc b1 (bvc b1 (bvc b1 bvn))))))))
(: (holds cln)
;; (decl_bv_term_var 5 a (\ ba1
;; (decl_bv_term_var 5 b (\ ba2
;; (decl_bv_term_const _ (bvc b0 (bvc b0 (bvc b0 (bvc b0 (bvc b0 bvn))))) (\ c (\ ba3
;; (decl_bv_term_const _ (bvc b1 (bvc b1 (bvc b1 (bvc b1 (bvc b1 bvn))))) (\ d (\ ba4
(decl_atom (bitof a 4) (\ v1 (\ a1
(decl_atom (bitof b 4) (\ v2 (\ a2
; bitblasting terms
(decl_bblast _ _ _ (bv_bbl_var 4 a _ ) (\ bt1
(decl_bblast _ _ _ (bv_bbl_var 4 b _ ) (\ bt2
(decl_bblast _ _ _ (bv_bbl_const 4 _ (bvc b0 (bvc b0 (bvc b0 (bvc b0 bvn))))) (\ bt3
(decl_bblast _ _ _ (bv_bbl_const 4 _ (bvc b1 (bvc b1 (bvc b1 (bvc b1 bvn))))) (\ bt4
(decl_bblast _ _ _ (bv_bbl_bvand 4 _ _ _ _ _ bt1 bt3) (\ bt5
; bitblasting formulas
(th_let_pf _ (bv_bbl_eq _ _ _ _ _ _ bt1 bt2) (\ bf1
(th_let_pf _ (bv_bbl_bvult _ _ _ _ _ _ bt1 bt5) (\ bf2
(th_let_pf _ (bv_bbl_eq _ _ _ _ _ _ bt2 bt4) (\ bf3
; CNFication
; a.4 V ~b.4
(satlem _ _
(asf _ _ _ a1 (\ l1
(ast _ _ _ a2 (\ l2
(clausify_false
trust
))))) (\ C2
; ~a.4
(satlem _ _
(ast _ _ _ a1 (\ l1
(clausify_false
trust
))) (\ C3
; b.4
(satlem _ _
(asf _ _ _ a2 (\ l2
(clausify_false
trust
))) (\ C6
(satlem_simplify _ _ _
(R _ _ (R _ _ C6 C2 v2) C3 v1) (\ x x))
)))))))))))))))))))))))))))))))))))))))))))))
|
