package.lisp

   1 ;;; -*- Mode: Lisp; Syntax: ANSI-Common-Lisp; Base: 10; -*-
   2 ;;;
   3 ;;; package.lisp --- SATWRAP package definitons
   4
   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.
  13 ;;
  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.
  18 ;;
  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
  25 ;;
  26 ;; Commentary:
  27
  28 ;;
  29
  30 ;;; Code:
  31
  32
  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   )
  44
  45
  46 (defpackage #:satwrap
  47   (:use #:CL)
  48   ;; class:
  49   (:export #:sat-solver)
  50   ;; ctor:
  51   (:export #:make-sat-solver)
  52   ;; accessors:
  53   (:export #:sat-solver-backend
  54            #:sat-solver-numvars
  55            #:sat-solver-numclauses)
  56   ;; conditions:
  57   (:export #:satwrap-condition #:invalid-clause)
  58   ;; interface:
  59   (:export #:add-variable #:add-clause #:satisfiablep #:solution
  60            #:get-essential-variables
  61            #:with-sat-solver #:with-index-hash)
  62   ;; input/output
  63   (:export #:read-dimacs #:write-dimacs)
  64   )
  65