• Top
  • Documentation
  • Books
  • Boolean-reasoning
    • Ipasir
    • Aignet
    • Aig
    • Satlink
      • Sat-solver-options
        • Unsat-checking
        • Check-config
          • Pigeon-hole
          • Simple-sat
          • Assert-unsat
          • Assert-sat
      • Config-p
      • 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

• Check-config

Simple-sat

Signature

(simple-sat formula &key config) → *

Arguments

formula — Guard (lit-list-listp formula).

config — Guard (config-p config).

Definitions and Theorems

Function: simple-sat-fn

(defun simple-sat-fn (formula config)
  (declare (xargs :guard (and (lit-list-listp formula)
                              (config-p config))))
  "Just returns STATUS, not env."
  (let ((__function__ 'simple-sat))
    (declare (ignorable __function__))
    (progn$
         (tshell-ensure)
         (with-local-stobj env$
                           (mv-let (status env$)
                                   (sat formula env$ :config config)
                             status)))))