• Top
  • Documentation
  • Books
  • Recursion-and-induction
  • Boolean-reasoning
    • Ipasir
    • Aignet
    • Aig
    • Satlink
    • Truth
    • Ubdds
    • Bdd
    • Faig
    • Bed
      • Bed-op-p
      • Bed-from-aig
      • Bed-mk1
      • Bed-eval
      • Up
      • Aig-translation
    • 4v
  • Projects
  • Debugging
  • Std
  • Proof-automation
  • Macro-libraries
  • ACL2
  • Interfacing-tools
  • Hardware-verification
  • Software-verification
  • Testing-utilities
  • Math

• Bed

Bed-eval

Semantics of BEDs.

Signature

(bed-eval x env) → bit

Arguments

x — BED to evaluate.

env — Fast alist mapping variables to Booleans (t/nil).

Returns

bit — Type (bitp bit).

Definitions and Theorems

Function: bed-eval

(defun bed-eval (x env)
       (declare (xargs :guard t))
       (let ((__function__ 'bed-eval))
            (declare (ignorable __function__))
            (b* (((when (atom x)) (if x 1 0))
                 ((cons a b) x)
                 ((unless (integerp b))
                  (if (bed-env-lookup a env)
                      (bed-eval (car$ b) env)
                      (bed-eval (cdr$ b) env)))
                 (op (bed-op-fix b))
                 (left (bed-eval (car$ a) env))
                 (right (bed-eval (cdr$ a) env)))
                (bed-op-eval op left right))))

Theorem: bitp-of-bed-eval

(defthm bitp-of-bed-eval
        (b* ((bit (bed-eval x env))) (bitp bit))
        :rule-classes :rewrite)

Function: bed-eval-memoize-condition

(defun bed-eval-memoize-condition (x env)
       (declare (ignorable x env)
                (xargs :guard 't))
       (consp x))

Theorem: bed-eval-when-atom

(defthm bed-eval-when-atom
        (implies (atom x)
                 (equal (bed-eval x env) (if x 1 0))))

Theorem: bed-eval-of-var

(defthm bed-eval-of-var
        (implies (and (consp x) (not (integerp (cdr x))))
                 (equal (bed-eval x env)
                        (if (bed-env-lookup (car x) env)
                            (bed-eval (car (cdr x)) env)
                            (bed-eval (cdr (cdr x)) env)))))

Theorem: bed-eval-when-known-op

(defthm
    bed-eval-when-known-op
    (implies
         (and (equal (bed-op-fix op) fixed-op)
              (integerp op))
         (equal (bed-eval (cons leftright op) env)
                (bed-op-eval fixed-op (bed-eval (car leftright) env)
                             (bed-eval (cdr leftright) env)))))