From: Alan Ruttenberg <alanruttenberg@gm...>  20060713 18:38:45

I'm working with snark theorem prover and am finding that it behaves differently depending on whether is is compiled or interpreted (wrong when compiled). It's a pretty big system, but as a start, here are two functions which cause an infinite loop when compiled, but not when interpreted, for the same input. Perhaps you have some insights ... Both of them have labels constructs, in case that has something to do with it. (defun clausify (wff &optional mapfun) ;; apply mapfun to each clause in the clause form of wff ;; if mapfun is NIL, return CNF of wff (let ((clauses nil) clauseslast) (labels ((clausify* (cc wff pos lits) (cond ((and pos (testoption6?) (clausep wff t)) (funcall cc (cons wff lits))) (t (ecase (headislogicalsymbol wff) ((nil) (cond ((eq true wff) (unless pos (funcall cc lits))) ((eq false wff) (when pos (funcall cc lits))) (t (let ((wff (makecompound *not* wff))) (dolist (lit lits (funcall cc (cons (if pos wff  wff) lits))) (cond ((equalp lit wff) (when pos (funcall cc lits)) (return)) ((equalp lit wff) (unless pos (funcall cc lits)) (return)))))))) (not (clausify* cc (first (args wff)) (not pos) lits)) (and (let ((args (args wff))) (if pos (if (and lits (some (lambda (arg) (memberp arg lits)) args)) (funcall cc lits) (dolist (arg args) (clausify* cc arg t lits))) (let ((y (makea1compound* *and* true (rest args)))) (clausify* (lambda (l) (clausify* cc y nil l)) (first args) nil lits))))) (or (let ((args (args wff))) (if pos (let ((y (makea1compound* *or* false (rest args)))) (clausify* (lambda (l) (clausify* cc y t l)) (first args) t lits)) (if (and lits (some (lambda (arg) (memberp (negate arg) lits)) args)) (funcall cc lits) (dolist (arg args) (clausify* cc arg nil lits)))))) (implies (let* ((args (args wff)) (x (first args)) (y (second args))) (if pos (clausify* (lambda (l) (clausify* cc y t l)) x nil lits) (progn (clausify* cc x t lits) (clausify* cc y nil lits))))) (impliedby (let* ((args (args wff)) (x (first args)) (y (second args))) (if pos (clausify* (lambda (l) (clausify* cc y nil l)) x t lits) (progn (clausify* cc y t lits) (clausify* cc x nil lits))))) (iff (let* ((args (args wff)) (x (first args)) (y (makea1 compound* *iff* true (rest args)))) (if pos (progn (clausify* (lambda (l) (clausify* cc y t l)) x nil lits) (clausify* (lambda (l) (clausify* cc y nil l)) x t lits)) (progn (clausify* (lambda (l) (clausify* cc y nil l)) x nil lits) (clausify* (lambda (l) (clausify* cc y t l)) x t lits))))) (xor (let* ((args (args wff)) (x (first args)) (y (makea1 compound* *xor* false (rest args)))) (if pos (progn (clausify* (lambda (l) (clausify* cc y nil l)) x nil lits) (clausify* (lambda (l) (clausify* cc y t l)) x t lits)) (progn (clausify* (lambda (l) (clausify* cc y t l)) x nil lits) (clausify* (lambda (l) (clausify* cc y nil l)) x t lits))))) (if (let* ((args (args wff)) (x (first args)) (y (second args)) (z (third args))) (clausify* (lambda (l) (clausify* cc y pos l)) x nil lits) (clausify* (lambda (l) (clausify* cc z pos l)) x t lits)))))))) (clausify* (lambda (lits) (let ((clause (makea1compound* *or* false (reverse lits)))) (if mapfun (funcall mapfun clause) (collect clause clauses)))) wff t nil) (if mapfun nil (makea1compound* *and* true clauses))))) (defun wffclauses (wff &optional mapfun) ;; apply mapfun to each clause in the clause form of wff (let ((clauses nil)) (labels ((wffkind (wff) (cond ((consp wff) (let ((head (first wff))) (case head (not (cl:assert (eql 1 (length (rest wff))) () "Wff ~A should have one argument." wff) head) ((and or) (cl:assert (<= 2 (length (rest wff))) () "Wff ~A should have two or more arguments." wff) head) ((implies impliedby iff xor) (cl:assert (eql 2 (length (rest wff))) () "Wff ~A should have two arguments." wff) head) (if (cl:assert (eql 3 (length (rest wff))) () "Wff ~A should have three arguments." wff) head) ((andover orover) (cl:assert (eql 2 (length (rest wff))) () "Wff ~A should have two arguments." wff) (cl:assert (variablesandrangesp (second wff))) head) (otherwise :literal)))) (t :literal))) (wffclauses* (wff pos lits mapfun) (case (wffkind wff) (:literal (let ((wff (complementaryliteral wff))) (when *inputsortwff* (declaresort* wff)) (unless (eq (if pos 'true 'false) wff) (dolist (lit lits (funcall mapfun (if (eq (if pos 'false 'true) wff) lits (cons (if pos wff wff) lits)))) (cond ((equal lit wff) (when pos (funcall mapfun lits)) (return)) ((equal lit wff) (unless pos (funcall mapfun lits)) (return))))))) (not (wffclauses* (second wff) (not pos) lits mapfun)) (and (if pos (if (and lits (some (lambda (arg) (member arg lits :test #'equal)) (rest wff))) (funcall mapfun lits) (dolist (arg (rest wff)) (wffclauses* arg t lits mapfun))) (wffclauses* (second wff) nil lits (lambda (l) (wffclauses* (if (rest (rest (rest wff))) `(and ,@(rest (rest wff))) (third wff)) nil l mapfun))))) (or (if pos (wffclauses* (second wff) t lits (lambda (l) (wffclauses* (if (rest (rest (rest wff))) `(or ,@(rest (rest wff))) (third wff)) t l mapfun))) (if (and lits (some (lambda (arg) (member (complementaryliteral arg) lits :test #'equal)) (rest wff))) (funcall mapfun lits) (dolist (arg (rest wff)) (wffclauses* arg nil lits mapfun))))) (implies (if pos (wffclauses* (second wff) nil lits (lambda (l) (wffclauses* (third wff) t l mapfun))) (progn (wffclauses* (second wff) t lits mapfun) (wffclauses* (third wff) nil lits mapfun)))) (impliedby (if pos (wffclauses* (third wff) nil lits (lambda (l) (wffclauses* (second wff) t l mapfun))) (progn (wffclauses* (third wff) t lits mapfun) (wffclauses* (second wff) nil lits mapfun)))) (iff (if pos (progn (wffclauses* (second wff) nil lits (lambda (l) (wffclauses* (third wff) t l mapfun))) (wffclauses* (second wff) t lits (lambda (l) (wffclauses* (third wff) nil l mapfun)))) (progn (wffclauses* (second wff) nil lits (lambda (l) (wffclauses* (third wff) nil l mapfun))) (wffclauses* (second wff) t lits (lambda (l) (wffclauses* (third wff) t l mapfun)))))) (xor (if pos (progn (wffclauses* (second wff) nil lits (lambda (l) (wffclauses* (third wff) nil l mapfun))) (wffclauses* (second wff) t lits (lambda (l) (wffclauses* (third wff) t l mapfun)))) (progn (wffclauses* (second wff) nil lits (lambda (l) (wffclauses* (third wff) t l mapfun))) (wffclauses* (second wff) t lits (lambda (l) (wffclauses* (third wff) nil l mapfun)))))) (if (wffclauses* (second wff) nil lits (lambda (l) (wff clauses* (third wff) pos l mapfun))) (wffclauses* (second wff) t lits (lambda (l) (wff clauses* (fourth wff) pos l mapfun)))) (andover (let ((wffs (expandrangeform (if (consp (first (second wff))) (second wff) (list (second wff))) (third wff) nil))) (cl:assert (not (null wffs)) () "Wff ~A expands into empty conjunction." wff) (wffclauses* (if (null (rest wffs)) (first wffs) ` (and ,@wffs)) pos lits mapfun))) (orover (let ((wffs (expandrangeform (if (consp (first (second wff))) (second wff) (list (second wff))) (third wff) nil))) (cl:assert (not (null wffs)) () "Wff ~A expands into empty disjunction." wff) (wffclauses* (if (null (rest wffs)) (first wffs) ` (or ,@wffs)) pos lits mapfun)))))) (wffclauses* wff t nil (lambda (lits) (if mapfun (funcall mapfun (reverse lits)) (push (reverse lits) clauses)))) (nreverse clauses)))) 