• Top
  • Documentation
  • Books
  • Boolean-reasoning
    • Ipasir
    • Aignet
      • Base-api
      • Aignet-construction
      • Representation
      • 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
        • Comb-equiv
        • Seq-equiv
        • Seq-equiv-init
        • Invals
        • Outs-comb-equiv
        • Nxsts-comb-equiv
      • 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

• Semantics

Invals

Bit array for the primary inputs to an aignet.

Definitions and Theorems

Definition: invalsp

(defabsstobj invals
  :foundation acl2::bitarr$c
  :recognizer (invalsp :logic acl2::bitarr$ap
                       :exec acl2::bitarr$cp)
  :creator (create-invals :logic acl2::create-bitarr$a
                          :exec acl2::create-bitarr$c)
  :exports ((aignet-invals-length :logic acl2::bits$a-length
                                  :exec acl2::bits$c-length
                                  :protect nil)
            (get-aignet-inval :logic acl2::bits$ai
                              :exec acl2::bits$ci
                              :protect nil)
            (set-aignet-inval :logic acl2::update-bits$ai
                              :exec acl2::update-bits$ci
                              :protect nil)
            (resize-aignet-invals :logic acl2::resize-bits$a
                                  :exec acl2::resize-bits$c
                                  :protect nil))
  :congruent-to bitarr)

Definition: create-invals

(defabsstobj invals
  :foundation acl2::bitarr$c
  :recognizer (invalsp :logic acl2::bitarr$ap
                       :exec acl2::bitarr$cp)
  :creator (create-invals :logic acl2::create-bitarr$a
                          :exec acl2::create-bitarr$c)
  :exports ((aignet-invals-length :logic acl2::bits$a-length
                                  :exec acl2::bits$c-length
                                  :protect nil)
            (get-aignet-inval :logic acl2::bits$ai
                              :exec acl2::bits$ci
                              :protect nil)
            (set-aignet-inval :logic acl2::update-bits$ai
                              :exec acl2::update-bits$ci
                              :protect nil)
            (resize-aignet-invals :logic acl2::resize-bits$a
                                  :exec acl2::resize-bits$c
                                  :protect nil))
  :congruent-to bitarr)

Definition: aignet-invals-length

(defabsstobj invals
  :foundation acl2::bitarr$c
  :recognizer (invalsp :logic acl2::bitarr$ap
                       :exec acl2::bitarr$cp)
  :creator (create-invals :logic acl2::create-bitarr$a
                          :exec acl2::create-bitarr$c)
  :exports ((aignet-invals-length :logic acl2::bits$a-length
                                  :exec acl2::bits$c-length
                                  :protect nil)
            (get-aignet-inval :logic acl2::bits$ai
                              :exec acl2::bits$ci
                              :protect nil)
            (set-aignet-inval :logic acl2::update-bits$ai
                              :exec acl2::update-bits$ci
                              :protect nil)
            (resize-aignet-invals :logic acl2::resize-bits$a
                                  :exec acl2::resize-bits$c
                                  :protect nil))
  :congruent-to bitarr)

Definition: get-aignet-inval

(defabsstobj invals
  :foundation acl2::bitarr$c
  :recognizer (invalsp :logic acl2::bitarr$ap
                       :exec acl2::bitarr$cp)
  :creator (create-invals :logic acl2::create-bitarr$a
                          :exec acl2::create-bitarr$c)
  :exports ((aignet-invals-length :logic acl2::bits$a-length
                                  :exec acl2::bits$c-length
                                  :protect nil)
            (get-aignet-inval :logic acl2::bits$ai
                              :exec acl2::bits$ci
                              :protect nil)
            (set-aignet-inval :logic acl2::update-bits$ai
                              :exec acl2::update-bits$ci
                              :protect nil)
            (resize-aignet-invals :logic acl2::resize-bits$a
                                  :exec acl2::resize-bits$c
                                  :protect nil))
  :congruent-to bitarr)

Definition: set-aignet-inval

(defabsstobj invals
  :foundation acl2::bitarr$c
  :recognizer (invalsp :logic acl2::bitarr$ap
                       :exec acl2::bitarr$cp)
  :creator (create-invals :logic acl2::create-bitarr$a
                          :exec acl2::create-bitarr$c)
  :exports ((aignet-invals-length :logic acl2::bits$a-length
                                  :exec acl2::bits$c-length
                                  :protect nil)
            (get-aignet-inval :logic acl2::bits$ai
                              :exec acl2::bits$ci
                              :protect nil)
            (set-aignet-inval :logic acl2::update-bits$ai
                              :exec acl2::update-bits$ci
                              :protect nil)
            (resize-aignet-invals :logic acl2::resize-bits$a
                                  :exec acl2::resize-bits$c
                                  :protect nil))
  :congruent-to bitarr)

Definition: resize-aignet-invals

(defabsstobj invals
  :foundation acl2::bitarr$c
  :recognizer (invalsp :logic acl2::bitarr$ap
                       :exec acl2::bitarr$cp)
  :creator (create-invals :logic acl2::create-bitarr$a
                          :exec acl2::create-bitarr$c)
  :exports ((aignet-invals-length :logic acl2::bits$a-length
                                  :exec acl2::bits$c-length
                                  :protect nil)
            (get-aignet-inval :logic acl2::bits$ai
                              :exec acl2::bits$ci
                              :protect nil)
            (set-aignet-inval :logic acl2::update-bits$ai
                              :exec acl2::update-bits$ci
                              :protect nil)
            (resize-aignet-invals :logic acl2::resize-bits$a
                                  :exec acl2::resize-bits$c
                                  :protect nil))
  :congruent-to bitarr)