Interface RatNum<Name>

A constant Rational value expression

const num = Real.val('1/3');

num.asString()
// '1/3'
num.value
// { numerator: 1n, denominator: 3n }
num.asNumber()
// 0.3333333333333333

interface RatNum<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>;
    asDecimal(prec?: number): string;
    asNumber(): number;
    asString(): string;
    children(): AnyExpr<Name>[];
    decl(): FuncDecl<Name, Sort<Name>[], Sort<Name>>;
    denominator(): IntNum<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;
    numerator(): IntNum<Name>;
    params(): (
        | string
        | number
        | Sort<Name>
        | FuncDecl<Name, Sort<Name>[], Sort<Name>>
        | Expr<Name, AnySort<Name>, unknown>
    )[];
    pow(exponent: CoercibleToArith<Name>): Arith<Name>;
    sexpr(): string;
    sub(other: CoercibleToArith<Name>): Arith<Name>;
    value(): { denominator: bigint; numerator: bigint };
}

Type Parameters

Name extends string = "main"

Hierarchy (View Summary)

Arith<Name>
- RatNum

Index

Properties

`Readonly`ctx

ctx: Context<Name>

Accessors

ast

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

sort

get sort(): S
Returns S
Inherited from Arith.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>
Inherited from Arith.add
- Defined in src/high-level/types.ts:1208

arg

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

asDecimal

asDecimal(prec?: number): string
Parameters
- Optionalprec: number
Returns string
- Defined in src/high-level/types.ts:1317

asNumber

asNumber(): number
Returns number
- Defined in src/high-level/types.ts:1315

asString

asString(): string
Returns string
- Defined in src/high-level/types.ts:1319

children

children(): AnyExpr<Name>[]
Returns AnyExpr<Name>[]
Inherited from Arith.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 Arith.decl
- Defined in src/high-level/types.ts:1091

denominator

denominator(): IntNum<Name>
Returns IntNum<Name>
- Defined in src/high-level/types.ts:1313

div

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

eq

eq(other: CoercibleToExpr<Name>): Bool<Name>
Parameters
- other: CoercibleToExpr<Name>
Returns Bool<Name>
Inherited from Arith.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 Arith.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>
Inherited from Arith.ge
- 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>
Inherited from Arith.gt
- Defined in src/high-level/types.ts:1267

hash

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

id

id(): number
Returns number
Inherited from Arith.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>
Inherited from Arith.le
- 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>
Inherited from Arith.lt
- 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>
Inherited from Arith.mod
- 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>
Inherited from Arith.mul
- Defined in src/high-level/types.ts:1213

name

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

neg

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

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

neq

neq(other: CoercibleToExpr<Name>): Bool<Name>
Parameters
- other: CoercibleToExpr<Name>
Returns Bool<Name>
Inherited from Arith.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 Arith.neqIdentity
- Defined in src/high-level/types.ts:696

numArgs

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

numerator

numerator(): IntNum<Name>
Returns IntNum<Name>
- Defined in src/high-level/types.ts:1311

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>
)[]
Inherited from Arith.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>
Inherited from Arith.pow
- Defined in src/high-level/types.ts:1230

sexpr

sexpr(): string
Returns string
Inherited from Arith.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>
Inherited from Arith.sub
- Defined in src/high-level/types.ts:1218

value

value(): { denominator: bigint; numerator: bigint }
Returns { denominator: bigint; numerator: bigint }
- Defined in src/high-level/types.ts:1309

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

asDecimal

Parameters

Returns string

asNumber

Returns number

asString

Returns string

children

Returns AnyExpr<Name>[]

decl

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

denominator

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

numerator

Returns IntNum<Name>

params

`Readonly`ctx

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