fix add-formula to drop :AND and :OR-symbols before adding clauses
authorUtz-Uwe Haus <lisp@uuhaus.de>
Tue, 22 Jun 2010 08:45:30 +0000 (22 10:45 +0200)
committerUtz-Uwe Haus <lisp@uuhaus.de>
Tue, 22 Jun 2010 08:45:30 +0000 (22 10:45 +0200)
Signed-off-by: Utz-Uwe Haus <lisp@uuhaus.de>
satwrap.lisp

index bc86495..78da8bd 100644 (file)
@@ -443,7 +443,10 @@ Supports :IMPLY, :IFF, binary :XOR, and :NOR. "
 Formula is an expression tree that can contain high-level abbreviations :IMPLY, :IFF, :NOR and :XOR, as well as the basic :AND, :OR, :NOT. Everything else is considered an atom. Atoms can also be explicitly written as (:ATOM foo). 
 All atoms will be mapped through MAPPING before being added to the solver to convert your favorite atoms to phased variables. MAPPING is a function of 1 argument, the atom. It defaults to  #'identity. Afterwards, clean clauses (removing duplicates and simplifying trivial clauses, comparing atoms using ATOM-TEST (default: #'eql).")
   (:method ((solver sat-solver) (formula list) &key (mapping #'identity) (atom-test #'eql))
-    (add-clauses solver (tree->cnf formula mapping atom-test))))
+    (dolist (c (cdr ;; drop outer :AND
+               (tree->cnf formula mapping atom-test)))
+      (add-clause solver (cdr ;; drop :OR
+                         c)))))
 
 (defgeneric add-and (solver literals &key mapping)
   (:documentation "Add clauses for AND(literals) to SOLVER.")