diff --git a/src/solvers/Makefile b/src/solvers/Makefile index 4b02b0621ff..6b6edee3a4e 100644 --- a/src/solvers/Makefile +++ b/src/solvers/Makefile @@ -197,6 +197,7 @@ SRC = $(BOOLEFORCE_SRC) \ smt2_incremental/smt_options.cpp \ smt2_incremental/smt_sorts.cpp \ smt2_incremental/smt_terms.cpp \ + smt2_incremental/smt_to_smt2_string.cpp \ smt2_incremental/smt2_incremental_decision_procedure.cpp \ # Empty last line diff --git a/src/solvers/smt2_incremental/smt_commands.cpp b/src/solvers/smt2_incremental/smt_commands.cpp index 45bfc418e38..6df79441599 100644 --- a/src/solvers/smt2_incremental/smt_commands.cpp +++ b/src/solvers/smt2_incremental/smt_commands.cpp @@ -83,7 +83,9 @@ smt_define_function_commandt::smt_define_function_commandt( smt_termt definition) : smt_commandt{ID_smt_define_function_command} { - set(ID_identifier, identifier); + set( + ID_identifier, + upcast(smt_identifier_termt{std::move(identifier), definition.get_sort()})); std::transform( std::make_move_iterator(parameters.begin()), std::make_move_iterator(parameters.end()), @@ -94,9 +96,10 @@ smt_define_function_commandt::smt_define_function_commandt( set(ID_code, upcast(std::move(definition))); } -const irep_idt &smt_define_function_commandt::identifier() const +const smt_identifier_termt &smt_define_function_commandt::identifier() const { - return get(ID_identifier); + return static_cast( + downcast(find(ID_identifier))); } std::vector> diff --git a/src/solvers/smt2_incremental/smt_commands.h b/src/solvers/smt2_incremental/smt_commands.h index 2b06f5b9fa5..aece515e41a 100644 --- a/src/solvers/smt2_incremental/smt_commands.h +++ b/src/solvers/smt2_incremental/smt_commands.h @@ -70,7 +70,7 @@ class smt_define_function_commandt irep_idt identifier, std::vector parameters, smt_termt definition); - const irep_idt &identifier() const; + const smt_identifier_termt &identifier() const; std::vector> parameters() const; const smt_sortt &return_sort() const; diff --git a/src/solvers/smt2_incremental/smt_sorts.cpp b/src/solvers/smt2_incremental/smt_sorts.cpp index bc721afd061..8a2567731f8 100644 --- a/src/solvers/smt2_incremental/smt_sorts.cpp +++ b/src/solvers/smt2_incremental/smt_sorts.cpp @@ -27,6 +27,10 @@ smt_bool_sortt::smt_bool_sortt() : smt_sortt{ID_smt_bool_sort} smt_bit_vector_sortt::smt_bit_vector_sortt(const std::size_t bit_width) : smt_sortt{ID_smt_bit_vector_sort} { + INVARIANT( + bit_width > 0, + "The definition of SMT2 bit vector theory requires the number of " + "bits to be greater than 0."); set_size_t(ID_width, bit_width); } diff --git a/src/solvers/smt2_incremental/smt_to_smt2_string.cpp b/src/solvers/smt2_incremental/smt_to_smt2_string.cpp new file mode 100644 index 00000000000..f4e4c48cf6b --- /dev/null +++ b/src/solvers/smt2_incremental/smt_to_smt2_string.cpp @@ -0,0 +1,375 @@ +// Author: Diffblue Ltd. + +#include + +#include +#include +#include +#include +#include + +#include +#include + +#include +#include +#include +#include +#include + +class smt_sort_output_visitort : public smt_sort_const_downcast_visitort +{ +protected: + std::ostream &os; + +public: + explicit smt_sort_output_visitort(std::ostream &os) : os(os) + { + } + + void visit(const smt_bool_sortt &) override + { + os << "Bool"; + } + + void visit(const smt_bit_vector_sortt &bit_vec) override + { + os << "(_ BitVec " << bit_vec.bit_width() << ")"; + } +}; + +std::ostream &operator<<(std::ostream &os, const smt_sortt &sort) +{ + sort.accept(smt_sort_output_visitort{os}); + return os; +} + +std::string smt_to_smt2_string(const smt_sortt &sort) +{ + std::stringstream ss; + ss << sort; + return ss.str(); +} + +/// \note The printing algorithm in the `smt_term_to_string_convertert` class is +/// implemented using an explicit `std::stack` rather than using recursion +/// and the call stack. This is done in order to ensure we can print smt terms +/// which are nested arbitrarily deeply without risk of exceeding the maximum +/// depth of the call stack. +/// \details +/// The set of `visit` functions push functions to `output_stack`, +/// which capture the value to be printed. When called these functions may +/// either print to the output stream or push further functions to the stack +/// in the case of nodes in the tree which have child nodes which also need to +/// be printed. +/// The `push_output(s)` functions exist as convenience functions to allow +/// pushing the capturing functions to the stack in the reverse order required +/// for printing, whilst keeping the visit functions easier to read by keeping +/// the outputs in reading order and separating the capturing code. +class smt_term_to_string_convertert : private smt_term_const_downcast_visitort +{ +private: + using output_functiont = std::function; + std::stack output_stack; + + static output_functiont make_output_function(const std::string &output); + static output_functiont make_output_function(const smt_sortt &output); + output_functiont make_output_function(const smt_termt &output); + output_functiont make_output_function( + const std::vector> &output); + + /// \brief Single argument version of `push_outputs`. + template + void push_output(outputt &&output); + + /// \brief Base case for the recursive `push_outputs` function template below. + void push_outputs(); + + /// \brief Pushes outputting functions to the output_stack for each of the + /// output values provided. This variadic template supports any (compile + /// time fixed) number of output arguments. + /// \details The arguments are pushed in order from right to left, so that + /// they are subsequently in left to right order when popped off the stack. + /// The types of argument supported are those supported by the overloads of + /// the `make_output_function` function. + /// \note This is implemented recursively, but does not risk exceeding the + /// maximum depth of the call stack. This is because the number of times it + /// recurses depends only on the number of arguments supplied in the source + /// code at compile time. + template + void push_outputs(outputt &&output, outputst &&... outputs); + + 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 + visit(const smt_function_application_termt &function_application) override; + +public: + /// \brief This function is complete the external interface to this class. All + /// construction of this class and printing of terms should be carried out + /// via this function. + static std::ostream &convert(std::ostream &os, const smt_termt &term); +}; + +smt_term_to_string_convertert::output_functiont +smt_term_to_string_convertert::make_output_function(const std::string &output) +{ + // `output` must be captured by value to avoid dangling references. + return [output](std::ostream &os) { os << output; }; +} + +smt_term_to_string_convertert::output_functiont +smt_term_to_string_convertert::make_output_function(const smt_sortt &output) +{ + return [=](std::ostream &os) { os << output; }; +} + +smt_term_to_string_convertert::output_functiont +smt_term_to_string_convertert::make_output_function(const smt_termt &output) +{ + return [=](std::ostream &os) { output.accept(*this); }; +} + +smt_term_to_string_convertert::output_functiont +smt_term_to_string_convertert::make_output_function( + const std::vector> &outputs) +{ + return [=](std::ostream &os) { + for(const auto &output : make_range(outputs.rbegin(), outputs.rend())) + { + push_outputs(" ", output.get()); + } + }; +} + +template +void smt_term_to_string_convertert::push_output(outputt &&output) +{ + output_stack.push(make_output_function(std::forward(output))); +} + +void smt_term_to_string_convertert::push_outputs() +{ +} + +template +void smt_term_to_string_convertert::push_outputs( + outputt &&output, + outputst &&... outputs) +{ + push_outputs(std::forward(outputs)...); + push_output(std::forward(output)); +} + +void smt_term_to_string_convertert::visit( + const smt_bool_literal_termt &bool_literal) +{ + 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) +{ + push_outputs( + "|", smt2_convt::convert_identifier(identifier_term.identifier()), "|"); +} + +void smt_term_to_string_convertert::visit( + const smt_bit_vector_constant_termt &bit_vector_constant) +{ + auto value = integer2string(bit_vector_constant.value()); + auto bit_width = std::to_string(bit_vector_constant.get_sort().bit_width()); + push_outputs("(_ bv", std::move(value), " ", std::move(bit_width), ")"); +} + +void smt_term_to_string_convertert::visit( + const smt_function_application_termt &function_application) +{ + const auto &id = function_application.function_identifier(); + auto arguments = function_application.arguments(); + push_outputs("(", id, std::move(arguments), ")"); +} + +std::ostream & +smt_term_to_string_convertert::convert(std::ostream &os, const smt_termt &term) +{ + smt_term_to_string_convertert converter; + term.accept(converter); + while(!converter.output_stack.empty()) + { + auto output_function = std::move(converter.output_stack.top()); + converter.output_stack.pop(); + output_function(os); + } + return os; +} + +std::ostream &operator<<(std::ostream &os, const smt_termt &term) +{ + return smt_term_to_string_convertert::convert(os, term); +} + +std::string smt_to_smt2_string(const smt_termt &term) +{ + std::stringstream ss; + ss << term; + return ss.str(); +} + +class smt_option_to_string_convertert + : public smt_option_const_downcast_visitort +{ +protected: + std::ostream &os; + +public: + explicit smt_option_to_string_convertert(std::ostream &os) : os(os) + { + } + + void visit(const smt_option_produce_modelst &produce_models) override + { + os << ":produce-models " << (produce_models.setting() ? "true" : "false"); + } +}; + +std::ostream &operator<<(std::ostream &os, const smt_optiont &option) +{ + option.accept(smt_option_to_string_convertert{os}); + return os; +} + +std::string smt_to_smt2_string(const smt_optiont &option) +{ + std::stringstream ss; + ss << option; + return ss.str(); +} + +class smt_logic_to_string_convertert : public smt_logic_const_downcast_visitort +{ +protected: + std::ostream &os; + +public: + explicit smt_logic_to_string_convertert(std::ostream &os) : os(os) + { + } + + void visit(const smt_logic_quantifier_free_bit_vectorst &) override + { + os << "QF_BV"; + } +}; + +std::ostream &operator<<(std::ostream &os, const smt_logict &logic) +{ + logic.accept(smt_logic_to_string_convertert{os}); + return os; +} + +std::string smt_to_smt2_string(const smt_logict &logic) +{ + std::stringstream ss; + ss << logic; + return ss.str(); +} + +class smt_command_to_string_convertert + : public smt_command_const_downcast_visitort +{ +protected: + std::ostream &os; + +public: + explicit smt_command_to_string_convertert(std::ostream &os) : os(os) + { + } + + void visit(const smt_assert_commandt &assert) override + { + os << "(assert " << assert.condition() << ")"; + } + + void visit(const smt_check_sat_commandt &check_sat) override + { + os << "(check-sat)"; + } + + void visit(const smt_declare_function_commandt &declare_function) override + { + os << "(declare-fun " << declare_function.identifier() << " ("; + const auto parameter_sorts = declare_function.parameter_sorts(); + join_strings(os, parameter_sorts.begin(), parameter_sorts.end(), ' '); + os << ") " << declare_function.return_sort() << ")"; + } + + void visit(const smt_define_function_commandt &define_function) override + { + os << "(define-fun " << define_function.identifier() << " ("; + const auto parameters = define_function.parameters(); + join_strings( + os, + parameters.begin(), + parameters.end(), + " ", + [](const smt_identifier_termt &identifier) { + return "(" + smt_to_smt2_string(identifier) + " " + + smt_to_smt2_string(identifier.get_sort()) + ")"; + }); + os << ") " << define_function.return_sort() << " " + << define_function.definition() << ")"; + } + + void visit(const smt_exit_commandt &exit) override + { + os << "(exit)"; + } + + void visit(const smt_get_value_commandt &get_value) override + { + os << "(get-value " << get_value.descriptor() << ")"; + } + + void visit(const smt_pop_commandt &pop) override + { + os << "(pop " << pop.levels() << ")"; + } + + void visit(const smt_push_commandt &push) override + { + os << "(push " << push.levels() << ")"; + } + + void visit(const smt_set_logic_commandt &set_logic) override + { + os << "(set-logic " << set_logic.logic() << ")"; + } + + void visit(const smt_set_option_commandt &set_option) override + { + os << "(set-option " << set_option.option() << ")"; + } +}; + +std::ostream &operator<<(std::ostream &os, const smt_commandt &command) +{ + command.accept(smt_command_to_string_convertert{os}); + return os; +} + +std::string smt_to_smt2_string(const smt_commandt &command) +{ + std::stringstream ss; + ss << command; + return ss.str(); +} diff --git a/src/solvers/smt2_incremental/smt_to_smt2_string.h b/src/solvers/smt2_incremental/smt_to_smt2_string.h new file mode 100644 index 00000000000..c8e78aa5255 --- /dev/null +++ b/src/solvers/smt2_incremental/smt_to_smt2_string.h @@ -0,0 +1,32 @@ +// Author: Diffblue Ltd. + +/// \file +/// Streaming SMT data structures to a string based output stream. The generated +/// output strings are intended to be valid input for SMT2 solvers compliant +/// with the SMT-LIB standard version 2.6. + +#ifndef CPROVER_SOLVERS_SMT2_INCREMENTAL_SMT_TO_SMT2_STRING_H +#define CPROVER_SOLVERS_SMT2_INCREMENTAL_SMT_TO_SMT2_STRING_H + +class smt_sortt; +class smt_termt; +class smt_optiont; +class smt_commandt; +class smt_logict; + +#include +#include + +std::ostream &operator<<(std::ostream &os, const smt_sortt &sort); +std::ostream &operator<<(std::ostream &os, const smt_termt &term); +std::ostream &operator<<(std::ostream &os, const smt_optiont &option); +std::ostream &operator<<(std::ostream &os, const smt_logict &logic); +std::ostream &operator<<(std::ostream &os, const smt_commandt &command); + +std::string smt_to_smt2_string(const smt_sortt &sort); +std::string smt_to_smt2_string(const smt_termt &term); +std::string smt_to_smt2_string(const smt_optiont &option); +std::string smt_to_smt2_string(const smt_logict &logic); +std::string smt_to_smt2_string(const smt_commandt &command); + +#endif // CPROVER_SOLVERS_SMT2_INCREMENTAL_SMT_TO_SMT2_STRING_H diff --git a/unit/Makefile b/unit/Makefile index 46fab54b042..1026b8bba0b 100644 --- a/unit/Makefile +++ b/unit/Makefile @@ -88,6 +88,7 @@ SRC += analyses/ai/ai.cpp \ solvers/smt2_incremental/smt_commands.cpp \ solvers/smt2_incremental/smt_sorts.cpp \ solvers/smt2_incremental/smt_terms.cpp \ + solvers/smt2_incremental/smt_to_smt2_string.cpp \ solvers/strings/array_pool/array_pool.cpp \ solvers/strings/string_constraint_generator_valueof/calculate_max_string_length.cpp \ solvers/strings/string_constraint_generator_valueof/get_numeric_value_from_character.cpp \ diff --git a/unit/solvers/smt2_incremental/smt_commands.cpp b/unit/solvers/smt2_incremental/smt_commands.cpp index 8aefb52a1f9..510574d7fae 100644 --- a/unit/solvers/smt2_incremental/smt_commands.cpp +++ b/unit/solvers/smt2_incremental/smt_commands.cpp @@ -37,7 +37,9 @@ TEST_CASE("smt_define_function_commandt getters", "[core][smt2_incremental]") {smt_identifier_termt{"x", smt_bool_sortt{}}, smt_identifier_termt{"y", smt_bool_sortt{}}}, smt_not_termt{smt_identifier_termt{"x", smt_bool_sortt{}}}}; - CHECK(function_definition.identifier() == "not first"); + CHECK( + function_definition.identifier() == + smt_identifier_termt{"not first", smt_bool_sortt{}}); CHECK( function_definition.parameters()[0].get() == smt_identifier_termt{"x", smt_bool_sortt{}}); diff --git a/unit/solvers/smt2_incremental/smt_sorts.cpp b/unit/solvers/smt2_incremental/smt_sorts.cpp index 94f532d3ece..50c1e3ec7fb 100644 --- a/unit/solvers/smt2_incremental/smt_sorts.cpp +++ b/unit/solvers/smt2_incremental/smt_sorts.cpp @@ -10,6 +10,14 @@ TEST_CASE("Test smt_sortt.pretty is accessible.", "[core][smt2_incremental]") REQUIRE(bool_sort.pretty(0, 0) == "smt_bool_sort"); } +TEST_CASE( + "Test smt_bit_vec_sortt bit width invariant", + "[core][smt2_incremental]") +{ + const cbmc_invariants_should_throwt invariants_throw_during_test; + REQUIRE_THROWS(smt_bit_vector_sortt{0}); +} + TEST_CASE( "Test smt_bit_vec_sortt bit_width getter.", "[core][smt2_incremental]") diff --git a/unit/solvers/smt2_incremental/smt_to_smt2_string.cpp b/unit/solvers/smt2_incremental/smt_to_smt2_string.cpp new file mode 100644 index 00000000000..becdde33022 --- /dev/null +++ b/unit/solvers/smt2_incremental/smt_to_smt2_string.cpp @@ -0,0 +1,144 @@ +// Author: Diffblue Ltd. + +#include + +#include +#include +#include +#include +#include + +#include + +TEST_CASE("Test smt_sortt to string conversion", "[core][smt2_incremental]") +{ + CHECK(smt_to_smt2_string(smt_bool_sortt{}) == "Bool"); + 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]") +{ + CHECK(smt_to_smt2_string(smt_bit_vector_constant_termt{0, 8}) == "(_ bv0 8)"); +} + +TEST_CASE( + "Test smt_bool_literal_termt to string conversion", + "[core][smt2_incremental]") +{ + CHECK(smt_to_smt2_string(smt_bool_literal_termt{true}) == "true"); + CHECK(smt_to_smt2_string(smt_bool_literal_termt{false}) == "false"); +} + +TEST_CASE( + "Test smt_function_application_termt to string conversion", + "[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}}}}}) == + "(|=| |foo| |bar|)"); +} + +TEST_CASE( + "Test smt_check_sat_commandt to string conversion", + "[core][smt2_incremental]") +{ + CHECK(smt_to_smt2_string(smt_check_sat_commandt{}) == "(check-sat)"); +} + +TEST_CASE( + "Test smt_exit_commandt to string conversion", + "[core][smt2_incremental]") +{ + CHECK(smt_to_smt2_string(smt_exit_commandt{}) == "(exit)"); +} + +TEST_CASE( + "Test smt_push_commandt to string conversion", + "[core][smt2_incremental]") +{ + CHECK(smt_to_smt2_string(smt_push_commandt{1}) == "(push 1)"); + CHECK(smt_to_smt2_string(smt_push_commandt{2}) == "(push 2)"); +} + +TEST_CASE( + "Test smt_pop_commandt to string conversion", + "[core][smt2_incremental]") +{ + CHECK(smt_to_smt2_string(smt_pop_commandt{1}) == "(pop 1)"); + CHECK(smt_to_smt2_string(smt_pop_commandt{2}) == "(pop 2)"); +} + +TEST_CASE( + "Test smt_assert_commandt to string conversion", + "[core][smt2_incremental]") +{ + CHECK( + smt_to_smt2_string(smt_assert_commandt{smt_bool_literal_termt{true}}) == + "(assert true)"); +} + +TEST_CASE( + "Test smt_declare_function_commandt to string conversion", + "[core][smt2_incremental]") +{ + CHECK( + smt_to_smt2_string(smt_declare_function_commandt{ + smt_identifier_termt{"f", smt_bit_vector_sortt{31}}, + {smt_bit_vector_sortt{32}, smt_bit_vector_sortt{33}}}) == + "(declare-fun |f| ((_ BitVec 32) (_ BitVec 33)) (_ BitVec 31))"); +} + +TEST_CASE( + "Test smt_define_function_commandt to string conversion", + "[core][smt2_incremental]") +{ + const auto g = smt_identifier_termt{"g", smt_bit_vector_sortt{32}}; + const auto h = smt_identifier_termt{"h", smt_bit_vector_sortt{32}}; + + CHECK( + smt_to_smt2_string(smt_define_function_commandt{ + "f", + {g, h}, + smt_function_application_termt{ + smt_identifier_termt{"=", smt_bool_sortt{}}, {g, h}}}) == + "(define-fun |f| ((|g| (_ BitVec 32)) (|h| (_ BitVec 32))) Bool (|=| |g| " + "|h|))"); +} + +TEST_CASE( + "Test smt_set_option_commandt to string conversion", + "[core][smt2_incremental]") +{ + const auto with_models = smt_option_produce_modelst{true}; + const auto no_models = smt_option_produce_modelst{false}; + CHECK(smt_to_smt2_string(with_models) == ":produce-models true"); + CHECK(smt_to_smt2_string(no_models) == ":produce-models false"); + CHECK( + smt_to_smt2_string(smt_set_option_commandt{with_models}) == + "(set-option :produce-models true)"); + CHECK( + smt_to_smt2_string(smt_set_option_commandt{no_models}) == + "(set-option :produce-models false)"); +} + +TEST_CASE( + "Test smt_set_logic_commandt to string conversion", + "[core][smt2_incremental]") +{ + const smt_logic_quantifier_free_bit_vectorst qf_bv; + CHECK(smt_to_smt2_string(qf_bv) == "QF_BV"); + CHECK( + smt_to_smt2_string(smt_set_logic_commandt{qf_bv}) == "(set-logic QF_BV)"); +}