		Search-engine friendly clone of the ACL2 documentation.

Skip-detection

Sd-problem-score

Signature
(sd-problem-score x) → score
Arguments: x — Guard (sd-problem-p x).
Returns: score — Type (natp score).

Definitions and Theorems

Function: sd-problem-score

(defun sd-problem-score (x)
  (declare (xargs :guard (sd-problem-p x)))
  (let ((__function__ 'sd-problem-score))
    (declare (ignorable __function__))
    (b* (((sd-problem x) x)
         (elem (vl-context1->elem x.ctx))
         (elem-score (cond ((eq (tag elem) :vl-assign) 1)
                           ((eq (tag elem) :vl-always) -1)
                           ((eq (tag elem) :vl-initial) -1)
                           (t 0)))
         (gs-score (cond ((< x.groupsize 4) -1)
                         ((< x.groupsize 5) 0)
                         ((< x.groupsize 8) 3)
                         ((< x.groupsize 10) 4)
                         (t 5)))
         (score (+ x.priority gs-score elem-score)))
      (nfix score))))

Theorem: natp-of-sd-problem-score

(defthm natp-of-sd-problem-score
  (b* ((score (sd-problem-score x)))
    (natp score))
  :rule-classes :type-prescription)