solve_z3_simple
Solve Z3 constraint problems by specifying variables and constraints as simple lists, bypassing the need for complex model structures. Ideal for straightforward problem-solving with minimal setup.
Instructions
Simplified interface for Z3 constraint problems.
A more direct way to solve Z3 problems without full model structure.
Just provide variables and constraints as simple lists.
Args:
variables: List of dicts with 'name' and 'type' for each variable
constraints: List of constraint expressions as strings
description: Optional problem description
Returns:
Solution results as TextContent list
Input Schema
TableJSON Schema
| Name | Required | Description | Default |
|---|---|---|---|
| constraints | Yes | ||
| description | No | ||
| variables | Yes |
Implementation Reference
- usolver_mcp/server/main.py:95-175 (handler)The handler function decorated with @app.tool('solve_z3_simple'), implementing the core logic: input validation, conversion to Z3Problem model, calling solve_problem, and formatting output as TextContent.@app.tool("solve_z3_simple") async def solve_z3_simple( variables: list[dict[str, str]], constraints: list[str], description: str = "", ) -> list[TextContent]: """Simplified interface for Z3 constraint problems. A more direct way to solve Z3 problems without full model structure. Just provide variables and constraints as simple lists. Args: variables: List of dicts with 'name' and 'type' for each variable constraints: List of constraint expressions as strings description: Optional problem description Returns: Solution results as TextContent list """ try: # Convert to Problem model problem_variables = [] for var in variables: if "name" not in var or "type" not in var: return [ TextContent( type="text", text="Each variable must have 'name' and 'type' fields", ) ] try: var_type = Z3VariableType(var["type"]) except ValueError: return [ TextContent( type="text", text=( f"Invalid variable type: {var['type']}. " f"Must be one of: {', '.join([t.value for t in Z3VariableType])}" ), ) ] problem_variables.append(Z3Variable(name=var["name"], type=var_type)) problem_constraints = [Z3Constraint(expression=expr) for expr in constraints] problem = Z3Problem( variables=problem_variables, constraints=problem_constraints, description=description, ) # Solve the problem 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_simple") ] except Exception as e: return [TextContent(type="text", text=f"Error in solve_z3_simple: {e!s}")]
- Core solver function solve_problem that orchestrates variable creation, constraint parsing, Z3 solving, and solution extraction. Called by the tool handler.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}")
- usolver_mcp/models/z3_models.py:7-49 (schema)Pydantic models and types defining the structure for Z3 problems, variables, constraints, and solutions used internally by the tool.Z3Value = bool | int | float | str Z3Ref = z3.BoolRef | z3.ArithRef | z3.ExprRef Z3Sort = Union[z3.BoolSort, z3.IntSort, z3.RealSort, z3.StringSort] # noqa: UP007 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
- usolver_mcp/server/main.py:95-95 (registration)FastMCP decorator registering the solve_z3_simple function as an MCP tool.@app.tool("solve_z3_simple")