• 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-handle-lines

Signature

(satlink-handle-lines lines pstate env$) 
  → 
(mv error-p new-pstate env$)

Arguments

lines — Guard (string-listp lines).

pstate — Guard (satlink-parser-state-p pstate).

env$ — evolving variable bindings.

Returns

error-p — did we see something we don't understand?.

new-pstate — Type (satlink-parser-state-p new-pstate).

Definitions and Theorems

Function: satlink-handle-lines

(defun satlink-handle-lines (lines pstate env$)
  (declare (xargs :stobjs (env$)))
  (declare (xargs :guard (and (string-listp lines)
                              (satlink-parser-state-p pstate))))
  (let ((__function__ 'satlink-handle-lines))
    (declare (ignorable __function__))
    (b* (((when (atom lines))
          (mv nil (satlink-parser-state-fix pstate)
              env$))
         ((mv error-p pstate env$)
          (satlink-handle-line (car lines)
                               pstate env$))
         ((when error-p)
          (mv error-p pstate env$)))
      (satlink-handle-lines (cdr lines)
                            pstate env$))))

Theorem: satlink-parser-state-p-of-satlink-handle-lines.new-pstate

(defthm satlink-parser-state-p-of-satlink-handle-lines.new-pstate
  (b* (((mv ?error-p ?new-pstate ?env$)
        (satlink-handle-lines lines pstate env$)))
    (satlink-parser-state-p new-pstate))
  :rule-classes :rewrite)