• Top
  • Documentation
  • Books
  • Boolean-reasoning
    • Ipasir
    • Aignet
    • Aig
    • Satlink
      • Sat-solver-options
      • Config-p
        • Config
        • Make-config
        • Change-config
        • Honsed-config
        • Make-honsed-config
        • *default-config*
        • Config->verbose
        • Config->timing
        • Config->remove-temps
        • Config->mintime
        • Config->lrat-check
        • Config->cmdline
      • Logical-story
      • Dimacs
      • 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

• Config-p

Honsed-config

Raw constructor for honsed config-p structures.

Syntax:

(honsed-config cmdline verbose
               timing mintime remove-temps lrat-check)

This is identical to config, except that we hons the structure we are creating.

Definition

This is an ordinary honsing constructor introduced by defaggregate.

Function: honsed-config

(defun honsed-config
       (cmdline verbose
                timing mintime remove-temps lrat-check)
 (declare (xargs :guard (and (stringp cmdline)
                             (booleanp verbose)
                             (booleanp timing)
                             (booleanp remove-temps)
                             (booleanp lrat-check))))
 (mbe
  :logic (config cmdline verbose
                 timing mintime remove-temps lrat-check)
  :exec
  (hons
   :satlink-config
   (hons (hons 'cmdline cmdline)
         (hons (hons 'verbose verbose)
               (hons (hons 'timing timing)
                     (hons (hons 'mintime mintime)
                           (hons (hons 'remove-temps remove-temps)
                                 (hons (hons 'lrat-check lrat-check)
                                       nil)))))))))