Allow assumptions to be lists or vectors in backend
authorUtz-Uwe Haus <lisp@uuhaus.de>
Tue, 22 Jun 2010 20:42:03 +0000 (22 22:42 +0200)
committerUtz-Uwe Haus <lisp@uuhaus.de>
Tue, 22 Jun 2010 20:42:03 +0000 (22 22:42 +0200)
Implement vector variant for minisat backend

Signed-off-by: Utz-Uwe Haus <lisp@uuhaus.de>
backend.lisp
backends/minisat/minisat-cffi.i
satwrap.lisp

index 908e6f8..9a10ef2 100644 (file)
 
 (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."))
index 0ee567d..14166d2 100644 (file)
@@ -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)))
index 116b7b2..9bd436c 100644 (file)
      :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")))