diff --git a/src/solvers/Makefile b/src/solvers/Makefile index 6b6edee3a4e..6c87438ad56 100644 --- a/src/solvers/Makefile +++ b/src/solvers/Makefile @@ -192,7 +192,9 @@ SRC = $(BOOLEFORCE_SRC) \ smt2/smt2_parser.cpp \ smt2/smt2_tokenizer.cpp \ smt2/smt2irep.cpp \ + smt2_incremental/smt_bit_vector_theory.cpp \ smt2_incremental/smt_commands.cpp \ + smt2_incremental/smt_core_theory.cpp \ smt2_incremental/smt_logics.cpp \ smt2_incremental/smt_options.cpp \ smt2_incremental/smt_sorts.cpp \ diff --git a/src/solvers/smt2_incremental/smt_bit_vector_theory.cpp b/src/solvers/smt2_incremental/smt_bit_vector_theory.cpp new file mode 100644 index 00000000000..2f1f866a87e --- /dev/null +++ b/src/solvers/smt2_incremental/smt_bit_vector_theory.cpp @@ -0,0 +1,44 @@ +// Author: Diffblue Ltd. + +#include + +#include + +static void validate_bit_vector_predicate_arguments( + const smt_termt &left, + const smt_termt &right) +{ + const auto left_sort = left.get_sort().cast(); + INVARIANT(left_sort, "Left operand must have bitvector sort."); + const auto right_sort = right.get_sort().cast(); + INVARIANT(right_sort, "Right operand must have bitvector sort."); + // The below invariant is based on the smtlib standard. + // See http://smtlib.cs.uiowa.edu/logics-all.shtml#QF_BV + INVARIANT( + left_sort->bit_width() == right_sort->bit_width(), + "Left and right operands must have the same bit width."); +} + +#define SMT_BITVECTOR_THEORY_PREDICATE(the_identifier, the_name) \ + void smt_bit_vector_theoryt::the_name##t::validate( \ + const smt_termt &left, const smt_termt &right) \ + { \ + validate_bit_vector_predicate_arguments(left, right); \ + } \ + \ + smt_sortt smt_bit_vector_theoryt::the_name##t::return_sort( \ + const smt_termt &, const smt_termt &) \ + { \ + return smt_bool_sortt{}; \ + } \ + \ + const char *smt_bit_vector_theoryt::the_name##t::identifier() \ + { \ + return #the_identifier; \ + } \ + \ + const smt_function_application_termt::factoryt< \ + smt_bit_vector_theoryt::the_name##t> \ + smt_bit_vector_theoryt::the_name{}; +#include "smt_bit_vector_theory.def" +#undef SMT_BITVECTOR_THEORY_PREDICATE diff --git a/src/solvers/smt2_incremental/smt_bit_vector_theory.def b/src/solvers/smt2_incremental/smt_bit_vector_theory.def new file mode 100644 index 00000000000..675526aa0b5 --- /dev/null +++ b/src/solvers/smt2_incremental/smt_bit_vector_theory.def @@ -0,0 +1,13 @@ +/// \file +/// This set of definitions is used as part of the +/// [X-macro](https://en.wikipedia.org/wiki/X_Macro) pattern. These define the +/// set of bitvector theory functions which are implemented and it is used to +/// automate repetitive parts of the implementation. +SMT_BITVECTOR_THEORY_PREDICATE(bvult, unsigned_less_than) +SMT_BITVECTOR_THEORY_PREDICATE(bvule, unsigned_less_than_or_equal) +SMT_BITVECTOR_THEORY_PREDICATE(bvugt, unsigned_greater_than) +SMT_BITVECTOR_THEORY_PREDICATE(bvuge, unsigned_greater_than_or_equal) +SMT_BITVECTOR_THEORY_PREDICATE(bvslt, signed_less_than) +SMT_BITVECTOR_THEORY_PREDICATE(bvsle, signed_less_than_or_equal) +SMT_BITVECTOR_THEORY_PREDICATE(bvsgt, signed_greater_than) +SMT_BITVECTOR_THEORY_PREDICATE(bvsge, signed_greater_than_or_equal) diff --git a/src/solvers/smt2_incremental/smt_bit_vector_theory.h b/src/solvers/smt2_incremental/smt_bit_vector_theory.h new file mode 100644 index 00000000000..2a5fffc8a2f --- /dev/null +++ b/src/solvers/smt2_incremental/smt_bit_vector_theory.h @@ -0,0 +1,25 @@ +// Author: Diffblue Ltd. + +#ifndef CPROVER_SOLVERS_SMT2_INCREMENTAL_SMT_BIT_VECTOR_THEORY_H +#define CPROVER_SOLVERS_SMT2_INCREMENTAL_SMT_BIT_VECTOR_THEORY_H + +#include + +class smt_bit_vector_theoryt +{ +public: +#define SMT_BITVECTOR_THEORY_PREDICATE(the_identifier, the_name) \ + /* NOLINTNEXTLINE(readability/identifiers) cpplint does not match the ## */ \ + struct the_name##t final \ + { \ + static const char *identifier(); \ + static smt_sortt \ + return_sort(const smt_termt &left, const smt_termt &right); \ + static void validate(const smt_termt &left, const smt_termt &right); \ + }; \ + static const smt_function_application_termt::factoryt the_name; +#include "smt_bit_vector_theory.def" +#undef SMT_BITVECTOR_THEORY_PREDICATE +}; + +#endif // CPROVER_SOLVERS_SMT2_INCREMENTAL_SMT_BIT_VECTOR_THEORY_H diff --git a/src/solvers/smt2_incremental/smt_commands.cpp b/src/solvers/smt2_incremental/smt_commands.cpp index 6df79441599..17ccfe31681 100644 --- a/src/solvers/smt2_incremental/smt_commands.cpp +++ b/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(); +} + +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(); +} + +irep_idt smt_command_functiont::identifier() const +{ + return _identifier.identifier(); +} + +smt_sortt smt_command_functiont::return_sort( + const std::vector &arguments) const +{ + return _identifier.get_sort(); +} + +void smt_command_functiont::validate( + const std::vector &arguments) const +{ + INVARIANT( + parameter_sorts.size() == arguments.size(), + "Number of parameters and number of arguments must be the same."); + const auto parameter_sort_arguments = + make_range(parameter_sorts).zip(make_range(arguments)); + for(const auto ¶meter_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."); + } +} diff --git a/src/solvers/smt2_incremental/smt_commands.h b/src/solvers/smt2_incremental/smt_commands.h index aece515e41a..39a721c1b38 100644 --- a/src/solvers/smt2_incremental/smt_commands.h +++ b/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 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 &arguments) const; + void validate(const std::vector &arguments) const; +}; + #endif // CPROVER_SOLVERS_SMT2_INCREMENTAL_SMT_COMMANDS_H diff --git a/src/solvers/smt2_incremental/smt_core_theory.cpp b/src/solvers/smt2_incremental/smt_core_theory.cpp new file mode 100644 index 00000000000..6c3348caf64 --- /dev/null +++ b/src/solvers/smt2_incremental/smt_core_theory.cpp @@ -0,0 +1,200 @@ +// Author: Diffblue Ltd. + +#include + +const char *smt_core_theoryt::nott::identifier() +{ + return "not"; +} + +smt_sortt smt_core_theoryt::nott::return_sort(const smt_termt &operand) +{ + return smt_bool_sortt{}; +} + +void smt_core_theoryt::nott::validate(const smt_termt &operand) +{ + INVARIANT( + operand.get_sort() == smt_bool_sortt{}, + "\"not\" may only be applied to terms which have bool sort."); +} + +const smt_function_application_termt::factoryt + smt_core_theoryt::make_not{}; + +const char *smt_core_theoryt::impliest::identifier() +{ + return "=>"; +} + +smt_sortt +smt_core_theoryt::impliest::return_sort(const smt_termt &, const smt_termt &) +{ + return smt_bool_sortt{}; +} + +void smt_core_theoryt::impliest::validate( + const smt_termt &lhs, + const smt_termt &rhs) +{ + INVARIANT( + lhs.get_sort() == smt_bool_sortt{}, + "Left hand side of \"=>\" must have bool sort."); + INVARIANT( + rhs.get_sort() == smt_bool_sortt{}, + "Right hand side of \"=>\" must have bool sort."); +} + +const smt_function_application_termt::factoryt + smt_core_theoryt::implies{}; + +const char *smt_core_theoryt::andt::identifier() +{ + return "and"; +} + +smt_sortt +smt_core_theoryt::andt::return_sort(const smt_termt &, const smt_termt &) +{ + return smt_bool_sortt{}; +} + +void smt_core_theoryt::andt::validate( + const smt_termt &lhs, + const smt_termt &rhs) +{ + INVARIANT( + lhs.get_sort() == smt_bool_sortt{}, + "Left hand side of \"and\" must have bool sort."); + INVARIANT( + rhs.get_sort() == smt_bool_sortt{}, + "Right hand side of \"and\" must have bool sort."); +} + +const smt_function_application_termt::factoryt + smt_core_theoryt::make_and{}; + +const char *smt_core_theoryt::ort::identifier() +{ + return "or"; +} + +smt_sortt +smt_core_theoryt::ort::return_sort(const smt_termt &, const smt_termt &) +{ + return smt_bool_sortt{}; +} + +void smt_core_theoryt::ort::validate(const smt_termt &lhs, const smt_termt &rhs) +{ + INVARIANT( + lhs.get_sort() == smt_bool_sortt{}, + "Left hand side of \"or\" must have bool sort."); + INVARIANT( + rhs.get_sort() == smt_bool_sortt{}, + "Right hand side of \"or\" must have bool sort."); +} + +const smt_function_application_termt::factoryt + smt_core_theoryt::make_or{}; + +const char *smt_core_theoryt::xort::identifier() +{ + return "xor"; +} + +smt_sortt +smt_core_theoryt::xort::return_sort(const smt_termt &, const smt_termt &) +{ + return smt_bool_sortt{}; +} + +void smt_core_theoryt::xort::validate( + const smt_termt &lhs, + const smt_termt &rhs) +{ + INVARIANT( + lhs.get_sort() == smt_bool_sortt{}, + "Left hand side of \"xor\" must have bool sort."); + INVARIANT( + rhs.get_sort() == smt_bool_sortt{}, + "Right hand side of \"xor\" must have bool sort."); +} + +const smt_function_application_termt::factoryt + smt_core_theoryt::make_xor{}; + +const char *smt_core_theoryt::equalt::identifier() +{ + return "="; +} + +smt_sortt +smt_core_theoryt::equalt::return_sort(const smt_termt &, const smt_termt &) +{ + return smt_bool_sortt{}; +} + +void smt_core_theoryt::equalt::validate( + const smt_termt &lhs, + const smt_termt &rhs) +{ + INVARIANT( + lhs.get_sort() == rhs.get_sort(), + "\"=\" may only be applied to terms which have the same sort."); +} + +const smt_function_application_termt::factoryt + smt_core_theoryt::equal{}; + +const char *smt_core_theoryt::distinctt::identifier() +{ + return "distinct"; +} + +smt_sortt +smt_core_theoryt::distinctt::return_sort(const smt_termt &, const smt_termt &) +{ + return smt_bool_sortt{}; +} + +void smt_core_theoryt::distinctt::validate( + const smt_termt &lhs, + const smt_termt &rhs) +{ + INVARIANT( + lhs.get_sort() == rhs.get_sort(), + "\"distinct\" may only be applied to terms which have the same sort."); +} + +const smt_function_application_termt::factoryt + smt_core_theoryt::distinct{}; + +const char *smt_core_theoryt::if_then_elset::identifier() +{ + return "ite"; +} + +smt_sortt smt_core_theoryt::if_then_elset::return_sort( + const smt_termt &, + const smt_termt &then_term, + const smt_termt &) +{ + return then_term.get_sort(); +} + +void smt_core_theoryt::if_then_elset::validate( + const smt_termt &condition, + const smt_termt &then_term, + const smt_termt &else_term) +{ + INVARIANT( + condition.get_sort() == smt_bool_sortt{}, + "Condition term must have bool sort."); + INVARIANT( + then_term.get_sort() == else_term.get_sort(), + "\"ite\" must have \"then\" and \"else\" terms of the same sort."); +} + +const smt_function_application_termt::factoryt + smt_core_theoryt::if_then_else; diff --git a/src/solvers/smt2_incremental/smt_core_theory.h b/src/solvers/smt2_incremental/smt_core_theory.h new file mode 100644 index 00000000000..d59725ac57d --- /dev/null +++ b/src/solvers/smt2_incremental/smt_core_theory.h @@ -0,0 +1,83 @@ +// Author: Diffblue Ltd. + +#ifndef CPROVER_SOLVERS_SMT2_INCREMENTAL_SMT_CORE_THEORY_H +#define CPROVER_SOLVERS_SMT2_INCREMENTAL_SMT_CORE_THEORY_H + +#include + +class smt_core_theoryt +{ +public: + struct nott 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 make_not; + + struct impliest 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 implies; + + struct andt 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 make_and; + + struct ort 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 make_or; + + struct xort 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 make_xor; + + struct 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 equal; + + struct distinctt 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 distinct; + + struct if_then_elset final + { + static const char *identifier(); + static smt_sortt return_sort( + const smt_termt &condition, + const smt_termt &then_term, + const smt_termt &else_term); + static void validate( + const smt_termt &condition, + const smt_termt &then_term, + const smt_termt &else_term); + }; + static const smt_function_application_termt::factoryt + if_then_else; +}; + +#endif // CPROVER_SOLVERS_SMT2_INCREMENTAL_SMT_CORE_THEORY_H diff --git a/src/solvers/smt2_incremental/smt_sorts.cpp b/src/solvers/smt2_incremental/smt_sorts.cpp index 8a2567731f8..ed06bfee629 100644 --- a/src/solvers/smt2_incremental/smt_sorts.cpp +++ b/src/solvers/smt2_incremental/smt_sorts.cpp @@ -10,6 +10,29 @@ #include #undef SORT_ID +#define SORT_ID(the_id) \ + template <> \ + const smt_##the_id##_sortt *smt_sortt::cast() const & \ + { \ + return id() == ID_smt_##the_id##_sort \ + ? static_cast(this) \ + : nullptr; \ + } +#include // NOLINT(build/include) +#undef SORT_ID + +#define SORT_ID(the_id) \ + template <> \ + optionalt smt_sortt::cast() && \ + { \ + if(id() == ID_smt_##the_id##_sort) \ + return {std::move(*static_cast(this))}; \ + else \ + return {}; \ + } +#include // NOLINT(build/include) +#undef SORT_ID + bool smt_sortt::operator==(const smt_sortt &other) const { return irept::operator==(other); diff --git a/src/solvers/smt2_incremental/smt_sorts.h b/src/solvers/smt2_incremental/smt_sorts.h index ae5244b984f..5d80fbc0500 100644 --- a/src/solvers/smt2_incremental/smt_sorts.h +++ b/src/solvers/smt2_incremental/smt_sorts.h @@ -8,6 +8,7 @@ #define CPROVER_SOLVERS_SMT2_INCREMENTAL_SMT_SORTS_H #include +#include #include @@ -42,6 +43,12 @@ class smt_sortt : protected irept static const smt_sortt &downcast(const irept &); }; + template + const sub_classt *cast() const &; + + template + optionalt cast() &&; + protected: using irept::irept; }; diff --git a/src/solvers/smt2_incremental/smt_terms.cpp b/src/solvers/smt2_incremental/smt_terms.cpp index 8c631ff6ffb..72300fab67a 100644 --- a/src/solvers/smt2_incremental/smt_terms.cpp +++ b/src/solvers/smt2_incremental/smt_terms.cpp @@ -48,20 +48,6 @@ bool smt_bool_literal_termt::value() const return get_bool(ID_value); } -smt_not_termt::smt_not_termt(smt_termt operand) - : smt_termt{ID_smt_not_term, smt_bool_sortt{}} -{ - INVARIANT( - operand.get_sort() == smt_bool_sortt{}, - "smt_not_termt may only be applied to terms which have bool sort."); - get_sub().push_back(std::move(operand)); -} - -const smt_termt &smt_not_termt::operand() const -{ - return static_cast(get_sub().at(0)); -} - static bool is_valid_smt_identifier(irep_idt identifier) { static const std::regex valid{R"(^[^\|\\]*$)"}; diff --git a/src/solvers/smt2_incremental/smt_terms.def b/src/solvers/smt2_incremental/smt_terms.def index 77b5f210225..fbd46311e03 100644 --- a/src/solvers/smt2_incremental/smt_terms.def +++ b/src/solvers/smt2_incremental/smt_terms.def @@ -7,7 +7,6 @@ /// * The member functions of the `smt_term_const_downcast_visitort` class. /// * The type of term checks required to implement `smt_termt::accept`. TERM_ID(bool_literal) -TERM_ID(not) TERM_ID(identifier) TERM_ID(bit_vector_constant) TERM_ID(function_application) diff --git a/src/solvers/smt2_incremental/smt_terms.h b/src/solvers/smt2_incremental/smt_terms.h index f6b4d611a1e..0925c598c4a 100644 --- a/src/solvers/smt2_incremental/smt_terms.h +++ b/src/solvers/smt2_incremental/smt_terms.h @@ -75,13 +75,6 @@ class smt_bool_literal_termt : public smt_termt bool value() const; }; -class smt_not_termt : public smt_termt -{ -public: - explicit smt_not_termt(smt_termt operand); - const smt_termt &operand() const; -}; - /// Stores identifiers in unescaped and unquoted form. Any escaping or quoting /// required should be performed during printing. class smt_identifier_termt : public smt_termt @@ -120,12 +113,42 @@ class smt_bit_vector_constant_termt : public smt_termt class smt_function_application_termt : public smt_termt { -public: +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 arguments); + +public: const smt_identifier_termt &function_identifier() const; std::vector> arguments() const; + + template + class factoryt + { + private: + functiont function; + + public: + template + explicit factoryt(function_type_argument_typest &&... arguments) + : function{std::forward(arguments)...} + { + } + + template + 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(arguments)...}}; + } + }; }; class smt_term_const_downcast_visitort diff --git a/src/solvers/smt2_incremental/smt_to_smt2_string.cpp b/src/solvers/smt2_incremental/smt_to_smt2_string.cpp index da486f4f227..9be50d7e98e 100644 --- a/src/solvers/smt2_incremental/smt_to_smt2_string.cpp +++ b/src/solvers/smt2_incremental/smt_to_smt2_string.cpp @@ -102,7 +102,6 @@ class smt_term_to_string_convertert : private smt_term_const_downcast_visitort smt_term_to_string_convertert() = default; void visit(const smt_bool_literal_termt &bool_literal) override; - void visit(const smt_not_termt ¬_term) override; void visit(const smt_identifier_termt &identifier_term) override; void visit(const smt_bit_vector_constant_termt &bit_vector_constant) override; void @@ -171,11 +170,6 @@ void smt_term_to_string_convertert::visit( push_output(bool_literal.value() ? "true" : "false"); } -void smt_term_to_string_convertert::visit(const smt_not_termt ¬_term) -{ - push_outputs("(not ", not_term.operand(), ")"); -} - void smt_term_to_string_convertert::visit( const smt_identifier_termt &identifier_term) { diff --git a/unit/Makefile b/unit/Makefile index 4e730e7dc5f..572d8cf22b4 100644 --- a/unit/Makefile +++ b/unit/Makefile @@ -85,7 +85,9 @@ SRC += analyses/ai/ai.cpp \ solvers/sat/satcheck_cadical.cpp \ solvers/sat/satcheck_minisat2.cpp \ solvers/smt2/smt2_conv.cpp \ + solvers/smt2_incremental/smt_bit_vector_theory.cpp \ solvers/smt2_incremental/smt_commands.cpp \ + solvers/smt2_incremental/smt_core_theory.cpp \ solvers/smt2_incremental/smt_sorts.cpp \ solvers/smt2_incremental/smt_terms.cpp \ solvers/smt2_incremental/smt_to_smt2_string.cpp \ diff --git a/unit/solvers/smt2_incremental/smt_bit_vector_theory.cpp b/unit/solvers/smt2_incremental/smt_bit_vector_theory.cpp new file mode 100644 index 00000000000..3f0207c8857 --- /dev/null +++ b/unit/solvers/smt2_incremental/smt_bit_vector_theory.cpp @@ -0,0 +1,168 @@ +// Author: Diffblue Ltd. + +#include + +#include +#include + +#include + +TEST_CASE("SMT bit vector predicates", "[core][smt2_incremental]") +{ + const smt_bit_vector_constant_termt two{2, 8}; + const smt_bit_vector_constant_termt three{3, 8}; + const smt_bool_literal_termt false_term{false}; + const smt_bit_vector_constant_termt wider{2, 16}; + SECTION("unsigned less than") + { + const auto function_application = + smt_bit_vector_theoryt::unsigned_less_than(two, three); + REQUIRE( + function_application.function_identifier() == + smt_identifier_termt("bvult", smt_bool_sortt{})); + REQUIRE(function_application.get_sort() == smt_bool_sortt{}); + REQUIRE(function_application.arguments().size() == 2); + REQUIRE(function_application.arguments()[0].get() == two); + REQUIRE(function_application.arguments()[1].get() == three); + cbmc_invariants_should_throwt invariants_throw; + CHECK_THROWS(smt_bit_vector_theoryt::unsigned_less_than(false_term, two)); + CHECK_THROWS(smt_bit_vector_theoryt::unsigned_less_than(two, false_term)); + CHECK_THROWS(smt_bit_vector_theoryt::unsigned_less_than(wider, two)); + CHECK_THROWS(smt_bit_vector_theoryt::unsigned_less_than(two, wider)); + } + SECTION("unsigned less than or equal") + { + const auto function_application = + smt_bit_vector_theoryt::unsigned_less_than_or_equal(two, three); + REQUIRE( + function_application.function_identifier() == + smt_identifier_termt("bvule", smt_bool_sortt{})); + REQUIRE(function_application.get_sort() == smt_bool_sortt{}); + REQUIRE(function_application.arguments().size() == 2); + REQUIRE(function_application.arguments()[0].get() == two); + REQUIRE(function_application.arguments()[1].get() == three); + cbmc_invariants_should_throwt invariants_throw; + CHECK_THROWS( + smt_bit_vector_theoryt::unsigned_less_than_or_equal(false_term, two)); + CHECK_THROWS( + smt_bit_vector_theoryt::unsigned_less_than_or_equal(two, false_term)); + CHECK_THROWS( + smt_bit_vector_theoryt::unsigned_less_than_or_equal(wider, two)); + CHECK_THROWS( + smt_bit_vector_theoryt::unsigned_less_than_or_equal(two, wider)); + } + SECTION("unsigned greater than") + { + const auto function_application = + smt_bit_vector_theoryt::unsigned_greater_than(two, three); + REQUIRE( + function_application.function_identifier() == + smt_identifier_termt("bvugt", smt_bool_sortt{})); + REQUIRE(function_application.get_sort() == smt_bool_sortt{}); + REQUIRE(function_application.arguments().size() == 2); + REQUIRE(function_application.arguments()[0].get() == two); + REQUIRE(function_application.arguments()[1].get() == three); + cbmc_invariants_should_throwt invariants_throw; + CHECK_THROWS( + smt_bit_vector_theoryt::unsigned_greater_than(false_term, two)); + CHECK_THROWS( + smt_bit_vector_theoryt::unsigned_greater_than(two, false_term)); + CHECK_THROWS(smt_bit_vector_theoryt::unsigned_greater_than(wider, two)); + CHECK_THROWS(smt_bit_vector_theoryt::unsigned_greater_than(two, wider)); + } + SECTION("unsigned greater than or equal") + { + const auto function_application = + smt_bit_vector_theoryt::unsigned_greater_than_or_equal(two, three); + REQUIRE( + function_application.function_identifier() == + smt_identifier_termt("bvuge", smt_bool_sortt{})); + REQUIRE(function_application.get_sort() == smt_bool_sortt{}); + REQUIRE(function_application.arguments().size() == 2); + REQUIRE(function_application.arguments()[0].get() == two); + REQUIRE(function_application.arguments()[1].get() == three); + cbmc_invariants_should_throwt invariants_throw; + CHECK_THROWS( + smt_bit_vector_theoryt::unsigned_greater_than_or_equal(false_term, two)); + CHECK_THROWS( + smt_bit_vector_theoryt::unsigned_greater_than_or_equal(two, false_term)); + CHECK_THROWS( + smt_bit_vector_theoryt::unsigned_greater_than_or_equal(wider, two)); + CHECK_THROWS( + smt_bit_vector_theoryt::unsigned_greater_than_or_equal(two, wider)); + } + SECTION("signed less than") + { + const auto function_application = + smt_bit_vector_theoryt::signed_less_than(two, three); + REQUIRE( + function_application.function_identifier() == + smt_identifier_termt("bvslt", smt_bool_sortt{})); + REQUIRE(function_application.get_sort() == smt_bool_sortt{}); + REQUIRE(function_application.arguments().size() == 2); + REQUIRE(function_application.arguments()[0].get() == two); + REQUIRE(function_application.arguments()[1].get() == three); + cbmc_invariants_should_throwt invariants_throw; + CHECK_THROWS(smt_bit_vector_theoryt::signed_less_than(false_term, two)); + CHECK_THROWS(smt_bit_vector_theoryt::signed_less_than(two, false_term)); + CHECK_THROWS(smt_bit_vector_theoryt::signed_less_than(wider, two)); + CHECK_THROWS(smt_bit_vector_theoryt::signed_less_than(two, wider)); + } + SECTION("signed less than or equal") + { + const auto function_application = + smt_bit_vector_theoryt::signed_less_than_or_equal(two, three); + REQUIRE( + function_application.function_identifier() == + smt_identifier_termt("bvsle", smt_bool_sortt{})); + REQUIRE(function_application.get_sort() == smt_bool_sortt{}); + REQUIRE(function_application.arguments().size() == 2); + REQUIRE(function_application.arguments()[0].get() == two); + REQUIRE(function_application.arguments()[1].get() == three); + cbmc_invariants_should_throwt invariants_throw; + CHECK_THROWS( + smt_bit_vector_theoryt::signed_less_than_or_equal(false_term, two)); + CHECK_THROWS( + smt_bit_vector_theoryt::signed_less_than_or_equal(two, false_term)); + CHECK_THROWS(smt_bit_vector_theoryt::signed_less_than_or_equal(wider, two)); + CHECK_THROWS(smt_bit_vector_theoryt::signed_less_than_or_equal(two, wider)); + } + SECTION("signed greater than") + { + const auto function_application = + smt_bit_vector_theoryt::signed_greater_than(two, three); + REQUIRE( + function_application.function_identifier() == + smt_identifier_termt("bvsgt", smt_bool_sortt{})); + REQUIRE(function_application.get_sort() == smt_bool_sortt{}); + REQUIRE(function_application.arguments().size() == 2); + REQUIRE(function_application.arguments()[0].get() == two); + REQUIRE(function_application.arguments()[1].get() == three); + cbmc_invariants_should_throwt invariants_throw; + CHECK_THROWS(smt_bit_vector_theoryt::signed_greater_than(false_term, two)); + CHECK_THROWS(smt_bit_vector_theoryt::signed_greater_than(two, false_term)); + CHECK_THROWS(smt_bit_vector_theoryt::signed_greater_than(wider, two)); + CHECK_THROWS(smt_bit_vector_theoryt::signed_greater_than(two, wider)); + } + SECTION("signed greater than or equal") + { + const auto function_application = + smt_bit_vector_theoryt::signed_greater_than_or_equal(two, three); + REQUIRE( + function_application.function_identifier() == + smt_identifier_termt("bvsge", smt_bool_sortt{})); + REQUIRE(function_application.get_sort() == smt_bool_sortt{}); + REQUIRE(function_application.arguments().size() == 2); + REQUIRE(function_application.arguments()[0].get() == two); + REQUIRE(function_application.arguments()[1].get() == three); + cbmc_invariants_should_throwt invariants_throw; + CHECK_THROWS( + smt_bit_vector_theoryt::signed_greater_than_or_equal(false_term, two)); + CHECK_THROWS( + smt_bit_vector_theoryt::signed_greater_than_or_equal(two, false_term)); + CHECK_THROWS( + smt_bit_vector_theoryt::signed_greater_than_or_equal(wider, two)); + CHECK_THROWS( + smt_bit_vector_theoryt::signed_greater_than_or_equal(two, wider)); + } +} diff --git a/unit/solvers/smt2_incremental/smt_commands.cpp b/unit/solvers/smt2_incremental/smt_commands.cpp index 510574d7fae..29f0b992fea 100644 --- a/unit/solvers/smt2_incremental/smt_commands.cpp +++ b/unit/solvers/smt2_incremental/smt_commands.cpp @@ -3,6 +3,7 @@ #include #include +#include TEST_CASE("Test smt_commandt.pretty is accessible.", "[core][smt2_incremental]") { @@ -32,11 +33,13 @@ TEST_CASE("smt_declare_function_commandt getters", "[core][smt2_incremental]") TEST_CASE("smt_define_function_commandt getters", "[core][smt2_incremental]") { + const auto not_x = + smt_core_theoryt::make_not(smt_identifier_termt{"x", smt_bool_sortt{}}); const smt_define_function_commandt function_definition{ "not first", {smt_identifier_termt{"x", smt_bool_sortt{}}, smt_identifier_termt{"y", smt_bool_sortt{}}}, - smt_not_termt{smt_identifier_termt{"x", smt_bool_sortt{}}}}; + not_x}; CHECK( function_definition.identifier() == smt_identifier_termt{"not first", smt_bool_sortt{}}); @@ -46,9 +49,7 @@ TEST_CASE("smt_define_function_commandt getters", "[core][smt2_incremental]") CHECK( function_definition.parameters()[1].get() == smt_identifier_termt{"y", smt_bool_sortt{}}); - CHECK( - function_definition.definition() == - smt_not_termt{smt_identifier_termt{"x", smt_bool_sortt{}}}); + CHECK(function_definition.definition() == not_x); } TEST_CASE("smt_get_value_commandt getter", "[core][smt2_incremental]") @@ -94,3 +95,20 @@ 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_bool_sortt{}, smt_bool_sortt{}}}; + const smt_function_application_termt::factoryt factory{ + function_declaration}; + const smt_function_application_termt application = + factory(std::vector{smt_bool_literal_termt{true}, + smt_bool_literal_termt{false}}); + CHECK(application.get_sort() == smt_bool_sortt{}); + CHECK(application.function_identifier() == arbitary); + REQUIRE(application.arguments().size() == 2); + CHECK(application.arguments()[0].get() == smt_bool_literal_termt{true}); + CHECK(application.arguments()[1].get() == smt_bool_literal_termt{false}); +} diff --git a/unit/solvers/smt2_incremental/smt_core_theory.cpp b/unit/solvers/smt2_incremental/smt_core_theory.cpp new file mode 100644 index 00000000000..c51603c4d17 --- /dev/null +++ b/unit/solvers/smt2_incremental/smt_core_theory.cpp @@ -0,0 +1,198 @@ +// Author: Diffblue Ltd. + +#include + +#include +#include + +#include + +TEST_CASE("SMT core theory \"not\".", "[core][smt2_incremental]") +{ + const smt_bool_literal_termt operand{true}; + const auto not_term = smt_core_theoryt::make_not(operand); + + CHECK(not_term.get_sort() == smt_bool_sortt{}); + CHECK( + not_term.function_identifier() == + smt_identifier_termt{"not", smt_bool_sortt{}}); + REQUIRE(not_term.arguments().size() == 1); + REQUIRE(not_term.arguments()[0].get() == operand); + cbmc_invariants_should_throwt invariants_throw; + CHECK_THROWS(smt_core_theoryt::make_not(smt_bit_vector_constant_termt{0, 1})); +} + +TEST_CASE("SMT core theory implies.", "[core][smt2_incremental]") +{ + const smt_bool_literal_termt true_term{true}; + const smt_bool_literal_termt false_term{false}; + const auto implies = smt_core_theoryt::implies(true_term, false_term); + CHECK(implies.get_sort() == smt_bool_sortt{}); + CHECK( + implies.function_identifier() == + smt_identifier_termt{"=>", smt_bool_sortt{}}); + REQUIRE(implies.arguments().size() == 2); + CHECK(implies.arguments()[0].get() == true_term); + CHECK(implies.arguments()[1].get() == false_term); + cbmc_invariants_should_throwt invariants_throw; + const smt_bit_vector_constant_termt two{2, 8}; + CHECK_THROWS(smt_core_theoryt::implies(two, false_term)); + CHECK_THROWS(smt_core_theoryt::implies(true_term, two)); +} + +TEST_CASE("SMT core theory \"and\".", "[core][smt2_incremental]") +{ + const smt_bool_literal_termt true_term{true}; + const smt_bool_literal_termt false_term{false}; + const auto implies = smt_core_theoryt::make_and(true_term, false_term); + CHECK(implies.get_sort() == smt_bool_sortt{}); + CHECK( + implies.function_identifier() == + smt_identifier_termt{"and", smt_bool_sortt{}}); + REQUIRE(implies.arguments().size() == 2); + CHECK(implies.arguments()[0].get() == true_term); + CHECK(implies.arguments()[1].get() == false_term); + cbmc_invariants_should_throwt invariants_throw; + const smt_bit_vector_constant_termt two{2, 8}; + CHECK_THROWS(smt_core_theoryt::make_and(two, false_term)); + CHECK_THROWS(smt_core_theoryt::make_and(true_term, two)); +} + +TEST_CASE("SMT core theory \"or\".", "[core][smt2_incremental]") +{ + const smt_bool_literal_termt true_term{true}; + const smt_bool_literal_termt false_term{false}; + const auto implies = smt_core_theoryt::make_or(true_term, false_term); + CHECK(implies.get_sort() == smt_bool_sortt{}); + CHECK( + implies.function_identifier() == + smt_identifier_termt{"or", smt_bool_sortt{}}); + REQUIRE(implies.arguments().size() == 2); + CHECK(implies.arguments()[0].get() == true_term); + CHECK(implies.arguments()[1].get() == false_term); + cbmc_invariants_should_throwt invariants_throw; + const smt_bit_vector_constant_termt two{2, 8}; + CHECK_THROWS(smt_core_theoryt::make_or(two, false_term)); + CHECK_THROWS(smt_core_theoryt::make_or(true_term, two)); +} + +TEST_CASE("SMT core theory \"xor\".", "[core][smt2_incremental]") +{ + const smt_bool_literal_termt true_term{true}; + const smt_bool_literal_termt false_term{false}; + const auto implies = smt_core_theoryt::make_xor(true_term, false_term); + CHECK(implies.get_sort() == smt_bool_sortt{}); + CHECK( + implies.function_identifier() == + smt_identifier_termt{"xor", smt_bool_sortt{}}); + REQUIRE(implies.arguments().size() == 2); + CHECK(implies.arguments()[0].get() == true_term); + CHECK(implies.arguments()[1].get() == false_term); + cbmc_invariants_should_throwt invariants_throw; + const smt_bit_vector_constant_termt two{2, 8}; + CHECK_THROWS(smt_core_theoryt::make_xor(two, false_term)); + CHECK_THROWS(smt_core_theoryt::make_xor(true_term, two)); +} + +TEST_CASE("SMT core theory \"=\".", "[core][smt2_incremental]") +{ + SECTION("Bool sorted term comparison") + { + const smt_bool_literal_termt true_term{true}; + const smt_bool_literal_termt false_term{false}; + const auto bool_comparison = smt_core_theoryt::equal(true_term, false_term); + CHECK(bool_comparison.get_sort() == smt_bool_sortt{}); + CHECK( + bool_comparison.function_identifier() == + smt_identifier_termt{"=", smt_bool_sortt{}}); + REQUIRE(bool_comparison.arguments().size() == 2); + REQUIRE(bool_comparison.arguments()[0].get() == true_term); + REQUIRE(bool_comparison.arguments()[1].get() == false_term); + } + + SECTION("Bit vector sorted term comparison") + { + const smt_bit_vector_constant_termt two{2, 8}; + const smt_bit_vector_constant_termt three{3, 8}; + const auto bit_vector_comparison = smt_core_theoryt::equal(two, three); + CHECK(bit_vector_comparison.get_sort() == smt_bool_sortt{}); + CHECK( + bit_vector_comparison.function_identifier() == + smt_identifier_termt{"=", smt_bool_sortt{}}); + REQUIRE(bit_vector_comparison.arguments().size() == 2); + REQUIRE(bit_vector_comparison.arguments()[0].get() == two); + REQUIRE(bit_vector_comparison.arguments()[1].get() == three); + } + + SECTION("Mismatch sort invariant") + { + cbmc_invariants_should_throwt invariants_throw; + CHECK_THROWS(smt_core_theoryt::equal( + smt_bit_vector_constant_termt{2, 8}, + smt_bit_vector_constant_termt{2, 16})); + CHECK_THROWS(smt_core_theoryt::equal( + smt_bit_vector_constant_termt{2, 8}, smt_bool_literal_termt{true})); + } +} + +TEST_CASE("SMT core theory \"distinct\".", "[core][smt2_incremental]") +{ + SECTION("Bool sorted term comparison") + { + const smt_bool_literal_termt true_term{true}; + const smt_bool_literal_termt false_term{false}; + const auto bool_comparison = + smt_core_theoryt::distinct(true_term, false_term); + CHECK(bool_comparison.get_sort() == smt_bool_sortt{}); + CHECK( + bool_comparison.function_identifier() == + smt_identifier_termt{"distinct", smt_bool_sortt{}}); + REQUIRE(bool_comparison.arguments().size() == 2); + REQUIRE(bool_comparison.arguments()[0].get() == true_term); + REQUIRE(bool_comparison.arguments()[1].get() == false_term); + } + + SECTION("Bit vector sorted term comparison") + { + const smt_bit_vector_constant_termt two{2, 8}; + const smt_bit_vector_constant_termt three{3, 8}; + const auto bit_vector_comparison = smt_core_theoryt::distinct(two, three); + CHECK(bit_vector_comparison.get_sort() == smt_bool_sortt{}); + CHECK( + bit_vector_comparison.function_identifier() == + smt_identifier_termt{"distinct", smt_bool_sortt{}}); + REQUIRE(bit_vector_comparison.arguments().size() == 2); + REQUIRE(bit_vector_comparison.arguments()[0].get() == two); + REQUIRE(bit_vector_comparison.arguments()[1].get() == three); + } + + SECTION("Mismatch sort invariant") + { + cbmc_invariants_should_throwt invariants_throw; + CHECK_THROWS(smt_core_theoryt::distinct( + smt_bit_vector_constant_termt{2, 8}, + smt_bit_vector_constant_termt{2, 16})); + CHECK_THROWS(smt_core_theoryt::distinct( + smt_bit_vector_constant_termt{2, 8}, smt_bool_literal_termt{true})); + } +} + +TEST_CASE("SMT core theory if then else.", "[core][smt2_incremental]") +{ + const smt_bool_literal_termt false_term{false}; + const smt_bit_vector_constant_termt two{2, 8}; + const smt_bit_vector_constant_termt three{2, 8}; + const auto if_then_else = + smt_core_theoryt::if_then_else(false_term, two, three); + CHECK(if_then_else.get_sort() == smt_bit_vector_sortt{8}); + CHECK( + if_then_else.function_identifier() == + smt_identifier_termt{"ite", smt_bit_vector_sortt{8}}); + REQUIRE(if_then_else.arguments().size() == 3); + CHECK(if_then_else.arguments()[0].get() == false_term); + CHECK(if_then_else.arguments()[1].get() == two); + CHECK(if_then_else.arguments()[2].get() == three); + cbmc_invariants_should_throwt invariants_throw; + CHECK_THROWS(smt_core_theoryt::if_then_else(two, two, three)); + CHECK_THROWS(smt_core_theoryt::if_then_else(false_term, false_term, three)); +} diff --git a/unit/solvers/smt2_incremental/smt_terms.cpp b/unit/solvers/smt2_incremental/smt_terms.cpp index 5dd48356d89..94f87b9e481 100644 --- a/unit/solvers/smt2_incremental/smt_terms.cpp +++ b/unit/solvers/smt2_incremental/smt_terms.cpp @@ -2,6 +2,7 @@ #include +#include #include #include @@ -33,19 +34,6 @@ TEST_CASE( REQUIRE_FALSE(smt_bool_literal_termt{false}.value()); } -TEST_CASE("smt_not_termt sort.", "[core][smt2_incremental]") -{ - REQUIRE( - smt_not_termt{smt_bool_literal_termt{true}}.get_sort() == smt_bool_sortt{}); -} - -TEST_CASE("smt_not_termt operand getter.", "[core][smt2_incremental]") -{ - const smt_bool_literal_termt bool_term{true}; - const smt_not_termt not_term{bool_term}; - REQUIRE(not_term.operand() == bool_term); -} - TEST_CASE("smt_identifier_termt construction", "[core][smt2_incremental]") { cbmc_invariants_should_throwt invariants_throw; @@ -78,11 +66,6 @@ TEST_CASE("smt_termt equality.", "[core][smt2_incremental]") CHECK( smt_bit_vector_constant_termt{42, 8} != smt_bit_vector_constant_termt{12, 8}); - smt_termt not_false = smt_not_termt{smt_bool_literal_termt{false}}; - smt_termt not_true = smt_not_termt{smt_bool_literal_termt{true}}; - CHECK_FALSE(not_false == true_term); - CHECK_FALSE(not_false == not_true); - CHECK(not_false == smt_not_termt{smt_bool_literal_termt{false}}); } template @@ -104,18 +87,6 @@ class term_visit_type_checkert final : public smt_term_const_downcast_visitort } } - void visit(const smt_not_termt &) override - { - if(std::is_same::value) - { - expected_term_visited = true; - } - else - { - unexpected_term_visited = true; - } - } - void visit(const smt_identifier_termt &) override { if(std::is_same::value) @@ -162,12 +133,6 @@ smt_bool_literal_termt make_test_term() return smt_bool_literal_termt{false}; } -template <> -smt_not_termt make_test_term() -{ - return smt_not_termt{smt_bool_literal_termt{false}}; -} - template <> smt_identifier_termt make_test_term() { @@ -183,15 +148,13 @@ smt_bit_vector_constant_termt make_test_term() template <> smt_function_application_termt make_test_term() { - 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( "smt_termt::accept(visitor)", "[core][smt2_incremental]", smt_bool_literal_termt, - smt_not_termt, smt_identifier_termt, smt_bit_vector_constant_termt, smt_function_application_termt) diff --git a/unit/solvers/smt2_incremental/smt_to_smt2_string.cpp b/unit/solvers/smt2_incremental/smt_to_smt2_string.cpp index 9d4b689417d..2ed9c9d86bc 100644 --- a/unit/solvers/smt2_incremental/smt_to_smt2_string.cpp +++ b/unit/solvers/smt2_incremental/smt_to_smt2_string.cpp @@ -3,6 +3,7 @@ #include #include +#include #include #include #include @@ -16,13 +17,6 @@ TEST_CASE("Test smt_sortt to string conversion", "[core][smt2_incremental]") CHECK(smt_to_smt2_string(smt_bit_vector_sortt{16}) == "(_ BitVec 16)"); } -TEST_CASE("Test smt_not_termt to string conversion", "[core][smt2_incremental]") -{ - CHECK( - smt_to_smt2_string(smt_not_termt{ - smt_identifier_termt{"foo", smt_bool_sortt{}}}) == "(not |foo|)"); -} - TEST_CASE( "Test smt_bit_vector_constant_termt to string conversion", "[core][smt2_incremental]") @@ -43,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|)"); } @@ -109,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|))"); }