• Top
  • Documentation
  • Books
  • Boolean-reasoning
    • Ipasir
    • Aignet
    • Aig
    • Satlink
      • Sat-solver-options
      • Config-p
      • Logical-story
      • Dimacs
        • Dimacs-export
        • Dimacs-interp
          • Satlink-handle-line
          • Satlink-parse-variable-line
          • Satlink-skip-ws
          • Satlink-parse-output
          • Satlink-handle-lines
      • Gather-benchmarks
      • Cnf
      • Satlink-extra-hook
      • Sat
    • Truth
    • Ubdds
    • Bdd
    • Faig
    • Bed
    • 4v
  • Projects
  • Debugging
  • Std
  • Proof-automation
  • Macro-libraries
  • ACL2
  • Interfacing-tools
  • Hardware-verification
  • Software-verification
  • Math
  • Testing-utilities

• Dimacs-interp

Satlink-skip-ws

Signature

(satlink-skip-ws x n xl) → new-n

Arguments

x — String we're processing.
    Guard (stringp x).

n — Current position in x.
    Guard (natp n).

xl — Pre-computed length of x.
    Guard (equal xl (length x)).

Returns

new-n — New position after skipping whitespace.
    Type (natp new-n).

Definitions and Theorems

Function: satlink-skip-ws

(defun satlink-skip-ws (x n xl)
  (declare (xargs :guard (and (stringp x)
                              (natp n)
                              (equal xl (length x)))))
  (declare (xargs :guard (<= n xl)))
  (let ((__function__ 'satlink-skip-ws))
    (declare (ignorable __function__))
    (b* (((when (mbe :logic (zp (- (nfix xl) (nfix n)))
                     :exec (int= xl n)))
          (lnfix n))
         (char (char x n))
         ((when (or (eql char #\Space)
                    (eql char #\Tab)))
          (satlink-skip-ws x (+ 1 (lnfix n)) xl)))
      (lnfix n))))

Theorem: natp-of-satlink-skip-ws

(defthm natp-of-satlink-skip-ws
  (b* ((new-n (satlink-skip-ws x n xl)))
    (natp new-n))
  :rule-classes :rewrite)

Theorem: lower-bound-satlink-skip-ws

(defthm lower-bound-satlink-skip-ws
  (implies (natp n)
           (<= n (satlink-skip-ws x n xl)))
  :rule-classes ((:rewrite) (:linear)))

Theorem: lower-bound-satlink-skip-ws-nfix

(defthm lower-bound-satlink-skip-ws-nfix
  (<= (nfix n) (satlink-skip-ws x n xl))
  :rule-classes (:rewrite :linear))

Theorem: upper-bound-satlink-skip-ws

(defthm upper-bound-satlink-skip-ws
  (implies (and (natp n) (natp xl) (<= n xl))
           (<= (satlink-skip-ws x n xl) xl))
  :rule-classes ((:rewrite) (:linear)))