127 lines
4.6 KiB
Plaintext
127 lines
4.6 KiB
Plaintext
(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 (! 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 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 (clr (pos n) c1)
|
|
(clr (neg n) c2)))))))))
|
|
|
|
(declare Q (! c1 clause (! c2 clause
|
|
(! u1 (holds c1)
|
|
(! u2 (holds c2)
|
|
(! n var
|
|
(holds (concat (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 (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 (clc (neg v1) cln)
|
|
; (clr (neg v1) (clc (neg v1) cln)))))
|
|
; (satlem _ _ _ u1 (\ x x)))))) |