mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-12 20:18:18 +00:00
Code Activity

test fromString

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2022-08-18 12:41:02 -07:00
parent 53e168879a
commit 6fb7a049ea
1 changed files with 10 additions and 0 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

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

@ -109,6 +109,16 @@ describe('high-level', () => {
expect(await solver.check()).toStrictEqual('unsat'); expect(await solver.check()).toStrictEqual('unsat');
}); });
it('test loading a solver state from a string', async () => {
const { Solver } = 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')
const x = Int.const('x')
solver.add(Not(x.eq(1)))
expect(await solver.check()).toStrictEqual('unsat')
}
it('disproves x = y implies g(g(x)) = g(y)', async () => { it('disproves x = y implies g(g(x)) = g(y)', async () => {
const { Solver, Int, Function, Implies, Not } = api.Context('main'); const { Solver, Int, Function, Implies, Not } = api.Context('main');
const solver = new Solver(); const solver = new Solver();