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

Author: tautschnig

regression/cbmc/uninterpreted_function/uf1.desc

@@ -1,4 +1,4 @@
-CORE no-new-smt
+CORE
 uf1.c
 
 ^EXIT=10$

regression/cbmc/uninterpreted_function/uf2.desc

@@ -1,4 +1,4 @@
-CORE no-new-smt
+CORE
 uf2.c
 
 ^EXIT=0$

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<mathematical_function_typet>(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<mathematical_function_typet>(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<symbol_exprt>(function_application.function()))
+  {
+    INVARIANT(
+      can_cast_type<mathematical_function_typet>(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<smt_termt> 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<smt_termt> &) const
+      {
+        return return_type;
+      }
+
+      void validate(const std::vector<smt_termt> &) 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_functiont>(
+      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<function_application_exprt>(expr))
+  {
+    return convert_expr_to_smt(*function_application, converted);
+  }
   if(const auto object_size = expr_try_dynamic_cast<object_size_exprt>(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<address_of_exprt>(expr);
-      if(!address_of)
-        return true;
-      return !can_cast_type<code_typet>(address_of->object().type());
+      if(address_of && can_cast_type<code_typet>(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<symbol_exprt>(expr) &&
+        can_cast_type<mathematical_function_typet>(expr.type()))
+        return;
+
       const auto find_result = sub_expression_map.find(expr);
       if(find_result != sub_expression_map.cend())
         return;

src/solvers/smt2_incremental/smt2_incremental_decision_procedure.cpp

@@ -6,6 +6,8 @@
 #include <util/bitvector_expr.h>
 #include <util/byte_operators.h>
 #include <util/c_types.h>
+#include <util/mathematical_expr.h>
+#include <util/mathematical_types.h>
 #include <util/range.h>
 #include <util/simplify_expr.h>
 #include <util/std_expr.h>
@@ -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<exprt> gather_dependent_expressions(const exprt &root_expr)
 {
   std::vector<exprt> dependent_expressions;
@@ -90,6 +93,24 @@ static std::vector<exprt> 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<function_application_exprt>(expr_node))
+    {
+      if(can_cast_expr<symbol_exprt>(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<irep_idt, smt_identifier_termt> &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<mathematical_function_typet>(expr.type()))
+  {
+    // Build parameter sorts from the function domain
+    std::vector<smt_sortt> parameter_sorts;
+    for(const auto &param_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