Fix macro expansion time confusion in with-index-hash
[cl-satwrap.git] / package.lisp
bloba3f58a2ccc8fab763c510893736196ab8a748b1f
1 ;;; -*- Mode: Lisp; Syntax: ANSI-Common-Lisp; Base: 10; -*-
2 ;;;
3 ;;; package.lisp --- SATWRAP package definitons
5 ;; Copyright (C) 2010 Utz-Uwe Haus <lisp@uuhaus.de>
6 ;;
7 ;; $Id:$
8 ;;
9 ;; This code is free software; you can redistribute it and/or modify
10 ;; it under the terms of the version 3 of the GNU General
11 ;; Public License as published by the Free Software Foundation, as
12 ;; clarified by the prequel found in LICENSE.Lisp-GPL-Preface.
14 ;; This code is distributed in the hope that it will be useful, but
15 ;; without any warranty; without even the implied warranty of
16 ;; merchantability or fitness for a particular purpose. See the GNU
17 ;; Lesser General Public License for more details.
19 ;; Version 3 of the GNU General Public License is in the file
20 ;; LICENSE.GPL that was distributed with this file. If it is not
21 ;; present, you can access it from
22 ;; http://www.gnu.org/copyleft/gpl.txt (until superseded by a
23 ;; newer version) or write to the Free Software Foundation, Inc., 59
24 ;; Temple Place, Suite 330, Boston, MA 02111-1307 USA
26 ;; Commentary:
28 ;;
30 ;;; Code:
33 (defpackage #:satwrap.backend
34 (:use #:cl)
35 ;; required interface for each backend:
36 (:export #:satwrap-backend
37 #:numvars
38 #:add-clause
39 #:satisfiablep
40 #:solution)
41 ;; optional interface:
42 (:export #:get-essential-variables
43 #:synchronize-backend)
44 ;; utilities
45 (:export #:sat-backend-name #:sat-backend-version)
49 (defpackage #:satwrap
50 (:use #:CL)
51 ;; class:
52 (:export #:sat-solver)
53 ;; ctor:
54 (:export #:make-sat-solver)
55 ;; accessors:
56 (:export #:sat-solver-backend
57 #:sat-solver-numvars
58 #:sat-solver-numclauses)
59 ;; conditions:
60 (:export #:satwrap-condition #:invalid-clause)
61 ;; interface:
62 (:export #:add-variable #:add-clause #:satisfiablep #:solution
63 #:get-essential-variables
64 #:with-sat-solver #:with-index-hash
65 #:add-clauses)
66 ;; convenience functions for common logical operations; could be
67 ;; handled specially one day by backends that support structure informations
68 ;; on CNFs
69 (:export #:add-formula)
70 (:export #:add-and #:add-or #:add-xor #:add-if #:add-iff)
71 ;; input/output
72 (:export #:read-dimacs #:write-dimacs)
73 ;; utils
74 (:export #:describe-supported-backends
75 #:*default-sat-backend*