remove debugging output and ensure empty clauses are deleted from CNFs
authorUtz-Uwe Haus <lisp@uuhaus.de>
Thu, 17 Jun 2010 23:26:44 +0000 (18 01:26 +0200)
committerUtz-Uwe Haus <lisp@uuhaus.de>
Thu, 17 Jun 2010 23:26:44 +0000 (18 01:26 +0200)
Signed-off-by: Utz-Uwe Haus <lisp@uuhaus.de>
satwrap.lisp

index 562d9b9..f7e11aa 100644 (file)
@@ -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