blob: d732b9ff08291eb0e611d7dbe7ad59ea200f307d (
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
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
|
; COMMAND-LINE: --bitblast=eager
; EXPECT: unsat
(set-logic QF_BV)
(set-info :status unsat)
(define-fun hamming-weight ((bv (_ BitVec 4))) (_ BitVec 4)
(bvadd
(bvadd
(bvadd ((_ zero_extend 3) ((_ extract 0 0) bv))
((_ zero_extend 3) ((_ extract 1 1) bv)))
((_ zero_extend 3) ((_ extract 2 2) bv)))
((_ zero_extend 3) ((_ extract 3 3) bv))))
(define-fun left-hamming-weight ((index (_ BitVec 4)) (bv (_ BitVec 4)))
(_ BitVec 4)
(hamming-weight (bvand bv (bvnot (bvsub (bvshl index (_ bv1 4)) (_ bv1 4))))))
(define-fun right-hamming-weight ((index (_ BitVec 4)) (bv (_ BitVec 4)))
(_ BitVec 4) (hamming-weight (bvand bv (bvsub index (_ bv1 4)))))
(define-fun bit-1 ((bv (_ BitVec 4))) (_ BitVec 4) (bvand bv (bvneg bv)))
(define-fun bit-2 ((bv (_ BitVec 4))) (_ BitVec 4)
(bit-1 (bvand bv (bvsub bv (_ bv1 4)))))
(define-fun bit-3 ((bv (_ BitVec 4))) (_ BitVec 4)
(bit-2 (bvand bv (bvsub bv (_ bv1 4)))))
(define-fun bit-4 ((bv (_ BitVec 4))) (_ BitVec 4)
(bit-3 (bvand bv (bvsub bv (_ bv1 4)))))
(define-fun bit-5 ((bv (_ BitVec 4))) (_ BitVec 4)
(bit-4 (bvand bv (bvsub bv (_ bv1 4)))))
(define-fun index-bit ((index (_ BitVec 4)) (bv (_ BitVec 4))) (_ BitVec 4)
(ite (= index (_ bv0 4)) (bit-1 bv)
(ite (= index (_ bv1 4)) (bit-2 bv)
(ite (= index (_ bv2 4)) (bit-3 bv) (bit-4 bv)))))
(define-fun permute
((index (_ BitVec 4)) (obj-0 (_ BitVec 4)) (obj-1 (_ BitVec 4))
(obj-2 (_ BitVec 4)) (obj-3 (_ BitVec 4)))
(_ BitVec 4)
(let ((my-index-bit (bvshl (_ bv1 4) index)))
(ite (= my-index-bit obj-0) (_ bv0 4)
(ite (= my-index-bit obj-1) (_ bv1 4)
(ite (= my-index-bit obj-2) (_ bv2 4) (_ bv3 4))))))
(define-fun left-zeros ((index (_ BitVec 4))) (_ BitVec 8)
(ite (bvugt index (_ bv2 4)) (ite (bvugt index (_ bv4 4)) (_ bv0 8) (_ bv1 8))
(ite (bvugt index (_ bv1 4)) (_ bv2 8) (_ bv3 8))))
(define-fun centered ((index (_ BitVec 4)) (bv (_ BitVec 4))) (_ BitVec 8)
(bvshl ((_ zero_extend 4) bv) (left-zeros index)))
(declare-const v0 (_ BitVec 4))
(assert (= (_ bv4 4) (hamming-weight v0)))
(declare-const v1 (_ BitVec 4))
(assert (= (_ bv4 4) (hamming-weight v1)))
(declare-const vp1-0 (_ BitVec 4))
(assert
(or (= (_ bv1 4) vp1-0) (= (_ bv2 4) vp1-0) (= (_ bv4 4) vp1-0)
(= (_ bv8 4) vp1-0)))
(declare-const vp1-1 (_ BitVec 4))
(assert
(or (= (_ bv1 4) vp1-1) (= (_ bv2 4) vp1-1) (= (_ bv4 4) vp1-1)
(= (_ bv8 4) vp1-1)))
(declare-const vp1-2 (_ BitVec 4))
(assert
(or (= (_ bv1 4) vp1-2) (= (_ bv2 4) vp1-2) (= (_ bv4 4) vp1-2)
(= (_ bv8 4) vp1-2)))
(declare-const vp1-3 (_ BitVec 4))
(assert
(or (= (_ bv1 4) vp1-3) (= (_ bv2 4) vp1-3) (= (_ bv4 4) vp1-3)
(= (_ bv8 4) vp1-3)))
(assert (= (_ bv15 4) (bvor vp1-0 (bvor vp1-1 (bvor vp1-2 vp1-3)))))
(assert
(and
(= (_ bv0 8)
(bvxor
(bvand
(centered (index-bit (permute (_ bv0 4) vp1-0 vp1-1 vp1-2 vp1-3) v1) v1)
(centered (index-bit (_ bv0 4) v0) v0))
(_ bv8 8)))
(= (_ bv0 8)
(bvxor
(bvand
(centered (index-bit (permute (_ bv1 4) vp1-0 vp1-1 vp1-2 vp1-3) v1) v1)
(centered (index-bit (_ bv1 4) v0) v0))
(_ bv8 8)))
(= (_ bv0 8)
(bvxor
(bvand
(centered (index-bit (permute (_ bv2 4) vp1-0 vp1-1 vp1-2 vp1-3) v1) v1)
(centered (index-bit (_ bv2 4) v0) v0))
(_ bv8 8)))
(= (_ bv0 8)
(bvxor
(bvand
(centered (index-bit (permute (_ bv3 4) vp1-0 vp1-1 vp1-2 vp1-3) v1) v1)
(centered (index-bit (_ bv3 4) v0) v0))
(_ bv8 8)))))
(check-sat)
|
