From b93205ceb9c175369e41bc2598a2304a79d90642 Mon Sep 17 00:00:00 2001 From: Utz-Uwe Haus Date: Fri, 18 Jun 2010 01:26:44 +0200 Subject: [PATCH] remove debugging output and ensure empty clauses are deleted from CNFs Signed-off-by: Utz-Uwe Haus --- satwrap.lisp | 31 ++++++++++++++----------------- 1 file changed, 14 insertions(+), 17 deletions(-) diff --git a/satwrap.lisp b/satwrap.lisp index 562d9b9..f7e11aa 100644 --- a/satwrap.lisp +++ b/satwrap.lisp @@ -359,17 +359,16 @@ Supports :IMPLY, :IFF, binary :XOR, and :NOR. " (push `(,term) ands))) (let ((clauses (crossprod ands))) `(:AND ,@(mapcar #'(lambda (c) - (format T "~&;; c=~A~%" c) (if (not (consp c)) c `(:OR ,@ (loop :for subterm :in c - :if (and (consp subterm) - (eq :OR (car subterm))) - ;; (OR(OR...)) == (OR ...) - :append (cdr subterm) - ;; if C is not an OR-clause - ;; it is considered atomic: - :else :append `(,subterm))))) + :if (and (consp subterm) + (eq :OR (car subterm))) + ;; (OR(OR...)) == (OR ...) + :append (cdr subterm) + ;; if C is not an OR-clause + ;; it is considered atomic: + :else :append `(,subterm))))) clauses))))) (otherwise tree)) @@ -424,15 +423,13 @@ Supports :IMPLY, :IFF, binary :XOR, and :NOR. " (if (atomic cnf) (setf cnf (funcall mapping cnf)) (setf (cdr cnf) ;; we must be looking at an AND - (mapcar #'(lambda (clause) - (if (atomic clause) - (funcall mapping clause) - (if (trivial-clausep clause) - '(:OR ) - `(:OR ,@(remove-duplicates - (cdr clause) - :test #'duplicate-literalsp))))) - (cdr cnf)))) + (loop :for clause :in (cdr cnf) + :if (atomic clause) + :collect (funcall mapping clause) + :else :if (not (trivial-clausep clause)) + :collect `(:OR ,@(remove-duplicates + (cdr clause) + :test #'duplicate-literalsp))))) cnf)) (clean-clauses (map-literals -- 2.11.4.GIT