1 ;;; -*- Mode: Lisp; Syntax: ANSI-Common-Lisp; Base: 10; -*-
3 ;;; backend.lisp --- SAT wrapper generic backend definition
5 ;; Copyright (C) 2010 Utz-Uwe Haus <lisp@uuhaus.de>
7 ;; This code is free software; you can redistribute it and/or modify
8 ;; it under the terms of the version 3 of the GNU General
9 ;; Public License as published by the Free Software Foundation, as
10 ;; clarified by the prequel found in LICENSE.Lisp-GPL-Preface.
12 ;; This code is distributed in the hope that it will be useful, but
13 ;; without any warranty; without even the implied warranty of
14 ;; merchantability or fitness for a particular purpose. See the GNU
15 ;; Lesser General Public License for more details.
17 ;; Version 3 of the GNU General Public License is in the file
18 ;; LICENSE.GPL that was distributed with this file. If it is not
19 ;; present, you can access it from
20 ;; http://www.gnu.org/copyleft/gpl.txt (until superseded by a
21 ;; newer version) or write to the Free Software Foundation, Inc., 59
22 ;; Temple Place, Suite 330, Boston, MA 02111-1307 USA
31 (eval-when (:compile-toplevel
:load-toplevel
)
32 (declaim (optimize (speed 3) (debug 1) (safety 1))))
34 (in-package #:satwrap.backend
)
37 (defclass satwrap-backend
()
38 ((name :accessor sat-backend-name
:initarg
:name
)
39 (version :accessor sat-backend-version
:initarg
:version
))
40 (:documentation
"Superclass of all sat backends"))
43 ;; these generics need implementations for each backend:
44 (defgeneric (setf numvars
) (numvars backend
)
45 (:documentation
"Declare number of variables used in backend."))
47 (defgeneric add-clause
(backend clause
)
48 (:documentation
"Add CLAUSE to CNF of BACKEND."))
50 (defgeneric satisfiablep
(backend assumptions
)
51 (:documentation
"Check BACKEND for satisfiability under ASSUMPTIONS.
53 ;; no default implementation, but convert vector to list for dumb backends
54 (:method
((be satwrap-backend
) (assumptions vector
))
55 (satisfiablep be
(coerce assumptions
'list
))))
57 (defgeneric solution
(backend interesting-vars
)
58 (:documentation
"Return the values of INTERESTING-VARS in last SAT solution of BACKEND."))
61 ;; these generics do not need to be implemented as there are default implementations
62 (defgeneric get-essential-variables
(backend)
63 (:documentation
"Compute the variables that are essential, i.e. fixed in all solutions of SOLVER.
64 Returns a list of literals fixed, sign according to phase."))
66 (defgeneric synchronize-backend
(backend numvars new-clauses deleted-clauses old-clauses
)
67 (:documentation
"Populate CNF with NUMVARS variables in BACKEND.
68 NEW-CLAUSES are the clauses added since the last call to synchronize-backend,
69 DELETED-CLAUSES are the clauses deleted since the last call to synchronize-backend,
70 OLD-CLAUSES is the union of the NEW-CLAUSES and the OLD-CLAUSES minus the DELETED-CLAUSES when synchronize-backend was last called, including the DELETED-CLAUSES.")
71 (:method
((backend satwrap-backend
) numvars
73 (deleted-clauses list
)
75 "Default implementation: Stuff everything into a possibly fresh solver."
76 (reinitialize-instance backend
)
77 ;; declare proper number of variables
78 (setf (numvars backend
) numvars
)
79 ;; old clauses, including deletion
80 (loop :for c
:in old-clauses
81 :unless
(member c deleted-clauses
:test
#'equal
)
82 :do
(add-clause backend c
))
84 (dolist (c new-clauses
)
85 (add-clause backend c
))))