• Top
  • Documentation
  • Books
  • Boolean-reasoning
    • Ipasir
    • Aignet
      • Base-api
      • Aignet-construction
      • Representation
        • Aignet-impl
        • Node
        • Network
        • Combinational-type
          • Ctype
            • *stype-ctype-map*
          • Ctype-equiv
          • Ctype-fix
          • Ctypep
        • Typecode
        • Stypep
      • Aignet-copy-init
      • Aignet-simplify-with-tracking
      • Aignet-simplify-marked-with-tracking
      • Aignet-cnf
      • Aignet-simplify-marked
      • Aignet-complete-copy
      • Aignet-transforms
      • Aignet-eval
      • Semantics
      • Aignet-read-aiger
      • Aignet-write-aiger
      • Aignet-abc-interface
      • Utilities
    • Aig
    • Satlink
    • Truth
    • Ubdds
    • Bdd
    • Faig
    • Bed
    • 4v
  • Projects
  • Debugging
  • Std
  • Proof-automation
  • Macro-libraries
  • ACL2
  • Interfacing-tools
  • Hardware-verification
  • Software-verification
  • Math
  • Testing-utilities

• Combinational-type

Ctype

Map a sequential-type keyword to its combinational-type keywords.

Signature

(ctype x) → type

Arguments

x — Guard (stypep x).

Returns

type — Type (ctypep type).

Definitions and Theorems

Function: ctype

(defun ctype (x)
  (declare (xargs :guard (stypep x)))
  (let ((__function__ 'ctype))
    (declare (ignorable __function__))
    (let ((x (stype-fix x)))
      (cdr (assoc x *stype-ctype-map*)))))

Theorem: ctypep-of-ctype

(defthm ctypep-of-ctype
  (b* ((type (ctype x))) (ctypep type))
  :rule-classes :rewrite)

Theorem: ctype-possibilities

(defthm ctype-possibilities
  (or (equal (ctype x) (const-ctype))
      (equal (ctype x) (gate-ctype))
      (equal (ctype x) (in-ctype))
      (equal (ctype x) (out-ctype)))
  :rule-classes ((:forward-chaining :trigger-terms ((ctype x)))))

Theorem: stype-equiv-implies-equal-ctype-1

(defthm stype-equiv-implies-equal-ctype-1
  (implies (stype-equiv x x-equiv)
           (equal (ctype x) (ctype x-equiv)))
  :rule-classes (:congruence))

Theorem: ctype-not-const-implies-nonempty

(defthm ctype-not-const-implies-nonempty
  (implies (not (equal (ctype (stype (car x)))
                       (const-ctype)))
           (consp x))
  :rule-classes
  ((:forward-chaining :trigger-terms ((ctype (stype (car x)))))))

Theorem: stype-by-ctype

(defthm stype-by-ctype
  (and (equal (equal (ctype (stype x)) (const-ctype))
              (equal (stype x) (const-stype)))
       (implies (equal (regp (stype x)) 1)
                (and (equal (equal (ctype (stype x)) (in-ctype))
                            (equal (stype x) (reg-stype)))
                     (equal (equal (ctype (stype x)) (out-ctype))
                            (equal (stype x) (nxst-stype)))
                     (equal (equal (ctype (stype x)) (gate-ctype))
                            (equal (stype x) (xor-stype)))))
       (implies (not (equal (regp (stype x)) 1))
                (and (equal (equal (ctype (stype x)) (in-ctype))
                            (equal (stype x) (pi-stype)))
                     (equal (equal (ctype (stype x)) (out-ctype))
                            (equal (stype x) (po-stype)))
                     (equal (equal (ctype (stype x)) (gate-ctype))
                            (equal (stype x) (and-stype)))))))

Theorem: ctype-gate-fwd

(defthm ctype-gate-fwd
  (implies (equal (ctype (stype x)) (gate-ctype))
           (or (equal (stype x) (and-stype))
               (equal (stype x) (xor-stype))))
  :rule-classes
  ((:forward-chaining
        :trigger-terms ((equal (ctype (stype x)) (gate-ctype))
                        (equal (gate-ctype)
                               (ctype (stype x)))))))

Theorem: ctype-not-gate-fwd

(defthm ctype-not-gate-fwd
  (implies (not (equal (ctype (stype x)) (gate-ctype)))
           (and (not (equal (stype x) (and-stype)))
                (not (equal (stype x) (xor-stype)))))
  :rule-classes
  ((:forward-chaining
        :trigger-terms ((equal (ctype (stype x)) (gate-ctype))
                        (equal (gate-ctype)
                               (ctype (stype x)))))))

Theorem: ctype-in-fwd

(defthm ctype-in-fwd
  (implies (equal (ctype (stype x)) (in-ctype))
           (or (equal (stype x) (pi-stype))
               (equal (stype x) (reg-stype))))
  :rule-classes
  ((:forward-chaining
        :trigger-terms ((equal (ctype (stype x)) (in-ctype))
                        (equal (in-ctype) (ctype (stype x)))))))

Theorem: ctype-not-in-fwd

(defthm ctype-not-in-fwd
  (implies (not (equal (ctype (stype x)) (in-ctype)))
           (and (not (equal (stype x) (pi-stype)))
                (not (equal (stype x) (reg-stype)))))
  :rule-classes
  ((:forward-chaining
        :trigger-terms ((equal (ctype (stype x)) (in-ctype))
                        (equal (in-ctype) (ctype (stype x)))))))

Theorem: ctype-out-fwd

(defthm ctype-out-fwd
  (implies (equal (ctype (stype x)) (out-ctype))
           (or (equal (stype x) (po-stype))
               (equal (stype x) (nxst-stype))))
  :rule-classes
  ((:forward-chaining
        :trigger-terms ((equal (ctype (stype x)) (out-ctype))
                        (equal (out-ctype)
                               (ctype (stype x)))))))

Theorem: ctype-not-out-fwd

(defthm ctype-not-out-fwd
  (implies (not (equal (ctype (stype x)) (out-ctype)))
           (and (not (equal (stype x) (po-stype)))
                (not (equal (stype x) (nxst-stype)))))
  :rule-classes
  ((:forward-chaining
        :trigger-terms ((equal (ctype (stype x)) (out-ctype))
                        (equal (out-ctype)
                               (ctype (stype x)))))))

Theorem: ctype-of-stype-fix-x

(defthm ctype-of-stype-fix-x
  (equal (ctype (stype-fix x)) (ctype x)))

Theorem: ctype-stype-equiv-congruence-on-x

(defthm ctype-stype-equiv-congruence-on-x
  (implies (stype-equiv x x-equiv)
           (equal (ctype x) (ctype x-equiv)))
  :rule-classes :congruence)

Subtopics

*stype-ctype-map*