Guessing the secret formula (#116)

* language config and test file for z3-duo

* parsing z3-duo block

* only show RunButton for z3-duo

* run button text for z3-duo

* copied NB's check solution snippet over

website/docs-smtlib/07 - games/01 - test.md

@@ -0,0 +1,11 @@
+---
+title: Guessing Game Tests
+sidebar_position: 1
+---
+
+```z3-duo
+(declare-const x Int)
+------
+(declare-const x Int)
+(assert (= (mod x 2) 0))
+```

website/language.config.js

@@ -50,7 +50,16 @@ async function createConfig() {
                 showLineNumbers: true, // whether to show line numbers in all code block of this language
                 githubRepo: 'Z3Prover/z3',
                 githubDiscussion: true,
-            }
+            },
+            {
+                name: 'Z3 Secret Formula Guessing',
+                label: 'z3-duo',
+                highlight: 'lisp',
+                showLineNumbers: true, // whether to show line numbers in all code block of this language
+                githubRepo: 'Z3Prover/z3',
+                githubDiscussion: true,
+                readonly: false,
+            },
         ],
         solutionsDir: './solutions',
     }

website/sidebars/smtlibSidebars.js

@@ -95,6 +95,16 @@ const sidebars = {
         'fixedpoints/syntax'
       ]
     },
+
+    {
+      type: 'category',
+      label: 'GuessingGames',
+      collapsible: true,
+      collapsed: true,
+      items: [
+        'games/test',
+      ]
+    },
   ]
 
 };

website/src/components/TutorialComponents/index.tsx

@@ -24,6 +24,7 @@ import runZ3JSWeb from "./runZ3JSWeb";
 const clientConfig = {
   'z3': runZ3Web,
   'z3-js': runZ3JSWeb,
+  'z3-duo': runZ3JSWeb,
 };
 
 interface CodeBlockProps {
@@ -50,11 +51,12 @@ function OutputToggle(props: { onClick: () => void, disabled?: boolean, version?
   );
 }
 
-function RunButton(props: { onClick: () => void, runFinished: boolean }) {
-  const { onClick, runFinished } = props;
+function RunButton(props: { onClick: () => void, runFinished: boolean, isZ3Duo: boolean }) {
+  const { onClick, runFinished, isZ3Duo } = props;
+  const text = isZ3Duo ? "Check" : "Run";
   return (
     <button className="button button--primary" onClick={onClick}>
-      {runFinished ? `Run` : "Running..."}
+      {runFinished ? text : "Running..."}
     </button>
   );
 }
@@ -142,6 +144,9 @@ export default function CustomCodeBlock(props: { input: CodeBlockProps }) {
   const { input } = props;
   const { lang, highlight, statusCodes, code, result, githubRepo, editable, showLineNumbers, readonly } = input
 
+  const isZ3Duo = lang === "z3-duo";
+
+
   const [currCode, setCurrCode] = useState(code);
 
   const [codeChanged, setCodeChanged] = useState(false);
@@ -164,8 +169,30 @@ export default function CustomCodeBlock(props: { input: CodeBlockProps }) {
     let errorMsg;
 
     const runProcess = clientConfig[lang];
+    const z3DuoCode = `const s1 = new Z3.Solver()
+    const s2 = new Z3.Solver()
+    s1.from_string(user_input)
+    s2.from_string(secret_input)
+    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 secret_not_user = await s2.check()
+    const user_not_secret = await s1.check()
+    if (secret_not_user == "sat")
+        // say   s2.model().sexpr() satisfies secret but not user formula
+    if (user_not_secret == "sat")
+       // etc`;
+
+    let input = currCode;
+    if (isZ3Duo) {
+      input = `let user_input = ${currCode}
+      let secret_input = ${result.output}
+      ${z3DuoCode}`
+    }
+
     // `z3.interrupt` -- set the cancel status of an ongoing execution, potentially with a timeout (soft? hard? we should use hard)
-    runProcess(currCode)
+    runProcess(input)
       .then((res: string) => {
         const result = JSON.parse(res);
         if (result.output !== '') {
@@ -203,6 +230,7 @@ export default function CustomCodeBlock(props: { input: CodeBlockProps }) {
     if (outputRendered) setCodeChanged(true);
   };
 
+
   return (
     <div>
       <CustomCodeEditor
@@ -217,8 +245,8 @@ export default function CustomCodeBlock(props: { input: CodeBlockProps }) {
       />
       <>
         <div className={styles.buttons}>
-          {!readonly && !editable && !outputRendered && <OutputToggle onClick={onDidClickOutputToggle} />}
-          {!readonly && (editable || outputRendered) && <RunButton onClick={onDidClickRun} runFinished={runFinished} />}
+          {(!isZ3Duo && !readonly && !editable && !outputRendered) && <OutputToggle onClick={onDidClickOutputToggle} />}
+          {(isZ3Duo || !readonly && (editable || outputRendered)) && <RunButton isZ3Duo={isZ3Duo} onClick={onDidClickRun} runFinished={runFinished} />}
         </div>
         {outputRendered ? (
           <Output

website/src/remark/render-code-blocks.mjs

@@ -172,6 +172,7 @@ export default function plugin() {
             const editableRegex = /(always-editable)/;
             const alwaysEditable = editableRegex.test(meta);
             const lineNumRegex = /(show-line-numbers)/i;
+            const splitterRegex = /------/;
 
 
             for (const langConfig of languageConfig.languages) {
@@ -183,7 +184,7 @@ export default function plugin() {
                 // or for a specific block through `show-line-numbers`
                 // e.g. ```z3 show-line-numbers
                 const showLineNumbers = langConfig.showLineNumbers || lineNumRegex.test(meta);
-
+                
                 if (lang !== label) {
                     continue; // onto the next lang config available until we are out
                 }
@@ -193,15 +194,28 @@ export default function plugin() {
                 if (!langConfig.buildConfig) {
                     // there is no runtime configured,
                     // so just add the syntax highlighting and github discussion button (if configured)
+
+                    let code = value;
+                    let result = {};
+
+                    // hard-coded for z3-duo
+                    const splitter = splitterRegex.test(value);
+
+                    if (splitter) {
+                        const [starter, solution] = value.split(splitterRegex).map(s => s.trim());
+                        code = starter;
+                        result = {output: solution};
+                    }
+
                     const val = JSON.stringify({
                         lang: lang,
                         highlight: highlight,
                         statusCodes: {},
-                        code: value,
-                        result: {},
+                        code: code,
+                        result: result,
                         githubRepo: githubRepo,
-                        editable: false,
-                        readonly: true,
+                        editable: lang === 'z3-duo',
+                        readonly: langConfig.readonly ?? true,
                         showLineNumbers: showLineNumbers
                     });
                     parent.children.splice(