From fd81d3c3f97210a3261fbb157cd5d26aa0b9e9a8 Mon Sep 17 00:00:00 2001 From: Utz-Uwe Haus Date: Tue, 22 Jun 2010 22:44:40 +0200 Subject: [PATCH] Reduce consing in flush-to-backend Signed-off-by: Utz-Uwe Haus --- satwrap.lisp | 25 ++++++++++++++----------- 1 file changed, 14 insertions(+), 11 deletions(-) diff --git a/satwrap.lisp b/satwrap.lisp index 9bd436c..d0aaa0a 100644 --- a/satwrap.lisp +++ b/satwrap.lisp @@ -123,17 +123,20 @@ (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) '()))) (defun make-sat-solver (&optional (backend *default-sat-backend*)) -- 2.11.4.GIT