USolver

Instructions

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

Implementation Reference

• usolver_mcp/server/main.py:95-175 (handler)

  The main handler function for the 'solve_z3_simple' MCP tool. Converts simple input lists into Z3Problem model and calls solve_problem from z3_solver.

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

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

  Pydantic models defining the structure for Z3 problems, variables, constraints, and solutions, used internally by the tool handler.

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

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

  Core solver function that takes Z3Problem and uses Z3 library to find a satisfying assignment or determine unsatisfiability.

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