From fcbbade0f3e3186315a32c602e6a0cd432363854 Mon Sep 17 00:00:00 2001 From: Utz-Uwe Haus Date: Tue, 22 Jun 2010 10:45:30 +0200 Subject: [PATCH] fix add-formula to drop :AND and :OR-symbols before adding clauses Signed-off-by: Utz-Uwe Haus --- satwrap.lisp | 5 ++++- 1 file changed, 4 insertions(+), 1 deletion(-) diff --git a/satwrap.lisp b/satwrap.lisp index bc86495..78da8bd 100644 --- a/satwrap.lisp +++ b/satwrap.lisp @@ -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.") -- 2.11.4.GIT