This project is a visualizer for proof certificate generated by CVC5, a SMT solver. This website provides customizable views through graphs and tables that allow a better understanding of certificates and the operation of SMT solvers.
This project was bootstrapped with Create React App.
In the project directory, you can run:
Runs the app in the development mode.
Open http://localhost:3000 to view it in the browser.
The page will reload if you make edits.
You will also see any lint errors in the console.
Builds the app for production to the build folder.
It correctly bundles React in production mode and optimizes the build for the best performance.
The build is minified and the filenames include the hashes.
Your app is ready to be deployed!
See the section about deployment for more information.
Builds the app and publish it at the homepage URL given in the package.json.
The proof visualizer allows to run the CVC5 solver inside the browser. The WebAssembly binary used to run this in the browser is compiled via emscripten.
This pull request was made to give an easy way to compile the library to WebAssembly. Then, it is possible to generate the .wasm file needed to run the library inside the web app.
As the expectations to support this app are not that long, the user is able to use the cvc5 WebAssembly compilation, generate a .wasm file and substitute the current .wasm file located at /frontend/public/cvc5.wasm, using then a more recent version of CVC5.
The version of the emscripten used to compile the current binary is the 3.1.18 and the --wasm-flags='-s INCOMING_MODULE_JS_API=arguments -s INVOKE_RUN=1 -s MODULARIZE -s EXIT_RUNTIME=0 -s ENVIRONMENT=web'. To make sure the .wasm that will be generated by the user is compatible with the cvc5.js (the current modified glue code), it is important to use the same emscripten flags.