• Top
  • Documentation
  • Books
  • Recursion-and-induction
  • 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
  • Debugging
  • Projects
  • Std
  • Proof-automation
  • Macro-libraries
  • ACL2
  • Interfacing-tools
  • Hardware-verification
  • Software-verification
  • Testing-utilities
  • Math

• 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)