blob: 02cadaeab43b79cf42a52dfef0890db37935e8ed (
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
|
; a = b ^ a = 00000 ^ b = 11111 is UNSAT
(check
(% a var_bv
(% b var_bv
(% f1 (th_holds (= BitVec (a_var_bv a) (a_var_bv b)))
(% f2 (th_holds (= BitVec (a_var_bv a) (a_bv (bvc b0 (bvc b0 (bvc b0 (bvc b0 (bvc b0 bvn))))))))
(% f3 (th_holds (= BitVec (a_var_bv b) (a_bv (bvc b1 (bvc b1 (bvc b1 (bvc b1 (bvc b1 bvn))))))))
(: (holds cln)
(decl_bv_atom_var 5 a (\ ba1
(decl_bv_atom_var 5 b (\ ba2
(decl_bv_atom_const _ (bvc b0 (bvc b0 (bvc b0 (bvc b0 (bvc b0 bvn))))) (\ c (\ ba3
(decl_bv_atom_const _ (bvc b1 (bvc b1 (bvc b1 (bvc b1 (bvc b1 bvn))))) (\ d (\ ba4
(decl_atom (bblast a 4) (\ v1 (\ a1
(decl_atom (bblast b 4) (\ v2 (\ a2
; bitblasting terms
(th_let_pf _ (bv_bbl_var _ _ _ ba1) (\ bt1
(th_let_pf _ (bv_bbl_var _ _ _ ba2) (\ bt2
(th_let_pf _ (bv_bbl_const _ _ _ _ ba3) (\ bt3
(th_let_pf _ (bv_bbl_const _ _ _ _ ba4) (\ bt4
; bitblasting formulas
(th_let_pf _ (bv_bbl_eq _ _ _ _ _ bt1 bt2) (\ bf1
(th_let_pf _ (bv_bbl_eq _ _ _ _ _ bt1 bt3) (\ 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
(contra _ (impl_elim _ _ l2 (iff_elim_2 _ _ (and_elim_1 _ _ (impl_elim _ _ f1 bf1)))) l1) ; notice at the intermost we impl_elim, which converts from atom to bit-blasting representation
))))) (\ C2
; ~a.4
(satlem _ _
(ast _ _ _ a1 (\ l1
(clausify_false
(impl_elim _ _ l1 (iff_elim_1 _ _ (and_elim_1 _ _ (impl_elim _ _ f2 bf2))))
))) (\ C3
; b.4
(satlem _ _
(asf _ _ _ a2 (\ l2
(clausify_false
(contra _ (impl_elim _ _ truth (iff_elim_2 _ _ (and_elim_1 _ _ (impl_elim _ _ f3 bf3)))) l2)
))) (\ C6
(satlem_simplify _ _ _
(R _ _ (R _ _ C6 C2 v2) C3 v1) (\ x x))
)))))))))))))))))))))))))))))))))))))))))))
|
