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            #:synchronize-backend)
  44   ;; utilities
  45   (:export #:sat-backend-name #:sat-backend-version)
  46   )
  47
  48
  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*
  76 )
  77   )
  78