Sequential type of a logical AIG node.
Recall that AIG nodes are represented as lists like
The sequential type of such a type is just its leading keyword. The valid sequential types are:
See also combinational-type for a combinational (instead of sequential) view of AIG node types.
This is an ordinary defenum.
(defun stypep (x) (declare (xargs :guard t)) (or (eq x ':pi) (eq x ':reg) (eq x ':po) (eq x ':nxst) (eq x ':and) (eq x ':xor) (eq x ':const)))
(defthm type-when-stypep (implies (stypep x) (if (symbolp x) (if (not (equal x 't)) (not (equal x 'nil)) 'nil) 'nil)) :rule-classes :compound-recognizer)