• Top
    • Documentation
    • Books
    • Recursion-and-induction
    • Boolean-reasoning
      • Ipasir
      • Aignet
        • Base-api
        • Aignet-construction
        • Representation
        • Aignet-copy-init
        • Aignet-simplify-marked-with-tracking
        • Aignet-cnf
        • Aignet-simplify-with-tracking
        • Aignet-complete-copy
        • Aignet-eval
        • Semantics
          • Comb-equiv
          • Seq-equiv
          • Seq-equiv-init
          • Invals
            • Outs-comb-equiv
            • Nxsts-comb-equiv
          • Aignet-transforms
          • Aignet-simplify-marked
          • Aignet-read-aiger
          • Aignet-write-aiger
          • Aignet-abc-interface
          • Utilities
        • Aig
        • Satlink
        • Truth
        • Ubdds
        • Bdd
        • Faig
        • Bed
        • 4v
      • Debugging
      • Projects
      • Std
      • Proof-automation
      • Macro-libraries
      • ACL2
      • Interfacing-tools
      • Hardware-verification
      • Software-verification
      • Testing-utilities
      • Math
    • 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)