blob: 574191493d9d5addc91c7ac9c8a628625ea65a5d (
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
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
142
143
144
145
146
147
148
149
150
151
152
153
154
155
156
157
158
159
160
161
162
163
164
165
166
167
168
169
170
171
172
173
|
(declare bool type)
(declare tt bool)
(declare ff bool)
(declare var type)
(declare lit type)
(declare pos (! x var lit))
(declare neg (! x var lit))
; Flip the polarity of the literal
(program lit_flip ((l lit)) lit
(match l
((pos v) (neg v))
((neg v) (pos v))))
(declare clause type)
(declare cln clause)
(declare clc (! x lit (! c clause clause)))
; A list of clauses, CNF if interpretted as a formula,
; but also sometimes just a list
(declare cnf type)
(declare cnfn cnf)
(declare cnfc (! h clause (! t cnf cnf)))
; constructs for general clauses for R, Q, satlem
(declare concat_cl (! c1 clause (! c2 clause clause)))
(declare clr (! l lit (! c clause clause)))
; code to check resolutions
(program clause_append ((c1 clause) (c2 clause)) clause
(match c1 (cln c2) ((clc l c1') (clc l (clause_append c1' c2)))))
; we use marks as follows:
; -- mark 1 to record if we are supposed to remove a positive occurrence of the variable.
; -- mark 2 to record if we are supposed to remove a negative occurrence of the variable.
; -- mark 3 if we did indeed remove the variable positively
; -- mark 4 if we did indeed remove the variable negatively
(program simplify_clause ((c clause)) clause
(match c
(cln cln)
((clc l c1)
(match l
; Set mark 1 on v if it is not set, to indicate we should remove it.
; After processing the rest of the clause, set mark 3 if we were already
; supposed to remove v (so if mark 1 was set when we began). Clear mark3
; if we were not supposed to be removing v when we began this call.
((pos v)
(let m (ifmarked v tt (do (markvar v) ff))
(let c' (simplify_clause c1)
(match m
(tt (do (ifmarked3 v v (markvar3 v)) c'))
(ff (do (ifmarked3 v (markvar3 v) v) (markvar v) (clc l c')))))))
; the same as the code for tt, but using different marks.
((neg v)
(let m (ifmarked2 v tt (do (markvar2 v) ff))
(let c' (simplify_clause c1)
(match m
(tt (do (ifmarked4 v v (markvar4 v)) c'))
(ff (do (ifmarked4 v (markvar4 v) v) (markvar2 v) (clc l c')))))))))
((concat_cl c1 c2) (clause_append (simplify_clause c1) (simplify_clause c2)))
((clr l c1)
(match l
; set mark 1 to indicate we should remove v, and fail if
; mark 3 is not set after processing the rest of the clause
; (we will set mark 3 if we remove a positive occurrence of v).
((pos v)
(let m (ifmarked v tt (do (markvar v) ff))
(let m3 (ifmarked3 v (do (markvar3 v) tt) ff)
(let c' (simplify_clause c1)
(ifmarked3 v (do (match m3 (tt v) (ff (markvar3 v)))
(match m (tt v) (ff (markvar v))) c')
(fail clause))))))
; same as the tt case, but with different marks.
((neg v)
(let m2 (ifmarked2 v tt (do (markvar2 v) ff))
(let m4 (ifmarked4 v (do (markvar4 v) tt) ff)
(let c' (simplify_clause c1)
(ifmarked4 v (do (match m4 (tt v) (ff (markvar4 v)))
(match m2 (tt v) (ff (markvar2 v))) c')
(fail clause))))))
))))
; resolution proofs
(declare holds (! c clause type))
(declare R (! c1 clause (! c2 clause
(! u1 (holds c1)
(! u2 (holds c2)
(! n var
(holds (concat_cl (clr (pos n) c1)
(clr (neg n) c2)))))))))
(declare Q (! c1 clause (! c2 clause
(! u1 (holds c1)
(! u2 (holds c2)
(! n var
(holds (concat_cl (clr (neg n) c1)
(clr (pos n) c2)))))))))
(declare satlem_simplify
(! c1 clause
(! c2 clause
(! c3 clause
(! u1 (holds c1)
(! r (^ (simplify_clause c1) c2)
(! u2 (! x (holds c2) (holds c3))
(holds c3))))))))
(declare satlem
(! c clause
(! c2 clause
(! u (holds c)
(! u2 (! v (holds c) (holds c2))
(holds c2))))))
; Returns a copy of `c` with any duplicate literals removed.
; Never fails.
; Uses marks 3 & 4. Expects them to be clear before hand, and leaves them clear
; afterwards.
(program clause_dedup ((c clause)) clause
(match c
(cln cln)
((clc l rest)
(match l
((pos v) (ifmarked3
v
(clause_dedup rest)
(do (markvar3 v)
(let result (clc (pos v) (clause_dedup rest))
(do (markvar3 v) result)))))
((neg v) (ifmarked4
v
(clause_dedup rest)
(do (markvar4 v)
(let result (clc (neg v) (clause_dedup rest))
(do (markvar4 v) result)))))))))
(declare cnf_holds (! c cnf type))
(declare cnfn_proof (cnf_holds cnfn))
(declare cnfc_proof
(! c clause
(! deduped_c clause
(! rest cnf
(! proof_c (holds c)
(! proof_rest (cnf_holds rest)
(! sc (^ (clause_dedup c) deduped_c)
(cnf_holds (cnfc c rest)))))))))
; A little example to demonstrate simplify_clause.
; It can handle nested clr's of both polarities,
; and correctly cleans up marks when it leaves a
; clr or clc scope. Uncomment and run with
; --show-runs to see it in action.
;
; (check
; (% v1 var
; (% u1 (holds (concat_cl (clr (neg v1) (clr (pos v1) (clc (pos v1) (clr (pos v1) (clc (pos v1) (clc (neg v1) cln))))))
; (clc (pos v1) (clc (pos v1) cln))))
; (satlem _ _ _ u1 (\ x x))))))
;(check
; (% v1 var
; (% u1 (holds (clr (neg v1) (concat_cl (clc (neg v1) cln)
; (clr (neg v1) (clc (neg v1) cln)))))
; (satlem _ _ _ u1 (\ x x))))))
|
