• 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-output-ranges
          • Aignet-comb-transforms
            • Fraig
            • Parametrize
              • Aignet-parametrize-output-ranges
              • Aignet-parametrize-copy-set-regs
              • Aignet-parametrize-copy-set-ins
              • Aignet-parametrize-collect-bdd-order-aux
              • Aignet-parametrize-collect-bdd-order
              • Aignet-output-range-conjoin-ubdds
              • Aignet-output-range-collect-in/reg-ubdd-order
              • Aignet-finish-reg-ubdd-order
              • Aignet-finish-in-ubdd-order
              • Aignet-copy-dfs-output-range
              • Aignet-parametrize-m-n
              • Aignet-node-to-ubdd
              • Aignet-output-range-to-ubdds
              • Ubdd-to-aignet
              • Aignet-parametrize-copy-init
              • Parametrize-config
              • Parametrize-output-type
              • Ubdd-arr-to-param-space
              • Copy-lits-compose
              • Bitarr-range-1bit-indices
              • Bitarr-range-count
              • Aignet-count-ubdd-branches-wrap
              • Ubdd-to-aignet-memo-ok
              • Aignet-node-to-ubdd-build-cond
              • Copy-lits-compose-in-place
              • Bitarr-range-set
              • Ubdd/level
              • Ubdd-arr
                • Set-ubdd
                • Resize-ubdds
                • Get-ubdd
                • Ubdds-length
                • Ubdd-arr-max-depth
                • Aignet-count-ubdd-branches
                • Ubdd-negate-cond
                • Ubdd-apply-gate
                • Aignet-node-to-ubdd-short-circuit-cond
                • Bits->bools
                • Eval-ubddarr
                • Ubdd-to-aignet-memo
                • Parametrize-output-type-map
                • Lubdd-fix
              • Observability-fix
              • Constprop
              • Apply-m-assumption-n-output-output-transform-default
              • Balance
              • Apply-n-output-comb-transform-default
              • Apply-comb-transform-default
              • Obs-constprop
              • Rewrite
              • Comb-transform
              • Abc-comb-simplify
              • Prune
              • Rewrite!
              • M-assumption-n-output-comb-transform->name
              • N-output-comb-transform->name
              • Comb-transform->name
              • N-output-comb-transformlist
              • M-assumption-n-output-comb-transformlist
              • Comb-transformlist
              • Apply-comb-transform
            • Aignet-m-assumption-n-output-transforms
            • Aignet-n-output-comb-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
    • Ubdd-arr

    Ubdds-length

    Get the length of the ubdd-arr array.

    In the execution this just gets the array length. The logical definition is just a wrapper for len:

    Function: ubdds$a-length

    (defun ubdds$a-length (ubdd-arr$a)
      (declare (xargs :guard (ubdd-arr$ap ubdd-arr$a)))
      (len ubdd-arr$a))