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.
54 (defgeneric solution
(backend interesting-vars
)
55 (:documentation
"Return the values of INTERESTING-VARS in last SAT solution of BACKEND."))
59 ;; these generics do not need to be implemented as there are default implementations
60 (defgeneric get-essential-variables
(backend)
61 (:documentation
"Compute the variables that are essential, i.e. fixed in all solutions of SOLVER.
62 Returns a list of literals fixed, sign according to phase."))