Add vector variant for clause-valid method
authorUtz-Uwe Haus <lisp@uuhaus.de>
Tue, 22 Jun 2010 20:44:20 +0000 (22 22:44 +0200)
committerUtz-Uwe Haus <lisp@uuhaus.de>
Tue, 22 Jun 2010 20:44:20 +0000 (22 22:44 +0200)
Signed-off-by: Utz-Uwe Haus <lisp@uuhaus.de>
satwrap.lisp

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