Interface IntNum<Name>

Readonlyctx

ast

• get ast(): Z3_ast

• Returns Z3_ast

sort

• get sort(): S

• Returns S

add

• add(other: CoercibleToArith<Name>): Arith<Name>

• Adds two numbers together

  Parameters

  • other: CoercibleToArith<Name>

  Returns Arith<Name>

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>>

div

• div(other: CoercibleToArith<Name>): Arith<Name>

• Divides the number by the second one

  Parameters

  • other: CoercibleToArith<Name>

  Returns Arith<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

ge

• ge(other: CoercibleToArith<Name>): Bool<Name>

• Returns whether the number is greater or equal than the second one (>=)

  Parameters

  • other: CoercibleToArith<Name>

  Returns Bool<Name>

gt

• gt(other: CoercibleToArith<Name>): Bool<Name>

• Returns whether the number is greater than the second one (>)

  Parameters

  • other: CoercibleToArith<Name>

  Returns Bool<Name>

hash

• hash(): number

• Returns number

id

• id(): number

• Returns number

le

• le(other: CoercibleToArith<Name>): Bool<Name>

• Return whether the number is less or equal than the second one (<=)

  Parameters

  • other: CoercibleToArith<Name>

  Returns Bool<Name>

lt

• lt(other: CoercibleToArith<Name>): Bool<Name>

• Returns whether the number is less than the second one (<)

  Parameters

  • other: CoercibleToArith<Name>

  Returns Bool<Name>

mod

• mod(other: CoercibleToArith<Name>): Arith<Name>

• Returns a number modulo second one

  const x = Int.const('x');
  
  await solve(x.mod(7).eq(1), x.gt(7)) // x % 7 == 1, x > 7
  // x=8
  Copy

  Parameters

  • other: CoercibleToArith<Name>

  Returns Arith<Name>

mul

• mul(other: CoercibleToArith<Name>): Arith<Name>

• Multiplies two numbers together

  Parameters

  • other: CoercibleToArith<Name>

  Returns Arith<Name>

name

• name(): string | number

• Returns string | number

neg

• neg(): Arith<Name>

• Returns a negation of the number

  Returns Arith<Name>

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>
      | FuncDecl<Name, Sort<Name>[], Sort<Name>>
      | Expr<Name, AnySort<Name>, unknown>
  )[]

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

pow

• pow(exponent: CoercibleToArith<Name>): Arith<Name>

• Applies power to the number

  const x = Int.const('x');
  
  await solve(x.pow(2).eq(4), x.lt(0)); // x**2 == 4, x < 0
  // x=-2
  Copy

  Parameters

  • exponent: CoercibleToArith<Name>

  Returns Arith<Name>

sexpr

• sexpr(): string

• Returns string

sub

• sub(other: CoercibleToArith<Name>): Arith<Name>

• Subtract second number from the first one

  Parameters

  • other: CoercibleToArith<Name>

  Returns Arith<Name>