solve_z3
Solve constraint satisfaction and optimization problems using the Z3 solver. Input structured problem definitions with variables and constraints to output solution 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
TableJSON Schema
| Name | Required | Description | Default |
|---|---|---|---|
| problem | Yes |
Implementation Reference
- usolver_mcp/server/main.py:60-93 (handler)MCP tool handler for solve_z3, which delegates to solve_problem from z3_solver and formats the result as 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")]
- Pydantic model 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 = ""
- usolver_mcp/server/main.py:60-60 (registration)Registration of the solve_z3 tool using FastMCP decorator.@app.tool("solve_z3")
- Core solver function solve_problem that implements the Z3 solving logic: creates variables, parses constraints, solves with z3.Solver, and extracts solution.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}")