diff options
Diffstat (limited to 'proofs/signatures/sat.plf')
-rwxr-xr-x | proofs/signatures/sat.plf | 254 |
1 files changed, 127 insertions, 127 deletions
diff --git a/proofs/signatures/sat.plf b/proofs/signatures/sat.plf index 09255f612..5e2f1cc44 100755 --- a/proofs/signatures/sat.plf +++ b/proofs/signatures/sat.plf @@ -1,127 +1,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 (! 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))))))
\ No newline at end of file +(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)))))) |