From: Utz-Uwe Haus <lisp@uuhaus.de>
Date: Tue, 22 Jun 2010 20:44:20 +0000 (+0200)
Subject: Add vector variant for clause-valid method
X-Git-Url: https://repo.or.cz/w/cl-satwrap.git/commitdiff_plain/4e94cd31b8c41f2d2c2e98d0dad5916ad88dd636

Add vector variant for clause-valid method

Signed-off-by: Utz-Uwe Haus <lisp@uuhaus.de>
---

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")))