From 6fcc3684d3efd889fc57b984e571120d1141dd16 Mon Sep 17 00:00:00 2001 From: Thomas Spriggs Date: Fri, 30 Jul 2021 10:55:00 +0100 Subject: [PATCH 01/10] Add sort casting For checking parameterised sorts. --- src/solvers/smt2_incremental/smt_sorts.cpp | 23 ++++++++++++++++++++++ src/solvers/smt2_incremental/smt_sorts.h | 7 +++++++ 2 files changed, 30 insertions(+) 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; }; From f5d4d3082eae96f8412cc97fc4d7f3125a70b896 Mon Sep 17 00:00:00 2001 From: Thomas Spriggs Date: Fri, 30 Jul 2021 10:55:01 +0100 Subject: [PATCH 02/10] Add parameterised function application factory So that function specific INVARIANTS can be checked. --- src/solvers/smt2_incremental/smt_commands.cpp | 48 +++++++++++++++++++ src/solvers/smt2_incremental/smt_commands.h | 18 +++++++ src/solvers/smt2_incremental/smt_terms.h | 28 +++++++++++ .../solvers/smt2_incremental/smt_commands.cpp | 17 +++++++ 4 files changed, 111 insertions(+) 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_terms.h b/src/solvers/smt2_incremental/smt_terms.h index f6b4d611a1e..6afe158cd85 100644 --- a/src/solvers/smt2_incremental/smt_terms.h +++ b/src/solvers/smt2_incremental/smt_terms.h @@ -121,11 +121,39 @@ 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. smt_function_application_termt( smt_identifier_termt function_identifier, std::vector arguments); 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/unit/solvers/smt2_incremental/smt_commands.cpp b/unit/solvers/smt2_incremental/smt_commands.cpp index 510574d7fae..d0d414dc1aa 100644 --- a/unit/solvers/smt2_incremental/smt_commands.cpp +++ b/unit/solvers/smt2_incremental/smt_commands.cpp @@ -94,3 +94,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}); +} From c44f4b04a51a9497d821ad0c1f5b9a175521ad7f Mon Sep 17 00:00:00 2001 From: Thomas Spriggs Date: Fri, 30 Jul 2021 10:55:02 +0100 Subject: [PATCH 03/10] Add bitvector theory predicates --- src/solvers/Makefile | 1 + .../smt_bit_vector_theory.cpp | 44 +++++ .../smt_bit_vector_theory.def | 13 ++ .../smt2_incremental/smt_bit_vector_theory.h | 25 +++ unit/Makefile | 1 + .../smt_bit_vector_theory.cpp | 168 ++++++++++++++++++ 6 files changed, 252 insertions(+) create mode 100644 src/solvers/smt2_incremental/smt_bit_vector_theory.cpp create mode 100644 src/solvers/smt2_incremental/smt_bit_vector_theory.def create mode 100644 src/solvers/smt2_incremental/smt_bit_vector_theory.h create mode 100644 unit/solvers/smt2_incremental/smt_bit_vector_theory.cpp diff --git a/src/solvers/Makefile b/src/solvers/Makefile index 6b6edee3a4e..d707d6660fb 100644 --- a/src/solvers/Makefile +++ b/src/solvers/Makefile @@ -192,6 +192,7 @@ 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_logics.cpp \ smt2_incremental/smt_options.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/unit/Makefile b/unit/Makefile index 4e730e7dc5f..9b4229c61cb 100644 --- a/unit/Makefile +++ b/unit/Makefile @@ -85,6 +85,7 @@ 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_sorts.cpp \ solvers/smt2_incremental/smt_terms.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)); + } +} From 9025514ac2d86374de0ef7eafe1a20e6e30e29b3 Mon Sep 17 00:00:00 2001 From: Thomas Spriggs Date: Fri, 30 Jul 2021 10:55:04 +0100 Subject: [PATCH 04/10] Refactor `smt_not_term` into core theory For consistency with how the functions for the bit vector theory are defined. Note that the factory is called `make_not` rather than `not`, because not is a keyword in C++ which is equivalent to the `!` operator. --- src/solvers/Makefile | 1 + .../smt2_incremental/smt_core_theory.cpp | 23 ++++++++++++ .../smt2_incremental/smt_core_theory.h | 20 ++++++++++ src/solvers/smt2_incremental/smt_terms.cpp | 14 ------- src/solvers/smt2_incremental/smt_terms.def | 1 - src/solvers/smt2_incremental/smt_terms.h | 7 ---- .../smt2_incremental/smt_to_smt2_string.cpp | 6 --- unit/Makefile | 1 + .../solvers/smt2_incremental/smt_commands.cpp | 9 +++-- .../smt2_incremental/smt_core_theory.cpp | 23 ++++++++++++ unit/solvers/smt2_incremental/smt_terms.cpp | 37 ------------------- .../smt2_incremental/smt_to_smt2_string.cpp | 7 ---- 12 files changed, 73 insertions(+), 76 deletions(-) create mode 100644 src/solvers/smt2_incremental/smt_core_theory.cpp create mode 100644 src/solvers/smt2_incremental/smt_core_theory.h create mode 100644 unit/solvers/smt2_incremental/smt_core_theory.cpp diff --git a/src/solvers/Makefile b/src/solvers/Makefile index d707d6660fb..6c87438ad56 100644 --- a/src/solvers/Makefile +++ b/src/solvers/Makefile @@ -194,6 +194,7 @@ SRC = $(BOOLEFORCE_SRC) \ 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_core_theory.cpp b/src/solvers/smt2_incremental/smt_core_theory.cpp new file mode 100644 index 00000000000..9517c7f0ca3 --- /dev/null +++ b/src/solvers/smt2_incremental/smt_core_theory.cpp @@ -0,0 +1,23 @@ +// 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{}; 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..60e39f48917 --- /dev/null +++ b/src/solvers/smt2_incremental/smt_core_theory.h @@ -0,0 +1,20 @@ +// 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; +}; + +#endif // CPROVER_SOLVERS_SMT2_INCREMENTAL_SMT_CORE_THEORY_H 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 6afe158cd85..c5937affaef 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 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 9b4229c61cb..572d8cf22b4 100644 --- a/unit/Makefile +++ b/unit/Makefile @@ -87,6 +87,7 @@ SRC += analyses/ai/ai.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_commands.cpp b/unit/solvers/smt2_incremental/smt_commands.cpp index d0d414dc1aa..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]") 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..f1cdd272bf6 --- /dev/null +++ b/unit/solvers/smt2_incremental/smt_core_theory.cpp @@ -0,0 +1,23 @@ +// 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})); +} diff --git a/unit/solvers/smt2_incremental/smt_terms.cpp b/unit/solvers/smt2_incremental/smt_terms.cpp index 5dd48356d89..6da7001e915 100644 --- a/unit/solvers/smt2_incremental/smt_terms.cpp +++ b/unit/solvers/smt2_incremental/smt_terms.cpp @@ -33,19 +33,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 +65,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 +86,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 +132,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() { @@ -191,7 +155,6 @@ 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..f1f07740c33 100644 --- a/unit/solvers/smt2_incremental/smt_to_smt2_string.cpp +++ b/unit/solvers/smt2_incremental/smt_to_smt2_string.cpp @@ -16,13 +16,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]") From 5b5aabc7a96201dcd5173d3d5649ed3baeb3336b Mon Sep 17 00:00:00 2001 From: Thomas Spriggs Date: Fri, 30 Jul 2021 15:48:46 +0100 Subject: [PATCH 05/10] Add `equal` to smt core theory --- .../smt2_incremental/smt_core_theory.cpp | 23 +++++++++++ .../smt2_incremental/smt_core_theory.h | 8 ++++ .../smt2_incremental/smt_core_theory.cpp | 41 +++++++++++++++++++ 3 files changed, 72 insertions(+) diff --git a/src/solvers/smt2_incremental/smt_core_theory.cpp b/src/solvers/smt2_incremental/smt_core_theory.cpp index 9517c7f0ca3..e32a56bf719 100644 --- a/src/solvers/smt2_incremental/smt_core_theory.cpp +++ b/src/solvers/smt2_incremental/smt_core_theory.cpp @@ -21,3 +21,26 @@ void smt_core_theoryt::nott::validate(const smt_termt &operand) const smt_function_application_termt::factoryt smt_core_theoryt::make_not{}; + +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{}; diff --git a/src/solvers/smt2_incremental/smt_core_theory.h b/src/solvers/smt2_incremental/smt_core_theory.h index 60e39f48917..391c307fa6f 100644 --- a/src/solvers/smt2_incremental/smt_core_theory.h +++ b/src/solvers/smt2_incremental/smt_core_theory.h @@ -15,6 +15,14 @@ class smt_core_theoryt static void validate(const smt_termt &operand); }; static const smt_function_application_termt::factoryt make_not; + + 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; }; #endif // CPROVER_SOLVERS_SMT2_INCREMENTAL_SMT_CORE_THEORY_H diff --git a/unit/solvers/smt2_incremental/smt_core_theory.cpp b/unit/solvers/smt2_incremental/smt_core_theory.cpp index f1cdd272bf6..eeaaaf665fc 100644 --- a/unit/solvers/smt2_incremental/smt_core_theory.cpp +++ b/unit/solvers/smt2_incremental/smt_core_theory.cpp @@ -21,3 +21,44 @@ TEST_CASE("SMT core theory \"not\".", "[core][smt2_incremental]") 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 \"=\".", "[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})); + } +} From 01f4b18e240d70aeab624f8edfe888d724d95951 Mon Sep 17 00:00:00 2001 From: Thomas Spriggs Date: Fri, 30 Jul 2021 10:55:06 +0100 Subject: [PATCH 06/10] 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. --- src/solvers/smt2_incremental/smt_terms.h | 10 ++++++---- unit/solvers/smt2_incremental/smt_terms.cpp | 4 ++-- .../solvers/smt2_incremental/smt_to_smt2_string.cpp | 13 +++++-------- 3 files changed, 13 insertions(+), 14 deletions(-) diff --git a/src/solvers/smt2_incremental/smt_terms.h b/src/solvers/smt2_incremental/smt_terms.h index c5937affaef..0925c598c4a 100644 --- a/src/solvers/smt2_incremental/smt_terms.h +++ b/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 arguments); + +public: const smt_identifier_termt &function_identifier() const; std::vector> arguments() const; diff --git a/unit/solvers/smt2_incremental/smt_terms.cpp b/unit/solvers/smt2_incremental/smt_terms.cpp index 6da7001e915..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 @@ -147,8 +148,7 @@ 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( diff --git a/unit/solvers/smt2_incremental/smt_to_smt2_string.cpp b/unit/solvers/smt2_incremental/smt_to_smt2_string.cpp index f1f07740c33..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 @@ -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|))"); } From aea57ed6977302476f557bee35a99b03e9c2b5d3 Mon Sep 17 00:00:00 2001 From: Thomas Spriggs Date: Fri, 30 Jul 2021 10:55:08 +0100 Subject: [PATCH 07/10] Add SMT2 core theory "distinct" --- .../smt2_incremental/smt_core_theory.cpp | 23 ++++++++++ .../smt2_incremental/smt_core_theory.h | 8 ++++ .../smt2_incremental/smt_core_theory.cpp | 42 +++++++++++++++++++ 3 files changed, 73 insertions(+) diff --git a/src/solvers/smt2_incremental/smt_core_theory.cpp b/src/solvers/smt2_incremental/smt_core_theory.cpp index e32a56bf719..d65381e38f7 100644 --- a/src/solvers/smt2_incremental/smt_core_theory.cpp +++ b/src/solvers/smt2_incremental/smt_core_theory.cpp @@ -44,3 +44,26 @@ void smt_core_theoryt::equalt::validate( 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{}; diff --git a/src/solvers/smt2_incremental/smt_core_theory.h b/src/solvers/smt2_incremental/smt_core_theory.h index 391c307fa6f..d6b655c47fe 100644 --- a/src/solvers/smt2_incremental/smt_core_theory.h +++ b/src/solvers/smt2_incremental/smt_core_theory.h @@ -23,6 +23,14 @@ class smt_core_theoryt 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; }; #endif // CPROVER_SOLVERS_SMT2_INCREMENTAL_SMT_CORE_THEORY_H diff --git a/unit/solvers/smt2_incremental/smt_core_theory.cpp b/unit/solvers/smt2_incremental/smt_core_theory.cpp index eeaaaf665fc..045b9ced602 100644 --- a/unit/solvers/smt2_incremental/smt_core_theory.cpp +++ b/unit/solvers/smt2_incremental/smt_core_theory.cpp @@ -62,3 +62,45 @@ TEST_CASE("SMT core theory \"=\".", "[core][smt2_incremental]") 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})); + } +} From cf23d63b8a2a0071a8a93c214e36710af2ce259a Mon Sep 17 00:00:00 2001 From: Thomas Spriggs Date: Fri, 30 Jul 2021 10:55:09 +0100 Subject: [PATCH 08/10] Add core theory "if then else" operation --- .../smt2_incremental/smt_core_theory.cpp | 29 +++++++++++++++++++ .../smt2_incremental/smt_core_theory.h | 15 ++++++++++ .../smt2_incremental/smt_core_theory.cpp | 20 +++++++++++++ 3 files changed, 64 insertions(+) diff --git a/src/solvers/smt2_incremental/smt_core_theory.cpp b/src/solvers/smt2_incremental/smt_core_theory.cpp index d65381e38f7..3d31679a8f8 100644 --- a/src/solvers/smt2_incremental/smt_core_theory.cpp +++ b/src/solvers/smt2_incremental/smt_core_theory.cpp @@ -67,3 +67,32 @@ void smt_core_theoryt::distinctt::validate( 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 index d6b655c47fe..0807006e0b5 100644 --- a/src/solvers/smt2_incremental/smt_core_theory.h +++ b/src/solvers/smt2_incremental/smt_core_theory.h @@ -31,6 +31,21 @@ class smt_core_theoryt 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/unit/solvers/smt2_incremental/smt_core_theory.cpp b/unit/solvers/smt2_incremental/smt_core_theory.cpp index 045b9ced602..885f857208d 100644 --- a/unit/solvers/smt2_incremental/smt_core_theory.cpp +++ b/unit/solvers/smt2_incremental/smt_core_theory.cpp @@ -104,3 +104,23 @@ TEST_CASE("SMT core theory \"distinct\".", "[core][smt2_incremental]") 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)); +} From 2f09110cc5ac6cb47cbc77ede274e42d8be1c820 Mon Sep 17 00:00:00 2001 From: Thomas Spriggs Date: Fri, 30 Jul 2021 10:55:10 +0100 Subject: [PATCH 09/10] Add core theory "implies" operation --- .../smt2_incremental/smt_core_theory.cpp | 26 +++++++++++++++++++ .../smt2_incremental/smt_core_theory.h | 8 ++++++ .../smt2_incremental/smt_core_theory.cpp | 18 +++++++++++++ 3 files changed, 52 insertions(+) diff --git a/src/solvers/smt2_incremental/smt_core_theory.cpp b/src/solvers/smt2_incremental/smt_core_theory.cpp index 3d31679a8f8..e9c63b33e0b 100644 --- a/src/solvers/smt2_incremental/smt_core_theory.cpp +++ b/src/solvers/smt2_incremental/smt_core_theory.cpp @@ -22,6 +22,32 @@ void smt_core_theoryt::nott::validate(const smt_termt &operand) 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::equalt::identifier() { return "="; diff --git a/src/solvers/smt2_incremental/smt_core_theory.h b/src/solvers/smt2_incremental/smt_core_theory.h index 0807006e0b5..81aac5c3aec 100644 --- a/src/solvers/smt2_incremental/smt_core_theory.h +++ b/src/solvers/smt2_incremental/smt_core_theory.h @@ -16,6 +16,14 @@ class smt_core_theoryt }; 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 equalt final { static const char *identifier(); diff --git a/unit/solvers/smt2_incremental/smt_core_theory.cpp b/unit/solvers/smt2_incremental/smt_core_theory.cpp index 885f857208d..f003f0099c8 100644 --- a/unit/solvers/smt2_incremental/smt_core_theory.cpp +++ b/unit/solvers/smt2_incremental/smt_core_theory.cpp @@ -22,6 +22,24 @@ TEST_CASE("SMT core theory \"not\".", "[core][smt2_incremental]") 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 \"=\".", "[core][smt2_incremental]") { SECTION("Bool sorted term comparison") From 686ba379534048ca27c78aa5199225049bda66a3 Mon Sep 17 00:00:00 2001 From: Thomas Spriggs Date: Fri, 30 Jul 2021 10:55:12 +0100 Subject: [PATCH 10/10] Add SMT2 incremental core theory logical operators --- .../smt2_incremental/smt_core_theory.cpp | 76 +++++++++++++++++++ .../smt2_incremental/smt_core_theory.h | 24 ++++++ .../smt2_incremental/smt_core_theory.cpp | 54 +++++++++++++ 3 files changed, 154 insertions(+) diff --git a/src/solvers/smt2_incremental/smt_core_theory.cpp b/src/solvers/smt2_incremental/smt_core_theory.cpp index e9c63b33e0b..6c3348caf64 100644 --- a/src/solvers/smt2_incremental/smt_core_theory.cpp +++ b/src/solvers/smt2_incremental/smt_core_theory.cpp @@ -48,6 +48,82 @@ void smt_core_theoryt::impliest::validate( 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 "="; diff --git a/src/solvers/smt2_incremental/smt_core_theory.h b/src/solvers/smt2_incremental/smt_core_theory.h index 81aac5c3aec..d59725ac57d 100644 --- a/src/solvers/smt2_incremental/smt_core_theory.h +++ b/src/solvers/smt2_incremental/smt_core_theory.h @@ -24,6 +24,30 @@ class smt_core_theoryt }; 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(); diff --git a/unit/solvers/smt2_incremental/smt_core_theory.cpp b/unit/solvers/smt2_incremental/smt_core_theory.cpp index f003f0099c8..c51603c4d17 100644 --- a/unit/solvers/smt2_incremental/smt_core_theory.cpp +++ b/unit/solvers/smt2_incremental/smt_core_theory.cpp @@ -40,6 +40,60 @@ TEST_CASE("SMT core theory implies.", "[core][smt2_incremental]") 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")