Pretty-print an expression into a string.
This pretty-prints an expression "as is," i.e., in its current, possibly transformed state. Depending on what you're trying to do, it may be better to use vl-pps-origexpr instead, which tries to print the "original," pre-transformed version of the expression, as it occurred in the real Verilog file.
(defun vl-pps-expr (x) (declare (xargs :guard (vl-expr-p x))) (let ((__function__ 'vl-pps-expr)) (declare (ignorable __function__)) (with-local-ps (vl-pp-expr x))))
(defthm stringp-of-vl-pps-expr (b* ((pretty-x (vl-pps-expr x))) (stringp pretty-x)) :rule-classes :type-prescription)
(defthm vl-pps-expr-of-vl-expr-fix-x (equal (vl-pps-expr (vl-expr-fix x)) (vl-pps-expr x)))
(defthm vl-pps-expr-vl-expr-equiv-congruence-on-x (implies (vl-expr-equiv x x-equiv) (equal (vl-pps-expr x) (vl-pps-expr x-equiv))) :rule-classes :congruence)