Add parameterised function application factory

So that function specific INVARIANTS can be checked.

Author: thomasspriggs

src/solvers/smt2_incremental/smt_commands.cpp

@@ -198,3 +198,51 @@ void smt_commandt::accept(smt_command_const_downcast_visitort &&visitor) const
 {
   ::accept(*this, id(), std::move(visitor));
 }
+
+smt_command_functiont::smt_command_functiont(
+  const smt_declare_function_commandt &function_declaration)
+  : _identifier(function_declaration.identifier())
+{
+  const auto sort_references = function_declaration.parameter_sorts();
+  parameter_sorts =
+    make_range(sort_references).collect<decltype(parameter_sorts)>();
+}
+
+smt_command_functiont::smt_command_functiont(
+  const smt_define_function_commandt &function_definition)
+  : _identifier{function_definition.identifier()}
+{
+  const auto parameters = function_definition.parameters();
+  parameter_sorts =
+    make_range(parameters)
+      .map([](const smt_termt &term) { return term.get_sort(); })
+      .collect<decltype(parameter_sorts)>();
+}
+
+irep_idt smt_command_functiont::identifier() const
+{
+  return _identifier.identifier();
+}
+
+smt_sortt smt_command_functiont::return_sort(
+  const std::vector<smt_termt> &arguments) const
+{
+  return _identifier.get_sort();
+}
+
+void smt_command_functiont::validate(
+  const std::vector<smt_termt> &arguments) const
+{
+  INVARIANT(
+    parameter_sorts.size() == arguments.size(),
+    "Number of parameters and number of arguments must the the same.");
+  const auto parameter_sort_arguments =
+    make_range(parameter_sorts).zip(make_range(arguments));
+  for(const auto &parameter_sort_argument_pair : parameter_sort_arguments)
+  {
+    INVARIANT(
+      parameter_sort_argument_pair.first ==
+        parameter_sort_argument_pair.second.get_sort(),
+      "Sort of argument must have the same sort as the parameter.");
+  }
+}

src/solvers/smt2_incremental/smt_commands.h

@@ -132,4 +132,22 @@ class smt_command_const_downcast_visitort
 #undef COMMAND_ID
 };
 
+/// \brief A function generated from a command. Used for validating function
+///   application term arguments.
+class smt_command_functiont
+{
+private:
+  std::vector<smt_sortt> parameter_sorts;
+  smt_identifier_termt _identifier;
+
+public:
+  explicit smt_command_functiont(
+    const smt_declare_function_commandt &function_declaration);
+  explicit smt_command_functiont(
+    const smt_define_function_commandt &function_definition);
+  irep_idt identifier() const;
+  smt_sortt return_sort(const std::vector<smt_termt> &arguments) const;
+  void validate(const std::vector<smt_termt> &arguments) const;
+};
+
 #endif // CPROVER_SOLVERS_SMT2_INCREMENTAL_SMT_COMMANDS_H

src/solvers/smt2_incremental/smt_terms.h

@@ -121,11 +121,39 @@ class smt_bit_vector_constant_termt : public smt_termt
 class smt_function_application_termt : public smt_termt
 {
 public:
+  // Public access is deprecated and will be replaced with the `of` factory
+  // function which will perform checks relevant to the particular function
+  // being applied. To be fixed before the end of this PR.
   smt_function_application_termt(
     smt_identifier_termt function_identifier,
     std::vector<smt_termt> arguments);
   const smt_identifier_termt &function_identifier() const;
   std::vector<std::reference_wrapper<const smt_termt>> arguments() const;
+
+  template <typename functiont>
+  class factoryt
+  {
+  private:
+    functiont function;
+
+  public:
+    template <typename... function_type_argument_typest>
+    explicit factoryt(function_type_argument_typest &&... arguments)
+      : function{std::forward<function_type_argument_typest>(arguments)...}
+    {
+    }
+
+    template <typename... argument_typest>
+    smt_function_application_termt
+    operator()(argument_typest &&... arguments) const
+    {
+      function.validate(arguments...);
+      auto return_sort = function.return_sort(arguments...);
+      return smt_function_application_termt{
+        smt_identifier_termt{function.identifier(), std::move(return_sort)},
+        {std::forward<argument_typest>(arguments)...}};
+    }
+  };
 };
 
 class smt_term_const_downcast_visitort

unit/solvers/smt2_incremental/smt_commands.cpp

@@ -94,3 +94,15 @@ TEST_CASE("smt_set_option_commandt getter", "[core][smt2_incremental]")
   CHECK(smt_set_option_commandt{models_on}.option() == models_on);
   CHECK(smt_set_option_commandt{models_off}.option() == models_off);
 }
+
+TEST_CASE("SMT2 function application factory tests", "[core][smt2_incremental]")
+{
+  const smt_identifier_termt arbitary{"arbitary", smt_bool_sortt{}};
+  const smt_declare_function_commandt function_declaration{
+    arbitary, std::vector<smt_sortt>{smt_bool_sortt{}, smt_bool_sortt{}}};
+  const smt_function_application_termt::factoryt<smt_command_functiont> factory{
+    function_declaration};
+  const smt_function_application_termt application =
+    factory(std::vector<smt_termt>{smt_bool_literal_termt{true},
+                                   smt_bool_literal_termt{false}});
+}