-
Notifications
You must be signed in to change notification settings - Fork 1
/
rosette_unsat_core.z3
96 lines (96 loc) · 2.61 KB
/
rosette_unsat_core.z3
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
92
93
94
95
96
(set-option :produce-unsat-cores true)
(declare-const x Bool)
(declare-const y Bool)
(declare-const a Bool)
(declare-const b Bool)
(declare-const c Bool)
(declare-const d Bool)
(assert (and (= a false) (= b true) (= c true) (= d true)))
(assert (= x (xor (= a b) (= c d))))
;;;;;;;;;;;;;;;;;;
(declare-const p0 Bool)
(assert (! (= p0 (not a)):named a0))
(declare-const p1 Bool)
(assert (! (= p1 (not b)):named a1))
(declare-const p2 Bool)
(assert (! (= p2 (and p0 p1)):named a2))
;;
(declare-const p3 Bool)
(assert (! (= p3 (or a b)):named a3))
(declare-const p4 Bool)
(assert (! (= p4 (not p3)):named a4))
;;
(declare-const p13 Bool)
(assert (! (= p13 (and p2 p4)) :named a13))
(declare-const p14 Bool)
(assert (! (= p14 (not p13)) :named a14))
;;;;
(declare-const p5 Bool)
(assert (! (= p5 (and c d)):named a5))
(declare-const p6 Bool)
(assert (! (= p6 (not p5)):named a6))
;;
(declare-const p7 Bool)
(assert (! (= p7 (not c)):named a7))
(declare-const p8 Bool)
(assert (! (= p8 (not d)):named a8))
(declare-const p9 Bool)
(assert (! (= p9 (and p7 p8)):named a9))
;;;;
(declare-const p10 Bool)
(assert (! (= p10 (and p9 p6)) :named a10))
(declare-const p11 Bool)
(assert (! (= p11 (not p10)) :named a11))
;;;;;
(declare-const p12 Bool)
(assert (! (= p12 (and p14 p11)) :named a12))
(declare-const p15 Bool)
(assert (! (= p15 (not p12)):named a15))
;;;;;;;;;;;;;;
(declare-const q0 Bool)
(assert (! (= q0 (not a)) :named b0))
(declare-const q1 Bool)
(assert (! (= q1 (not b)) :named b1))
(declare-const q2 Bool)
(assert (! (= q2 (and q0 q1)) :named b2))
(declare-const q2n Bool)
(assert (! (= q2n (not q2)) :named b21))
;;
(declare-const q3 Bool)
(assert (! (= q3 (and a b)) :named b3))
(declare-const q4 Bool)
(assert (! (= q4 (not q3)) :named b4))
;;
(declare-const q13 Bool)
(assert (! (= q13 (and q2 q4)) :named b13))
;;;;
(declare-const q5 Bool)
(assert (! (= q5 (and c d)):named b5))
(declare-const q6 Bool)
(assert (! (= q6 (not q5)):named b6))
;;
(declare-const q7 Bool)
(assert (! (= q7 (not c)):named b7))
(declare-const q8 Bool)
(assert (! (= q8 (not d)):named b8))
(declare-const q9 Bool)
(assert (! (= q9 (and q7 q8)):named b9))
(declare-const q10 Bool)
(assert (! (= q10 (not q9)):named b10))
;;;;
(declare-const q11 Bool)
(assert (! (= q11 (and q9 q6)):named b11))
;;;;;;
(declare-const q12 Bool)
(assert (! (= q12 (and q13 q11)):named b12))
(declare-const q14 Bool)
(assert (! (= q14 (not q12)) :named b14))
;;;;;;;;;;;;;;;;;;
(declare-const pq Bool)
(assert (! (= pq (and p15 q14)) :named ab))
(assert (= y pq))
(assert (! (= x y) :named eq))
(check-sat)
(get-unsat-core)
;(get-model)
; unsat (ab eq a15 a12 a14 a11 a13 a10 a2 a4 a3 a9 a6 a5 a0 a1 a7 a8)