• Top
  • Documentation
  • Books
  • Boolean-reasoning
    • Ipasir
    • Aignet
    • Aig
    • Satlink
    • Truth
    • Ubdds
      • Equal-by-eval-bdds
      • Ubdd-constructors
        • Q-and
        • Q-ite
          • Q-ite-reductions
          • Canonicalize-to-q-ite
        • Q-or
        • Q-implies
        • Q-iff
        • Q-and-c2
        • Q-and-c1
        • Q-or-c2
        • Q-not
        • Q-ite-fn
        • Q-xor
        • Cheap-and-expensive-arguments
        • Q-and-is-nil
        • Q-compose-list
        • Qv
        • Q-compose
        • Q-and-is-nilc2
        • Q-nor
        • Q-nand
      • Eval-bdd
      • Ubddp
      • Ubdd-fix
      • Q-sat
      • Bdd-sat-dfs
      • Eval-bdd-list
      • Qcdr
      • Qcar
      • Q-sat-any
      • Canonicalize-to-q-ite
      • Ubdd-listp
      • Qcons
    • Bdd
    • Faig
    • Bed
    • 4v
  • Projects
  • Debugging
  • Std
  • Proof-automation
  • Macro-libraries
  • ACL2
  • Interfacing-tools
  • Hardware-verification
  • Software-verification
  • Math
  • Testing-utilities

• Q-ite

Q-ite-reductions

Basic rewriting of q-ite expressions.

When using the canonicalize-to-q-ite strategy, you generally end up with big nests of q-ite calls. Afterward, these basic sorts of reductions can be useful.

Definitions and Theorems

Theorem: (q-ite x (q-ite y nil t) z)

(defthm |(q-ite x (q-ite y nil t) z)|
  (implies (and (syntaxp (not (equal z ''t)))
                (force (ubddp x))
                (force (ubddp y))
                (force (ubddp z)))
           (equal (q-ite x (q-ite y nil t) z)
                  (q-ite y (q-ite x nil z)
                         (q-ite x t z)))))

Theorem: (q-ite x (q-ite y nil t) t)

(defthm |(q-ite x (q-ite y nil t) t)|
  (implies (and (force (ubddp x))
                (force (ubddp y))
                (force (ubddp z)))
           (equal (q-ite x (q-ite y nil t) t)
                  (q-ite y (q-ite x nil t) t))))

Theorem: (q-ite (q-ite a b c) x y)

(defthm |(q-ite (q-ite a b c) x y)|
  (implies (and (force (ubddp a))
                (force (ubddp b))
                (force (ubddp c))
                (force (ubddp x))
                (force (ubddp y)))
           (equal (q-ite (q-ite a b c) x y)
                  (q-ite a (q-ite b x y) (q-ite c x y)))))

Theorem: (q-ite x y y)

(defthm |(q-ite x y y)|
  (equal (q-ite x y y) y))

Theorem: (q-ite x x y)

(defthm |(q-ite x x y)|
  (implies (and (force (ubddp x))
                (force (ubddp y)))
           (equal (q-ite x x y) (q-ite x t y))))

Theorem: (q-ite x y x)

(defthm |(q-ite x y x)|
  (equal (q-ite x y x) (q-ite x y nil)))

Theorem: (q-ite x t nil)

(defthm |(q-ite x t nil)|
  (implies (force (ubddp x))
           (equal (q-ite x t nil) x)))

Theorem: (q-ite non-nil y z)

(defthm |(q-ite non-nil y z)|
  (implies (and (atom x) x)
           (equal (q-ite x y z) y)))

Theorem: (q-ite t x y)

(defthm |(q-ite t x y)|
  (equal (q-ite t x y) x))

Theorem: (q-ite nil x y)

(defthm |(q-ite nil x y)|
  (equal (q-ite nil x y) y))