		Search-engine friendly clone of the ACL2 documentation.

Arity-reasoning

Rules for reasoning about how many arguments an expression has.

These rules have evolved a lot over time. The current iteration seems to be fairly good and fixes some problems with previous versions.

One previous approach was just to separately recognize each unary, binary, and ternary operator, e.g.,

(implies (and (or (equal (vl-nonatom->op x) :vl-unary-plus)
                  (equal (vl-nonatom->op x) :vl-unary-minus)
                  ...)
             ...)
         (and (vl-nonatom->args x)
              ...))

These rules seemed to be pretty effective, but they were slow. To fix the slowness, I tried using a free variable to only apply the rule when the op was exactly known, e.g.,

(implies (and (equal (vl-nonatom->op x) op)
              (<= (vl-op-arity op) 1)
              ...)
         (and (vl-nonatom->args x)
              ...))

This did seem to be quite a bit faster and also seemed to wrok well when the operands were known precisely. But it did not handle cases like VL-HIDEXPR-P very well, where if we know

(not (equal (vl-nonatom->op x) :vl-hid-dot))

then we should be able to infer that this is a :vl-hid-arraydot. I had trouble getting ACL2 to always canonicalize such things the "positive" form.

The new rules don't have a free variable, but still avoid the big case split. We don't ask about particular operands, but instead just ask whether the arity is known. This works and should be pretty efficient when a direct equality is known, e.g., if we know

(equal (vl-nonatom->op x) :vl-binary-times),

then we'll backchain to (vl-op-arity (vl-nonatom->op x)), which type-set should settle to (vl-op-arity :vl-binary-times) and which we should then get by evaluation.

But since there isn't a free variable, we'll also get a chance to apply any rules that tell us what the arity is in some other way, which allows us to fairly easily solve the HIDEXPR problem.

Definitions and Theorems

Theorem: arg1-exists-by-arity

(defthm arg1-exists-by-arity
  (let ((arity (vl-op-arity (vl-nonatom->op x))))
    (implies arity
             (and (implies (<= 1 arity)
                           (vl-nonatom->args x))
                  (iff (first (vl-nonatom->args x))
                       (<= 1 arity))
                  (equal (consp (vl-nonatom->args x))
                         (<= 1 arity))))))

Theorem: arg2-exists-by-arity

(defthm arg2-exists-by-arity
  (let ((arity (vl-op-arity (vl-nonatom->op x))))
    (implies arity
             (and (implies (<= 2 arity)
                           (cdr (vl-nonatom->args x)))
                  (iff (second (vl-nonatom->args x))
                       (<= 2 arity))
                  (equal (consp (cdr (vl-nonatom->args x)))
                         (<= 2 arity))))))

Theorem: arg3-exists-by-arity

(defthm arg3-exists-by-arity
  (let ((arity (vl-op-arity (vl-nonatom->op x))))
    (implies arity
             (and (implies (<= 3 arity)
                           (cddr (vl-nonatom->args x)))
                  (iff (third (vl-nonatom->args x))
                       (<= 3 arity))
                  (equal (consp (cddr (vl-nonatom->args x)))
                         (<= 3 arity))))))