diff --git a/src/api/js/src/high-level/high-level.test.ts b/src/api/js/src/high-level/high-level.test.ts index 0a8245301..78b003b89 100644 --- a/src/api/js/src/high-level/high-level.test.ts +++ b/src/api/js/src/high-level/high-level.test.ts @@ -110,7 +110,7 @@ describe('high-level', () => { }); 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(); solver.fromString("(declare-const x Int) (assert (and (< x 2) (> x 0)))") expect(await solver.check()).toStrictEqual('sat') diff --git a/src/api/js/src/high-level/types.ts b/src/api/js/src/high-level/types.ts index d8bda01a1..838a6ef11 100644 --- a/src/api/js/src/high-level/types.ts +++ b/src/api/js/src/high-level/types.ts @@ -398,6 +398,7 @@ export interface Solver { add(...exprs: (Bool | AstVector>)[]): void; addAndTrack(expr: Bool, constant: Bool | string): void; assertions(): AstVector>; + from_string(s : string): void; check(...exprs: (Bool | AstVector>)[]): Promise; model(): Model; }