Reduce consing in flush-to-backend
authorUtz-Uwe Haus <lisp@uuhaus.de>
Tue, 22 Jun 2010 20:44:40 +0000 (22 22:44 +0200)
committerUtz-Uwe Haus <lisp@uuhaus.de>
Tue, 22 Jun 2010 20:44:40 +0000 (22 22:44 +0200)
Signed-off-by: Utz-Uwe Haus <lisp@uuhaus.de>
satwrap.lisp

index 9bd436c..d0aaa0a 100644 (file)
 
 (defmethod flush-to-backend ((solver sat-solver))
   "Populate backend, possibly flushing old backend contents."
-  (satwrap.backend:synchronize-backend (sat-solver-backend solver)
-                                      (sat-solver-numvars solver)
-                                      (sat-solver-new-clauses solver)
-                                      '() ;; deleted clauses, not yet supported
-                                      (sat-solver-old-clauses solver))
-  (loop :with deleted := '()
-     :for c :in (sat-solver-old-clauses solver)
-     :unless (find c deleted :test #'equal)
-     :do (push c (sat-solver-new-clauses solver)))
-  (setf (sat-solver-old-clauses solver) (sat-solver-new-clauses solver)
-       (sat-solver-new-clauses solver) '()))
+  (let ((deleted '()))
+    (satwrap.backend:synchronize-backend (sat-solver-backend solver)
+                                        (sat-solver-numvars solver)
+                                        (sat-solver-new-clauses solver)
+                                        deleted
+                                        (sat-solver-old-clauses solver))
+    (setf (sat-solver-old-clauses solver) 
+         (nconc (sat-solver-new-clauses solver)
+                (if deleted
+                    (delete-if #'(lambda (c)
+                                   (find c deleted :test #'equal))
+                               (sat-solver-old-clauses solver))
+                    (sat-solver-old-clauses solver))))
+    (setf (sat-solver-new-clauses solver) '())))
 
 \f
 (defun make-sat-solver (&optional (backend *default-sat-backend*))