Interface DatatypeExpr<Name>

Readonlyctx

ast

• get ast(): Z3_ast

• Returns Z3_ast

sort

• get sort(): S

• Returns S

arg

• arg(i: number): AnyExpr<Name>

• Parameters

  • i: number

  Returns AnyExpr<Name>

children

• children(): AnyExpr<Name>[]

• Returns AnyExpr<Name>[]

decl

• decl(): FuncDecl<Name, Sort<Name>[], Sort<Name>>

• Returns FuncDecl<Name, Sort<Name>[], Sort<Name>>

eq

• eq(other: CoercibleToExpr<Name>): Bool<Name>

• Parameters

  • other: CoercibleToExpr<Name>

  Returns Bool<Name>

eqIdentity

• eqIdentity(other: Ast<Name, unknown>): boolean

• Parameters

  • other: Ast<Name, unknown>

  Returns boolean

hash

• hash(): number

• Returns number

id

• id(): number

• Returns number

name

• name(): string | number

• Returns string | number

neq

• neq(other: CoercibleToExpr<Name>): Bool<Name>

• Parameters

  • other: CoercibleToExpr<Name>

  Returns Bool<Name>

neqIdentity

• neqIdentity(other: Ast<Name, unknown>): boolean

• Parameters

  • other: Ast<Name, unknown>

  Returns boolean

numArgs

• numArgs(): number

• Returns number

params

• params(): (
      | string
      | number
      | Sort<Name>
      | Expr<Name, AnySort<Name>, unknown>
      | FuncDecl<Name, Sort<Name>[], Sort<Name>>
  )[]

• Returns (
      | string
      | number
      | Sort<Name>
      | Expr<Name, AnySort<Name>, unknown>
      | FuncDecl<Name, Sort<Name>[], Sort<Name>>
  )[]

sexpr

• sexpr(): string

• Returns string