From 9634f7edaa4d4ff2cace4fe567e0f61f95199bc0 Mon Sep 17 00:00:00 2001 From: Michael Tautschnig Date: Sat, 29 Nov 2025 17:28:59 +0100 Subject: [PATCH] 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 --- .../cbmc/integer-assignments1/test.desc | 2 +- src/solvers/Makefile | 1 + .../smt2_incremental/ast/smt_logics.def | 2 + .../smt2_incremental/ast/smt_sorts.cpp | 4 + .../smt2_incremental/ast/smt_sorts.def | 1 + src/solvers/smt2_incremental/ast/smt_sorts.h | 6 + .../smt2_incremental/ast/smt_terms.cpp | 18 ++ .../smt2_incremental/ast/smt_terms.def | 1 + src/solvers/smt2_incremental/ast/smt_terms.h | 11 + .../construct_value_expr_from_smt.cpp | 18 ++ .../smt2_incremental/convert_expr_to_smt.cpp | 57 +++- .../smt2_incremental/smt_to_smt2_string.cpp | 13 + .../theories/smt_integer_theory.cpp | 256 ++++++++++++++++++ .../theories/smt_integer_theory.h | 97 +++++++ src/util/mathematical_types.h | 9 + 15 files changed, 493 insertions(+), 3 deletions(-) create mode 100644 src/solvers/smt2_incremental/theories/smt_integer_theory.cpp create mode 100644 src/solvers/smt2_incremental/theories/smt_integer_theory.h diff --git a/regression/cbmc/integer-assignments1/test.desc b/regression/cbmc/integer-assignments1/test.desc index dd038ca9cf6..d2615e371c7 100644 --- a/regression/cbmc/integer-assignments1/test.desc +++ b/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$ diff --git a/src/solvers/Makefile b/src/solvers/Makefile index d8c790ae8db..00e66cf6f46 100644 --- a/src/solvers/Makefile +++ b/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 diff --git a/src/solvers/smt2_incremental/ast/smt_logics.def b/src/solvers/smt2_incremental/ast/smt_logics.def index 8caab47798b..125577fd2ec 100644 --- a/src/solvers/smt2_incremental/ast/smt_logics.def +++ b/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) diff --git a/src/solvers/smt2_incremental/ast/smt_sorts.cpp b/src/solvers/smt2_incremental/ast/smt_sorts.cpp index 589a21df8c9..794e5319281 100644 --- a/src/solvers/smt2_incremental/ast/smt_sorts.cpp +++ b/src/solvers/smt2_incremental/ast/smt_sorts.cpp @@ -83,6 +83,10 @@ const smt_sortt &smt_array_sortt::element_sort() const return static_cast(find(ID_value)); } +smt_int_sortt::smt_int_sortt() : smt_sortt{ID_smt_int_sort} +{ +} + template void accept(const smt_sortt &sort, const irep_idt &id, visitort &&visitor) { diff --git a/src/solvers/smt2_incremental/ast/smt_sorts.def b/src/solvers/smt2_incremental/ast/smt_sorts.def index 374cdcba4b3..1b47bfce944 100644 --- a/src/solvers/smt2_incremental/ast/smt_sorts.def +++ b/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) diff --git a/src/solvers/smt2_incremental/ast/smt_sorts.h b/src/solvers/smt2_incremental/ast/smt_sorts.h index 4cc58a9b94d..b5fc74ca635 100644 --- a/src/solvers/smt2_incremental/ast/smt_sorts.h +++ b/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: diff --git a/src/solvers/smt2_incremental/ast/smt_terms.cpp b/src/solvers/smt2_incremental/ast/smt_terms.cpp index f679217e1c4..c12f0e738c5 100644 --- a/src/solvers/smt2_incremental/ast/smt_terms.cpp +++ b/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(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(smt_termt::get_sort()); +} + smt_function_application_termt::smt_function_application_termt( smt_identifier_termt function_identifier, std::vector arguments) diff --git a/src/solvers/smt2_incremental/ast/smt_terms.def b/src/solvers/smt2_incremental/ast/smt_terms.def index 33fc99248e9..ea9835f4a48 100644 --- a/src/solvers/smt2_incremental/ast/smt_terms.def +++ b/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) diff --git a/src/solvers/smt2_incremental/ast/smt_terms.h b/src/solvers/smt2_incremental/ast/smt_terms.h index 5354cd62d72..2350df06ff3 100644 --- a/src/solvers/smt2_incremental/ast/smt_terms.h +++ b/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: diff --git a/src/solvers/smt2_incremental/construct_value_expr_from_smt.cpp b/src/solvers/smt2_incremental/construct_value_expr_from_smt.cpp index d9d3b7a1ce0..3a37a8db14a 100644 --- a/src/solvers/smt2_incremental/construct_value_expr_from_smt.cpp +++ b/src/solvers/smt2_incremental/construct_value_expr_from_smt.cpp @@ -2,6 +2,7 @@ #include #include +#include #include #include #include @@ -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(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 { diff --git a/src/solvers/smt2_incremental/convert_expr_to_smt.cpp b/src/solvers/smt2_incremental/convert_expr_to_smt.cpp index d5910628470..c16b3e68aef 100644 --- a/src/solvers/smt2_incremental/convert_expr_to_smt.cpp +++ b/src/solvers/smt2_incremental/convert_expr_to_smt.cpp @@ -8,6 +8,7 @@ #include #include #include +#include #include #include #include @@ -19,6 +20,7 @@ #include #include #include +#include #include #include @@ -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(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(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(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(operand.type()); + return can_cast_type(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(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(operand.type()); + return can_cast_type(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(operand.type()); + })) { return convert_multiary_operator_to_terms( multiply, converted, smt_bit_vector_theoryt::multiply); diff --git a/src/solvers/smt2_incremental/smt_to_smt2_string.cpp b/src/solvers/smt2_incremental/smt_to_smt2_string.cpp index 4d3558af3cc..53633335bbf 100644 --- a/src/solvers/smt2_incremental/smt_to_smt2_string.cpp +++ b/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) { diff --git a/src/solvers/smt2_incremental/theories/smt_integer_theory.cpp b/src/solvers/smt2_incremental/theories/smt_integer_theory.cpp new file mode 100644 index 00000000000..20583825011 --- /dev/null +++ b/src/solvers/smt2_incremental/theories/smt_integer_theory.cpp @@ -0,0 +1,256 @@ +// Author: Michael Tautschnig + +#include "smt_integer_theory.h" + +#include + +const char *smt_integer_theoryt::negt::identifier() +{ + return "-"; +} + +smt_sortt smt_integer_theoryt::negt::return_sort(const smt_termt &operand) +{ + return operand.get_sort(); +} + +void smt_integer_theoryt::negt::validate(const smt_termt &operand) +{ + INVARIANT( + operand.get_sort().cast(), + "Integer theory negation may only be applied to integer sorted terms."); +} + +const smt_function_application_termt::factoryt + smt_integer_theoryt::negate; + +const char *smt_integer_theoryt::addt::identifier() +{ + return "+"; +} + +smt_sortt smt_integer_theoryt::addt::return_sort( + const smt_termt &lhs, + const smt_termt &rhs) +{ + return lhs.get_sort(); +} + +void smt_integer_theoryt::addt::validate( + const smt_termt &lhs, + const smt_termt &rhs) +{ + INVARIANT( + lhs.get_sort().cast() && + rhs.get_sort().cast(), + "Integer theory addition may only be applied to integer sorted terms."); +} + +const smt_function_application_termt::factoryt + smt_integer_theoryt::add; + +const char *smt_integer_theoryt::subt::identifier() +{ + return "-"; +} + +smt_sortt smt_integer_theoryt::subt::return_sort( + const smt_termt &lhs, + const smt_termt &rhs) +{ + return lhs.get_sort(); +} + +void smt_integer_theoryt::subt::validate( + const smt_termt &lhs, + const smt_termt &rhs) +{ + INVARIANT( + lhs.get_sort().cast() && + rhs.get_sort().cast(), + "Integer theory subtraction may only be applied to integer sorted terms."); +} + +const smt_function_application_termt::factoryt + smt_integer_theoryt::sub; + +const char *smt_integer_theoryt::mult::identifier() +{ + return "*"; +} + +smt_sortt smt_integer_theoryt::mult::return_sort( + const smt_termt &lhs, + const smt_termt &rhs) +{ + return lhs.get_sort(); +} + +void smt_integer_theoryt::mult::validate( + const smt_termt &lhs, + const smt_termt &rhs) +{ + INVARIANT( + lhs.get_sort().cast() && + rhs.get_sort().cast(), + "Integer theory multiplication may only be applied to integer sorted " + "terms."); +} + +const smt_function_application_termt::factoryt + smt_integer_theoryt::mul; + +const char *smt_integer_theoryt::divt::identifier() +{ + return "div"; +} + +smt_sortt smt_integer_theoryt::divt::return_sort( + const smt_termt &lhs, + const smt_termt &rhs) +{ + return lhs.get_sort(); +} + +void smt_integer_theoryt::divt::validate( + const smt_termt &lhs, + const smt_termt &rhs) +{ + INVARIANT( + lhs.get_sort().cast() && + rhs.get_sort().cast(), + "Integer theory division may only be applied to integer sorted terms."); +} + +const smt_function_application_termt::factoryt + smt_integer_theoryt::divide; + +const char *smt_integer_theoryt::modt::identifier() +{ + return "mod"; +} + +smt_sortt smt_integer_theoryt::modt::return_sort( + const smt_termt &lhs, + const smt_termt &rhs) +{ + return lhs.get_sort(); +} + +void smt_integer_theoryt::modt::validate( + const smt_termt &lhs, + const smt_termt &rhs) +{ + INVARIANT( + lhs.get_sort().cast() && + rhs.get_sort().cast(), + "Integer theory modulo may only be applied to integer sorted terms."); +} + +const smt_function_application_termt::factoryt + smt_integer_theoryt::mod; + +const char *smt_integer_theoryt::less_thant::identifier() +{ + return "<"; +} + +smt_sortt smt_integer_theoryt::less_thant::return_sort( + const smt_termt &lhs, + const smt_termt &rhs) +{ + return smt_bool_sortt{}; +} + +void smt_integer_theoryt::less_thant::validate( + const smt_termt &lhs, + const smt_termt &rhs) +{ + INVARIANT( + lhs.get_sort().cast() && + rhs.get_sort().cast(), + "Integer theory less than may only be applied to integer sorted terms."); +} + +const smt_function_application_termt::factoryt + smt_integer_theoryt::less_than; + +const char *smt_integer_theoryt::less_than_or_equalt::identifier() +{ + return "<="; +} + +smt_sortt smt_integer_theoryt::less_than_or_equalt::return_sort( + const smt_termt &lhs, + const smt_termt &rhs) +{ + return smt_bool_sortt{}; +} + +void smt_integer_theoryt::less_than_or_equalt::validate( + const smt_termt &lhs, + const smt_termt &rhs) +{ + INVARIANT( + lhs.get_sort().cast() && + rhs.get_sort().cast(), + "Integer theory less than or equal may only be applied to integer sorted " + "terms."); +} + +const smt_function_application_termt::factoryt< + smt_integer_theoryt::less_than_or_equalt> + smt_integer_theoryt::less_than_or_equal; + +const char *smt_integer_theoryt::greater_thant::identifier() +{ + return ">"; +} + +smt_sortt smt_integer_theoryt::greater_thant::return_sort( + const smt_termt &lhs, + const smt_termt &rhs) +{ + return smt_bool_sortt{}; +} + +void smt_integer_theoryt::greater_thant::validate( + const smt_termt &lhs, + const smt_termt &rhs) +{ + INVARIANT( + lhs.get_sort().cast() && + rhs.get_sort().cast(), + "Integer theory greater than may only be applied to integer sorted terms."); +} + +const smt_function_application_termt::factoryt< + smt_integer_theoryt::greater_thant> + smt_integer_theoryt::greater_than; + +const char *smt_integer_theoryt::greater_than_or_equalt::identifier() +{ + return ">="; +} + +smt_sortt smt_integer_theoryt::greater_than_or_equalt::return_sort( + const smt_termt &lhs, + const smt_termt &rhs) +{ + return smt_bool_sortt{}; +} + +void smt_integer_theoryt::greater_than_or_equalt::validate( + const smt_termt &lhs, + const smt_termt &rhs) +{ + INVARIANT( + lhs.get_sort().cast() && + rhs.get_sort().cast(), + "Integer theory greater than or equal may only be applied to integer " + "sorted terms."); +} + +const smt_function_application_termt::factoryt< + smt_integer_theoryt::greater_than_or_equalt> + smt_integer_theoryt::greater_than_or_equal; diff --git a/src/solvers/smt2_incremental/theories/smt_integer_theory.h b/src/solvers/smt2_incremental/theories/smt_integer_theory.h new file mode 100644 index 00000000000..80af11a29b1 --- /dev/null +++ b/src/solvers/smt2_incremental/theories/smt_integer_theory.h @@ -0,0 +1,97 @@ +// Author: Michael Tautschnig + +#ifndef CPROVER_SOLVERS_SMT2_INCREMENTAL_SMT_INTEGER_THEORY_H +#define CPROVER_SOLVERS_SMT2_INCREMENTAL_SMT_INTEGER_THEORY_H + +#include + +class smt_integer_theoryt +{ +public: + // Arithmetic operators + struct negt final + { + static const char *identifier(); + static smt_sortt return_sort(const smt_termt &operand); + static void validate(const smt_termt &operand); + }; + static const smt_function_application_termt::factoryt negate; + + struct addt final + { + static const char *identifier(); + static smt_sortt return_sort(const smt_termt &lhs, const smt_termt &rhs); + static void validate(const smt_termt &lhs, const smt_termt &rhs); + }; + static const smt_function_application_termt::factoryt add; + + struct subt final + { + static const char *identifier(); + static smt_sortt return_sort(const smt_termt &lhs, const smt_termt &rhs); + static void validate(const smt_termt &lhs, const smt_termt &rhs); + }; + static const smt_function_application_termt::factoryt sub; + + struct mult final + { + static const char *identifier(); + static smt_sortt return_sort(const smt_termt &lhs, const smt_termt &rhs); + static void validate(const smt_termt &lhs, const smt_termt &rhs); + }; + static const smt_function_application_termt::factoryt mul; + + struct divt final + { + static const char *identifier(); + static smt_sortt return_sort(const smt_termt &lhs, const smt_termt &rhs); + static void validate(const smt_termt &lhs, const smt_termt &rhs); + }; + static const smt_function_application_termt::factoryt divide; + + struct modt final + { + static const char *identifier(); + static smt_sortt return_sort(const smt_termt &lhs, const smt_termt &rhs); + static void validate(const smt_termt &lhs, const smt_termt &rhs); + }; + static const smt_function_application_termt::factoryt mod; + + // Comparison operators + struct less_thant final + { + static const char *identifier(); + static smt_sortt return_sort(const smt_termt &lhs, const smt_termt &rhs); + static void validate(const smt_termt &lhs, const smt_termt &rhs); + }; + static const smt_function_application_termt::factoryt less_than; + + struct less_than_or_equalt final + { + static const char *identifier(); + static smt_sortt return_sort(const smt_termt &lhs, const smt_termt &rhs); + static void validate(const smt_termt &lhs, const smt_termt &rhs); + }; + static const smt_function_application_termt::factoryt + less_than_or_equal; + + struct greater_thant final + { + static const char *identifier(); + static smt_sortt return_sort(const smt_termt &lhs, const smt_termt &rhs); + static void validate(const smt_termt &lhs, const smt_termt &rhs); + }; + static const smt_function_application_termt::factoryt + greater_than; + + struct greater_than_or_equalt final + { + static const char *identifier(); + static smt_sortt return_sort(const smt_termt &lhs, const smt_termt &rhs); + static void validate(const smt_termt &lhs, const smt_termt &rhs); + }; + static const smt_function_application_termt::factoryt + greater_than_or_equal; +}; + +#endif // CPROVER_SOLVERS_SMT2_INCREMENTAL_SMT_INTEGER_THEORY_H diff --git a/src/util/mathematical_types.h b/src/util/mathematical_types.h index 48d4438b12e..cb1ce88f6c8 100644 --- a/src/util/mathematical_types.h +++ b/src/util/mathematical_types.h @@ -31,6 +31,15 @@ class integer_typet : public typet constant_exprt one_expr() const; }; +/// Check whether a reference to a typet is a \ref integer_typet. +/// \param type: Source type. +/// \return True if \p type is a \ref integer_typet. +template <> +inline bool can_cast_type(const typet &type) +{ + return type.id() == ID_integer; +} + /// Natural numbers including zero (mathematical integers, not bitvectors) class natural_typet : public typet {