blob: b95caa8fd8d9ade4d540139dfa9e15d82d9855a5 (
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
|
(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))
(declare clause type)
(declare cln clause)
(declare clc (! x lit (! c clause clause)))
; 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 append ((c1 clause) (c2 clause)) clause
(match c1 (cln c2) ((clc l c1') (clc l (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) (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))))))
; 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))))))
|
