Repository: sympy/sympy
File: sympy/logic/algorithms/z3_wrapper.py (Python)

Code before:
        return False
    elif res == "sat":
        model = z3_model_to_sympy_model(s.model(), expr)
        has_theory_preds = any(is_supported_predicate(pred) for pred in expr.encoding.keys())

        if has_theory_preds:
            return True
        if model:
            return model

        return True


def z3_model_to_sympy_model(z3_model, enc_cnf):
    rev_enc = {value: key for key, value in enc_cnf.encoding.items()}
    result = {}
    for var in z3_model:
        var_name = var.name()
        # Only process variables that start with 'd' followed by digits
        if var_name.startswith('d') and var_name[1:].isdigit():
            var_id = int(var_name[1:])
            # Only include if this variable ID exists in our reverse encoding
            if var_id in rev_enc:
                result[rev_enc[var_id]] = bool(z3_model[var])
    return result


def clause_to_assertion(clause):
    """Converts a single CNF clause to SMT-LIB assertion format."""
    clause_strings = [f"d{abs(lit)}" if lit > 0 else f"(not d{abs(lit)})" for lit in clause]
    return "(assert (or " + " ".join(clause_strings) + "))"


def find_uninterpreted_functions(expr):
    uf_arity = {}
    # Handle bare function heads (symbols that are functions but not called)
    for head in expr.atoms(UndefinedFunction):
        uf_arity.setdefault(str(head), None)
    # Handle function calls like f(a), g(x,y)
    if AppliedUndef is not None:
        calls = expr.atoms(AppliedUndef)
    else:
        calls = [c for c in expr.atoms(Function) if isinstance(c.func, UndefinedFunction)]

    for call in calls:
        name = str(call.func)
        arity = len(call.args)
        prev = uf_arity.get(name)
        uf_arity[name] = arity if prev is None else max(prev or 0, arity)

    return uf_arity

Review comment (suggestion):
I'm pretty sure there will never be any UndefinedFunctions -- there should only every be AppliedUndef 

Code after:
    for pred, enc in enc_cnf.encoding.items():
        uninterpreted_functions_to_arity.update({uf.func : len(uf.args) for uf in pred.atoms(AppliedUndef)})

    # symbol_table must be provided for smtlib_code, even though
    # it's unused when auto_declare is set to False
    symbol_table = dict.fromkeys(uninterpreted_functions_to_arity,Callable[..., float] )

    symbols = set()
    for pred, enc in enc_cnf.encoding.items():
        if not isinstance(pred, AppliedPredicate):
            continue
        if pred.function not in supported_predicates:
            continue

        pred_str = smtlib_code(pred, auto_declare=False, auto_assert=False, known_functions=known_functions,
                               symbol_table=symbol_table)

        symbols |= pred.free_symbols
        pred = pred_str
        assertion = f"(assert  (implies d{enc} {pred}))"
        assertions.append(assertion)

    for sym in symbols:
        declarations.append(f"(declare-const {sym} Real)")

    for f, arity in uninterpreted_functions_to_arity.items():
        # Rather than defining new types for the domain and range
        # we assume they are real to avoid unnecesary complexity.
        arg_types = " ".join(["Real"] * arity)
        declarations.append(f"(declare-fun {f} ({arg_types}) Real)")

    declarations = "\n".join(declarations)
    assertions = "\n".join(assertions)
    s.from_string(declarations)
    s.from_string(assertions)

    return s


known_functions = {
            Add: '+',
            Mul: '*',

            Equality: '=',
            LessThan: '<=',
            GreaterThan: '>=',
            StrictLessThan: '<',
            StrictGreaterThan: '>',

            EqualityPredicate(): '=',
            LessThanPredicate(): '<=',