diff options
| author | Andrew Reynolds <andrew.j.reynolds@gmail.com> | 2013-10-03 09:52:24 -0500 |
|---|---|---|
| committer | Tianyi Liang <tianyi-liang@uiowa.edu> | 2013-10-03 10:55:14 -0500 |
| commit | 38503bde0d58e80bd6c39152fb7d2f226d8ac3c9 (patch) | |
| tree | 75e0bc7ebf8d7da29d04ca9f36ebb130bf5bec45 /proofs/signatures/sat.plf | |
| parent | b663c658c80cee918afe37222e62dd1e5db33f5c (diff) | |
Adding example proof signatures for LFSC.
Diffstat (limited to 'proofs/signatures/sat.plf')
| -rwxr-xr-x | proofs/signatures/sat.plf | 127 |
1 files changed, 127 insertions, 0 deletions
diff --git a/proofs/signatures/sat.plf b/proofs/signatures/sat.plf new file mode 100755 index 000000000..09255f612 --- /dev/null +++ b/proofs/signatures/sat.plf @@ -0,0 +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 |