diff --git a/src/solvers/Makefile b/src/solvers/Makefile index 2d891c8cf9b..7e72e8349ca 100644 --- a/src/solvers/Makefile +++ b/src/solvers/Makefile @@ -186,6 +186,7 @@ SRC = $(BOOLEFORCE_SRC) \ sat/pbs_dimacs_cnf.cpp \ sat/resolution_proof.cpp \ smt2/letify.cpp \ + smt2/smt2_ast.cpp \ smt2/smt2_conv.cpp \ smt2/smt2_dec.cpp \ smt2/smt2_format.cpp \ diff --git a/src/solvers/smt2/smt2_ast.cpp b/src/solvers/smt2/smt2_ast.cpp new file mode 100644 index 00000000000..f4a0ac31f5f --- /dev/null +++ b/src/solvers/smt2/smt2_ast.cpp @@ -0,0 +1,192 @@ +/*******************************************************************\ + +Module: SMT2 solver + +Author: Romain Brenguier, romain.brenguier@diffblue.com + +\*******************************************************************/ + +#include "smt2_ast.h" +#include +#include +#include +#include +#include + +struct smt2_ast_strategyt +{ + std::function data; + std::function parent; + std::function first_child; + std::function next_sibling; +}; + +/// Intermediary types for the \ref smt2_dfs_stackt definition +using tree_iteratort = smt2_astt::tree_implementationt::subt::const_iterator; +using stack_elementt = ranget; + +/// Stack class to help with DFS exploration of smt2_astt. +/// The stack stores an iterator for each level above the current position, +/// as well as the corresponding \c end iterator +class smt2_dfs_stackt : public std::deque +{ +public: + /// Current node if the stack is currently pointing to one, nullptr if it + /// needs to come back to its parent. + const smt2_astt *current_node() const + { + PRECONDITION(!empty()); + if(back().empty()) + return nullptr; + return &(*back().begin()); + } + + bool has_next_sibling() const + { + PRECONDITION(!empty()); + auto it = back().begin(); + it++; + return it != back().end(); + } + + /// Advance to next sibling if it exists, otherwise render the `back` + /// element of the stack empty. + void go_to_next_sibling() + { + PRECONDITION(!empty()); + back() = std::move(back()).drop(1); + } + + const smt2_astt *parent() const + { + if(this->empty()) + return nullptr; + auto it = this->end(); + (it--)--; + return &(*it->begin()); + } +}; + +static void dfs(const smt2_astt &ast, const smt2_ast_strategyt &strategy) +{ + strategy.data(ast); + auto begin = ast.read().sub.begin(); + auto end = ast.read().sub.end(); + if(begin == end) + return; + strategy.first_child(ast); + smt2_dfs_stackt stack; + stack.emplace_back(begin, end); + + while(!stack.empty()) + { + const auto current = stack.current_node(); + INVARIANT( + current != nullptr, + "at each iteration of the loop, the stack should be positioned on an " + "existing element"); + strategy.data(*current); + const smt2_astt::tree_implementationt::subt &children = current->read().sub; + if(!children.empty()) + { + stack.emplace_back(children.begin(), children.end()); + strategy.first_child(*current); + } + else + { + if(stack.has_next_sibling()) + { + auto p = stack.parent(); + INVARIANT(p, "siblings must have a parent"); + strategy.next_sibling(*p); + } + stack.go_to_next_sibling(); + while(!stack.empty() && stack.current_node() == nullptr) + { + stack.pop_back(); + if(!stack.empty()) + { + auto current = stack.current_node(); + INVARIANT( + current != nullptr, + "ranges in the stack should be positioned on existing nodes"); + // We came back to current after all its children + strategy.parent(*current); + if(stack.has_next_sibling()) + { + auto p = stack.parent(); + INVARIANT(p, "siblings must have a parent"); + strategy.next_sibling(*p); + } + stack.go_to_next_sibling(); + } + else + { + strategy.parent(ast); + } + } + } + } +} + +static void print_data(std::ostream &stream, const smt2_astt &ast) +{ + if(ast.id() == ID_symbol || ast.id() == ID_constant) + { + INVARIANT( + ast.read().named_sub.has_value(), + "constant and symbols should have an non-empty `named_sub` field"); + stream << ast.read().named_sub.value(); + } + else if(ast.id() == ID_string_constant) + { + stream << '\"' << ast.read().named_sub.value() << '\"'; + } + else if(ast.id() == ID_tuple && ast.read().sub.empty()) + { + stream << "()"; + } +} + +std::ostream &operator<<(std::ostream &stream, const smt2_astt &ast) +{ + smt2_ast_strategyt print_visitor; + print_visitor.data = [&stream](const smt2_astt &ast) { + print_data(stream, ast); + }; + print_visitor.first_child = [&stream](const smt2_astt &ast) { + if(ast.id() == ID_identifier) + stream << "(_ "; + else if(ast.id() == ID_forall) + stream << "(forall "; + else if(ast.id() == ID_exists) + stream << "(exists "; + else if(ast.id() == ID_let) + stream << "(let "; + else if(ast.id() == ID_par) + stream << "(par "; + else + stream << "("; + }; + print_visitor.next_sibling = [&stream](const smt2_astt &ast) { + stream << " "; + }; + print_visitor.parent = [&stream](const smt2_astt &ast) { stream << ")"; }; + dfs(ast, print_visitor); + return stream; +} + +smt2_sortt::smt2_sortt( + smt2_identifiert identifier, + std::vector &¶meters) + : smt2_astt(ID_type) +{ + if(!parameters.empty()) + { + auto &subs = write().sub; + subs.emplace_back(std::move(identifier)); + std::move(parameters.begin(), parameters.end(), std::back_inserter(subs)); + } + else + *this = smt2_sortt(std::move(identifier)); +} diff --git a/src/solvers/smt2/smt2_ast.h b/src/solvers/smt2/smt2_ast.h new file mode 100644 index 00000000000..b1c8ac7491d --- /dev/null +++ b/src/solvers/smt2/smt2_ast.h @@ -0,0 +1,311 @@ +/*******************************************************************\ + +Module: SMT2 solver + +Author: Romain Brenguier, romain.brenguier@diffblue.com + +\*******************************************************************/ + +/// \file +/// Abstract Syntax Tree for SMT2 + +#ifndef CPROVER_SOLVERS_SMT2_SMT2_AST_H +#define CPROVER_SOLVERS_SMT2_SMT2_AST_H + +#include +#include + +#include +#include +#include +#include + +/// Base class for Abstract Syntax Tree of SMT2 expressions. +/// Instances of this class are: +/// - \ref smt2_constantt with id \c ID_constant, +/// - \ref smt2_binary_literalt, special case of \ref smt2_constantt +/// - \ref smt2_symbolt, with id \c ID_symbol +/// - \ref smt2_string_literalt with id \c ID_string_constant +/// - \ref smt2_identifiert with id \c ID_identifier +/// - \ref smt2_sortt with with id \c ID_type +/// - \ref smt2_function_applicationt with id \c ID_function_application +/// - \ref smt2_listt with id \c ID_tuple +/// - \ref smt2_pairt, special case of \ref smt2_listt with exactly 2 elements +/// - \ref smt2_non_empty_listt, special case of \ref smt2_listt with at least +/// one element +/// - \ref smt2_forallt with id \c ID_forall +/// - \ref smt2_existst with id \c ID_exists +/// - \ref smt2_lett with id \c ID_let +/// - \ref smt2_sort_declarationt, special case of \ref smt2_pairt +/// - \ref smt2_selector_declarationt, special case of \ref smt2_pairt +/// - \ref smt2_constructor_declarationt with id \c ID_declaration +/// - \ref smt2_datatype_declarationt with id \c ID_par +class smt2_astt : public non_sharing_treet> +{ +public: + /// Empty constructor + smt2_astt() : tree_implementationt(irep_idt()) + { + } + + const irep_idt &id() const + { + return read().data; + } + + explicit smt2_astt(irep_idt id) : tree_implementationt(std::move(id)) + { + } +}; + +std::ostream &operator<<(std::ostream &stream, const smt2_astt &ast); + +class smt2_constantt : public smt2_astt +{ +public: + /// Make an AST representing a integer literal + static smt2_constantt make(const mp_integer &m) + { + return smt2_constantt(integer2string(m)); + } + +protected: + explicit smt2_constantt(irep_idt value) : smt2_astt(ID_constant) + { + write().named_sub = std::move(value); + } +}; + +class smt2_binary_literalt : public smt2_constantt +{ +public: + /// Make an AST representing a integer literal + static smt2_binary_literalt make(const mp_integer &m) + { + return smt2_binary_literalt(integer2string(m, 2)); + } + + /// Takes a string in binary + explicit smt2_binary_literalt(const irep_idt &m) + : smt2_constantt("#b" + id2string(m)) + { + } +}; + +class smt2_symbolt : public smt2_astt +{ +public: + explicit smt2_symbolt(irep_idt symbol) : smt2_astt(ID_symbol) + { + write().named_sub = std::move(symbol); + } +}; + +class smt2_string_literalt : public smt2_astt +{ +public: + explicit smt2_string_literalt(irep_idt literal) + : smt2_astt(ID_string_constant) + { + write().named_sub = std::move(literal); + } +}; + +class smt2_identifiert : public smt2_astt +{ +public: + /// Identifiers are either symbols, or indexed: `( _ + )` + explicit smt2_identifiert(smt2_symbolt sym) : smt2_astt(std::move(sym)) + { + } + + smt2_identifiert(smt2_symbolt sym, std::vector indexes) + : smt2_astt(ID_identifier) + { + auto &subs = write().sub; + subs.emplace_back(std::move(sym)); + std::move(indexes.begin(), indexes.end(), std::back_inserter(subs)); + } +}; + +class smt2_sortt : public smt2_astt +{ +public: + static smt2_sortt Bool() + { + return smt2_sortt(smt2_symbolt{"Bool"}); + } + + static smt2_sortt Int() + { + return smt2_sortt(smt2_symbolt{"Int"}); + } + + static smt2_sortt Real() + { + return smt2_sortt(smt2_symbolt{"Real"}); + } + + static smt2_sortt BitVec(const mp_integer &i) + { + return smt2_sortt{ + smt2_identifiert{smt2_symbolt("BitVec"), {smt2_constantt::make(i)}}, {}}; + } + + explicit smt2_sortt(smt2_symbolt symbol) + : smt2_astt(smt2_identifiert{std::move(symbol)}) + { + } + + explicit smt2_sortt(smt2_identifiert identifier) + : smt2_astt(std::move(identifier)) + { + } + + smt2_sortt(smt2_identifiert identifier, std::vector &¶meters); +}; + +class smt2_function_applicationt : public smt2_astt +{ +public: + explicit smt2_function_applicationt( + smt2_identifiert sym, + std::vector &&args) + : smt2_astt(ID_function_application) + { + auto &subs = write().sub; + subs.emplace_back(std::move(sym)); + std::move(args.begin(), args.end(), std::back_inserter(subs)); + } + + void add_argument(smt2_astt arg) + { + write().sub.emplace_back(std::move(arg)); + } +}; + +template +class smt2_listt : public smt2_astt +{ + static_assert( + std::is_base_of::value, + "smt2_listt should contain smt2_astt elements"); + +public: + explicit smt2_listt(std::vector &&list) : smt2_astt(ID_tuple) + { + std::move(list.begin(), list.end(), std::back_inserter(write().sub)); + } +}; + +template +class smt2_pairt : public smt2_listt +{ +public: + explicit smt2_pairt(firstt first, secondt second) : smt2_listt({}) + { + auto &subs = write().sub; + subs.push_back(std::move(first)); + subs.push_back(std::move(second)); + } + + const firstt &first() const + { + return static_cast(read().sub[0]); + } + + const smt2_sortt &second() const + { + return static_cast(read().sub[1]); + } +}; + +template +class smt2_non_empty_listt : public smt2_listt +{ +public: + explicit smt2_non_empty_listt( + underlyingt head, + std::vector &&tail) + : smt2_listt({std::move(head)}) + { + std::move( + tail.begin(), tail.end(), std::back_inserter(smt2_astt::write().sub)); + } +}; + +class smt2_forallt : public smt2_astt +{ +public: + explicit smt2_forallt( + smt2_listt> variables, + smt2_astt expr) + : smt2_astt(ID_forall) + { + auto &subs = write().sub; + subs.emplace_back(std::move(variables)); + subs.emplace_back(std::move(expr)); + } +}; + +class smt2_existst : public smt2_astt +{ +public: + explicit smt2_existst( + smt2_listt> variables, + smt2_astt expr) + : smt2_astt(ID_exists) + { + auto &subs = write().sub; + subs.emplace_back(std::move(variables)); + subs.emplace_back(std::move(expr)); + } +}; + +class smt2_lett : public smt2_astt +{ +public: + explicit smt2_lett( + smt2_listt> variables, + smt2_astt expr) + : smt2_astt(ID_let) + { + subt &subs = write().sub; + subs.emplace_back(std::move(variables)); + subs.emplace_back(std::move(expr)); + } +}; + +using smt2_sort_declarationt = smt2_pairt; +using smt2_selector_declarationt = smt2_pairt; + +class smt2_constructor_declarationt : public smt2_astt +{ +public: + explicit smt2_constructor_declarationt( + smt2_symbolt symbol, + std::vector selector_decs) + : smt2_astt(ID_declaration) + { + auto sub = write().sub; + sub.push_back(std::move(symbol)); + std::move( + selector_decs.begin(), selector_decs.end(), std::back_inserter(sub)); + } +}; + +class smt2_datatype_declarationt : public smt2_astt +{ +public: + explicit smt2_datatype_declarationt( + smt2_non_empty_listt symbols, + smt2_non_empty_listt selector_decs) + : smt2_astt(ID_par) + { + auto sub = write().sub; + sub.push_back(std::move(symbols)); + sub.push_back(std::move(selector_decs)); + } +}; + +#endif // CPROVER_SOLVERS_SMT2_SMT2_AST_H diff --git a/src/solvers/smt2/smt2_command.h b/src/solvers/smt2/smt2_command.h new file mode 100644 index 00000000000..c6b440ac547 --- /dev/null +++ b/src/solvers/smt2/smt2_command.h @@ -0,0 +1,201 @@ +/*******************************************************************\ + +Module: SMT2 solver + +Author: Romain Brenguier, romain.brenguier@diffblue.com + +\*******************************************************************/ + +/// \file +/// SMT2 commands + +#ifndef CPROVER_SOLVERS_SMT2_SMT2_COMMAND_H +#define CPROVER_SOLVERS_SMT2_SMT2_COMMAND_H + +#include "smt2_ast.h" + +class smt2_command_or_commentt +{ +public: + virtual void print(std::ostream &stream) const = 0; + virtual ~smt2_command_or_commentt() = default; +}; + +inline std::ostream & +operator<<(std::ostream &stream, const smt2_command_or_commentt &command) +{ + command.print(stream); + return stream; +} + +/// See the SMT-LIB standard for explanations about the meaning of the commands: +/// http://smtlib.cs.uiowa.edu/papers/smt-lib-reference-v2.0-r10.12.21.pdf +class smt2_commandt final : public smt2_command_or_commentt +{ +public: + void print(std::ostream &stream) const override; + + static smt2_commandt set_logic(smt2_symbolt symbol) + { + return smt2_commandt{"set-logic", {std::move(symbol)}}; + } + + static smt2_commandt declare_fun( + smt2_symbolt symbol, + smt2_listt arguments, + smt2_sortt result) + { + return smt2_commandt{ + "declare-fun", + {std::move(symbol), std::move(arguments), std::move(result)}}; + } + + static smt2_commandt define_fun( + smt2_symbolt symbol, + smt2_listt> arguments, + smt2_sortt result_sort, + smt2_astt result_expr) + { + return smt2_commandt{"define-fun", + {std::move(symbol), + std::move(arguments), + std::move(result_sort), + std::move(result_expr)}}; + } + + static smt2_commandt declare_sort(smt2_symbolt symbol, smt2_constantt numeral) + { + return smt2_commandt{"declare-sort", + {std::move(symbol), std::move(numeral)}}; + } + + static smt2_commandt define_sort( + smt2_symbolt symbol, + smt2_listt arguments, + smt2_astt expr) + { + return smt2_commandt{ + "define-sort", + {std::move(symbol), std::move(arguments), std::move(expr)}}; + } + + static smt2_commandt _assert(smt2_astt expr) + { + return smt2_commandt{"assert", {std::move(expr)}}; + } + + static smt2_commandt get_assertions() + { + return smt2_commandt{"get-assertions", {}}; + } + + static smt2_commandt check_sat() + { + return smt2_commandt{"check-sat", {}}; + } + + static smt2_commandt get_proof() + { + return smt2_commandt{"get-proof", {}}; + } + + static smt2_commandt get_unsat_core() + { + return smt2_commandt{"get-unsat-core", {}}; + } + + static smt2_commandt get_value(smt2_listt terms) + { + return smt2_commandt{"get-value", {std::move(terms)}}; + } + + static smt2_commandt get_assignment() + { + return smt2_commandt{"get-assignment", {}}; + } + + static smt2_commandt push(smt2_constantt numeral) + { + return smt2_commandt{"push", {std::move(numeral)}}; + } + + static smt2_commandt pop(smt2_constantt numeral) + { + return smt2_commandt{"pop", {std::move(numeral)}}; + } + + static smt2_commandt get_option(smt2_symbolt keyword) + { + return smt2_commandt{"get-option", {std::move(keyword)}}; + } + + static smt2_commandt set_option(smt2_symbolt keyword, smt2_astt value) + { + return smt2_commandt{"set-option", {std::move(keyword), std::move(value)}}; + } + + static smt2_commandt get_info(smt2_symbolt keyword) + { + return smt2_commandt{"get-info", {std::move(keyword)}}; + } + + static smt2_commandt set_info(smt2_symbolt keyword, smt2_astt value) + { + return smt2_commandt{"set-info", {std::move(keyword), std::move(value)}}; + } + + static smt2_commandt exit() + { + return smt2_commandt{"exit", {}}; + } + + static smt2_commandt declare_datatypes( + smt2_listt sort_decs, + smt2_listt datatype_decs) + { + return smt2_commandt{"declare-datatypes", + {std::move(sort_decs), std::move(datatype_decs)}}; + } + + static smt2_commandt + declare_datatypes(smt2_listt datatype_decs) + { + return declare_datatypes( + smt2_listt{{}}, std::move(datatype_decs)); + } + +private: + irep_idt name; + std::vector arguments; + + smt2_commandt(irep_idt name, std::vector arguments) + : name(std::move(name)), arguments(std::move(arguments)) + { + } +}; + +void smt2_commandt::print(std::ostream &stream) const +{ + stream << '(' << name; + for(const auto &arg : arguments) + stream << ' ' << arg; + stream << ")\n"; +} + +class smt2_commentt final : public smt2_command_or_commentt +{ +public: + void print(std::ostream &stream) const override + { + stream << "; " << content << '\n'; + } + + explicit smt2_commentt(std::string content) : content(std::move(content)) + { + } + +private: + std::string content; +}; + +#endif // CPROVER_SOLVERS_SMT2_SMT2_COMMAND_H diff --git a/src/solvers/smt2/smt2_conv.cpp b/src/solvers/smt2/smt2_conv.cpp index 61b3eb642d4..513262800e6 100644 --- a/src/solvers/smt2/smt2_conv.cpp +++ b/src/solvers/smt2/smt2_conv.cpp @@ -10,6 +10,9 @@ Author: Daniel Kroening, kroening@kroening.com /// SMT Backend #include "smt2_conv.h" +#include "smt2_ast.h" +#include "smt2_command.h" +#include "smt2_util.h" #include #include @@ -32,6 +35,7 @@ Author: Daniel Kroening, kroening@kroening.com #include #include #include +#include // Mark different kinds of error conditions @@ -148,15 +152,16 @@ void smt2_convt::write_header() // clang-format on } - out << "(set-info :source \"" << notes << "\")" << "\n"; - - out << "(set-option :produce-models true)" << "\n"; + out << smt2_commandt::set_info( + smt2_symbolt{":source"}, smt2_string_literalt(notes)) + << smt2_commandt::set_option( + smt2_symbolt{":produce-models"}, smt2_symbolt{"true"}); // We use a broad mixture of logics, so on some solvers // its better not to declare here. // set-logic should come after setting options if(emit_set_logic && !logic.empty()) - out << "(set-logic " << logic << ")" << "\n"; + out << smt2_commandt::set_logic(smt2_symbolt{logic}); } void smt2_convt::write_footer(std::ostream &os) @@ -170,10 +175,8 @@ void smt2_convt::write_footer(std::ostream &os) for(const auto &assumption : assumptions) { - os << "(assert "; - convert_literal(to_literal_expr(assumption).get_literal()); - os << ")" - << "\n"; + os << smt2_commandt::_assert( + convert_literal(to_literal_expr(assumption).get_literal())); } } @@ -181,20 +184,21 @@ void smt2_convt::write_footer(std::ostream &os) for(const auto &object : object_sizes) define_object_size(object.second, object.first); - os << "(check-sat)" - << "\n"; + os << smt2_commandt::check_sat(); os << "\n"; if(solver!=solvert::BOOLECTOR) { for(const auto &id : smt2_identifiers) - os << "(get-value (|" << id << "|))" - << "\n"; + { + os << smt2_commandt::get_value( + smt2_listt{{smt2_symbolt{"|" + id + "|"}}}); + } } os << "\n"; - os << "(exit)\n"; + os << smt2_commandt::exit(); os << "; end of SMT2 file" << "\n"; @@ -226,12 +230,13 @@ void smt2_convt::define_object_size( continue; } - out << "(assert (implies (= " << - "((_ extract " << h << " " << l << ") "; - convert_expr(ptr); - out << ") (_ bv" << number << " " << config.bv_encoding.object_bits << "))" - << "(= " << id << " (_ bv" << *object_size << " " << size_width - << "))))\n"; + // (assert (implies (= ((_ extract h l) ptr) (_ bv number + // config.bv_encoding.object_bits)) (= id (_ bv object_size size_width)))) + out << smt2_commandt::_assert(smt2_implies( + smt2_eq( + smt2_function_applicationt(smt2_extract(h, l), {convert_expr(ptr)}), + smt2_bv(number, config.bv_encoding.object_bits)), + smt2_eq(smt2_symbolt{id}, smt2_bv(*object_size, size_width)))); ++number; } @@ -601,7 +606,7 @@ exprt smt2_convt::parse_rec(const irept &src, const typet &type) return nil_exprt(); } -void smt2_convt::convert_address_of_rec( +smt2_astt smt2_convt::convert_address_of_rec( const exprt &expr, const pointer_typet &result_type) { @@ -610,12 +615,9 @@ void smt2_convt::convert_address_of_rec( expr.id()==ID_string_constant || expr.id()==ID_label) { - out - << "(concat (_ bv" - << pointer_logic.add_object(expr) << " " - << config.bv_encoding.object_bits << ")" - << " (_ bv0 " - << boolbv_width(result_type)-config.bv_encoding.object_bits << "))"; + return smt2_concat( + smt2_bv(pointer_logic.add_object(expr), config.bv_encoding.object_bits), + smt2_bv(0, boolbv_width(result_type) - config.bv_encoding.object_bits)); } else if(expr.id()==ID_index) { @@ -627,9 +629,9 @@ void smt2_convt::convert_address_of_rec( if(index.is_zero()) { if(array.type().id()==ID_pointer) - convert_expr(array); + return convert_expr(array); else if(array.type().id()==ID_array) - convert_address_of_rec(array, result_type); + return convert_address_of_rec(array, result_type); else UNREACHABLE; } @@ -645,7 +647,7 @@ void smt2_convt::convert_address_of_rec( plus_exprt plus_expr{address_of_expr, index}; - convert_expr(plus_expr); + return convert_expr(plus_expr); } } else if(expr.id()==ID_member) @@ -669,22 +671,17 @@ void smt2_convt::convert_address_of_rec( unsignedbv_typet index_type(boolbv_width(result_type)); // pointer arithmetic - out << "(bvadd "; - convert_address_of_rec(struct_op, result_type); - convert_expr(from_integer(*offset, index_type)); - out << ")"; // bvadd + return smt2_bvadd( + convert_address_of_rec(struct_op, result_type), + convert_expr(from_integer(*offset, index_type))); } else if(expr.id()==ID_if) { const if_exprt &if_expr = to_if_expr(expr); - - out << "(ite "; - convert_expr(if_expr.cond()); - out << " "; - convert_address_of_rec(if_expr.true_case(), result_type); - out << " "; - convert_address_of_rec(if_expr.false_case(), result_type); - out << ")"; + return smt2_ite( + convert_expr(if_expr.cond()), + convert_address_of_rec(if_expr.true_case(), result_type), + convert_address_of_rec(if_expr.false_case(), result_type)); } else INVARIANT( @@ -693,6 +690,16 @@ void smt2_convt::convert_address_of_rec( expr.id_string()); } +/// Create a name for the literal with the given number, add it to the set of +/// identifiers and return a corresponding symbolt +static smt2_symbolt +literal_name(literalt::var_not var_no, std::set &smt2_identifiers) +{ + std::string literal_name = "B" + std::to_string(var_no); + smt2_identifiers.insert(literal_name); + return smt2_symbolt("|" + literal_name + "|"); +} + literalt smt2_convt::convert(const exprt &expr) { PRECONDITION(expr.type().id() == ID_bool); @@ -710,17 +717,21 @@ literalt smt2_convt::convert(const exprt &expr) out << "\n"; - exprt prepared_expr = prepare_for_convert_expr(expr); + auto prepared_expr_with_dependencies = prepare_for_convert_expr(expr); + for(const auto &command : prepared_expr_with_dependencies.first) + out << *command; literalt l(no_boolean_variables, false); no_boolean_variables++; out << "; convert\n"; - out << "(define-fun "; - convert_literal(l); - out << " () Bool "; - convert_expr(prepared_expr); - out << ")" << "\n"; + + // (define-fun l () Bool expr) + out << smt2_commandt::define_fun( + literal_name(l.var_no(), smt2_identifiers), + smt2_listt>{{}}, + smt2_sortt::Bool(), + convert_expr(prepared_expr_with_dependencies.second)); return l; } @@ -734,24 +745,18 @@ exprt smt2_convt::handle(const exprt &expr) return literal_exprt(convert(expr)); } -void smt2_convt::convert_literal(const literalt l) +smt2_astt smt2_convt::convert_literal(const literalt l) { if(l==const_literal(false)) - out << "false"; - else if(l==const_literal(true)) - out << "true"; - else - { - if(l.sign()) - out << "(not "; - - out << "|B" << l.var_no() << "|"; + return smt2_symbolt("false"); + if(l == const_literal(true)) + return smt2_symbolt("true"); - if(l.sign()) - out << ")"; + auto literal_without_sign = literal_name(l.var_no(), smt2_identifiers); - smt2_identifiers.insert("B"+std::to_string(l.var_no())); - } + if(!l.sign()) + return std::move(literal_without_sign); + return smt2_not(std::move(literal_without_sign)); } void smt2_convt::push() @@ -845,80 +850,77 @@ std::string smt2_convt::floatbv_suffix(const exprt &expr) const return "_"+type2id(expr.op0().type())+"->"+type2id(expr.type()); } -void smt2_convt::convert_floatbv(const exprt &expr) +smt2_astt smt2_convt::convert_floatbv(const exprt &expr) { PRECONDITION(!use_FPA_theory); if(expr.id()==ID_symbol) { const irep_idt &id = to_symbol_expr(expr).get_identifier(); - out << '|' << convert_identifier(id) << '|'; - return; + return smt2_symbolt("|" + convert_identifier(id) + '|'); } if(expr.id()==ID_smt2_symbol) { const irep_idt &id = to_smt2_symbol(expr).get_identifier(); - out << id; - return; + return smt2_symbolt(id2string(id)); } INVARIANT( !expr.operands().empty(), "non-symbol expressions shall have operands"); - out << "(|float_bv." << expr.id() - << floatbv_suffix(expr) - << '|'; + smt2_symbolt quoted_symbol{"|float_bv." + id2string(expr.id()) + + floatbv_suffix(expr) + '|'}; + smt2_function_applicationt node{smt2_identifiert{std::move(quoted_symbol)}, + {}}; forall_operands(it, expr) - { - out << ' '; - convert_expr(*it); - } + node.add_argument(convert_expr(*it)); - out << ')'; + return std::move(node); } -void smt2_convt::convert_expr(const exprt &expr) +smt2_astt smt2_convt::convert_expr(const exprt &expr) { // huge monster case split over expression id if(expr.id()==ID_symbol) { const irep_idt &id = to_symbol_expr(expr).get_identifier(); DATA_INVARIANT(!id.empty(), "symbol must have identifier"); - out << '|' << convert_identifier(id) << '|'; + return smt2_symbolt("|" + convert_identifier(id) + '|'); } else if(expr.id()==ID_nondet_symbol) { const irep_idt &id = to_nondet_symbol_expr(expr).get_identifier(); DATA_INVARIANT(!id.empty(), "nondet symbol must have identifier"); - out << '|' << convert_identifier("nondet_"+id2string(id)) << '|'; + return smt2_symbolt( + "|" + convert_identifier("nondet_" + id2string(id)) + "|"); } else if(expr.id()==ID_smt2_symbol) { const irep_idt &id = to_smt2_symbol(expr).get_identifier(); DATA_INVARIANT(!id.empty(), "smt2 symbol must have identifier"); - out << id; + return smt2_symbolt(id2string(id)); } else if(expr.id()==ID_typecast) { - convert_typecast(to_typecast_expr(expr)); + return convert_typecast(to_typecast_expr(expr)); } else if(expr.id()==ID_floatbv_typecast) { - convert_floatbv_typecast(to_floatbv_typecast_expr(expr)); + return convert_floatbv_typecast(to_floatbv_typecast_expr(expr)); } else if(expr.id()==ID_struct) { - convert_struct(to_struct_expr(expr)); + return convert_struct(to_struct_expr(expr)); } else if(expr.id()==ID_union) { - convert_union(to_union_expr(expr)); + return convert_union(to_union_expr(expr)); } else if(expr.id()==ID_constant) { - convert_constant(to_constant_expr(expr)); + return convert_constant(to_constant_expr(expr)); } else if(expr.id() == ID_concatenation && expr.operands().size() == 1) { @@ -927,7 +929,7 @@ void smt2_convt::convert_expr(const exprt &expr) "concatenation over a single operand should have matching types", expr.pretty()); - convert_expr(expr.operands().front()); + return convert_expr(expr.operands().front()); } else if(expr.id()==ID_concatenation || expr.id()==ID_bitand || @@ -941,28 +943,27 @@ void smt2_convt::convert_expr(const exprt &expr) "given expression should have at least two operands", expr.id_string()); - out << "("; - - if(expr.id()==ID_concatenation) - out << "concat"; - else if(expr.id()==ID_bitand) - out << "bvand"; - else if(expr.id()==ID_bitor) - out << "bvor"; - else if(expr.id()==ID_bitxor) - out << "bvxor"; - else if(expr.id()==ID_bitnand) - out << "bvnand"; - else if(expr.id()==ID_bitnor) - out << "bvnor"; - - forall_operands(it, expr) - { - out << " "; - flatten2bv(*it); - } + auto function_name = smt2_symbolt([&] { + if(expr.id() == ID_concatenation) + return "concat"; + else if(expr.id() == ID_bitand) + return "bvand"; + else if(expr.id() == ID_bitor) + return "bvor"; + else if(expr.id() == ID_bitxor) + return "bvxor"; + else if(expr.id() == ID_bitnand) + return "bvnand"; + else if(expr.id() == ID_bitnor) + return "bvnor"; + UNREACHABLE; + }()); - out << ")"; + smt2_function_applicationt application{ + smt2_identifiert{std::move(function_name)}, {}}; + for(const exprt &e : expr.operands()) + application.add_argument(flatten2bv(e)); + return std::move(application); } else if(expr.id()==ID_bitnot) { @@ -978,32 +979,33 @@ void smt2_convt::convert_expr(const exprt &expr) const vector_typet &vector_type = to_vector_type(bitnot_expr.type()); mp_integer size = numeric_cast_v(vector_type.size()); - - out << "(let ((?vectorop "; - convert_expr(bitnot_expr.op()); - out << ")) "; - - out << "(mk-" << smt_typename; - typet index_type=vector_type.size().type(); + smt2_function_applicationt bvnot_node{ + smt2_identifiert{smt2_symbolt{"mk-" + smt_typename}}, {}}; + // do bitnot component-by-component for(mp_integer i=0; i!=size; ++i) { - out << " (bvnot (" << smt_typename << "." << (size-i-1) - << " ?vectorop))"; + smt2_symbolt function_name{smt_typename + "." + + std::to_string((size - i - 1).to_long())}; + bvnot_node.add_argument(smt2_bvnot(smt2_function_applicationt{ + smt2_identifiert{std::move(function_name)}, + {smt2_symbolt{"?vectorop"}}})); } - out << "))"; // mk-, let + return smt2_lett{ + smt2_listt>{ + {smt2_pairt{ + smt2_symbolt{"?vectorop"}, convert_expr(bitnot_expr.op())}}}, + std::move(bvnot_node)}; } else SMT2_TODO("bitnot for vectors"); } else { - out << "(bvnot "; - convert_expr(bitnot_expr.op()); - out << ")"; + return smt2_bvnot(convert_expr(bitnot_expr.op())); } } else if(expr.id()==ID_unary_minus) @@ -1015,21 +1017,20 @@ void smt2_convt::convert_expr(const exprt &expr) unary_minus_expr.type().id() == ID_integer || unary_minus_expr.type().id() == ID_real) { - out << "(- "; - convert_expr(unary_minus_expr.op()); - out << ")"; + return smt2_function_applicationt{smt2_identifiert{smt2_symbolt{"-"}}, + {convert_expr(unary_minus_expr.op())}}; } else if(unary_minus_expr.type().id() == ID_floatbv) { // this has no rounding mode if(use_FPA_theory) { - out << "(fp.neg "; - convert_expr(unary_minus_expr.op()); - out << ")"; + return smt2_function_applicationt{ + smt2_identifiert{smt2_symbolt{"fp.neg"}}, + {convert_expr(unary_minus_expr.op())}}; } else - convert_floatbv(unary_minus_expr); + return convert_floatbv(unary_minus_expr); } else if(unary_minus_expr.type().id() == ID_vector) { @@ -1044,37 +1045,38 @@ void smt2_convt::convert_expr(const exprt &expr) mp_integer size = numeric_cast_v(vector_type.size()); - out << "(let ((?vectorop "; - convert_expr(unary_minus_expr.op()); - out << ")) "; - - out << "(mk-" << smt_typename; - + auto bvneg_node = smt2_function_applicationt{ + smt2_identifiert{smt2_symbolt{"mk-" + smt_typename}}, {}}; typet index_type=vector_type.size().type(); // negate component-by-component for(mp_integer i=0; i!=size; ++i) { - out << " (bvneg (" << smt_typename << "." << (size-i-1) - << " ?vectorop))"; + smt2_symbolt function_name{smt_typename + "." + + std::to_string((size - i - 1).to_long())}; + bvneg_node.add_argument(smt2_bvneg(smt2_function_applicationt{ + smt2_identifiert{std::move(function_name)}, + {smt2_symbolt{"?vectorop"}}})); } - out << "))"; // mk-, let + return smt2_lett{ + smt2_listt>{ + {smt2_pairt{ + smt2_symbolt{"?vectorop"}, convert_expr(unary_minus_expr.op())}}}, + std::move(bvneg_node)}; } else SMT2_TODO("unary minus for vector"); } else { - out << "(bvneg "; - convert_expr(unary_minus_expr.op()); - out << ")"; + return smt2_bvneg(convert_expr(unary_minus_expr.op())); } } else if(expr.id()==ID_unary_plus) { // A no-op (apart from type promotion) - convert_expr(to_unary_plus_expr(expr).op()); + return convert_expr(to_unary_plus_expr(expr).op()); } else if(expr.id()==ID_sign) { @@ -1086,20 +1088,17 @@ void smt2_convt::convert_expr(const exprt &expr) { if(use_FPA_theory) { - out << "(fp.isNegative "; - convert_expr(sign_expr.op()); - out << ")"; + return smt2_function_applicationt{ + smt2_identifiert{smt2_symbolt{"fp.isNegative"}}, + {convert_expr(sign_expr.op())}}; } else - convert_floatbv(sign_expr); + return convert_floatbv(sign_expr); } else if(op_type.id()==ID_signedbv) { std::size_t op_width=to_signedbv_type(op_type).get_width(); - - out << "(bvslt "; - convert_expr(sign_expr.op()); - out << " (_ bv0 " << op_width << "))"; + return smt2_bvslt(convert_expr(sign_expr.op()), smt2_bv(0, op_width)); } else INVARIANT_WITH_DIAGNOSTICS( @@ -1110,14 +1109,10 @@ void smt2_convt::convert_expr(const exprt &expr) else if(expr.id()==ID_if) { const if_exprt &if_expr = to_if_expr(expr); - - out << "(ite "; - convert_expr(if_expr.cond()); - out << " "; - convert_expr(if_expr.true_case()); - out << " "; - convert_expr(if_expr.false_case()); - out << ")"; + return smt2_ite( + convert_expr(if_expr.cond()), + convert_expr(if_expr.true_case()), + convert_expr(if_expr.false_case())); } else if(expr.id()==ID_and || expr.id()==ID_or || @@ -1130,13 +1125,11 @@ void smt2_convt::convert_expr(const exprt &expr) expr.operands().size() >= 2, "logical and, or, and xor expressions should have at least two operands"); - out << "(" << expr.id(); + auto node = + smt2_function_applicationt{smt2_identifiert{smt2_symbolt{expr.id()}}, {}}; forall_operands(it, expr) - { - out << " "; - convert_expr(*it); - } - out << ")"; + node.add_argument(convert_expr(*it)); + return std::move(node); } else if(expr.id()==ID_implies) { @@ -1146,11 +1139,8 @@ void smt2_convt::convert_expr(const exprt &expr) implies_expr.type().id() == ID_bool, "implies expression should have Boolean type"); - out << "(=> "; - convert_expr(implies_expr.op0()); - out << " "; - convert_expr(implies_expr.op1()); - out << ")"; + return smt2_implies( + convert_expr(implies_expr.op0()), convert_expr(implies_expr.op1())); } else if(expr.id()==ID_not) { @@ -1160,9 +1150,7 @@ void smt2_convt::convert_expr(const exprt &expr) not_expr.type().id() == ID_bool, "not expression should have Boolean type"); - out << "(not "; - convert_expr(not_expr.op()); - out << ")"; + return smt2_not(convert_expr(not_expr.op())); } else if(expr.id() == ID_equal) { @@ -1172,11 +1160,7 @@ void smt2_convt::convert_expr(const exprt &expr) equal_expr.op0().type() == equal_expr.op1().type(), "operands of equal expression shall have same type"); - out << "(= "; - convert_expr(expr.op0()); - out << " "; - convert_expr(expr.op1()); - out << ")"; + return smt2_eq(convert_expr(expr.op0()), convert_expr(expr.op1())); } else if(expr.id() == ID_notequal) { @@ -1186,11 +1170,8 @@ void smt2_convt::convert_expr(const exprt &expr) notequal_expr.op0().type() == notequal_expr.op1().type(), "operands of not equal expression shall have same type"); - out << "(not (= "; - convert_expr(notequal_expr.op0()); - out << " "; - convert_expr(notequal_expr.op1()); - out << "))"; + return smt2_not(smt2_eq( + convert_expr(notequal_expr.op0()), convert_expr(notequal_expr.op1()))); } else if(expr.id()==ID_ieee_float_equal || expr.id()==ID_ieee_float_notequal) @@ -1207,68 +1188,63 @@ void smt2_convt::convert_expr(const exprt &expr) // The FPA theory properly treats NaN and negative zero. if(use_FPA_theory) { + smt2_function_applicationt node{ + smt2_identifiert{smt2_symbolt{"fp.eq"}}, + {convert_expr(expr.op0()), convert_expr(expr.op1())}}; if(expr.id()==ID_ieee_float_notequal) - out << "(not "; - - out << "(fp.eq "; - convert_expr(expr.op0()); - out << " "; - convert_expr(expr.op1()); - out << ")"; - - if(expr.id()==ID_ieee_float_notequal) - out << ")"; + return smt2_not(std::move(node)); + return std::move(node); } else - convert_floatbv(expr); + return convert_floatbv(expr); } else if(expr.id()==ID_le || expr.id()==ID_lt || expr.id()==ID_ge || expr.id()==ID_gt) { - convert_relation(expr); + return convert_relation(expr); } else if(expr.id()==ID_plus) { - convert_plus(to_plus_expr(expr)); + return convert_plus(to_plus_expr(expr)); } else if(expr.id()==ID_floatbv_plus) { - convert_floatbv_plus(to_ieee_float_op_expr(expr)); + return convert_floatbv_plus(to_ieee_float_op_expr(expr)); } else if(expr.id()==ID_minus) { - convert_minus(to_minus_expr(expr)); + return convert_minus(to_minus_expr(expr)); } else if(expr.id()==ID_floatbv_minus) { - convert_floatbv_minus(to_ieee_float_op_expr(expr)); + return convert_floatbv_minus(to_ieee_float_op_expr(expr)); } else if(expr.id()==ID_div) { - convert_div(to_div_expr(expr)); + return convert_div(to_div_expr(expr)); } else if(expr.id()==ID_floatbv_div) { - convert_floatbv_div(to_ieee_float_op_expr(expr)); + return convert_floatbv_div(to_ieee_float_op_expr(expr)); } else if(expr.id()==ID_mod) { - convert_mod(to_mod_expr(expr)); + return convert_mod(to_mod_expr(expr)); } else if(expr.id()==ID_mult) { - convert_mult(to_mult_expr(expr)); + return convert_mult(to_mult_expr(expr)); } else if(expr.id()==ID_floatbv_mult) { - convert_floatbv_mult(to_ieee_float_op_expr(expr)); + return convert_floatbv_mult(to_ieee_float_op_expr(expr)); } else if(expr.id()==ID_address_of) { const address_of_exprt &address_of_expr = to_address_of_expr(expr); - convert_address_of_rec( + return convert_address_of_rec( address_of_expr.object(), to_pointer_type(address_of_expr.type())); } else if(expr.id()==ID_array_of) @@ -1282,11 +1258,11 @@ void smt2_convt::convert_expr(const exprt &expr) defined_expressionst::const_iterator it = defined_expressions.find(array_of_expr); CHECK_RETURN(it != defined_expressions.end()); - out << it->second; + return smt2_symbolt(id2string(it->second)); } else if(expr.id()==ID_index) { - convert_index(to_index_expr(expr)); + return convert_index(to_index_expr(expr)); } else if(expr.id()==ID_ashr || expr.id()==ID_lshr || @@ -1299,61 +1275,65 @@ void smt2_convt::convert_expr(const exprt &expr) type.id()==ID_signedbv || type.id()==ID_bv) { - if(shift_expr.id() == ID_ashr) - out << "(bvashr "; - else if(shift_expr.id() == ID_lshr) - out << "(bvlshr "; - else if(shift_expr.id() == ID_shl) - out << "(bvshl "; - else - UNREACHABLE; - - convert_expr(shift_expr.op()); - out << " "; + auto function_name = smt2_symbolt([&] { + if(shift_expr.id() == ID_ashr) + return "bvashr"; + else if(shift_expr.id() == ID_lshr) + return "bvlshr"; + else if(shift_expr.id() == ID_shl) + return "bvshl"; + else + UNREACHABLE; + }()); + smt2_function_applicationt application{smt2_identifiert{function_name}, + {}}; + application.add_argument(convert_expr(shift_expr.op())); // SMT2 requires the shift distance to have the same width as // the value that is shifted -- odd! - if(shift_expr.distance().type().id() == ID_integer) - { - const mp_integer i = - numeric_cast_v(to_constant_expr(shift_expr.distance())); - - // shift distance must be bit vector - std::size_t width_op0 = boolbv_width(shift_expr.op().type()); - exprt tmp=from_integer(i, unsignedbv_typet(width_op0)); - convert_expr(tmp); - } - else if( - shift_expr.distance().type().id() == ID_signedbv || - shift_expr.distance().type().id() == ID_unsignedbv || - shift_expr.distance().type().id() == ID_c_enum || - shift_expr.distance().type().id() == ID_c_bool) - { - std::size_t width_op0 = boolbv_width(shift_expr.op().type()); - std::size_t width_op1 = boolbv_width(shift_expr.distance().type()); - - if(width_op0==width_op1) - convert_expr(shift_expr.distance()); - else if(width_op0>width_op1) + auto child = [&]() -> smt2_astt { + if(shift_expr.distance().type().id() == ID_integer) { - out << "((_ zero_extend " << width_op0-width_op1 << ") "; - convert_expr(shift_expr.distance()); - out << ")"; // zero_extend + const mp_integer i = + numeric_cast_v(to_constant_expr(shift_expr.distance())); + + // shift distance must be bit vector + std::size_t width_op0 = boolbv_width(shift_expr.op().type()); + exprt tmp = from_integer(i, unsignedbv_typet(width_op0)); + return convert_expr(tmp); } - else // width_op0 width_op1) + { + return smt2_function_applicationt{ + smt2_zero_extend(width_op0 - width_op1), + {convert_expr(shift_expr.distance())}}; + } + else // width_op0result_width) offset_bits=result_width; - // too few bits? - if(result_width>offset_bits) - out << "((_ zero_extend " << result_width-offset_bits << ") "; - - out << "((_ extract " << offset_bits-1 << " 0) "; - convert_expr(expr.op0()); - out << ")"; + smt2_function_applicationt application{smt2_extract(offset_bits - 1, 0), + {convert_expr(expr.op0())}}; + // too few bits? if(result_width>offset_bits) - out << ")"; // zero_extend + { + return smt2_function_applicationt{ + smt2_zero_extend(result_width - offset_bits), {std::move(application)}}; + } + return std::move(application); } else if(expr.id()==ID_pointer_object) { @@ -1413,21 +1393,18 @@ void smt2_convt::convert_expr(const exprt &expr) std::size_t ext=boolbv_width(expr.type())-config.bv_encoding.object_bits; std::size_t pointer_width=boolbv_width(expr.op0().type()); - if(ext>0) - out << "((_ zero_extend " << ext << ") "; + smt2_function_applicationt node{ + smt2_extract( + pointer_width - 1, pointer_width - config.bv_encoding.object_bits), + {convert_expr(expr.op0())}}; - out << "((_ extract " - << pointer_width-1 << " " - << pointer_width-config.bv_encoding.object_bits << ") "; - convert_expr(expr.op0()); - out << ")"; - - if(ext>0) - out << ")"; // zero_extend + if(ext <= 0) + return std::move(node); + return smt2_function_applicationt{smt2_zero_extend(ext), {std::move(node)}}; } else if(expr.id() == ID_is_dynamic_object) { - convert_is_dynamic_object(expr); + return convert_is_dynamic_object(expr); } else if(expr.id() == ID_is_invalid_pointer) { @@ -1436,18 +1413,19 @@ void smt2_convt::convert_expr(const exprt &expr) "invalid pointer expression shall have one operand"); std::size_t pointer_width=boolbv_width(expr.op0().type()); - out << "(= ((_ extract " - << pointer_width-1 << " " - << pointer_width-config.bv_encoding.object_bits << ") "; - convert_expr(expr.op0()); - out << ") (_ bv" << pointer_logic.get_invalid_object() - << " " << config.bv_encoding.object_bits << "))"; + return smt2_eq( + smt2_function_applicationt{ + smt2_extract( + pointer_width - 1, pointer_width - config.bv_encoding.object_bits), + {convert_expr(expr.op0())}}, + smt2_bv( + pointer_logic.get_invalid_object(), config.bv_encoding.object_bits)); } else if(expr.id()==ID_string_constant) { defined_expressionst::const_iterator it=defined_expressions.find(expr); CHECK_RETURN(it != defined_expressions.end()); - out << it->second; + return smt2_symbolt(it->second); } else if(expr.id()==ID_extractbit) { @@ -1457,20 +1435,20 @@ void smt2_convt::convert_expr(const exprt &expr) { const mp_integer i = numeric_cast_v(to_constant_expr(extractbit_expr.index())); - - out << "(= ((_ extract " << i << " " << i << ") "; - flatten2bv(extractbit_expr.src()); - out << ") #b1)"; + return smt2_eq( + smt2_function_applicationt{smt2_extract(i, i), + {flatten2bv(extractbit_expr.src())}}, + smt2_symbolt("#b1")); } else { - out << "(= ((_ extract 0 0) "; - // the arguments of the shift need to have the same width - out << "(bvlshr "; - flatten2bv(extractbit_expr.src()); typecast_exprt tmp(extractbit_expr.index(), extractbit_expr.src().type()); - convert_expr(tmp); - out << ")) bin1)"; // bvlshr, extract, = + return smt2_eq( + smt2_function_applicationt{smt2_extract(0, 0), + {smt2_symbolt{"bvlshr"}, + flatten2bv(extractbit_expr.src()), + convert_expr(tmp)}}, + smt2_symbolt{"bin1"}); } } else if(expr.id()==ID_extractbits) @@ -1490,10 +1468,8 @@ void smt2_convt::convert_expr(const exprt &expr) std::swap(op1_i, op2_i); // now op1_i>=op2_i - - out << "((_ extract " << op1_i << " " << op2_i << ") "; - flatten2bv(extractbits_expr.src()); - out << ")"; + return smt2_function_applicationt{smt2_extract(op1_i, op2_i), + {flatten2bv(extractbits_expr.src())}}; } else { @@ -1515,10 +1491,8 @@ void smt2_convt::convert_expr(const exprt &expr) const replication_exprt &replication_expr = to_replication_expr(expr); mp_integer times = numeric_cast_v(replication_expr.times()); - - out << "((_ repeat " << times << ") "; - flatten2bv(replication_expr.op()); - out << ")"; + return smt2_function_applicationt{smt2_repeat(smt2_constantt::make(times)), + {flatten2bv(replication_expr.op())}}; } else if(expr.id()==ID_byte_extract_little_endian || expr.id()==ID_byte_extract_big_endian) @@ -1543,8 +1517,7 @@ void smt2_convt::convert_expr(const exprt &expr) std::size_t op_width=boolbv_width(expr.op0().type()); CHECK_RETURN(op_width != 0); - out << "(_ bv" << op_width/8 - << " " << result_width << ")"; + return smt2_bv(op_width / 8, result_width); } else if(expr.id()==ID_abs) { @@ -1555,39 +1528,29 @@ void smt2_convt::convert_expr(const exprt &expr) if(type.id()==ID_signedbv) { std::size_t result_width = to_signedbv_type(type).get_width(); - - out << "(ite (bvslt "; - convert_expr(abs_expr.op()); - out << " (_ bv0 " << result_width << ")) "; - out << "(bvneg "; - convert_expr(abs_expr.op()); - out << ") "; - convert_expr(abs_expr.op()); - out << ")"; + return smt2_ite( + smt2_bvslt(convert_expr(abs_expr.op()), smt2_bv(0, result_width)), + smt2_bvneg(convert_expr(abs_expr.op())), + convert_expr(abs_expr.op())); } else if(type.id()==ID_fixedbv) { std::size_t result_width=to_fixedbv_type(type).get_width(); - - out << "(ite (bvslt "; - convert_expr(abs_expr.op()); - out << " (_ bv0 " << result_width << ")) "; - out << "(bvneg "; - convert_expr(abs_expr.op()); - out << ") "; - convert_expr(abs_expr.op()); - out << ")"; + return smt2_ite( + smt2_bvslt(convert_expr(abs_expr.op()), smt2_bv(0, result_width)), + smt2_bvneg(convert_expr(abs_expr.op())), + convert_expr(abs_expr.op())); } else if(type.id()==ID_floatbv) { if(use_FPA_theory) { - out << "(fp.abs "; - convert_expr(abs_expr.op()); - out << ")"; + return smt2_function_applicationt{ + smt2_identifiert{smt2_symbolt{"fp.abs"}}, + {convert_expr(abs_expr.op())}}; } else - convert_floatbv(abs_expr); + return convert_floatbv(abs_expr); } else UNREACHABLE; @@ -1599,17 +1562,13 @@ void smt2_convt::convert_expr(const exprt &expr) const typet &op_type = isnan_expr.op().type(); if(op_type.id()==ID_fixedbv) - out << "false"; + return smt2_symbolt{"false"}; else if(op_type.id()==ID_floatbv) { if(use_FPA_theory) - { - out << "(fp.isNaN "; - convert_expr(isnan_expr.op()); - out << ")"; - } + return smt2_fp_is_nan(convert_expr(isnan_expr.op())); else - convert_floatbv(isnan_expr); + return convert_floatbv(isnan_expr); } else UNREACHABLE; @@ -1621,25 +1580,17 @@ void smt2_convt::convert_expr(const exprt &expr) const typet &op_type = isfinite_expr.op().type(); if(op_type.id()==ID_fixedbv) - out << "true"; + return smt2_symbolt{"true"}; else if(op_type.id()==ID_floatbv) { if(use_FPA_theory) { - out << "(and "; - - out << "(not (fp.isNaN "; - convert_expr(isfinite_expr.op()); - out << "))"; - - out << "(not (fp.isInf "; - convert_expr(isfinite_expr.op()); - out << "))"; - - out << ")"; + return smt2_and( + smt2_not(smt2_fp_is_nan(convert_expr(isfinite_expr.op()))), + smt2_not(smt2_fp_is_infinite(convert_expr(isfinite_expr.op())))); } else - convert_floatbv(isfinite_expr); + return convert_floatbv(isfinite_expr); } else UNREACHABLE; @@ -1651,17 +1602,13 @@ void smt2_convt::convert_expr(const exprt &expr) const typet &op_type = isinf_expr.op().type(); if(op_type.id()==ID_fixedbv) - out << "false"; + return smt2_symbolt("false"); else if(op_type.id()==ID_floatbv) { if(use_FPA_theory) - { - out << "(fp.isInfinite "; - convert_expr(isinf_expr.op()); - out << ")"; - } + return smt2_fp_is_infinite(convert_expr(isinf_expr.op())); else - convert_floatbv(isinf_expr); + return convert_floatbv(isinf_expr); } else UNREACHABLE; @@ -1673,17 +1620,13 @@ void smt2_convt::convert_expr(const exprt &expr) const typet &op_type = isnormal_expr.op().type(); if(op_type.id()==ID_fixedbv) - out << "true"; + return smt2_symbolt{"true"}; else if(op_type.id()==ID_floatbv) { if(use_FPA_theory) - { - out << "(fp.isNormal "; - convert_expr(isnormal_expr.op()); - out << ")"; - } + return smt2_fp_is_normal(convert_expr(isnormal_expr.op())); else - convert_floatbv(isnormal_expr); + return convert_floatbv(isnormal_expr); } else UNREACHABLE; @@ -1706,39 +1649,47 @@ void smt2_convt::convert_expr(const exprt &expr) if(op_type.id()==ID_signedbv) { // an overflow occurs if the top two bits of the extended sum differ - out << "(let ((?sum ("; - out << (subtract?"bvsub":"bvadd"); - out << " ((_ sign_extend 1) "; - convert_expr(expr.op0()); - out << ")"; - out << " ((_ sign_extend 1) "; - convert_expr(expr.op1()); - out << ")))) "; // sign_extend, bvadd/sub let2 - out << "(not (= " - "((_ extract " << width << " " << width << ") ?sum) " - "((_ extract " << (width-1) << " " << (width-1) << ") ?sum)"; - out << ")))"; // =, not, let + return smt2_lett( + smt2_listt>{ + {smt2_pairt{ + smt2_symbolt("?sum"), + smt2_function_applicationt{ + smt2_identifiert{smt2_symbolt{subtract ? "bvsub" : "bvadd"}}, + {smt2_function_applicationt{ + smt2_sign_extend(smt2_constantt::make(1)), + {convert_expr(expr.op0())}}, + smt2_function_applicationt{ + smt2_sign_extend(smt2_constantt::make(1)), + {convert_expr(expr.op1())}}}}, + }}}, + smt2_not(smt2_eq( + smt2_function_applicationt{smt2_extract(width, width), + {smt2_symbolt{"?sum"}}}, + smt2_function_applicationt{smt2_extract(width - 1, width - 1), + {smt2_symbolt{"?sum"}}}))); } else if(op_type.id()==ID_unsignedbv || op_type.id()==ID_pointer) { // overflow is simply carry-out - out << "(= "; - out << "((_ extract " << width << " " << width << ") "; - out << "(" << (subtract?"bvsub":"bvadd"); - out << " ((_ zero_extend 1) "; - convert_expr(expr.op0()); - out << ")"; - out << " ((_ zero_extend 1) "; - convert_expr(expr.op1()); - out << ")))"; // zero_extend, bvsub/bvadd, extract - out << " #b1)"; // = + return smt2_eq( + smt2_function_applicationt{ + smt2_extract(width, width), + {smt2_function_applicationt{ + smt2_identifiert{smt2_symbolt{subtract ? "bvsub" : "bvadd"}}, + {smt2_function_applicationt{smt2_zero_extend(1), + {convert_expr(expr.op0())}}, + smt2_function_applicationt{smt2_zero_extend(1), + {convert_expr(expr.op1())}}}}}}, + smt2_symbolt{"#b1"}); } else + { INVARIANT_WITH_DIAGNOSTICS( false, "overflow check should not be performed on unsupported type", op_type.id_string()); + } } else if(expr.id()==ID_overflow_mult) { @@ -1758,23 +1709,33 @@ void smt2_convt::convert_expr(const exprt &expr) if(op_type.id()==ID_signedbv) { - out << "(let ( (prod (bvmul ((_ sign_extend " << width << ") "; - convert_expr(expr.op0()); - out << ") ((_ sign_extend " << width << ") "; - convert_expr(expr.op1()); - out << ")) )) "; - out << "(or (bvsge prod (_ bv" << power(2, width-1) << " " - << width*2 << "))"; - out << " (bvslt prod (bvneg (_ bv" << power(2, width-1) << " " - << width*2 << ")))))"; + return smt2_lett{ + smt2_listt>{ + {smt2_pairt{ + smt2_symbolt{"prod"}, + smt2_bvmul( + smt2_function_applicationt{ + smt2_sign_extend(smt2_constantt::make(width)), + {convert_expr(expr.op0())}}, + smt2_function_applicationt{ + smt2_sign_extend(smt2_constantt::make(width)), + {convert_expr(expr.op1())}})}}}, + smt2_or( + smt2_bvsge( + smt2_symbolt("prod"), smt2_bv(power(2, width - 1), width * 2)), + smt2_bvslt( + smt2_symbolt("prod"), + smt2_bvneg(smt2_bv(power(2, width - 1), width * 2))))}; } else if(op_type.id()==ID_unsignedbv) { - out << "(bvuge (bvmul ((_ zero_extend " << width << ") "; - convert_expr(expr.op0()); - out << ") ((_ zero_extend " << width << ") "; - convert_expr(expr.op1()); - out << ")) (_ bv" << power(2, width) << " " << width*2 << "))"; + return smt2_bvuge( + smt2_bvmul( + smt2_function_applicationt{smt2_zero_extend(width), + {convert_expr(expr.op0())}}, + smt2_function_applicationt{smt2_zero_extend(width), + {convert_expr(expr.op1())}}), + smt2_bv(power(2, width), width * 2)); } else INVARIANT_WITH_DIAGNOSTICS( @@ -1786,11 +1747,11 @@ void smt2_convt::convert_expr(const exprt &expr) { defined_expressionst::const_iterator it=defined_expressions.find(expr); CHECK_RETURN(it != defined_expressions.end()); - out << it->second; + return smt2_symbolt((id2string(it->second))); } else if(expr.id()==ID_literal) { - convert_literal(to_literal_expr(expr).get_literal()); + return convert_literal(to_literal_expr(expr).get_literal()); } else if(expr.id()==ID_forall || expr.id()==ID_exists) @@ -1801,22 +1762,27 @@ void smt2_convt::convert_expr(const exprt &expr) // NOLINTNEXTLINE(readability/throw) throw "MathSAT does not support quantifiers"; - if(quantifier_expr.id() == ID_forall) - out << "(forall "; - else if(quantifier_expr.id() == ID_exists) - out << "(exists "; - exprt bound=expr.op0(); + smt2_astt bound_ast = convert_expr(bound); + INVARIANT( + bound_ast.id() == ID_symbol, "quantifier bound should be a symbol"); + const auto &bound_symbol = static_cast(bound_ast); + smt2_sortt bound_type_ast = convert_type(bound.type()); + auto where_ast = convert_expr(quantifier_expr.where()); - out << "(("; - convert_expr(bound); - out << " "; - convert_type(bound.type()); - out << ")) "; - - convert_expr(quantifier_expr.where()); - - out << ")"; + if(quantifier_expr.id() == ID_forall) + { + return smt2_forallt( + smt2_listt>{ + {smt2_pairt{bound_symbol, + std::move(bound_type_ast)}}}, + std::move(where_ast)); + } + return smt2_existst( + smt2_listt>{ + {smt2_pairt( + bound_symbol, std::move(bound_type_ast))}}, + std::move(where_ast)); } else if(expr.id()==ID_vector) { @@ -1829,38 +1795,35 @@ void smt2_convt::convert_expr(const exprt &expr) size == vector_expr.operands().size(), "size indicated by type shall be equal to the number of operands"); - if(use_datatypes) - { + auto function_name = smt2_symbolt([&]() -> std::string { + if(!use_datatypes) + return "concat"; const std::string &smt_typename = datatype_map.at(vector_type); + return "mk-" + smt_typename; + }()); - out << "(mk-" << smt_typename; - } - else - out << "(concat"; + smt2_function_applicationt application{ + smt2_identifiert{std::move(function_name)}, {}}; // build component-by-component forall_operands(it, vector_expr) - { - out << " "; - convert_expr(*it); - } - - out << ")"; // mk-... or concat + application.add_argument(convert_expr(*it)); } else if(expr.id()==ID_object_size) { - out << object_sizes[expr]; + return smt2_symbolt(id2string(object_sizes[expr])); } else if(expr.id()==ID_let) { const let_exprt &let_expr=to_let_expr(expr); - out << "(let (("; - convert_expr(let_expr.symbol()); - out << ' '; - convert_expr(let_expr.value()); - out << ")) "; - convert_expr(let_expr.where()); - out << ')'; // let + auto symbol_ast = convert_expr(let_expr.symbol()); + CHECK_RETURN(symbol_ast.id() == ID_symbol); + auto &smt2_symbol = static_cast(symbol_ast); + return smt2_lett( + smt2_listt>{ + {smt2_pairt{smt2_symbol, + convert_expr(let_expr.value())}}}, + convert_expr(let_expr.where())); } else if(expr.id()==ID_constraint_select_one) { @@ -1876,75 +1839,80 @@ void smt2_convt::convert_expr(const exprt &expr) bswap_expr.op().type() == bswap_expr.type(), "operand of byte swap expression shall have same type as the expression"); - // first 'let' the operand - out << "(let ((bswap_op "; - convert_expr(bswap_expr.op()); - out << ")) "; - - if( - bswap_expr.type().id() == ID_signedbv || - bswap_expr.type().id() == ID_unsignedbv) - { - const std::size_t width = - to_bitvector_type(bswap_expr.type()).get_width(); - - const std::size_t bits_per_byte = bswap_expr.get_bits_per_byte(); + auto node = [&]() -> smt2_astt { + if( + bswap_expr.type().id() == ID_signedbv || + bswap_expr.type().id() == ID_unsignedbv) + { + const std::size_t width = + to_bitvector_type(bswap_expr.type()).get_width(); - // width must be multiple of bytes - DATA_INVARIANT( - width % bits_per_byte == 0, - "bit width indicated by type of bswap expression should be a multiple " - "of the number of bits per byte"); + const std::size_t bits_per_byte = bswap_expr.get_bits_per_byte(); - const std::size_t bytes = width / bits_per_byte; + // width must be multiple of bytes + DATA_INVARIANT( + width % bits_per_byte == 0, + "bit width indicated by type of bswap expression should be a " + "multiple " + "of the number of bits per byte"); - if(bytes <= 1) - out << "bswap_op"; - else - { - // do a parallel 'let' for each byte - out << "(let ("; + const std::size_t bytes = width / bits_per_byte; - for(std::size_t byte = 0; byte < bytes; byte++) + if(bytes <= 1) + return smt2_symbolt{"bswap_op"}; + else { - if(byte != 0) - out << ' '; - out << "(bswap_byte_" << byte << ' '; - out << "((_ extract " << (byte * bits_per_byte + (bits_per_byte - 1)) - << " " << (byte * bits_per_byte) << ") bswap_op)"; - out << ')'; - } - - out << ") "; + // do a parallel 'let' for each byte + std::vector> list; - // now stitch back together with 'concat' - out << "(concat"; + for(std::size_t byte = 0; byte < bytes; byte++) + { + list.emplace_back( + smt2_symbolt("bswap_byte_" + std::to_string(byte)), + smt2_function_applicationt{ + smt2_extract( + byte * bits_per_byte + (bits_per_byte - 1), + byte * bits_per_byte), + {smt2_symbolt{"bswap_op"}}}); + } - for(std::size_t byte = 0; byte < bytes; byte++) - out << " bswap_byte_" << byte; + smt2_function_applicationt concat{ + smt2_identifiert{smt2_symbolt{"concat"}}, {}}; + for(std::size_t byte = 0; byte < bytes; byte++) + { + concat.add_argument( + smt2_symbolt("bswap_byte_" + std::to_string(byte))); + } - out << ')'; // concat - out << ')'; // let bswap_byte_* + return smt2_lett{ + smt2_listt>{std::move(list)}, + std::move(concat)}; + } } - } - else - UNEXPECTEDCASE("bswap must get bitvector operand"); - - out << ')'; // let bswap_op + else + UNEXPECTEDCASE("bswap must get bitvector operand"); + UNREACHABLE; + }(); + return smt2_lett( + smt2_listt>{ + {smt2_pairt{smt2_symbolt("bswap_op"), + convert_expr(bswap_expr.op())}}}, + std::move(node)); } else if(expr.id() == ID_popcount) { exprt lowered = lower_popcount(to_popcount_expr(expr), ns); - convert_expr(lowered); + return convert_expr(lowered); } else INVARIANT_WITH_DIAGNOSTICS( false, "smt2_convt::convert_expr should not be applied to unsupported type", expr.id_string()); + UNREACHABLE; } -void smt2_convt::convert_typecast(const typecast_exprt &expr) +smt2_astt smt2_convt::convert_typecast(const typecast_exprt &expr) { const exprt &src = expr.op(); @@ -1966,22 +1934,17 @@ void smt2_convt::convert_typecast(const typecast_exprt &expr) src_type.id()==ID_pointer || src_type.id()==ID_integer) { - out << "(not (= "; - convert_expr(src); - out << " "; - convert_expr(from_integer(0, src_type)); - out << "))"; + return smt2_not( + smt2_eq(convert_expr(src), convert_expr(from_integer(0, src_type)))); } else if(src_type.id()==ID_floatbv) { if(use_FPA_theory) { - out << "(not (fp.isZero "; - convert_expr(src); - out << "))"; + return smt2_not(smt2_fp_is_zero(convert_expr(src))); } else - convert_floatbv(expr); + return convert_floatbv(expr); } else { @@ -1991,15 +1954,11 @@ void smt2_convt::convert_typecast(const typecast_exprt &expr) else if(dest_type.id()==ID_c_bool) { std::size_t to_width=boolbv_width(dest_type); - out << "(ite "; - out << "(not (= "; - convert_expr(src); - out << " "; - convert_expr(from_integer(0, src_type)); - out << ")) "; // not, = - out << " (_ bv1 " << to_width << ")"; - out << " (_ bv0 " << to_width << ")"; - out << ")"; // ite + return smt2_ite( + smt2_not( + smt2_eq(convert_expr(src), convert_expr(from_integer(0, src_type)))), + smt2_bv(1, to_width), + smt2_bv(0, to_width)); } else if(dest_type.id()==ID_signedbv || dest_type.id()==ID_unsignedbv || @@ -2017,24 +1976,20 @@ void smt2_convt::convert_typecast(const typecast_exprt &expr) std::size_t from_width=boolbv_width(src_type); if(from_width==to_width) - convert_expr(src); // ignore + return convert_expr(src); // ignore else if(from_widthfrom_integer_bits) - { - out << "((_ sign_extend " - << (to_width-from_integer_bits) << ") "; - out << "((_ extract " << (from_width-1) << " " - << from_fraction_bits << ") "; - convert_expr(src); - out << "))"; - } - else - { - out << "((_ extract " << (from_fraction_bits+to_width-1) - << " " << from_fraction_bits << ") "; - convert_expr(src); - out << ")"; - } - - out << " (ite (and "; - - // some fraction bit is not zero - out << "(not (= ((_ extract " << (from_fraction_bits-1) << " 0) ?tcop) " - "(_ bv0 " << from_fraction_bits << ")))"; - - // number negative - out << " (= ((_ extract " << (from_width-1) << " " << (from_width-1) - << ") ?tcop) #b1)"; - - out << ")"; // and - - out << " (_ bv1 " << to_width << ") (_ bv0 " << to_width << "))"; // ite - out << ")"; // bvadd - out << ")"; // let - } - else if(src_type.id()==ID_floatbv) // from floatbv to int + return smt2_function_applicationt( + smt2_identifiert{smt2_symbolt{"?tcop"}}, + {convert_expr(src), + smt2_bvadd( + [&] { + if(to_width > from_integer_bits) + { + return smt2_function_applicationt{ + smt2_sign_extend( + smt2_constantt::make(to_width - from_integer_bits)), + {smt2_function_applicationt{ + smt2_extract(from_width - 1, from_fraction_bits), + {convert_expr(src)}}}}; + } + else + { + return smt2_function_applicationt{ + smt2_extract( + from_fraction_bits + to_width - 1, from_fraction_bits), + {convert_expr(src)}}; + } + }(), + smt2_ite( + smt2_and( + smt2_not(smt2_eq( + smt2_function_applicationt{ + smt2_extract(from_fraction_bits - 1, 0), + {smt2_symbolt("?tcop")}}, + smt2_bv(0, from_fraction_bits))), + smt2_eq( + smt2_function_applicationt{ + smt2_extract(from_width - 1, from_width - 1), + {smt2_symbolt("?tcop")}}, + smt2_symbolt("#b1"))), + smt2_bv(1, to_width), + smt2_bv(0, to_width)))}); + } + else if(src_type.id() == ID_floatbv) // from floatbv to int { if(dest_type.id()==ID_bv) { @@ -2103,7 +2055,7 @@ void smt2_convt::convert_typecast(const typecast_exprt &expr) else { // straight-forward if width matches - convert_expr(src); + return convert_expr(src); } } else if(dest_type.id()==ID_signedbv) @@ -2123,24 +2075,22 @@ void smt2_convt::convert_typecast(const typecast_exprt &expr) } else if(src_type.id()==ID_bool) // from boolean to int { - out << "(ite "; - convert_expr(src); + auto cond = convert_expr(src); if(dest_type.id()==ID_fixedbv) { fixedbv_spect spec(to_fixedbv_type(dest_type)); - out << " (concat (_ bv1 " - << spec.integer_bits << ") " << - "(_ bv0 " << spec.get_fraction_bits() << ")) " << - "(_ bv0 " << spec.width << ")"; + return smt2_ite( + cond, + smt2_concat( + smt2_bv(1, spec.integer_bits), + smt2_bv(0, spec.get_fraction_bits())), + smt2_bv(0, spec.width)); } else { - out << " (_ bv1 " << to_width << ")"; - out << " (_ bv0 " << to_width << ")"; + return smt2_ite(cond, smt2_bv(1, to_width), smt2_bv(0, to_width)); } - - out << ")"; } else if(src_type.id()==ID_pointer) // from pointer to int { @@ -2148,17 +2098,14 @@ void smt2_convt::convert_typecast(const typecast_exprt &expr) if(from_width(to_constant_expr(src)); - out << "(_ bv" << i << " " << to_width << ")"; + return smt2_bv( + numeric_cast_v(to_constant_expr(src)), to_width); } else SMT2_TODO("can't convert non-constant integer to bitvector"); @@ -2181,14 +2128,14 @@ void smt2_convt::convert_typecast(const typecast_exprt &expr) INVARIANT( boolbv_width(src_type) == boolbv_width(dest_type), "bit vector with of source and destination type shall be equal"); - flatten2bv(src); + return flatten2bv(src); } else { INVARIANT( boolbv_width(src_type) == boolbv_width(dest_type), "bit vector with of source and destination type shall be equal"); - convert_expr(src); // nothing else to do! + return convert_expr(src); // nothing else to do! } } else if( @@ -2198,19 +2145,19 @@ void smt2_convt::convert_typecast(const typecast_exprt &expr) INVARIANT( boolbv_width(src_type) == boolbv_width(dest_type), "bit vector with of source and destination type shall be equal"); - convert_expr(src); // nothing else to do! + return convert_expr(src); // nothing else to do! } else if(src_type.id()==ID_c_bit_field) { std::size_t from_width=boolbv_width(src_type); if(from_width==to_width) - convert_expr(src); // ignore + return convert_expr(src); // ignore else { typet t=c_bit_field_replacement_type(to_c_bit_field_type(src_type), ns); typecast_exprt tmp(typecast_exprt(src, t), dest_type); - convert_typecast(tmp); + return convert_typecast(tmp); } } else @@ -2234,51 +2181,45 @@ void smt2_convt::convert_typecast(const typecast_exprt &expr) // integer to fixedbv std::size_t from_width=to_bitvector_type(src_type).get_width(); - out << "(concat "; - - if(from_width==to_integer_bits) - convert_expr(src); - else if(from_width>to_integer_bits) - { - // too many integer bits - out << "((_ extract " << (to_integer_bits-1) << " 0) "; - convert_expr(src); - out << ")"; - } - else - { - // too few integer bits - INVARIANT( - from_width < to_integer_bits, - "from_width should be smaller than to_integer_bits as other case " - "have been handled above"); - if(dest_type.id()==ID_unsignedbv) - { - out << "(_ zero_extend " - << (to_integer_bits-from_width) << ") "; - convert_expr(src); - out << ")"; - } - else - { - out << "((_ sign_extend " - << (to_integer_bits-from_width) << ") "; - convert_expr(src); - out << ")"; - } - } - - out << "(_ bv0 " << to_fraction_bits << ")"; - out << ")"; // concat + return smt2_concat( + [&]() -> smt2_astt { + if(from_width == to_integer_bits) + return convert_expr(src); + else if(from_width > to_integer_bits) + { + // too many integer bits + return smt2_function_applicationt( + smt2_extract((to_integer_bits - 1), 0), {convert_expr(src)}); + } + else + { + // too few integer bits + INVARIANT( + from_width < to_integer_bits, + "from_width should be smaller than to_integer_bits as other case " + "have been handled above"); + if(dest_type.id() == ID_unsignedbv) + { + return smt2_function_applicationt( + smt2_zero_extend(to_integer_bits - from_width), + {convert_expr(src)}); + } + else + { + return smt2_function_applicationt( + smt2_sign_extend( + smt2_constantt::make(to_integer_bits - from_width)), + {convert_expr(src)}); + } + } + }(), + smt2_bv(0, to_fraction_bits)); } else if(src_type.id()==ID_bool) // bool to fixedbv { - out << "(concat (concat" - << " (_ bv0 " << (to_integer_bits-1) << ") "; - flatten2bv(src); // produces #b0 or #b1 - out << ") (_ bv0 " - << to_fraction_bits - << "))"; + return smt2_concat( + smt2_concat(smt2_bv(0, to_integer_bits - 1), flatten2bv(src)), + smt2_bv(0, to_fraction_bits)); } else if(src_type.id()==ID_fixedbv) // fixedbv to fixedbv { @@ -2287,57 +2228,59 @@ void smt2_convt::convert_typecast(const typecast_exprt &expr) std::size_t from_integer_bits=from_fixedbv_type.get_integer_bits(); std::size_t from_width=from_fixedbv_type.get_width(); - out << "(let ((?tcop "; - convert_expr(src); - out << ")) "; - - out << "(concat "; - - if(to_integer_bits<=from_integer_bits) - { - out << "((_ extract " - << (from_fraction_bits+to_integer_bits-1) << " " - << from_fraction_bits - << ") ?tcop)"; - } - else - { - INVARIANT( - to_integer_bits > from_integer_bits, - "to_integer_bits should be greater than from_integer_bits as the" - "other case has been handled above"); - out << "((_ sign_extend " - << (to_integer_bits-from_integer_bits) - << ") ((_ extract " - << (from_width-1) << " " - << from_fraction_bits - << ") ?tcop))"; - } - - out << " "; - - if(to_fraction_bits<=from_fraction_bits) - { - out << "((_ extract " - << (from_fraction_bits-1) << " " - << (from_fraction_bits-to_fraction_bits) - << ") ?tcop)"; - } - else - { - INVARIANT( - to_fraction_bits > from_fraction_bits, - "to_fraction_bits should be greater than from_fraction_bits as the" - "other case has been handled above"); - out << "(concat ((_ extract " - << (from_fraction_bits-1) << " 0) "; - convert_expr(src); - out << ")" - << " (_ bv0 " << to_fraction_bits-from_fraction_bits - << "))"; - } - - out << "))"; // concat, let + return smt2_lett( + smt2_listt>{ + {smt2_pairt{smt2_symbolt("?tcop"), + convert_expr(src)}}}, + smt2_concat( + [&]() -> smt2_astt { + if(to_integer_bits <= from_integer_bits) + { + return smt2_function_applicationt( + smt2_extract( + from_fraction_bits + to_integer_bits - 1, from_fraction_bits), + {smt2_symbolt("?tcop")}); + } + else + { + INVARIANT( + to_integer_bits > from_integer_bits, + "to_integer_bits should be greater than from_integer_bits as " + "the" + "other case has been handled above"); + return smt2_function_applicationt( + smt2_sign_extend( + smt2_constantt::make(to_integer_bits - from_integer_bits)), + {smt2_function_applicationt{ + smt2_extract(from_width - 1, from_fraction_bits), + {smt2_symbolt("?tcop")}}}); + } + }(), + smt2_concat( + [&]() -> smt2_astt { + if(to_fraction_bits <= from_fraction_bits) + { + return smt2_function_applicationt{ + smt2_extract( + from_fraction_bits - 1, + from_fraction_bits - to_fraction_bits), + {smt2_symbolt("?tcop")}}; + } + else + { + INVARIANT( + to_fraction_bits > from_fraction_bits, + "to_fraction_bits should be greater than from_fraction_bits " + "as " + "the other case has been handled above"); + return smt2_concat( + smt2_function_applicationt{ + smt2_extract(from_fraction_bits - 1, 0), + {convert_expr(src)}}, + smt2_bv(0, to_fraction_bits - from_fraction_bits)); + } + }(), + smt2_symbolt{"TODO: missing argument"}))); } else UNEXPECTEDCASE("unexpected typecast to fixedbv"); @@ -2349,7 +2292,7 @@ void smt2_convt::convert_typecast(const typecast_exprt &expr) if(src_type.id()==ID_pointer) // pointer to pointer { // this just passes through - convert_expr(src); + return convert_expr(src); } else if( src_type.id() == ID_unsignedbv || src_type.id() == ID_signedbv || @@ -2360,20 +2303,17 @@ void smt2_convt::convert_typecast(const typecast_exprt &expr) std::size_t from_width=boolbv_width(src_type); if(from_width==to_width) - convert_expr(src); + return convert_expr(src); else if(from_widthto_width { - out << "((_ extract " << to_width << " 0) "; - convert_expr(src); - out << ")"; // extract + return smt2_function_applicationt{smt2_extract(to_width, 0), + {convert_expr(src)}}; } } else @@ -2401,31 +2341,28 @@ void smt2_convt::convert_typecast(const typecast_exprt &expr) mp_integer significand; mp_integer exponent; - out << "(ite "; - convert_expr(src); - out << " "; - - significand = 1; - exponent = 0; - a.build(significand, exponent); - val.set_value(integer2bvrep(a.pack(), a.spec.width())); - - convert_constant(val); - out << " "; - - significand = 0; - exponent = 0; - a.build(significand, exponent); - val.set_value(integer2bvrep(a.pack(), a.spec.width())); - - convert_constant(val); - out << ")"; + return smt2_ite( + convert_expr(src), + [&]() { + significand = 1; + exponent = 0; + a.build(significand, exponent); + val.set_value(integer2bvrep(a.pack(), a.spec.width())); + return convert_constant(val); + }(), + [&]() { + significand = 0; + exponent = 0; + a.build(significand, exponent); + val.set_value(integer2bvrep(a.pack(), a.spec.width())); + return convert_constant(val); + }()); } else if(src_type.id()==ID_c_bool) { // turn into proper bool const typecast_exprt tmp(src, bool_typet()); - convert_typecast(typecast_exprt(tmp, dest_type)); + return convert_typecast(typecast_exprt(tmp, dest_type)); } else if(src_type.id() == ID_bv) { @@ -2436,13 +2373,13 @@ void smt2_convt::convert_typecast(const typecast_exprt &expr) if(use_FPA_theory) { - out << "((_ to_fp " << dest_floatbv_type.get_e() << " " - << dest_floatbv_type.get_f() + 1 << ") "; - convert_expr(src); - out << ')'; + return smt2_function_applicationt{ + smt2_identifiert{smt2_symbolt{"to_fp"}, + {smt2_constantt::make(dest_floatbv_type.get_e())}}, + {convert_expr(src)}}; } else - convert_expr(src); + return convert_expr(src); } else UNEXPECTEDCASE("Unknown typecast "+src_type.id_string()+" -> float"); @@ -2451,9 +2388,8 @@ void smt2_convt::convert_typecast(const typecast_exprt &expr) { if(src_type.id()==ID_bool) { - out << "(ite "; - convert_expr(src); - out <<" 1 0)"; + return smt2_ite( + convert_expr(src), smt2_constantt::make(1), smt2_constantt::make(0)); } else UNEXPECTEDCASE("Unknown typecast "+src_type.id_string()+" -> integer"); @@ -2464,20 +2400,22 @@ void smt2_convt::convert_typecast(const typecast_exprt &expr) std::size_t to_width=boolbv_width(dest_type); if(from_width==to_width) - convert_expr(src); // ignore + return convert_expr(src); // ignore else { typet t=c_bit_field_replacement_type(to_c_bit_field_type(dest_type), ns); typecast_exprt tmp(typecast_exprt(src, t), dest_type); - convert_typecast(tmp); + return convert_typecast(tmp); } } else UNEXPECTEDCASE( "TODO typecast8 "+src_type.id_string()+" -> "+dest_type.id_string()); + UNREACHABLE; } -void smt2_convt::convert_floatbv_typecast(const floatbv_typecast_exprt &expr) +smt2_astt +smt2_convt::convert_floatbv_typecast(const floatbv_typecast_exprt &expr) { const exprt &src=expr.op(); // const exprt &rounding_mode=expr.rounding_mode(); @@ -2513,15 +2451,14 @@ void smt2_convt::convert_floatbv_typecast(const floatbv_typecast_exprt &expr) if(use_FPA_theory) { - out << "((_ to_fp " << dst.get_e() << " " - << dst.get_f() + 1 << ") "; - convert_rounding_mode_FPA(expr.op1()); - out << " "; - convert_expr(src); - out << ")"; + return smt2_function_applicationt( + smt2_identifiert{smt2_symbolt{"to_fp"}, + {smt2_constantt::make(dst.get_e()), + smt2_constantt::make(dst.get_f() + 1)}}, + {convert_rounding_mode_FPA(expr.op1()), convert_expr(src)}); } else - convert_floatbv(expr); + return convert_floatbv(expr); } else if(src_type.id()==ID_unsignedbv) { @@ -2552,7 +2489,7 @@ void smt2_convt::convert_floatbv_typecast(const floatbv_typecast_exprt &expr) out << ")"; } else - convert_floatbv(expr); + return convert_floatbv(expr); } else if(src_type.id()==ID_signedbv) { @@ -2570,7 +2507,7 @@ void smt2_convt::convert_floatbv_typecast(const floatbv_typecast_exprt &expr) out << ")"; } else - convert_floatbv(expr); + return convert_floatbv(expr); } else if(src_type.id()==ID_c_enum_tag) { @@ -2582,7 +2519,7 @@ void smt2_convt::convert_floatbv_typecast(const floatbv_typecast_exprt &expr) typecast_exprt( src, ns.follow_tag(to_c_enum_tag_type(src_type)).subtype()); - convert_floatbv_typecast(tmp); + return convert_floatbv_typecast(tmp); } else UNEXPECTEDCASE( @@ -2600,7 +2537,7 @@ void smt2_convt::convert_floatbv_typecast(const floatbv_typecast_exprt &expr) out << ")"; } else - convert_floatbv(expr); + return convert_floatbv(expr); } else if(dest_type.id()==ID_unsignedbv) { @@ -2614,16 +2551,17 @@ void smt2_convt::convert_floatbv_typecast(const floatbv_typecast_exprt &expr) out << ")"; } else - convert_floatbv(expr); + return convert_floatbv(expr); } else { UNEXPECTEDCASE( "TODO typecast12 "+src_type.id_string()+" -> "+dest_type.id_string()); } + UNREACHABLE; } -void smt2_convt::convert_struct(const struct_exprt &expr) +smt2_astt smt2_convt::convert_struct(const struct_exprt &expr) { const struct_typet &struct_type = to_struct_type(ns.follow(expr.type())); @@ -2642,52 +2580,43 @@ void smt2_convt::convert_struct(const struct_exprt &expr) const std::string &smt_typename = datatype_map.at(struct_type); // use the constructor for the Z3 datatype - out << "(mk-" << smt_typename; + auto node = smt2_function_applicationt( + smt2_identifiert{smt2_symbolt{"mk-" + smt_typename}}, {}); - std::size_t i=0; - for(struct_typet::componentst::const_iterator - it=components.begin(); - it!=components.end(); - it++, i++) - { - out << " "; - convert_expr(expr.operands()[i]); - } + for(std::size_t i = 0; i < components.size(); ++i) + node.add_argument(convert_expr(expr.operands()[i])); - out << ")"; + return std::move(node); } else { if(components.size()==1) - convert_expr(expr.op0()); + return convert_expr(expr.op0()); else { + auto node = convert_expr(expr.op0()); + // SMT-LIB 2 concat is binary only - for(std::size_t i=components.size(); i>1; i--) + for(std::size_t i = 1; i < components.size(); ++i) { - out << "(concat "; - - exprt op=expr.operands()[i-1]; - - // may need to flatten array-theory arrays in there - if(op.type().id() == ID_array) - flatten_array(op); - else - convert_expr(op); - - out << " "; + node = smt2_concat( + [&]() { + exprt op = expr.operands()[i]; + // may need to flatten array-theory arrays in there + if(op.type().id() == ID_array) + return flatten_array(op); + return convert_expr(op); + }(), + std::move(node)); } - convert_expr(expr.op0()); - - for(std::size_t i=1; i(to_constant_expr(size_expr)); CHECK_RETURN_WITH_DIAGNOSTICS(size != 0, "can't convert zero-sized array"); - out << "(let ((?far "; - convert_expr(expr); - out << ")) "; + auto concatenation = smt2_select( + smt2_symbolt("?far"), + convert_expr(from_integer(0, array_type.size().type()))); + for(mp_integer i = 1; i < size; ++i) + { + concatenation = smt2_concat( + smt2_select( + smt2_symbolt("?far"), + convert_expr(from_integer(i - 1, array_type.size().type()))), + std::move(concatenation)); + } + return smt2_lett( + smt2_listt>{ + {smt2_pairt{smt2_symbolt("?far"), + convert_expr(expr)}}}, + std::move(concatenation)); +} - for(mp_integer i=size; i!=0; --i) - { - if(i!=1) - out << "(concat "; - out << "(select ?far "; - convert_expr(from_integer(i-1, array_type.size().type())); - out << ")"; - if(i!=1) - out << " "; - } - - // close the many parentheses - for(mp_integer i=size; i>1; --i) - out << ")"; - - out << ")"; // let -} - -void smt2_convt::convert_union(const union_exprt &expr) +smt2_astt smt2_convt::convert_union(const union_exprt &expr) { const union_typet &union_type = to_union_type(ns.follow(expr.type())); const exprt &op=expr.op(); @@ -2733,7 +2658,7 @@ void smt2_convt::convert_union(const union_exprt &expr) if(total_width==member_width) { - flatten2bv(op); + return flatten2bv(op); } else { @@ -2743,15 +2668,11 @@ void smt2_convt::convert_union(const union_exprt &expr) "total_width should be greater than member_width as member_width can be" "at most as large as total_width and the other case has been handled " "above"); - out << "(concat "; - out << "(_ bv0 " - << (total_width-member_width) << ") "; - flatten2bv(op); - out << ")"; + return smt2_concat(smt2_bv(0, total_width - member_width), flatten2bv(op)); } } -void smt2_convt::convert_constant(const constant_exprt &expr) +smt2_astt smt2_convt::convert_constant(const constant_exprt &expr) { const typet &expr_type=expr.type(); @@ -2766,17 +2687,14 @@ void smt2_convt::convert_constant(const constant_exprt &expr) const std::size_t width = boolbv_width(expr_type); const mp_integer value = bvrep2integer(expr.get_value(), width, false); - - out << "(_ bv" << value - << " " << width << ")"; + return smt2_bv(value, width); } else if(expr_type.id()==ID_fixedbv) { const fixedbv_spect spec(to_fixedbv_type(expr_type)); const mp_integer v = bvrep2integer(expr.get_value(), spec.width, false); - - out << "(_ bv" << v << " " << spec.width << ")"; + return smt2_bv(v, spec.width); } else if(expr_type.id()==ID_floatbv) { @@ -2804,14 +2722,20 @@ void smt2_convt::convert_constant(const constant_exprt &expr) if(v.is_NaN()) { - out << "(_ NaN " << e << " " << f << ")"; + return smt2_identifiert{ + smt2_symbolt{"NaN"}, + {smt2_constantt::make(e), smt2_constantt::make(f)}}; } else if(v.is_infinity()) { if(v.get_sign()) - out << "(_ -oo " << e << " " << f << ")"; + return smt2_identifiert( + smt2_symbolt("-oo"), + {smt2_constantt::make(e), smt2_constantt::make(f)}); else - out << "(_ +oo " << e << " " << f << ")"; + return smt2_identifiert( + smt2_symbolt("+oo"), + {smt2_constantt::make(e), smt2_constantt::make(f)}); } else { @@ -2819,11 +2743,11 @@ void smt2_convt::convert_constant(const constant_exprt &expr) mp_integer binary = v.pack(); std::string binaryString(integer2binary(v.pack(), v.spec.width())); - - out << "(fp " - << "#b" << binaryString.substr(0, 1) << " " - << "#b" << binaryString.substr(1, e) << " " - << "#b" << binaryString.substr(1+e, f-1) << ")"; + return smt2_identifiert( + smt2_symbolt{"fp"}, + {smt2_binary_literalt(binaryString.substr(0, 1)), + smt2_binary_literalt(binaryString.substr(1, e)), + smt2_binary_literalt(binaryString.substr(1 + e, f - 1))}); } } else @@ -2831,7 +2755,7 @@ void smt2_convt::convert_constant(const constant_exprt &expr) // produce corresponding bit-vector const ieee_float_spect spec(floatbv_type); const mp_integer v = bvrep2integer(expr.get_value(), spec.width(), false); - out << "(_ bv" << v << " " << spec.width() << ")"; + return smt2_bv(v, spec.width()); } } else if(expr_type.id()==ID_pointer) @@ -2840,8 +2764,7 @@ void smt2_convt::convert_constant(const constant_exprt &expr) if(value==ID_NULL) { - out << "(_ bv0 " << boolbv_width(expr_type) - << ")"; + return smt2_bv(0, boolbv_width(expr_type)); } else UNEXPECTEDCASE("unknown pointer constant: "+id2string(value)); @@ -2849,9 +2772,9 @@ void smt2_convt::convert_constant(const constant_exprt &expr) else if(expr_type.id()==ID_bool) { if(expr.is_true()) - out << "true"; + return smt2_symbolt("true"); else if(expr.is_false()) - out << "false"; + return smt2_symbolt("false"); else UNEXPECTEDCASE("unknown Boolean constant"); } @@ -2859,7 +2782,7 @@ void smt2_convt::convert_constant(const constant_exprt &expr) { defined_expressionst::const_iterator it=defined_expressions.find(expr); CHECK_RETURN(it != defined_expressions.end()); - out << it->second; + return smt2_symbolt(id2string(it->second)); } else if(expr_type.id()==ID_rational) { @@ -2867,41 +2790,40 @@ void smt2_convt::convert_constant(const constant_exprt &expr) size_t pos=value.find("/"); if(pos==std::string::npos) - out << value << ".0"; + return smt2_symbolt(value + ".0"); else { - out << "(/ " << value.substr(0, pos) << ".0 " - << value.substr(pos+1) << ".0)"; + return smt2_function_applicationt( + smt2_identifiert{smt2_symbolt{"/"}}, + {smt2_symbolt(value.substr(0, pos) + ".0"), + smt2_symbolt(value.substr(pos + 1) + ".0")}); } } else if(expr_type.id()==ID_integer) { - out << expr.get_value(); + return smt2_symbolt(id2string(expr.get_value())); } else UNEXPECTEDCASE("unknown constant: "+expr_type.id_string()); + UNREACHABLE; } -void smt2_convt::convert_mod(const mod_exprt &expr) +smt2_astt smt2_convt::convert_mod(const mod_exprt &expr) { if(expr.type().id()==ID_unsignedbv || expr.type().id()==ID_signedbv) { if(expr.type().id()==ID_unsignedbv) - out << "(bvurem "; - else - out << "(bvsrem "; - - convert_expr(expr.op0()); - out << " "; - convert_expr(expr.op1()); - out << ")"; + { + return smt2_bvurem(convert_expr(expr.op0()), convert_expr(expr.op1())); + } + return smt2_bvsrem(convert_expr(expr.op0()), convert_expr(expr.op1())); } else UNEXPECTEDCASE("unsupported type for mod: "+expr.type().id_string()); } -void smt2_convt::convert_is_dynamic_object(const exprt &expr) +smt2_astt smt2_convt::convert_is_dynamic_object(const exprt &expr) { std::vector dynamic_objects; pointer_logic.get_dynamic_objects(dynamic_objects); @@ -2911,38 +2833,38 @@ void smt2_convt::convert_is_dynamic_object(const exprt &expr) "is_dynamic_object expression should have one operand"); if(dynamic_objects.empty()) - out << "false"; - else - { - std::size_t pointer_width=boolbv_width(expr.op0().type()); - - out << "(let ((?obj ((_ extract " - << pointer_width-1 << " " - << pointer_width-config.bv_encoding.object_bits << ") "; - convert_expr(expr.op0()); - out << "))) "; - - if(dynamic_objects.size()==1) - { - out << "(= (_ bv" << dynamic_objects.front() - << " " << config.bv_encoding.object_bits << ") ?obj)"; - } - else - { - out << "(or"; - + return smt2_symbolt("false"); + + std::size_t pointer_width = boolbv_width(expr.op0().type()); + + return smt2_lett( + smt2_listt>{ + {smt2_pairt{ + smt2_symbolt("?obj"), + smt2_function_applicationt{ + smt2_extract( + pointer_width - 1, pointer_width - config.bv_encoding.object_bits), + {convert_expr(expr.op0())}}}}}, + [&]() -> smt2_astt { + if(dynamic_objects.size() == 1) + { + return smt2_eq( + smt2_bv(dynamic_objects.front(), config.bv_encoding.object_bits), + smt2_symbolt("?obj")); + } + auto node = + smt2_function_applicationt(smt2_identifiert{smt2_symbolt{"or"}}, {}); for(const auto &object : dynamic_objects) - out << " (= (_ bv" << object - << " " << config.bv_encoding.object_bits << ") ?obj)"; - - out << ")"; // or - } - - out << ")"; // let - } + { + node.add_argument(smt2_eq( + smt2_bv(object, config.bv_encoding.object_bits), + smt2_symbolt("?obj"))); + } + return std::move(node); + }()); } -void smt2_convt::convert_relation(const exprt &expr) +smt2_astt smt2_convt::convert_relation(const exprt &expr) { PRECONDITION(expr.operands().size() == 2); @@ -2952,97 +2874,89 @@ void smt2_convt::convert_relation(const exprt &expr) op_type.id()==ID_pointer || op_type.id()==ID_bv) { - out << "("; - if(expr.id()==ID_le) - out << "bvule"; - else if(expr.id()==ID_lt) - out << "bvult"; - else if(expr.id()==ID_ge) - out << "bvuge"; - else if(expr.id()==ID_gt) - out << "bvugt"; - - out << " "; - convert_expr(expr.op0()); - out << " "; - convert_expr(expr.op1()); - out << ")"; + auto function_name = [&]() { + if(expr.id() == ID_le) + return smt2_symbolt{"bvule"}; + else if(expr.id() == ID_lt) + return smt2_symbolt{"bvult"}; + else if(expr.id() == ID_ge) + return smt2_symbolt{"bvuge"}; + else if(expr.id() == ID_gt) + return smt2_symbolt{"bvugt"}; + UNREACHABLE; + }(); + + return smt2_function_applicationt( + smt2_identifiert{std::move(function_name)}, + {convert_expr(expr.op0()), convert_expr(expr.op1())}); } else if(op_type.id()==ID_signedbv || op_type.id()==ID_fixedbv) { - out << "("; - if(expr.id()==ID_le) - out << "bvsle"; - else if(expr.id()==ID_lt) - out << "bvslt"; - else if(expr.id()==ID_ge) - out << "bvsge"; - else if(expr.id()==ID_gt) - out << "bvsgt"; - - out << " "; - convert_expr(expr.op0()); - out << " "; - convert_expr(expr.op1()); - out << ")"; + auto function_name = [&]() { + if(expr.id() == ID_le) + return smt2_symbolt("bvsle"); + else if(expr.id() == ID_lt) + return smt2_symbolt("bvslt"); + else if(expr.id() == ID_ge) + return smt2_symbolt("bvsge"); + else if(expr.id() == ID_gt) + return smt2_symbolt("bvsgt"); + UNREACHABLE; + }(); + + return smt2_function_applicationt( + smt2_identifiert{std::move(function_name)}, + {convert_expr(expr.op0()), convert_expr(expr.op1())}); } else if(op_type.id()==ID_floatbv) { if(use_FPA_theory) { - out << "("; - if(expr.id()==ID_le) - out << "fp.leq"; - else if(expr.id()==ID_lt) - out << "fp.lt"; - else if(expr.id()==ID_ge) - out << "fp.geq"; - else if(expr.id()==ID_gt) - out << "fp.gt"; + auto function_name = [&]() { + if(expr.id() == ID_le) + return smt2_symbolt("fp.leq"); + else if(expr.id() == ID_lt) + return smt2_symbolt("fp.lt"); + else if(expr.id() == ID_ge) + return smt2_symbolt("fp.geq"); + else if(expr.id() == ID_gt) + return smt2_symbolt("fp.gt"); + UNREACHABLE; + }(); - out << " "; - convert_expr(expr.op0()); - out << " "; - convert_expr(expr.op1()); - out << ")"; + return smt2_function_applicationt( + smt2_identifiert{std::move(function_name)}, + {convert_expr(expr.op0()), convert_expr(expr.op1())}); } else - convert_floatbv(expr); + return convert_floatbv(expr); } else if(op_type.id()==ID_rational || op_type.id()==ID_integer) { - out << "("; - out << expr.id(); - - out << " "; - convert_expr(expr.op0()); - out << " "; - convert_expr(expr.op1()); - out << ")"; + return smt2_function_applicationt( + smt2_identifiert{smt2_symbolt{expr.id()}}, + {convert_expr(expr.op0()), convert_expr(expr.op1())}); } else UNEXPECTEDCASE( "unsupported type for "+expr.id_string()+": "+op_type.id_string()); + UNREACHABLE; } -void smt2_convt::convert_plus(const plus_exprt &expr) +smt2_astt smt2_convt::convert_plus(const plus_exprt &expr) { if( expr.type().id() == ID_rational || expr.type().id() == ID_integer || expr.type().id() == ID_real) { // these are multi-ary in SMT-LIB2 - out << "(+"; - + smt2_function_applicationt function{smt2_identifiert{smt2_symbolt{ID_plus}}, + {}}; for(const auto &op : expr.operands()) - { - out << ' '; - convert_expr(op); - } - - out << ')'; + function.add_argument(convert_expr(op)); + return std::move(function); } else if( expr.type().id() == ID_unsignedbv || expr.type().id() == ID_signedbv || @@ -3052,16 +2966,9 @@ void smt2_convt::convert_plus(const plus_exprt &expr) // but at least MathSat doesn't like that. if(expr.operands().size() == 2) { - out << "(bvadd "; - convert_expr(expr.op0()); - out << " "; - convert_expr(expr.op1()); - out << ")"; - } - else - { - convert_plus(to_plus_expr(make_binary(expr))); + return smt2_bvadd(convert_expr(expr.op0()), convert_expr(expr.op1())); } + return convert_plus(to_plus_expr(make_binary(expr))); } else if(expr.type().id() == ID_floatbv) { @@ -3072,57 +2979,44 @@ void smt2_convt::convert_plus(const plus_exprt &expr) } else if(expr.type().id() == ID_pointer) { - if(expr.operands().size() == 2) - { - exprt p = expr.op0(), i = expr.op1(); + if(expr.operands().size() != 2) + return convert_plus(to_plus_expr(make_binary(expr))); - if(p.type().id() != ID_pointer) - p.swap(i); + exprt p = expr.op0(), i = expr.op1(); - DATA_INVARIANT( - p.type().id() == ID_pointer, - "one of the operands should have pointer type"); + if(p.type().id() != ID_pointer) + p.swap(i); - const auto element_size = pointer_offset_size(expr.type().subtype(), ns); - CHECK_RETURN(element_size.has_value() && *element_size >= 1); + DATA_INVARIANT( + p.type().id() == ID_pointer, + "one of the operands should have pointer type"); - out << "(bvadd "; - convert_expr(p); - out << " "; + const auto element_size = pointer_offset_size(expr.type().subtype(), ns); + CHECK_RETURN(element_size.has_value() && *element_size >= 1); - if(*element_size >= 2) - { - out << "(bvmul "; - convert_expr(i); - out << " (_ bv" << *element_size << " " << boolbv_width(expr.type()) - << "))"; - } - else - convert_expr(i); + auto second_element = [&]() { + if(*element_size < 2) + return convert_expr(i); + return smt2_bvmul( + convert_expr(i), smt2_bv(*element_size, boolbv_width(expr.type()))); + }(); - out << ')'; - } - else - { - convert_plus(to_plus_expr(make_binary(expr))); - } + return smt2_bvadd(convert_expr(p), std::move(second_element)); } else if(expr.type().id() == ID_vector) { const vector_typet &vector_type = to_vector_type(expr.type()); - mp_integer size = numeric_cast_v(vector_type.size()); - typet index_type = vector_type.size().type(); - if(use_datatypes) - { + auto function_name = [&]() { + if(!use_datatypes) + return smt2_symbolt("concat"); const std::string &smt_typename = datatype_map.at(vector_type); - - out << "(mk-" << smt_typename; - } - else - out << "(concat"; + return smt2_symbolt("mk-" + smt_typename); + }(); + smt2_function_applicationt function{ + smt2_identifiert{std::move(function_name)}, {}}; // add component-by-component for(mp_integer i = 0; i != size; ++i) @@ -3133,13 +3027,11 @@ void smt2_convt::convert_plus(const plus_exprt &expr) summands.push_back(index_exprt( op, from_integer(size - i - 1, index_type), vector_type.subtype())); - plus_exprt tmp(std::move(summands), vector_type.subtype()); - - out << " "; - convert_expr(tmp); + function.add_argument( + convert_expr(plus_exprt(std::move(summands), vector_type.subtype()))); } - out << ")"; // mk-... or concat + return std::move(function); } else UNEXPECTEDCASE("unsupported type for +: " + expr.type().id_string()); @@ -3149,7 +3041,7 @@ void smt2_convt::convert_plus(const plus_exprt &expr) /// use_FPA_theory is enabled /// \par parameters: The expression representing the rounding mode. /// \return SMT-LIB output to out. -void smt2_convt::convert_rounding_mode_FPA(const exprt &expr) +smt2_astt smt2_convt::convert_rounding_mode_FPA(const exprt &expr) { PRECONDITION(use_FPA_theory); @@ -3169,13 +3061,13 @@ void smt2_convt::convert_rounding_mode_FPA(const exprt &expr) mp_integer value = numeric_cast_v(cexpr); if(value==0) - out << "roundNearestTiesToEven"; + return smt2_symbolt{"roundNearestTiesToEven"}; else if(value==1) - out << "roundTowardNegative"; + return smt2_symbolt{"roundTowardNegative"}; else if(value==2) - out << "roundTowardPositive"; + return smt2_symbolt{"roundTowardPositive"}; else if(value==3) - out << "roundTowardZero"; + return smt2_symbolt{"roundTowardZero"}; else INVARIANT_WITH_DIAGNOSTICS( false, @@ -3186,27 +3078,23 @@ void smt2_convt::convert_rounding_mode_FPA(const exprt &expr) { std::size_t width=to_bitvector_type(expr.type()).get_width(); + auto converted = convert_expr(expr); // Need to make the choice above part of the model - out << "(ite (= (_ bv0 " << width << ") "; - convert_expr(expr); - out << ") roundNearestTiesToEven "; - - out << "(ite (= (_ bv1 " << width << ") "; - convert_expr(expr); - out << ") roundTowardNegative "; - - out << "(ite (= (_ bv2 " << width << ") "; - convert_expr(expr); - out << ") roundTowardPositive "; - - // TODO: add some kind of error checking here - out << "roundTowardZero"; - - out << ")))"; + return smt2_ite( + smt2_eq(smt2_bv(0, width), converted), + smt2_symbolt{"roundNearestTiesToEven"}, + smt2_ite( + smt2_eq(smt2_bv(1, width), converted), + smt2_symbolt{"roundTowardNegative"}, + smt2_ite( + smt2_eq(smt2_bv(2, width), converted), + smt2_symbolt{"roundTowardPositve"}, + // TODO: add some kind of error checking here + smt2_symbolt{"roundTowardZero"}))); } } -void smt2_convt::convert_floatbv_plus(const ieee_float_op_exprt &expr) +smt2_astt smt2_convt::convert_floatbv_plus(const ieee_float_op_exprt &expr) { const typet &type=expr.type(); @@ -3219,13 +3107,10 @@ void smt2_convt::convert_floatbv_plus(const ieee_float_op_exprt &expr) { if(type.id()==ID_floatbv) { - out << "(fp.add "; - convert_rounding_mode_FPA(expr.rounding_mode()); - out << " "; - convert_expr(expr.lhs()); - out << " "; - convert_expr(expr.rhs()); - out << ")"; + return smt2_fp_add( + convert_rounding_mode_FPA(expr.rounding_mode()), + convert_expr(expr.lhs()), + convert_expr(expr.rhs())); } else if(type.id()==ID_complex) { @@ -3242,18 +3127,15 @@ void smt2_convt::convert_floatbv_plus(const ieee_float_op_exprt &expr) type.id_string()); } else - convert_floatbv(expr); + return convert_floatbv(expr); + UNREACHABLE; } -void smt2_convt::convert_minus(const minus_exprt &expr) +smt2_astt smt2_convt::convert_minus(const minus_exprt &expr) { if(expr.type().id()==ID_integer) { - out << "(- "; - convert_expr(expr.op0()); - out << " "; - convert_expr(expr.op1()); - out << ")"; + return smt2_minus(convert_expr(expr.op0()), convert_expr(expr.op1())); } else if(expr.type().id()==ID_unsignedbv || expr.type().id()==ID_signedbv || @@ -3266,31 +3148,24 @@ void smt2_convt::convert_minus(const minus_exprt &expr) auto element_size = pointer_offset_size(expr.op0().type().subtype(), ns); CHECK_RETURN(element_size.has_value() && *element_size >= 1); - if(*element_size >= 2) - out << "(bvsdiv "; INVARIANT( boolbv_width(expr.op0().type()) == boolbv_width(expr.type()), "bitvector width of operand shall be equal to the bitvector width of " "the expression"); - out << "(bvsub "; - convert_expr(expr.op0()); - out << " "; - convert_expr(expr.op1()); - out << ")"; + auto sub = smt2_bvsub(convert_expr(expr.op0()), convert_expr(expr.op1())); if(*element_size >= 2) - out << " (_ bv" << *element_size << " " << boolbv_width(expr.type()) - << "))"; + { + return smt2_bvsdiv( + std::move(sub), smt2_bv(*element_size, boolbv_width(expr.type()))); + } + return sub; } else { - out << "(bvsub "; - convert_expr(expr.op0()); - out << " "; - convert_expr(expr.op1()); - out << ")"; + return smt2_bvsub(convert_expr(expr.op0()), convert_expr(expr.op1())); } } else if(expr.type().id()==ID_floatbv) @@ -3312,14 +3187,16 @@ void smt2_convt::convert_minus(const minus_exprt &expr) typet index_type=vector_type.size().type(); - if(use_datatypes) - { - const std::string &smt_typename = datatype_map.at(vector_type); - - out << "(mk-" << smt_typename; - } - else - out << "(concat"; + auto function_name = [&]() { + if(use_datatypes) + { + const std::string &smt_typename = datatype_map.at(vector_type); + return smt2_symbolt{"mk-" + smt_typename}; + } + return smt2_symbolt{"concat"}; + }(); + smt2_function_applicationt node{smt2_identifiert{std::move(function_name)}, + {}}; // subtract component-by-component for(mp_integer i=0; i!=size; ++i) @@ -3331,18 +3208,15 @@ void smt2_convt::convert_minus(const minus_exprt &expr) *it, from_integer(size-i-1, index_type), vector_type.subtype())); - - out << " "; - convert_expr(tmp); + node.add_argument(convert_expr(tmp)); } - - out << ")"; // mk-... or concat + return std::move(node); } else UNEXPECTEDCASE("unsupported type for -: "+expr.type().id_string()); } -void smt2_convt::convert_floatbv_minus(const ieee_float_op_exprt &expr) +smt2_astt smt2_convt::convert_floatbv_minus(const ieee_float_op_exprt &expr) { DATA_INVARIANT( expr.type().id() == ID_floatbv, @@ -3350,50 +3224,39 @@ void smt2_convt::convert_floatbv_minus(const ieee_float_op_exprt &expr) if(use_FPA_theory) { - out << "(fp.sub "; - convert_rounding_mode_FPA(expr.rounding_mode()); - out << " "; - convert_expr(expr.lhs()); - out << " "; - convert_expr(expr.rhs()); - out << ")"; + return smt2_fp_sub( + convert_rounding_mode_FPA(expr.rounding_mode()), + convert_expr(expr.lhs()), + convert_expr(expr.rhs())); } else - convert_floatbv(expr); + return convert_floatbv(expr); + UNREACHABLE; } -void smt2_convt::convert_div(const div_exprt &expr) +smt2_astt smt2_convt::convert_div(const div_exprt &expr) { if(expr.type().id()==ID_unsignedbv || expr.type().id()==ID_signedbv) { if(expr.type().id()==ID_unsignedbv) - out << "(bvudiv "; - else - out << "(bvsdiv "; - - convert_expr(expr.op0()); - out << " "; - convert_expr(expr.op1()); - out << ")"; + { + return smt2_bvudiv(convert_expr(expr.op0()), convert_expr(expr.op1())); + } + return smt2_bvsdiv(convert_expr(expr.op0()), convert_expr(expr.op1())); } else if(expr.type().id()==ID_fixedbv) { fixedbv_spect spec(to_fixedbv_type(expr.type())); std::size_t fraction_bits=spec.get_fraction_bits(); - out << "((_ extract " << spec.width-1 << " 0) "; - out << "(bvsdiv "; - - out << "(concat "; - convert_expr(expr.op0()); - out << " (_ bv0 " << fraction_bits << ")) "; - - out << "((_ sign_extend " << fraction_bits << ") "; - convert_expr(expr.op1()); - out << ")"; - - out << "))"; + return smt2_function_applicationt{ + smt2_extract(spec.width - 1, 0), + {smt2_bvsdiv( + smt2_concat(convert_expr(expr.op0()), smt2_bv(0, fraction_bits)), + smt2_function_applicationt{ + smt2_sign_extend(smt2_constantt::make(fraction_bits)), + {convert_expr(expr.op1())}})}}; } else if(expr.type().id()==ID_floatbv) { @@ -3406,7 +3269,7 @@ void smt2_convt::convert_div(const div_exprt &expr) UNEXPECTEDCASE("unsupported type for /: "+expr.type().id_string()); } -void smt2_convt::convert_floatbv_div(const ieee_float_op_exprt &expr) +smt2_astt smt2_convt::convert_floatbv_div(const ieee_float_op_exprt &expr) { DATA_INVARIANT( expr.type().id() == ID_floatbv, @@ -3414,19 +3277,17 @@ void smt2_convt::convert_floatbv_div(const ieee_float_op_exprt &expr) if(use_FPA_theory) { - out << "(fp.div "; - convert_rounding_mode_FPA(expr.rounding_mode()); - out << " "; - convert_expr(expr.lhs()); - out << " "; - convert_expr(expr.rhs()); - out << ")"; + return smt2_fp_div( + convert_rounding_mode_FPA(expr.rounding_mode()), + convert_expr(expr.lhs()), + convert_expr(expr.rhs())); } else - convert_floatbv(expr); + return convert_floatbv(expr); + UNREACHABLE; } -void smt2_convt::convert_mult(const mult_exprt &expr) +smt2_astt smt2_convt::convert_mult(const mult_exprt &expr) { // re-write to binary if needed if(expr.operands().size()>2) @@ -3449,11 +3310,7 @@ void smt2_convt::convert_mult(const mult_exprt &expr) // Note that bvmul is really unsigned, // but this is irrelevant as we chop-off any extra result // bits. - out << "(bvmul "; - convert_expr(expr.op0()); - out << " "; - convert_expr(expr.op1()); - out << ")"; + return smt2_bvmul(convert_expr(expr.op0()), convert_expr(expr.op1())); } else if(expr.type().id()==ID_floatbv) { @@ -3466,42 +3323,31 @@ void smt2_convt::convert_mult(const mult_exprt &expr) { fixedbv_spect spec(to_fixedbv_type(expr.type())); std::size_t fraction_bits=spec.get_fraction_bits(); - - out << "((_ extract " - << spec.width+fraction_bits-1 << " " - << fraction_bits << ") "; - - out << "(bvmul "; - - out << "((_ sign_extend " << fraction_bits << ") "; - convert_expr(expr.op0()); - out << ") "; - - out << "((_ sign_extend " << fraction_bits << ") "; - convert_expr(expr.op1()); - out << ")"; - - out << "))"; // bvmul, extract + return smt2_function_applicationt{ + smt2_extract(spec.width + fraction_bits - 1, fraction_bits), + {smt2_bvmul( + smt2_function_applicationt{ + smt2_sign_extend(smt2_constantt::make(fraction_bits)), + {convert_expr(expr.op0())}}, + smt2_function_applicationt{ + smt2_sign_extend(smt2_constantt::make(fraction_bits)), + {convert_expr(expr.op1())}})}}; } else if(expr.type().id()==ID_rational || expr.type().id()==ID_integer || expr.type().id()==ID_real) { - out << "(*"; - - forall_operands(it, expr) - { - out << " "; - convert_expr(*it); - } + smt2_function_applicationt node(smt2_identifiert{smt2_symbolt{"*"}}, {}); - out << ")"; + for(const exprt &op : expr.operands()) + node.add_argument(convert_expr(op)); + return std::move(node); } else UNEXPECTEDCASE("unsupported type for *: "+expr.type().id_string()); } -void smt2_convt::convert_floatbv_mult(const ieee_float_op_exprt &expr) +smt2_astt smt2_convt::convert_floatbv_mult(const ieee_float_op_exprt &expr) { DATA_INVARIANT( expr.type().id() == ID_floatbv, @@ -3509,19 +3355,17 @@ void smt2_convt::convert_floatbv_mult(const ieee_float_op_exprt &expr) if(use_FPA_theory) { - out << "(fp.mul "; - convert_rounding_mode_FPA(expr.rounding_mode()); - out << " "; - convert_expr(expr.lhs()); - out << " "; - convert_expr(expr.rhs()); - out << ")"; + return smt2_fp_mul( + convert_rounding_mode_FPA(expr.rounding_mode()), + convert_expr(expr.lhs()), + convert_expr(expr.rhs())); } else - convert_floatbv(expr); + return convert_floatbv(expr); + UNREACHABLE; } -void smt2_convt::convert_with(const with_exprt &expr) +smt2_astt smt2_convt::convert_with(const with_exprt &expr) { // get rid of "with" that has more than three operands @@ -3553,13 +3397,11 @@ void smt2_convt::convert_with(const with_exprt &expr) if(use_array_theory(expr)) { - out << "(store "; - convert_expr(expr.old()); - out << " "; - convert_expr(typecast_exprt(expr.where(), array_type.size().type())); - out << " "; - convert_expr(expr.new_value()); - out << ")"; + return smt2_function_applicationt( + smt2_identifiert{smt2_symbolt{"store"}}, + {convert_expr(expr.old()), + convert_expr(typecast_exprt(expr.where(), array_type.size().type())), + convert_expr(expr.new_value())}); } else { @@ -3570,39 +3412,36 @@ void smt2_convt::convert_with(const with_exprt &expr) // We mask out the updated bits with AND, // and then OR-in the shifted new value. - - out << "(let ((distance? "; - out << "(bvmul (_ bv" << sub_width << " " << array_width << ") "; - - // SMT2 says that the shift distance needs to be as wide - // as the stuff we are shifting. - if(array_width>index_width) - { - out << "((_ zero_extend " << array_width-index_width << ") "; - convert_expr(expr.where()); - out << ")"; - } - else - { - out << "((_ extract " << array_width-1 << " 0) "; - convert_expr(expr.where()); - out << ")"; - } - - out << "))) "; // bvmul, distance? - - out << "(bvor "; - out << "(bvand "; - out << "(bvnot "; - out << "(bvshl (_ bv" << power(2, sub_width) - 1 << " " << array_width - << ") "; - out << "distance?)) "; // bvnot, bvlshl - convert_expr(expr.old()); - out << ") "; // bvand - out << "(bvshl "; - out << "((_ zero_extend " << array_width-sub_width << ") "; - convert_expr(expr.new_value()); - out << ") distance?)))"; // zero_extend, bvshl, bvor, let + return smt2_lett( + smt2_listt>{ + {smt2_pairt{ + smt2_symbolt("distance?"), + smt2_bvmul( + smt2_bv(sub_width, array_width), + [&]() { + // SMT2 says that the shift distance needs to be as wide + // as the stuff we are shifting. + if(array_width > index_width) + { + return smt2_function_applicationt{ + smt2_zero_extend(array_width - index_width), + {convert_expr(expr.where())}}; + } + return smt2_function_applicationt{ + smt2_extract(array_width - 1, 0), + {convert_expr(expr.where())}}; + }())}}}, + smt2_bvor( + smt2_bvand( + smt2_bvnot(smt2_bvshl( + smt2_bv(power(2, sub_width) - 1, array_width), + smt2_symbolt("distance?"))), + convert_expr(expr.old())), + smt2_bvshl( + smt2_function_applicationt{ + smt2_zero_extend(array_width - sub_width), + {convert_expr(expr.new_value())}}, + smt2_symbolt("distance?")))); } } else if(expr_type.id() == ID_struct || expr_type.id() == ID_struct_tag) @@ -3621,12 +3460,10 @@ void smt2_convt::convert_with(const with_exprt &expr) if(use_datatypes) { const std::string &smt_typename = datatype_map.at(expr_type); - - out << "(update-" << smt_typename << "." << component_name << " "; - convert_expr(expr.old()); - out << " "; - convert_expr(value); - out << ")"; + return smt2_function_applicationt( + smt2_identifiert{smt2_symbolt{"update-" + smt_typename + "." + + id2string(component_name)}}, + {convert_expr(expr.old()), convert_expr(value)}); } else { @@ -3636,44 +3473,47 @@ void smt2_convt::convert_with(const with_exprt &expr) boolbv_widtht::membert m= boolbv_width.get_member(struct_type, component_name); - out << "(let ((?withop "; - convert_expr(expr.old()); - out << ")) "; - - if(m.width==struct_width) - { - // the struct is the same as the member, no concat needed, - // ?withop won't be used - convert_expr(value); - } - else if(m.offset==0) - { - // the member is at the beginning - out << "(concat " - << "((_ extract " << (struct_width-1) << " " - << m.width << ") ?withop) "; - convert_expr(value); - out << ")"; // concat - } - else if(m.offset+m.width==struct_width) - { - // the member is at the end - out << "(concat "; - convert_expr(value); - out << " ((_ extract " << (m.offset - 1) << " 0) ?withop))"; - } - else - { - // most general case, need two concat-s - out << "(concat (concat " - << "((_ extract " << (struct_width-1) << " " - << (m.offset+m.width) << ") ?withop) "; - convert_expr(value); - out << ") ((_ extract " << (m.offset-1) << " 0) ?withop)"; - out << ")"; // concat - } - - out << ")"; // let ?withop + return smt2_lett( + smt2_listt>{ + {smt2_pairt{smt2_symbolt("?withop"), + convert_expr(expr.old())}}}, + [&]() { + if(m.width == struct_width) + { + // the struct is the same as the member, no concat needed, + // ?withop won't be used + return convert_expr(value); + } + else if(m.offset == 0) + { + // the member is at the beginning + return smt2_concat( + smt2_function_applicationt{ + smt2_extract(struct_width - 1, m.width), + {smt2_symbolt("?withop")}}, + convert_expr(value)); + } + else if(m.offset + m.width == struct_width) + { + // the member is at the end + return smt2_concat( + convert_expr(value), + smt2_function_applicationt{smt2_extract(m.offset - 1, 0), + {smt2_symbolt("?withop")}}); + } + else + { + // most general case, need two concat-s + return smt2_concat( + smt2_concat( + smt2_function_applicationt{ + smt2_extract(struct_width - 1, m.offset + m.width), + {smt2_symbolt("?withop")}}, + convert_expr(value)), + smt2_function_applicationt{smt2_extract(m.offset - 1, 0), + {smt2_symbolt("?withop")}}); + } + }()); } } else if(expr_type.id() == ID_union || expr_type.id() == ID_union_tag) @@ -3692,7 +3532,7 @@ void smt2_convt::convert_with(const with_exprt &expr) if(total_width==member_width) { - flatten2bv(value); + return flatten2bv(value); } else { @@ -3701,14 +3541,10 @@ void smt2_convt::convert_with(const with_exprt &expr) "total width should be greater than member_width as member_width is at " "most as large as total_width and the other case has been handled " "above"); - out << "(concat "; - out << "((_ extract " - << (total_width-1) - << " " << member_width << ") "; - convert_expr(expr.old()); - out << ") "; - flatten2bv(value); - out << ")"; + return smt2_concat( + smt2_function_applicationt{smt2_extract(total_width - 1, member_width), + {convert_expr(expr.old())}}, + flatten2bv(value)); } } else if(expr_type.id()==ID_bv || @@ -3768,14 +3604,14 @@ void smt2_convt::convert_with(const with_exprt &expr) expr.type().id_string()); } -void smt2_convt::convert_update(const exprt &expr) +smt2_astt smt2_convt::convert_update(const exprt &expr) { PRECONDITION(expr.operands().size() == 3); SMT2_TODO("smt2_convt::convert_update to be implemented"); } -void smt2_convt::convert_index(const index_exprt &expr) +smt2_astt smt2_convt::convert_index(const index_exprt &expr) { const typet &array_op_type = expr.array().type(); @@ -3787,21 +3623,20 @@ void smt2_convt::convert_index(const index_exprt &expr) { if(expr.type().id() == ID_bool && !use_array_of_bool) { - out << "(= "; - out << "(select "; - convert_expr(expr.array()); - out << " "; - convert_expr(typecast_exprt(expr.index(), array_type.size().type())); - out << ")"; - out << " #b1 #b0)"; + return smt2_function_applicationt( + smt2_identifiert{smt2_symbolt{"="}}, + {smt2_select( + convert_expr(expr.array()), + convert_expr( + typecast_exprt(expr.index(), array_type.size().type()))), + smt2_binary_literalt::make(1), + smt2_binary_literalt::make(0)}); } else { - out << "(select "; - convert_expr(expr.array()); - out << " "; - convert_expr(typecast_exprt(expr.index(), array_type.size().type())); - out << ")"; + return smt2_select( + convert_expr(expr.array()), + convert_expr(typecast_exprt(expr.index(), array_type.size().type()))); } } else @@ -3810,35 +3645,31 @@ void smt2_convt::convert_index(const index_exprt &expr) std::size_t array_width=boolbv_width(array_type); CHECK_RETURN(array_width != 0); - unflatten(wheret::BEGIN, array_type.subtype()); std::size_t sub_width=boolbv_width(array_type.subtype()); std::size_t index_width=boolbv_width(expr.index().type()); - out << "((_ extract " << sub_width-1 << " 0) "; - out << "(bvlshr "; - convert_expr(expr.array()); - out << " "; - out << "(bvmul (_ bv" << sub_width << " " << array_width << ") "; - - // SMT2 says that the shift distance must be the same as - // the width of what we shift. - if(array_width>index_width) - { - out << "((_ zero_extend " << array_width-index_width << ") "; - convert_expr(expr.index()); - out << ")"; // zero_extend - } - else - { - out << "((_ extract " << array_width-1 << " 0) "; - convert_expr(expr.index()); - out << ")"; // extract - } - - out << ")))"; // mult, bvlshr, extract - - unflatten(wheret::END, array_type.subtype()); + auto node = smt2_function_applicationt( + smt2_extract(sub_width - 1, 0), + {smt2_bvlshr( + convert_expr(expr.array()), + smt2_bvmul(smt2_bv(sub_width, array_width), [&] { + // SMT2 says that the shift distance must be the same as + // the width of what we shift. + if(array_width > index_width) + { + return smt2_function_applicationt{ + smt2_zero_extend(array_width - index_width), + {convert_expr(expr.index())}}; + } + else + { + return smt2_function_applicationt{ + smt2_extract(array_width - 1, 0), {convert_expr(expr.index())}}; + } + }()))}); + + return unflatten(array_type.subtype(), std::move(node)); } } else if(array_op_type.id()==ID_vector) @@ -3858,9 +3689,10 @@ void smt2_convt::convert_index(const index_exprt &expr) } else { - out << "(" << smt_typename << "." << *index_int << " "; - convert_expr(expr.array()); - out << ")"; + return smt2_function_applicationt{ + smt2_identifiert{smt2_symbolt( + smt_typename + "." + std::to_string(index_int->to_long()))}, + {convert_expr(expr.array())}}; } } else @@ -3873,7 +3705,7 @@ void smt2_convt::convert_index(const index_exprt &expr) false, "index with unsupported array type: " + array_op_type.id_string()); } -void smt2_convt::convert_member(const member_exprt &expr) +smt2_astt smt2_convt::convert_member(const member_exprt &expr) { const member_exprt &member_expr=to_member_expr(expr); const exprt &struct_op=member_expr.struct_op(); @@ -3890,12 +3722,11 @@ void smt2_convt::convert_member(const member_exprt &expr) if(use_datatypes) { const std::string &smt_typename = datatype_map.at(struct_type); - - out << "(" << smt_typename << "." - << struct_type.get_component(name).get_name() - << " "; - convert_expr(struct_op); - out << ")"; + const std::string &component = + id2string(struct_type.get_component(name).get_name()); + smt2_symbolt member_ast{std::string(smt_typename) + "." + component}; + return smt2_function_applicationt( + smt2_identifiert{std::move(member_ast)}, {convert_expr(struct_op)}); } else { @@ -3906,10 +3737,10 @@ void smt2_convt::convert_member(const member_exprt &expr) CHECK_RETURN_WITH_DIAGNOSTICS( member_offset.has_value(), "failed to get struct member offset"); - out << "((_ extract " << (member_offset.value() + member_width - 1) << " " - << member_offset.value() << ") "; - convert_expr(struct_op); - out << ")"; + return smt2_function_applicationt{ + smt2_extract( + member_offset.value() + member_width - 1, member_offset.value()), + {convert_expr(struct_op)}}; } } else if( @@ -3919,30 +3750,25 @@ void smt2_convt::convert_member(const member_exprt &expr) CHECK_RETURN_WITH_DIAGNOSTICS( width != 0, "failed to get union member width"); - unflatten(wheret::BEGIN, expr.type()); - - out << "((_ extract " - << (width-1) - << " 0) "; - convert_expr(struct_op); - out << ")"; - - unflatten(wheret::END, expr.type()); + return unflatten( + expr.type(), + smt2_function_applicationt{smt2_extract(width - 1, 0), + {convert_expr(struct_op)}}); } else UNEXPECTEDCASE( "convert_member on an unexpected type "+struct_op_type.id_string()); } -void smt2_convt::flatten2bv(const exprt &expr) +smt2_astt smt2_convt::flatten2bv(const exprt &expr) { const typet &type = expr.type(); if(type.id()==ID_bool) { - out << "(ite "; - convert_expr(expr); // this returns a Bool - out << " #b1 #b0)"; // this is a one-bit bit-vector + // expr returns a boolean and #b0 and #b1 are one-bit bit-vector + return smt2_ite( + convert_expr(expr), smt2_symbolt("#b1"), smt2_symbolt("#b0")); } else if(type.id()==ID_vector) { @@ -3954,26 +3780,27 @@ void smt2_convt::flatten2bv(const exprt &expr) const vector_typet &vector_type=to_vector_type(type); mp_integer size = numeric_cast_v(vector_type.size()); - - out << "(let ((?vflop "; - convert_expr(expr); - out << ")) "; - - out << "(concat"; - + smt2_function_applicationt concat( + smt2_identifiert{smt2_symbolt{"concat"}}, {}); for(mp_integer i=0; i!=size; ++i) { - out << " (" << smt_typename << "." << i << " ?vflop)"; + concat.add_argument( + smt2_function_applicationt{smt2_identifiert{smt2_symbolt( + smt_typename + "." + integer2string(i))}, + {smt2_symbolt("?vflop")}}); } - - out << "))"; // concat, let + return smt2_lett( + smt2_listt>{ + {smt2_pairt{smt2_symbolt("?vflop"), + convert_expr(expr)}}}, + std::move(concat)); } else - convert_expr(expr); // already a bv + return convert_expr(expr); // already a bv } else if(type.id()==ID_array) { - convert_expr(expr); + return convert_expr(expr); } else if(type.id() == ID_struct || type.id() == ID_struct_tag) { @@ -3983,33 +3810,33 @@ void smt2_convt::flatten2bv(const exprt &expr) // concatenate elements const struct_typet &struct_type = to_struct_type(ns.follow(type)); - - out << "(let ((?sflop "; - convert_expr(expr); - out << ")) "; - const struct_typet::componentst &components= struct_type.components(); + smt2_symbolt function_name{smt_typename + "." + + id2string(components[0].get_name())}; + smt2_astt concat_node = smt2_function_applicationt( + smt2_identifiert{std::move(function_name)}, {smt2_symbolt("?sflop")}); + // SMT-LIB 2 concat is binary only - for(std::size_t i=components.size(); i>1; i--) + for(std::size_t i = 0; i < components.size(); ++i) { - out << "(concat (" << smt_typename << "." - << components[i-1].get_name() << " ?sflop)"; - - out << " "; + concat_node = smt2_concat( + smt2_function_applicationt( + smt2_identifiert{smt2_symbolt( + smt_typename + "." + id2string(components[i - 1].get_name()))}, + {smt2_symbolt("?sflop")}), + std::move(concat_node)); } - out << "(" << smt_typename << "." - << components[0].get_name() << " ?sflop)"; - - for(std::size_t i=1; i>{ + {smt2_pairt{smt2_symbolt("?sflop"), + convert_expr(expr)}}}, + std::move(concat_node)); } else - convert_expr(expr); + return convert_expr(expr); } else if(type.id()==ID_floatbv) { @@ -4017,114 +3844,93 @@ void smt2_convt::flatten2bv(const exprt &expr) !use_FPA_theory, "floatbv expressions should be flattened when using FPA theory"); - convert_expr(expr); + return convert_expr(expr); } else - convert_expr(expr); + return convert_expr(expr); } -void smt2_convt::unflatten( - wheret where, - const typet &type, - unsigned nesting) +smt2_astt +smt2_convt::unflatten(const typet &type, smt2_astt ast, unsigned nesting) { if(type.id()==ID_bool) + return smt2_eq(std::move(ast), smt2_symbolt("#b1")); + + if(type.id() == ID_vector) { - if(where==wheret::BEGIN) - out << "(= "; // produces a bool - else - out << " #b1)"; - } - else if(type.id()==ID_vector) - { - if(use_datatypes) + if(!use_datatypes) { - const std::string &smt_typename = datatype_map.at(type); - - // extract elements - const vector_typet &vector_type=to_vector_type(type); - - std::size_t subtype_width=boolbv_width(vector_type.subtype()); - - mp_integer size = numeric_cast_v(vector_type.size()); - - if(where==wheret::BEGIN) - out << "(let ((?ufop" << nesting << " "; - else - { - out << ")) "; + // nothing to do, already a bv + return ast; + } - out << "(mk-" << smt_typename; + return smt2_lett( + smt2_listt>{ + {smt2_pairt{smt2_symbolt("?ufop"), + smt2_constantt::make(nesting)}}}, + [&]() { + const std::string &smt_typename = datatype_map.at(type); + // extract elements + const vector_typet &vector_type = to_vector_type(type); + std::size_t subtype_width = boolbv_width(vector_type.subtype()); + mp_integer size = numeric_cast_v(vector_type.size()); + smt2_function_applicationt mk_fun( + smt2_identifiert{smt2_symbolt{"mk-" + smt_typename}}, {}); std::size_t offset=0; for(mp_integer i=0; i!=size; ++i, offset+=subtype_width) { - out << " "; - unflatten(wheret::BEGIN, vector_type.subtype(), nesting+1); - out << "((_ extract " << offset+subtype_width-1 << " " - << offset << ") ?ufop" << nesting << ")"; - unflatten(wheret::END, vector_type.subtype(), nesting+1); + auto extract = smt2_function_applicationt( + smt2_extract(offset + subtype_width - 1, offset), + {smt2_symbolt("?ufop"), smt2_constantt::make(nesting)}); + mk_fun.add_argument( + unflatten(vector_type.subtype(), std::move(extract), nesting + 1)); } - - out << "))"; // mk-, let - } - } - else - { - // nop, already a bv - } + return mk_fun; + }()); } else if(type.id() == ID_struct || type.id() == ID_struct_tag) { - if(use_datatypes) + if(!use_datatypes) { - // extract members - if(where==wheret::BEGIN) - out << "(let ((?ufop" << nesting << " "; - else - { - out << ")) "; + // nothing to do, already a bv + return ast; + } + return smt2_lett( + smt2_listt>{ + {smt2_pairt{smt2_symbolt("?ufop"), + smt2_constantt::make(nesting)}}}, + [&]() { + // TODO ast is missing from here!!! + // extract members const std::string &smt_typename = datatype_map.at(type); - out << "(mk-" << smt_typename; - + smt2_function_applicationt mk_fun{ + smt2_identifiert{smt2_symbolt{"mk-" + smt_typename}}, {}}; const struct_typet &struct_type = to_struct_type(ns.follow(type)); - const struct_typet::componentst &components= struct_type.components(); std::size_t offset=0; - - std::size_t i=0; - for(struct_typet::componentst::const_iterator - it=components.begin(); - it!=components.end(); + std::size_t i = 0; + for(struct_typet::componentst::const_iterator it = components.begin(); + it != components.end(); it++, i++) { std::size_t member_width=boolbv_width(it->type()); - - out << " "; - unflatten(wheret::BEGIN, it->type(), nesting+1); - out << "((_ extract " << offset+member_width-1 << " " - << offset << ") ?ufop" << nesting << ")"; - unflatten(wheret::END, it->type(), nesting+1); - offset+=member_width; + smt2_function_applicationt extract_node{ + smt2_extract(offset + member_width - 1, offset), + {smt2_symbolt("?ufop"), smt2_constantt::make(nesting)}}; + mk_fun.add_argument( + unflatten(it->type(), std::move(extract_node), nesting + 1)); + offset += member_width; } - - out << "))"; // mk-, let - } - } - else - { - // nop, already a bv - } - } - else - { - // nop + return mk_fun; + }()); } + return ast; } void smt2_convt::set_to(const exprt &expr, bool value) @@ -4170,46 +3976,44 @@ void smt2_convt::set_to(const exprt &expr, bool value) CHECK_RETURN(id.type.is_nil()); id.type=equal_expr.lhs().type(); - find_symbols(id.type); - exprt prepared_rhs = prepare_for_convert_expr(equal_expr.rhs()); + for(const auto &command : find_symbols(id.type)) + out << *command; + const auto prepared_rhs_with_dependencies = + prepare_for_convert_expr(equal_expr.rhs()); + const exprt &prepared_rhs = prepared_rhs_with_dependencies.second; std::string smt2_identifier=convert_identifier(identifier); smt2_identifiers.insert(smt2_identifier); - out << "; set_to true (equal)\n"; - out << "(define-fun |" << smt2_identifier << "| () "; + for(const auto &command : prepared_rhs_with_dependencies.first) + out << *command; - convert_type(equal_expr.lhs().type()); - out << " "; - convert_expr(prepared_rhs); - - out << ")" << "\n"; + out << smt2_commentt{"set_to true (equal)"}; + out << smt2_commandt::define_fun( + smt2_symbolt{"|" + smt2_identifier + "|"}, + smt2_listt>{{}}, + convert_type(equal_expr.lhs().type()), + convert_expr(prepared_rhs)); return; // done } } } - exprt prepared_expr = prepare_for_convert_expr(expr); + const auto prepared_expr_with_dependencies = prepare_for_convert_expr(expr); + const exprt &prepared_expr = prepared_expr_with_dependencies.second; #if 0 out << "; CONV: " << format(expr) << "\n"; #endif - out << "; set_to " << (value?"true":"false") << "\n" - << "(assert "; - - if(!value) - { - out << "(not "; - convert_expr(prepared_expr); - out << ")"; - } - else - convert_expr(prepared_expr); - - out << ")" << "\n"; // assert + for(const auto &command : prepared_expr_with_dependencies.first) + out << *command; + smt2_astt assertion = + value ? convert_expr(prepared_expr) : smt2_not(convert_expr(prepared_expr)); + out << "; set_to " << (value ? "true" : "false") << "\n" + << smt2_commandt::_assert(std::move(assertion)); return; } @@ -4251,7 +4055,8 @@ exprt smt2_convt::lower_byte_operators(const exprt &expr) /// expressions. /// \param expr: expression to prepare /// \return equivalent expression suitable for convert_expr. -exprt smt2_convt::prepare_for_convert_expr(const exprt &expr) +std::pair>, exprt> +smt2_convt::prepare_for_convert_expr(const exprt &expr) { // First, replace byte operators, because they may introduce new array // expressions that must be seen by find_symbols: @@ -4261,15 +4066,14 @@ exprt smt2_convt::prepare_for_convert_expr(const exprt &expr) "lower_byte_operators should remove all byte operators"); // Now create symbols for all composite expressions present in lowered_expr: - find_symbols(lowered_expr); - - return lowered_expr; + return std::make_pair(find_symbols(lowered_expr), lowered_expr); } -void smt2_convt::find_symbols(const exprt &expr) +std::list> +smt2_convt::find_symbols(const exprt &expr) { // recursive call on type - find_symbols(expr.type()); + auto result = find_symbols(expr.type()); if(expr.id() == ID_exists || expr.id() == ID_forall) { @@ -4280,20 +4084,22 @@ void smt2_convt::find_symbols(const exprt &expr) identifiert &id = identifier_map[identifier]; id.type = q_expr.symbol().type(); id.is_bound = true; - find_symbols(q_expr.where()); - return; + + auto where_result = find_symbols(q_expr.where()); + result.splice(result.end(), where_result); + return result; } // recursive call on operands forall_operands(it, expr) - find_symbols(*it); + result.splice(result.end(), find_symbols(*it)); if(expr.id()==ID_symbol || expr.id()==ID_nondet_symbol) { // we don't track function-typed symbols if(expr.type().id()==ID_code) - return; + return result; irep_idt identifier; @@ -4312,12 +4118,12 @@ void smt2_convt::find_symbols(const exprt &expr) std::string smt2_identifier=convert_identifier(identifier); smt2_identifiers.insert(smt2_identifier); - out << "; find_symbols\n"; - out << "(declare-fun |" - << smt2_identifier - << "| () "; - convert_type(expr.type()); - out << ")" << "\n"; + result.push_back(util_make_unique("find_symbols")); + result.push_back( + util_make_unique(smt2_commandt::declare_fun( + smt2_symbolt{"|" + smt2_identifier + "|"}, + smt2_listt{{}}, + convert_type(expr.type())))); } } else if(expr.id()==ID_array_of) @@ -4326,10 +4132,13 @@ void smt2_convt::find_symbols(const exprt &expr) { const irep_idt id = "array_of." + std::to_string(defined_expressions.size()); - out << "; the following is a substitute for lambda i. x" << "\n"; - out << "(declare-fun " << id << " () "; - convert_type(expr.type()); - out << ")" << "\n"; + result.push_back(util_make_unique( + "the following is a substitute for lambda i. x")); + result.push_back( + util_make_unique(smt2_commandt::declare_fun( + smt2_symbolt{id}, + smt2_listt{{}}, + convert_type(expr.type())))); // use a quantifier instead of the lambda #if 0 // not really working in any solver yet! @@ -4350,18 +4159,22 @@ void smt2_convt::find_symbols(const exprt &expr) const array_typet &array_type=to_array_type(expr.type()); const irep_idt id = "array." + std::to_string(defined_expressions.size()); - out << "; the following is a substitute for an array constructor" << "\n"; - out << "(declare-fun " << id << " () "; - convert_type(array_type); - out << ")" << "\n"; + result.push_back(util_make_unique( + "the following is a substitute for an array constructor")); + result.push_back( + util_make_unique(smt2_commandt::declare_fun( + smt2_symbolt{id}, + smt2_listt{{}}, + convert_type(array_type)))); for(std::size_t i=0; i(smt2_commandt::_assert(smt2_eq( + smt2_select( + smt2_symbolt{id}, + convert_expr(from_integer(i, array_type.size().type()))), + convert_expr(expr.operands()[i]))))); } defined_expressions[expr]=id; @@ -4377,18 +4190,23 @@ void smt2_convt::find_symbols(const exprt &expr) const irep_idt id = "string." + std::to_string(defined_expressions.size()); - out << "; the following is a substitute for a string" << "\n"; - out << "(declare-fun " << id << " () "; - convert_type(array_type); - out << ")" << "\n"; + result.push_back(util_make_unique( + "the following is a substitute for a string")); + + result.push_back( + util_make_unique(smt2_commandt::declare_fun( + smt2_symbolt{id}, + smt2_listt{{}}, + convert_type(array_type)))); for(std::size_t i=0; i(smt2_commandt::_assert(smt2_eq( + smt2_select( + smt2_symbolt{id}, + convert_expr(from_integer(i, array_type.size().type()))), + convert_expr(tmp.operands()[i]))))); } defined_expressions[expr]=id; @@ -4405,9 +4223,11 @@ void smt2_convt::find_symbols(const exprt &expr) { const irep_idt id = "object_size." + std::to_string(object_sizes.size()); - out << "(declare-fun " << id << " () "; - convert_type(expr.type()); - out << ")" << "\n"; + result.push_back( + util_make_unique(smt2_commandt::declare_fun( + smt2_symbolt{id}, + smt2_listt{{}}, + convert_type(expr.type())))); object_sizes[expr]=id; } @@ -4441,38 +4261,37 @@ void smt2_convt::find_symbols(const exprt &expr) if(bvfp_set.insert(function).second) { - out << "; this is a model for " << expr.id() - << " : " << type2id(expr.op0().type()) - << " -> " << type2id(expr.type()) << "\n" - << "(define-fun " << function << " ("; + result.push_back(util_make_unique( + "this is a model for " + id2string(expr.id()) + " : " + + id2string(type2id(expr.op0().type())) + " -> " + + id2string(type2id(expr.type())))); + std::vector> args; for(std::size_t i = 0; i < expr.operands().size(); i++) { - if(i!=0) - out << " "; - out << "(op" << i << ' '; - convert_type(expr.operands()[i].type()); - out << ')'; + args.emplace_back( + smt2_symbolt{"op" + std::to_string(i)}, + convert_type(expr.operands()[i].type())); } - out << ") "; - convert_type(expr.type()); // return type - out << ' '; - exprt tmp1=expr; for(std::size_t i = 0; i < tmp1.operands().size(); i++) - tmp1.operands()[i]= - smt2_symbolt("op"+std::to_string(i), tmp1.operands()[i].type()); + tmp1.operands()[i] = smt2_symbol_exprt( + "op" + std::to_string(i), tmp1.operands()[i].type()); exprt tmp2=float_bv(tmp1); tmp2=letify(tmp2); CHECK_RETURN(!tmp2.is_nil()); - convert_expr(tmp2); - - out << ")\n"; // define-fun + result.push_back( + util_make_unique(smt2_commandt::define_fun( + smt2_symbolt{function}, + smt2_listt>(std::move(args)), + convert_type(expr.type()), + convert_expr(tmp2)))); } } + return result; } bool smt2_convt::use_array_theory(const exprt &expr) @@ -4496,7 +4315,7 @@ bool smt2_convt::use_array_theory(const exprt &expr) } } -void smt2_convt::convert_type(const typet &type) +smt2_sortt smt2_convt::convert_type(const typet &type) { if(type.id()==ID_array) { @@ -4506,49 +4325,45 @@ void smt2_convt::convert_type(const typet &type) // we always use array theory for top-level arrays const typet &subtype = array_type.subtype(); - out << "(Array "; - convert_type(array_type.size().type()); - out << " "; - - if(subtype.id()==ID_bool && !use_array_of_bool) - out << "(_ BitVec 1)"; - else - convert_type(array_type.subtype()); - - out << ")"; + auto subtype_ast = [&] { + if(subtype.id() == ID_bool && !use_array_of_bool) + return smt2_sortt::BitVec(1); + return convert_type(array_type.subtype()); + }(); + return smt2_sortt{ + smt2_identifiert{smt2_symbolt{"Array"}}, + {convert_type(array_type.size().type()), std::move(subtype_ast)}}; } else if(type.id()==ID_bool) { - out << "Bool"; + return smt2_sortt::Bool(); } else if(type.id() == ID_struct || type.id() == ID_struct_tag) { if(use_datatypes) { - out << datatype_map.at(type); + return smt2_sortt{smt2_symbolt{datatype_map.at(type)}}; } else { std::size_t width=boolbv_width(type); CHECK_RETURN_WITH_DIAGNOSTICS( width != 0, "failed to get width of struct"); - - out << "(_ BitVec " << width << ")"; + return smt2_sortt::BitVec(width); } } else if(type.id()==ID_vector) { if(use_datatypes) { - out << datatype_map.at(type); + return smt2_sortt{smt2_symbolt{datatype_map.at(type)}}; } else { std::size_t width=boolbv_width(type); CHECK_RETURN_WITH_DIAGNOSTICS( width != 0, "failed to get width of vector"); - - out << "(_ BitVec " << width << ")"; + return smt2_sortt::BitVec(width); } } else if(type.id()==ID_code) @@ -4556,19 +4371,17 @@ void smt2_convt::convert_type(const typet &type) // These may appear in structs. // We replace this by "Bool" in order to keep the same // member count. - out << "Bool"; + return smt2_sortt::Bool(); } else if(type.id() == ID_union || type.id() == ID_union_tag) { std::size_t width=boolbv_width(type); CHECK_RETURN_WITH_DIAGNOSTICS(width != 0, "failed to get width of union"); - - out << "(_ BitVec " << width << ")"; + return smt2_sortt::BitVec(width); } else if(type.id()==ID_pointer) { - out << "(_ BitVec " - << boolbv_width(type) << ")"; + return smt2_sortt::BitVec(boolbv_width(type)); } else if(type.id()==ID_bv || type.id()==ID_fixedbv || @@ -4576,54 +4389,54 @@ void smt2_convt::convert_type(const typet &type) type.id()==ID_signedbv || type.id()==ID_c_bool) { - out << "(_ BitVec " - << to_bitvector_type(type).get_width() << ")"; + return smt2_sortt::BitVec(to_bitvector_type(type).get_width()); } else if(type.id()==ID_c_enum) { // these have a subtype - out << "(_ BitVec " - << to_bitvector_type(type.subtype()).get_width() << ")"; + return smt2_sortt::BitVec(to_bitvector_type(type.subtype()).get_width()); } else if(type.id()==ID_c_enum_tag) { - convert_type(ns.follow_tag(to_c_enum_tag_type(type))); + return convert_type(ns.follow_tag(to_c_enum_tag_type(type))); } else if(type.id()==ID_floatbv) { const floatbv_typet &floatbv_type=to_floatbv_type(type); if(use_FPA_theory) - out << "(_ FloatingPoint " - << floatbv_type.get_e() << " " - << floatbv_type.get_f() + 1 << ")"; + return smt2_sortt{ + smt2_identifiert{smt2_symbolt("FloatingPoint"), + {smt2_constantt::make(floatbv_type.get_e()), + smt2_constantt::make(floatbv_type.get_f() + 1)}}, + {}}; + else - out << "(_ BitVec " - << floatbv_type.get_width() << ")"; + return smt2_sortt::BitVec(floatbv_type.get_width()); } else if(type.id()==ID_rational || type.id()==ID_real) - out << "Real"; + return smt2_sortt::Real(); else if(type.id()==ID_integer) - out << "Int"; + return smt2_sortt::Int(); else if(type.id()==ID_complex) { if(use_datatypes) { - out << datatype_map.at(type); + return smt2_sortt{smt2_symbolt(datatype_map.at(type))}; } else { std::size_t width=boolbv_width(type); CHECK_RETURN_WITH_DIAGNOSTICS( width != 0, "failed to get width of complex"); - - out << "(_ BitVec " << width << ")"; + return smt2_sortt::BitVec(width); } } else if(type.id()==ID_c_bit_field) { - convert_type(c_bit_field_replacement_type(to_c_bit_field_type(type), ns)); + return convert_type( + c_bit_field_replacement_type(to_c_bit_field_type(type), ns)); } else { @@ -4631,25 +4444,27 @@ void smt2_convt::convert_type(const typet &type) } } -void smt2_convt::find_symbols(const typet &type) +std::list> +smt2_convt::find_symbols(const typet &type) { std::set recstack; - find_symbols_rec(type, recstack); + return find_symbols_rec(type, recstack); } -void smt2_convt::find_symbols_rec( - const typet &type, - std::set &recstack) +std::list> +smt2_convt::find_symbols_rec(const typet &type, std::set &recstack) { if(type.id()==ID_array) { const array_typet &array_type=to_array_type(type); - find_symbols(array_type.size()); - find_symbols_rec(array_type.subtype(), recstack); + auto result = find_symbols(array_type.size()); + auto rec_result = find_symbols_rec(array_type.subtype(), recstack); + result.splice(result.end(), rec_result); + return result; } else if(type.id()==ID_complex) { - find_symbols_rec(type.subtype(), recstack); + auto result = find_symbols_rec(type.subtype(), recstack); if(use_datatypes && datatype_map.find(type)==datatype_map.end()) @@ -4658,23 +4473,26 @@ void smt2_convt::find_symbols_rec( "complex." + std::to_string(datatype_map.size()); datatype_map[type] = smt_typename; - out << "(declare-datatypes () ((" << smt_typename << " " - << "(mk-" << smt_typename; - - out << " (" << smt_typename << ".imag "; - convert_type(type.subtype()); - out << ")"; - - out << " (" << smt_typename << ".real "; - convert_type(type.subtype()); - out << ")"; - - out << "))))\n"; + // (declare-datatypes () ((smt_typename (mk-smt_typename ( + // smt_typename.imag type_subtype) (smt_typename.real type_subtype))))) + result.push_back(util_make_unique< + smt2_commandt>(smt2_commandt::declare_datatypes( + smt2_listt{{smt2_datatype_declarationt{ + smt2_non_empty_listt{smt2_symbolt{smt_typename}, {}}, + smt2_non_empty_listt{ + smt2_constructor_declarationt{ + smt2_symbolt{"mk-" + smt_typename}, + {smt2_selector_declarationt{smt2_symbolt{smt_typename + ".imag"}, + convert_type(type.subtype())}, + smt2_selector_declarationt{smt2_symbolt{smt_typename + ".real "}, + convert_type(type.subtype())}}}, + {}}}}}))); } + return result; } else if(type.id()==ID_vector) { - find_symbols_rec(type.subtype(), recstack); + auto result = find_symbols_rec(type.subtype(), recstack); if(use_datatypes && datatype_map.find(type)==datatype_map.end()) @@ -4687,18 +4505,24 @@ void smt2_convt::find_symbols_rec( "vector." + std::to_string(datatype_map.size()); datatype_map[type] = smt_typename; - out << "(declare-datatypes () ((" << smt_typename << " " - << "(mk-" << smt_typename; + std::vector selectors; for(mp_integer i=0; i!=size; ++i) { - out << " (" << smt_typename << "." << i << " "; - convert_type(type.subtype()); - out << ")"; + selectors.emplace_back( + smt2_symbolt{smt_typename + "." + integer2string(i)}, + convert_type(type.subtype())); } - - out << "))))\n"; + result.push_back( + util_make_unique(smt2_commandt::declare_datatypes( + smt2_listt{{smt2_datatype_declarationt{ + smt2_non_empty_listt{smt2_symbolt{smt_typename}, {}}, + smt2_non_empty_listt{ + {smt2_constructor_declarationt{smt2_symbolt{"mk-" + smt_typename}, + std::move(selectors)}}, + {}}}}}))); } + return result; } else if(type.id() == ID_struct) { @@ -4716,8 +4540,12 @@ void smt2_convt::find_symbols_rec( const struct_typet::componentst &components = to_struct_type(type).components(); + std::list> result; for(const auto &component : components) - find_symbols_rec(component.type(), recstack); + { + auto tmp_result = find_symbols_rec(component.type(), recstack); + result.splice(result.end(), tmp_result); + } // Declare the corresponding SMT type if we haven't already. if(need_decl) @@ -4733,25 +4561,29 @@ void smt2_convt::find_symbols_rec( // (struct.0.component1 type1) // ... // (struct.0.componentN typeN))))) - out << "(declare-datatypes () ((" << smt_typename << " " - << "(mk-" << smt_typename << " "; + std::vector selectors; for(const auto &component : components) { - out << "(" << smt_typename << "." << component.get_name() - << " "; - convert_type(component.type()); - out << ") "; + selectors.emplace_back( + smt2_symbolt{smt_typename + "." + id2string(component.get_name())}, + convert_type(component.type())); } - - out << "))))" << "\n"; + result.push_back( + util_make_unique(smt2_commandt::declare_datatypes( + smt2_listt{{smt2_datatype_declarationt{ + smt2_non_empty_listt{smt2_symbolt{smt_typename}, {}}, + smt2_non_empty_listt{ + {smt2_constructor_declarationt{smt2_symbolt{"mk-" + smt_typename}, + std::move(selectors)}}, + {}}}}}))); // Let's also declare convenience functions to update individual - // members of the struct whil we're at it. The functions are + // members of the struct while we're at it. The functions are // named like `update-struct.0.component1'. Their declarations // look like: // - // (declare-fun update-struct.0.component1 + // (define-fun update-struct.0.component1 // ((s struct.0) ; first arg -- the struct to update // (v type1)) ; second arg -- the value to update // struct.0 ; the output type @@ -4767,66 +4599,89 @@ void smt2_convt::find_symbols_rec( ++it) { const struct_union_typet::componentt &component=*it; - out << "(define-fun update-" << smt_typename << "." - << component.get_name() << " " - << "((s " << smt_typename << ") " - << "(v "; - convert_type(component.type()); - out << ")) " << smt_typename << " " - << "(mk-" << smt_typename - << " "; - - for(struct_union_typet::componentst::const_iterator - it2=components.begin(); - it2!=components.end(); + const smt2_symbolt s{"s"}; + const smt2_symbolt v{"v"}; + const smt2_sortt sort{smt2_symbolt{smt_typename}}; + smt2_listt> arguments{ + {smt2_pairt{s, sort}, + smt2_pairt{ + v, convert_type(component.type())}}}; + + std::vector mk_arguments; + for(struct_union_typet::componentst::const_iterator it2 = + components.begin(); + it2 != components.end(); ++it2) { if(it==it2) - out << "v "; + mk_arguments.push_back(v); else { - out << "(" << smt_typename << "." - << it2->get_name() << " s) "; + mk_arguments.push_back(smt2_function_applicationt{ + smt2_identifiert{ + smt2_symbolt{smt_typename + "." + id2string(it2->get_name())}}, + {s}}); } } - out << "))" << "\n"; + result.push_back( + util_make_unique(smt2_commandt::define_fun( + smt2_symbolt{"update-" + smt_typename + "." + + id2string(component.get_name())}, + std::move(arguments), + smt2_sortt{smt2_symbolt{smt_typename}}, + smt2_function_applicationt{ + smt2_identifiert{smt2_symbolt{"mk-" + smt_typename}}, + std::move(mk_arguments)}))); } - - out << "\n"; } + return result; } else if(type.id() == ID_union) { const union_typet::componentst &components = to_union_type(type).components(); - + std::list> result; for(const auto &component : components) - find_symbols_rec(component.type(), recstack); + { + auto tmp_result = find_symbols_rec(component.type(), recstack); + result.splice(result.end(), tmp_result); + } + return result; } else if(type.id()==ID_code) { + std::list> result; const code_typet::parameterst ¶meters= to_code_type(type).parameters(); for(const auto ¶m : parameters) - find_symbols_rec(param.type(), recstack); + { + auto tmp_result = find_symbols_rec(param.type(), recstack); + result.splice(result.end(), tmp_result); + } - find_symbols_rec(to_code_type(type).return_type(), recstack); + auto tmp_result = + find_symbols_rec(to_code_type(type).return_type(), recstack); + result.splice(result.end(), tmp_result); + return result; } else if(type.id()==ID_pointer) { - find_symbols_rec(type.subtype(), recstack); + return find_symbols_rec(type.subtype(), recstack); } else if(type.id() == ID_struct_tag) { const auto &struct_tag = to_struct_tag_type(type); const irep_idt &id = struct_tag.get_identifier(); + std::list> result; if(recstack.find(id) == recstack.end()) { recstack.insert(id); - find_symbols_rec(ns.follow_tag(struct_tag), recstack); + auto tmp_result = find_symbols_rec(ns.follow_tag(struct_tag), recstack); + result.splice(result.end(), tmp_result); } + return result; } else if(type.id() == ID_union_tag) { @@ -4836,9 +4691,10 @@ void smt2_convt::find_symbols_rec( if(recstack.find(id) == recstack.end()) { recstack.insert(id); - find_symbols_rec(ns.follow_tag(union_tag), recstack); + return find_symbols_rec(ns.follow_tag(union_tag), recstack); } } + return {}; } std::size_t smt2_convt::get_number_of_solver_calls() const diff --git a/src/solvers/smt2/smt2_conv.h b/src/solvers/smt2/smt2_conv.h index 47c17f395fe..ad7d79f6db0 100644 --- a/src/solvers/smt2/smt2_conv.h +++ b/src/solvers/smt2/smt2_conv.h @@ -10,8 +10,10 @@ Author: Daniel Kroening, kroening@kroening.com #ifndef CPROVER_SOLVERS_SMT2_SMT2_CONV_H #define CPROVER_SOLVERS_SMT2_SMT2_CONV_H -#include +#include +#include #include +#include #include #include @@ -20,9 +22,10 @@ Author: Daniel Kroening, kroening@kroening.com # include #endif -#include #include #include +#include +#include #include "letify.h" @@ -30,6 +33,7 @@ class typecast_exprt; class constant_exprt; class index_exprt; class member_exprt; +class smt2_command_or_commentt; class smt2_convt : public stack_decision_proceduret { @@ -96,47 +100,51 @@ class smt2_convt : public stack_decision_proceduret // tweaks for arrays bool use_array_theory(const exprt &); - void flatten_array(const exprt &); + smt2_astt flatten_array(const exprt &); // specific expressions go here - void convert_typecast(const typecast_exprt &expr); - void convert_floatbv_typecast(const floatbv_typecast_exprt &expr); - void convert_struct(const struct_exprt &expr); - void convert_union(const union_exprt &expr); - void convert_constant(const constant_exprt &expr); - void convert_relation(const exprt &expr); - void convert_is_dynamic_object(const exprt &expr); - void convert_plus(const plus_exprt &expr); - void convert_minus(const minus_exprt &expr); - void convert_div(const div_exprt &expr); - void convert_mult(const mult_exprt &expr); - void convert_rounding_mode_FPA(const exprt &expr); - void convert_floatbv_plus(const ieee_float_op_exprt &expr); - void convert_floatbv_minus(const ieee_float_op_exprt &expr); - void convert_floatbv_div(const ieee_float_op_exprt &expr); - void convert_floatbv_mult(const ieee_float_op_exprt &expr); - void convert_mod(const mod_exprt &expr); - void convert_index(const index_exprt &expr); - void convert_member(const member_exprt &expr); - - void convert_with(const with_exprt &expr); - void convert_update(const exprt &expr); + smt2_astt convert_typecast(const typecast_exprt &expr); + smt2_astt convert_floatbv_typecast(const floatbv_typecast_exprt &expr); + smt2_astt convert_struct(const struct_exprt &expr); + smt2_astt convert_union(const union_exprt &expr); + smt2_astt convert_constant(const constant_exprt &expr); + smt2_astt convert_relation(const exprt &expr); + smt2_astt convert_is_dynamic_object(const exprt &expr); + smt2_astt convert_plus(const plus_exprt &expr); + smt2_astt convert_minus(const minus_exprt &expr); + smt2_astt convert_div(const div_exprt &expr); + smt2_astt convert_mult(const mult_exprt &expr); + smt2_astt convert_rounding_mode_FPA(const exprt &expr); + smt2_astt convert_floatbv_plus(const ieee_float_op_exprt &expr); + smt2_astt convert_floatbv_minus(const ieee_float_op_exprt &expr); + smt2_astt convert_floatbv_div(const ieee_float_op_exprt &expr); + smt2_astt convert_floatbv_mult(const ieee_float_op_exprt &expr); + smt2_astt convert_mod(const mod_exprt &expr); + smt2_astt convert_index(const index_exprt &expr); + smt2_astt convert_member(const member_exprt &expr); + + smt2_astt convert_with(const with_exprt &expr); + smt2_astt convert_update(const exprt &expr); std::string convert_identifier(const irep_idt &identifier); - void convert_expr(const exprt &); - void convert_type(const typet &); - void convert_literal(const literalt); + smt2_astt convert_expr(const exprt &); + smt2_sortt convert_type(const typet &); + smt2_astt convert_literal(const literalt); literalt convert(const exprt &expr); tvt l_get(literalt l) const; // auxiliary methods - exprt prepare_for_convert_expr(const exprt &expr); + std::pair>, exprt> + prepare_for_convert_expr(const exprt &expr); exprt lower_byte_operators(const exprt &expr); - void find_symbols(const exprt &expr); - void find_symbols(const typet &type); - void find_symbols_rec(const typet &type, std::set &recstack); + std::list> + find_symbols(const exprt &expr); + std::list> + find_symbols(const typet &type); + std::list> + find_symbols_rec(const typet &type, std::set &recstack); // letification letifyt letify; @@ -149,15 +157,15 @@ class smt2_convt : public stack_decision_proceduret exprt parse_rec(const irept &s, const typet &type); // we use this to build a bit-vector encoding of the FPA theory - void convert_floatbv(const exprt &expr); + smt2_astt convert_floatbv(const exprt &expr); std::string type2id(const typet &) const; std::string floatbv_suffix(const exprt &) const; std::set bvfp_set; // already converted - class smt2_symbolt : public nullary_exprt + class smt2_symbol_exprt : public nullary_exprt { public: - smt2_symbolt(const irep_idt &_identifier, const typet &_type) + smt2_symbol_exprt(const irep_idt &_identifier, const typet &_type) : nullary_exprt(ID_smt2_symbol, _type) { set(ID_identifier, _identifier); } @@ -167,10 +175,10 @@ class smt2_convt : public stack_decision_proceduret } }; - const smt2_symbolt &to_smt2_symbol(const exprt &expr) + const smt2_symbol_exprt &to_smt2_symbol(const exprt &expr) { assert(expr.id()==ID_smt2_symbol && !expr.has_operands()); - return static_cast(expr); + return static_cast(expr); } // flattens any non-bitvector type into a bitvector, @@ -178,13 +186,13 @@ class smt2_convt : public stack_decision_proceduret // floats when using the FPA theory. // unflatten() does the opposite. enum class wheret { BEGIN, END }; - void flatten2bv(const exprt &); - void unflatten(wheret, const typet &, unsigned nesting=0); + smt2_astt flatten2bv(const exprt &); + smt2_astt unflatten(const typet &, smt2_astt ast, unsigned nesting = 0); // pointers pointer_logict pointer_logic; - void convert_address_of_rec( - const exprt &expr, const pointer_typet &result_type); + smt2_astt + convert_address_of_rec(const exprt &expr, const pointer_typet &result_type); void define_object_size(const irep_idt &id, const exprt &expr); diff --git a/src/solvers/smt2/smt2_util.h b/src/solvers/smt2/smt2_util.h new file mode 100644 index 00000000000..5cf1d935ff6 --- /dev/null +++ b/src/solvers/smt2/smt2_util.h @@ -0,0 +1,255 @@ +/*******************************************************************\ + +Module: SMT2 solver + +Author: Romain Brenguier + +*******************************************************************/ + +/// \file +/// Helper functions for constructing standard SMT2 expressions + +#ifndef CPROVER_SOLVERS_SMT2_SMT2_UTIL_H +#define CPROVER_SOLVERS_SMT2_SMT2_UTIL_H + +#include "smt2_ast.h" + +inline smt2_astt smt2_and(smt2_astt ast1, smt2_astt ast2) +{ + return smt2_function_applicationt{smt2_identifiert{smt2_symbolt{ID_and}}, + {std::move(ast1), std::move(ast2)}}; +} + +inline smt2_astt smt2_bv(const mp_integer &index, const mp_integer &width) +{ + smt2_symbolt bv{"bv" + integer2string(index)}; + return smt2_identifiert{std::move(bv), {smt2_constantt::make(width)}}; +} + +inline smt2_astt smt2_bvadd(smt2_astt ast1, smt2_astt ast2) +{ + return smt2_function_applicationt{smt2_identifiert{smt2_symbolt{"bvadd"}}, + {std::move(ast1), std::move(ast2)}}; +} + +inline smt2_astt smt2_bvand(smt2_astt ast1, smt2_astt ast2) +{ + return smt2_function_applicationt{smt2_identifiert{smt2_symbolt{"bvand"}}, + {std::move(ast1), std::move(ast2)}}; +} + +inline smt2_astt smt2_bvmul(smt2_astt arg1, smt2_astt arg2) +{ + return smt2_function_applicationt{smt2_identifiert{smt2_symbolt{"bvmul"}}, + {std::move(arg1), std::move(arg2)}}; +} + +inline smt2_astt smt2_bvlshr(smt2_astt arg1, smt2_astt arg2) +{ + return smt2_function_applicationt{smt2_identifiert{smt2_symbolt{"bvlshr"}}, + {std::move(arg1), std::move(arg2)}}; +} + +inline smt2_astt smt2_bvnot(smt2_astt arg) +{ + return smt2_function_applicationt{smt2_identifiert{smt2_symbolt{"bvnot"}}, + {std::move(arg)}}; +} + +inline smt2_astt smt2_bvneg(smt2_astt arg) +{ + return smt2_function_applicationt{smt2_identifiert{smt2_symbolt{"bvneg"}}, + {std::move(arg)}}; +} + +inline smt2_astt smt2_bvor(smt2_astt arg1, smt2_astt arg2) +{ + return smt2_function_applicationt{smt2_identifiert{smt2_symbolt{"bvor"}}, + {std::move(arg1), std::move(arg2)}}; +} + +inline smt2_astt smt2_bvsdiv(smt2_astt arg1, smt2_astt arg2) +{ + return smt2_function_applicationt{smt2_identifiert{smt2_symbolt{"bvsdiv"}}, + {std::move(arg1), std::move(arg2)}}; +} + +inline smt2_astt smt2_bvsge(smt2_astt arg1, smt2_astt arg2) +{ + return smt2_function_applicationt{smt2_identifiert{smt2_symbolt{"bvsge"}}, + {std::move(arg1), std::move(arg2)}}; +} + +inline smt2_astt smt2_bvshl(smt2_astt arg1, smt2_astt arg2) +{ + return smt2_function_applicationt{smt2_identifiert{smt2_symbolt{"bvshl"}}, + {std::move(arg1), std::move(arg2)}}; +} + +inline smt2_astt smt2_bvslt(smt2_astt arg1, smt2_astt arg2) +{ + return smt2_function_applicationt{smt2_identifiert{smt2_symbolt{"bvslt"}}, + {std::move(arg1), std::move(arg2)}}; +} + +inline smt2_astt smt2_bvsrem(smt2_astt arg1, smt2_astt arg2) +{ + return smt2_function_applicationt{smt2_identifiert{smt2_symbolt{"bvsrem"}}, + {std::move(arg1), std::move(arg2)}}; +} + +inline smt2_astt smt2_bvsub(smt2_astt arg1, smt2_astt arg2) +{ + return smt2_function_applicationt{smt2_identifiert{smt2_symbolt{"bvsub"}}, + {std::move(arg1), std::move(arg2)}}; +} + +inline smt2_astt smt2_bvudiv(smt2_astt arg1, smt2_astt arg2) +{ + return smt2_function_applicationt{smt2_identifiert{smt2_symbolt{"bvudiv"}}, + {std::move(arg1), std::move(arg2)}}; +} + +inline smt2_astt smt2_bvuge(smt2_astt arg1, smt2_astt arg2) +{ + return smt2_function_applicationt{smt2_identifiert{smt2_symbolt{"bvuge"}}, + {std::move(arg1), std::move(arg2)}}; +} + +inline smt2_astt smt2_bvurem(smt2_astt arg1, smt2_astt arg2) +{ + return smt2_function_applicationt{smt2_identifiert{smt2_symbolt{"bvurem"}}, + {std::move(arg1), std::move(arg2)}}; +} + +inline smt2_astt smt2_concat(smt2_astt ast1, smt2_astt ast2) +{ + return smt2_function_applicationt{smt2_identifiert{smt2_symbolt{"concat"}}, + {std::move(ast1), std::move(ast2)}}; +} + +inline smt2_identifiert +smt2_extract(const mp_integer &width, const mp_integer &offset) +{ + return smt2_identifiert{ + smt2_symbolt{"extract"}, + {smt2_constantt::make(width), smt2_constantt::make(offset)}}; +} + +inline smt2_astt smt2_eq(smt2_astt left, smt2_astt right) +{ + return smt2_function_applicationt{smt2_identifiert{smt2_symbolt{ID_equal}}, + {std::move(left), std::move(right)}}; +} + +inline smt2_astt +smt2_fp_add(smt2_astt rounding_mode, smt2_astt ast1, smt2_astt ast2) +{ + return smt2_function_applicationt{ + smt2_identifiert{smt2_symbolt{"fp.add"}}, + {std::move(rounding_mode), std::move(ast1), std::move(ast2)}}; +} + +inline smt2_astt +smt2_fp_div(smt2_astt rounding_mode, smt2_astt ast1, smt2_astt ast2) +{ + return smt2_function_applicationt{ + smt2_identifiert{smt2_symbolt{"fp.sub"}}, + {std::move(rounding_mode), std::move(ast1), std::move(ast2)}}; +} + +inline smt2_astt smt2_fp_is_infinite(smt2_astt arg) +{ + return smt2_function_applicationt{ + smt2_identifiert{smt2_symbolt{"fp.isInfinite"}}, {std::move(arg)}}; +} + +inline smt2_astt smt2_fp_is_nan(smt2_astt arg) +{ + return smt2_function_applicationt{smt2_identifiert{smt2_symbolt{"fp.isNaN"}}, + {std::move(arg)}}; +} + +inline smt2_astt smt2_fp_is_normal(smt2_astt arg) +{ + return smt2_function_applicationt{ + smt2_identifiert{smt2_symbolt{"fp.isNormal"}}, {std::move(arg)}}; +} + +inline smt2_astt smt2_fp_is_zero(smt2_astt arg) +{ + return smt2_function_applicationt{smt2_identifiert{smt2_symbolt{"fp.isZero"}}, + {std::move(arg)}}; +} + +inline smt2_astt +smt2_fp_mul(smt2_astt rounding_mode, smt2_astt ast1, smt2_astt ast2) +{ + return smt2_function_applicationt{ + smt2_identifiert{smt2_symbolt{"fp.mul"}}, + {std::move(rounding_mode), std::move(ast1), std::move(ast2)}}; +} + +inline smt2_astt +smt2_fp_sub(smt2_astt rounding_mode, smt2_astt ast1, smt2_astt ast2) +{ + return smt2_function_applicationt{ + smt2_identifiert{smt2_symbolt{"fp.sub"}}, + {std::move(rounding_mode), std::move(ast1), std::move(ast2)}}; +} + +inline smt2_astt smt2_implies(smt2_astt left, smt2_astt right) +{ + return smt2_function_applicationt{smt2_identifiert{smt2_symbolt{ID_implies}}, + {std::move(left), std::move(right)}}; +} + +inline smt2_astt +smt2_ite(smt2_astt condition, smt2_astt true_case, smt2_astt false_case) +{ + return smt2_function_applicationt{ + smt2_identifiert{smt2_symbolt{"ite"}}, + {std::move(condition), std::move(true_case), std::move(false_case)}}; +} + +inline smt2_astt smt2_minus(smt2_astt arg1, smt2_astt arg2) +{ + return smt2_function_applicationt{smt2_identifiert{smt2_symbolt{ID_minus}}, + {std::move(arg1), std::move(arg2)}}; +} + +inline smt2_astt smt2_not(smt2_astt ast) +{ + return smt2_function_applicationt{smt2_identifiert{smt2_symbolt{ID_not}}, + {std::move(ast)}}; +} + +inline smt2_astt smt2_or(smt2_astt arg1, smt2_astt arg2) +{ + return smt2_function_applicationt{smt2_identifiert{smt2_symbolt{ID_or}}, + {std::move(arg1), std::move(arg2)}}; +} + +inline smt2_identifiert smt2_repeat(smt2_constantt times) +{ + return smt2_identifiert{smt2_symbolt{"repeat"}, {std::move(times)}}; +} + +inline smt2_astt smt2_select(smt2_astt arg1, smt2_astt arg2) +{ + return smt2_function_applicationt{smt2_identifiert{smt2_symbolt{"select"}}, + {std::move(arg1), std::move(arg2)}}; +} + +inline smt2_identifiert smt2_sign_extend(smt2_constantt constant) +{ + return smt2_identifiert{smt2_symbolt{"sign_extend"}, {std::move(constant)}}; +} + +inline smt2_identifiert smt2_zero_extend(const mp_integer &width) +{ + return smt2_identifiert{smt2_symbolt{"zero_extend"}, + {smt2_constantt::make(width)}}; +} + +#endif // CPROVER_SOLVERS_SMT2_SMT2_UTIL_H diff --git a/src/util/irep_ids.def b/src/util/irep_ids.def index 5b21c8f388d..dc5c0274f9a 100644 --- a/src/util/irep_ids.def +++ b/src/util/irep_ids.def @@ -802,6 +802,7 @@ IREP_ID_ONE(statement_list_xor) IREP_ID_ONE(statement_list_xor_not) IREP_ID_ONE(statement_list_instruction) IREP_ID_ONE(statement_list_instructions) +IREP_ID_ONE(par) // Projects depending on this code base that wish to extend the list of // available ids should provide a file local_irep_ids.def in their source tree