mirror of
https://github.com/Z3Prover/z3
synced 2026-01-19 08:43:18 +00:00
Add Floating-Point and String/Sequence APIs to TypeScript bindings (#8135)
* Initial plan * Add FP and String/Seq type definitions to TypeScript bindings Co-authored-by: NikolajBjorner <3085284+NikolajBjorner@users.noreply.github.com> * Implement FP and String/Seq in TypeScript high-level bindings Co-authored-by: NikolajBjorner <3085284+NikolajBjorner@users.noreply.github.com> * Add comprehensive tests for FP and String/Seq APIs Co-authored-by: NikolajBjorner <3085284+NikolajBjorner@users.noreply.github.com> * Fix build errors: Add isFP to test scope and use eqIdentity for Sort comparison Co-authored-by: NikolajBjorner <3085284+NikolajBjorner@users.noreply.github.com> * Fix code formatting with Prettier for WASM build Co-authored-by: NikolajBjorner <3085284+NikolajBjorner@users.noreply.github.com> * Fix FPNum.value() to use Z3_get_numeral_double instead of parsing string Co-authored-by: NikolajBjorner <3085284+NikolajBjorner@users.noreply.github.com> * Simplify length check for empty sequence Refactor length check for empty sequence in tests. --------- Co-authored-by: copilot-swe-agent[bot] <198982749+Copilot@users.noreply.github.com> Co-authored-by: NikolajBjorner <3085284+NikolajBjorner@users.noreply.github.com> Co-authored-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Copilot
GitHub
parent
05994345cb
commit
d7579706e2
3 changed files with 1187 additions and 4 deletions
|
|
@ -1051,7 +1051,6 @@ describe('high-level', () => {
|
|||
expect(nonUnits).toBeDefined();
|
||||
expect(nonUnits.length()).toBeGreaterThanOrEqual(0);
|
||||
});
|
||||
|
||||
});
|
||||
|
||||
describe('solver congruence closure APIs', () => {
|
||||
|
|
@ -1196,4 +1195,325 @@ describe('high-level', () => {
|
|||
expect(typeof solver.fromFile).toBe('function');
|
||||
});
|
||||
});
|
||||
|
||||
describe('floating-point', () => {
|
||||
it('can create FP sorts', () => {
|
||||
const { Float } = api.Context('main');
|
||||
|
||||
const fp16 = Float.sort16();
|
||||
expect(fp16.ebits()).toBe(5);
|
||||
expect(fp16.sbits()).toBe(11);
|
||||
|
||||
const fp32 = Float.sort32();
|
||||
expect(fp32.ebits()).toBe(8);
|
||||
expect(fp32.sbits()).toBe(24);
|
||||
|
||||
const fp64 = Float.sort64();
|
||||
expect(fp64.ebits()).toBe(11);
|
||||
expect(fp64.sbits()).toBe(53);
|
||||
|
||||
const fp128 = Float.sort128();
|
||||
expect(fp128.ebits()).toBe(15);
|
||||
expect(fp128.sbits()).toBe(113);
|
||||
|
||||
const custom = Float.sort(5, 10);
|
||||
expect(custom.ebits()).toBe(5);
|
||||
expect(custom.sbits()).toBe(10);
|
||||
});
|
||||
|
||||
it('can create FP rounding modes', () => {
|
||||
const { FloatRM } = api.Context('main');
|
||||
|
||||
const rne = FloatRM.RNE();
|
||||
const rna = FloatRM.RNA();
|
||||
const rtp = FloatRM.RTP();
|
||||
const rtn = FloatRM.RTN();
|
||||
const rtz = FloatRM.RTZ();
|
||||
|
||||
expect(rne.toString()).toContain('roundNearestTiesToEven');
|
||||
});
|
||||
|
||||
it('can create FP constants and values', () => {
|
||||
const { Float, FloatRM } = api.Context('main');
|
||||
const fp32 = Float.sort32();
|
||||
|
||||
const x = Float.const('x', fp32);
|
||||
expect(x.sort.ebits()).toBe(8);
|
||||
expect(x.sort.sbits()).toBe(24);
|
||||
|
||||
const val = Float.val(3.14, fp32);
|
||||
expect(val.value()).toBeCloseTo(3.14, 2);
|
||||
|
||||
const nan = Float.NaN(fp32);
|
||||
const inf = Float.inf(fp32);
|
||||
const negInf = Float.inf(fp32, true);
|
||||
const zero = Float.zero(fp32);
|
||||
const negZero = Float.zero(fp32, true);
|
||||
|
||||
expect(typeof nan.value()).toBe('number');
|
||||
expect(typeof inf.value()).toBe('number');
|
||||
});
|
||||
|
||||
it('can perform FP arithmetic', async () => {
|
||||
const { Float, FloatRM, Solver } = api.Context('main');
|
||||
const fp32 = Float.sort32();
|
||||
const rm = FloatRM.RNE();
|
||||
|
||||
const x = Float.const('x', fp32);
|
||||
const y = Float.const('y', fp32);
|
||||
|
||||
const sum = x.add(rm, y);
|
||||
const diff = x.sub(rm, y);
|
||||
const prod = x.mul(rm, y);
|
||||
const quot = x.div(rm, y);
|
||||
|
||||
const solver = new Solver();
|
||||
solver.add(x.eq(Float.val(2.0, fp32)));
|
||||
solver.add(y.eq(Float.val(3.0, fp32)));
|
||||
solver.add(sum.eq(Float.val(5.0, fp32)));
|
||||
|
||||
const result = await solver.check();
|
||||
expect(result).toBe('sat');
|
||||
});
|
||||
|
||||
it('can perform FP comparisons', async () => {
|
||||
const { Float, FloatRM, Solver, isFP } = api.Context('main');
|
||||
const fp32 = Float.sort32();
|
||||
|
||||
const x = Float.const('x', fp32);
|
||||
const two = Float.val(2.0, fp32);
|
||||
const three = Float.val(3.0, fp32);
|
||||
|
||||
const solver = new Solver();
|
||||
solver.add(x.gt(two));
|
||||
solver.add(x.lt(three));
|
||||
|
||||
const result = await solver.check();
|
||||
expect(result).toBe('sat');
|
||||
|
||||
const model = solver.model();
|
||||
const xVal = model.eval(x);
|
||||
expect(isFP(xVal)).toBe(true);
|
||||
});
|
||||
|
||||
it('can use FP predicates', async () => {
|
||||
const { Float, Solver, isFP } = api.Context('main');
|
||||
const fp32 = Float.sort32();
|
||||
|
||||
const x = Float.const('x', fp32);
|
||||
const nan = Float.NaN(fp32);
|
||||
const inf = Float.inf(fp32);
|
||||
const zero = Float.zero(fp32);
|
||||
|
||||
// Test NaN predicate
|
||||
{
|
||||
const solver = new Solver();
|
||||
solver.add(x.eq(nan));
|
||||
solver.add(x.isNaN());
|
||||
expect(await solver.check()).toBe('sat');
|
||||
}
|
||||
|
||||
// Test infinity predicate
|
||||
{
|
||||
const solver = new Solver();
|
||||
solver.add(x.eq(inf));
|
||||
solver.add(x.isInf());
|
||||
expect(await solver.check()).toBe('sat');
|
||||
}
|
||||
|
||||
// Test zero predicate
|
||||
{
|
||||
const solver = new Solver();
|
||||
solver.add(x.eq(zero));
|
||||
solver.add(x.isZero());
|
||||
expect(await solver.check()).toBe('sat');
|
||||
}
|
||||
});
|
||||
|
||||
it('supports FP type checking', () => {
|
||||
const { Float, FloatRM, isFPSort, isFP, isFPVal, isFPRMSort, isFPRM } = api.Context('main');
|
||||
const fp32 = Float.sort32();
|
||||
const rmSort = FloatRM.sort();
|
||||
|
||||
expect(isFPSort(fp32)).toBe(true);
|
||||
expect(isFPRMSort(rmSort)).toBe(true);
|
||||
|
||||
const x = Float.const('x', fp32);
|
||||
const val = Float.val(1.0, fp32);
|
||||
const rm = FloatRM.RNE();
|
||||
|
||||
expect(isFP(x)).toBe(true);
|
||||
expect(isFPVal(val)).toBe(true);
|
||||
expect(isFPRM(rm)).toBe(true);
|
||||
});
|
||||
});
|
||||
|
||||
describe('strings and sequences', () => {
|
||||
it('can create string sort and values', () => {
|
||||
const { String: Str } = api.Context('main');
|
||||
|
||||
const strSort = Str.sort();
|
||||
expect(strSort.isString()).toBe(true);
|
||||
|
||||
const hello = Str.val('hello');
|
||||
expect(hello.isString()).toBe(true);
|
||||
expect(hello.asString()).toBe('hello');
|
||||
|
||||
const x = Str.const('x');
|
||||
expect(x.isString()).toBe(true);
|
||||
});
|
||||
|
||||
it('can create sequence sorts', () => {
|
||||
const { Seq, Int, eqIdentity } = api.Context('main');
|
||||
|
||||
const intSeq = Seq.sort(Int.sort());
|
||||
expect(eqIdentity(intSeq.basis(), Int.sort())).toBe(true);
|
||||
|
||||
const empty = Seq.empty(Int.sort());
|
||||
const len_empty = empty.length();
|
||||
// TOOD: simplify len_empty const len_empty_simplified =
|
||||
// expect(len_empty_simplified.toString()).toContain('0');
|
||||
});
|
||||
|
||||
it('can concatenate strings', async () => {
|
||||
const { String: Str, Solver } = api.Context('main');
|
||||
|
||||
const x = Str.const('x');
|
||||
const y = Str.const('y');
|
||||
|
||||
const hello = Str.val('hello');
|
||||
const world = Str.val('world');
|
||||
|
||||
const solver = new Solver();
|
||||
solver.add(x.eq(hello));
|
||||
solver.add(y.eq(world));
|
||||
solver.add(x.concat(y).eq(Str.val('helloworld')));
|
||||
|
||||
const result = await solver.check();
|
||||
expect(result).toBe('sat');
|
||||
});
|
||||
|
||||
it('can compute string length', async () => {
|
||||
const { String: Str, Solver, Int } = api.Context('main');
|
||||
|
||||
const x = Str.const('x');
|
||||
const hello = Str.val('hello');
|
||||
|
||||
const solver = new Solver();
|
||||
solver.add(x.eq(hello));
|
||||
solver.add(x.length().eq(Int.val(5)));
|
||||
|
||||
const result = await solver.check();
|
||||
expect(result).toBe('sat');
|
||||
});
|
||||
|
||||
it('can extract substrings', async () => {
|
||||
const { String: Str, Solver } = api.Context('main');
|
||||
|
||||
const x = Str.const('x');
|
||||
const hello = Str.val('hello');
|
||||
|
||||
const solver = new Solver();
|
||||
solver.add(x.eq(hello));
|
||||
solver.add(x.extract(0, 2).eq(Str.val('he')));
|
||||
|
||||
const result = await solver.check();
|
||||
expect(result).toBe('sat');
|
||||
});
|
||||
|
||||
it('can check string containment', async () => {
|
||||
const { String: Str, Solver } = api.Context('main');
|
||||
|
||||
const x = Str.const('x');
|
||||
const hello = Str.val('hello');
|
||||
|
||||
const solver = new Solver();
|
||||
solver.add(x.eq(hello));
|
||||
solver.add(x.contains('ell'));
|
||||
|
||||
const result = await solver.check();
|
||||
expect(result).toBe('sat');
|
||||
});
|
||||
|
||||
it('can find substring index', async () => {
|
||||
const { String: Str, Solver, Int } = api.Context('main');
|
||||
|
||||
const x = Str.const('x');
|
||||
const hello = Str.val('hello');
|
||||
|
||||
const solver = new Solver();
|
||||
solver.add(x.eq(hello));
|
||||
solver.add(x.indexOf('ell').eq(Int.val(1)));
|
||||
|
||||
const result = await solver.check();
|
||||
expect(result).toBe('sat');
|
||||
});
|
||||
|
||||
it('can check string prefix and suffix', async () => {
|
||||
const { String: Str, Solver } = api.Context('main');
|
||||
|
||||
const x = Str.const('x');
|
||||
const hello = Str.val('hello');
|
||||
|
||||
const solver = new Solver();
|
||||
solver.add(x.eq(hello));
|
||||
solver.add(x.prefixOf('helloworld'));
|
||||
solver.add(Str.val('lo').suffixOf(x));
|
||||
|
||||
const result = await solver.check();
|
||||
expect(result).toBe('sat');
|
||||
});
|
||||
|
||||
it('can replace substrings', async () => {
|
||||
const { String: Str, Solver } = api.Context('main');
|
||||
|
||||
const x = Str.const('x');
|
||||
const hello = Str.val('hello');
|
||||
|
||||
const solver = new Solver();
|
||||
solver.add(x.eq(hello));
|
||||
solver.add(x.replace('l', 'L').eq(Str.val('heLlo'))); // First occurrence
|
||||
|
||||
const result = await solver.check();
|
||||
expect(result).toBe('sat');
|
||||
});
|
||||
|
||||
it('supports string type checking', () => {
|
||||
const { String: Str, Seq, Int, isSeqSort, isSeq, isStringSort, isString } = api.Context('main');
|
||||
|
||||
const strSort = Str.sort();
|
||||
const intSeqSort = Seq.sort(Int.sort());
|
||||
|
||||
expect(isSeqSort(strSort)).toBe(true);
|
||||
expect(isStringSort(strSort)).toBe(true);
|
||||
expect(isSeqSort(intSeqSort)).toBe(true);
|
||||
expect(isStringSort(intSeqSort)).toBe(false);
|
||||
|
||||
const hello = Str.val('hello');
|
||||
const x = Str.const('x');
|
||||
|
||||
expect(isSeq(hello)).toBe(true);
|
||||
expect(isString(hello)).toBe(true);
|
||||
expect(isSeq(x)).toBe(true);
|
||||
expect(isString(x)).toBe(true);
|
||||
});
|
||||
|
||||
it('can work with sequences of integers', async () => {
|
||||
const { Seq, Int, Solver } = api.Context('main');
|
||||
|
||||
const one = Int.val(1);
|
||||
const seq1 = Seq.unit(one);
|
||||
|
||||
const two = Int.val(2);
|
||||
const seq2 = Seq.unit(two);
|
||||
|
||||
const concat = seq1.concat(seq2);
|
||||
|
||||
const solver = new Solver();
|
||||
solver.add(concat.length().eq(Int.val(2)));
|
||||
|
||||
const result = await solver.check();
|
||||
expect(result).toBe('sat');
|
||||
});
|
||||
});
|
||||
});
|
||||
|
|
|
|||
|
|
@ -64,9 +64,15 @@ import {
|
|||
CoercibleToBitVec,
|
||||
CoercibleToExpr,
|
||||
CoercibleFromMap,
|
||||
CoercibleToFP,
|
||||
Context,
|
||||
ContextCtor,
|
||||
Expr,
|
||||
FP,
|
||||
FPNum,
|
||||
FPSort,
|
||||
FPRM,
|
||||
FPRMSort,
|
||||
Fixedpoint,
|
||||
FuncDecl,
|
||||
FuncDeclSignature,
|
||||
|
|
@ -79,6 +85,8 @@ import {
|
|||
Quantifier,
|
||||
BodyT,
|
||||
RatNum,
|
||||
Seq,
|
||||
SeqSort,
|
||||
SMTArray,
|
||||
SMTArraySort,
|
||||
Solver,
|
||||
|
|
@ -267,6 +275,12 @@ export function createApi(Z3: Z3Core): Z3HighLevel {
|
|||
return new ArithSortImpl(ast);
|
||||
case Z3_sort_kind.Z3_BV_SORT:
|
||||
return new BitVecSortImpl(ast);
|
||||
case Z3_sort_kind.Z3_FLOATING_POINT_SORT:
|
||||
return new FPSortImpl(ast);
|
||||
case Z3_sort_kind.Z3_ROUNDING_MODE_SORT:
|
||||
return new FPRMSortImpl(ast);
|
||||
case Z3_sort_kind.Z3_SEQ_SORT:
|
||||
return new SeqSortImpl(ast);
|
||||
case Z3_sort_kind.Z3_ARRAY_SORT:
|
||||
return new ArraySortImpl(ast);
|
||||
default:
|
||||
|
|
@ -301,6 +315,15 @@ export function createApi(Z3: Z3Core): Z3HighLevel {
|
|||
return new BitVecNumImpl(ast);
|
||||
}
|
||||
return new BitVecImpl(ast);
|
||||
case Z3_sort_kind.Z3_FLOATING_POINT_SORT:
|
||||
if (kind === Z3_ast_kind.Z3_NUMERAL_AST || kind === Z3_ast_kind.Z3_APP_AST) {
|
||||
return new FPNumImpl(ast);
|
||||
}
|
||||
return new FPImpl(ast);
|
||||
case Z3_sort_kind.Z3_ROUNDING_MODE_SORT:
|
||||
return new FPRMImpl(ast);
|
||||
case Z3_sort_kind.Z3_SEQ_SORT:
|
||||
return new SeqImpl(ast);
|
||||
case Z3_sort_kind.Z3_ARRAY_SORT:
|
||||
return new ArrayImpl(ast);
|
||||
default:
|
||||
|
|
@ -520,6 +543,56 @@ export function createApi(Z3: Z3Core): Z3HighLevel {
|
|||
return isAppOf(obj, Z3_decl_kind.Z3_OP_CONST_ARRAY);
|
||||
}
|
||||
|
||||
function isFPRMSort(obj: unknown): obj is FPRMSort<Name> {
|
||||
const r = obj instanceof FPRMSortImpl;
|
||||
r && _assertContext(obj);
|
||||
return r;
|
||||
}
|
||||
|
||||
function isFPRM(obj: unknown): obj is FPRM<Name> {
|
||||
const r = obj instanceof FPRMImpl;
|
||||
r && _assertContext(obj);
|
||||
return r;
|
||||
}
|
||||
|
||||
function isFPSort(obj: unknown): obj is FPSort<Name> {
|
||||
const r = obj instanceof FPSortImpl;
|
||||
r && _assertContext(obj);
|
||||
return r;
|
||||
}
|
||||
|
||||
function isFP(obj: unknown): obj is FP<Name> {
|
||||
const r = obj instanceof FPImpl;
|
||||
r && _assertContext(obj);
|
||||
return r;
|
||||
}
|
||||
|
||||
function isFPVal(obj: unknown): obj is FPNum<Name> {
|
||||
const r = obj instanceof FPNumImpl;
|
||||
r && _assertContext(obj);
|
||||
return r;
|
||||
}
|
||||
|
||||
function isSeqSort(obj: unknown): obj is SeqSort<Name> {
|
||||
const r = obj instanceof SeqSortImpl;
|
||||
r && _assertContext(obj);
|
||||
return r;
|
||||
}
|
||||
|
||||
function isSeq(obj: unknown): obj is Seq<Name> {
|
||||
const r = obj instanceof SeqImpl;
|
||||
r && _assertContext(obj);
|
||||
return r;
|
||||
}
|
||||
|
||||
function isStringSort(obj: unknown): obj is SeqSort<Name> {
|
||||
return isSeqSort(obj) && obj.isString();
|
||||
}
|
||||
|
||||
function isString(obj: unknown): obj is Seq<Name> {
|
||||
return isSeq(obj) && obj.isString();
|
||||
}
|
||||
|
||||
function isProbe(obj: unknown): obj is Probe<Name> {
|
||||
const r = obj instanceof ProbeImpl;
|
||||
r && _assertContext(obj);
|
||||
|
|
@ -762,6 +835,119 @@ export function createApi(Z3: Z3Core): Z3HighLevel {
|
|||
);
|
||||
},
|
||||
};
|
||||
|
||||
const Float = {
|
||||
sort(ebits: number, sbits: number): FPSort<Name> {
|
||||
assert(Number.isSafeInteger(ebits) && ebits > 0, 'ebits must be a positive integer');
|
||||
assert(Number.isSafeInteger(sbits) && sbits > 0, 'sbits must be a positive integer');
|
||||
return new FPSortImpl(Z3.mk_fpa_sort(contextPtr, ebits, sbits));
|
||||
},
|
||||
|
||||
sort16(): FPSort<Name> {
|
||||
return new FPSortImpl(Z3.mk_fpa_sort_16(contextPtr));
|
||||
},
|
||||
|
||||
sort32(): FPSort<Name> {
|
||||
return new FPSortImpl(Z3.mk_fpa_sort_32(contextPtr));
|
||||
},
|
||||
|
||||
sort64(): FPSort<Name> {
|
||||
return new FPSortImpl(Z3.mk_fpa_sort_64(contextPtr));
|
||||
},
|
||||
|
||||
sort128(): FPSort<Name> {
|
||||
return new FPSortImpl(Z3.mk_fpa_sort_128(contextPtr));
|
||||
},
|
||||
|
||||
const(name: string, sort: FPSort<Name>): FP<Name> {
|
||||
return new FPImpl(check(Z3.mk_const(contextPtr, _toSymbol(name), sort.ptr)));
|
||||
},
|
||||
|
||||
consts(names: string | string[], sort: FPSort<Name>): FP<Name>[] {
|
||||
if (typeof names === 'string') {
|
||||
names = names.split(' ');
|
||||
}
|
||||
return names.map(name => Float.const(name, sort));
|
||||
},
|
||||
|
||||
val(value: number, sort: FPSort<Name>): FPNum<Name> {
|
||||
return new FPNumImpl(check(Z3.mk_fpa_numeral_double(contextPtr, value, sort.ptr)));
|
||||
},
|
||||
|
||||
NaN(sort: FPSort<Name>): FPNum<Name> {
|
||||
return new FPNumImpl(check(Z3.mk_fpa_nan(contextPtr, sort.ptr)));
|
||||
},
|
||||
|
||||
inf(sort: FPSort<Name>, negative: boolean = false): FPNum<Name> {
|
||||
return new FPNumImpl(check(Z3.mk_fpa_inf(contextPtr, sort.ptr, negative)));
|
||||
},
|
||||
|
||||
zero(sort: FPSort<Name>, negative: boolean = false): FPNum<Name> {
|
||||
return new FPNumImpl(check(Z3.mk_fpa_zero(contextPtr, sort.ptr, negative)));
|
||||
},
|
||||
};
|
||||
|
||||
const FloatRM = {
|
||||
sort(): FPRMSort<Name> {
|
||||
return new FPRMSortImpl(Z3.mk_fpa_rounding_mode_sort(contextPtr));
|
||||
},
|
||||
|
||||
RNE(): FPRM<Name> {
|
||||
return new FPRMImpl(check(Z3.mk_fpa_rne(contextPtr)));
|
||||
},
|
||||
|
||||
RNA(): FPRM<Name> {
|
||||
return new FPRMImpl(check(Z3.mk_fpa_rna(contextPtr)));
|
||||
},
|
||||
|
||||
RTP(): FPRM<Name> {
|
||||
return new FPRMImpl(check(Z3.mk_fpa_rtp(contextPtr)));
|
||||
},
|
||||
|
||||
RTN(): FPRM<Name> {
|
||||
return new FPRMImpl(check(Z3.mk_fpa_rtn(contextPtr)));
|
||||
},
|
||||
|
||||
RTZ(): FPRM<Name> {
|
||||
return new FPRMImpl(check(Z3.mk_fpa_rtz(contextPtr)));
|
||||
},
|
||||
};
|
||||
|
||||
const String = {
|
||||
sort(): SeqSort<Name> {
|
||||
return new SeqSortImpl(Z3.mk_string_sort(contextPtr));
|
||||
},
|
||||
|
||||
const(name: string): Seq<Name> {
|
||||
return new SeqImpl(check(Z3.mk_const(contextPtr, _toSymbol(name), String.sort().ptr)));
|
||||
},
|
||||
|
||||
consts(names: string | string[]): Seq<Name>[] {
|
||||
if (typeof names === 'string') {
|
||||
names = names.split(' ');
|
||||
}
|
||||
return names.map(name => String.const(name));
|
||||
},
|
||||
|
||||
val(value: string): Seq<Name> {
|
||||
return new SeqImpl(check(Z3.mk_string(contextPtr, value)));
|
||||
},
|
||||
};
|
||||
|
||||
const Seq = {
|
||||
sort<ElemSort extends Sort<Name>>(elemSort: ElemSort): SeqSort<Name, ElemSort> {
|
||||
return new SeqSortImpl<ElemSort>(Z3.mk_seq_sort(contextPtr, elemSort.ptr));
|
||||
},
|
||||
|
||||
empty<ElemSort extends Sort<Name>>(elemSort: ElemSort): Seq<Name, ElemSort> {
|
||||
return new SeqImpl<ElemSort>(check(Z3.mk_seq_empty(contextPtr, Seq.sort(elemSort).ptr)));
|
||||
},
|
||||
|
||||
unit<ElemSort extends Sort<Name>>(elem: Expr<Name>): Seq<Name, ElemSort> {
|
||||
return new SeqImpl<ElemSort>(check(Z3.mk_seq_unit(contextPtr, elem.ast)));
|
||||
},
|
||||
};
|
||||
|
||||
const Array = {
|
||||
sort<DomainSort extends NonEmptySortArray<Name>, RangeSort extends AnySort<Name>>(
|
||||
...sig: [...DomainSort, RangeSort]
|
||||
|
|
@ -2860,6 +3046,261 @@ export function createApi(Z3: Z3Core): Z3HighLevel {
|
|||
}
|
||||
}
|
||||
|
||||
class FPRMSortImpl extends SortImpl implements FPRMSort<Name> {
|
||||
declare readonly __typename: FPRMSort['__typename'];
|
||||
|
||||
cast(other: FPRM<Name>): FPRM<Name>;
|
||||
cast(other: CoercibleToExpr<Name>): never;
|
||||
cast(other: any): any {
|
||||
if (isFPRM(other)) {
|
||||
_assertContext(other);
|
||||
return other;
|
||||
}
|
||||
throw new Error("Can't cast to FPRMSort");
|
||||
}
|
||||
}
|
||||
|
||||
class FPRMImpl extends ExprImpl<Z3_ast, FPRMSortImpl> implements FPRM<Name> {
|
||||
declare readonly __typename: FPRM['__typename'];
|
||||
}
|
||||
|
||||
class FPSortImpl extends SortImpl implements FPSort<Name> {
|
||||
declare readonly __typename: FPSort['__typename'];
|
||||
|
||||
ebits() {
|
||||
return Z3.fpa_get_ebits(contextPtr, this.ptr);
|
||||
}
|
||||
|
||||
sbits() {
|
||||
return Z3.fpa_get_sbits(contextPtr, this.ptr);
|
||||
}
|
||||
|
||||
cast(other: CoercibleToFP<Name>): FP<Name>;
|
||||
cast(other: CoercibleToExpr<Name>): Expr<Name>;
|
||||
cast(other: CoercibleToExpr<Name>): Expr<Name> {
|
||||
if (isExpr(other)) {
|
||||
_assertContext(other);
|
||||
return other;
|
||||
}
|
||||
if (typeof other === 'number') {
|
||||
return Float.val(other, this);
|
||||
}
|
||||
throw new Error("Can't cast to FPSort");
|
||||
}
|
||||
}
|
||||
|
||||
class FPImpl extends ExprImpl<Z3_ast, FPSortImpl> implements FP<Name> {
|
||||
declare readonly __typename: FP['__typename'];
|
||||
|
||||
add(rm: FPRM<Name>, other: CoercibleToFP<Name>): FP<Name> {
|
||||
const otherFP = isFP(other) ? other : Float.val(other, this.sort);
|
||||
return new FPImpl(check(Z3.mk_fpa_add(contextPtr, rm.ast, this.ast, otherFP.ast)));
|
||||
}
|
||||
|
||||
sub(rm: FPRM<Name>, other: CoercibleToFP<Name>): FP<Name> {
|
||||
const otherFP = isFP(other) ? other : Float.val(other, this.sort);
|
||||
return new FPImpl(check(Z3.mk_fpa_sub(contextPtr, rm.ast, this.ast, otherFP.ast)));
|
||||
}
|
||||
|
||||
mul(rm: FPRM<Name>, other: CoercibleToFP<Name>): FP<Name> {
|
||||
const otherFP = isFP(other) ? other : Float.val(other, this.sort);
|
||||
return new FPImpl(check(Z3.mk_fpa_mul(contextPtr, rm.ast, this.ast, otherFP.ast)));
|
||||
}
|
||||
|
||||
div(rm: FPRM<Name>, other: CoercibleToFP<Name>): FP<Name> {
|
||||
const otherFP = isFP(other) ? other : Float.val(other, this.sort);
|
||||
return new FPImpl(check(Z3.mk_fpa_div(contextPtr, rm.ast, this.ast, otherFP.ast)));
|
||||
}
|
||||
|
||||
neg(): FP<Name> {
|
||||
return new FPImpl(check(Z3.mk_fpa_neg(contextPtr, this.ast)));
|
||||
}
|
||||
|
||||
abs(): FP<Name> {
|
||||
return new FPImpl(check(Z3.mk_fpa_abs(contextPtr, this.ast)));
|
||||
}
|
||||
|
||||
sqrt(rm: FPRM<Name>): FP<Name> {
|
||||
return new FPImpl(check(Z3.mk_fpa_sqrt(contextPtr, rm.ast, this.ast)));
|
||||
}
|
||||
|
||||
rem(other: CoercibleToFP<Name>): FP<Name> {
|
||||
const otherFP = isFP(other) ? other : Float.val(other, this.sort);
|
||||
return new FPImpl(check(Z3.mk_fpa_rem(contextPtr, this.ast, otherFP.ast)));
|
||||
}
|
||||
|
||||
fma(rm: FPRM<Name>, y: CoercibleToFP<Name>, z: CoercibleToFP<Name>): FP<Name> {
|
||||
const yFP = isFP(y) ? y : Float.val(y, this.sort);
|
||||
const zFP = isFP(z) ? z : Float.val(z, this.sort);
|
||||
return new FPImpl(check(Z3.mk_fpa_fma(contextPtr, rm.ast, this.ast, yFP.ast, zFP.ast)));
|
||||
}
|
||||
|
||||
lt(other: CoercibleToFP<Name>): Bool<Name> {
|
||||
const otherFP = isFP(other) ? other : Float.val(other, this.sort);
|
||||
return new BoolImpl(check(Z3.mk_fpa_lt(contextPtr, this.ast, otherFP.ast)));
|
||||
}
|
||||
|
||||
gt(other: CoercibleToFP<Name>): Bool<Name> {
|
||||
const otherFP = isFP(other) ? other : Float.val(other, this.sort);
|
||||
return new BoolImpl(check(Z3.mk_fpa_gt(contextPtr, this.ast, otherFP.ast)));
|
||||
}
|
||||
|
||||
le(other: CoercibleToFP<Name>): Bool<Name> {
|
||||
const otherFP = isFP(other) ? other : Float.val(other, this.sort);
|
||||
return new BoolImpl(check(Z3.mk_fpa_leq(contextPtr, this.ast, otherFP.ast)));
|
||||
}
|
||||
|
||||
ge(other: CoercibleToFP<Name>): Bool<Name> {
|
||||
const otherFP = isFP(other) ? other : Float.val(other, this.sort);
|
||||
return new BoolImpl(check(Z3.mk_fpa_geq(contextPtr, this.ast, otherFP.ast)));
|
||||
}
|
||||
|
||||
isNaN(): Bool<Name> {
|
||||
return new BoolImpl(check(Z3.mk_fpa_is_nan(contextPtr, this.ast)));
|
||||
}
|
||||
|
||||
isInf(): Bool<Name> {
|
||||
return new BoolImpl(check(Z3.mk_fpa_is_infinite(contextPtr, this.ast)));
|
||||
}
|
||||
|
||||
isZero(): Bool<Name> {
|
||||
return new BoolImpl(check(Z3.mk_fpa_is_zero(contextPtr, this.ast)));
|
||||
}
|
||||
|
||||
isNormal(): Bool<Name> {
|
||||
return new BoolImpl(check(Z3.mk_fpa_is_normal(contextPtr, this.ast)));
|
||||
}
|
||||
|
||||
isSubnormal(): Bool<Name> {
|
||||
return new BoolImpl(check(Z3.mk_fpa_is_subnormal(contextPtr, this.ast)));
|
||||
}
|
||||
|
||||
isNegative(): Bool<Name> {
|
||||
return new BoolImpl(check(Z3.mk_fpa_is_negative(contextPtr, this.ast)));
|
||||
}
|
||||
|
||||
isPositive(): Bool<Name> {
|
||||
return new BoolImpl(check(Z3.mk_fpa_is_positive(contextPtr, this.ast)));
|
||||
}
|
||||
}
|
||||
|
||||
class FPNumImpl extends FPImpl implements FPNum<Name> {
|
||||
declare readonly __typename: FPNum['__typename'];
|
||||
|
||||
value(): number {
|
||||
// Get the floating-point numeral as a JavaScript number
|
||||
// Note: This may lose precision for values outside JavaScript number range
|
||||
return Z3.get_numeral_double(contextPtr, this.ast);
|
||||
}
|
||||
}
|
||||
|
||||
class SeqSortImpl<ElemSort extends Sort<Name> = Sort<Name>> extends SortImpl implements SeqSort<Name, ElemSort> {
|
||||
declare readonly __typename: SeqSort['__typename'];
|
||||
|
||||
isString(): boolean {
|
||||
return Z3.is_string_sort(contextPtr, this.ptr);
|
||||
}
|
||||
|
||||
basis(): Sort<Name> {
|
||||
return _toSort(check(Z3.get_seq_sort_basis(contextPtr, this.ptr)));
|
||||
}
|
||||
|
||||
cast(other: Seq<Name>): Seq<Name>;
|
||||
cast(other: string): Seq<Name>;
|
||||
cast(other: CoercibleToExpr<Name>): Expr<Name>;
|
||||
cast(other: any): any {
|
||||
if (isSeq(other)) {
|
||||
_assertContext(other);
|
||||
return other;
|
||||
}
|
||||
if (typeof other === 'string') {
|
||||
return String.val(other);
|
||||
}
|
||||
throw new Error("Can't cast to SeqSort");
|
||||
}
|
||||
}
|
||||
|
||||
class SeqImpl<ElemSort extends Sort<Name> = Sort<Name>>
|
||||
extends ExprImpl<Z3_ast, SeqSortImpl<ElemSort>>
|
||||
implements Seq<Name, ElemSort>
|
||||
{
|
||||
declare readonly __typename: Seq['__typename'];
|
||||
|
||||
isString(): boolean {
|
||||
return Z3.is_string_sort(contextPtr, Z3.get_sort(contextPtr, this.ast));
|
||||
}
|
||||
|
||||
asString(): string {
|
||||
if (!Z3.is_string(contextPtr, this.ast)) {
|
||||
throw new Error('Not a string value');
|
||||
}
|
||||
return Z3.get_string(contextPtr, this.ast);
|
||||
}
|
||||
|
||||
concat(other: Seq<Name, ElemSort> | string): Seq<Name, ElemSort> {
|
||||
const otherSeq = isSeq(other) ? other : String.val(other);
|
||||
return new SeqImpl<ElemSort>(check(Z3.mk_seq_concat(contextPtr, [this.ast, otherSeq.ast])));
|
||||
}
|
||||
|
||||
length(): Arith<Name> {
|
||||
return new ArithImpl(check(Z3.mk_seq_length(contextPtr, this.ast)));
|
||||
}
|
||||
|
||||
at(index: Arith<Name> | number | bigint): Seq<Name, ElemSort> {
|
||||
const indexExpr = isArith(index) ? index : Int.val(index);
|
||||
return new SeqImpl<ElemSort>(check(Z3.mk_seq_at(contextPtr, this.ast, indexExpr.ast)));
|
||||
}
|
||||
|
||||
nth(index: Arith<Name> | number | bigint): Expr<Name> {
|
||||
const indexExpr = isArith(index) ? index : Int.val(index);
|
||||
return _toExpr(check(Z3.mk_seq_nth(contextPtr, this.ast, indexExpr.ast)));
|
||||
}
|
||||
|
||||
extract(offset: Arith<Name> | number | bigint, length: Arith<Name> | number | bigint): Seq<Name, ElemSort> {
|
||||
const offsetExpr = isArith(offset) ? offset : Int.val(offset);
|
||||
const lengthExpr = isArith(length) ? length : Int.val(length);
|
||||
return new SeqImpl<ElemSort>(check(Z3.mk_seq_extract(contextPtr, this.ast, offsetExpr.ast, lengthExpr.ast)));
|
||||
}
|
||||
|
||||
indexOf(substr: Seq<Name, ElemSort> | string, offset?: Arith<Name> | number | bigint): Arith<Name> {
|
||||
const substrSeq = isSeq(substr) ? substr : String.val(substr);
|
||||
const offsetExpr = offset !== undefined ? (isArith(offset) ? offset : Int.val(offset)) : Int.val(0);
|
||||
return new ArithImpl(check(Z3.mk_seq_index(contextPtr, this.ast, substrSeq.ast, offsetExpr.ast)));
|
||||
}
|
||||
|
||||
lastIndexOf(substr: Seq<Name, ElemSort> | string): Arith<Name> {
|
||||
const substrSeq = isSeq(substr) ? substr : String.val(substr);
|
||||
return new ArithImpl(check(Z3.mk_seq_last_index(contextPtr, this.ast, substrSeq.ast)));
|
||||
}
|
||||
|
||||
contains(substr: Seq<Name, ElemSort> | string): Bool<Name> {
|
||||
const substrSeq = isSeq(substr) ? substr : String.val(substr);
|
||||
return new BoolImpl(check(Z3.mk_seq_contains(contextPtr, this.ast, substrSeq.ast)));
|
||||
}
|
||||
|
||||
prefixOf(s: Seq<Name, ElemSort> | string): Bool<Name> {
|
||||
const sSeq = isSeq(s) ? s : String.val(s);
|
||||
return new BoolImpl(check(Z3.mk_seq_prefix(contextPtr, this.ast, sSeq.ast)));
|
||||
}
|
||||
|
||||
suffixOf(s: Seq<Name, ElemSort> | string): Bool<Name> {
|
||||
const sSeq = isSeq(s) ? s : String.val(s);
|
||||
return new BoolImpl(check(Z3.mk_seq_suffix(contextPtr, this.ast, sSeq.ast)));
|
||||
}
|
||||
|
||||
replace(src: Seq<Name, ElemSort> | string, dst: Seq<Name, ElemSort> | string): Seq<Name, ElemSort> {
|
||||
const srcSeq = isSeq(src) ? src : String.val(src);
|
||||
const dstSeq = isSeq(dst) ? dst : String.val(dst);
|
||||
return new SeqImpl<ElemSort>(check(Z3.mk_seq_replace(contextPtr, this.ast, srcSeq.ast, dstSeq.ast)));
|
||||
}
|
||||
|
||||
replaceAll(src: Seq<Name, ElemSort> | string, dst: Seq<Name, ElemSort> | string): Seq<Name, ElemSort> {
|
||||
const srcSeq = isSeq(src) ? src : String.val(src);
|
||||
const dstSeq = isSeq(dst) ? dst : String.val(dst);
|
||||
return new SeqImpl<ElemSort>(check(Z3.mk_seq_replace_all(contextPtr, this.ast, srcSeq.ast, dstSeq.ast)));
|
||||
}
|
||||
}
|
||||
|
||||
class ArraySortImpl<DomainSort extends NonEmptySortArray<Name>, RangeSort extends Sort<Name>>
|
||||
extends SortImpl
|
||||
implements SMTArraySort<Name, DomainSort, RangeSort>
|
||||
|
|
@ -3529,6 +3970,15 @@ export function createApi(Z3: Z3Core): Z3HighLevel {
|
|||
isBitVecSort,
|
||||
isBitVec,
|
||||
isBitVecVal, // TODO fix ordering
|
||||
isFPRMSort,
|
||||
isFPRM,
|
||||
isFPSort,
|
||||
isFP,
|
||||
isFPVal,
|
||||
isSeqSort,
|
||||
isSeq,
|
||||
isStringSort,
|
||||
isString,
|
||||
isArraySort,
|
||||
isArray,
|
||||
isConstArray,
|
||||
|
|
@ -3550,6 +4000,10 @@ export function createApi(Z3: Z3Core): Z3HighLevel {
|
|||
Int,
|
||||
Real,
|
||||
BitVec,
|
||||
Float,
|
||||
FloatRM,
|
||||
String,
|
||||
Seq,
|
||||
Array,
|
||||
Set,
|
||||
Datatype,
|
||||
|
|
|
|||
|
|
@ -25,7 +25,10 @@ export type AnySort<Name extends string = 'main'> =
|
|||
| BoolSort<Name>
|
||||
| ArithSort<Name>
|
||||
| BitVecSort<number, Name>
|
||||
| SMTArraySort<Name>;
|
||||
| SMTArraySort<Name>
|
||||
| FPSort<Name>
|
||||
| FPRMSort<Name>
|
||||
| SeqSort<Name>;
|
||||
/** @hidden */
|
||||
export type AnyExpr<Name extends string = 'main'> =
|
||||
| Expr<Name>
|
||||
|
|
@ -35,7 +38,11 @@ export type AnyExpr<Name extends string = 'main'> =
|
|||
| RatNum<Name>
|
||||
| BitVec<number, Name>
|
||||
| BitVecNum<number, Name>
|
||||
| SMTArray<Name>;
|
||||
| SMTArray<Name>
|
||||
| FP<Name>
|
||||
| FPNum<Name>
|
||||
| FPRM<Name>
|
||||
| Seq<Name>;
|
||||
/** @hidden */
|
||||
export type AnyAst<Name extends string = 'main'> = AnyExpr<Name> | AnySort<Name> | FuncDecl<Name>;
|
||||
|
||||
|
|
@ -49,6 +56,12 @@ export type SortToExprMap<S extends AnySort<Name>, Name extends string = 'main'>
|
|||
? BitVec<Size, Name>
|
||||
: S extends SMTArraySort<Name, infer DomainSort, infer RangeSort>
|
||||
? SMTArray<Name, DomainSort, RangeSort>
|
||||
: S extends FPSort<Name>
|
||||
? FP<Name>
|
||||
: S extends FPRMSort<Name>
|
||||
? FPRM<Name>
|
||||
: S extends SeqSort<Name>
|
||||
? Seq<Name>
|
||||
: S extends Sort<Name>
|
||||
? Expr<Name, S, Z3_ast>
|
||||
: never;
|
||||
|
|
@ -71,6 +84,9 @@ export type CoercibleToBitVec<Bits extends number = number, Name extends string
|
|||
| number
|
||||
| BitVec<Bits, Name>;
|
||||
|
||||
/** @hidden */
|
||||
export type CoercibleToFP<Name extends string = 'main'> = number | FP<Name>;
|
||||
|
||||
export type CoercibleRational = { numerator: bigint | number; denominator: bigint | number };
|
||||
|
||||
/** @hidden */
|
||||
|
|
@ -97,6 +113,8 @@ export type CoercibleToMap<T extends AnyExpr<Name>, Name extends string = 'main'
|
|||
? CoercibleToArith<Name>
|
||||
: T extends BitVec<infer Size, Name>
|
||||
? CoercibleToBitVec<Size, Name>
|
||||
: T extends FP<Name>
|
||||
? CoercibleToFP<Name>
|
||||
: T extends SMTArray<Name, infer DomainSort, infer RangeSort>
|
||||
? SMTArray<Name, DomainSort, RangeSort>
|
||||
: T extends Expr<Name>
|
||||
|
|
@ -258,6 +276,33 @@ export interface Context<Name extends string = 'main'> {
|
|||
/** @category Functions */
|
||||
isConstArray(obj: unknown): boolean;
|
||||
|
||||
/** @category Functions */
|
||||
isFPSort(obj: unknown): obj is FPSort<Name>;
|
||||
|
||||
/** @category Functions */
|
||||
isFP(obj: unknown): obj is FP<Name>;
|
||||
|
||||
/** @category Functions */
|
||||
isFPVal(obj: unknown): obj is FPNum<Name>;
|
||||
|
||||
/** @category Functions */
|
||||
isFPRMSort(obj: unknown): obj is FPRMSort<Name>;
|
||||
|
||||
/** @category Functions */
|
||||
isFPRM(obj: unknown): obj is FPRM<Name>;
|
||||
|
||||
/** @category Functions */
|
||||
isSeqSort(obj: unknown): obj is SeqSort<Name>;
|
||||
|
||||
/** @category Functions */
|
||||
isSeq(obj: unknown): obj is Seq<Name>;
|
||||
|
||||
/** @category Functions */
|
||||
isStringSort(obj: unknown): obj is SeqSort<Name>;
|
||||
|
||||
/** @category Functions */
|
||||
isString(obj: unknown): obj is Seq<Name>;
|
||||
|
||||
/** @category Functions */
|
||||
isProbe(obj: unknown): obj is Probe<Name>;
|
||||
|
||||
|
|
@ -371,6 +416,14 @@ export interface Context<Name extends string = 'main'> {
|
|||
/** @category Expressions */
|
||||
readonly BitVec: BitVecCreation<Name>;
|
||||
/** @category Expressions */
|
||||
readonly Float: FPCreation<Name>;
|
||||
/** @category Expressions */
|
||||
readonly FloatRM: FPRMCreation<Name>;
|
||||
/** @category Expressions */
|
||||
readonly String: StringCreation<Name>;
|
||||
/** @category Expressions */
|
||||
readonly Seq: SeqCreation<Name>;
|
||||
/** @category Expressions */
|
||||
readonly Array: SMTArrayCreation<Name>;
|
||||
/** @category Expressions */
|
||||
readonly Set: SMTSetCreation<Name>;
|
||||
|
|
@ -1327,7 +1380,10 @@ export interface Sort<Name extends string = 'main'> extends Ast<Name, Z3_sort> {
|
|||
| ArithSort['__typename']
|
||||
| BitVecSort['__typename']
|
||||
| SMTArraySort['__typename']
|
||||
| DatatypeSort['__typename'];
|
||||
| DatatypeSort['__typename']
|
||||
| FPSort['__typename']
|
||||
| FPRMSort['__typename']
|
||||
| SeqSort['__typename'];
|
||||
|
||||
kind(): Z3_sort_kind;
|
||||
|
||||
|
|
@ -1451,6 +1507,9 @@ export interface Expr<Name extends string = 'main', S extends Sort<Name> = AnySo
|
|||
| Bool['__typename']
|
||||
| Arith['__typename']
|
||||
| BitVec['__typename']
|
||||
| FP['__typename']
|
||||
| FPRM['__typename']
|
||||
| Seq['__typename']
|
||||
| SMTArray['__typename']
|
||||
| DatatypeExpr['__typename'];
|
||||
|
||||
|
|
@ -2256,6 +2315,356 @@ export interface DatatypeExpr<Name extends string = 'main'> extends Expr<Name, D
|
|||
readonly __typename: 'DatatypeExpr';
|
||||
}
|
||||
|
||||
///////////////////////
|
||||
// Floating-Point API //
|
||||
///////////////////////
|
||||
|
||||
/**
|
||||
* Floating-point rounding mode sort
|
||||
* @category Floating-Point
|
||||
*/
|
||||
export interface FPRMSort<Name extends string = 'main'> extends Sort<Name> {
|
||||
/** @hidden */
|
||||
readonly __typename: 'FPRMSort';
|
||||
|
||||
cast(other: FPRM<Name>): FPRM<Name>;
|
||||
cast(other: CoercibleToExpr<Name>): never;
|
||||
}
|
||||
|
||||
/**
|
||||
* Floating-point sort (IEEE 754)
|
||||
* @category Floating-Point
|
||||
*/
|
||||
export interface FPSort<Name extends string = 'main'> extends Sort<Name> {
|
||||
/** @hidden */
|
||||
readonly __typename: 'FPSort';
|
||||
|
||||
/**
|
||||
* Number of exponent bits
|
||||
*/
|
||||
ebits(): number;
|
||||
|
||||
/**
|
||||
* Number of significand bits (including hidden bit)
|
||||
*/
|
||||
sbits(): number;
|
||||
|
||||
cast(other: CoercibleToFP<Name>): FP<Name>;
|
||||
cast(other: CoercibleToExpr<Name>): Expr<Name>;
|
||||
}
|
||||
|
||||
/** @category Floating-Point */
|
||||
export interface FPCreation<Name extends string> {
|
||||
/**
|
||||
* Create a floating-point sort with custom exponent and significand bit sizes
|
||||
* @param ebits Number of exponent bits
|
||||
* @param sbits Number of significand bits (including hidden bit)
|
||||
*/
|
||||
sort(ebits: number, sbits: number): FPSort<Name>;
|
||||
|
||||
/**
|
||||
* IEEE 754 16-bit floating-point sort (half precision)
|
||||
*/
|
||||
sort16(): FPSort<Name>;
|
||||
|
||||
/**
|
||||
* IEEE 754 32-bit floating-point sort (single precision)
|
||||
*/
|
||||
sort32(): FPSort<Name>;
|
||||
|
||||
/**
|
||||
* IEEE 754 64-bit floating-point sort (double precision)
|
||||
*/
|
||||
sort64(): FPSort<Name>;
|
||||
|
||||
/**
|
||||
* IEEE 754 128-bit floating-point sort (quadruple precision)
|
||||
*/
|
||||
sort128(): FPSort<Name>;
|
||||
|
||||
/**
|
||||
* Create a floating-point constant
|
||||
*/
|
||||
const(name: string, sort: FPSort<Name>): FP<Name>;
|
||||
|
||||
/**
|
||||
* Create multiple floating-point constants
|
||||
*/
|
||||
consts(names: string | string[], sort: FPSort<Name>): FP<Name>[];
|
||||
|
||||
/**
|
||||
* Create a floating-point value from a number
|
||||
*/
|
||||
val(value: number, sort: FPSort<Name>): FPNum<Name>;
|
||||
|
||||
/**
|
||||
* Create floating-point NaN
|
||||
*/
|
||||
NaN(sort: FPSort<Name>): FPNum<Name>;
|
||||
|
||||
/**
|
||||
* Create floating-point infinity
|
||||
* @param negative If true, creates negative infinity
|
||||
*/
|
||||
inf(sort: FPSort<Name>, negative?: boolean): FPNum<Name>;
|
||||
|
||||
/**
|
||||
* Create floating-point zero
|
||||
* @param negative If true, creates negative zero
|
||||
*/
|
||||
zero(sort: FPSort<Name>, negative?: boolean): FPNum<Name>;
|
||||
}
|
||||
|
||||
/** @category Floating-Point */
|
||||
export interface FPRMCreation<Name extends string> {
|
||||
/**
|
||||
* Get the floating-point rounding mode sort
|
||||
*/
|
||||
sort(): FPRMSort<Name>;
|
||||
|
||||
/**
|
||||
* Round nearest, ties to even (default rounding mode)
|
||||
*/
|
||||
RNE(): FPRM<Name>;
|
||||
|
||||
/**
|
||||
* Round nearest, ties to away
|
||||
*/
|
||||
RNA(): FPRM<Name>;
|
||||
|
||||
/**
|
||||
* Round toward positive infinity
|
||||
*/
|
||||
RTP(): FPRM<Name>;
|
||||
|
||||
/**
|
||||
* Round toward negative infinity
|
||||
*/
|
||||
RTN(): FPRM<Name>;
|
||||
|
||||
/**
|
||||
* Round toward zero
|
||||
*/
|
||||
RTZ(): FPRM<Name>;
|
||||
}
|
||||
|
||||
/**
|
||||
* Floating-point rounding mode expression
|
||||
* @category Floating-Point
|
||||
*/
|
||||
export interface FPRM<Name extends string = 'main'> extends Expr<Name, FPRMSort<Name>, Z3_ast> {
|
||||
/** @hidden */
|
||||
readonly __typename: 'FPRM';
|
||||
}
|
||||
|
||||
/**
|
||||
* Floating-point expression (IEEE 754)
|
||||
* @category Floating-Point
|
||||
*/
|
||||
export interface FP<Name extends string = 'main'> extends Expr<Name, FPSort<Name>, Z3_ast> {
|
||||
/** @hidden */
|
||||
readonly __typename: 'FP' | FPNum['__typename'];
|
||||
|
||||
/** @category Arithmetic */
|
||||
add(rm: FPRM<Name>, other: CoercibleToFP<Name>): FP<Name>;
|
||||
|
||||
/** @category Arithmetic */
|
||||
sub(rm: FPRM<Name>, other: CoercibleToFP<Name>): FP<Name>;
|
||||
|
||||
/** @category Arithmetic */
|
||||
mul(rm: FPRM<Name>, other: CoercibleToFP<Name>): FP<Name>;
|
||||
|
||||
/** @category Arithmetic */
|
||||
div(rm: FPRM<Name>, other: CoercibleToFP<Name>): FP<Name>;
|
||||
|
||||
/** @category Arithmetic */
|
||||
neg(): FP<Name>;
|
||||
|
||||
/** @category Arithmetic */
|
||||
abs(): FP<Name>;
|
||||
|
||||
/** @category Arithmetic */
|
||||
sqrt(rm: FPRM<Name>): FP<Name>;
|
||||
|
||||
/** @category Arithmetic */
|
||||
rem(other: CoercibleToFP<Name>): FP<Name>;
|
||||
|
||||
/** @category Arithmetic */
|
||||
fma(rm: FPRM<Name>, y: CoercibleToFP<Name>, z: CoercibleToFP<Name>): FP<Name>;
|
||||
|
||||
/** @category Comparison */
|
||||
lt(other: CoercibleToFP<Name>): Bool<Name>;
|
||||
|
||||
/** @category Comparison */
|
||||
gt(other: CoercibleToFP<Name>): Bool<Name>;
|
||||
|
||||
/** @category Comparison */
|
||||
le(other: CoercibleToFP<Name>): Bool<Name>;
|
||||
|
||||
/** @category Comparison */
|
||||
ge(other: CoercibleToFP<Name>): Bool<Name>;
|
||||
|
||||
/** @category Predicates */
|
||||
isNaN(): Bool<Name>;
|
||||
|
||||
/** @category Predicates */
|
||||
isInf(): Bool<Name>;
|
||||
|
||||
/** @category Predicates */
|
||||
isZero(): Bool<Name>;
|
||||
|
||||
/** @category Predicates */
|
||||
isNormal(): Bool<Name>;
|
||||
|
||||
/** @category Predicates */
|
||||
isSubnormal(): Bool<Name>;
|
||||
|
||||
/** @category Predicates */
|
||||
isNegative(): Bool<Name>;
|
||||
|
||||
/** @category Predicates */
|
||||
isPositive(): Bool<Name>;
|
||||
}
|
||||
|
||||
/**
|
||||
* Floating-point numeral value
|
||||
* @category Floating-Point
|
||||
*/
|
||||
export interface FPNum<Name extends string = 'main'> extends FP<Name> {
|
||||
/** @hidden */
|
||||
readonly __typename: 'FPNum';
|
||||
|
||||
/**
|
||||
* Get the floating-point value as a JavaScript number
|
||||
* Note: May lose precision for values outside JavaScript number range
|
||||
*/
|
||||
value(): number;
|
||||
}
|
||||
|
||||
///////////////////////
|
||||
// String/Sequence API //
|
||||
///////////////////////
|
||||
|
||||
/**
|
||||
* Sequence sort (can be string or sequence of any element type)
|
||||
* @category String/Sequence
|
||||
*/
|
||||
export interface SeqSort<Name extends string = 'main', ElemSort extends Sort<Name> = Sort<Name>> extends Sort<Name> {
|
||||
/** @hidden */
|
||||
readonly __typename: 'SeqSort';
|
||||
|
||||
/**
|
||||
* Check if this is a string sort
|
||||
*/
|
||||
isString(): boolean;
|
||||
|
||||
/**
|
||||
* Get the element sort of this sequence
|
||||
*/
|
||||
basis(): Sort<Name>;
|
||||
|
||||
cast(other: Seq<Name>): Seq<Name>;
|
||||
cast(other: string): Seq<Name>;
|
||||
cast(other: CoercibleToExpr<Name>): Expr<Name>;
|
||||
}
|
||||
|
||||
/** @category String/Sequence */
|
||||
export interface StringCreation<Name extends string> {
|
||||
/**
|
||||
* Create a string sort
|
||||
*/
|
||||
sort(): SeqSort<Name>;
|
||||
|
||||
/**
|
||||
* Create a string constant
|
||||
*/
|
||||
const(name: string): Seq<Name>;
|
||||
|
||||
/**
|
||||
* Create multiple string constants
|
||||
*/
|
||||
consts(names: string | string[]): Seq<Name>[];
|
||||
|
||||
/**
|
||||
* Create a string value
|
||||
*/
|
||||
val(value: string): Seq<Name>;
|
||||
}
|
||||
|
||||
/** @category String/Sequence */
|
||||
export interface SeqCreation<Name extends string> {
|
||||
/**
|
||||
* Create a sequence sort over the given element sort
|
||||
*/
|
||||
sort<ElemSort extends Sort<Name>>(elemSort: ElemSort): SeqSort<Name, ElemSort>;
|
||||
|
||||
/**
|
||||
* Create an empty sequence
|
||||
*/
|
||||
empty<ElemSort extends Sort<Name>>(elemSort: ElemSort): Seq<Name, ElemSort>;
|
||||
|
||||
/**
|
||||
* Create a unit sequence (sequence with single element)
|
||||
*/
|
||||
unit<ElemSort extends Sort<Name>>(elem: Expr<Name>): Seq<Name, ElemSort>;
|
||||
}
|
||||
|
||||
/**
|
||||
* Sequence expression (includes strings)
|
||||
* @category String/Sequence
|
||||
*/
|
||||
export interface Seq<Name extends string = 'main', ElemSort extends Sort<Name> = Sort<Name>>
|
||||
extends Expr<Name, SeqSort<Name, ElemSort>, Z3_ast> {
|
||||
/** @hidden */
|
||||
readonly __typename: 'Seq';
|
||||
|
||||
/**
|
||||
* Check if this is a string value
|
||||
*/
|
||||
isString(): boolean;
|
||||
|
||||
/**
|
||||
* Get string value if this is a concrete string
|
||||
*/
|
||||
asString(): string;
|
||||
|
||||
/** @category Operations */
|
||||
concat(other: Seq<Name, ElemSort> | string): Seq<Name, ElemSort>;
|
||||
|
||||
/** @category Operations */
|
||||
length(): Arith<Name>;
|
||||
|
||||
/** @category Operations */
|
||||
at(index: Arith<Name> | number | bigint): Seq<Name, ElemSort>;
|
||||
|
||||
/** @category Operations */
|
||||
nth(index: Arith<Name> | number | bigint): Expr<Name>;
|
||||
|
||||
/** @category Operations */
|
||||
extract(offset: Arith<Name> | number | bigint, length: Arith<Name> | number | bigint): Seq<Name, ElemSort>;
|
||||
|
||||
/** @category Operations */
|
||||
indexOf(substr: Seq<Name, ElemSort> | string, offset?: Arith<Name> | number | bigint): Arith<Name>;
|
||||
|
||||
/** @category Operations */
|
||||
lastIndexOf(substr: Seq<Name, ElemSort> | string): Arith<Name>;
|
||||
|
||||
/** @category Operations */
|
||||
contains(substr: Seq<Name, ElemSort> | string): Bool<Name>;
|
||||
|
||||
/** @category Operations */
|
||||
prefixOf(s: Seq<Name, ElemSort> | string): Bool<Name>;
|
||||
|
||||
/** @category Operations */
|
||||
suffixOf(s: Seq<Name, ElemSort> | string): Bool<Name>;
|
||||
|
||||
/** @category Operations */
|
||||
replace(src: Seq<Name, ElemSort> | string, dst: Seq<Name, ElemSort> | string): Seq<Name, ElemSort>;
|
||||
|
||||
/** @category Operations */
|
||||
replaceAll(src: Seq<Name, ElemSort> | string, dst: Seq<Name, ElemSort> | string): Seq<Name, ElemSort>;
|
||||
}
|
||||
|
||||
/**
|
||||
* Defines the expression type of the body of a quantifier expression
|
||||
*
|
||||
|
|
|
|||
Loading…
Add table
Add a link
Reference in a new issue