solve_z3

Instructions

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

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")

• usolver_mcp/models/z3_models.py:35-41 (schema)

  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 = ""

• usolver_mcp/solvers/z3_solver.py:238-269 (helper)

  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}")

• usolver_mcp/models/z3_models.py:12-49 (schema)

  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