From 862a20cb5ac7de924d9cf2814f87cb6b9ee6e925 Mon Sep 17 00:00:00 2001 From: Michael Tautschnig Date: Sat, 29 Nov 2025 20:52:58 +0100 Subject: [PATCH] Add support for uninterpreted functions in incremental SMT2 solver Added handling for `ID_function_application` expressions in `convert_expr_to_smt()` and the `ID_mathematical_function` case to `convert_type_to_smt_sort()`. Fixes: #8068 --- .../cbmc/uninterpreted_function/uf1.desc | 2 +- .../cbmc/uninterpreted_function/uf2.desc | 2 +- .../smt2_incremental/convert_expr_to_smt.cpp | 114 +++++++++++++++++- .../smt2_incremental_decision_procedure.cpp | 66 ++++++++-- 4 files changed, 170 insertions(+), 14 deletions(-) diff --git a/regression/cbmc/uninterpreted_function/uf1.desc b/regression/cbmc/uninterpreted_function/uf1.desc index e03ec44fa2f..879865e93e3 100644 --- a/regression/cbmc/uninterpreted_function/uf1.desc +++ b/regression/cbmc/uninterpreted_function/uf1.desc @@ -1,4 +1,4 @@ -CORE no-new-smt +CORE uf1.c ^EXIT=10$ diff --git a/regression/cbmc/uninterpreted_function/uf2.desc b/regression/cbmc/uninterpreted_function/uf2.desc index f86b1257f94..b0daa371dd8 100644 --- a/regression/cbmc/uninterpreted_function/uf2.desc +++ b/regression/cbmc/uninterpreted_function/uf2.desc @@ -1,4 +1,4 @@ -CORE no-new-smt +CORE uf2.c ^EXIT=0$ diff --git a/src/solvers/smt2_incremental/convert_expr_to_smt.cpp b/src/solvers/smt2_incremental/convert_expr_to_smt.cpp index d5910628470..70ebcb90797 100644 --- a/src/solvers/smt2_incremental/convert_expr_to_smt.cpp +++ b/src/solvers/smt2_incremental/convert_expr_to_smt.cpp @@ -110,11 +110,27 @@ smt_sortt convert_type_to_smt_sort(const typet &type) { return convert_type_to_smt_sort(*array_type); } + if(can_cast_type(type)) + { + // Mathematical function types are not directly converted to sorts. + // They are used as function symbols in SMT and their applications + // are handled via function_application_exprt. + INVARIANT( + false, "mathematical_function type should not be converted to a sort"); + } UNIMPLEMENTED_FEATURE("Generation of SMT formula for type: " + type.pretty()); } static smt_termt convert_expr_to_smt(const symbol_exprt &symbol_expr) { + // Symbols with mathematical_function_typet represent uninterpreted functions. + // They should not be converted to SMT terms directly - only their applications + // (function_application_exprt) should be converted. + INVARIANT( + !can_cast_type(symbol_expr.type()), + "Symbols with mathematical_function_typet should not be converted to SMT " + "terms - only function applications should be converted"); + return smt_identifier_termt{symbol_expr.get_identifier(), convert_type_to_smt_sort(symbol_expr.type())}; } @@ -1405,6 +1421,67 @@ static smt_termt convert_expr_to_smt( "Generation of SMT formula for vector expression: " + vector.pretty()); } +static smt_termt convert_expr_to_smt( + const function_application_exprt &function_application, + const sub_expression_mapt &converted) +{ + // Get the function identifier - it should be a symbol with mathematical_function_typet + if( + const auto func_symbol = + expr_try_dynamic_cast(function_application.function())) + { + INVARIANT( + can_cast_type(func_symbol->type()), + "Function in function_application_exprt should have " + "mathematical_function_typet"); + + const auto &math_func_type = + to_mathematical_function_type(func_symbol->type()); + const smt_sortt return_sort = + convert_type_to_smt_sort(math_func_type.codomain()); + + // Convert function arguments + std::vector argument_terms; + for(const auto &arg : function_application.arguments()) + { + argument_terms.push_back(converted.at(arg)); + } + + // Create a simple factory for uninterpreted functions + struct uninterpreted_functiont + { + irep_idt name; + smt_sortt return_type; + + const char *identifier() const + { + return id2string(name).c_str(); + } + + smt_sortt return_sort(const std::vector &) const + { + return return_type; + } + + void validate(const std::vector &) const + { + // No validation needed for uninterpreted functions + } + }; + + const uninterpreted_functiont uninterpreted_function{ + func_symbol->get_identifier(), return_sort}; + + return smt_function_application_termt::factoryt( + uninterpreted_function)(argument_terms); + } + + UNIMPLEMENTED_FEATURE( + "Generation of SMT formula for function application with non-symbol " + "function: " + + function_application.pretty()); +} + static smt_termt convert_expr_to_smt( const object_size_exprt &object_size, const sub_expression_mapt &converted, @@ -1794,6 +1871,21 @@ static smt_termt dispatch_expr_to_smt_conversion( { return convert_expr_to_smt(*vector, converted); } + if(expr.id() == ID_tuple) + { + // Tuple expressions are used internally by function_application_exprt to + // store arguments. They should not be converted directly to SMT. + INVARIANT( + false, + "tuple expression should not be directly converted to SMT - it is used " + "internally by function_application_exprt"); + } + if( + const auto function_application = + expr_try_dynamic_cast(expr)) + { + return convert_expr_to_smt(*function_application, converted); + } if(const auto object_size = expr_try_dynamic_cast(expr)) { return convert_expr_to_smt(*object_size, converted, call_object_size); @@ -1956,11 +2048,27 @@ smt_termt convert_expr_to_smt( // Avoiding the conversion side steps a need to convert arbitrary code to // SMT terms. const auto address_of = expr_try_dynamic_cast(expr); - if(!address_of) - return true; - return !can_cast_type(address_of->object().type()); + if(address_of && can_cast_type(address_of->object().type())) + return false; + + // Tuple expressions are internal to function_application_exprt and + // should not be traversed or converted directly + if(expr.id() == ID_tuple) + return false; + + return true; }, [&](const exprt &expr) { + // Skip tuple expressions entirely - they're internal to function_application + if(expr.id() == ID_tuple) + return; + + // Skip symbols with mathematical_function_typet - they're declarations, not terms + if( + can_cast_expr(expr) && + can_cast_type(expr.type())) + return; + const auto find_result = sub_expression_map.find(expr); if(find_result != sub_expression_map.cend()) return; diff --git a/src/solvers/smt2_incremental/smt2_incremental_decision_procedure.cpp b/src/solvers/smt2_incremental/smt2_incremental_decision_procedure.cpp index 0d8a91a6f89..175ece217ff 100644 --- a/src/solvers/smt2_incremental/smt2_incremental_decision_procedure.cpp +++ b/src/solvers/smt2_incremental/smt2_incremental_decision_procedure.cpp @@ -6,6 +6,8 @@ #include #include #include +#include +#include #include #include #include @@ -68,8 +70,9 @@ get_problem_messages(const smt_responset &response) /// `convert_expr_to_smt`. This is because any sub expressions which /// `convert_expr_to_smt` translates into function applications, must also be /// returned by this`gather_dependent_expressions` function. -/// \details `symbol_exprt`, `array_exprt` and `nondet_symbol_exprt` add -/// dependant expressions. +/// \details `symbol_exprt`, `array_exprt`, `nondet_symbol_exprt`, and +/// `function_application_exprt` (for the function part) add dependant +/// expressions. static std::vector gather_dependent_expressions(const exprt &root_expr) { std::vector dependent_expressions; @@ -90,6 +93,24 @@ static std::vector gather_dependent_expressions(const exprt &root_expr) { dependent_expressions.push_back(expr_node); } + // For function applications, we need to gather the function symbol as a + // dependency so it gets declared, and we need to traverse the arguments + // explicitly to avoid traversing the tuple wrapper. + if( + const auto func_app = + expr_try_dynamic_cast(expr_node)) + { + if(can_cast_expr(func_app->function())) + { + dependent_expressions.push_back(func_app->function()); + } + // Push arguments for traversal (not the tuple wrapper) + for(const auto &arg : func_app->arguments()) + { + stack.push(&arg); + } + continue; // Skip normal operand traversal + } // The decision procedure does not depend on the values inside address of // code typed expressions. We can build the address without knowing the // value at that memory location. In this case the hypothetical compiled @@ -170,13 +191,40 @@ void send_function_definition( &expression_identifiers, std::unordered_map &identifier_table) { - const smt_declare_function_commandt function{ - smt_identifier_termt( - symbol_identifier, convert_type_to_smt_sort(expr.type())), - {}}; - expression_identifiers.emplace(expr, function.identifier()); - identifier_table.emplace(symbol_identifier, function.identifier()); - solver_process->send(function); + // Handle mathematical (uninterpreted) functions + if( + const auto math_func_type = + type_try_dynamic_cast(expr.type())) + { + // Build parameter sorts from the function domain + std::vector parameter_sorts; + for(const auto ¶m_type : math_func_type->domain()) + { + parameter_sorts.push_back(convert_type_to_smt_sort(param_type)); + } + + // The return sort comes from the codomain + const smt_sortt return_sort = + convert_type_to_smt_sort(math_func_type->codomain()); + + const smt_declare_function_commandt function{ + smt_identifier_termt(symbol_identifier, return_sort), parameter_sorts}; + + expression_identifiers.emplace(expr, function.identifier()); + identifier_table.emplace(symbol_identifier, function.identifier()); + solver_process->send(function); + } + else + { + // Normal symbol (non-function) declaration + const smt_declare_function_commandt function{ + smt_identifier_termt( + symbol_identifier, convert_type_to_smt_sort(expr.type())), + {}}; + expression_identifiers.emplace(expr, function.identifier()); + identifier_table.emplace(symbol_identifier, function.identifier()); + solver_process->send(function); + } } /// \brief Defines any functions which \p expr depends on, which have not yet