return to wasm

babaeee · Jan 8, 2024 · 6198910 · 6198910
1 parent bd7939d
commit 6198910
Show file tree

Hide file tree

Showing 16 changed files with 273 additions and 81 deletions.
diff --git a/.github/workflows/build_example_web.yml b/.github/workflows/build_example_web.yml
@@ -76,14 +76,14 @@ jobs:
           node-version: "16"
 
       # enable in wasm mode:
-      # - name: Build wasm
-      #   run: |
-      #     cd hakim-json
-      #     EMCC_CFLAGS="-s TOTAL_STACK=32MB" cargo build -vv --release --target wasm32-unknown-emscripten
-      #     cd ..
-      #     node scripts/patch-emscripten.js ./target/wasm32-unknown-emscripten/release/hakim-json.js
-      #     cp ./target/wasm32-unknown-emscripten/release/hakim-json.js ./front/static/.
-      #     cp ./target/wasm32-unknown-emscripten/release/hakim_json.wasm ./front/static/.
+       - name: Build wasm
+         run: |
+           cd hakim-json
+           EMCC_CFLAGS="-s TOTAL_STACK=32MB -s INITIAL_MEMORY=64MB" cargo build -vv --release --target wasm32-unknown-emscripten
+           cd ..
+           node scripts/patch-emscripten.js ./target/wasm32-unknown-emscripten/release/hakim-json.js
+           cp ./target/wasm32-unknown-emscripten/release/hakim-json.js ./front/static/.
+           cp ./target/wasm32-unknown-emscripten/release/hakim_json.wasm ./front/static/.
 
       # Runs a set of commands using the runners shell
       - name: Build www

diff --git a/.github/workflows/preview.yml b/.github/workflows/preview.yml
@@ -23,14 +23,14 @@ jobs:
         with:
           node-version: "16"
       # enable in wasm mode:
-      # - name: Build wasm
-      #   run: |
-      #     cd hakim-json
-      #     EMCC_CFLAGS="-s TOTAL_STACK=32MB" cargo build -vv --release --target wasm32-unknown-emscripten
-      #     cd ..
-      #     node scripts/patch-emscripten.js ./target/wasm32-unknown-emscripten/release/hakim-json.js
-      #     cp ./target/wasm32-unknown-emscripten/release/hakim-json.js ./front/static/.
-      #     cp ./target/wasm32-unknown-emscripten/release/hakim_json.wasm ./front/static/.
+       - name: Build wasm
+         run: |
+           cd hakim-json
+           EMCC_CFLAGS="-s TOTAL_STACK=32MB" cargo build -vv --release --target wasm32-unknown-emscripten
+           cd ..
+           node scripts/patch-emscripten.js ./target/wasm32-unknown-emscripten/release/hakim-json.js
+           cp ./target/wasm32-unknown-emscripten/release/hakim-json.js ./front/static/.
+           cp ./target/wasm32-unknown-emscripten/release/hakim_json.wasm ./front/static/.
       - name: Build www
         run: |
           cd front

diff --git a/.gitignore b/.gitignore
@@ -4,3 +4,4 @@ perf.data*
 flamegraph.svg
 .z3-trace
 hakim_log*
+node_modules
diff --git a/front/src/components/proof/Toolbar.tsx b/front/src/components/proof/Toolbar.tsx
@@ -1,6 +1,6 @@
 import { useEffect, useState } from "react";
 import { normalPrompt } from "../../dialog";
-import { sendTactic, subscribe, tryAuto, TryAutoResult } from "../../hakim";
+import { sendTactic, subscribe, tryAuto, TryAutoResult, z3Solved } from "../../hakim";
 import { g } from "../../i18n";
 import css from "./toolbar.module.css";
 import logo from "../../logo.png"
