Interface BitVecNum<Bits, Name>

Represents Bit Vector constant value

interface BitVecNum<Bits extends number = number, Name extends string = "main"> {
    ctx: Context<Name>;
    get ast(): Z3_ast;
    get sort(): S;
    add(other: CoercibleToBitVec<Bits, Name>): BitVec<Bits, Name>;
    addNoOverflow(
        other: CoercibleToBitVec<Bits, Name>,
        isSigned: boolean,
    ): Bool<Name>;
    addNoUnderflow(other: CoercibleToBitVec<Bits, Name>): Bool<Name>;
    and(other: CoercibleToBitVec<Bits, Name>): BitVec<Bits, Name>;
    arg(i: number): AnyExpr<Name>;
    asBinaryString(): string;
    asSignedValue(): bigint;
    asString(): string;
    children(): AnyExpr<Name>[];
    decl(): FuncDecl<Name, Sort<Name>[], Sort<Name>>;
    eq(other: CoercibleToExpr<Name>): Bool<Name>;
    eqIdentity(other: Ast<Name, unknown>): boolean;
    extract(high: number, low: number): BitVec<number, Name>;
    hash(): number;
    id(): number;
    lshr(count: CoercibleToBitVec<Bits, Name>): BitVec<Bits, Name>;
    mul(other: CoercibleToBitVec<Bits, Name>): BitVec<Bits, Name>;
    mulNoOverflow(
        other: CoercibleToBitVec<Bits, Name>,
        isSigned: boolean,
    ): Bool<Name>;
    mulNoUndeflow(other: CoercibleToBitVec<Bits, Name>): Bool<Name>;
    name(): string | number;
    nand(other: CoercibleToBitVec<Bits, Name>): BitVec<Bits, Name>;
    neg(): BitVec<Bits, Name>;
    negNoOverflow(): Bool<Name>;
    neq(other: CoercibleToExpr<Name>): Bool<Name>;
    neqIdentity(other: Ast<Name, unknown>): boolean;
    not(): BitVec<Bits, Name>;
    numArgs(): number;
    or(other: CoercibleToBitVec<Bits, Name>): BitVec<Bits, Name>;
    params(): (
        | string
        | number
        | Sort<Name>
        | FuncDecl<Name, Sort<Name>[], Sort<Name>>
        | Expr<Name, AnySort<Name>, unknown>
    )[];
    redAnd(): BitVec<number, Name>;
    redOr(): BitVec<number, Name>;
    repeat(count: number): BitVec<number, Name>;
    rotateLeft(count: CoercibleToBitVec<number, Name>): BitVec<Bits, Name>;
    rotateRight(count: CoercibleToBitVec<number, Name>): BitVec<Bits, Name>;
    sdiv(other: CoercibleToBitVec<Bits, Name>): BitVec<Bits, Name>;
    sdivNoOverflow(other: CoercibleToBitVec<Bits, Name>): Bool<Name>;
    sexpr(): string;
    sge(other: CoercibleToBitVec<Bits, Name>): Bool<Name>;
    sgt(other: CoercibleToBitVec<Bits, Name>): Bool<Name>;
    shl(count: CoercibleToBitVec<Bits, Name>): BitVec<Bits, Name>;
    shr(count: CoercibleToBitVec<Bits, Name>): BitVec<Bits, Name>;
    signExt(count: number): BitVec<number, Name>;
    size(): Bits;
    sle(other: CoercibleToBitVec<Bits, Name>): Bool<Name>;
    slt(other: CoercibleToBitVec<Bits, Name>): Bool<Name>;
    smod(other: CoercibleToBitVec<Bits, Name>): BitVec<Bits, Name>;
    srem(other: CoercibleToBitVec<Bits, Name>): BitVec<Bits, Name>;
    sub(other: CoercibleToBitVec<Bits, Name>): BitVec<Bits, Name>;
    subNoOverflow(other: CoercibleToBitVec<Bits, Name>): Bool<Name>;
    subNoUndeflow(
        other: CoercibleToBitVec<Bits, Name>,
        isSigned: boolean,
    ): Bool<Name>;
    udiv(other: CoercibleToBitVec<Bits, Name>): BitVec<Bits, Name>;
    uge(other: CoercibleToBitVec<Bits, Name>): Bool<Name>;
    ugt(other: CoercibleToBitVec<Bits, Name>): Bool<Name>;
    ule(other: CoercibleToBitVec<Bits, Name>): Bool<Name>;
    ult(other: CoercibleToBitVec<Bits, Name>): Bool<Name>;
    urem(other: CoercibleToBitVec<Bits, Name>): BitVec<Bits, Name>;
    value(): bigint;
    xnor(other: CoercibleToBitVec<Bits, Name>): BitVec<Bits, Name>;
    xor(other: CoercibleToBitVec<Bits, Name>): BitVec<Bits, Name>;
    zeroExt(count: number): BitVec<number, Name>;
}

Type Parameters

  • Bits extends number = number
  • Name extends string = "main"

Hierarchy (View Summary)

Arithmetic

add mul neg sdiv smod srem sub udiv urem

Bitwise

and lshr nand not rotateLeft rotateRight shl shr xnor xor

Boolean

addNoOverflow addNoUnderflow mulNoOverflow mulNoUndeflow negNoOverflow sdivNoOverflow subNoOverflow subNoUndeflow

Comparison

sge sgt sle slt uge ugt ule ult

Other

ctx ast sort arg asBinaryString asSignedValue asString children decl eq eqIdentity extract hash id name neq neqIdentity numArgs or params redAnd redOr repeat sexpr signExt size value zeroExt

Arithmetic

add

mul

neg

sdiv

smod

srem

sub

udiv

urem

Bitwise

and

lshr

nand

not

rotateLeft

rotateRight

shl

shr

xnor

xor

Boolean

addNoOverflow

addNoUnderflow

mulNoOverflow

mulNoUndeflow

negNoOverflow

sdivNoOverflow

subNoOverflow

subNoUndeflow

Comparison

sge

sgt

sle

slt

uge

ugt

ule

ult

Other

Readonlyctx

ctx: Context<Name>

ast

sort

arg

asBinaryString

asSignedValue

asString

children

decl

eq

eqIdentity

extract

  • extract(high: number, low: number): BitVec<number, Name>

  • Creates an extraction operation. Bits are indexed starting from 1 from the most right one (least significant) increasing to left (most significant)

    const x = BitVec.const('x', 8);

    x.extract(6, 2)
    // Extract(6, 2, x)
    x.extract(6, 2).sort
    // BitVec(5)

    Parameters

    • high: number

      The most significant bit to be extracted

    • low: number

      The least significant bit to be extracted

    Returns BitVec<number, Name>

hash

id

name

neq

neqIdentity

numArgs

or

params

redAnd

redOr

repeat

sexpr

signExt

size

  • size(): Bits

  • The amount of bits of this BitVectors sort

    const x = BitVec.const('x', 32);

    x.size
    // 32

    const Y = BitVec.sort(8);
    const y = BitVec.const('y', Y);

    y.size
    // 8

    Returns Bits

value

zeroExt

Settings

Member Visibility

On This Page

Arithmetic
Bitwise
Boolean
Comparison
Other