From 73d36d832d14b81cf96b6388a2e832fa830ec542 Mon Sep 17 00:00:00 2001
From: Utz-Uwe Haus <lisp@uuhaus.de>
Date: Tue, 22 Jun 2010 22:42:03 +0200
Subject: [PATCH] Allow assumptions to be lists or vectors in backend

Implement vector variant for minisat backend

Signed-off-by: Utz-Uwe Haus <lisp@uuhaus.de>
---
 backend.lisp                    |  5 ++++-
 backends/minisat/minisat-cffi.i | 15 ++++++++++-----
 satwrap.lisp                    |  9 +++++++++
 3 files changed, 23 insertions(+), 6 deletions(-)

diff --git a/backend.lisp b/backend.lisp
index 908e6f8..9a10ef2 100644
--- a/backend.lisp
+++ b/backend.lisp
@@ -49,7 +49,10 @@
 
 (defgeneric satisfiablep (backend assumptions)
   (:documentation "Check BACKEND for satisfiability under ASSUMPTIONS. 
-Returns T or NIL."))
+Returns T or NIL.")
+  ;; no default implementation, but convert vector to list for dumb backends
+  (:method ((be satwrap-backend) (assumptions vector))
+    (satisfiablep be (coerce assumptions 'list))))
 
 (defgeneric solution (backend interesting-vars)
   (:documentation "Return the values of INTERESTING-VARS in last SAT solution of BACKEND."))
diff --git a/backends/minisat/minisat-cffi.i b/backends/minisat/minisat-cffi.i
index 0ee567d..14166d2 100644
--- a/backends/minisat/minisat-cffi.i
+++ b/backends/minisat/minisat-cffi.i
@@ -159,17 +159,22 @@ TYPEMAP_WRAPPED_POINTER(struct minisat_solver *, minisat-solver)
 
 (defmacro with-assumptions ((solver assumptions) &body body)
   (let ((i (gensym "i"))
-	(s (gensym "solver")))
-    `(let ((,s ,solver))
+	(s (gensym "solver"))
+	(a (gensym "assumptions")))
+    `(let ((,s ,solver)
+	   (,a ,assumptions))
        (unwind-protect 
 	    (progn
 	      (minisat-clear-assumptions ,s)
-	      (dolist (,i ,assumptions)
-		(minisat-add-assumption ,s ,i))
+	      (etypecase ,a
+		(list (dolist (,i ,a)
+			(minisat-add-assumption ,s ,i)))
+		(vector (loop :for ,i :across ,a
+			   :do (minisat-add-assumption ,s ,i))))
 	      ,@body)
 	 (minisat-clear-assumptions ,s)))))
 
-(defmethod satisfiablep ((backend minisat-backend) (assumptions list))
+(defmethod satisfiablep ((backend minisat-backend) (assumptions sequence))
   (ecase (let ((be (minisat-backend-solver backend)))
 	   (with-assumptions (be assumptions)
 	     (minisat-solve be)))
diff --git a/satwrap.lisp b/satwrap.lisp
index 116b7b2..9bd436c 100644
--- a/satwrap.lisp
+++ b/satwrap.lisp
@@ -84,6 +84,15 @@
      :always (and (not (zerop v))
 		  (<= min v max))))
 
+(defmethod clause-valid ((solver sat-solver) (clause vector))
+  "Check that CLAUSE is a valid clause for SOLVER."
+  (loop
+     :with max := (sat-solver-numvars solver)
+     :with min := (- max)
+     :for v :across clause
+     :always (and (not (zerop v))
+		  (<= min v max))))
+
 (defmacro iota (n &optional (start 1))
   "Return a list of the N sequential integers starting at START (default: 1)."
   (let ((i (gensym "i")))
-- 
2.11.4.GIT