backends/precosat/precosat-cffi.i

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