commit c938aea821dbbbac85b7832595a3d18ffc9068cd
parent 681f9021a83ef557a287758368ac08266b230103
Author: Tomas Hlavaty <tom@logand.com>
Date: Sun, 22 Jun 2014 03:12:41 +0200
optimize bdd a bit
Diffstat:
| M | bdd.lisp | | | 41 | ++++++++++++++++++++++++++--------------- |
1 file changed, 26 insertions(+), 15 deletions(-)
diff --git a/bdd.lisp b/bdd.lisp
@@ -27,22 +27,21 @@
(defparameter *mk-htab* (make-hash-table :test #'equal)) ;; (v l . h) equal => eq
+(deftype var () '(integer 2 #.(floor most-positive-fixnum 2)))
+(deftype nvar () '(integer #.(floor most-negative-fixnum 2) #.(floor most-positive-fixnum 2)))
+
(let ((k (list nil nil))) ;; reduce consing
(defun mk (v l h)
- (check-type v (integer 2 *))
- (check-type l (or bit list))
- (check-type h (or bit list))
- (let ((zero '(#.most-positive-fixnum nil . zero))
- (one '(#.most-positive-fixnum nil . one)))
+ (declare (optimize speed)
+ (type var v)
+ (type (or bit list) l h))
+ (let ((zero '(#.(floor most-positive-fixnum 2) nil . zero)) ;; TODO use nvars+1
+ (one '(#.(floor most-positive-fixnum 2) nil . one))) ;; TODO ue nvars+1
(when (typep l 'bit)
(setq l (if (zerop l) zero one)))
(when (typep h 'bit)
(setq h (if (zerop h) zero one)))
- (check-type l list)
- (check-type h list)
(cond
- ;;((zerop v) zero)
- ;;((= 1 v) one)
((eq l h) l)
(t
(rplaca k v)
@@ -57,6 +56,7 @@
;;(eq (mk 2 1 1) (mk 2 1 1))
(defun app (op u1 u2)
+ (declare (optimize speed))
(let ((g (make-hash-table :test #'equal))
(k (list nil))
(zero (mk 2 0 0))
@@ -67,7 +67,9 @@
(or (gethash k g)
(setf (gethash (cons u1 u2) g)
(destructuring-bind (v1 l1 &rest h1) u1
+ (declare (type var v1))
(destructuring-bind (v2 l2 &rest h2) u2
+ (declare (type var v2))
(cond
((and (or (eq zero u1) (eq one u1))
(or (eq zero u2) (eq one u2)))
@@ -90,14 +92,16 @@
;;(app 'or (app 'eq (mk 2 0 1) (mk 3 0 1)) (mk 4 0 1))
(defun build (exp)
+ (declare (optimize speed))
(labels ((rec (x)
(etypecase x
(bit (mk 2 x x))
- (integer
- (let ((v (abs x)))
- (if (minusp x)
- (mk v 1 0)
- (mk v 0 1))))
+ (nvar
+ (locally (declare (type fixnum x))
+ (let ((v (abs x)))
+ (if (minusp x)
+ (mk v 1 0)
+ (mk v 0 1)))))
(cons
(let ((op (car x)))
(etypecase op
@@ -117,7 +121,9 @@
(destructuring-bind (y) (cdr x)
(etypecase y
(bit (rec (if (zerop y) 1 0)))
- (integer (rec (- y)))
+ (integer
+ (locally (declare (type nvar y))
+ (rec (- y))))
(cons
(destructuring-bind (v l &rest h) (rec y)
(mk v h l))))))))))))))
@@ -155,6 +161,7 @@
;;(restrict (app 'or (app 'eq (mk 2 0 1) (mk 3 0 1)) (mk 4 0 1)) 3 0)
(defun any-sat (u &optional ones) ;; TODO expand all dont-care vars
+ (declare (optimize speed))
(let ((zero (mk 2 0 0))
(one (mk 2 1 1)))
(labels ((rec (u)
@@ -162,6 +169,7 @@
(return-from any-sat nil))
(unless (eq one u)
(destructuring-bind (v l &rest h) u
+ (declare (type var v))
(if ones
(if (eq zero h)
(cons (- v) (any-sat l))
@@ -181,7 +189,10 @@
;;(any-sat (build '(or -2 3)) t)
(defun build-n-queens (n)
+ (declare (optimize speed)
+ (type (integer 1 12345) n))
(flet ((var (i j)
+ (declare (type (integer 0 12345) i j))
(+ 2 (* i n) j)))
`(and
,@(loop ;; place a queen in each row
