Filtering...

lrat-parser

books/projects/sat/lrat/stobj-based/lrat-parser
other
(in-package "LRAT")
other
(include-book "std/util/bstar" :dir :system)
other
(include-book "limits")
other
(include-book "lrat-checker")
!macro
(defmacro !
  (x y)
  (declare (xargs :guard (symbolp x)))
  `(assign ,LRAT::X ,LRAT::Y))
!!macro
(defmacro !!
  (variable new-value)
  (declare (xargs :guard t))
  `(mv-let (erp result state)
    (assign ,VARIABLE ,LRAT::NEW-VALUE)
    (declare (ignore result))
    (value (if erp
        'error!
        ',VARIABLE))))
other
(set-state-ok t)
firstnfunction
(defun firstn
  (n x)
  (declare (xargs :guard (natp n)))
  (if (atom x)
    nil
    (if (mbe :logic (zp n) :exec (<= n 0))
      nil
      (cons (car x)
        (firstn (1- n) (cdr x))))))
other
(defthm integer-listp-firstn
  (implies (integer-listp l)
    (integer-listp (firstn n l))))
other
(defthm integer-listp-nth-cdr
  (implies (integer-listp l)
    (integer-listp (nthcdr s l))))
my-rev1function
(defun my-rev1
  (x a)
  (declare (xargs :guard (true-listp a)))
  (if (atom x)
    a
    (my-rev1 (cdr x) (cons (car x) a))))
other
(defthm true-listp-my-rev1
  (implies (true-listp a)
    (true-listp (my-rev1 x a))))
other
(defthm nat-listp-my-rev1
  (implies (and (nat-listp x) (nat-listp a))
    (nat-listp (my-rev1 x a))))
other
(defthm integer-listp-my-rev1
  (implies (and (integer-listp x)
      (integer-listp a))
    (integer-listp (my-rev1 x a))))
my-revfunction
(defun my-rev
  (x)
  (declare (xargs :guard t))
  (if (atom x)
    nil
    (my-rev1 x nil)))
other
(defthm true-listp-my-rev
  (true-listp (my-rev x)))
other
(defthm nat-listp-my-rev
  (implies (nat-listp x)
    (nat-listp (my-rev x))))
other
(defthm integer-listp-my-rev
  (implies (integer-listp x)
    (integer-listp (my-rev x))))
other
(in-theory (disable my-rev))
other
(defun-inline char-to-nat
  (ch)
  (declare (xargs :guard (characterp ch)))
  (let ((code (u59 (char-code ch))))
    (and (>= code 48)
      (<= code 57)
      (- code 48))))
other
(defthm natp-or-null-char-to-nat
  (or (natp (char-to-nat ch))
    (null (char-to-nat ch)))
  :rule-classes :type-prescription)
other
(defthm natp-char-to-nat
  (implies (char-to-nat ch)
    (natp (char-to-nat ch))))
other
(defthm char-to-nat-is-less-than-10
  (implies (char-to-nat ch)
    (< (char-to-nat ch) 10))
  :rule-classes :linear)
other
(in-theory (disable char-to-nat))
lrat-guardfunction
(defun lrat-guard
  (str len pos)
  (declare (xargs :guard t))
  (and (stringp str)
    (natp pos)
    (natp len)
    (equal len (length str))
    (< pos len)
    (< len 72057594037927936)))
lrat-flg-nat1function
(defun lrat-flg-nat1
  (str len pos n)
  (declare (xargs :guard (and (lrat-guard str len pos)
        (natp n)
        (< n *2^56*))
      :measure (nfix (- len pos))))
  (let* ((len (u56 len)) (pos (u56 pos))
      (n (u56 n))
      (ch (char str pos))
      (digit (char-to-nat ch)))
    (if (null digit)
      (mv pos n)
      (let ((pos+1 (u59 (1+ pos))))
        (if (mbe :logic (zp (- len pos+1))
            :exec (>= pos+1 len))
          (mv nil 0)
          (if (not (< n 4503599627370496))
            (mv nil 0)
            (let* ((10n+digit (u56 (+ (u04 digit) (u56 (* n 10))))))
              (lrat-flg-nat1 str
                len
                pos+1
                10n+digit))))))))
other
(defthm integerp-lrat-flg-nat1
  (implies (and (natp pos)
      (car (lrat-flg-nat1 str len pos n)))
    (integerp (car (lrat-flg-nat1 str len pos n))))
  :hints (("Goal" :in-theory (disable length)
     :induct (lrat-flg-nat1 str len pos n))))
other
(defthm natp-lrat-flg-nat1
  (implies (and (natp pos)
      (car (lrat-flg-nat1 str len pos n)))
    (<= 0
      (car (lrat-flg-nat1 str len pos n))))
  :hints (("Goal" :in-theory (disable length)
     :induct (lrat-flg-nat1 str len pos n)))
  :rule-classes :linear)
other
(defthm pos-has-increased-lrat-flg-nat1
  (implies (and (char-to-nat (char str pos))
      (car (lrat-flg-nat1 str len pos n)))
    (< pos
      (car (lrat-flg-nat1 str len pos n)))))
other
(defthm pos-has-increased-lrat-flg-nat1-1
  (implies (and (char-to-nat (char str pos1))
      (natp pos)
      (<= pos pos1)
      (car (lrat-flg-nat1 str len pos1 n)))
    (< pos
      (car (lrat-flg-nat1 str len pos1 n)))))
other
(defthm car-lrat-flag-nat1-less-than-len
  (implies (and (lrat-guard str len pos)
      (car (lrat-flg-nat1 str len pos n)))
    (< (car (lrat-flg-nat1 str len pos n))
      len))
  :hints (("Goal" :in-theory (disable length)
     :induct (lrat-flg-nat1 str len pos n))))
other
(encapsulate nil
  (local (defthm mv-nth-1-natp-lrat-flg-nat1
      (implies (and (natp n)
          (car (lrat-flg-nat1 str len pos n)))
        (natp (mv-nth 1
            (lrat-flg-nat1 str len pos n))))))
  (defthm integerp-mv-nth-1-natp-lrat-flg-nat1
    (implies (and (natp n)
        (car (lrat-flg-nat1 str len pos n)))
      (integerp (mv-nth 1
          (lrat-flg-nat1 str len pos n)))))
  (defthm ge-0-mv-nth-1-natp-lrat-flg-nat1
    (implies (and (natp n)
        (car (lrat-flg-nat1 str len pos n)))
      (<= 0
        (mv-nth 1
          (lrat-flg-nat1 str len pos n))))))
other
(defthm mv-nth1-lrat-flg-nat1-less-than-*2^56*
  (implies (and (natp n)
      (< n *2^56*)
      (car (lrat-flg-nat1 str len pos n)))
    (< (mv-nth 1
        (lrat-flg-nat1 str len pos n))
      *2^56*))
  :hints (("Goal" :in-theory (disable length)
     :induct (lrat-flg-nat1 str len pos n))))
other
(in-theory (disable lrat-flg-nat1))
lrat-flg-natfunction
(defun lrat-flg-nat
  (str len pos)
  (declare (xargs :guard (lrat-guard str len pos)))
  (b* ((ch (char str pos)) ((unless (char-to-nat ch)) (mv nil 0)))
    (lrat-flg-nat1 str len pos 0)))
other
(defthm integerp-lrat-flg-nat
  (implies (and (natp pos)
      (car (lrat-flg-nat str len pos)))
    (integerp (car (lrat-flg-nat str len pos))))
  :hints (("Goal" :in-theory (disable length))))
other
(defthm natp-lrat-flg-nat
  (implies (and (natp pos)
      (car (lrat-flg-nat str len pos)))
    (<= 0
      (car (lrat-flg-nat str len pos))))
  :hints (("Goal" :in-theory (disable length)))
  :rule-classes :linear)
other
(defthm pos-has-increased-lrat-flg-nat
  (implies (car (lrat-flg-nat str len pos))
    (< pos
      (car (lrat-flg-nat str len pos)))))
other
(defthm pos-has-increased-lrat-flg-nat-1
  (implies (and (natp pos)
      (<= pos pos1)
      (car (lrat-flg-nat str len pos1)))
    (< pos
      (car (lrat-flg-nat str len pos1)))))
other
(defthm car-lrat-flag-nat-less-than-len
  (implies (and (lrat-guard str len pos)
      (car (lrat-flg-nat str len pos)))
    (< (car (lrat-flg-nat str len pos))
      len)))
other
(encapsulate nil
  (local (defthm mv-nth-1-natp-lrat-flg-nat
      (implies (car (lrat-flg-nat str len pos))
        (natp (mv-nth 1
            (lrat-flg-nat str len pos))))))
  (defthm integerp-mv-nth-1-lrat-flg-nat
    (implies (car (lrat-flg-nat str len pos))
      (integerp (mv-nth 1
          (lrat-flg-nat str len pos))))
    :rule-classes :type-prescription :hints (("Goal" :in-theory (disable mv-nth lrat-flg-nat)
       :use ((:instance mv-nth-1-natp-lrat-flg-nat
          (str str)
          (len len)
          (pos pos))))))
  (defthm ge-0-mv-nth-1-lrat-flg-nat
    (implies (car (lrat-flg-nat str len pos))
      (<= 0
        (mv-nth 1
          (lrat-flg-nat str len pos))))
    :rule-classes :linear :hints (("Goal" :in-theory (disable mv-nth lrat-flg-nat)
       :use ((:instance mv-nth-1-natp-lrat-flg-nat
          (str str)
          (len len)
          (pos pos)))))))
other
(defthm mv-nth1-lrat-flg-nat-less-than-*2^56*
  (implies (car (lrat-flg-nat str len pos))
    (< (mv-nth 1
        (lrat-flg-nat str len pos))
      *2^56*)))
other
(in-theory (disable lrat-flg-nat))
lrat-flg-intfunction
(defun lrat-flg-int
  (str len pos)
  (declare (xargs :guard (lrat-guard str len pos)))
  (b* ((ch (char str pos)))
    (if (eql ch #\-)
      (b* ((pos (u56 pos)) (len (u56 len))
          (pos+1 (u59 (1+ pos)))
          ((unless (< pos+1 len)) (mv nil 0))
          ((mv pos-after-nat num) (lrat-flg-nat str len pos+1))
          ((unless pos-after-nat) (mv nil 0))
          (num (u56 num)))
        (mv pos-after-nat (- num)))
      (lrat-flg-nat str len pos))))
other
(defthm integerp-lrat-flg-int
  (implies (and (natp pos)
      (car (lrat-flg-nat str len pos)))
    (integerp (car (lrat-flg-nat str len pos))))
  :hints (("Goal" :in-theory (disable length))))
other
(defthm natp-lrat-flg-int
  (implies (and (natp pos)
      (car (lrat-flg-int str len pos)))
    (<= 0
      (car (lrat-flg-int str len pos))))
  :hints (("Goal" :in-theory (disable length)))
  :rule-classes :linear)
other
(defthm pos-has-increased-lrat-flg-int-1
  (implies (and (natp pos)
      (<= pos pos1)
      (car (lrat-flg-int str len pos1)))
    (< pos
      (car (lrat-flg-int str len pos1)))))
other
(defthm car-lrat-flag-int-less-than-len
  (implies (and (lrat-guard str len pos)
      (or (car (lrat-flg-int str len pos))
        (integerp (lrat-flg-int str len pos))))
    (< (car (lrat-flg-int str len pos))
      len)))
other
(defthm mv-nth-1-natp-lrat-flg-int
  (implies (car (lrat-flg-int str len pos))
    (integerp (mv-nth 1
        (lrat-flg-int str len pos))))
  :rule-classes (:rewrite :type-prescription))
other
(encapsulate nil
  (local (defthm one-time-math-fact
      (implies (and (integerp i) (integerp n))
        (iff (< (- i) (- n)) (< n i)))
      :rule-classes ((:rewrite :corollary (implies (and (integerp i) (integerp n))
           (equal (< (- i) (- n)) (< n i)))))))
  (defthm mv-nth1-lrat-flg-int-abs-less-than-*2^56*
    (implies (car (lrat-flg-int str len pos))
      (and (< (- *2^56*)
          (mv-nth 1
            (lrat-flg-int str len pos)))
        (< (mv-nth 1
            (lrat-flg-int str len pos))
          *2^56*)))
    :hints (("Goal" :do-not-induct t))))
other
(in-theory (disable lrat-flg-int))
lrat-flg-pos-skip-spacesfunction
(defun lrat-flg-pos-skip-spaces
  (str len pos)
  (declare (xargs :guard (lrat-guard str len pos)
      :measure (nfix (- len pos))))
  (b* ((ch (char str pos)) ((when (not (eql ch #\ ))) pos)
      (len (u56 len))
      (pos (u56 pos))
      (pos+1 (u56 (1+ pos))))
    (if (mbe :logic (zp (- len pos+1))
        :exec (>= pos+1 len))
      pos
      (lrat-flg-pos-skip-spaces str
        len
        pos+1))))
other
(encapsulate nil
  (local (defthm natp-lrat-flg-pos-skip-spaces
      (implies (natp pos)
        (natp (lrat-flg-pos-skip-spaces str
            len
            pos)))))
  (defthm integerp-lrat-flg-pos-skip-spaces
    (implies (integerp pos)
      (integerp (lrat-flg-pos-skip-spaces str
          len
          pos)))
    :rule-classes :type-prescription)
  (defthm ge-0-lrat-flg-pos-skip-spaces
    (implies (natp pos)
      (<= 0
        (lrat-flg-pos-skip-spaces str
          len
          pos)))
    :rule-classes (:rewrite :linear)))
other
(defthm pos-fact-lrat-flg-pos-skip-spaces
  (<= pos
    (lrat-flg-pos-skip-spaces str
      len
      pos))
  :rule-classes (:rewrite :linear))
other
(defthm lrat-flg-pos-skip-spaces-<-length-str
  (implies (lrat-guard str len pos)
    (< (lrat-flg-pos-skip-spaces str
        len
        pos)
      len))
  :hints (("Goal" :in-theory (enable nth)
     :induct (lrat-flg-pos-skip-spaces len pos n))))
other
(defthm lrat-flg-pos-skip-spaces-<-*2^56*
  (implies (and (equal limit *2^56*)
      (lrat-guard str len pos))
    (< (lrat-flg-pos-skip-spaces str
        len
        pos)
      limit))
  :hints (("Goal" :in-theory (enable nth)
     :induct (lrat-flg-pos-skip-spaces len pos n))))
other
(in-theory (disable lrat-flg-pos-skip-spaces))
lrat-flg-nat-list-until-0function
(defun lrat-flg-nat-list-until-0
  (str len pos lst cnt)
  (declare (xargs :guard (and (lrat-guard str len pos)
        (true-listp lst)
        (natp cnt)
        (<= cnt len))
      :guard-hints (("Goal" :in-theory (disable length car-lrat-flag-nat-less-than-len)
         :use ((:instance car-lrat-flag-nat-less-than-len
            (str str)
            (len (length str))
            (pos (lrat-flg-pos-skip-spaces str
                (length str)
                pos))))))
      :measure (acl2-count cnt)))
  (b* ((pos (u59 pos)) (pos-after-spaces (lrat-flg-pos-skip-spaces str
          len
          pos))
      ((unless (integerp pos-after-spaces)) (mv nil nil))
      (pos-after-spaces (u56 pos-after-spaces))
      ((mv pos-after-nat nat-read) (lrat-flg-nat str
          len
          pos-after-spaces))
      ((unless (integerp pos-after-nat)) (mv nil nil))
      (pos-after-nat (u59 pos-after-nat))
      (nat-read (u56 nat-read))
      ((if (= nat-read 0)) (mv pos-after-nat (my-rev lst)))
      ((unless (< pos pos-after-nat)) (mv nil nil))
      (len (u59 len))
      (cnt (u59 cnt))
      (cnt-1 (1- cnt)))
    (if (mbe :logic (zp cnt)
        :exec (<= cnt 0))
      (mv nil nil)
      (lrat-flg-nat-list-until-0 str
        len
        pos-after-nat
        (cons nat-read lst)
        cnt-1))))
other
(defthm integerp-lrat-flg-nat-list-until-0
  (implies (and (natp pos)
      (car (lrat-flg-nat-list-until-0 str
          len
          pos
          lst
          cnt)))
    (integerp (car (lrat-flg-nat-list-until-0 str
          len
          pos
          lst
          cnt))))
  :hints (("Goal" :in-theory (disable length))))
other
(defthm natp-lrat-flg-nat-list-until-0
  (implies (and (natp pos)
      (car (lrat-flg-nat-list-until-0 str
          len
          pos
          lst
          cnt)))
    (<= 0
      (car (lrat-flg-nat-list-until-0 str
          len
          pos
          lst
          cnt))))
  :hints (("Goal" :in-theory (disable length)))
  :rule-classes :linear)
other
(defthm pos-has-increased-lrat-flg-nat-list-until-0
  (implies (and (natp pos)
      (<= pos pos1)
      (car (lrat-flg-nat-list-until-0 str
          len
          pos1
          lst
          cnt)))
    (< pos
      (car (lrat-flg-nat-list-until-0 str
          len
          pos1
          lst
          cnt)))))
other
(defthm nat-listp-lrat-flg-nat-list-until-0
  (implies (nat-listp lst)
    (nat-listp (mv-nth 1
        (lrat-flg-nat-list-until-0 str
          len
          pos
          lst
          cnt)))))
other
(in-theory (disable lrat-flg-nat-list-until-0))
lrat-flg-int-list-until-0function
(defun lrat-flg-int-list-until-0
  (str len pos lst cnt)
  (declare (xargs :guard (and (lrat-guard str len pos)
        (true-listp lst)
        (natp cnt)
        (<= cnt len))
      :guard-hints (("Goal" :in-theory (disable length car-lrat-flag-int-less-than-len)
         :use ((:instance car-lrat-flag-int-less-than-len
            (str str)
            (len (length str))
            (pos (lrat-flg-pos-skip-spaces str
                (length str)
                pos))) (:instance mv-nth1-lrat-flg-int-abs-less-than-*2^56*
             (str str)
             (len (length str))
             (pos (lrat-flg-pos-skip-spaces str
                 (length str)
                 pos))))))
      :measure (acl2-count cnt)))
  (b* ((pos (u59 pos)) (pos-after-spaces (lrat-flg-pos-skip-spaces str
          len
          pos))
      ((unless (integerp pos-after-spaces)) (mv nil nil))
      (pos-after-spaces (u56 pos-after-spaces))
      ((mv pos-after-int int-read) (lrat-flg-int str
          len
          pos-after-spaces))
      ((unless (integerp pos-after-int)) (mv nil nil))
      (pos-after-int (u59 pos-after-int))
      (int-read (s57 int-read))
      ((if (= int-read 0)) (mv pos-after-int (my-rev lst)))
      (len (u59 len))
      (cnt (u59 cnt))
      (cnt-1 (1- cnt)))
    (if (mbe :logic (zp cnt)
        :exec (<= cnt 0))
      (mv nil nil)
      (lrat-flg-int-list-until-0 str
        len
        pos-after-int
        (cons int-read lst)
        cnt-1))))
other
(defthm integerp-lrat-flg-int-list-until-0
  (implies (and (natp pos)
      (car (lrat-flg-int-list-until-0 str
          len
          pos
          lst
          cnt)))
    (integerp (car (lrat-flg-int-list-until-0 str
          len
          pos
          lst
          cnt))))
  :hints (("Goal" :in-theory (disable length))))
other
(defthm natp-lrat-flg-int-list-until-0
  (implies (and (natp pos)
      (car (lrat-flg-int-list-until-0 str
          len
          pos
          lst
          cnt)))
    (<= 0
      (car (lrat-flg-int-list-until-0 str
          len
          pos
          lst
          cnt))))
  :hints (("Goal" :in-theory (disable length)))
  :rule-classes :linear)
other
(defthm int-listp-lrat-flg-int-list-until-0
  (implies (integer-listp lst)
    (integer-listp (mv-nth 1
        (lrat-flg-int-list-until-0 str
          len
          pos
          lst
          cnt)))))
lrat-flg-int-list-until-0-or--function
(defun lrat-flg-int-list-until-0-or--
  (str len pos lst cnt)
  (declare (xargs :guard (and (lrat-guard str len pos)
        (true-listp lst)
        (natp cnt)
        (<= cnt len))
      :guard-hints (("Goal" :in-theory (disable length car-lrat-flag-int-less-than-len)
         :use ((:instance car-lrat-flag-int-less-than-len
            (str str)
            (len (length str))
            (pos (lrat-flg-pos-skip-spaces str
                (length str)
                pos))) (:instance mv-nth1-lrat-flg-int-abs-less-than-*2^56*
             (str str)
             (len (length str))
             (pos (lrat-flg-pos-skip-spaces str
                 (length str)
                 pos))))))
      :measure (acl2-count cnt)))
  (b* ((pos (u59 pos)) (pos-after-spaces (lrat-flg-pos-skip-spaces str
          len
          pos))
      ((unless (integerp pos-after-spaces)) (mv nil nil))
      (pos-after-spaces (u56 pos-after-spaces))
      (ch (char str pos-after-spaces))
      ((if (eql #\- ch)) (b* ((pos-after-spaces+1 (1+ (u56 pos-after-spaces))))
          (if (not (and (< pos pos-after-spaces+1)
                (< pos-after-spaces+1 len)))
            (mv pos nil)
            (mv pos-after-spaces+1 (my-rev lst)))))
      ((mv pos-after-int int-read) (lrat-flg-int str
          len
          pos-after-spaces))
      ((unless (integerp pos-after-int)) (mv nil nil))
      (len (u59 len))
      ((unless (< pos-after-int len)) (mv nil nil))
      (pos-after-int (u59 pos-after-int))
      (int-read (s57 int-read))
      ((if (= int-read 0)) (mv pos-after-int (my-rev lst)))
      (cnt (u59 cnt))
      (cnt-1 (1- cnt)))
    (if (mbe :logic (zp cnt)
        :exec (<= cnt 0))
      (mv nil nil)
      (lrat-flg-int-list-until-0-or-- str
        len
        pos-after-int
        (cons int-read lst)
        cnt-1))))
other
(defthm integerp-lrat-flg-int-list-until-0-or--
  (implies (and (natp pos)
      (car (lrat-flg-int-list-until-0-or-- str
          len
          pos
          lst
          cnt)))
    (integerp (car (lrat-flg-int-list-until-0-or-- str
          len
          pos
          lst
          cnt))))
  :hints (("Goal" :in-theory (disable length))))
other
(defthm natp-lrat-flg-int-list-until-0-or--
  (implies (and (natp pos)
      (car (lrat-flg-int-list-until-0-or-- str
          len
          pos
          lst
          cnt)))
    (<= 0
      (car (lrat-flg-int-list-until-0-or-- str
          len
          pos
          lst
          cnt))))
  :hints (("Goal" :in-theory (disable length)))
  :rule-classes :linear)
other
(defthm car-lrat-flag-int-list-until-0-or---less-than-len
  (implies (and (lrat-guard str len pos)
      (car (lrat-flg-int-list-until-0-or-- str
          len
          pos
          lst
          cnt)))
    (< (car (lrat-flg-int-list-until-0-or-- str
          len
          pos
          lst
          cnt))
      len))
  :hints (("Goal" :in-theory (disable length)) ("Subgoal *1/3" :in-theory (disable car-lrat-flag-int-less-than-len)
      :use ((:instance car-lrat-flag-int-less-than-len
         (str str)
         (len (length str))
         (pos (lrat-flg-pos-skip-spaces str
             (length str)
             pos)))))))
other
(defthm int-listp-lrat-flg-int-list-until-0-or--
  (implies (integer-listp lst)
    (integer-listp (mv-nth 1
        (lrat-flg-int-list-until-0-or-- str
          len
          pos
          lst
          cnt)))))
other
(in-theory (disable lrat-flg-int-list-until-0-or--))
lrat-flg-int-rev-list-of-lists-until-0-or--function
(defun lrat-flg-int-rev-list-of-lists-until-0-or--
  (str len pos lst cnt)
  (declare (xargs :guard (and (lrat-guard str len pos)
        (true-listp lst)
        (natp cnt)
        (<= cnt len))
      :measure (acl2-count cnt)))
  (b* ((ch (char str pos)) ((if (eql #\
 ch)) (mv pos lst))
      ((mv pos-after-int-list int-list) (lrat-flg-int-list-until-0-or-- str
          len
          pos
          nil
          len))
      ((unless (and (integerp pos-after-int-list)
           (< pos-after-int-list 72057594037927936))) (mv nil nil))
      (pos (u59 pos))
      (pos-after-int-list (u59 pos-after-int-list))
      ((unless (< pos pos-after-int-list)) (mv nil nil))
      (cnt (u59 cnt))
      (cnt-1 (s60 (1- cnt))))
    (if (mbe :logic (zp cnt)
        :exec (<= cnt 0))
      (mv nil nil)
      (lrat-flg-int-rev-list-of-lists-until-0-or-- str
        len
        pos-after-int-list
        (cons int-list lst)
        cnt-1))))
lrat-line-mvfunction
(defun lrat-line-mv
  (str len pos)
  (declare (xargs :guard (lrat-guard str len pos)
      :guard-hints (("Goal" :in-theory (disable length)))))
  (b* ((pos (u59 pos)) ((mv pos-after-line-number proof-step) (lrat-flg-nat str len pos))
      (in-bounds (and (integerp pos-after-line-number)
          (< pos-after-line-number 72057594037927936)))
      ((unless in-bounds) (mv nil nil))
      (pos-after-line-number (u59 pos-after-line-number))
      (ch (char str pos-after-line-number))
      ((unless (eql ch #\ )) (mv nil nil))
      (pos-after-line-number+1 (u59 (1+ pos-after-line-number)))
      (len (u59 len))
      ((unless (< pos-after-line-number+1 len)) (mv nil nil))
      (ch (char str pos-after-line-number+1)))
    (if (eql ch #\d)
      (b* ((pos-after-line-number+2 (1+ pos-after-line-number+1)) ((unless (< pos-after-line-number+2 len)) (mv nil nil))
          (ch (char str pos-after-line-number+2))
          ((unless (eql ch #\ )) (mv nil nil))
          (pos-after-line-number+3 (1+ pos-after-line-number+2))
          ((unless (< pos-after-line-number+3 len)) (mv nil nil))
          ((mv pos-after-nat-list nat-list) (lrat-flg-nat-list-until-0 str
              len
              pos-after-line-number+3
              nil
              len))
          ((unless pos-after-nat-list) (mv nil nil)))
        (mv pos-after-nat-list (cons t nat-list)))
      (b* (((mv pos-after-int-list-1 int-list-1) (lrat-flg-int-list-until-0 str
             len
             pos-after-line-number+1
             nil
             len)) ((unless (and (integerp pos-after-int-list-1)
               (< pos-after-int-list-1 len))) (mv nil nil))
          ((mv pos-after-int-list-2 int-list-2) (lrat-flg-int-list-until-0-or-- str
              len
              pos-after-int-list-1
              nil
              len))
          ((unless pos-after-int-list-2) (mv nil nil))
          ((mv pos-after-int-list-3 int-list-3) (lrat-flg-int-rev-list-of-lists-until-0-or-- str
              len
              pos-after-int-list-2
              nil
              len))
          ((unless pos-after-int-list-3) (mv nil nil))
          (ans (cons (cons proof-step int-list-1)
              (cons int-list-2 int-list-3))))
        (mv pos-after-int-list-3 ans)))))
other
(in-theory (disable lrat-line-mv))
lrat-strfunction
(defun lrat-str
  (str len pos cnt rev-lines)
  (declare (xargs :guard (and (stringp str)
        (natp pos)
        (natp len)
        (equal len (length str))
        (<= pos len)
        (< len 72057594037927936)
        (natp cnt))
      :measure (acl2-count cnt)))
  (if (>= pos len)
    nil
    (b* (((mv pos-after-line line) (lrat-line-mv str len pos)) ((unless (natp pos-after-line)) nil)
        ((unless (< pos-after-line len)) nil)
        (ch (char str pos-after-line))
        ((unless (eql ch #\
)) nil)
        (pos-after-line+1 (1+ pos-after-line))
        ((unless (< pos-after-line+1 len)) (cons line rev-lines))
        ((if (mbe :logic (zp cnt)
             :exec (<= cnt 0))) nil))
      (lrat-str str
        len
        pos-after-line+1
        (1- cnt)
        (cons line rev-lines)))))
other
(in-theory (disable lrat-str))
lrat-read-filefunction
(defun lrat-read-file
  (file-name state)
  (declare (xargs :guard (stringp file-name)
      :guard-hints (("Goal" :in-theory (disable open-input-channel)))
      :stobjs state))
  (b* ((str (read-file-into-string file-name)) (len (length str))
      ((unless (lrat-guard str len 0)) nil)
      (ans (my-rev (lrat-str str len 0 len nil))))
    ans))
pos-to-eol+1function
(defun pos-to-eol+1
  (str len pos)
  (declare (xargs :guard (lrat-guard str len pos)
      :measure (nfix (- len pos))))
  (b* ((ch (char str pos)) ((unless (< pos 72057594037927936)) len)
      (pos+1 (1+ (u56 pos)))
      ((if (eql ch #\
)) pos+1)
      (len (u56 len))
      ((if (mbe :logic (zp (- len pos+1))
           :exec (>= pos+1 len))) len))
    (pos-to-eol+1 str len pos+1)))
other
(defthm natp-pos-to-eol+1
  (implies (and (natp pos) (natp len))
    (<= 0 (pos-to-eol+1 str len pos))))
other
(defthm pos-to-eol+1-is-limited
  (implies (lrat-guard str len pos)
    (< (pos-to-eol+1 str len pos)
      72057594037927936))
  :hints (("Goal" :induct (pos-to-eol+1 str len pos))))
cnf-strfunction
(defun cnf-str
  (str len
    pos
    cnt
    line-num
    rev-lines
    file-name)
  (declare (xargs :guard (and (stringp str)
        (natp pos)
        (natp len)
        (equal len (length str))
        (< pos len)
        (< len 72057594037927936)
        (natp cnt)
        (< cnt len)
        (natp line-num))
      :guard-hints (("Goal" :in-theory (disable length)))
      :measure (acl2-count cnt))
    (ignorable rev-lines))
  (b* (((when (eql (char str pos) #\c)) (er hard?
         'parse-cnf-file
         "Line ~x0 of file ~x1 starts with character `c', perhaps ~
             indicating a DIMACS comment; but such lines are not supported by ~
             this checker."
         line-num
         file-name)) ((mv pos-after-line int-list) (lrat-flg-int-list-until-0 str
          len
          pos
          nil
          cnt))
      ((when (null int-list)) (er hard?
          'parse-cnf-file
          "Line ~x0 of file ~x1 contains no data."
          line-num
          file-name))
      ((unless (integerp pos-after-line)) nil)
      ((unless (< pos-after-line len)) nil)
      (int-list (cons line-num int-list))
      (pos-at-eol+1 (pos-to-eol+1 str
          len
          pos-after-line))
      ((unless (integerp pos-at-eol+1)) nil)
      ((if (= pos-at-eol+1 len)) (cons int-list rev-lines))
      ((unless (< pos-at-eol+1 len)) nil)
      ((if (mbe :logic (zp cnt)
           :exec (<= cnt 0))) nil))
    (cnf-str str
      len
      pos-at-eol+1
      (1- (u59 cnt))
      (1+ line-num)
      (cons int-list rev-lines)
      file-name)))
other
(in-theory (disable cnf-str))
cnf-read-filefunction
(defun cnf-read-file
  (file-name state)
  (declare (xargs :guard (stringp file-name)
      :guard-hints (("Goal" :in-theory (disable read-file-into-string)))
      :verify-guards nil
      :stobjs state))
  (b* ((str (read-file-into-string file-name)) (len (length str))
      ((unless (lrat-guard str len 0)) nil)
      (pos (pos-to-eol+1 str len 0))
      (ans (cnf-str str
          len
          pos
          (1- len)
          1
          nil
          file-name)))
    ans))
parse-lrat-filefunction
(defun parse-lrat-file
  (filename state)
  (let ((x (lrat-read-file filename state)))
    (pprogn (increment-file-clock state)
      (value x))))
parse-cnf-filefunction
(defun parse-cnf-file
  (filename state)
  (let ((x (cnf-read-file filename state)))
    (pprogn (increment-file-clock state)
      (value x))))
verify-lrat-proof-fnfunction
(defun verify-lrat-proof-fn
  (cnf-file lrat-file
    incomplete-okp
    state)
  (b* (((er formula) (time$ (parse-cnf-file cnf-file state))) ((er proof) (time$ (parse-lrat-file lrat-file state))))
    (value (time$ (valid-proofp$-top formula
          proof
          incomplete-okp)))))
verify-lrat-proofmacro
(defmacro verify-lrat-proof
  (cnf-file lrat-file
    &optional
    (incomplete-okp 'nil))
  `(verify-lrat-proof-fn ,LRAT::CNF-FILE
    ,LRAT::LRAT-FILE
    ,LRAT::INCOMPLETE-OKP
    state))
show-proof-entryfunction
(defun show-proof-entry
  (entry)
  (cond ((proof-entry-deletion-p entry) (cons 'deletion (cdr entry)))
    (t (list :index (access add-step entry :index)
        :clause (access add-step entry :clause)
        :rup-indices (access add-step entry :rup-indices)
        :drat-hints (access add-step entry :drat-hints)))))
show-lrat-prooffunction
(defun show-lrat-proof
  (proof acc)
  (cond ((endp proof) (reverse acc))
    (t (show-lrat-proof (cdr proof)
        (cons (show-proof-entry (car proof)) acc)))))
show-lrat-parsefunction
(defun show-lrat-parse
  (lrat-file state)
  (er-let* ((proof (parse-lrat-file lrat-file state)))
    (value (show-lrat-proof proof nil))))
show-drat-hints-rawfunction
(defun show-drat-hints-raw
  (drat-hints acc)
  (cond ((endp drat-hints) acc)
    (t (show-drat-hints-raw (cdr drat-hints)
        (cons (- (caar drat-hints))
          (append (cdar drat-hints) acc))))))
show-proof-entry-rawfunction
(defun show-proof-entry-raw
  (index entry)
  (cond ((proof-entry-deletion-p entry) (list* index 'd (cdr entry)))
    (t (cons (access add-step entry :index)
        (append (access add-step entry :clause)
          (cons 0
            (append (access add-step entry :rup-indices)
              (show-drat-hints-raw (access add-step entry :drat-hints)
                nil))))))))
show-lrat-proof-rawfunction
(defun show-lrat-proof-raw
  (index proof acc)
  (cond ((endp proof) (reverse acc))
    (t (let ((entry-raw (show-proof-entry-raw index (car proof))))
        (show-lrat-proof-raw (car entry-raw)
          (cdr proof)
          (cons entry-raw acc))))))
other
(program)
show-lrat-parse-rawfunction
(defun show-lrat-parse-raw
  (lrat-file state)
  (er-let* ((proof (parse-lrat-file lrat-file state)))
    (pprogn (print-on-separate-lines (show-lrat-proof-raw nil proof nil)
        nil
        *standard-co*
        state)
      (value :invisible))))
lrat-test-fnfunction
(defun lrat-test-fn
  (doublets dir okp chan state)
  (cond ((endp doublets) (pprogn (fms "OVERALL RESULT: ~s0~|~%"
          (list (cons #\0
              (if okp
                "success"
                "FAILURE")))
          chan
          state
          nil)
        (value okp)))
    (t (let* ((d (car doublets)) (cnf (concatenate 'string dir (car d)))
          (lrat (concatenate 'string dir (cadr d)))
          (incomplete-okp (caddr d)))
        (pprogn (fms "Starting ~x0.~|"
            (list (cons #\0
                `(verify-lrat-proof ,LRAT::CNF
                  ,LRAT::LRAT
                  ,@(CDDR LRAT::D))))
            chan
            state
            nil)
          (er-let* ((val (verify-lrat-proof cnf
                 lrat
                 incomplete-okp)))
            (pprogn (princ$ "Result: " chan state)
              (princ$ (if val
                  "success"
                  "FAILURE")
                chan
                state)
              (newline chan state)
              (lrat-test-fn (cdr doublets)
                dir
                (and val okp)
                chan
                state))))))))
lrat-testmacro
(defmacro lrat-test
  (doublets &optional (dir '""))
  (declare (xargs :guard (stringp dir)))
  (let ((dir (if (and (not (equal dir ""))
           (not (eql (char dir (1- (length dir))) #\/)))
         (concatenate 'string dir "/")
         dir)))
    `(lrat-test-fn ',LRAT::DOUBLETS
      ',LRAT::DIR
      t
      (standard-co state)
      state)))