• Top
    • Documentation
    • Books
    • Boolean-reasoning
    • Projects
    • Debugging
    • Std
    • Proof-automation
    • Macro-libraries
    • ACL2
    • Interfacing-tools
    • Hardware-verification
      • Gl
      • Esim
      • Vl2014
      • Sv
        • Svex-stvs
        • Svex-decomposition-methodology
        • Sv-versus-esim
        • Svex-decomp
        • Svex-compose-dfs
        • Svex-compilation
        • Moddb
        • Svmods
        • Svstmt
        • Sv-tutorial
        • Expressions
          • Rewriting
          • Svex
          • Bit-blasting
            • Svex-focused-equivalence-checking
            • A4vec-operations
              • Aig-head-tail-concat-aux
              • A4vec-part-install
              • Aig-rev-blocks-sss
              • A4vec-wildeq-safe-aux
              • A4vec-concat
              • Aig-overlap-width-ss-aux
              • A4vec-wildeq-aux
              • A4vec-part-select
              • A4vec-rsh
              • A4vec-mask-check
              • Aig-head-of-concat
              • A4vec-===*-aux
              • A4vec-sign-ext
              • A4vec-rev-blocks
              • A3vec-bit?
              • A4vec-zero-ext
              • A3vec-?*
              • A3vec-?
              • A4vec-lsh
              • A4vec-bit?!
              • A4vec-?!
              • Aig-scons-with-hint
              • A4vec-override
              • A4vec-symwildeq
              • A4vec-remainder
              • A4vec-pow
              • A4vec-bit-extract
              • A4vec-wildeq-safe
              • A4vec-quotient
              • A4vec-mask
              • Aig-list->s-upper-bound
              • A4vec-wildeq
              • A4vec-resor
              • A4vec-resand
              • A3vec-bitxor
              • A4vec-times
              • A4vec-syntactic-3vec-p
              • A4vec-plus
              • A4vec-minus
              • A3vec-bitor
              • A3vec-bitand
              • A4vec-===*
              • A4vec-===
              • A4vec-<
              • A4vec-res
              • Aig-list->s-lower-bound
              • A3vec-==
              • A4vec-parity
              • 4vec->a4vec
              • Aig-force-sign-s
              • A4vec-wildeq-safe-bit
              • A4vec-onehot0
              • A4vec-onehot
              • A4vec-countones
              • A3vec-reduction-or
              • A3vec-reduction-and
              • A2vec-p
              • Aig-countones-aux
              • A4vec-uminus
              • A4vec-clog2
              • A3vec-fix
              • Aig-onehot-aux
              • A4vec-xdet
              • A4vec-onset
              • A4vec-offset
              • A3vec-bitnot
              • Aig-iszero-s
              • A4vec-wildeq-bit
              • A4vec-ite
                • A4vec-ite-fn
              • Aig-sterm-with-hint
              • A4vec-===*-bit
              • A4vec-x
              • A4vec-1x
              • A4vec-0
              • And4
            • Svexlist-eval-gl
            • Aig-symbolic-arithmetic
            • Svex-varmasks/env->aig-env-rec
            • Svex-varmasks->a4env-rec
            • Svexlist/env-list-eval-gl
            • 4vmask-to-a4vec-rec-env
            • 4vmask-to-a4vec-rec
            • Svexlist->a4vecs-for-varlist
            • Svex-varmasks/env->aig-env-stats-rec
            • Svexlist->a4vec-nrev
            • A4veclist/svex-env-list-eval
            • A4vec
            • Svexlist-x-out-unused-vars
            • Svex->a4vec-memotable-correctp
            • A4vec/svex-env-eval
            • Svex-varmasks->a4env
            • Svex-varmasks/env->aig-env-rec-log
            • 4vmask-to-a4vec-env
            • 4veclist-from-bitlist-log-rec
            • Svex-apply-aig
            • Svexlist-vars-for-symbolic-eval
            • Nat-bool-a4env-upper-boundp
            • 4vmask-to-a4vec
            • Svexlist/env-list-vars-for-symbolic-eval
            • Svex-maskbits-for-vars
            • Svexlist->a4vec-aig-env-for-varlist
            • 4vec-from-bitlist
            • Svexlist-full-masks-p
            • Svex-varmasks/env->aig-env-stats
            • Svex-varmasks/env->aig-env
            • Svexlistlist->a4vec
            • Svex-const-concat-args
            • Svex-mask-alist-extract-vars
            • Svexlist->a4vec-top
            • Nat-bool-a4vec-upper-boundp
            • Nat-bool-a4env-lower-boundp
            • Maybe-a3vec-fix
            • Svex-maskbits-ok
            • Svex-envlist-check-boolmasks
            • Svex-env-check-boolmasks
            • Nat-bool-list-upper-boundp
            • Nat-bool-a4vec-lower-boundp
            • Maybe-svexlist-rewrite-fixpoint
            • 4vmask-to-a4vec-varcount
            • A4vec-eval
            • Svexlist-nth
            • A4veclist-nth
            • Nat-bool-list-lower-boundp
            • 4veclist-from-bitlist
            • V2i-first-n
            • A4veclist-eval-gl
            • Svex-envlist-keyset
            • Svex-a4vec-env-eval
            • A4veclist/env-list-eval
            • Svexlist-variable-mask-alist
            • Sparseint-nfix
            • A4veclist-length
            • A4veclist-eval
            • 4vec-boolmaskp
            • Nat-bool-list-nats
            • Nat-bool-a4env-p
            • Nat-bool-listp
            • A4veclist->aiglist
            • Svexlist-rewrite-fixpoint-memo
            • Nat-bool-a4vec-p
            • A4vec->aiglist
            • Svex-is-const-concat
            • Nat-bool-a4env-vars
            • Svexlist-mask-alist-memo
            • Nat-bool-a4vec-vars
            • Svexlist-vars-memo
            • A4vec-constantp
            • Svex-aig-memotable
            • Svex-a4vec-env
            • A4veclistlist
            • A4veclist
            • Symbolic-params-x-out-cond
          • Functions
          • 4vmask
          • Why-infinite-width
          • Svex-vars
          • Evaluation
          • Values
        • Symbolic-test-vector
        • Vl-to-svex
      • Fgl
      • Vwsim
      • Vl
      • X86isa
      • Svl
      • Rtl
    • Software-verification
    • Math
    • Testing-utilities
  • A4vec-operations

A4vec-ite

Lazy macro for if-then-else of symbolic 4vecs.

(a4vec-ite test then else) --> ans
  • test is a single AIG, not an a4vec.
  • then and else are a4vecs.
  • ans is also an a4vec.

This is widely used in the implementation of our a4vec-operations. It is similar in spirit to ACL2::q-ite; we try to avoid evaluating then or else if we can resolve test.

Subtopics

A4vec-ite-fn
Basic if-then-else for symbolic 4vecs.