solve_z3
Solve constraint satisfaction and optimization problems using the Z3 solver. Processes structured problem definitions with variables and constraints to determine satisfiability and find solutions.
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
TableJSON Schema
| Name | Required | Description | Default |
|---|---|---|---|
| problem | Yes |
Implementation Reference
- usolver_mcp/server/main.py:60-93 (handler)The primary handler function for the 'solve_z3' MCP tool. It receives a Z3Problem input, calls the underlying solve_problem helper, and returns the result formatted as JSON in TextContent.@app.tool("solve_z3") async def solve_z3(problem: Z3Problem) -> list[TextContent]: """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 """ result = solve_problem(problem) match result: case Success(solution): return [ TextContent( type="text", text=json.dumps( { "values": solution.values, "is_satisfiable": solution.is_satisfiable, "status": solution.status, } ), ) ] case Failure(error): return [TextContent(type="text", text=f"Error solving problem: {error}")] case _: return [TextContent(type="text", text="Unexpected error in solve_z3")]
- usolver_mcp/server/main.py:60-60 (registration)FastMCP tool registration decorator binding the solve_z3 handler to the tool name.@app.tool("solve_z3")
- Pydantic BaseModel defining the input schema (Z3Problem) for the solve_z3 tool, including variables and constraints.class Z3Problem(BaseModel): """Complete Z3 constraint satisfaction problem.""" variables: list[Z3Variable] constraints: list[Z3Constraint] description: str = ""
- Core solver logic that creates Z3 variables and constraints from the problem model, solves using z3.Solver.check(), and extracts the solution values.def solve_problem(problem: Z3Problem) -> Result[Z3Solution, str]: """Orchestrates the complete process of solving a Z3 problem. Args: problem: The problem definition containing variables and constraints. Returns: Result: A Result containing either a Solution object or a failure with error details. """ try: vars_result = create_variables(problem.variables) if isinstance(vars_result, Failure): return vars_result variables = vars_result.unwrap() constraints_result = create_constraints(problem.constraints, variables) if isinstance(constraints_result, Failure): return constraints_result z3_constraints = constraints_result.unwrap() solve_result = solve(variables, z3_constraints) if isinstance(solve_result, Failure): return solve_result result_tuple = solve_result.unwrap() return extract_solution(result_tuple[0], result_tuple[1], variables) except Exception as e: return Failure(f"Error solving problem: {e!s}")
- Supporting Pydantic models and enum for Z3 variables, constraints, problem, and solution used by the solve_z3 tool.class Z3VariableType(str, Enum): """Variable types in Z3.""" INTEGER = "integer" REAL = "real" BOOLEAN = "boolean" STRING = "string" class Z3Variable(BaseModel): """Typed variable in a Z3 problem.""" name: str type: Z3VariableType class Z3Constraint(BaseModel): """Constraint in a Z3 problem.""" expression: str # expression as string (run through eval) description: str = "" class Z3Problem(BaseModel): """Complete Z3 constraint satisfaction problem.""" variables: list[Z3Variable] constraints: list[Z3Constraint] description: str = "" class Z3Solution(BaseModel): """Solution to a Z3 problem.""" values: dict[str, Z3Value] is_satisfiable: bool status: str