microsoft · pelikhan · Apr 24, 2025 · Apr 24, 2025 · Apr 24, 2025 · Apr 24, 2025
diff --git a/.vscode/settings.json b/.vscode/settings.json
@@ -80,6 +80,7 @@
         "Fmepg",
         "frontmatter",
         "fscache",
+        "fuzzsearch",
         "gdir",
         "genai",
         "Genaiscript",
@@ -192,6 +193,7 @@
         "resd",
         "RIPGREP",
         "RULEID",
+        "runpromptcontext",
         "sarif",
         "SARIFF",
         "scripters",
@@ -231,19 +233,23 @@
         "typecheck",
         "unfence",
         "unmarkdown",
+        "unsat",
         "unthink",
         "unwrappers",
         "urllib",
         "urlparse",
+        "vectorsearch",
         "vectra",
         "venv",
         "vllm",
         "vshost",
         "vsix",
         "waltoss",
         "wasms",
+        "websearch",
         "WEBVTT",
         "whisperasr",
+        "wksrx",
         "wsclient",
         "xpai",
         "Yohan"

diff --git a/docs/src/content/docs/reference/scripts/system.mdx b/docs/src/content/docs/reference/scripts/system.mdx
@@ -4837,72 +4837,6 @@ system({
 })
 const dbg = host.logger("system:z3")
 
