• Top
  • Documentation
  • Books
  • Boolean-reasoning
    • Ipasir
    • Aignet
    • Aig
    • Satlink
      • Sat-solver-options
      • Config-p
      • Logical-story
      • Dimacs
        • Dimacs-export
        • Dimacs-interp
      • 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

Dimacs-export

Writer to translate cnf formulas into DIMACS files.

The basic idea here is that acc is a character list with the output we have printed in reverse order. This means (cons char acc) is the same as printing a char, (str::revappend-chars str acc) is the same as printing str, etc. See str::revappend-chars for more background about this basic approach.

Definitions and Theorems

Function: dimacs-write-lit$inline

(defun dimacs-write-lit$inline (lit acc)
  (declare (xargs :guard (and (litp lit) (character-listp acc))))
  (let ((__function__ 'dimacs-write-lit))
    (declare (ignorable __function__))
    (b* ((negatedp (int= (lit->neg lit) 1))
         (id+1 (+ 1 (lit->var lit)))
         (acc (if negatedp (cons #\- acc) acc)))
      (str::revappend-nat-to-dec-chars id+1 acc))))

Theorem: character-listp-of-dimacs-write-lit

(defthm character-listp-of-dimacs-write-lit
  (implies (and (litp lit) (character-listp acc))
           (b* ((acc (dimacs-write-lit$inline lit acc)))
             (character-listp acc)))
  :rule-classes :rewrite)

Function: dimacs-write-clause

(defun dimacs-write-clause (clause acc)
  (declare (xargs :guard (and (lit-listp clause)
                              (character-listp acc))))
  (let ((__function__ 'dimacs-write-clause))
    (declare (ignorable __function__))
    (b* (((when (atom clause))
          (cons #\Newline (cons #\0 acc)))
         (acc (dimacs-write-lit (car clause) acc))
         (acc (cons #\Space acc)))
      (dimacs-write-clause (cdr clause)
                           acc))))

Theorem: character-listp-of-dimacs-write-clause

(defthm character-listp-of-dimacs-write-clause
  (implies (and (lit-listp clause)
                (character-listp acc))
           (b* ((acc (dimacs-write-clause clause acc)))
             (character-listp acc)))
  :rule-classes :rewrite)

Function: dimacs-write-clauses

(defun dimacs-write-clauses (clauses acc)
  (declare (xargs :guard (and (lit-list-listp clauses)
                              (character-listp acc))))
  (let ((__function__ 'dimacs-write-clauses))
    (declare (ignorable __function__))
    (b* (((when (atom clauses)) acc)
         (acc (dimacs-write-clause (car clauses)
                                   acc)))
      (dimacs-write-clauses (cdr clauses)
                            acc))))

Theorem: character-listp-of-dimacs-write-clauses

(defthm character-listp-of-dimacs-write-clauses
  (implies (and (lit-list-listp clauses)
                (character-listp acc))
           (b* ((acc (dimacs-write-clauses clauses acc)))
             (character-listp acc)))
  :rule-classes :rewrite)

Function: dimacs-write-formula

(defun dimacs-write-formula (formula)
  (declare (xargs :guard (lit-list-listp formula)))
  (let ((__function__ 'dimacs-write-formula))
    (declare (ignorable __function__))
    (b* ((max-index (max-index-formula formula))
         (dimacs-num-vars (+ 1 max-index))
         (acc nil)
         (acc (str::revappend-chars "p cnf " acc))
         (acc (str::revappend-nat-to-dec-chars dimacs-num-vars acc))
         (acc (cons #\Space acc))
         (acc (str::revappend-nat-to-dec-chars (len formula)
                                               acc))
         (acc (cons #\Newline acc))
         (acc (dimacs-write-clauses formula acc)))
      (mv (str::rchars-to-string acc)
          max-index))))

Theorem: stringp-of-dimacs-write-formula.dimacs-text

(defthm stringp-of-dimacs-write-formula.dimacs-text
  (implies (and (lit-list-listp formula))
           (b* (((mv ?dimacs-text ?max-index)
                 (dimacs-write-formula formula)))
             (stringp dimacs-text)))
  :rule-classes :rewrite)

Theorem: return-type-of-dimacs-write-formula.max-index

(defthm return-type-of-dimacs-write-formula.max-index
  (b* (((mv ?dimacs-text ?max-index)
        (dimacs-write-formula formula)))
    (equal max-index (max-index-formula formula)))
  :rule-classes :rewrite)

Function: dimacs-export-fn

(defun dimacs-export-fn (formula filename state)
  (declare (xargs :stobjs (state)))
  (declare (xargs :guard (and (lit-list-listp formula)
                              (stringp filename))))
  (let ((__function__ 'dimacs-export))
    (declare (ignorable __function__))
    (b* ((filename (mbe :logic (if (stringp filename) filename "")
                        :exec filename))
         ((mv channel state)
          (open-output-channel filename
                               :character state))
         ((unless channel)
          (mv nil (max-index-formula formula)
              state))
         ((mv str max-index)
          (dimacs-write-formula formula))
         (state (princ$ str channel state))
         (state (close-output-channel channel state)))
      (mv t max-index state))))

Theorem: booleanp-of-dimacs-export.successp

(defthm booleanp-of-dimacs-export.successp
  (b* (((mv ?successp ?max-index acl2::?state)
        (dimacs-export-fn formula filename state)))
    (booleanp successp))
  :rule-classes :type-prescription)

Theorem: return-type-of-dimacs-export.max-index

(defthm return-type-of-dimacs-export.max-index
  (b* (((mv ?successp ?max-index acl2::?state)
        (dimacs-export-fn formula filename state)))
    (equal max-index (max-index-formula formula)))
  :rule-classes :rewrite)

Theorem: state-p1-of-dimacs-export.state

(defthm state-p1-of-dimacs-export.state
  (implies (force (state-p1 state))
           (b* (((mv ?successp ?max-index acl2::?state)
                 (dimacs-export-fn formula filename state)))
             (state-p1 state)))
  :rule-classes :rewrite)