Commit [d5aaca] Maximize Restore History

progress in structuring bitvec sets, dumb implementation started

Utz-Uwe Haus Utz-Uwe Haus 2007-09-16

added clause.lisp
added oracles.lisp
changed jg.lisp
changed jointgen.asd
changed package.lisp
copied jg-bitops.lisp -> clause-sets.lisp
clause.lisp Diff Switch to side-by-side view
Loading...
oracles.lisp Diff Switch to side-by-side view
Loading...
jg.lisp Diff Switch to side-by-side view
Loading...
jointgen.asd Diff Switch to side-by-side view
Loading...
package.lisp Diff Switch to side-by-side view
Loading...
jg-bitops.lisp to clause-sets.lisp
--- a/jg-bitops.lisp
+++ b/clause-sets.lisp
@@ -20,66 +20,112 @@
 ;;;; Foundation, Inc., 675 Mass Ave, Cambridge, MA 02139, USA.
 ;;;; ********************************************************************
 
-;;; Bit-operations on jg-vec structures.
-;;; The goal is to have this file compiled at (safety 0), since all routines
-;;; are performance-critical
+;;; Container for clauses
+;;; Conceptionally these are just sets of bit-vectors that are all
+;;; pairwise incomparable under subsetness (as tested by #'clause-contains)
+
+;;; Potentially we want to have a cheap way to compute subsets of a container
+;;; when masking out a column (think of deleting it), or by selecting all elements
+;;; that have a common entry in a column.
+;;; Red-Black-Trees with persistence would solve this. We only need the 'deletion'
+;;; persistence, actually, to rollback the deletion of nodes after masking/selecting
+;;; For now, we just do full copies
+
 (eval-when (:compile-toplevel :load-toplevel :execute)
   (declaim 
    (optimize (speed 1) (debug 3) (safety 3))
-   ;   (optimize (speed 3) (debug 3) (space 0) (safety 0))
-   ;   (:explain :types :boxing :variables :tailmerging :inlining)
    ))
 
 (in-package #:DE.UUHAUS.JOINTGEN)
 
-(defun get-nzcnt (v)
-  "Return (the hopefully cached) nzcnt of V"
-  (declare (type jg-vec v)
-	   (optimize (speed 3) (safety 0))
-	   )
-  (let ((res (jg-vec-nzcnt v)))
-    (if res
-	res
-	(setf (jg-vec-nzcnt v) (logcount (jg-vec-bitvec v))))))
+(defstruct clutter
+  "Representatation of a clutter of clauses"
+  ;; the raw data -- contents only grows
+  (data (make-array 0 :element-type 'clause :adjustable T :fill-pointer 0) :type (vector clause))
+  ;; the live elements of DATA in the current state
+  ;; TODO: use something better than a list here (e.g. RBT)
+  (live-mask (make-0-clause) :type 'clause)   ;; the variables to be out-masked as in c1 ANDC mask
+  (live-data '() :type list)                  ;; the surviving clauses (indices into data slot)
+  (live-data-size 0 :type (integer 0 #.ARRAY-DIMENSION-LIMIT)) ;; count of them
+  ;; stack of old versions of live-data: each entry is a 3-element list of data, mask and size suitable for the above two slots
+  ;; if this is empty we allow addition to the data slot, otherwise it is blocked
+  (live-data-stack '() :type list))
 
-(declaim (ftype (function (jg-vec fixnum) (member 0 1)) get-bit))
-(defun get-bit (v n)
-  "Return the Nth bit of V, as fixnum 0 or 1"
-  (declare (type fixnum n)
-	   (type jg-vec v))
-  (if (logbitp n (jg-vec-bitvec v)) 1 0))
+
+(defun store-clause/no-check (clutter clause)
+  "Store CLAUSE in BITVECSET, without checking subsetness."
+  (cond
+    ((null (clutter-live-data-stack clutter))
+     (error "Attempt to modify clutter with live subset view(s): ~A" clutter))
+    (T
+     (let ((new-idx (vector-push-extend clause (clutter-data clutter))))
+       (push new-idx (clutter-live-data clutter))
+       (incf (clutter-live-data-size clutter))))))
 
-(declaim (ftype (function (jg-vec fixnum) null) set-bit))
-(defun set-bit (v n)
-  "Set the Nth bit of V"
-  (declare (type fixnum n)
-	   (type jg-vec v))
-  (unless (logbitp n (jg-vec-bitvec v))
-    (setf (ldb (byte 1 n) (jg-vec-bitvec v)) 1)
-    (incf (jg-vec-nzcnt v)))
-  (values))
+
+;;; creating subset views
 
-(declaim (ftype (function (jg-vec fixnum) null) clear-bit))
-(defun clear-bit (v n)
-  "Set the Nth bit of V"
-  (declare (type fixnum n)
-	   (type jg-vec v))
-  (when (logbitp n (jg-vec-bitvec v))
-    (setf (ldb (byte 1 n) (jg-vec-bitvec v)) 0)
-    (decf (jg-vec-nzcnt v)))
-  (values))
+(defun restrict-clutter/select-0-at-idx (clutter idx)
+  "Restrict the live data of CLUTTER to all clauses of the current live data that have a 0 in variable index IDX."
+  ;; save current state
+  (with-slots (live-mask live-data live-data-size)
+      clutter
+    (push `(,live-data ,live-mask ,live-data-size)
+	  (clutter-live-data-stack clutter))
+    ;; build new view:
+    ;; mask IDX
+    (setf live-mask (clause-set-bit (copy-clause live-mask) idx))
+    ;; clean
+    (multiple-value-bind (survivors count)
+	(loop for c1 in live-data
+	      when (error "fix this"  (find-if #'(lambda (c2) (unless 1) (clause-contains/mask c1 c2 live-mask)) live-data))
+	      collect c1 into data
+	      counting c1 into num
+	      finally (return (values data num)))
+      (setf live-data survivors
+	    live-data-size count))
+    clutter))
+
+(defun restrict-clutter/ignore-idx (clutter idx)
+  "Restrict the live data of CLUTTER to all clauses of the current live data, ignoring the variable at index IDX."
+  ;; save current state
+  (push `(,(clutter-live-data clutter) ,(clutter-live-mask clutter) ,(clutter-live-data-size clutter))
+	(clutter-live-data-stack clutter))
+  ;; build new view
+  (error "implement me"))
+
+(defun pop-live-data-stack (clutter)
+  "Remove last level of restriction of CLUTTER."
+  ;; fetch previous state
+  (cond
+    ((null (clutter-live-data-stack clutter))
+     (error "trying to pop from empty live-data-stack"))
+    (T
+     (destructuring-bind (data mask size)
+	 (pop (clutter-live-data-stack clutter))
+       (setf (clutter-live-data clutter) data
+	     (clutter-live-mask clutter) mask	     
+	     (clutter-live-data-size clutter) size)))))
+
+(defmacro with-restricted-clauses/0-at-idx ((c idx) &body body)
+  "Execute BODY while clutter C is restricted to the clauses having variable at IDX = 0"
+  (let ((clutter (gensym "idx-selected-clutter")))
+    `(let ((,clutter ,c))
+      (unwind-protect 
+	   (progn
+	     (restrict-clutter/select-0-at-idx ,clutter ,idx)
+	     ,@body)
+	(pop-live-data-stack ,clutter)))))
+
+(defmacro with-restricted-clauses/dropping-idx ((c idx) &body body)
+  "Execute BODY while clutter C is restricted by forgetting the differences at IDX = 0"
+  (let ((clutter (gensym "idx-dropped-clutter")))
+    `(let ((,clutter ,c))
+      (unwind-protect 
+	   (progn
+	     (restrict-clutter/ignore-idx ,clutter ,idx)
+	     ,@body)
+	(pop-live-data-stack ,clutter)))))
 
 
-(defun jg-vec-equal (v1 v2)
-  "Check v1 and v2 for equality"
-  (= (jg-vec-bits v1) (jg-vec-bits v2)))
 
-(defun jg-vec-contains (v1 v2)
-  "Check whether V1 contains V2 (as bit-superset)"
-  (declare (optimize (safety 0) (speed 3)))
-  (let ((v1-int (jg-vec-bits v1)))
-    (= v1-int (logand v1-int (jg-vec-bits v2)))))
-
-(defun jg-vec-contained (v1 v2)
-  "Check whether V1 is contained in V2 (as bit-subset)"
-  (jg-vec-contains v2 v1))