Implement SMT2 incremental support for arithmetic integers

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
   {

src/solvers/smt2_incremental/convert_expr_to_smt.cpp

@@ -8,6 +8,7 @@
 #include <util/expr_cast.h>
 #include <util/floatbv_expr.h>
 #include <util/mathematical_expr.h>
+#include <util/mathematical_types.h>
 #include <util/pointer_expr.h>
 #include <util/pointer_predicates.h>
 #include <util/range.h>
@@ -19,6 +20,7 @@
 #include <solvers/smt2_incremental/theories/smt_array_theory.h>
 #include <solvers/smt2_incremental/theories/smt_bit_vector_theory.h>
 #include <solvers/smt2_incremental/theories/smt_core_theory.h>
+#include <solvers/smt2_incremental/theories/smt_integer_theory.h>
 
 #include <algorithm>
 #include <functional>
@@ -96,6 +98,11 @@ static smt_sortt convert_type_to_smt_sort(const array_typet &type)
     convert_type_to_smt_sort(type.element_type())};
 }
 
+static smt_sortt convert_type_to_smt_sort(const integer_typet &type)
+{
+  return smt_int_sortt{};
+}
+
 smt_sortt convert_type_to_smt_sort(const typet &type)
 {
   if(const auto bool_type = type_try_dynamic_cast<bool_typet>(type))
@@ -110,6 +117,10 @@ smt_sortt convert_type_to_smt_sort(const typet &type)
   {
     return convert_type_to_smt_sort(*array_type);
   }
+  if(const auto integer_type = type_try_dynamic_cast<integer_typet>(type))
+  {
+    return convert_type_to_smt_sort(*integer_type);
+  }
   UNIMPLEMENTED_FEATURE("Generation of SMT formula for type: " + type.pretty());
 }
 
@@ -237,6 +248,13 @@ struct sort_based_cast_to_bit_vector_convertert final
       "Generation of SMT formula for type cast to bit vector from type: " +
       from_type.pretty());
   }
+
+  void visit(const smt_int_sortt &) override
+  {
+    UNIMPLEMENTED_FEATURE(
+      "Generation of SMT formula for type cast to bit vector from integer "
+      "type");
+  }
 };
 
 static smt_termt convert_bit_vector_cast(
@@ -324,6 +342,21 @@ struct sort_based_literal_convertert : public smt_sort_const_downcast_visitort
     UNIMPLEMENTED_FEATURE(
       "Conversion of array SMT literal " + array_sort.pretty());
   }
+
+  void visit(const smt_int_sortt &) override
+  {
+    if(member_input.type() == integer_typet{})
+    {
+      const auto value = numeric_cast_v<mp_integer>(member_input);
+      result = smt_int_constant_termt{value};
+    }
+    else
+    {
+      UNIMPLEMENTED_FEATURE(
+        "Conversion of non-integer constant to integer SMT sort: " +
+        member_input.type().pretty());
+    }
+  }
 };
 
 static smt_termt convert_expr_to_smt(const constant_exprt &constant_literal)
@@ -640,8 +673,18 @@ static smt_termt convert_expr_to_smt(
 {
   if(std::all_of(
        plus.operands().cbegin(), plus.operands().cend(), [](exprt operand) {
-         return can_cast_type<integer_bitvector_typet>(operand.type());
+         return can_cast_type<integer_typet>(operand.type());
        }))
+  {
+    return convert_multiary_operator_to_terms(
+      plus, converted, smt_integer_theoryt::add);
+  }
+  else if(std::all_of(
+            plus.operands().cbegin(),
+            plus.operands().cend(),
+            [](exprt operand) {
+              return can_cast_type<integer_bitvector_typet>(operand.type());
+            }))
   {
     return convert_multiary_operator_to_terms(
       plus, converted, smt_bit_vector_theoryt::add);
@@ -841,8 +884,18 @@ static smt_termt convert_expr_to_smt(
        multiply.operands().cbegin(),
        multiply.operands().cend(),
        [](exprt operand) {
-         return can_cast_type<integer_bitvector_typet>(operand.type());
+         return can_cast_type<integer_typet>(operand.type());
        }))
+  {
+    return convert_multiary_operator_to_terms(
+      multiply, converted, smt_integer_theoryt::mul);
+  }
+  else if(std::all_of(
+            multiply.operands().cbegin(),
+            multiply.operands().cend(),
+            [](exprt operand) {
+              return can_cast_type<integer_bitvector_typet>(operand.type());
+            }))
   {
     return convert_multiary_operator_to_terms(
       multiply, converted, smt_bit_vector_theoryt::multiply);

src/solvers/smt2_incremental/smt_to_smt2_string.cpp

@@ -80,6 +80,11 @@ class smt_sort_output_visitort : public smt_sort_const_downcast_visitort
   {
     os << "(Array " << array.index_sort() << " " << array.element_sort() << ")";
   }
+
+  void visit(const smt_int_sortt &) override
+  {
+    os << "Int";
+  }
 };
 
 std::ostream &operator<<(std::ostream &os, const smt_sortt &sort)
@@ -156,6 +161,7 @@ class smt_term_to_string_convertert : private smt_term_const_downcast_visitort
   void visit(const smt_bool_literal_termt &bool_literal) override;
   void visit(const smt_identifier_termt &identifier_term) override;
   void visit(const smt_bit_vector_constant_termt &bit_vector_constant) override;
+  void visit(const smt_int_constant_termt &int_constant) override;
   void
   visit(const smt_function_application_termt &function_application) override;
   void visit(const smt_forall_termt &forall) override;
@@ -273,6 +279,13 @@ void smt_term_to_string_convertert::visit(
   push_outputs("(_ bv", std::move(value), " ", std::move(bit_width), ")");
 }
 
+void smt_term_to_string_convertert::visit(
+  const smt_int_constant_termt &int_constant)
+{
+  auto value = integer2string(int_constant.value());
+  push_outputs(std::move(value));
+}
+
 void smt_term_to_string_convertert::visit(
   const smt_function_application_termt &function_application)
 {