Repository: sympy/sympy
File: sympy/printing/smtlib.py (Python)

Code before:
            return name
        else:
            f = x.evalf(self._precision) if self._precision else x.evalf()
            return self._print_Float(f)

    def _print_UndefinedFunction(self, x):
        assert self._is_legal_name(x.name)
        return x.name

    def _print_Exp1(self, x):
        return (
            self._print_Function(exp(1, evaluate=False))
            if exp in self._known_functions else
            self._print_NumberSymbol(x)
        )

    def emptyPrinter(self, expr):
        raise NotImplementedError(f'Cannot convert `{repr(expr)}` of type `{type(expr)}` to SMT.')


from sympy.core.function import Function, FunctionClass
from sympy import Symbol
import sympy
from typing import Callable, get_args

def generate_smtlib_declaration(func_head, p):
    """Generate SMT-LIB declaration for a function head.

    This version keys into p.symbol_table by the **function head object**
    (e.g., `f`, `g`, `h`) rather than by its Python type, so mixed arities
    across different heads won't collide.
    """
    # find function head's domain/range 
    type_signature = p.symbol_table[func_head]
    func_name = func_head.name

    # checks if uf head is a function
    if callable(type_signature):
        # Callable[[arg_types...], return_type]
        tuple_args = get_args(type_signature)
        if tuple_args:  # has type arguments
            func_params, func_return_type = tuple_args[0], tuple_args[1]
            if isinstance(func_params, (list, tuple)):
                arg_types = list(func_params)   # already a list/tuple → just convert
            else:
                arg_types = [func_params] 

            smt_arg_types = [p._known_types[arg_type] for arg_type in arg_types]
            smt_return_type = p._known_types[func_return_type]

            params_signature = f"({' '.join(smt_arg_types)})"

Review comment (suggestion):
Rather than defining a new function it would be better to do this in the existing `_auto_declare_smtlib` function.

Code after:
            return name
        else:
            f = x.evalf(self._precision) if self._precision else x.evalf()
            return self._print_Float(f)

    def _print_UndefinedFunction(self, x):
        assert self._is_legal_name(x.name)
        return x.name

    def _print_Exp1(self, x):
        return (
            self._print_Function(exp(1, evaluate=False))
            if exp in self._known_functions else
            self._print_NumberSymbol(x)
        )

    def emptyPrinter(self, expr):
        raise NotImplementedError(f'Cannot convert `{repr(expr)}` of type `{type(expr)}` to SMT.')


def smtlib_code(
    expr,
    auto_assert=True, auto_declare=True,
    precision=None,
    symbol_table=None,
    known_types=None, known_constants=None, known_functions=None,
    prefix_expressions=None, suffix_expressions=None,
    log_warn=None
):
    r"""Converts ``expr`` to a string of smtlib code.

    Parameters
    ==========

    expr : Expr | List[Expr]
        A SymPy expression or system to be converted.
    auto_assert : bool, optional
        If false, do not modify expr and produce only the S-Expression equivalent of expr.
        If true, assume expr is a system and assert each boolean element.
    auto_declare : bool, optional
        If false, do not produce declarations for the symbols used in expr.
        If true, prepend all necessary declarations for variables used in expr based on symbol_table.
    precision : integer, optional
        The ``evalf(..)`` precision for numbers such as pi.
    symbol_table : dict, optional
        A dictionary where keys are ``Symbol`` or ``Function`` instances and values are their Python type i.e. ``bool``, ``int``, ``float``, or ``Callable[...]``.
        If incomplete, an attempt will be made to infer types from ``expr``.
    known_types: dict, optional
        A dictionary where keys are ``bool``, ``int``, ``float`` etc. and values are their corresponding SMT type names.
        If not given, a partial listing compatible with several solvers will be used.
    known_functions : dict, optional