From ff7d33c2f75668fde0f149943e3cf1bedad1102f Mon Sep 17 00:00:00 2001 From: Morgan Deters Date: Mon, 5 Aug 2013 18:29:34 -0400 Subject: Proof-checking code; fixups of segfaults and missing functionality in proof generation; fix bug 285. * segfaults/assert-fails in proof-generation fixed, including bug 285 * added --check-proofs to automatically check proofs, like --check-models (but only for UF/SAT at present) * proof generation now works in portfolio (but *not* --check-proofs, since LFSC code uses globals) * proofs are *not* yet supported in incremental mode * added --dump-proofs to dump out proofs, like --dump-models * run_regression script now runs with --check-proofs where appropriate * options scripts now support :link-smt for SMT options, like :link for command-line --- proofs/signatures/sat.plf | 254 +++++++++++++++++++++++----------------------- 1 file changed, 127 insertions(+), 127 deletions(-) (limited to 'proofs/signatures/sat.plf') 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)))))) -- cgit v1.2.3