From c680ba77b2b216101612abfc573f9557faec7cf7 Mon Sep 17 00:00:00 2001
From: "copilot-swe-agent[bot]" <198982749+Copilot@users.noreply.github.com>
Date: Tue, 9 Jun 2026 22:42:56 +0000
Subject: [PATCH 1/3] chore: plan dependency security updates
---
.../src/components/HomepageFeatures/index.js | 24 ++
.../TutorialComponents/CodeBlock.js | 165 ++++++++++++++
.../TutorialComponents/CodeEditor.js | 85 +++++++
.../components/TutorialComponents/index.js | 212 ++++++++++++++++++
.../components/TutorialComponents/loadZ3.js | 9 +
.../TutorialComponents/runZ3DuoWeb.js | 96 ++++++++
.../TutorialComponents/runZ3JSWeb.js | 55 +++++
.../TutorialComponents/runZ3PYWeb.js | 63 ++++++
.../components/TutorialComponents/runZ3Web.js | 33 +++
website/src/eval-z3/eval-z3.js | 168 ++++++++++++++
website/src/pages/index.js | 43 ++++
11 files changed, 953 insertions(+)
create mode 100644 website/src/components/HomepageFeatures/index.js
create mode 100644 website/src/components/TutorialComponents/CodeBlock.js
create mode 100644 website/src/components/TutorialComponents/CodeEditor.js
create mode 100644 website/src/components/TutorialComponents/index.js
create mode 100644 website/src/components/TutorialComponents/loadZ3.js
create mode 100644 website/src/components/TutorialComponents/runZ3DuoWeb.js
create mode 100644 website/src/components/TutorialComponents/runZ3JSWeb.js
create mode 100644 website/src/components/TutorialComponents/runZ3PYWeb.js
create mode 100644 website/src/components/TutorialComponents/runZ3Web.js
create mode 100644 website/src/eval-z3/eval-z3.js
create mode 100644 website/src/pages/index.js
diff --git a/website/src/components/HomepageFeatures/index.js b/website/src/components/HomepageFeatures/index.js
new file mode 100644
index 000000000..bee9925d1
--- /dev/null
+++ b/website/src/components/HomepageFeatures/index.js
@@ -0,0 +1,24 @@
+import React from 'react';
+import clsx from 'clsx';
+import styles from './styles.module.css';
+const FeatureList = [];
+function Feature({ title, Svg, description }) {
+ return (
+
+
+
+
+
{title}
+
{description}
+
+
+
+ {FeatureList.map((props, idx) => ())}
+
+
+
+ {({ className: _className, tokens, getLineProps, getTokenProps, style: _style, }) => (
+ {props.showLineNumbers && (
+ {tokens.map((line, i) => (<>
+ {i + 1}
+
+ ))}
+ )}
+
+
+ {tokens.map((line, lineIndex) => (
+ // eslint-disable-next-line react/jsx-key
+
+ {line
+ .filter((token) => !token.empty)
+ .map((token, tokenIndex) => (
+ // eslint-disable-next-line react/jsx-key
+ ))}
+ {"\n"}
+
))}
+
+
+
+
+
+ {!props.readonly && !allowUndo && ()}
+ {!props.readonly && allowUndo && ()}
+ {props.githubRepo && ()}
+
+
+
+
+
+ {!props.readonly && !allowUndo && }
+ {!props.readonly && allowUndo && }
+ {props.githubRepo && }
+
+
+
+ {model2}
+ |
+ {icon(res2.user)} |
+
+ {icon(res2.secret)}
+ |
+
) : (<>);
+ return (
+
+ | Model |
+ Satisfies your formula? |
+ Satisfies the secret formula? |
+
+
+
+ {model1}
+ |
+ {icon(res1.user)} |
+
+ {icon(res1.secret)}
+ |
+
+ {secondRow}
+
);
+ };
+ const z3DuoTable = z3DuoOutput ? (buildOutput(z3DuoOutput.model1, z3DuoOutput.res1, z3DuoOutput.model2, z3DuoOutput.res2)) : (<>);
+ const regularOutput = (
+ {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 (
+ 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 = (
+ {editable ? () : ()}
+ );
+ return <>{isBrowser ? component : <>};
+}
+export default function CustomCodeBlock(props) {
+ let { input } = props;
+ if (typeof input === "string")
+ input = JSON.parse(input);
+ if (typeof input !== "object")
+ throw new Error("Invalid input");
+ const { lang, highlight, statusCodes, code, result, githubRepo, editable, showLineNumbers, readonly, } = input;
+ const isZ3Duo = lang === "z3-duo";
+ const [currCode, setCurrCode] = useState(code);
+ const [outputRendered, setOutputRendered] = useState(false);
+ const [runFinished, setRunFinished] = useState(true);
+ const [output, setOutput] = useState(result);
+ const [lastSnippet, setLastSnippet] = useState(code);
+ const codeChanged = lastSnippet !== currCode;
+ const onDidClickOutputToggle = () => {
+ setOutputRendered(!outputRendered);
+ };
+ // bypassing server-side rendering
+ const onDidClickRun = async () => {
+ setRunFinished(false);
+ const newResult = { ...result };
+ let errorMsg;
+ const runProcess = clientConfig[lang];
+ let input = currCode;
+ let process = isZ3Duo
+ ? runProcess(input, result.output)
+ : runProcess(input);
+ // `z3.interrupt` -- set the cancel status of an ongoing execution, potentially with a timeout (soft? hard? we should use hard)
+ try {
+ let res = await process;
+ const result = JSON.parse(res);
+ if (result.output !== "") {
+ const errRegex = /(\(error)|(unsupported)|([eE]rror:)/;
+ const hasError = errRegex.test(result.output);
+ newResult.output = hasError ? "" : result.output;
+ newResult.error = hasError ? result.output : "";
+ newResult.status = hasError
+ ? statusCodes.runtimeError
+ : statusCodes.success;
+ }
+ else if (result.error !== "") {
+ newResult.error = result.error;
+ if (/timeout/.test(result.error)) {
+ newResult.status = statusCodes.timeout;
+ }
+ else {
+ newResult.status = statusCodes.runError;
+ }
+ }
+ else {
+ // no output nor error
+ newResult.output = "";
+ newResult.error = "";
+ newResult.status = statusCodes.success;
+ }
+ }
+ catch (error) {
+ errorMsg = `${lang}-web failed with input:\n${currCode}\n\nerror:\n${error}`;
+ newResult.error = errorMsg;
+ newResult.status = `${lang}-web-failed`;
+ throw new Error(errorMsg);
+ }
+ finally {
+ setLastSnippet(input);
+ setOutput(newResult);
+ setRunFinished(true);
+ if (!outputRendered) {
+ setOutputRendered(true); // hack for the playground editor
+ }
+ }
+ };
+ const onDidChangeCode = (code) => {
+ setCurrCode(code);
+ };
+ return (
+
+ <>
+
+ {!isZ3Duo && !readonly && !editable && !outputRendered && ()}
+ {(isZ3Duo ||
+ (!readonly && (editable || outputRendered))) && ()}
+
+ {outputRendered ? (
+
+
+
+
{siteConfig.title}
+
{siteConfig.tagline}
+
+
+ SMTLIB Tutorial
+
+ <>
+
+ Programming Z3
+
+ <>
+
+ Playground
+
+
+
+
+ {/*
*/}
+
.default}/)
+
+
+
+