Add indexed identifier support to smt function factoryt

This is implemented using sfinae to detect if the supplied `functiont`
has an `indices` member function or not, so that it is unneccessary to
add an `indices` member function which returns the empty collections of
indicies for the cases where `function` needs a simple (non indexed)
identifier.

`type_traits.h` is in `solvers/smt2_incremental/` because this is the
only part of the codebase where it is currently used and keeping it here
means the PR with this commit should need fewer code reviewer approvals.

Author: thomasspriggs

src/solvers/smt2_incremental/smt_terms.h

@@ -7,8 +7,10 @@
 
 #include <solvers/smt2_incremental/smt_index.h>
 #include <solvers/smt2_incremental/smt_sorts.h>
+#include <solvers/smt2_incremental/type_traits.h>
 
 #include <functional>
+#include <utility>
 
 class BigInt;
 using mp_integer = BigInt;
@@ -136,6 +138,44 @@ class smt_function_application_termt : public smt_termt
     smt_identifier_termt function_identifier,
     std::vector<smt_termt> arguments);
 
+  // This is used to detect if \p functiont has an `indicies` member function.
+  // It will resolve to std::true_type if it does or std::false type otherwise.
+  template <class functiont, class = void>
+  struct has_indicest : std::false_type
+  {
+  };
+
+  template <class functiont>
+  struct has_indicest<
+    functiont,
+    void_t<decltype(std::declval<functiont>().indices())>> : std::true_type
+  {
+  };
+
+  /// Overload for when \p functiont does not have indices.
+  template <class functiont>
+  static std::vector<smt_indext>
+  indices(const functiont &function, const std::false_type &has_indices)
+  {
+    return {};
+  }
+
+  /// Overload for when \p functiont has indices member function.
+  template <class functiont>
+  static std::vector<smt_indext>
+  indices(const functiont &function, const std::true_type &has_indices)
+  {
+    return function.indices();
+  }
+
+  /// Returns `function.indices` if `functiont` has an `indices` member function
+  /// or returns an empty collection otherwise.
+  template <class functiont>
+  static std::vector<smt_indext> indices(const functiont &function)
+  {
+    return indices(function, has_indicest<functiont>{});
+  }
+
 public:
   const smt_identifier_termt &function_identifier() const;
   std::vector<std::reference_wrapper<const smt_termt>> arguments() const;
@@ -160,7 +200,8 @@ class smt_function_application_termt : public smt_termt
       function.validate(arguments...);
       auto return_sort = function.return_sort(arguments...);
       return smt_function_application_termt{
-        smt_identifier_termt{function.identifier(), std::move(return_sort)},
+        smt_identifier_termt{
+          function.identifier(), std::move(return_sort), indices(function)},
         {std::forward<argument_typest>(arguments)...}};
     }
   };

src/solvers/smt2_incremental/type_traits.h

@@ -0,0 +1,37 @@
+// Author: Diffblue Ltd.
+
+/// \file
+/// Back ports of utilities available in the `<type_traits>` library for C++14
+/// or C++17 to C++11. These can be replaced with the standard library versions
+/// as and when we upgrade the version CBMC is compiled with.
+
+#ifndef CPROVER_SOLVERS_SMT2_INCREMENTAL_TYPE_TRAITS_H
+#define CPROVER_SOLVERS_SMT2_INCREMENTAL_TYPE_TRAITS_H
+
+#include <type_traits>
+
+namespace detail // NOLINT
+{
+// Implementation detail of `void_t`.
+template <typename... typest>
+struct make_voidt
+{
+  using type = void;
+};
+} // namespace detail
+
+// The below definition is of a back-ported version of the C++17 STL
+// `std::void_t` template. This makes this particular template available when
+// compiling for the C++11 or C++14 standard versions. It will also compile
+// as-is when targeting the C++17 standard. The back-ported version is not added
+// to the `std` namespace as this would be undefined behaviour. However once we
+// permanently move to the new standard the below code should be removed
+// and `std::void_t` should be used directly, to avoid polluting the global
+// namespace. For example -
+//   `void_t<decltype(foo.bar())>`
+// should be updated to -
+//   `std::void_t<decltype(foo.bar())>`
+template <typename... typest>
+using void_t = typename detail::make_voidt<typest...>::type;
+
+#endif // CPROVER_SOLVERS_SMT2_INCREMENTAL_TYPE_TRAITS_H