Implement SMT2 incremental support for arithmetic integers

Adds support for mathematical integers (`__CPROVER_integer`) via a new
smt_integer_theory with arithmetic and comparison operators.

Fixes: #8074

Author: tautschnig

regression/cbmc/integer-assignments1/test.desc

@@ -1,4 +1,4 @@
-CORE smt-backend broken-cprover-smt-backend no-new-smt
+CORE smt-backend broken-cprover-smt-backend
 main.c
 --trace --smt2
 ^EXIT=10$

src/solvers/Makefile

@@ -218,6 +218,7 @@ SRC = $(BOOLEFORCE_SRC) \
       smt2_incremental/theories/smt_array_theory.cpp \
       smt2_incremental/theories/smt_bit_vector_theory.cpp \
       smt2_incremental/theories/smt_core_theory.cpp \
+      smt2_incremental/theories/smt_integer_theory.cpp \
       # Empty last line
 
 include ../common

src/solvers/smt2_incremental/ast/smt_logics.def

@@ -11,4 +11,6 @@ LOGIC_ID(quantifier_free_bit_vectors, QF_BV)
 LOGIC_ID(quantifier_free_uninterpreted_functions_bit_vectors, QF_UFBV)
 LOGIC_ID(quantifier_free_bit_vectors_arrays, QF_ABV)
 LOGIC_ID(quantifier_free_arrays_uninterpreted_functions_bit_vectors, QF_AUFBV)
+LOGIC_ID(quantifier_free_uninterpreted_functions_linear_integer_arithmetic, QF_UFLIA)
+LOGIC_ID(quantifier_free_arrays_uninterpreted_functions_linear_integer_arithmetic, QF_AUFLIA)
 LOGIC_ID(all, ALL)

src/solvers/smt2_incremental/ast/smt_sorts.cpp

@@ -83,6 +83,10 @@ const smt_sortt &smt_array_sortt::element_sort() const
   return static_cast<const smt_sortt &>(find(ID_value));
 }
 
+smt_int_sortt::smt_int_sortt() : smt_sortt{ID_smt_int_sort}
+{
+}
+
 template <typename visitort>
 void accept(const smt_sortt &sort, const irep_idt &id, visitort &&visitor)
 {

src/solvers/smt2_incremental/ast/smt_sorts.def

@@ -9,3 +9,4 @@
 SORT_ID(bool)
 SORT_ID(bit_vector)
 SORT_ID(array)
+SORT_ID(int)

src/solvers/smt2_incremental/ast/smt_sorts.h

@@ -97,6 +97,12 @@ class smt_array_sortt final : public smt_sortt
   const smt_sortt &element_sort() const;
 };
 
+class smt_int_sortt final : public smt_sortt
+{
+public:
+  smt_int_sortt();
+};
+
 class smt_sort_const_downcast_visitort
 {
 public:

src/solvers/smt2_incremental/ast/smt_terms.cpp

@@ -125,6 +125,24 @@ const smt_bit_vector_sortt &smt_bit_vector_constant_termt::get_sort() const
   return static_cast<const smt_bit_vector_sortt &>(smt_termt::get_sort());
 }
 
+smt_int_constant_termt::smt_int_constant_termt(const mp_integer &value)
+  : smt_termt{ID_smt_int_constant_term, smt_int_sortt{}}
+{
+  set(ID_value, integer2string(value));
+}
+
+mp_integer smt_int_constant_termt::value() const
+{
+  return string2integer(get_string(ID_value));
+}
+
+const smt_int_sortt &smt_int_constant_termt::get_sort() const
+{
+  // The below cast is sound because the constructor only allows int
+  // sorts to be set.
+  return static_cast<const smt_int_sortt &>(smt_termt::get_sort());
+}
+
 smt_function_application_termt::smt_function_application_termt(
   smt_identifier_termt function_identifier,
   std::vector<smt_termt> arguments)

src/solvers/smt2_incremental/ast/smt_terms.def

@@ -9,6 +9,7 @@
 TERM_ID(bool_literal)
 TERM_ID(identifier)
 TERM_ID(bit_vector_constant)
+TERM_ID(int_constant)
 TERM_ID(function_application)
 TERM_ID(forall)
 TERM_ID(exists)

src/solvers/smt2_incremental/ast/smt_terms.h

@@ -129,6 +129,17 @@ class smt_bit_vector_constant_termt : public smt_termt
   const smt_bit_vector_sortt &get_sort() const;
 };
 
+class smt_int_constant_termt : public smt_termt
+{
+public:
+  smt_int_constant_termt(const mp_integer &value);
+  mp_integer value() const;
+
+  // This deliberately hides smt_termt::get_sort, because int terms
+  // always have int sorts.
+  const smt_int_sortt &get_sort() const;
+};
+
 class smt_function_application_termt : public smt_termt
 {
 private:

src/solvers/smt2_incremental/construct_value_expr_from_smt.cpp

@@ -2,6 +2,7 @@
 
 #include <util/arith_tools.h>
 #include <util/c_types.h>
+#include <util/mathematical_types.h>
 #include <util/namespace.h>
 #include <util/pointer_expr.h>
 #include <util/std_expr.h>
@@ -97,6 +98,23 @@ class value_expr_from_smt_factoryt : public smt_term_const_downcast_visitort
         type_to_construct.pretty());
   }
 
+  void visit(const smt_int_constant_termt &int_constant) override
+  {
+    if(
+      const auto integer_type =
+        type_try_dynamic_cast<integer_typet>(type_to_construct))
+    {
+      result = from_integer(int_constant.value(), type_to_construct);
+      return;
+    }
+
+    INVARIANT(
+      false,
+      "construct_value_expr_from_smt for integer should not be applied to "
+      "unsupported type " +
+        type_to_construct.pretty());
+  }
+
   void
   visit(const smt_function_application_termt &function_application) override
   {