		Search-engine friendly clone of the ACL2 documentation.

Skip-detection

Sd-keylist-find-skipped

Perform skip-detection for a single pattern within an expression.

Signature
(sd-keylist-find-skipped x y ctx) → prob?
Arguments: x — Guard (sd-keylist-p x).; y — Guard (sd-keylist-p y).; ctx — Guard (vl-context1-p ctx).
Returns: prob? — Type (equal (sd-problem-p prob?) (if prob? t nil)), given the guard.

We expect that all of the keys in x and y have the same pattern. In practice, assuming the original wire names are free of * characters, this means that all keys throughout x and y should differ only by their indices. More specifically, our expectation here is that the keys in x have been generated from the wires in some particular expression, while the keys in y were generated by looking at the entire module.

Our goal is to investigate whether this expression uses "all but one" of the wires of this pattern. That is, it would be suspicious for x to mention all of foo1, foo2, foo3, and foo5, but not foo4. If there are a lot of wires in x and y, then this is a very easy comparison. The hard cases are when there aren't very many wires in the first place.

If there is only one wire that matches this pattern, then there are only two cases -- the expression mentions the wire or it doesn't -- and neither of these cases are suspicious.

If there are only two wires that share this pattern, then we might use none, one, or both of them, and none of these cases are suspicious.

If there are three wires that share this pattern, and we only use two of them, then this is starting to get slightly suspicious. We'll go ahead and flag it.

Beyond that point, if we find that exactly one wire is missing, we flag it with an alarm level equal to the number of wires that match the pattern. In other words, the alarm level is somehow like a confidence indicator that says how suspicious this omission is -- it's not too suspicious to omit one out of three wires, but it's really suspicious to omit one out of ten.

Definitions and Theorems

Function: sd-keylist-find-skipped

(defun sd-keylist-find-skipped (x y ctx)
  (declare (xargs :guard (and (sd-keylist-p x)
                              (sd-keylist-p y)
                              (vl-context1-p ctx))))
  (let ((__function__ 'sd-keylist-find-skipped))
    (declare (ignorable __function__))
    (b* ((ys (mergesort y))
         (yl (len ys))
         ((unless (> yl 2)) nil)
         (xs (mergesort x))
         (missing (difference ys xs))
         (nmissing (len missing))
         ((unless (= nmissing 1)) nil)
         (linearp (sd-keylist-linear-increments-p ys))
         (idx-min (sd-key->index (car ys)))
         (idx-max (sd-key->index (car (last ys))))
         (idx-missing (sd-key->index (car missing)))
         (middlep (and linearp (natp idx-min)
                       (natp idx-max)
                       (natp idx-missing)
                       (< idx-min idx-missing)
                       (< idx-missing idx-max)))
         (dupep (same-lengthp x ys))
         (priority (cond ((and middlep dupep) 10)
                         (middlep 6)
                         (dupep 4)
                         (linearp 2)
                         (t 1))))
      (make-sd-problem :type :skipped
                       :priority priority
                       :groupsize yl
                       :key (car missing)
                       :ctx ctx))))

Theorem: return-type-of-sd-keylist-find-skipped

(defthm return-type-of-sd-keylist-find-skipped
  (implies (and (force (sd-keylist-p x))
                (force (sd-keylist-p y))
                (force (vl-context1-p ctx)))
           (b* ((prob? (sd-keylist-find-skipped x y ctx)))
             (equal (sd-problem-p prob?)
                    (if prob? t nil))))
  :rule-classes :rewrite)