• Top
  • Documentation
  • Books
  • 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
  • Math
  • Testing-utilities

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