generate z3-status with smt-lib2 language

babaeee · Feb 22, 2024 · e505efa · e505efa
1 parent 8a631a2
commit e505efa
Show file tree

Hide file tree

Showing 12 changed files with 431 additions and 700 deletions.
diff --git a/.vscode/settings.json b/.vscode/settings.json
@@ -1,4 +1,8 @@
 {
     "rust-analyzer.checkOnSave.command": "clippy",
-    "editor.formatOnSave": true
+    "editor.formatOnSave": true,
+    "rust-analyzer.linkedProjects": [
+        "./hakim-engine/Cargo.toml"
+    ],
+    "rust-analyzer.checkOnSave": false
 }
diff --git a/Cargo.lock b/Cargo.lock
diff --git a/front/package.json b/front/package.json
@@ -81,7 +81,7 @@
     "webpack-manifest-plugin": "4.0.2",
     "yaml-include-loader": "^1.0.0",
     "yaml-loader": "^0.6.0",
-    "z3-solver": "^4.12.4"
+    "z3-solver": "^4.12.5"
   },
   "scripts": {
     "build": "webpack build --mode production",

diff --git a/front/src/components/proof/Toolbar.tsx b/front/src/components/proof/Toolbar.tsx
@@ -52,12 +52,8 @@ const AutoProofButton = () => {
             const r = await tryAuto();
             if (mode === 'boost') {
                 if (r.available) {
-                    if (r.tactic[0] === "z3_solved") {
-                        z3Solved();
-                    } else {
-                        for (const tac of r.tactic) {
-                            await sendTactic(tac);
-                        }
+                    for (const tac of r.tactic) {
+                        await sendTactic(tac);
                     }
                 }
             } else {
@@ -79,12 +75,8 @@ const AutoProofButton = () => {
                     }
                     if (s.available) {
                         console.log(s.tactic[0]);
-                        if (s.tactic[0] === "z3_solved") {
-                            z3Solved();
-                        } else {
-                            for (const tac of s.tactic) {
-                                await sendTactic(tac);
-                            }
+                        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
@@ -2,6 +2,7 @@ import { normalPrompt } from "../dialog";
 import { fromRust } from "../i18n";
 import { loadLibText } from "./lib_text";
 import { hakimQueryImpl } from "./wasm_provider";
+import { init } from "z3-solver";
 
 declare let window: Window & {
   ask_question: (q: string) => Promise<string>;
@@ -47,6 +48,9 @@ await window.hakimQueryLoad;
 
 let queryLock = false;
 
+const { Context, em } = await init();
+const Z3 = Context('main');
+
 const instance: Instance = new Proxy(
   {},
   {
@@ -66,16 +70,16 @@ const instance: Instance = new Proxy(
             });
           }
           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";
-            // }
+            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;
@@ -378,10 +382,11 @@ export const tryAuto = async (): Promise<TryAutoResult> => {
 
   if (tactic) {
     if (tactic === 'z3_solved') {
+      console.log("z3 solved");
       return {
         available: true,
         type: "normal",
-        tactic: ["z3_solved"],
+        tactic: ["z3"],
       };
     }
     if (tactic !== 'z3_cant_solve') {

diff --git a/front/src/index.html b/front/src/index.html
@@ -11,9 +11,9 @@
     <script src="/static/hakim-json.js"></script>
 </body>
 
-<!-- script src="/z3-built.js"></script >
+<script src="z3-built.js"></script>
 <script>
     globalThis.global = { initZ3: globalThis.initZ3 };
-</script-->
+</script>
 
 </html>
diff --git a/front/yarn.lock b/front/yarn.lock
@@ -10589,9 +10589,9 @@ yocto-queue@^0.1.0:
   resolved "https://registry.npmjs.org/yocto-queue/-/yocto-queue-0.1.0.tgz"
   integrity sha512-rVksvsnNCdJ/ohGc6xgPwyN8eheCxsiLM8mxuE/t/mOVqJewPuO1miLpTHQiRgTKCLexL4MeAFVagts7HmNZ2Q==
 
-z3-solver@^4.12.4:
-  version "4.12.4"
-  resolved "https://registry.yarnpkg.com/z3-solver/-/z3-solver-4.12.4.tgz#3f7f7eca0d0e2afb5fda409e4ed3639507346c71"
-  integrity sha512-B9ymul40bvtGSW0OQYfcYan1EhGm0JV/HgbO24JikIhuEOUv2+mdcOVd4V3q89UOx2mA0MOv+6d5msVF+/yJ6g==
+z3-solver@^4.12.5:
+  version "4.12.5"
+  resolved "https://registry.yarnpkg.com/z3-solver/-/z3-solver-4.12.5.tgz#ec8d4b17aa07b8792b9ab8b8f61dc8b0ea30d7b0"
+  integrity sha512-uh6zoe+ErxG2qLjWyOcZE41eb6CHUZ3IT7VYTh1SDswPaoe7I1mvC7ujA36TROdBdPm59UUFToDmRbfiyjdA1Q==
   dependencies:
     async-mutex "^0.3.2"
diff --git a/hakim-engine/Cargo.toml b/hakim-engine/Cargo.toml
@@ -14,15 +14,16 @@ typed-arena = "2.0.1"
 lazy_static = "1.2.0"
 minilp = { git = "https://github.com/HKalbasi/minilp" }
 pretty = "0.11.3"
-z3 = { git = "https://github.com/arshiamoeini/my_z3.git", optional = true, features = [
-    "static-link-z3",
-] }
-z3-sys = { git = "https://github.com/arshiamoeini/my_z3.git", optional = true, features = [
-    "static-link-z3",
-] }
+smt2 = { git = "https://github.com/achreto/rust-smtlib2", features = ["z3"] }
+#z3 = { git = "https://github.com/arshiamoeini/my_z3.git", features = [
+#    "static-link-z3",
+#] }
+#z3-sys = { git = "https://github.com/arshiamoeini/my_z3.git", features = [
+#    "static-link-z3",
+#] }
 
 [features]
-z3 = ["dep:z3", "dep:z3-sys"]
+z3 = []
 
 [dev-dependencies]
 rayon = "1.6.0"