• 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
        • Up-past-op
        • Up-past-var
        • Up-one-aux
        • Up-one*
        • Up-one
      • Aig-translation
    • 4v
  • Projects
  • Debugging
  • Std
  • Proof-automation
  • Macro-libraries
  • ACL2
  • Interfacing-tools
  • Hardware-verification
  • Software-verification
  • Math
  • Testing-utilities

• Up

Up-past-op

Lift a variable through a (single) operator.

Signature

(up-past-op vlift op left right order) → (mv bed order)

Arguments

vlift — The variable we are lifting.
    Guard (atom vlift).

op — The operator we are lifting it past.
    Guard (bed-op-p op).

left — Left branch of op, with vlift usually at the top.

right — Right branch of op, with vlift usually at the top.

order — Ordering to use for bed construction.

Returns

bed — Reduced bed, equivalent op(left,right), but with vlift lifted to the top, if possible.

order — Updated order for canonicalization.

Definitions and Theorems

Function: up-past-op

(defun up-past-op (vlift op left right order)
  (declare (xargs :guard (and (atom vlift) (bed-op-p op))))
  (let ((__function__ 'up-past-op))
    (declare (ignorable __function__))
    (b* ((op (bed-op-fix$ op))
         ((mv lok lvar ltrue lfalse)
          (bed-match-var left))
         ((mv rok rvar rtrue rfalse)
          (bed-match-var right))
         ((when (and lok rok (equal lvar vlift)
                     (equal rvar vlift)))
          (b* (((mv new-left order)
                (mk-op1 op ltrue rtrue order))
               ((mv new-right order)
                (mk-op1 op lfalse rfalse order))
               (ans (mk-var1 vlift new-left new-right)))
            (mv ans order)))
         ((when (and lok (equal lvar vlift)))
          (b* (((mv new-left order)
                (mk-op1 op ltrue right order))
               ((mv new-right order)
                (mk-op1 op lfalse right order))
               (ans (mk-var1 vlift new-left new-right)))
            (mv ans order)))
         ((when (and rok (equal rvar vlift)))
          (b* (((mv new-left order)
                (mk-op1 op left rtrue order))
               ((mv new-right order)
                (mk-op1 op left rfalse order))
               (ans (mk-var1 vlift new-left new-right)))
            (mv ans order)))
         ((mv ans order)
          (mk-op1 op left right order)))
      (mv ans order))))

Theorem: up-past-op-correct

(defthm up-past-op-correct
  (implies (force (atom vlift))
           (b* (((mv bed ?order)
                 (up-past-op vlift op left right order)))
             (equal (bed-eval bed env)
                    (bed-op-eval op (bed-eval left env)
                                 (bed-eval right env))))))