z3-wasm support #19
Comments
|
The format should be: It is missing some It still doesn't work through the wasm front end. This is not specific to wasm, but because we are replicating the command-line interpreter functionality over the API. When you run z3.exe from the command-line it will be in a different state than the command-line interpreter over the interface. There we can't change the proof state. |
|
Perhaps obvious: If there are syntax errors from z3 ask me (Kevin is two levels of indirection from z3 internals, but wasm connoisseur). |
|
Way to troubleshoot syntax errors over web:
|
|
I have no clue how node.js works. |
|
I think the |
|
|
you probably want to use child_process.exec which returns the output, but yes pretty much that. Recommend moving to creating subfolders for each sample rather files. |
|
What should be done with Github Action to accomplish this? https://github.com/Z3Prover/z3/actions/runs/2585405315/workflow |
|
@rlisahuang can you split the node.js vs z3 formatting issues? |
|
There is an example in the documentation for using the low-level API from node. Just replace Or if you want something which doesn't require typescript or building at all: 'use strict';
let { init } = require('z3-solver');
(async () => {
let { em, Z3 } = await init();
let config = Z3.mk_config();
let ctx = Z3.mk_context_rc(config);
Z3.del_config(config);
// Z3.global_param_set('verbose', '10');
console.log(await Z3.eval_smtlib2_string(ctx, `
(declare-fun f (Int) Int)
(declare-fun a () Int) ; a is a constant
(declare-const b Int) ; syntax sugar for (declare-fun b () Int)
(assert (> a 20))
(assert (> b a))
(assert (= (f 10) 1))
(check-sat)
(get-model)
`));
Z3.del_context(ctx);
em.PThread.terminateAllThreads();
})().catch(e => {
console.error('error', e);
process.exit(1);
}); |
|
Very useful. Do you have an example of running multiple |
|
|
|
Thanks @bakkot for the help! We are now able to run z3-wasm synchronously on the web. Closing this issue for now and moving the conversations on mismatched behavior between z3-wasm and executable to a separate issue. |
Context
I encountered some issues with getting the TypeScript bindings to work in Node.js. The idea is to break down a given code snippet (in the smt2 format) by line and obtain the output through
Z3.eval_smtlib2_string. My main reference is this z3-wasm webpage, which uses our official WASM build. The way inputs are processed is detailed in theirmain.jsfile.Problem with Node.js
Note that this website runs z3-wasm in the browser from the client side, while we want to run z3-wasm with Node.js from the server side. Therefore, their logic for running Z3 does not work in our scenario -- I had
RuntimeErrors complaining about the inability to findz3-built.wasm. My implementation for running Z3 (currently commented out) can be found inwebsite/src/remark/render-code-blocks.mjsin PR #18 .Additional issue(s) with z3-wasm
I also noticed that several code snippets from our tutorial would not work in the web interface cited above. I wonder if this is a bug with the WASM build, or if there are additional API calls we should use instead for such code snippets. An example of snippet that does not work in the web interface:
I got a bunch of syntax errors when I ran it in that web interface.
@NikolajBjorner We would like some help from Kevin on the following issues:
The text was updated successfully, but these errors were encountered: