solve_z3
Solve Z3 constraint satisfaction and optimization problems by inputting variables and constraints. Returns results including variable values and satisfiability status.
Instructions
Solve a Z3 constraint satisfaction problem.
Takes a structured problem definition and returns a solution using Z3 solver.
Handles both satisfiability and optimization problems.
Args:
problem: Problem definition containing variables and constraints
Returns:
Solution results as TextContent list, including values and satisfiability status
Input Schema
| Name | Required | Description | Default |
|---|---|---|---|
| problem | Yes |
Input Schema (JSON Schema)
{
"$defs": {
"Z3Constraint": {
"description": "Constraint in a Z3 problem.",
"properties": {
"description": {
"default": "",
"title": "Description",
"type": "string"
},
"expression": {
"title": "Expression",
"type": "string"
}
},
"required": [
"expression"
],
"title": "Z3Constraint",
"type": "object"
},
"Z3Problem": {
"description": "Complete Z3 constraint satisfaction problem.",
"properties": {
"constraints": {
"items": {
"$ref": "#/$defs/Z3Constraint"
},
"title": "Constraints",
"type": "array"
},
"description": {
"default": "",
"title": "Description",
"type": "string"
},
"variables": {
"items": {
"$ref": "#/$defs/Z3Variable"
},
"title": "Variables",
"type": "array"
}
},
"required": [
"variables",
"constraints"
],
"title": "Z3Problem",
"type": "object"
},
"Z3Variable": {
"description": "Typed variable in a Z3 problem.",
"properties": {
"name": {
"title": "Name",
"type": "string"
},
"type": {
"$ref": "#/$defs/Z3VariableType"
}
},
"required": [
"name",
"type"
],
"title": "Z3Variable",
"type": "object"
},
"Z3VariableType": {
"description": "Variable types in Z3.",
"enum": [
"integer",
"real",
"boolean",
"string"
],
"title": "Z3VariableType",
"type": "string"
}
},
"properties": {
"problem": {
"$ref": "#/$defs/Z3Problem"
}
},
"required": [
"problem"
],
"title": "solve_z3Arguments",
"type": "object"
}