Make smt_function_application_termt constructor private

To prevent construction of function application without checking that
the given arguments are valid for the given function.

Author: thomasspriggs

src/solvers/smt2_incremental/smt_terms.h

@@ -113,13 +113,15 @@ 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.
+private:
+  /// Unchecked construction of function application terms. The public factoryt
+  /// sub class should be used to construct instances of this term with the
+  /// appropriate checks for the function being applied.
   smt_function_application_termt(
     smt_identifier_termt function_identifier,
     std::vector<smt_termt> arguments);
+
+public:
   const smt_identifier_termt &function_identifier() const;
   std::vector<std::reference_wrapper<const smt_termt>> arguments() const;
 

unit/solvers/smt2_incremental/smt_terms.cpp

@@ -2,6 +2,7 @@
 
 #include <testing-utils/use_catch.h>
 
+#include <solvers/smt2_incremental/smt_core_theory.h>
 #include <solvers/smt2_incremental/smt_terms.h>
 
 #include <util/mp_arith.h>
@@ -147,8 +148,7 @@ smt_bit_vector_constant_termt make_test_term<smt_bit_vector_constant_termt>()
 template <>
 smt_function_application_termt make_test_term<smt_function_application_termt>()
 {
-  return smt_function_application_termt{
-    smt_identifier_termt{"bar", smt_bool_sortt{}}, {}};
+  return smt_core_theoryt::make_not(smt_bool_literal_termt{true});
 }
 
 TEMPLATE_TEST_CASE(

unit/solvers/smt2_incremental/smt_to_smt2_string.cpp

@@ -3,6 +3,7 @@
 #include <testing-utils/use_catch.h>
 
 #include <solvers/smt2_incremental/smt_commands.h>
+#include <solvers/smt2_incremental/smt_core_theory.h>
 #include <solvers/smt2_incremental/smt_logics.h>
 #include <solvers/smt2_incremental/smt_sorts.h>
 #include <solvers/smt2_incremental/smt_terms.h>
@@ -36,10 +37,9 @@ TEST_CASE(
   "[core][smt2_incremental]")
 {
   CHECK(
-    smt_to_smt2_string(smt_function_application_termt{
-      smt_identifier_termt{"=", smt_bool_sortt{}},
-      {smt_identifier_termt{"foo", smt_bit_vector_sortt{32}},
-       {smt_identifier_termt{"bar", smt_bit_vector_sortt{32}}}}}) ==
+    smt_to_smt2_string(smt_core_theoryt::equal(
+      smt_identifier_termt{"foo", smt_bit_vector_sortt{32}},
+      smt_identifier_termt{"bar", smt_bit_vector_sortt{32}})) ==
     "(|=| |foo| |bar|)");
 }
 
@@ -102,10 +102,7 @@ TEST_CASE(
 
   CHECK(
     smt_to_smt2_string(smt_define_function_commandt{
-      "f",
-      {g, h},
-      smt_function_application_termt{
-        smt_identifier_termt{"=", smt_bool_sortt{}}, {g, h}}}) ==
+      "f", {g, h}, smt_core_theoryt::equal(g, h)}) ==
     "(define-fun |f| ((|g| (_ BitVec 32)) (|h| (_ BitVec 32))) Bool (|=| |g| "
     "|h|))");
 }