		Search-engine friendly clone of the ACL2 documentation.

Node

Node-p

Recognizer for node structures.

Signature
(node-p x) → *

Definitions and Theorems

Function: node-p

(defun node-p (x)
  (declare (xargs :guard t))
  (let ((__function__ 'node-p))
    (declare (ignorable __function__))
    (cond ((or (atom x)
               (not (stypep (car x)))
               (eq (car x) :const))
           (and (eq x nil) (b* nil t)))
          ((eq (car x) :pi)
           (and (not (cdr x)) (b* nil t)))
          ((eq (car x) :reg)
           (and (not (cdr x)) (b* nil t)))
          ((eq (car x) :and)
           (and (true-listp x)
                (eql (len x) 3)
                (b* ((fanin0 (cadr x)) (fanin1 (caddr x)))
                  (and (litp fanin0) (litp fanin1)))))
          ((eq (car x) :xor)
           (and (true-listp x)
                (eql (len x) 3)
                (b* ((fanin0 (cadr x)) (fanin1 (caddr x)))
                  (and (litp fanin0) (litp fanin1)))))
          ((eq (car x) :po)
           (and (true-listp x)
                (eql (len x) 2)
                (b* ((fanin (cadr x))) (litp fanin))))
          ((eq (car x) :nxst)
           (and (true-listp x)
                (eql (len x) 3)
                (b* ((fanin (cadr x)) (reg (caddr x)))
                  (and (litp fanin) (natp reg))))))))