blob: 00487a1832e20a77139bef1ec86453bc4ca5f881 (
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
|
(set-logic QF_UF)
(set-info :status sat)
(declare-sort var 0)
(declare-sort reg 0)
(declare-fun a1_1 () var)
(declare-fun a2_1 () var)
(declare-fun c_3 () var)
(declare-fun c_4 () var)
(declare-fun b_3 () var)
(declare-fun r0 () reg)
(declare-fun r1 () reg)
(declare-fun r2 () reg)
(declare-fun r3 () reg)
(declare-fun r4 () reg)
(declare-fun r6 () reg)
(assert (not (= r0 r1)))
(assert (not (= r0 r2)))
(assert (not (= r0 r3)))
(assert (not (= r0 r4)))
(assert (not (= r0 r6)))
(assert (not (= r1 r2)))
(assert (not (= r1 r3)))
(assert (not (= r1 r4)))
(assert (not (= r1 r6)))
(assert (not (= r2 r3)))
(assert (not (= r2 r4)))
(assert (not (= r2 r6)))
(assert (not (= r3 r4)))
(assert (not (= r3 r6)))
(assert (not (= r4 r6)))
(declare-fun assign (var) reg)
(assert (or (= (assign a1_1) r0) (= (assign a1_1) r1) (= (assign a1_1) r2) (= (assign a1_1) r3) (= (assign a1_1) r4) (= (assign a1_1) r6) ))
(assert (or (= (assign a2_1) r0) (= (assign a2_1) r1) (= (assign a2_1) r2) (= (assign a2_1) r3) (= (assign a2_1) r4) (= (assign a2_1) r6) ))
(assert (or (= (assign c_3) r0) (= (assign c_3) r1) (= (assign c_3) r2) (= (assign c_3) r3) (= (assign c_3) r4) (= (assign c_3) r6) ))
(assert (or (= (assign c_4) r0) (= (assign c_4) r1) (= (assign c_4) r2) (= (assign c_4) r3) (= (assign c_4) r4) (= (assign c_4) r6) ))
(assert (or (= (assign b_3) r0) (= (assign b_3) r1) (= (assign b_3) r2) (= (assign b_3) r3) (= (assign b_3) r4) (= (assign b_3) r6) ))
(assert (not (= (assign a1_1) (assign c_4))))
(assert (not (= (assign a2_1) (assign c_3))))
(assert (not (= (assign a2_1) (assign b_3))))
(assert (not (= (assign c_3) (assign b_3))))
(assert (not (= (assign c_4) (assign b_3))))
(assert (= (assign a1_1) r0))
(assert (= (assign a2_1) r2))
(assert (= (assign c_3) r1))
(assert (= (assign c_4) r1))
(assert (= (assign b_3) r0))
(check-sat)
(exit)
|
