backends/minisat/minisat-cffi.i

   1 /* SWIG wrapper generation for minisat library -*- lisp -*- */
   2 /* (c) 2010 Utz-Uwe Haus */
   3
   4 %module "satwrap.minisat"
   5
   6 %feature("intern_function","1");   // use swig-lispify
   7 %feature("export");                // export wrapped things
   8
   9 %insert("lisphead")%{
  10 ;;; Auto-generated -*- lisp -*- file
  11 ;;; generated from $Id:$
  12 (eval-when (:compile-toplevel :load-toplevel)
  13   (declaim (optimize (speed 3) (debug 0) (safety 1))))
  14
  15 (cl:defpackage :satwrap.minisat
  16   (:use :cl :cffi :satwrap.backend)
  17   (:documentation "Package containing minisat-backend")
  18   ;; other exports done by swig
  19   (:export #:minisat-backend #:satisiablep #:solution #:add-clause #:numvars))
  20 (cl:in-package :satwrap.minisat)
  21 (eval-when (:compile-toplevel :load-toplevel :execute)
  22   (cl:defun swig-lispify (name flag cl:&optional (package (find-package :satwrap.minisat)))
  23     (cl:labels ((helper (lst last rest cl:&aux (c (cl:car lst)))
  24                   (cl:cond
  25                     ((cl:null lst)
  26                      rest)
  27                     ((cl:upper-case-p c)
  28                      (helper (cl:cdr lst) 'upper
  29                              (cl:case last
  30                                ((lower digit) (cl:list* c #\- rest))
  31                                (cl:t (cl:cons c rest)))))
  32                     ((cl:lower-case-p c)
  33                      (helper (cl:cdr lst) 'lower (cl:cons (cl:char-upcase c) rest)))
  34                     ((cl:digit-char-p c)
  35                      (helper (cl:cdr lst) 'digit
  36                              (cl:case last
  37                                ((upper lower) (cl:list* c #\- rest))
  38                                (cl:t (cl:cons c rest)))))
  39                     ((cl:char-equal c #\_)
  40                      (helper (cl:cdr lst) '_ (cl:cons #\- rest)))
  41                     ((cl:char-equal c #\-)
  42                      (helper (cl:cdr lst) '- (cl:cons #\- rest)))
  43                     (cl:t
  44                      (cl:error "Invalid character: ~A" c)))))
  45       (cl:let ((fix (cl:case flag
  46                       ((constant enumvalue) "+")
  47                       (variable "*")
  48                       (cl:t ""))))
  49         (cl:intern
  50          (cl:concatenate
  51           'cl:string
  52           fix
  53           (cl:nreverse (helper (cl:concatenate 'cl:list name) cl:nil cl:nil))
  54           fix)
  55          package)))))
  56
  57 %}
  58
  59 %insert ("swiglisp") %{
  60
  61
  62 %}
  63
  64 %insert ("swiglisp") %{
  65 ;; foreign type definitions to hide pointer values
  66 (defclass wrapped-pointer ()
  67   ((ptrval :reader get-ptrval :initarg :ptrval)
  68    (ctype  :reader get-ctype :initarg :ctype))
  69   (:documentation "A wrapped pointer"))
  70
  71 (defmethod print-object ((p wrapped-pointer) stream)
  72   (print-unreadable-object (p stream :type nil :identity nil)
  73     (format stream "wrapper around `~A' @0x~16R" (get-ctype p) (get-ptrval p))))
  74
  75 (define-condition foreign-null-pointer-condition (error)
  76   ((type :initarg :type
  77          :reader foreign-null-pointer-condition-type))
  78   (:report (lambda (condition stream)
  79              (format stream "The foreign pointer of type ~A was NULL"
  80                      (foreign-null-pointer-condition-type condition)))))
  81
  82 %}
  83
  84 %define TYPEMAP_WRAPPED_POINTER(PTRTYPE,LISPCLASS)
  85
  86 %insert ("swiglisp") %{
  87 (define-foreign-type LISPCLASS ()
  88   ()
  89   (:actual-type :pointer)
  90   (:documentation "cffi wrapper type around PTRTYPE."))
  91
  92 (define-parse-method LISPCLASS ()
  93   (make-instance 'LISPCLASS))
  94
  95 (defmethod translate-from-foreign (value (type LISPCLASS))
  96   "Wrap PTRTYPE, signaling a null-pointer-exception if value is NULL."
  97   (if (cffi:null-pointer-p value)
  98       (error 'foreign-null-pointer-condition :type type)
  99       (make-instance 'wrapped-pointer :ptrval value :ctype "PTRTYPE")))
 100
 101 (defmethod translate-to-foreign ((g wrapped-pointer) (type LISPCLASS))
 102   "Unwrap PTRTYPE"
 103   (get-ptrval g))
 104
 105 %}
 106 %typemap (cin) PTRTYPE "LISPCLASS"
 107 %typemap (cout) PTRTYPE "LISPCLASS"
 108 %enddef
 109
 110 TYPEMAP_WRAPPED_POINTER(struct minisat_solver *, minisat-solver)
 111
 112 %typemap (cin)  struct minisat_solver * "minisat-solver"
 113 %typemap (cout) struct minisat_solver * "minisat-solver"
 114
 115 /* Now parse and wrap the API header */
 116 %insert ("swiglisp") %{
 117 (eval-when (:compile-toplevel :load-toplevel)
 118   ;; Muffle compiler-notes globally
 119   #+sbcl (declaim (sb-ext:muffle-conditions sb-ext:defconstant-uneql))
 120
 121 %}
 122
 123 %include "minisat_wrap.h"
 124 %insert ("swiglisp") %{
 125
 126 ;; implementation of a satwrap backend using minisat:
 127 (defclass minisat-backend (satwrap-backend)
 128   ((solver :initarg :solver :accessor minisat-backend-solver)
 129    (solved :initform NIL :accessor minisat-backend-solvedp))
 130
 131   (:default-initargs :name "MiniSAT" :version "2-070721"
 132                      :solver (alloc-minisat-solver))
 133   (:documentation "MiniSAT solver backend"))
 134 ) ;; end of eval-when to avoid top-level export
 135
 136 (defmethod initialize-instance :after ((instance minisat-backend) &rest initargs)
 137   (let ((solver (minisat-backend-solver instance)))
 138     (tg:finalize instance #'(lambda ()
 139                               ;; (format T "Finalizing ~X." solver)
 140                               (free-minisat-solver solver)))))
 141
 142 ;; (defmethod reinitialize-instance ((instance minisat-backend) &rest initargs &key &allow-other-keys)
 143 ;;   (apply #'call-next-method initargs))
 144
 145
 146
 147 (defmethod (setf numvars) ((numvars fixnum) (backend minisat-backend)) ;; arguments reversed for setf methods...
 148   (minisat-set-numvars (minisat-backend-solver backend) numvars))
 149
 150 (defmethod add-clause ((backend minisat-backend) (clause list))
 151   (assert (not (member 0 clause :test #'=)))
 152
 153   (loop :with solver := (minisat-backend-solver backend)
 154      :for v :of-type fixnum :in clause
 155      :do (minisat-add-var-to-clause solver v)
 156      :finally (progn
 157                 (minisat-add-var-to-clause solver 0)
 158                 (setf (minisat-backend-solvedp backend) NIL))))
 159
 160 (defmacro with-assumptions ((solver assumptions) &body body)
 161   (let ((i (gensym "i"))
 162         (s (gensym "solver"))
 163         (a (gensym "assumptions")))
 164     `(let ((,s ,solver)
 165            (,a ,assumptions))
 166        (unwind-protect
 167             (progn
 168               (minisat-clear-assumptions ,s)
 169               (etypecase ,a
 170                 (list (dolist (,i ,a)
 171                         (minisat-add-assumption ,s ,i)))
 172                 (vector (loop :for ,i :across ,a
 173                            :do (minisat-add-assumption ,s ,i))))
 174               ,@body)
 175          (minisat-clear-assumptions ,s)))))
 176
 177 (defmethod satisfiablep ((backend minisat-backend) (assumptions sequence))
 178   (ecase (let ((be (minisat-backend-solver backend)))
 179            (with-assumptions (be assumptions)
 180              (minisat-solve be)))
 181     (:+MINISAT-SAT+
 182      (setf (minisat-backend-solvedp backend) T)
 183      T)
 184     (:+MINISAT-UNSAT+ NIL)))
 185
 186 (defmethod solution ((backend minisat-backend) (interesting-vars list))
 187   (if (not (minisat-backend-solvedp backend))
 188       (error "Problem still unsolved or UNSAT")
 189       (loop :with be := (minisat-backend-solver backend)
 190          :for i :of-type fixnum :in interesting-vars
 191          :collect (minisat-sol-val be i))))
 192
 193 (defmethod synchronize-backend ((backend minisat-backend)
 194                                 numvars
 195                                 (new-clauses list)
 196                                 (deleted-clauses (eql '()))
 197                                 (old-clauses list))
 198   "Adding clauses is easy with minisat."
 199   (declare (ignore numvars))
 200   (dolist (c new-clauses)
 201     (add-clause backend c)))
 202 %}
 203
 204
 205