• Top
  • Documentation
  • Books
  • Boolean-reasoning
  • Projects
  • Debugging
  • Std
  • Proof-automation
  • Macro-libraries
  • ACL2
  • Interfacing-tools
  • Hardware-verification
    • Gl
      • Term-level-reasoning
      • Glmc
      • Other-resources
      • Optimization
      • Reference
        • Def-gl-thm
        • Shape-specs
        • Symbolic-objects
        • Gl-aside
        • Def-gl-param-thm
        • Symbolic-arithmetic
        • Bfr
          • Pbfr-depends-on
          • Bfr-varname-p
          • Bfr-varname-fix
          • Bfr-to-param-space
          • Bfr-depends-on
          • Aig-var-fix
          • Bfr-reasoning
          • Bfr-andc2
          • Bfr-andc1
          • Bfr-unparam-env
          • Bfr-set-var
          • Bfr-nor
          • Bfr-nand
          • Bfr-mode
          • Bfr-equiv
          • Bfr-xor
          • Bfr-iff
          • Bfr-eval
          • Bfr-param-env
          • Bfr-lookup
          • Bfr-env-equiv
          • Bfr-and
          • Bfr-var
          • Bfr-or
          • Bfr-not
          • Bfr-ite
          • Bdd-mode-or-p-true
          • Aig-mode-or-p-true
          • Bfr-case
        • Def-gl-boolean-constraint
        • Gl-mbe
        • Bvec
        • Flex-bindings
        • Auto-bindings
        • Gl-interp
        • Gl-set-uninterpreted
        • Def-gl-clause-processor
        • Def-glcp-ctrex-rewrite
        • ACL2::always-equal
        • Gl-hint
        • Def-gl-rewrite
        • Def-gl-branch-merge
        • Gl-force-check
        • Gl-concretize
        • Gl-assert
        • Gl-param-thm
        • Gl-simplify-satlink-mode
        • Gl-satlink-mode
        • Gl-bdd-mode
        • Gl-aig-bddify-mode
        • Gl-fraig-satlink-mode
      • Debugging
      • Basic-tutorial
    • Esim
    • Vl2014
    • Sv
    • Fgl
    • Vwsim
    • Vl
    • X86isa
    • Svl
    • Rtl
  • Software-verification
  • Math
  • Testing-utilities

• Bfr

Pbfr-depends-on

Signature

(pbfr-depends-on k p x) → *

Definitions and Theorems

Function: pbfr-depends-on

(defun pbfr-depends-on (k p x)
  (declare (xargs :guard t))
  (let ((__function__ 'pbfr-depends-on))
    (declare (ignorable __function__))
    (bfr-case :bdd (pbfr-semantic-depends-on k p x)
              :aig (bfr-depends-on k (bfr-from-param-space p x)))))

Theorem: pbfr-eval-of-set-non-dep

(defthm pbfr-eval-of-set-non-dep
  (implies (and (not (pbfr-depends-on k p x))
                (bfr-eval p env)
                (bfr-eval p (bfr-set-var k v env)))
           (equal (bfr-eval x
                            (bfr-param-env p (bfr-set-var k v env)))
                  (bfr-eval x (bfr-param-env p env)))))

Theorem: non-var-implies-non-var-in-restrict-with-iterated-assigns-alist

(defthm
    non-var-implies-non-var-in-restrict-with-iterated-assigns-alist
 (implies
  (not (set::in v (acl2::aig-vars x)))
  (not
   (set::in
    v
    (acl2::aig-vars
         (acl2::aig-restrict
              x
              (acl2::aig-extract-iterated-assigns-alist y clk)))))))

Theorem: pbfr-depends-on-of-bfr-var

(defthm pbfr-depends-on-of-bfr-var
 (implies
     (and (not (bfr-depends-on m p))
          (bfr-eval p env))
     (equal (pbfr-depends-on m p (bfr-to-param-space p (bfr-var n)))
            (equal (bfr-varname-fix m)
                   (bfr-varname-fix n)))))

Theorem: pbfr-depends-on-of-constants

(defthm pbfr-depends-on-of-constants
  (and (not (pbfr-depends-on k p t))
       (not (pbfr-depends-on k p nil))))

Theorem: no-new-deps-of-pbfr-not

(defthm no-new-deps-of-pbfr-not
  (implies (not (pbfr-depends-on k p x))
           (not (pbfr-depends-on k p (bfr-not x)))))

Theorem: no-new-deps-of-pbfr-and

(defthm no-new-deps-of-pbfr-and
  (implies (and (not (pbfr-depends-on k p x))
                (not (pbfr-depends-on k p y)))
           (not (pbfr-depends-on k p (bfr-binary-and x y)))))

Theorem: no-new-deps-of-pbfr-or

(defthm no-new-deps-of-pbfr-or
  (implies (and (not (pbfr-depends-on k p x))
                (not (pbfr-depends-on k p y)))
           (not (pbfr-depends-on k p (bfr-binary-or x y)))))

Theorem: no-new-deps-of-pbfr-xor

(defthm no-new-deps-of-pbfr-xor
  (implies (and (not (pbfr-depends-on k p x))
                (not (pbfr-depends-on k p y)))
           (not (pbfr-depends-on k p (bfr-xor x y)))))

Theorem: no-new-deps-of-pbfr-iff

(defthm no-new-deps-of-pbfr-iff
  (implies (and (not (pbfr-depends-on k p x))
                (not (pbfr-depends-on k p y)))
           (not (pbfr-depends-on k p (bfr-iff x y)))))

Theorem: no-new-deps-of-pbfr-nor

(defthm no-new-deps-of-pbfr-nor
  (implies (and (not (pbfr-depends-on k p x))
                (not (pbfr-depends-on k p y)))
           (not (pbfr-depends-on k p (bfr-nor x y)))))

Theorem: no-new-deps-of-pbfr-nand

(defthm no-new-deps-of-pbfr-nand
  (implies (and (not (pbfr-depends-on k p x))
                (not (pbfr-depends-on k p y)))
           (not (pbfr-depends-on k p (bfr-nand x y)))))

Theorem: no-new-deps-of-pbfr-andc1

(defthm no-new-deps-of-pbfr-andc1
  (implies (and (not (pbfr-depends-on k p x))
                (not (pbfr-depends-on k p y)))
           (not (pbfr-depends-on k p (bfr-andc1 x y)))))

Theorem: no-new-deps-of-pbfr-andc2

(defthm no-new-deps-of-pbfr-andc2
  (implies (and (not (pbfr-depends-on k p x))
                (not (pbfr-depends-on k p y)))
           (not (pbfr-depends-on k p (bfr-andc2 x y)))))

Theorem: no-new-deps-of-pbfr-ite

(defthm no-new-deps-of-pbfr-ite
  (implies (and (not (pbfr-depends-on k p x))
                (not (pbfr-depends-on k p y))
                (not (pbfr-depends-on k p z)))
           (not (pbfr-depends-on k p (bfr-ite-fn x y z)))))

Theorem: pbfr-depends-on-when-booleanp

(defthm pbfr-depends-on-when-booleanp
  (implies (booleanp y)
           (not (pbfr-depends-on k p y)))
  :rule-classes ((:rewrite :backchain-limit-lst 0)))