		Search-engine friendly clone of the ACL2 documentation.

Trusted

Smt-write

SMT-write writes out the translated string to a SMT file as configured.

Definitions and Theorems

Function: princ$-paragraph

(defun princ$-paragraph (par channel state)
  (declare (xargs :stobjs (state)))
  (declare (xargs :guard (and (paragraphp par)
                              (symbolp channel))))
  (declare (xargs :guard (open-output-channel-p channel
                                                :character state)
                  :stobjs state))
  (let ((acl2::__function__ 'princ$-paragraph))
    (declare (ignorable acl2::__function__))
    (b* ((par (paragraph-fix par))
         (channel (symbol-fix channel))
         ((unless (consp par))
          (if (equal par nil)
              state
            (princ$ par channel state)))
         ((cons first rest) par)
         (state (princ$-paragraph first channel state)))
      (princ$-paragraph rest channel state))))

Theorem: open-output-channel-p1-of-princ$-paragraph

(defthm open-output-channel-p1-of-princ$-paragraph
  (implies (and (state-p1 state)
                (symbolp channel)
                (open-output-channel-p1 channel
                                        :character state))
           (let ((state (princ$-paragraph par channel state)))
             (and (state-p1 state)
                  (open-output-channel-p1 channel
                                          :character state)))))

Function: smt-write-file

(defun smt-write-file (fname acl22smt smt-head thm state)
  (declare (xargs :stobjs (state)))
  (declare (xargs :guard (and (stringp fname)
                              (paragraphp acl22smt)
                              (paragraphp smt-head)
                              (paragraphp thm))))
  (let ((acl2::__function__ 'smt-write-file))
    (declare (ignorable acl2::__function__))
    (b* ((fname (str-fix fname))
         (acl22smt (paragraph-fix acl22smt))
         ((mv channel state)
          (open-output-channel! fname
                                :character state))
         ((unless channel)
          (er hard? 'smt-write=>smt-write-file
              "Can't open file ~q0 as SMT file."
              fname)
          state)
         (state (princ$-paragraph acl22smt channel state))
         (state (princ$-paragraph smt-head channel state))
         (state (princ$-paragraph thm channel state)))
      (close-output-channel channel state))))