|
1 | 1 | --- |
2 | 2 | title: Z3 |
3 | | -description: Z3 is a high-performance theorem prover developed at Microsoft |
4 | | - Research. It is a built-in tool of GenAIScript. |
| 3 | +description: |
| 4 | + Z3 is a high-performance theorem prover developed at Microsoft |
| 5 | + Research. It is a built-in tool of GenAIScript. |
5 | 6 | sidebar: |
6 | | - order: 200 |
| 7 | + order: 200 |
7 | 8 | hero: |
8 | | - image: |
9 | | - alt: |
10 | | - "A small, 8-bit style computer chip labeled as Z3 is centrally positioned, |
11 | | - with fine lines linking it to three simple shapes: a circle containing a |
12 | | - checkmark to suggest problem solving, a square featuring an inequality |
13 | | - sign to indicate logical constraints, and a triangle with tiny gears |
14 | | - inside to represent verifying programs. The image uses only blue, gray, |
15 | | - black, white, and green, appears flat and geometric with a professional, |
16 | | - minimalistic look, and has no background or human figures." |
17 | | - file: ./plugin-z3.png |
| 9 | + image: |
| 10 | + alt: |
| 11 | + "A small, 8-bit style computer chip labeled as Z3 is centrally positioned, |
| 12 | + with fine lines linking it to three simple shapes: a circle containing a |
| 13 | + checkmark to suggest problem solving, a square featuring an inequality |
| 14 | + sign to indicate logical constraints, and a triangle with tiny gears |
| 15 | + inside to represent verifying programs. The image uses only blue, gray, |
| 16 | + black, white, and green, appears flat and geometric with a professional, |
| 17 | + minimalistic look, and has no background or human figures." |
| 18 | + file: ./plugin-z3.png |
18 | 19 | --- |
19 | 20 |
|
20 | 21 | [Z3](https://microsoft.github.io/z3guide/) is a high-performance theorem prover developed at Microsoft Research. It is a built-in tool of GenAIScript. Z3 is used to solve logical formulas |
21 | 22 | and can be used for various applications, including program verification, constraint solving, and symbolic execution. |
22 | 23 |
|
23 | 24 | GenAIScript uses the WebAssembly-based [z3-solver](https://www.npmjs.com/package/z3-solver) npm package to run Z3. |
24 | 25 |
|
| 26 | +## Installation |
| 27 | + |
| 28 | +<PackageManagers pkg="@genaiscript/plugin-z3" dev /> |
| 29 | + |
| 30 | +If you are using the plugin in a Node.JS environment, without a `.genai...` entry file, you will need |
| 31 | +to initialize the [runtime](/genaiscript/reference/runtime) before using the plugin: |
| 32 | + |
| 33 | +```ts |
| 34 | +import { initialize } from "@genaiscript/runtime"; |
| 35 | + |
| 36 | +await initialize(); |
| 37 | +``` |
| 38 | + |
25 | 39 | ## Z3 instance |
26 | 40 |
|
27 | | -The `host.z3()` method creates a new Z3 instance. The instance can be used to run Z3 commands and get the results. |
| 41 | +The `z3()` method creates a new Z3 instance. The instance can be used to run Z3 commands and get the results. |
28 | 42 | The `z3` instance is a wrapper around the [z3-solver](https://www.npmjs.com/package/z3-solver) npm package. |
29 | 43 | The `z3` instance has the `run` method that runs the given SMTLIB2 formula and returns the result. |
30 | 44 |
|
31 | 45 | ```js |
32 | | -import { z3 } from "@genaiscript/plugin-z3" |
| 46 | +import { z3 } from "@genaiscript/plugin-z3"; |
33 | 47 |
|
34 | | -const z3 = await z3() |
| 48 | +const z3 = await z3(); |
35 | 49 | const res = await z3.run(` |
36 | 50 | (declare-const a Int) |
37 | 51 | (declare-fun f (Int Bool) Int) |
38 | 52 | (assert (< a 10)) |
39 | 53 | (assert (< (f a true) 100)) |
40 | 54 | (check-sat) |
41 | | -`) |
42 | | -console.log(res) // unsat |
| 55 | +`); |
| 56 | +console.log(res); // unsat |
43 | 57 | ``` |
44 | 58 |
|
45 | 59 | ## Z3 tool |
@@ -70,16 +84,16 @@ tool with a LLM that can (try to) formalize arbitrary problems to SMTLIB2. |
70 | 84 |
|
71 | 85 | ```js |
72 | 86 | script({ |
73 | | - tools: ["agent_z3"], |
74 | | -}) |
| 87 | + tools: ["agent_z3"], |
| 88 | +}); |
75 | 89 |
|
76 | 90 | $`Solve the following problems using Z3: |
77 | 91 |
|
78 | 92 | Imagine we have a number called 'a' that is smaller than 10. |
79 | 93 | We also have a special machine called 'f' that takes a number and a 'true'/'false' answer, |
80 | 94 | and it gives back another number. |
81 | 95 | When we put the number 'a' and the answer “true” into this machine, |
82 | | -the number it gives us is smaller than 100.` |
| 96 | +the number it gives us is smaller than 100.`; |
83 | 97 | ``` |
84 | 98 |
|
85 | 99 | :::note |
|
0 commit comments