{model2}
+ | Model | +Satisfies your formula? | +Satisfies the secret formula? | +
|---|---|---|
+ {model1}
+ |
+ {icon(res1.user)} | ++ {icon(res1.secret)} + | +
+ {success ? ("") : timeout ? (
+ {`--${language} timeout--`}
+ ) : !result.output && !result.error ? ("Press 'Run' to run the sample") : (
+ Script contains one or more errors:
+
+ )}
+ {success
+ ? emptyOutput
+ ? "--Output is empty--"
+ : result.output
+ : !timeout && result.error}
+ );
+ const z3DuoOutputEl = (
+ {success ? ("") : (
+ Script contains one or more errors:
+
+ )} + {success + ? emptyOutput + ? "--Output is empty--" + : z3DuoTable + : result.error} +
);
+ return (+ )} + {success + ? emptyOutput + ? "--Output is empty--" + : z3DuoTable + : result.error} +
+ Output{codeChanged ? " (outdated)" : ""}:
+
+ {z3DuoOutput ? z3DuoOutputEl : regularOutput} +
);
+}
+function CustomCodeEditor(props) {
+ const { input, language, showLineNumbers, editable, githubRepo, onChange, readonly, } = props;
+ const prismTheme = usePrismTheme();
+ // console.log(prismTheme);
+ // the line above shows that we are still using `plain` for syntax highlighting
+ // despite that we have imported the language highlighting at the beginning
+ const isBrowser = useIsBrowser();
+ const component = (+ {z3DuoOutput ? z3DuoOutputEl : regularOutput} +
+
+ <>
+
);
+}
+export { GithubDiscussionBtn } from "./CodeBlock";
diff --git a/website/src/components/TutorialComponents/loadZ3.js b/website/src/components/TutorialComponents/loadZ3.js
new file mode 100644
index 000000000..572e2f12b
--- /dev/null
+++ b/website/src/components/TutorialComponents/loadZ3.js
@@ -0,0 +1,9 @@
+export default async function loadZ3() {
+ // eslint-disable-next-line @typescript-eslint/no-var-requires
+ const z3 = require('z3-solver');
+ // init z3
+ const z3p = window.z3Promise || (() => {
+ return window.z3Promise = z3.init();
+ })();
+ return z3p;
+}
diff --git a/website/src/components/TutorialComponents/runZ3DuoWeb.js b/website/src/components/TutorialComponents/runZ3DuoWeb.js
new file mode 100644
index 000000000..6690ae21d
--- /dev/null
+++ b/website/src/components/TutorialComponents/runZ3DuoWeb.js
@@ -0,0 +1,96 @@
+import loadZ3 from './loadZ3';
+import { Z3_error_code } from 'z3-solver';
+export default async function runZ3DuoWeb(user_input, secret_input) {
+ // init z3
+ const z3p = loadZ3();
+ const { Context, Z3: Z3Core } = await z3p;
+ const timeout = 10000;
+ Z3Core.global_param_set('timeout', String(timeout));
+ let Z3 = Context('main');
+ let output = '';
+ let error = '';
+ let outputObj;
+ const throwIfError = (ctxPtr) => {
+ if (Z3Core.get_error_code(ctxPtr) !== Z3_error_code.Z3_OK) {
+ throw new Error(Z3Core.get_error_msg(ctxPtr, Z3Core.get_error_code(ctxPtr)));
+ }
+ };
+ const startTime = (new Date()).getTime();
+ try {
+ const s1 = new Z3.Solver();
+ const s2 = new Z3.Solver();
+ s1.fromString(user_input);
+ s2.fromString(secret_input);
+ throwIfError(s1.ctx.ptr);
+ throwIfError(s2.ctx.ptr);
+ const not_user = Z3.Not(Z3.And(s1.assertions()));
+ const not_secret = Z3.Not(Z3.And(s2.assertions()));
+ s2.add(not_user);
+ s1.add(not_secret);
+ const user_not_secret = await s1.check();
+ const secret_not_user = await s2.check();
+ const sat = (s) => s === 'sat';
+ const unsat = (s) => s === 'unsat';
+ if (sat(secret_not_user) && sat(user_not_secret)) {
+ outputObj = {
+ model1: s2.model().sexpr(),
+ res1: {
+ secret: true,
+ user: false,
+ },
+ model2: s1.model().sexpr(),
+ res2: {
+ user: true,
+ secret: false
+ }
+ };
+ }
+ else if (sat(secret_not_user)) {
+ outputObj = {
+ model1: s2.model().sexpr(),
+ res1: {
+ secret: true,
+ user: false,
+ }
+ };
+ }
+ else if (sat(user_not_secret)) {
+ outputObj = {
+ model1: s1.model().sexpr(),
+ res1: {
+ user: true,
+ secret: false
+ }
+ };
+ }
+ else if (unsat(user_not_secret) && unsat(secret_not_user)) { // both unsat
+ output = `You got the right formula! Congratulations!`;
+ }
+ else {
+ output = 'unknown';
+ }
+ }
+ catch (e) {
+ // error with running z3
+ error = e.message ?? 'Error message is empty';
+ console.log({ error });
+ }
+ const timeEnd = (new Date()).getTime();
+ const unknownOutput = (/unknown/).test(output); // both unknown
+ const hasError = error !== '';
+ const timeoutError = (toAppend) => {
+ if (timeEnd - startTime >= timeout) {
+ return toAppend + '\nZ3 timeout\n';
+ }
+ return toAppend;
+ };
+ if (unknownOutput) {
+ output = timeoutError(output);
+ }
+ else if (hasError) {
+ error = timeoutError(error);
+ }
+ const finalOutput = outputObj ? JSON.stringify(outputObj) : output;
+ // we are guaranteed to have non-undefined output and error
+ return JSON.stringify({ output: finalOutput, error: error });
+}
diff --git a/website/src/components/TutorialComponents/runZ3JSWeb.js b/website/src/components/TutorialComponents/runZ3JSWeb.js
new file mode 100644
index 000000000..be1cad392
--- /dev/null
+++ b/website/src/components/TutorialComponents/runZ3JSWeb.js
@@ -0,0 +1,55 @@
+import { init } from 'z3-solver';
+let evalZ3JSPromise = null;
+async function loadEvalZ3() {
+ // typescript is several megabytes of JS
+ // so don't load it until someone actually calls it
+ if (evalZ3JSPromise != null) {
+ return evalZ3JSPromise;
+ }
+ evalZ3JSPromise = new Promise((res, rej) => {
+ const script = document.createElement('script');
+ script.src = '/z3guide/eval-z3.js';
+ script.onload = () => {
+ // eslint-disable-next-line @typescript-eslint/ban-ts-comment
+ // @ts-ignore eval-z3.js adds this binding to the global
+ // the name is defined in build.js
+ res(window.evalZ3Mod.evalZ3JS);
+ };
+ script.onerror = rej;
+ document.head.appendChild(script);
+ });
+ return evalZ3JSPromise;
+}
+let Z3Promise;
+async function loadZ3() {
+ if (Z3Promise != null) {
+ return Z3Promise;
+ }
+ Z3Promise = init();
+ return Z3Promise;
+}
+export default async function runZ3JSWeb(input) {
+ let output = '';
+ let error = '';
+ let timeStart, timeEnd = undefined;
+ const Z3 = await loadZ3();
+ const timeout = 10000;
+ try {
+ Z3.Z3.global_param_set('timeout', String(timeout));
+ timeStart = (new Date()).getTime();
+ const evalZ3JS = await loadEvalZ3();
+ output = await evalZ3JS(Z3, input) ?? '';
+ }
+ catch (e) {
+ // error with running z3
+ error = e.message ?? 'Error message is empty';
+ if (timeStart) {
+ timeEnd = (new Date()).getTime();
+ if (timeEnd - timeStart >= timeout) {
+ error = error + '\nZ3 timeout\n';
+ }
+ }
+ }
+ // we are guaranteed to have non-undefined output and error
+ return JSON.stringify({ output: String(output), error: error });
+}
diff --git a/website/src/components/TutorialComponents/runZ3PYWeb.js b/website/src/components/TutorialComponents/runZ3PYWeb.js
new file mode 100644
index 000000000..0585c118e
--- /dev/null
+++ b/website/src/components/TutorialComponents/runZ3PYWeb.js
@@ -0,0 +1,63 @@
+let _loadPyodideScriptPromise = null;
+async function loadPyodideScript() {
+ return new Promise((resolve, reject) => {
+ console.log(`loading pyodide`);
+ const script = document.createElement("script");
+ script.src = "https://cdn.jsdelivr.net/pyodide/v0.26.4/full/pyodide.js";
+ script.onload = () => resolve(globalThis.loadPyodide);
+ script.onerror = (e) => {
+ console.error(e);
+ reject(new Error("Failed to load Pyodide script"));
+ };
+ document.head.appendChild(script);
+ });
+}
+async function loadZ3Pyodide() {
+ if (_loadPyodideScriptPromise)
+ return _loadPyodideScriptPromise;
+ return (_loadPyodideScriptPromise = new Promise(async (resolve) => {
+ const loadPyodide = await loadPyodideScript();
+ //const { loadPyodide } = require('pyodide');
+ let pyodide = await loadPyodide();
+ await pyodide.loadPackage("micropip");
+ const micropip = pyodide.pyimport("micropip");
+ console.log(`loading z3`);
+ await micropip.install("https://microsoft.github.io/z3guide/z3_solver-4.13.4.0-py3-none-pyodide_2024_0_wasm32.whl");
+ console.log(`pyodide ready`);
+ resolve(pyodide);
+ }));
+}
+async function clearZ3Pyodide() {
+ console.log(`clearing pyodide`);
+ _loadPyodideScriptPromise = null;
+}
+async function runZ3PYWeb(input) {
+ const pyodide = await loadZ3Pyodide();
+ let output = "";
+ let error = "";
+ try {
+ if (!input.includes("from z3 import *"))
+ input = `from z3 import *\n${input}`;
+ console.log(`running python code: ${input}`);
+ pyodide.setStdout({
+ batched: (msg) => {
+ output += msg + "\n";
+ console.debug(msg);
+ },
+ });
+ pyodide.setStderr({
+ batched: (msg) => {
+ output += msg + "\n";
+ console.debug(msg);
+ },
+ });
+ pyodide.runPython(input);
+ }
+ catch (e) {
+ clearZ3Pyodide();
+ console.error(e);
+ error = e.message ?? "Error message is empty";
+ }
+ return JSON.stringify({ output: String(output), error: error });
+}
+export default runZ3PYWeb;
diff --git a/website/src/components/TutorialComponents/runZ3Web.js b/website/src/components/TutorialComponents/runZ3Web.js
new file mode 100644
index 000000000..da3dcba83
--- /dev/null
+++ b/website/src/components/TutorialComponents/runZ3Web.js
@@ -0,0 +1,33 @@
+import loadZ3 from "./loadZ3";
+export default async function runZ3Web(input) {
+ // init z3
+ const z3p = loadZ3();
+ const { Z3 } = await z3p;
+ // done on every snippet
+ const cfg = Z3.mk_config();
+ const ctx = Z3.mk_context(cfg);
+ Z3.del_config(cfg);
+ const timeStart = (new Date()).getTime();
+ const timeout = 10000;
+ Z3.global_param_set('timeout', String(timeout));
+ let output = '';
+ let error = '';
+ try {
+ output = await Z3.eval_smtlib2_string(ctx, input) ?? '';
+ }
+ catch (e) {
+ // error with running z3
+ error = e.message ?? 'Error message is empty';
+ }
+ finally {
+ Z3.del_context(ctx);
+ }
+ if ((/unknown/).test(output)) {
+ const timeEnd = (new Date()).getTime();
+ if (timeEnd - timeStart >= timeout) {
+ output = output + '\nZ3 timeout\n';
+ }
+ }
+ // we are guaranteed to have non-undefined output and error
+ return JSON.stringify({ output: String(output), error: error });
+}
diff --git a/website/src/eval-z3/eval-z3.js b/website/src/eval-z3/eval-z3.js
new file mode 100644
index 000000000..deff6c738
--- /dev/null
+++ b/website/src/eval-z3/eval-z3.js
@@ -0,0 +1,168 @@
+import * as ts from 'typescript';
+const MAIN = 'main.ts';
+function compile(source, fixupErrorLocations) {
+ let libs = TS_LIBS;
+ let options = {
+ module: ts.ModuleKind.None,
+ // comments interfere with codegen when mutating the AST `//a\nb` gets transformed to `return\n//a\nb`, instead of `//a\nreturn b\n`.
+ removeComments: true,
+ lib: ['lib.es2021.d.ts'],
+ target: ts.ScriptTarget.ES2021,
+ strict: true,
+ };
+ // @ts-ignore https://github.com/microsoft/TypeScript/issues/38385
+ let createdFiles = { __proto__: null };
+ let host = {
+ readFile: fileName => {
+ // console.log('reading', fileName);
+ if (fileName in libs) {
+ return libs[fileName];
+ }
+ return undefined;
+ },
+ writeFile: (fileName, content) => {
+ createdFiles[fileName] = content;
+ },
+ getSourceFile: (fileName, languageVersion) => {
+ if (fileName === MAIN) {
+ return source;
+ }
+ let sourceText = host.readFile(fileName);
+ let result = sourceText !== undefined ? ts.createSourceFile(fileName, sourceText, languageVersion) : undefined;
+ if (fileName.includes('main'))
+ debugger;
+ return result;
+ },
+ getDefaultLibFileName: () => 'lib.d.ts',
+ getCurrentDirectory: () => '/',
+ getDirectories: () => [],
+ getCanonicalFileName: fileName => fileName,
+ getNewLine: () => '\n',
+ useCaseSensitiveFileNames: () => true,
+ fileExists: fileName => {
+ // TODO
+ // console.log('checking', fileName);
+ return false;
+ },
+ resolveModuleNames,
+ };
+ function resolveModuleNames(moduleNames, containingFile) {
+ // console.log('resolving', moduleNames, 'for', containingFile);
+ return moduleNames.map(name => {
+ if (name === 'z3-solver') {
+ return {
+ resolvedFileName: '/node_modules/z3-solver/build/browser.d.ts',
+ isExternalLibraryImport: true,
+ };
+ }
+ else if (containingFile.startsWith('/node_modules/z3-solver/build/')) {
+ // this is only a small portion of TypeScript's resolution algorithm
+ // but it's sufficient for the files in z3-solver
+ let root = containingFile.split('/').slice(0, -1).join('/');
+ let joined = root + '/' + name;
+ joined = joined.replace(/(\/[^/]+\/\.\.\/)|(\/\.\/)/g, '/');
+ for (let suffix of ['', '.d.ts', '/index.d.ts']) {
+ let candidate = joined + suffix;
+ if (candidate in libs) {
+ return {
+ resolvedFileName: candidate,
+ isExternalLibraryImport: false,
+ };
+ }
+ }
+ throw new Error(`relative import of z3-solver internal file ${name} for ${containingFile} failed`);
+ }
+ throw new Error(`could not find module ${name}`);
+ });
+ }
+ let program = ts.createProgram([MAIN], options, host);
+ let emitResult = program.emit();
+ let diagnostics = ts
+ .getPreEmitDiagnostics(program)
+ .concat(emitResult.diagnostics)
+ .map(diagnostic => {
+ if (diagnostic.file) {
+ let { line, character: column } = ts.getLineAndCharacterOfPosition(diagnostic.file, diagnostic.start);
+ ({ line, column } = fixupErrorLocations({ line, column }));
+ let message = ts.flattenDiagnosticMessageText(diagnostic.messageText, '\n');
+ return `${diagnostic.file.fileName} (${line + 1},${column + 1}): ${message}`;
+ }
+ else {
+ return ts.flattenDiagnosticMessageText(diagnostic.messageText, '\n');
+ }
+ });
+ if (diagnostics.length > 0) {
+ return { success: false, message: diagnostics.join('\n') };
+ }
+ if (emitResult.emitSkipped || !('main.js' in createdFiles)) {
+ return { success: false, message: 'typechecking failed with unknown error' };
+ }
+ return { success: true, result: createdFiles['main.js'] };
+}
+// - takes a snippet like `let x = Z3.foo(); await Z3.check(x);`
+// - puts it in a context where `Z3` is defined and `await` works
+// - modifies the last expression to be a return statement, like `let x = Z3.foo(); return await Z3.check(x);`
+// - typechecks the result
+// - and strips types
+// successful output looks like `"use strict"; module.exports = (async () => { ... })();`
+export function compileZ3JS(src) {
+ let imports = `
+ import type { init as initT, Model, Solver, BitVecNum, AstVector, Arith } from 'z3-solver';
+ declare let init: typeof initT;
+ declare let { Context, setParam }: Awaited
+ {!isZ3Duo && !readonly && !editable && !outputRendered && ()}
+ {(isZ3Duo ||
+ (!readonly && (editable || outputRendered))) && ()}
+
+ {outputRendered ? (
+
);
+}
+export default function Home() {
+ const { siteConfig } = useDocusaurusContext();
+ return (
+
+
+
+
+
+ {siteConfig.title}
+{siteConfig.tagline}
+
+
+ SMTLIB Tutorial
+
+ <>
+
+ Programming Z3
+
+ <>
+
+ Playground
+
+
+
+ {/* 
*/}
+ .default}/)
+
+ */}
+
+