		Search-engine friendly clone of the ACL2 documentation.

Z3-py

Smt-pretty-print

Pretty printer for SMT formula. Currently only change line every 160 characters.

Definitions and Theorems

Function: flatten-paragraph

(defun flatten-paragraph (p)
  (declare (xargs :guard (paragraphp p)))
  (let ((acl2::__function__ 'flatten-paragraph))
    (declare (ignorable acl2::__function__))
    (b* ((p (paragraph-fix p))
         ((if (null p)) p)
         ((if (atom p)) (list p))
         ((cons first rest) p))
      (append (flatten-paragraph first)
              (flatten-paragraph rest)))))

Theorem: word-listp-of-flatten-paragraph

(defthm word-listp-of-flatten-paragraph
  (b* ((fp (flatten-paragraph p)))
    (word-listp fp))
  :rule-classes :rewrite)

Function: pretty-print-recur

(defun pretty-print-recur (thm wlimit acc)
  (declare (xargs :guard (and (word-listp thm)
                              (natp wlimit)
                              (natp acc))))
  (let ((acl2::__function__ 'pretty-print-recur))
    (declare (ignorable acl2::__function__))
    (b* ((thm (word-list-fix thm))
         (wlimit (nfix wlimit))
         ((unless (consp thm)) nil)
         ((cons first rest) thm)
         ((if (<= wlimit acc))
          (cons first
                (cons '#\Newline
                      (pretty-print-recur rest wlimit 0)))))
      (cons first
            (pretty-print-recur rest wlimit (1+ acc))))))

Theorem: word-listp-of-pretty-print-recur

(defthm word-listp-of-pretty-print-recur
  (b* ((pretty-thm (pretty-print-recur thm wlimit acc)))
    (word-listp pretty-thm))
  :rule-classes :rewrite)

Function: pretty-print-theorem

(defun pretty-print-theorem (thm wlimit)
  (declare (xargs :guard (and (paragraphp thm) (natp wlimit))))
  (declare (xargs :guard (>= wlimit 76)))
  (let ((acl2::__function__ 'pretty-print-theorem))
    (declare (ignorable acl2::__function__))
    (b* ((thm (paragraph-fix thm))
         (fthm (flatten-paragraph thm)))
      (pretty-print-recur fthm wlimit 0))))

Theorem: word-listp-of-pretty-print-theorem

(defthm word-listp-of-pretty-print-theorem
  (b* ((pretty-thm (pretty-print-theorem thm wlimit)))
    (word-listp pretty-thm))
  :rule-classes :rewrite)