~/talks/sat-proof-checking-talk$ acl2h Welcome to Clozure Common Lisp Version 1.7-dev-r14706M-trunk (DarwinX8664)! ; Aside: *hons-init-hook*: Setting *print-pretty* to t. ; Aside: (setq acl2::*hons-verbose* nil) to suppress asides. ; Aside: *hons-init-hook*: Setting *print-right-margin* to 80. ; Aside: *hons-init-hook*: Setting *save-source-locations* to t. ; Aside: *hons-init-hook*: Setting *record-source-file* to t. ACL2 Version 4.2 built April 12, 2011 15:40:54. Copyright (C) 2011 University of Texas at Austin ACL2 comes with ABSOLUTELY NO WARRANTY. This is free software and you are welcome to redistribute it under certain conditions. For details, see the GNU General Public License. WARNING: Do not redistribute. This is NOT an ACL2 release; it is, rather, an svn distribution, $Revision: 303 $. The authors of ACL2 consider svn distributions to be experimental. Initialized with (INITIALIZE-ACL2 'INCLUDE-BOOK *ACL2-PASS-2-FILES*). Experimental modification for HONS, memoization, and applicative hash tables. See the documentation topic note-4-2 for recent changes. Note: We have modified the prompt in some underlying Lisps to further distinguish it from the ACL2 prompt. ACL2 Version 4.2. Level 1. Cbd "/Users/kaufmann/talks/sat-proof-checking-talk/". Distributed books directory "/Users/kaufmann/fh/e/2011-04-11/e/acl2/books/". Type :help for help. Type (good-bye) to quit completely out of ACL2. ACL2 !>(make-fal '((a . 3) (b . 4)) nil) ACL2 Error in TOP-LEVEL: The symbol MAKE-FAL (in package "ACL2") has neither a function nor macro definition in ACL2. Please define it. Note: This error occurred in the context (MAKE-FAL '((A . 3) (B . 4)) NIL). ACL2 !>Bye. ~/talks/sat-proof-checking-talk$ acl2h Welcome to Clozure Common Lisp Version 1.7-dev-r14706M-trunk (DarwinX8664)! ; Aside: *hons-init-hook*: Setting *print-pretty* to t. ; Aside: (setq acl2::*hons-verbose* nil) to suppress asides. ; Aside: *hons-init-hook*: Setting *print-right-margin* to 80. ; Aside: *hons-init-hook*: Setting *save-source-locations* to t. ; Aside: *hons-init-hook*: Setting *record-source-file* to t. ACL2 Version 4.2 built April 12, 2011 15:40:54. Copyright (C) 2011 University of Texas at Austin ACL2 comes with ABSOLUTELY NO WARRANTY. This is free software and you are welcome to redistribute it under certain conditions. For details, see the GNU General Public License. WARNING: Do not redistribute. This is NOT an ACL2 release; it is, rather, an svn distribution, $Revision: 303 $. The authors of ACL2 consider svn distributions to be experimental. Initialized with (INITIALIZE-ACL2 'INCLUDE-BOOK *ACL2-PASS-2-FILES*). Experimental modification for HONS, memoization, and applicative hash tables. See the documentation topic note-4-2 for recent changes. Note: We have modified the prompt in some underlying Lisps to further distinguish it from the ACL2 prompt. Customizing with "/Users/kaufmann/acl2-customization.lisp". ACL2 Version 4.2. Level 1. Cbd "/Users/kaufmann/". Distributed books directory "/Users/kaufmann/fh/e/2011-04-11/e/acl2/books/". Type :help for help. Type (good-bye) to quit completely out of ACL2. ACL2 !> 55 ACL2 !> 68 ACL2 !>Bye. ACL2 Version 4.2. Level 1. Cbd "/Users/kaufmann/talks/sat-proof-checking-talk/". Distributed books directory "/Users/kaufmann/fh/e/2011-04-11/e/acl2/books/". Type :help for help. Type (good-bye) to quit completely out of ACL2. ACL2 !>(make-fal '((a . 3) (b . 4)) nil) ACL2 Error in TOP-LEVEL: The symbol MAKE-FAL (in package "ACL2") has neither a function nor macro definition in ACL2. Please define it. Note: This error occurred in the context (MAKE-FAL '((A . 3) (B . 4)) NIL). ACL2 !>(INCLUDE-BOOK "/Users/kaufmann/fh/e/2011-04-11/e/cbooks/g-logic/gl-extras") TTAG NOTE (for included book): Adding ttag INCLUDE-RAW from file /Users/kaufmann/fh/e/2011-04-11/e/acl2/books/tools/include-raw.lisp. ACL2 Warning [Ttags] in ( INCLUDE-BOOK "/Users/kaufmann/fh/e/2011-04-11/e/cbooks/g-logic/gl-extras" ...): The ttag note just printed to the terminal indicates a modification to ACL2. To avoid this warning, supply an explicit :TTAGS argument when including the book "/Users/kaufmann/fh/e/2011-04-11/e/cbooks/g-logic/gl-extras.lisp". TTAG NOTE (for included book): Adding ttag HONS-EXTRA from file /Users/kaufmann/fh/e/2011-04-11/e/cbooks/misc/hons-extra.lisp. ACL2 Warning [Ttags] in ( INCLUDE-BOOK "/Users/kaufmann/fh/e/2011-04-11/e/cbooks/g-logic/gl-extras" ...): The ttag note just printed to the terminal indicates a modification to ACL2. To avoid this warning, supply an explicit :TTAGS argument when including the book "/Users/kaufmann/fh/e/2011-04-11/e/cbooks/g-logic/gl-extras.lisp". TTAG NOTE (for included book): Adding ttag SNEAKY-LOAD from file /Users/kaufmann/fh/e/2011-04-11/e/cbooks/misc/sneaky-load.lisp. ACL2 Warning [Ttags] in ( INCLUDE-BOOK "/Users/kaufmann/fh/e/2011-04-11/e/cbooks/g-logic/gl-extras" ...): The ttag note just printed to the terminal indicates a modification to ACL2. To avoid this warning, supply an explicit :TTAGS argument when including the book "/Users/kaufmann/fh/e/2011-04-11/e/cbooks/g-logic/gl-extras.lisp". TTAG NOTE (for included book): Adding ttag AIG-VARS from file /Users/kaufmann/fh/e/2011-04-11/e/cbooks/aig/aig-vars-fast.lisp. ACL2 Warning [Ttags] in ( INCLUDE-BOOK "/Users/kaufmann/fh/e/2011-04-11/e/cbooks/g-logic/gl-extras" ...): The ttag note just printed to the terminal indicates a modification to ACL2. To avoid this warning, supply an explicit :TTAGS argument when including the book "/Users/kaufmann/fh/e/2011-04-11/e/cbooks/g-logic/gl-extras.lisp". TTAG NOTE (for included book): Adding ttag ZZ from file /Users/kaufmann/fh/e/2011-04-11/e/cbooks/aig/zz.lisp. ACL2 Warning [Ttags] in ( INCLUDE-BOOK "/Users/kaufmann/fh/e/2011-04-11/e/cbooks/g-logic/gl-extras" ...): The ttag note just printed to the terminal indicates a modification to ACL2. To avoid this warning, supply an explicit :TTAGS argument when including the book "/Users/kaufmann/fh/e/2011-04-11/e/cbooks/g-logic/gl-extras.lisp". TTAG NOTE (for included book): Adding ttag COUNT-BRANCHES-TO from file /Users/kaufmann/fh/e/2011-04-11/e/cbooks/aig/bddify.lisp. ACL2 Warning [Ttags] in ( INCLUDE-BOOK "/Users/kaufmann/fh/e/2011-04-11/e/cbooks/g-logic/gl-extras" ...): The ttag note just printed to the terminal indicates a modification to ACL2. To avoid this warning, supply an explicit :TTAGS argument when including the book "/Users/kaufmann/fh/e/2011-04-11/e/cbooks/g-logic/gl-extras.lisp". ;;; Starting full GC, 542,900,224 bytes allocated. ;;; Finished full GC. 171,256,048 bytes freed in 0.955224 s ;;; 78237 soft faults, 154541 faults, 2 pageins Loaded the GL library. For help, see :DOC GL. ; Memoize-fn: ** Warning: COUNT-BRANCHES-TO is currently memoized. ; So first we unmemoize it and then memoize it again. Summary Form: ( INCLUDE-BOOK "/Users/kaufmann/fh/e/2011-04-11/e/cbooks/g-logic/gl-extras" ...) Rules: NIL Warnings: Ttags Time: 3.70 seconds (prove: 0.00, print: 0.01, other: 3.70) "/Users/kaufmann/fh/e/2011-04-11/e/cbooks/g-logic/gl-extras.lisp" ACL2 !>(make-fal '((a . 3) (b . 4)) nil) ((A . 3) (B . 4)) ACL2 !>(make-fal '((a . 3) (b . 4)) 'my-name) ((A . 3) (B . 4) . MY-NAME) ACL2 !>:pe aig-and d 1:x(INCLUDE-BOOK "/Users/kaufmann/fh/e/2011-04-11/e/cbooks/g-logic/gl-extras") \ [Included books, outermost to innermost: "/Users/kaufmann/fh/e/2011-04-11/e/cbooks/g-logic/gl-extras.lisp" "/Users/kaufmann/fh/e/2011-04-11/e/cbooks/g-logic/gl.lisp" "/Users/kaufmann/fh/e/2011-04-11/e/cbooks/g-logic/g-ash.lisp" "/Users/kaufmann/fh/e/2011-04-11/e/cbooks/g-logic/g-if.lisp" "/Users/kaufmann/fh/e/2011-04-11/e/cbooks/g-logic/ite-merge.lisp" "/Users/kaufmann/fh/e/2011-04-11/e/cbooks/g-logic/general-objects.lisp" "/Users/kaufmann/fh/e/2011-04-11/e/cbooks/g-logic/gtypes.lisp" "/Users/kaufmann/fh/e/2011-04-11/e/cbooks/g-logic/gobjectp.lisp" "/Users/kaufmann/fh/e/2011-04-11/e/cbooks/g-logic/bfr.lisp" "/Users/kaufmann/fh/e/2011-04-11/e/cbooks/aig/witness.lisp" "/Users/kaufmann/fh/e/2011-04-11/e/cbooks/aig/base.lisp" ] \ >V d (DEFUN AIG-AND (X Y) (DECLARE (XARGS :GUARD T)) (COND ((OR (EQ X NIL) (EQ Y NIL)) NIL) ((EQ X T) Y) ((EQ Y T) X) ((HONS-EQUAL X Y) X) ((AND (CONSP Y) (EQ (CDR Y) NIL) (HONS-EQUAL (CAR Y) X)) NIL) ((AND (CONSP X) (EQ (CDR X) NIL) (HONS-EQUAL (CAR X) Y)) NIL) (T (HONS X Y)))) ACL2 !>(aig-and 'x nil) NIL ACL2 !>(aig-not (aig-not 'x)) X ACL2 !>(aig-or 'x (aig-or 'y 'x)) (((X) (Y) X)) ACL2 !>(aig-print '(((X) (Y) X))) (NOT (AND (NOT X) (NOT Y) (NOT X))) ACL2 !>(aig-and 'x (aig-and 'y 'x)) (X Y . X) ACL2 !>(aig-eval (aig-or (aig-and 'x 'y) (aig-not 'z)) (make-fal '((x . t) (y . nil) (z . t)) nil)) NIL ACL2 !>(aig-eval (aig-or (aig-and 'x 'y) (aig-not 'y)) (make-fal '((x . t) (y . nil) (z . t)) nil)) T ACL2 !>Bye. ~/talks/sat-proof-checking-talk$ stp Welcome to Clozure Common Lisp Version 1.7-dev-r14706M-trunk (DarwinX8664)! ; Aside: *hons-init-hook*: Setting *ofv-note-printed* to nil. ; Aside: *hons-init-hook*: Setting *print-pretty* to t. ; Aside: (setq acl2::*hons-verbose* nil) to suppress asides. ; Aside: *hons-init-hook*: Setting *print-right-margin* to 80. ACL2 Version 4.2 built April 12, 2011 15:40:54 then April 12, 2011 16:23:29. Copyright (C) 2011 University of Texas at Austin ACL2 comes with ABSOLUTELY NO WARRANTY. This is free software and you are welcome to redistribute it under certain conditions. For details, see the GNU General Public License. WARNING: Do not redistribute. This is NOT an ACL2 release; it is, rather, an svn distribution, $Revision: 303 $. The authors of ACL2 consider svn distributions to be experimental. Initialized with (INITIALIZE-ACL2 'INCLUDE-BOOK *ACL2-PASS-2-FILES*). Experimental modification for HONS, memoization, and applicative hash tables. See the documentation topic note-4-2 for recent changes. Note: We have modified the prompt in some underlying Lisps to further distinguish it from the ACL2 prompt. MODIFICATION NOTICE: STP extensions loaded Customizing with "/Users/kaufmann/acl2-customization.lisp". ACL2 Version 4.2. Level 1. Cbd "/Users/kaufmann/". Distributed books directory "/Users/kaufmann/fh/e/2011-04-11/e/acl2/books/". Type :help for help. Type (good-bye) to quit completely out of ACL2. ACL2 !> 55 ACL2 !> 68 ACL2 !>Bye. ACL2 Version 4.2. Level 1. Cbd "/Users/kaufmann/talks/sat-proof-checking-talk/". Distributed books directory "/Users/kaufmann/fh/e/2011-04-11/e/acl2/books/". Type :help for help. Type (good-bye) to quit completely out of ACL2. ACL2 !>(memoizedp 'aig-eval) ((:CONDITION-FN . AIG-EVAL-MEMOIZE-CONDITION) (:INLINE . T) (:TRACE) (:COMMUTATIVE) (:FORGET) (:MEMO-TABLE-INIT-SIZE . 60) (:AOKP)) ACL2 !>:pe aig-eval d -32 (INCLUDE-BOOK "aig/cnf" :DIR ...) \ [Included books, outermost to innermost: "/Users/kaufmann/fh/e/2011-04-11/e/cbooks/aig/cnf.lisp" "/Users/kaufmann/fh/e/2011-04-11/e/cbooks/aig/misc.lisp" "/Users/kaufmann/fh/e/2011-04-11/e/cbooks/aig/base.lisp" ] \ >V (DEFUN AIG-EVAL (X AL) (DECLARE (XARGS :GUARD T)) (AIG-CASES X :TRUE T :FALSE NIL :VAR (AND (AIG-ENV-LOOKUP X AL) T) :INV (NOT (AIG-EVAL (CAR X) AL)) :AND (AND (AIG-EVAL (CAR X) AL) (AIG-EVAL (CDR X) AL)))) ACL2 !>Bye. ~/talks/sat-proof-checking-talk$ acl2h Welcome to Clozure Common Lisp Version 1.7-dev-r14706M-trunk (DarwinX8664)! ; Aside: *hons-init-hook*: Setting *print-pretty* to t. ; Aside: (setq acl2::*hons-verbose* nil) to suppress asides. ; Aside: *hons-init-hook*: Setting *print-right-margin* to 80. ; Aside: *hons-init-hook*: Setting *save-source-locations* to t. ; Aside: *hons-init-hook*: Setting *record-source-file* to t. ACL2 Version 4.2 built April 12, 2011 15:40:54. Copyright (C) 2011 University of Texas at Austin ACL2 comes with ABSOLUTELY NO WARRANTY. This is free software and you are welcome to redistribute it under certain conditions. For details, see the GNU General Public License. WARNING: Do not redistribute. This is NOT an ACL2 release; it is, rather, an svn distribution, $Revision: 303 $. The authors of ACL2 consider svn distributions to be experimental. Initialized with (INITIALIZE-ACL2 'INCLUDE-BOOK *ACL2-PASS-2-FILES*). Experimental modification for HONS, memoization, and applicative hash tables. See the documentation topic note-4-2 for recent changes. Note: We have modified the prompt in some underlying Lisps to further distinguish it from the ACL2 prompt. Customizing with "/Users/kaufmann/acl2-customization.lisp". ACL2 Version 4.2. Level 1. Cbd "/Users/kaufmann/". Distributed books directory "/Users/kaufmann/fh/e/2011-04-11/e/acl2/books/". Type :help for help. Type (good-bye) to quit completely out of ACL2. ACL2 !> 55 ACL2 !> 68 ACL2 !>Bye. ACL2 Version 4.2. Level 1. Cbd "/Users/kaufmann/talks/sat-proof-checking-talk/". Distributed books directory "/Users/kaufmann/fh/e/2011-04-11/e/acl2/books/". Type :help for help. Type (good-bye) to quit completely out of ACL2. ACL2 !>(include-book "intro") Summary Form: ( INCLUDE-BOOK "intro" ...) Rules: NIL Time: 0.69 seconds (prove: 0.00, print: 0.00, other: 0.69) "/Users/kaufmann/talks/sat-proof-checking-talk/intro.lisp" ACL2 !>(mv-let (erp val) (zzchk-run-proof *proof* nil) (assert$ (null erp) val)) ((17 (((((((X) (Y) Z)) ((Z) (Y) X))) (((X) (Y) Z) (Z) (Y) X)))) (16 (((((((X) (Y) Z)) ((Z) (Y) X))) (((X) (Y) Z) (Z) (Y) X))) (((((X) (Y) Z)) ((Z) (Y) X)))) (15 (((((((X) (Y) Z)) ((Z) (Y) X))) (((X) (Y) Z) (Z) (Y) X))) ((((X) (Y) Z) (Z) (Y) X))) (14 ((Z) (Y) X) ((((X) (Y) Z)) ((Z) (Y) X))) (13 ((((X) (Y) Z)) ((Z) (Y) X)) ((X) (Y) Z) ((Z) (Y) X)) (12 (((X) (Y) Z)) (X)) (11 (((X) (Y) Z)) ((Y) Z)) (10 (((Y) Z)) (Y)) (9 (((Y) Z)) (Z)) (8 X Y ((Y) X)) (7 Z ((Z) (Y) X) (((Y) X))) (6 (Z) (((Z) (Y) X))) (5 (((Z) (Y) X)) ((Y) X)) (4 (((X) (Y) Z)) (((Z) (Y) X)) (((X) (Y) Z) (Z) (Y) X)) (3 (X) (((Y) X))) (2 (Y) (((Y) X))) (1 ((X) (Y) Z) X (((Y) Z))) (0 ((Y) Z) Y Z)) ACL2 !>(mv-let (erp val) (zzchk-run-proof *proof* nil) (assert$ (null erp) (let* ((last-step (car val)) (last-cl (cdr last-step))) (assert$ (eql (len last-cl) 1) (hons-equal (aig-norm *aig*) (aig-not (aig-norm (car last-cl)))))))) T ACL2 !>(include-book "print-proof") Summary Form: ( INCLUDE-BOOK "print-proof" ...) Rules: NIL Time: 0.00 seconds (prove: 0.00, print: 0.00, other: 0.00) "/Users/kaufmann/talks/sat-proof-checking-talk/print-proof.lisp" ACL2 !>(print-proof *proof*) ((0 ROOT ((AND (NOT Y) (NOT Z)) Y Z)) (1 ROOT ((AND (NOT X) (NOT Y) (NOT Z)) X (NOT (AND (NOT Y) (NOT Z))))) (2 ROOT ((NOT Y) (NOT (AND (NOT Y) (NOT X))))) (3 ROOT ((NOT X) (NOT (AND (NOT Y) (NOT X))))) (4 ROOT ((NOT (AND (NOT X) (NOT Y) (NOT Z))) (NOT (AND (NOT Z) (NOT Y) (NOT X))) (AND (NOT X) (NOT Y) (NOT Z) (NOT Z) (NOT Y) (NOT X)))) (5 ROOT ((NOT (AND (NOT Z) (NOT Y) (NOT X))) (AND (NOT Y) (NOT X)))) (6 ROOT ((NOT Z) (NOT (AND (NOT Z) (NOT Y) (NOT X))))) (7 ROOT (Z (AND (NOT Z) (NOT Y) (NOT X)) (NOT (AND (NOT Y) (NOT X))))) (8 ROOT (X Y (AND (NOT Y) (NOT X)))) (9 ROOT ((NOT (AND (NOT Y) (NOT Z))) (NOT Z))) (10 ROOT ((NOT (AND (NOT Y) (NOT Z))) (NOT Y))) (11 ROOT ((NOT (AND (NOT X) (NOT Y) (NOT Z))) (AND (NOT Y) (NOT Z)))) (12 ROOT ((NOT (AND (NOT X) (NOT Y) (NOT Z))) (NOT X))) (13 ROOT ((AND (NOT (AND (NOT X) (NOT Y) (NOT Z))) (NOT (AND (NOT Z) (NOT Y) (NOT X)))) (AND (NOT X) (NOT Y) (NOT Z)) (AND (NOT Z) (NOT Y) (NOT X)))) (14 CHAIN 7 ((8 (AND (NOT Y) (NOT X))) (9 (NOT Z)) (10 (NOT Y)) (11 (AND (NOT Y) (NOT Z))) (12 (NOT X)) (13 (AND (NOT X) (NOT Y) (NOT Z))))) (15 ROOT ((NOT (AND (NOT (AND (NOT (AND (NOT X) (NOT Y) (NOT Z))) (NOT (AND (NOT Z) (NOT Y) (NOT X))))) (NOT (AND (NOT X) (NOT Y) (NOT Z) (NOT Z) (NOT Y) (NOT X))))) (NOT (AND (NOT X) (NOT Y) (NOT Z) (NOT Z) (NOT Y) (NOT X))))) (16 ROOT ((NOT (AND (NOT (AND (NOT (AND (NOT X) (NOT Y) (NOT Z))) (NOT (AND (NOT Z) (NOT Y) (NOT X))))) (NOT (AND (NOT X) (NOT Y) (NOT Z) (NOT Z) (NOT Y) (NOT X))))) (NOT (AND (NOT (AND (NOT X) (NOT Y) (NOT Z))) (NOT (AND (NOT Z) (NOT Y) (NOT X))))))) (17 CHAIN 0 ((1 (NOT (AND (NOT Y) (NOT Z)))) (2 (NOT Y)) (3 (NOT X)) (4 (NOT (AND (NOT X) (NOT Y) (NOT Z)))) (5 (AND (NOT Y) (NOT X))) (6 (NOT Z)) (14 (AND (NOT Z) (NOT Y) (NOT X))) (15 (NOT (AND (NOT X) (NOT Y) (NOT Z) (NOT Z) (NOT Y) (NOT X)))) (16 (NOT (AND (NOT (AND (NOT X) (NOT Y) (NOT Z))) (NOT (AND (NOT Z) (NOT Y) (NOT X))))))))) ACL2 !>(print-proof *proof*) ((0 ROOT ((AND (NOT Y) (NOT Z)) Y Z)) (1 ROOT ((AND (NOT X) (NOT Y) (NOT Z)) X (NOT (AND (NOT Y) (NOT Z))))) (2 ROOT ((NOT Y) (NOT (AND (NOT Y) (NOT X))))) (3 ROOT ((NOT X) (NOT (AND (NOT Y) (NOT X))))) (4 ROOT ((NOT (AND (NOT X) (NOT Y) (NOT Z))) (NOT (AND (NOT Z) (NOT Y) (NOT X))) (AND (NOT X) (NOT Y) (NOT Z) (NOT Z) (NOT Y) (NOT X)))) (5 ROOT ((NOT (AND (NOT Z) (NOT Y) (NOT X))) (AND (NOT Y) (NOT X)))) (6 ROOT ((NOT Z) (NOT (AND (NOT Z) (NOT Y) (NOT X))))) (7 ROOT (Z (AND (NOT Z) (NOT Y) (NOT X)) (NOT (AND (NOT Y) (NOT X))))) (8 ROOT (X Y (AND (NOT Y) (NOT X)))) (9 ROOT ((NOT (AND (NOT Y) (NOT Z))) (NOT Z))) (10 ROOT ((NOT (AND (NOT Y) (NOT Z))) (NOT Y))) (11 ROOT ((NOT (AND (NOT X) (NOT Y) (NOT Z))) (AND (NOT Y) (NOT Z)))) (12 ROOT ((NOT (AND (NOT X) (NOT Y) (NOT Z))) (NOT X))) (13 ROOT ((AND (NOT (AND (NOT X) (NOT Y) (NOT Z))) (NOT (AND (NOT Z) (NOT Y) (NOT X)))) (AND (NOT X) (NOT Y) (NOT Z)) (AND (NOT Z) (NOT Y) (NOT X)))) (14 CHAIN 7 ((8 (AND (NOT Y) (NOT X))) (9 (NOT Z)) (10 (NOT Y)) (11 (AND (NOT Y) (NOT Z))) (12 (NOT X)) (13 (AND (NOT X) (NOT Y) (NOT Z))))) (15 ROOT ((NOT (AND (NOT (AND (NOT (AND (NOT X) (NOT Y) (NOT Z))) (NOT (AND (NOT Z) (NOT Y) (NOT X))))) (NOT (AND (NOT X) (NOT Y) (NOT Z) (NOT Z) (NOT Y) (NOT X))))) (NOT (AND (NOT X) (NOT Y) (NOT Z) (NOT Z) (NOT Y) (NOT X))))) (16 ROOT ((NOT (AND (NOT (AND (NOT (AND (NOT X) (NOT Y) (NOT Z))) (NOT (AND (NOT Z) (NOT Y) (NOT X))))) (NOT (AND (NOT X) (NOT Y) (NOT Z) (NOT Z) (NOT Y) (NOT X))))) (NOT (AND (NOT (AND (NOT X) (NOT Y) (NOT Z))) (NOT (AND (NOT Z) (NOT Y) (NOT X))))))) (17 CHAIN 0 ((1 (NOT (AND (NOT Y) (NOT Z)))) (2 (NOT Y)) (3 (NOT X)) (4 (NOT (AND (NOT X) (NOT Y) (NOT Z)))) (5 (AND (NOT Y) (NOT X))) (6 (NOT Z)) (14 (AND (NOT Z) (NOT Y) (NOT X))) (15 (NOT (AND (NOT X) (NOT Y) (NOT Z) (NOT Z) (NOT Y) (NOT X)))) (16 (NOT (AND (NOT (AND (NOT X) (NOT Y) (NOT Z))) (NOT (AND (NOT Z) (NOT Y) (NOT X))))))))) ACL2 !>*proof* ((0 ROOT ((Y) Z) Y Z) (1 ROOT ((X) (Y) Z) X (((Y) Z))) (2 ROOT (Y) (((Y) X))) (3 ROOT (X) (((Y) X))) (4 ROOT (((X) (Y) Z)) (((Z) (Y) X)) (((X) (Y) Z) (Z) (Y) X)) (5 ROOT (((Z) (Y) X)) ((Y) X)) (6 ROOT (Z) (((Z) (Y) X))) (7 ROOT Z ((Z) (Y) X) (((Y) X))) (8 ROOT X Y ((Y) X)) (9 ROOT (((Y) Z)) (Z)) (10 ROOT (((Y) Z)) (Y)) (11 ROOT (((X) (Y) Z)) ((Y) Z)) (12 ROOT (((X) (Y) Z)) (X)) (13 ROOT ((((X) (Y) Z)) ((Z) (Y) X)) ((X) (Y) Z) ((Z) (Y) X)) (14 CHAIN 7 (((Y) X) . 8) ((Z) . 9) ((Y) . 10) (((Y) Z) . 11) ((X) . 12) (((X) (Y) Z) . 13)) (15 ROOT (((((((X) (Y) Z)) ((Z) (Y) X))) (((X) (Y) Z) (Z) (Y) X))) ((((X) (Y) Z) (Z) (Y) X))) (16 ROOT (((((((X) (Y) Z)) ((Z) (Y) X))) (((X) (Y) Z) (Z) (Y) X))) (((((X) (Y) Z)) ((Z) (Y) X)))) (17 CHAIN 0 ((((Y) Z)) . 1) ((Y) . 2) ((X) . 3) ((((X) (Y) Z)) . 4) (((Y) X) . 5) ((Z) . 6) (((Z) (Y) X) . 14) (((((X) (Y) Z) (Z) (Y) X)) . 15) ((((((X) (Y) Z)) ((Z) (Y) X))) . 16))) ACL2 !>(print-proof *proof*) ((0 ROOT ((AND (NOT Y) (NOT Z)) Y Z)) (1 ROOT ((AND (NOT X) (NOT Y) (NOT Z)) X (NOT (AND (NOT Y) (NOT Z))))) (2 ROOT ((NOT Y) (NOT (AND (NOT Y) (NOT X))))) (3 ROOT ((NOT X) (NOT (AND (NOT Y) (NOT X))))) (4 ROOT ((NOT (AND (NOT X) (NOT Y) (NOT Z))) (NOT (AND (NOT Z) (NOT Y) (NOT X))) (AND (NOT X) (NOT Y) (NOT Z) (NOT Z) (NOT Y) (NOT X)))) (5 ROOT ((NOT (AND (NOT Z) (NOT Y) (NOT X))) (AND (NOT Y) (NOT X)))) (6 ROOT ((NOT Z) (NOT (AND (NOT Z) (NOT Y) (NOT X))))) (7 ROOT (Z (AND (NOT Z) (NOT Y) (NOT X)) (NOT (AND (NOT Y) (NOT X))))) (8 ROOT (X Y (AND (NOT Y) (NOT X)))) (9 ROOT ((NOT (AND (NOT Y) (NOT Z))) (NOT Z))) (10 ROOT ((NOT (AND (NOT Y) (NOT Z))) (NOT Y))) (11 ROOT ((NOT (AND (NOT X) (NOT Y) (NOT Z))) (AND (NOT Y) (NOT Z)))) (12 ROOT ((NOT (AND (NOT X) (NOT Y) (NOT Z))) (NOT X))) (13 ROOT ((AND (NOT (AND (NOT X) (NOT Y) (NOT Z))) (NOT (AND (NOT Z) (NOT Y) (NOT X)))) (AND (NOT X) (NOT Y) (NOT Z)) (AND (NOT Z) (NOT Y) (NOT X)))) (14 CHAIN 7 ((8 (AND (NOT Y) (NOT X))) (9 (NOT Z)) (10 (NOT Y)) (11 (AND (NOT Y) (NOT Z))) (12 (NOT X)) (13 (AND (NOT X) (NOT Y) (NOT Z))))) (15 ROOT ((NOT (AND (NOT (AND (NOT (AND (NOT X) (NOT Y) (NOT Z))) (NOT (AND (NOT Z) (NOT Y) (NOT X))))) (NOT (AND (NOT X) (NOT Y) (NOT Z) (NOT Z) (NOT Y) (NOT X))))) (NOT (AND (NOT X) (NOT Y) (NOT Z) (NOT Z) (NOT Y) (NOT X))))) (16 ROOT ((NOT (AND (NOT (AND (NOT (AND (NOT X) (NOT Y) (NOT Z))) (NOT (AND (NOT Z) (NOT Y) (NOT X))))) (NOT (AND (NOT X) (NOT Y) (NOT Z) (NOT Z) (NOT Y) (NOT X))))) (NOT (AND (NOT (AND (NOT X) (NOT Y) (NOT Z))) (NOT (AND (NOT Z) (NOT Y) (NOT X))))))) (17 CHAIN 0 ((1 (NOT (AND (NOT Y) (NOT Z)))) (2 (NOT Y)) (3 (NOT X)) (4 (NOT (AND (NOT X) (NOT Y) (NOT Z)))) (5 (AND (NOT Y) (NOT X))) (6 (NOT Z)) (14 (AND (NOT Z) (NOT Y) (NOT X))) (15 (NOT (AND (NOT X) (NOT Y) (NOT Z) (NOT Z) (NOT Y) (NOT X)))) (16 (NOT (AND (NOT (AND (NOT X) (NOT Y) (NOT Z))) (NOT (AND (NOT Z) (NOT Y) (NOT X))))))))) ACL2 !>(mv-let (erp val) (zzchk-run-proof *proof* nil) (assert$ (null erp) val)) ((17 (((((((X) (Y) Z)) ((Z) (Y) X))) (((X) (Y) Z) (Z) (Y) X)))) (16 (((((((X) (Y) Z)) ((Z) (Y) X))) (((X) (Y) Z) (Z) (Y) X))) (((((X) (Y) Z)) ((Z) (Y) X)))) (15 (((((((X) (Y) Z)) ((Z) (Y) X))) (((X) (Y) Z) (Z) (Y) X))) ((((X) (Y) Z) (Z) (Y) X))) (14 ((Z) (Y) X) ((((X) (Y) Z)) ((Z) (Y) X))) (13 ((((X) (Y) Z)) ((Z) (Y) X)) ((X) (Y) Z) ((Z) (Y) X)) (12 (((X) (Y) Z)) (X)) (11 (((X) (Y) Z)) ((Y) Z)) (10 (((Y) Z)) (Y)) (9 (((Y) Z)) (Z)) (8 X Y ((Y) X)) (7 Z ((Z) (Y) X) (((Y) X))) (6 (Z) (((Z) (Y) X))) (5 (((Z) (Y) X)) ((Y) X)) (4 (((X) (Y) Z)) (((Z) (Y) X)) (((X) (Y) Z) (Z) (Y) X)) (3 (X) (((Y) X))) (2 (Y) (((Y) X))) (1 ((X) (Y) Z) X (((Y) Z))) (0 ((Y) Z) Y Z)) ACL2 !>Bye. ~/talks/sat-proof-checking-talk$ acl2h Welcome to Clozure Common Lisp Version 1.7-dev-r14706M-trunk (DarwinX8664)! ; Aside: *hons-init-hook*: Setting *print-pretty* to t. ; Aside: (setq acl2::*hons-verbose* nil) to suppress asides. ; Aside: *hons-init-hook*: Setting *print-right-margin* to 80. ; Aside: *hons-init-hook*: Setting *save-source-locations* to t. ; Aside: *hons-init-hook*: Setting *record-source-file* to t. ACL2 Version 4.2 built April 12, 2011 15:40:54. Copyright (C) 2011 University of Texas at Austin ACL2 comes with ABSOLUTELY NO WARRANTY. This is free software and you are welcome to redistribute it under certain conditions. For details, see the GNU General Public License. WARNING: Do not redistribute. This is NOT an ACL2 release; it is, rather, an svn distribution, $Revision: 303 $. The authors of ACL2 consider svn distributions to be experimental. Initialized with (INITIALIZE-ACL2 'INCLUDE-BOOK *ACL2-PASS-2-FILES*). Experimental modification for HONS, memoization, and applicative hash tables. See the documentation topic note-4-2 for recent changes. Note: We have modified the prompt in some underlying Lisps to further distinguish it from the ACL2 prompt. Customizing with "/Users/kaufmann/acl2-customization.lisp". ACL2 Version 4.2. Level 1. Cbd "/Users/kaufmann/". Distributed books directory "/Users/kaufmann/fh/e/2011-04-11/e/acl2/books/". Type :help for help. Type (good-bye) to quit completely out of ACL2. ACL2 !> 55 ACL2 !> 68 ACL2 !>Bye. ACL2 Version 4.2. Level 1. Cbd "/Users/kaufmann/talks/sat-proof-checking-talk/". Distributed books directory "/Users/kaufmann/fh/e/2011-04-11/e/acl2/books/". Type :help for help. Type (good-bye) to quit completely out of ACL2. ACL2 !>(add-include-book-dir :cbooks "/Users/kaufmann/fh/e/current/e/cbooks") ((:CBOOKS . "/Users/kaufmann/fh/e/2011-04-11/e/cbooks/")) ACL2 !>(set-inhibit-warnings "theory") ; avoid some annoying warnings ("theory") ACL2 !>(include-book "aig/zz-check" :dir :cbooks) Summary Form: ( INCLUDE-BOOK "aig/zz-check" ...) Rules: NIL Time: 0.68 seconds (prove: 0.00, print: 0.00, other: 0.67) "/Users/kaufmann/fh/e/2011-04-11/e/cbooks/aig/zz-check.lisp" ACL2 !>(set-zzchk-debug-level 2) ; optional The guard proof obligation is (IMPLIES T T). Q.E.D. This concludes the guard proof. We now prove that the attachment satisfies the required constraint. The goal to prove is (NATP (ZZCHK-DEBUG-LEVEL-2)). Q.E.D. ACL2 Observation in ( DEFATTACH ZZCHK-DEBUG-LEVEL ZZCHK-DEBUG-LEVEL-2): The pre-existing attachment is being removed for function ZZCHK-DEBUG-LEVEL, before adding the requested attachment. Summary Form: ( DEFATTACH ZZCHK-DEBUG-LEVEL ZZCHK-DEBUG-LEVEL-2) Rules: ((:COMPOUND-RECOGNIZER NATP-COMPOUND-RECOGNIZER) (:TYPE-PRESCRIPTION ZZCHK-DEBUG-LEVEL-2)) Time: 0.00 seconds (prove: 0.00, print: 0.00, other: 0.00) :ATTACHMENTS-RECORDED ACL2 !>(defconst *aig* (aig-not (aig-iff (aig-or 'x (aig-or 'y 'z)) (aig-or 'z (aig-or 'y 'x))))) Summary Form: ( DEFCONST *AIG* ...) Rules: NIL Time: 0.00 seconds (prove: 0.00, print: 0.00, other: 0.00) *AIG* ACL2 !>(include-book "g-logic/gl-extras" :dir :cbooks) TTAG NOTE (for included book): Adding ttag INCLUDE-RAW from file /Users/kaufmann/fh/e/2011-04-11/e/acl2/books/tools/include-raw.lisp. ACL2 Warning [Ttags] in ( INCLUDE-BOOK "g-logic/gl-extras" ...): The ttag note just printed to the terminal indicates a modification to ACL2. To avoid this warning, supply an explicit :TTAGS argument when including the book "/Users/kaufmann/fh/e/2011-04-11/e/cbooks/g-logic/gl-extras.lisp". TTAG NOTE (for included book): Adding ttag HONS-EXTRA from file /Users/kaufmann/fh/e/2011-04-11/e/cbooks/misc/hons-extra.lisp. ACL2 Warning [Ttags] in ( INCLUDE-BOOK "g-logic/gl-extras" ...): The ttag note just printed to the terminal indicates a modification to ACL2. To avoid this warning, supply an explicit :TTAGS argument when including the book "/Users/kaufmann/fh/e/2011-04-11/e/cbooks/g-logic/gl-extras.lisp". TTAG NOTE (for included book): Adding ttag SNEAKY-LOAD from file /Users/kaufmann/fh/e/2011-04-11/e/cbooks/misc/sneaky-load.lisp. ACL2 Warning [Ttags] in ( INCLUDE-BOOK "g-logic/gl-extras" ...): The ttag note just printed to the terminal indicates a modification to ACL2. To avoid this warning, supply an explicit :TTAGS argument when including the book "/Users/kaufmann/fh/e/2011-04-11/e/cbooks/g-logic/gl-extras.lisp". TTAG NOTE (for included book): Adding ttag AIG-VARS from file /Users/kaufmann/fh/e/2011-04-11/e/cbooks/aig/aig-vars-fast.lisp. ACL2 Warning [Ttags] in ( INCLUDE-BOOK "g-logic/gl-extras" ...): The ttag note just printed to the terminal indicates a modification to ACL2. To avoid this warning, supply an explicit :TTAGS argument when including the book "/Users/kaufmann/fh/e/2011-04-11/e/cbooks/g-logic/gl-extras.lisp". TTAG NOTE (for included book): Adding ttag ZZ from file /Users/kaufmann/fh/e/2011-04-11/e/cbooks/aig/zz.lisp. ACL2 Warning [Ttags] in ( INCLUDE-BOOK "g-logic/gl-extras" ...): The ttag note just printed to the terminal indicates a modification to ACL2. To avoid this warning, supply an explicit :TTAGS argument when including the book "/Users/kaufmann/fh/e/2011-04-11/e/cbooks/g-logic/gl-extras.lisp". TTAG NOTE (for included book): Adding ttag COUNT-BRANCHES-TO from file /Users/kaufmann/fh/e/2011-04-11/e/cbooks/aig/bddify.lisp. ACL2 Warning [Ttags] in ( INCLUDE-BOOK "g-logic/gl-extras" ...): The ttag note just printed to the terminal indicates a modification to ACL2. To avoid this warning, supply an explicit :TTAGS argument when including the book "/Users/kaufmann/fh/e/2011-04-11/e/cbooks/g-logic/gl-extras.lisp". ;;; Starting full GC, 542,900,224 bytes allocated. ;;; Finished full GC. 170,615,088 bytes freed in 0.949131 s ;;; 77942 soft faults, 152767 faults, 0 pageins Loaded the GL library. For help, see :DOC GL. ; Memoize-fn: ** Warning: COUNT-BRANCHES-TO is currently memoized. ; So first we unmemoize it and then memoize it again. Summary Form: ( INCLUDE-BOOK "g-logic/gl-extras" ...) Rules: NIL Warnings: Ttags Time: 2.07 seconds (prove: 0.00, print: 0.01, other: 2.06) "/Users/kaufmann/fh/e/2011-04-11/e/cbooks/g-logic/gl-extras.lisp" ACL2 !>state ACL2 !>(assign zz-proof-alist 'zz-proof-alist) ; turn on proof generation ZZ-PROOF-ALIST ACL2 !>(zz-sat *aig*) ; Call external solver, ZZ (more below) Note: Starting C proof extraction.... Note: Completed C proof extraction. Note: Generating Lisp-level proof.... Note: Generated Lisp-level proof of length 18: 16 root clauses, 2 chain steps, and 17 total resolutions to perform. (UNSAT) ACL2 !>(cdr (hons-get *aig* (@ zz-proof-alist))) ((0 ROOT ((Y) Z) Y Z) (1 ROOT ((X) (Y) Z) X (((Y) Z))) (2 ROOT (Y) (((Y) X))) (3 ROOT (X) (((Y) X))) (4 ROOT (((X) (Y) Z)) (((Z) (Y) X)) (((X) (Y) Z) (Z) (Y) X)) (5 ROOT (((Z) (Y) X)) ((Y) X)) (6 ROOT (Z) (((Z) (Y) X))) (7 ROOT Z ((Z) (Y) X) (((Y) X))) (8 ROOT X Y ((Y) X)) (9 ROOT (((Y) Z)) (Z)) (10 ROOT (((Y) Z)) (Y)) (11 ROOT (((X) (Y) Z)) ((Y) Z)) (12 ROOT (((X) (Y) Z)) (X)) (13 ROOT ((((X) (Y) Z)) ((Z) (Y) X)) ((X) (Y) Z) ((Z) (Y) X)) (14 CHAIN 7 (((Y) X) . 8) ((Z) . 9) ((Y) . 10) (((Y) Z) . 11) ((X) . 12) (((X) (Y) Z) . 13)) (15 ROOT (((((((X) (Y) Z)) ((Z) (Y) X))) (((X) (Y) Z) (Z) (Y) X))) ((((X) (Y) Z) (Z) (Y) X))) (16 ROOT (((((((X) (Y) Z)) ((Z) (Y) X))) (((X) (Y) Z) (Z) (Y) X))) (((((X) (Y) Z)) ((Z) (Y) X)))) (17 CHAIN 0 ((((Y) Z)) . 1) ((Y) . 2) ((X) . 3) ((((X) (Y) Z)) . 4) (((Y) X) . 5) ((Z) . 6) (((Z) (Y) X) . 14) (((((X) (Y) Z) (Z) (Y) X)) . 15) ((((((X) (Y) Z)) ((Z) (Y) X))) . 16))) ACL2 !>(defconst *proof* '((0 ROOT ((Y) Z) Y Z) (1 ROOT ((X) (Y) Z) X (((Y) Z))) (2 ROOT (Y) (((Y) X))) (3 ROOT (X) (((Y) X))) (4 ROOT (((X) (Y) Z)) (((Z) (Y) X)) (((X) (Y) Z) (Z) (Y) X)) (5 ROOT (((Z) (Y) X)) ((Y) X)) (6 ROOT (Z) (((Z) (Y) X))) (7 ROOT Z ((Z) (Y) X) (((Y) X))) (8 ROOT X Y ((Y) X)) (9 ROOT (((Y) Z)) (Z)) (10 ROOT (((Y) Z)) (Y)) (11 ROOT (((X) (Y) Z)) ((Y) Z)) (12 ROOT (((X) (Y) Z)) (X)) (13 ROOT ((((X) (Y) Z)) ((Z) (Y) X)) ((X) (Y) Z) ((Z) (Y) X)) (14 CHAIN 7 (((Y) X) . 8) ((Z) . 9) ((Y) . 10) (((Y) Z) . 11) ((X) . 12) (((X) (Y) Z) . 13)) (15 ROOT (((((((X) (Y) Z)) ((Z) (Y) X))) (((X) (Y) Z) (Z) (Y) X))) ((((X) (Y) Z) (Z) (Y) X))) (16 ROOT (((((((X) (Y) Z)) ((Z) (Y) X))) (((X) (Y) Z) (Z) (Y) X))) (((((X) (Y) Z)) ((Z) (Y) X)))) (17 CHAIN 0 ((((Y) Z)) . 1) ((Y) . 2) ((X) . 3) ((((X) (Y) Z)) . 4) (((Y) X) . 5) ((Z) . 6) (((Z) (Y) X) . 14) (((((X) (Y) Z) (Z) (Y) X)) . 15) ((((((X) (Y) Z)) ((Z) (Y) X))) . 16)))) Summary Form: ( DEFCONST *PROOF* ...) Rules: NIL Time: 0.00 seconds (prove: 0.00, print: 0.00, other: 0.00) *PROOF* ACL2 !>(defthm aig-is-unsat (not (aig-eval *aig* env)) :hints (("Goal" :use ((:instance zzchk-check-correct (aig *aig*) (proof *proof*))) :in-theory '((zzchk-check) (aig-norm))))) ACL2 Warning [Disable] in ( DEFTHM AIG-IS-UNSAT ...): Forcing has transitioned from enabled to disabled. See :DOC force. Note: Checking SAT proof (18 lines, 15 resolution steps).... 0: root, length 3 1: root, length 3 2: root, length 2 3: root, length 2 4: root, length 3 5: root, length 2 6: root, length 2 7: root, length 3 8: root, length 3 9: root, length 2 10: root, length 2 11: root, length 2 12: root, length 2 13: root, length 3 14: chain, length 7 15: root, length 2 16: root, length 2 17: chain, length 10 done; cpu 0.01; real 0.01; mem 16,608 Note: Checking that input AIG is what was proved.... done; cpu 0.00; real 0.00; mem 1,280 Q.E.D. Summary Form: ( DEFTHM AIG-IS-UNSAT ...) Rules: ((:EXECUTABLE-COUNTERPART AIG-NORM) (:EXECUTABLE-COUNTERPART ZZCHK-CHECK)) Warnings: Disable Time: 0.02 seconds (prove: 0.01, print: 0.00, other: 0.00) Prover steps counted: 16 AIG-IS-UNSAT ACL2 !>(pe 'zz-sat) d 6 (INCLUDE-BOOK "g-logic/gl-extras" :DIR ...) \ [Included books, outermost to innermost: "/Users/kaufmann/fh/e/2011-04-11/e/cbooks/g-logic/gl-extras.lisp" "/Users/kaufmann/fh/e/2011-04-11/e/cbooks/g-logic/g-sat.lisp" "/Users/kaufmann/fh/e/2011-04-11/e/cbooks/aig/zz.lisp" ] \ > (DEFMACRO ZZ-SAT (AIG &KEY (MK-MODEL 'T) (TIMEOUT 'NIL)) (CONS 'ZZ-SAT-EXEC (CONS AIG (CONS MK-MODEL (CONS TIMEOUT 'NIL))))) ACL2 !>(pe 'zz-sat-exec) d 6 (INCLUDE-BOOK "g-logic/gl-extras" :DIR ...) \ [Included books, outermost to innermost: "/Users/kaufmann/fh/e/2011-04-11/e/cbooks/g-logic/gl-extras.lisp" "/Users/kaufmann/fh/e/2011-04-11/e/cbooks/g-logic/g-sat.lisp" "/Users/kaufmann/fh/e/2011-04-11/e/cbooks/aig/zz.lisp" ] \ >V (DEFUN ZZ-SAT-EXEC (AIG MK-MODEL TIMEOUT) (DECLARE (XARGS :GUARD (OR (NOT TIMEOUT) (NATP TIMEOUT)))) (ZZ-SAT-FN AIG MK-MODEL TIMEOUT)) ACL2 !>(fmx "Search for include-raw in file zz.lisp printed out above.~%~ Then search for zz-sat-exec in the resulting file zz-raw.lsp.~%~ Note the use there of zz-proof-alist.~%") Search for include-raw in file zz.lisp printed out above. Then search for zz-sat-exec in the resulting file zz-raw.lsp. Note the use there of zz-proof-alist. (0 ) ACL2 !>(zz-sat ; can also be used to generate counterexamples (aig-not (aig-iff (aig-or 'x 'y) (aig-or 'z (aig-or 'y 'x))))) (SAT (Z . T) (X) (Y)) ACL2 !>