diff --git a/.vscode/settings.json b/.vscode/settings.json index 3407d60c39..ae4343c4dd 100644 --- 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,10 +233,12 @@ "typecheck", "unfence", "unmarkdown", + "unsat", "unthink", "unwrappers", "urllib", "urlparse", + "vectorsearch", "vectra", "venv", "vllm", @@ -242,8 +246,10 @@ "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 index e2da96393e..1f1346a298 100644 --- 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> = 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 index b122a92eec..36a9a4bd6f 100644 --- a/docs/src/content/docs/reference/scripts/z3.mdx +++ b/docs/src/content/docs/reference/scripts/z3.mdx @@ -1,20 +1,20 @@ --- 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 @@ -22,6 +22,24 @@ and can be used for various applications, including program verification, constr 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 index 3d6ba27458..92f10ecd7a 100644 --- 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 index d210e3980c..9a421176c9 100644 --- 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> = 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 index 11b52b7064..2829f201d6 100644 --- 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(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 index 1db586b364..d671393188 100644 --- 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 + + /** + * Native underlying Z3 api + */ + api(): any +} + +interface Z3SolverHost { + /** + * Loads the Z3 solver from the host + */ + z3(): Promise +} + 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. diff --git a/packages/core/src/z3.ts b/packages/core/src/z3.ts new file mode 100644 index 0000000000..b9a5fbf2dc --- /dev/null +++ b/packages/core/src/z3.ts @@ -0,0 +1,91 @@ +import { CancellationOptions, checkCancelled } from "./cancellation" +import { genaiscriptDebug } from "./debug" +import { TraceOptions } from "./trace" +import { logWarn } from "./util" + +const dbg = genaiscriptDebug("z3") + +let _z3: Promise> = 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 + } +} + +/** + * Loads and initializes the Z3 SMT solver client. + * + * Optionally accepts trace and cancellation options. + * Returns a Z3Solver object if the Z3 solver module is properly installed and initialized, otherwise returns undefined. + * + * @param options Optional trace and cancellation options. + * - trace: Enables debug tracing for the Z3 solver. + * - cancellationToken: Token to allow cancellation of the initialization or run operation. + * + * @returns An object with: + * - run(input): Runs an SMT-LIB2 string input on the Z3 solver and returns its output. Throws on timeout or input error. + * - api(): Returns the raw Z3 API. + * + * Logs a warning if the Z3 solver module is not available. Ensures cancellation checks are respected at initialization and execution. + */ +export async function loadZ3Client( + options?: TraceOptions & CancellationOptions +): Promise { + const { trace, cancellationToken } = options || {} + const z3p = await (_z3 || (_z3 = importZ3())) + checkCancelled(cancellationToken) + if (!z3p) { + logWarn( + "Z3 not available. Make sure to install the https://www.npmjs.com/package/z3-solver package." + ) + return undefined + } + const { Z3 } = z3p + dbg(`loaded z3-solver`) + return Object.freeze({ + run: Z3Run, + api: () => Z3, + }) satisfies Z3Solver + + async function Z3Run(input: string) { + if (!input) throw new Error("No input provided") + + checkCancelled(cancellationToken) + dbg(`run: %s`, input) + 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)) ?? "" + } finally { + Z3.del_context(ctx) + } + dbg(`output: %s`, output) + if (/unknown/.test(output)) { + const timeEnd = new Date().getTime() + if (timeEnd - timeStart >= timeout) + throw new Error("Z3 timeout, " + output) + } + return output + } +}