@@ -51,8 +51,12 @@ const AutoProofButton = () => {
             const r = await tryAuto();
             if (mode === 'boost') {
                 if (r.available) {
-                    for (const tac of r.tactic) {
-                        await sendTactic(tac);
+                    if (r.tactic[0] === "z3_solved") {
+                        z3Solved();
+                    } else {
+                        for (const tac of r.tactic) {
+                            await sendTactic(tac);
+                        }
                     }
                 }
             } else {
@@ -73,8 +77,13 @@ const AutoProofButton = () => {
                         return;
                     }
                     if (s.available) {
-                        for (const tac of s.tactic) {
-                            await sendTactic(tac);
+                        console.log(s.tactic[0]);
+                        if (s.tactic[0] === "z3_solved") {
+                            z3Solved();
+                        } else {
+                            for (const tac of s.tactic) {
+                                await sendTactic(tac);
+                            }
                         }
                     } else if (mode === 'boost') {
                         setMode('normal');

diff --git a/front/src/hakim/index.ts b/front/src/hakim/index.ts
@@ -1,7 +1,8 @@
 import { normalPrompt } from "../dialog";
 import { fromRust } from "../i18n";
 import { loadLibText } from "./lib_text";
-import { hakimQueryImpl } from "./network_provider";
+import { hakimQueryImpl } from "./wasm_provider";
+import { init } from "z3-solver";
 
 declare let window: Window & {
   ask_question: (q: string) => Promise<string>;
@@ -43,10 +44,13 @@ type Instance = {
   [key: string]: (x?: any) => Promise<any>;
 };
 
-// await window.hakimQueryLoad;
+await window.hakimQueryLoad;
 
 let queryLock = false;
 
+const { Context, em } = await init();
+const Z3 = Context('main');
+
 const instance: Instance = new Proxy(
   {},
   {
@@ -65,6 +69,18 @@ const instance: Instance = new Proxy(
               arg: answer,
             });
           }
+          if (r && typeof r === "object" && r.Z3State) {
+            const solver = new Z3.Solver();
+
+            solver.fromString(r.Z3State);
+            solver.set("timeout", 1500);
+            let sat = await solver.check();
+            if (sat === 'unsat') {
+              r = "z3_solved";
+            } else {
+              r = "z3_cant_solve";
+            }
+          }
           queryLock = false;
           return r;
         } catch (e) {
@@ -103,15 +119,15 @@ export type State = {
   undoHistory: string[];
   redoHistory: string[];
 } & (
-  | { isFinished: true }
-  | {
+    | { isFinished: true }
+    | {
       isFinished: false;
       monitor: {
         hyps: string[];
         goals: string[];
       };
     }
-);
+  );
 
 type EventListener = (s: State) => void;
 
@@ -185,13 +201,28 @@ const checkErrorAndUpdate = async (
   return false;
 };
 
+const checkErrorOfTacticAndUpdate = async (
+  error: () => Promise<string | undefined>
+) => {
+  let r = await error();
+  if (r === 'z3_solved') {
+    return checkErrorAndUpdate(() => z3Solved());
+  }
+  if (checkError(r)) {
+    emit();
+    return true;
+  } else {
+    return false;
+  }
+};
+
 export const getActionHint = (tactic: string) => {
   return instance.action_of_tactic(tactic);
 };
 
 export const sendTactic = (tactic: string) => {
   console.log(`tactic: `, tactic);
-  return checkErrorAndUpdate(() => instance.run_tactic(tactic));
+  return checkErrorOfTacticAndUpdate(() => instance.run_tactic(tactic));
 };
 
 export const notationList = (): Promise<string[]> => {
@@ -202,6 +233,10 @@ export const getNatural = async (): Promise<string> => {
   return fromRust((await instance.natural()) || "$invalid_state");
 };
 
+export const z3Solved = (): Promise<string | undefined> => {
+  return instance.z3_solved();
+}
+
 export const tryTactic = (tactic: string): boolean => {
   return true; //window.hakimQuery({ command: "try_tactic", arg: tactic });
 };
@@ -333,23 +368,33 @@ export const suggMenuGoal = async () => {
 };
 
 export type TryAutoResult =
+  {
+    available: false;
+  }
   | {
-      available: false;
-    }
-  | {
-      available: true;
-      type: "normal" | "history";
-      tactic: string[];
-    };
+    available: true;
+    type: "normal" | "history";
+    tactic: string[];
+  };
 
 export const tryAuto = async (): Promise<TryAutoResult> => {
   const tactic = await instance.try_auto();
+
   if (tactic) {
-    return {
-      available: true,
-      type: "normal",
-      tactic: [tactic],
-    };
+    if (tactic === 'z3_solved') {
+      return {
+        available: true,
+        type: "normal",
+        tactic: ["z3_solved"],
+      };
+    }
+    if (tactic !== 'z3_cant_solve') {
+      return {
+        available: true,
+        type: "normal",
+        tactic: [tactic],
+      };
+    }
   }
   const history_tactics = await instance.try_auto_history();
   if (history_tactics) {

diff --git a/front/src/hakim/wasm_provider.ts b/front/src/hakim/wasm_provider.ts
@@ -0,0 +1,6 @@
+declare let window: Window & {
+    hakimQuery: (x: any) => any;
+};
+export const hakimQueryImpl = async (json_obj: any): Promise<any> => {
+    return window.hakimQuery(json_obj);;
+};
diff --git a/front/src/index.html b/front/src/index.html
@@ -7,7 +7,12 @@
 
 <body>
     <div id="root"></div>
-    <!-- enable in wasm mode: <script src="/static/hakim-json.js"></script> -->
+    <script src="/static/hakim-json.js"></script>
 </body>
 
-</html>
+<script src="z3-built.js"></script>
+<script>
+    globalThis.global = { initZ3: globalThis.initZ3 };
+</script>
+
+</html>
diff --git a/front/webpack.config.js b/front/webpack.config.js
@@ -62,14 +62,14 @@ const config = {
       React: "react",
     }),
     // enable in wasm mode:
-    // new CopyPlugin({
-    //   patterns: [
-    //     {
-    //       from: "static",
-    //       to: "static",
-    //     },
-    //   ],
-    // }),
+    new CopyPlugin({
+      patterns: [
+        {
+          from: "static",
+          to: "static",
+        },
+      ],
+    }),
   ],
   experiments: {
     topLevelAwait: true,

diff --git a/hakim-engine/src/interactive.rs b/hakim-engine/src/interactive.rs
@@ -167,6 +167,16 @@ impl Session {
         Ok(())
     }
 
+    pub fn z3_solved(&mut self) -> Option<()> {
+        let mut snapshot = self.last_snapshot().clone();
+        snapshot.pop_frame();
+        self.add_history_record(HistoryRecord {
+            tactic: "z3".to_string(),
+            snapshot: snapshot.clone(),
+        });
+        Some(())
+    }
+
     pub fn run_suggestion(
         &mut self,
         sugg: Suggestion,
@@ -270,6 +280,9 @@ impl Session {
         }
         self.last_snapshot().last_frame()?.try_auto()
     }
+    pub fn z3_get_state(&self) -> Option<String> {
+        Some(z3_auto(self.last_snapshot().last_frame()?.clone()))
+    }
 
     pub fn action_of_tactic(&self, tactic: &str) -> Option<GraphicalAction> {
         action_of_tactic(self, tactic)
@@ -469,7 +482,7 @@ impl Frame {
             "auto_set" => auto_set(frame),
             "auto_list" => auto_list(frame),
             "assumption" => assumption(frame),
-            "z3" => z3_auto(frame),
+            "z3" => Err(tactic::Error::Z3State(z3_auto(frame))),
             _ => Err(tactic::Error::UnknownTactic(name.to_string())),
         }
     }
@@ -484,7 +497,7 @@ impl Frame {
     }
 
     pub fn try_auto(&self) -> Option<String> {
-        const AUTO_TAC: &[&str] = &["assumption", "auto_set", "auto_list", "lia", "lra", "z3"];
+        const AUTO_TAC: &[&str] = &["assumption", "auto_set", "auto_list", "lia", "lra"];
         for tac in AUTO_TAC {
             if self.run_tactic(tac).ok().filter(|x| x.is_empty()).is_some() {
                 return Some(tac.to_string());

diff --git a/hakim-engine/src/interactive/tactic.rs b/hakim-engine/src/interactive/tactic.rs
@@ -58,6 +58,7 @@ pub enum Error {
     ContextDependOnHyp(String, TermRef),
     TermIsNotType(TermRef),
     MismatchedParen,
+    Z3State(String),
 }
 
 impl Error {