-let _z3: Promise<ReturnType<(typeof import("z3-solver"))["init"]>> = undefined
-
-async function importZ3(): Promise<
-    ReturnType<(typeof import("z3-solver"))["init"]>
-> {
-    try {
-        dbg(`importing z3-solver`)
-        const z3 = await import("z3-solver")
-        dbg(`initializing`)
-        const res = await z3.init()
-        dbg(`initialized`)
-        return res
-    } catch (e) {
-        dbg(e?.message)
-        return undefined
-    }
-}
-
-async function Z3Run(context: ToolCallContext, input: string) {
-    // init z3
-    const z3p = await (_z3 || (_z3 = importZ3()))
-    if (!z3p) {
-        context.log(
-            "Z3 not available. Make sure to install the https://www.npmjs.com/package/z3-solver package."
-        )
-        return undefined
-    }
-
-    const { Z3 } = z3p
-    // done on every snippet
-    const cfg = Z3.mk_config()
-    const ctx = Z3.mk_context(cfg)
-    Z3.del_config(cfg)
-
-    const timeStart = new Date().getTime()
-    const timeout = 10000
-
-    Z3.global_param_set("timeout", String(timeout))
-
-    let output = ""
-    let error = ""
-
-    try {
-        output = (await Z3.eval_smtlib2_string(ctx, input)) ?? ""
-    } catch (e) {
-        // error with running z3
-        error = e.message ?? "Error message is empty"
-    } finally {
-        Z3.del_context(ctx)
-    }
-
-    if (/unknown/.test(output)) {
-        const timeEnd = new Date().getTime()
-        if (timeEnd - timeStart >= timeout) {
-            output = output + "\nZ3 timeout\n"
-        }
-    }
-
-    // we are guaranteed to have non-undefined output and error
-    if (!error) return output
-    else
-        return `error: ${error}
-
-${output || ""}`
-}
-
 export default async function (_: ChatGenerationContext) {
     const { defTool } = _
 
@@ -4920,9 +4854,10 @@ export default async function (_: ChatGenerationContext) {
             required: ["smtlib2"],
         },
         async (args) => {
-            const { context, smtlib2 } = args
+            const { smtlib2 } = args
             dbg(`query: ${smtlib2}`)
-            const result = await Z3Run(context, smtlib2)
+            const z3 = await host.z3()
+            const result = await z3.run(smtlib2)
             dbg(`result: ${result}`)
             return result
         }

diff --git a/docs/src/content/docs/reference/scripts/z3.mdx b/docs/src/content/docs/reference/scripts/z3.mdx
@@ -1,27 +1,45 @@
 ---
 title: Z3
 description: Z3 is a high-performance theorem prover developed at Microsoft
-  Research. It is a built-in tool of GenAIScript.
+    Research. It is a built-in tool of GenAIScript.
 sidebar:
-  order: 200
+    order: 200
 hero:
-  image:
-    alt: "A small, 8-bit style computer chip labeled as Z3 is centrally positioned,
-      with fine lines linking it to three simple shapes: a circle containing a
-      checkmark to suggest problem solving, a square featuring an inequality
-      sign to indicate logical constraints, and a triangle with tiny gears
-      inside to represent verifying programs. The image uses only blue, gray,
-      black, white, and green, appears flat and geometric with a professional,
-      minimalistic look, and has no background or human figures."
-    file: ./z3.png
-
+    image:
+        alt:
+            "A small, 8-bit style computer chip labeled as Z3 is centrally positioned,
+            with fine lines linking it to three simple shapes: a circle containing a
+            checkmark to suggest problem solving, a square featuring an inequality
+            sign to indicate logical constraints, and a triangle with tiny gears
+            inside to represent verifying programs. The image uses only blue, gray,
+            black, white, and green, appears flat and geometric with a professional,
+            minimalistic look, and has no background or human figures."
+        file: ./z3.png
 ---
 
 [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
 and can be used for various applications, including program verification, constraint solving, and symbolic execution.
 
 GenAIScript uses the WebAssembly-based [z3-solver](https://www.npmjs.com/package/z3-solver) npm package to run Z3.
 
+## Z3 instance
+
+The `host.z3()` method creates a new Z3 instance. The instance can be used to run Z3 commands and get the results.
+The `z3` instance is a wrapper around the [z3-solver](https://www.npmjs.com/package/z3-solver) npm package.
+The `z3` instance has the `run` method that runs the given SMTLIB2 formula and returns the result.
+
+```js
+const z3 = await host.z3()
+const res = await z3.run(`
+(declare-const a Int)
+(declare-fun f (Int Bool) Int)
+(assert (< a 10))
+(assert (< (f a true) 100))
+(check-sat)
+`)
+console.log(res) // unsat
+```
+
 ## Z3 tool
 
 The `z3` tool (in [system.z3](/genaiscript/reference/scripts/system#systemz3)) script wraps Z3 as a LLM tool that can be used in GenAIScript.

diff --git a/packages/cli/genaisrc/system.agent_z3.genai.mts b/packages/cli/genaisrc/system.agent_z3.genai.mts
@@ -7,7 +7,7 @@ export default function (ctx: ChatGenerationContext) {
 
     defAgent(
         "z3",
-        "can formalize and solve problems using the Z3 constraint solver. If you need to run Z3, use this tool.",
+        "can formalize and solve problems using the Z3 constraint solver. If you need to run Z3 or solve constraint systems, use this tool.",
         async (_) => {
             _.$`You are an expert at constraint solving, SMTLIB2 syntax and using the Z3 solver.
         You are an incredibly smart mathematician that can formalize any problem into a set of constraints

diff --git a/packages/cli/genaisrc/system.z3.genai.mts b/packages/cli/genaisrc/system.z3.genai.mts
@@ -4,72 +4,6 @@ system({
 })
 const dbg = host.logger("system:z3")
 
-let _z3: Promise<ReturnType<(typeof import("z3-solver"))["init"]>> = undefined
-
-async function importZ3(): Promise<
-    ReturnType<(typeof import("z3-solver"))["init"]>
-> {
-    try {
-        dbg(`importing z3-solver`)
-        const z3 = await import("z3-solver")
-        dbg(`initializing`)
-        const res = await z3.init()
-        dbg(`initialized`)
-        return res
-    } catch (e) {
-        dbg(e?.message)
-        return undefined
-    }
-}
-
-async function Z3Run(context: ToolCallContext, input: string) {
-    // init z3
-    const z3p = await (_z3 || (_z3 = importZ3()))
-    if (!z3p) {
-        context.log(
-            "Z3 not available. Make sure to install the https://www.npmjs.com/package/z3-solver package."
-        )
-        return undefined
-    }
-
-    const { Z3 } = z3p
-    // done on every snippet
-    const cfg = Z3.mk_config()
-    const ctx = Z3.mk_context(cfg)
-    Z3.del_config(cfg)
-
-    const timeStart = new Date().getTime()
-    const timeout = 10000
-
-    Z3.global_param_set("timeout", String(timeout))
-
-    let output = ""
-    let error = ""
-
-    try {
-        output = (await Z3.eval_smtlib2_string(ctx, input)) ?? ""
-    } catch (e) {
-        // error with running z3
-        error = e.message ?? "Error message is empty"
-    } finally {
-        Z3.del_context(ctx)
-    }
-
-    if (/unknown/.test(output)) {
-        const timeEnd = new Date().getTime()
-        if (timeEnd - timeStart >= timeout) {
-            output = output + "\nZ3 timeout\n"
-        }
-    }
-
-    // we are guaranteed to have non-undefined output and error
-    if (!error) return output
-    else
-        return `error: ${error}
-
-${output || ""}`
-}
-
 export default async function (_: ChatGenerationContext) {
     const { defTool } = _
 
@@ -87,9 +21,10 @@ export default async function (_: ChatGenerationContext) {
             required: ["smtlib2"],
         },
         async (args) => {
-            const { context, smtlib2 } = args
+            const { smtlib2 } = args
             dbg(`query: ${smtlib2}`)
-            const result = await Z3Run(context, smtlib2)
+            const z3 = await host.z3()
+            const result = await z3.run(smtlib2)
             dbg(`result: ${result}`)
             return result
         }

diff --git a/packages/core/src/promptcontext.ts b/packages/core/src/promptcontext.ts
@@ -36,6 +36,7 @@ import {
     astGrepParse,
 } from "./astgrep"
 import { createCache } from "./cache"
+import { loadZ3Client } from "./z3"
 
 const dbg = debug("genaiscript:promptcontext")
 
@@ -47,7 +48,7 @@ const dbg = debug("genaiscript:promptcontext")
  * @param trace Markdown trace for logging and debugging.
  * @param options Generation options such as cancellation tokens, embeddings models, and content safety.
  * @param model The model identifier used for context creation.
- * @returns A context object providing methods for file operations, web retrieval, searches, execution, container operations, caching, and other utilities. Includes workspace file system operations (read/write files, grep, find files), retrieval methods (web search, fuzzy search, vector search), and host operations (command execution, browsing, container management, etc.).
+ * @returns A context object providing methods for file operations, web retrieval, searches, execution, container operations, caching, and other utilities. Includes workspace file system operations (read/write files, grep, find files), retrieval methods (web search, fuzzy search, vector search, index creation), and host operations (command execution, browsing, container management, resource publishing, server management, etc.).
  */
 export async function createPromptContext(
     prj: Project,
@@ -285,6 +286,7 @@ export async function createPromptContext(
             const res = createCache<any, any>(name, { type: "memory" })
             return res
         },
+        z3: () => loadZ3Client({ trace, cancellationToken }),
         exec: async (
             command: string,
             args?: string[] | ShellOptions,

diff --git a/packages/core/src/types/prompt_template.d.ts b/packages/core/src/types/prompt_template.d.ts
@@ -2804,6 +2804,26 @@ interface YAML {
     parse(text: string | WorkspaceFile): any
 }
 
+interface Z3Solver {
+    /**
+     * Runs Z3 on a given SMT string
+     * @param smt
+     */
+    run(smt: string): Promise<string>
+
+    /**
+     * Native underlying Z3 api
+     */
+    api(): any
+}
+
+interface Z3SolverHost {
+    /**
+     * Loads the Z3 solver from the host
+     */
+    z3(): Promise<Z3Solver>
+}
+
 interface PromptyFrontmatter {
     name?: string
     description?: string
@@ -5806,6 +5826,7 @@ interface PromptHost
         UserInterfaceHost,
         LanguageModelHost,
         SgHost,
+        Z3SolverHost,
         ContentSafetyHost {
     /**
      * A fetch wrapper with proxy, retry and timeout handling.