mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-06-02 04:11:21 +00:00
Code Activity

fixing interface and test'

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2022-08-18 12:59:00 -07:00
parent 103cd248f1
commit c7eda4e687
2 changed files with 2 additions and 1 deletions
Download patch file Download diff file Expand all files Collapse all files

2
src/api/js/src/high-level/high-level.test.ts
View file

@ -110,7 +110,7 @@ describe('high-level', () => {
}); });
it('test loading a solver state from a string', async () => { it('test loading a solver state from a string', async () => {
const { Solver } = api.Context('main'); const { Solver, Not, Int } = api.Context('main');
const solver = new Solver(); const solver = new Solver();
solver.fromString("(declare-const x Int) (assert (and (< x 2) (> x 0)))") solver.fromString("(declare-const x Int) (assert (and (< x 2) (> x 0)))")
expect(await solver.check()).toStrictEqual('sat') expect(await solver.check()).toStrictEqual('sat')

1
src/api/js/src/high-level/types.ts
View file

@ -398,6 +398,7 @@ export interface Solver<Name extends string = 'main'> {
add(...exprs: (Bool<Name> | AstVector<Name, Bool<Name>>)[]): void; add(...exprs: (Bool<Name> | AstVector<Name, Bool<Name>>)[]): void;
addAndTrack(expr: Bool<Name>, constant: Bool<Name> | string): void; addAndTrack(expr: Bool<Name>, constant: Bool<Name> | string): void;
assertions(): AstVector<Name, Bool<Name>>; assertions(): AstVector<Name, Bool<Name>>;
from_string(s : string): void;
check(...exprs: (Bool<Name> | AstVector<Name, Bool<Name>>)[]): Promise<CheckSatResult>; check(...exprs: (Bool<Name> | AstVector<Name, Bool<Name>>)[]): Promise<CheckSatResult>;
model(): Model<Name>; model(): Model<Name>;
} }