• Top
  • Documentation
  • Books
  • Boolean-reasoning
    • Ipasir
    • Aignet
    • Aig
    • Satlink
      • Sat-solver-options
      • Config-p
      • Logical-story
      • Dimacs
      • Gather-benchmarks
      • Cnf
        • Litp
        • Varp
        • Env$
        • Eval-formula
        • Max-index-formula
        • Max-index-clause
        • Formula-indices
        • Clause-indices
      • 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

• Cnf

Eval-formula

Semantics of CNF formulas.

Signature

(eval-formula formula env$) → bit

Arguments

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

Returns

bit — Type (bitp bit).

We define a simple evaluator for CNF formulas that uses an environment to assign values to the identifiers.

The environment, env$, is an abstract stobj that implements a simple bit array. Our evaluators produce a BIT (i.e., 0 or 1) instead of a BOOL (i.e., T or NIL) to make it directly compatible with the bitarr stobj.

Definitions and Theorems

Function: eval-formula

(defun eval-formula (formula env$)
  (declare (xargs :stobjs (env$)))
  (declare (xargs :guard (lit-list-listp formula)))
  (let ((__function__ 'eval-formula))
    (declare (ignorable __function__))
    (if (atom formula)
        1
      (mbe :logic
           (b-and (eval-clause (car formula) env$)
                  (eval-formula (cdr formula) env$))
           :exec
           (if (bit->bool (eval-clause (car formula) env$))
               (eval-formula (cdr formula) env$)
             0)))))

Theorem: bitp-of-eval-formula

(defthm bitp-of-eval-formula
  (b* ((bit (eval-formula formula env$)))
    (bitp bit))
  :rule-classes :rewrite)

Theorem: eval-formula-of-lit-list-list-fix-formula

(defthm eval-formula-of-lit-list-list-fix-formula
  (equal (eval-formula (lit-list-list-fix formula)
                       env$)
         (eval-formula formula env$)))

Theorem: eval-formula-lit-list-list-equiv-congruence-on-formula

(defthm eval-formula-lit-list-list-equiv-congruence-on-formula
  (implies (lit-list-list-equiv formula formula-equiv)
           (equal (eval-formula formula env$)
                  (eval-formula formula-equiv env$)))
  :rule-classes :congruence)