Interface Arith<Name>

Represents Integer or Real number expression

interface Arith<Name extends string = "main"> {
    ctx: Context<Name>;
    get ast(): Z3_ast;
    get sort(): S;
    add(other: CoercibleToArith<Name>): Arith<Name>;
    arg(i: number): AnyExpr<Name>;
    children(): AnyExpr<Name>[];
    decl(): FuncDecl<Name, Sort<Name>[], Sort<Name>>;
    div(other: CoercibleToArith<Name>): Arith<Name>;
    eq(other: CoercibleToExpr<Name>): Bool<Name>;
    eqIdentity(other: Ast<Name, unknown>): boolean;
    ge(other: CoercibleToArith<Name>): Bool<Name>;
    gt(other: CoercibleToArith<Name>): Bool<Name>;
    hash(): number;
    id(): number;
    le(other: CoercibleToArith<Name>): Bool<Name>;
    lt(other: CoercibleToArith<Name>): Bool<Name>;
    mod(other: CoercibleToArith<Name>): Arith<Name>;
    mul(other: CoercibleToArith<Name>): Arith<Name>;
    name(): string | number;
    neg(): Arith<Name>;
    neq(other: CoercibleToExpr<Name>): Bool<Name>;
    neqIdentity(other: Ast<Name, unknown>): boolean;
    numArgs(): number;
    params(): (
        | string
        | number
        | Sort<Name>
        | Expr<Name, AnySort<Name>, unknown>
        | FuncDecl<Name, Sort<Name>[], Sort<Name>>
    )[];
    pow(exponent: CoercibleToArith<Name>): Arith<Name>;
    sexpr(): string;
    sub(other: CoercibleToArith<Name>): Arith<Name>;
}

Type Parameters

Name extends string = "main"

Hierarchy (View Summary)

Expr<Name, ArithSort<Name>, Z3_ast>
- Arith
  - IntNum
  - RatNum

Index

Properties

`Readonly`ctx

ctx: Context<Name>

Accessors

ast

get ast(): Z3_ast
Returns Z3_ast
Inherited from Expr.ast
- Defined in src/high-level/types.ts:689

sort

get sort(): S
Returns S
Inherited from Expr.sort
- Defined in src/high-level/types.ts:1081

Methods

add

add(other: CoercibleToArith<Name>): Arith<Name>
Adds two numbers together
Parameters
- other: CoercibleToArith<Name>
Returns Arith<Name>
- Defined in src/high-level/types.ts:1208

arg

arg(i: number): AnyExpr<Name>
Parameters
- i: number
Returns AnyExpr<Name>
Inherited from Expr.arg
- Defined in src/high-level/types.ts:1095

children

children(): AnyExpr<Name>[]
Returns AnyExpr<Name>[]
Inherited from Expr.children
- Defined in src/high-level/types.ts:1097

decl

decl(): FuncDecl<Name, Sort<Name>[], Sort<Name>>
Returns FuncDecl<Name, Sort<Name>[], Sort<Name>>
Inherited from Expr.decl
- Defined in src/high-level/types.ts:1091

div

div(other: CoercibleToArith<Name>): Arith<Name>
Divides the number by the second one
Parameters
- other: CoercibleToArith<Name>
Returns Arith<Name>
- Defined in src/high-level/types.ts:1235

eq

eq(other: CoercibleToExpr<Name>): Bool<Name>
Parameters
- other: CoercibleToExpr<Name>
Returns Bool<Name>
Inherited from Expr.eq
- Defined in src/high-level/types.ts:1083

eqIdentity

eqIdentity(other: Ast<Name, unknown>): boolean
Parameters
- other: Ast<Name, unknown>
Returns boolean
Inherited from Expr.eqIdentity
- Defined in src/high-level/types.ts:694

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>
- Defined in src/high-level/types.ts:1272

gt

gt(other: CoercibleToArith<Name>): Bool<Name>
Returns whether the number is greater than the second one (>)
Parameters
- other: CoercibleToArith<Name>
Returns Bool<Name>
- Defined in src/high-level/types.ts:1267

hash

hash(): number
Returns number
Inherited from Expr.hash
- Defined in src/high-level/types.ts:700

id

id(): number
Returns number
Inherited from Expr.id
- Defined in src/high-level/types.ts:692

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>
- Defined in src/high-level/types.ts:1257

lt

lt(other: CoercibleToArith<Name>): Bool<Name>
Returns whether the number is less than the second one (<)
Parameters
- other: CoercibleToArith<Name>
Returns Bool<Name>
- Defined in src/high-level/types.ts:1262

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
```
Parameters
- other: CoercibleToArith<Name>
Returns Arith<Name>
- Defined in src/high-level/types.ts:1247

mul

mul(other: CoercibleToArith<Name>): Arith<Name>
Multiplies two numbers together
Parameters
- other: CoercibleToArith<Name>
Returns Arith<Name>
- Defined in src/high-level/types.ts:1213

name

name(): string | number
Returns string | number
Inherited from Expr.name
- Defined in src/high-level/types.ts:1089

neg

neg(): Arith<Name>
Returns a negation of the number

Returns Arith<Name>
- Defined in src/high-level/types.ts:1252

neq

neq(other: CoercibleToExpr<Name>): Bool<Name>
Parameters
- other: CoercibleToExpr<Name>
Returns Bool<Name>
Inherited from Expr.neq
- Defined in src/high-level/types.ts:1085

neqIdentity

neqIdentity(other: Ast<Name, unknown>): boolean
Parameters
- other: Ast<Name, unknown>
Returns boolean
Inherited from Expr.neqIdentity
- Defined in src/high-level/types.ts:696

numArgs

numArgs(): number
Returns number
Inherited from Expr.numArgs
- Defined in src/high-level/types.ts:1093

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>>
)[]
Inherited from Expr.params
- Defined in src/high-level/types.ts:1087

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
```
Parameters
- exponent: CoercibleToArith<Name>
Returns Arith<Name>
- Defined in src/high-level/types.ts:1230

sexpr

sexpr(): string
Returns string
Inherited from Expr.sexpr
- Defined in src/high-level/types.ts:698

sub

sub(other: CoercibleToArith<Name>): Arith<Name>
Subtract second number from the first one
Parameters
- other: CoercibleToArith<Name>
Returns Arith<Name>
- Defined in src/high-level/types.ts:1218

Interface Arith<Name>

Type Parameters

Hierarchy (View Summary)

Index

Properties

Accessors

Methods

Properties

Readonlyctx

Accessors

ast

Returns Z3_ast

sort

Returns S

Methods

add

Parameters

Returns Arith<Name>

arg

Parameters

Returns AnyExpr<Name>

children

Returns AnyExpr<Name>[]

decl

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

div

Parameters

Returns Arith<Name>

eq

Parameters

Returns Bool<Name>

eqIdentity

Parameters

Returns boolean

ge

Parameters

Returns Bool<Name>

gt

Parameters

Returns Bool<Name>

hash

Returns number

id

Returns number

le

Parameters

Returns Bool<Name>

lt

Parameters

Returns Bool<Name>

mod

Parameters

Returns Arith<Name>

mul

Parameters

Returns Arith<Name>

name

Returns string | number

neg

Returns Arith<Name>

neq

Parameters

Returns Bool<Name>

neqIdentity

Parameters

Returns boolean

numArgs

Returns number

params

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

pow

Parameters

Returns Arith<Name>

sexpr

Returns string

sub

Parameters

Returns Arith<Name>

Settings

On This Page

`Readonly`ctx

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