From 4e94cd31b8c41f2d2c2e98d0dad5916ad88dd636 Mon Sep 17 00:00:00 2001 From: Utz-Uwe Haus Date: Tue, 22 Jun 2010 22:44:20 +0200 Subject: [PATCH] Add vector variant for clause-valid method Signed-off-by: Utz-Uwe Haus --- satwrap.lisp | 9 +++++++++ 1 file changed, 9 insertions(+) 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