From 313e40429a534ab2c7b529c666b0c3e891b13bf4 Mon Sep 17 00:00:00 2001 From: Daniel Kroening Date: Tue, 1 Oct 2019 22:41:26 +0100 Subject: [PATCH 1/3] smt2_parser: introduce table of commands This refactors the SMT2 parser to use hash tables instead of chains of if()...else if()... for commands. This enables extensions, and may have a performance benefit as the number of commands grows. --- src/solvers/smt2/smt2_parser.cpp | 51 ++++++++++++++++---------- src/solvers/smt2/smt2_parser.h | 15 +++++--- src/solvers/smt2/smt2_solver.cpp | 63 ++++++++++++++++---------------- 3 files changed, 72 insertions(+), 57 deletions(-) diff --git a/src/solvers/smt2/smt2_parser.cpp b/src/solvers/smt2/smt2_parser.cpp index dc79a2dcf4a..2987ea26af9 100644 --- a/src/solvers/smt2/smt2_parser.cpp +++ b/src/solvers/smt2/smt2_parser.cpp @@ -1259,21 +1259,36 @@ typet smt2_parsert::function_signature_declaration() void smt2_parsert::command(const std::string &c) { - if(c == "declare-const" || c == "declare-var") + auto c_it = commands.find(c); + if(c_it == commands.end()) { - // declare-var appears to be a synonym for declare-const that is - // accepted by Z3 and CVC4 + // silently ignore + ignore_command(); + } + else + c_it->second(); +} + +void smt2_parsert::setup_commands() +{ + commands["declare-const"] = [this]() { + const auto s = smt2_tokenizer.get_buffer(); + if(next_token() != smt2_tokenizert::SYMBOL) - throw error() << "expected a symbol after '" << c << '\''; + throw error() << "expected a symbol after " << s; irep_idt id = smt2_tokenizer.get_buffer(); auto type = sort(); if(add_fresh_id(id, exprt(ID_nil, type)) != id) throw error() << "identifier '" << id << "' defined twice"; - } - else if(c=="declare-fun") - { + }; + + // declare-var appears to be a synonym for declare-const that is + // accepted by Z3 and CVC4 + commands["declare-var"] = commands["declare-const"]; + + commands["declare-fun"] = [this]() { if(next_token() != smt2_tokenizert::SYMBOL) throw error("expected a symbol after declare-fun"); @@ -1282,9 +1297,9 @@ void smt2_parsert::command(const std::string &c) if(add_fresh_id(id, exprt(ID_nil, type)) != id) throw error() << "identifier '" << id << "' defined twice"; - } - else if(c == "define-const") - { + }; + + commands["define-const"] = [this]() { if(next_token() != smt2_tokenizert::SYMBOL) throw error("expected a symbol after define-const"); @@ -1304,9 +1319,9 @@ void smt2_parsert::command(const std::string &c) // create the entry if(add_fresh_id(id, value) != id) throw error() << "identifier '" << id << "' defined twice"; - } - else if(c=="define-fun") - { + }; + + commands["define-fun"] = [this]() { if(next_token() != smt2_tokenizert::SYMBOL) throw error("expected a symbol after define-fun"); @@ -1345,11 +1360,7 @@ void smt2_parsert::command(const std::string &c) id_map.at(id).type = signature.type; id_map.at(id).parameters = signature.parameters; - } - else if(c=="exit") - { - exit=true; - } - else - ignore_command(); + }; + + commands["exit"] = [this]() { exit = true; }; } diff --git a/src/solvers/smt2/smt2_parser.h b/src/solvers/smt2/smt2_parser.h index 540fcabc376..9b6ebde717c 100644 --- a/src/solvers/smt2/smt2_parser.h +++ b/src/solvers/smt2/smt2_parser.h @@ -10,6 +10,7 @@ Author: Daniel Kroening, kroening@kroening.com #define CPROVER_SOLVERS_SMT2_SMT2_PARSER_H #include +#include #include #include @@ -22,6 +23,7 @@ class smt2_parsert explicit smt2_parsert(std::istream &_in) : exit(false), smt2_tokenizer(_in), parenthesis_level(0) { + setup_commands(); } virtual ~smt2_parsert() = default; @@ -82,10 +84,6 @@ class smt2_parsert std::size_t parenthesis_level; smt2_tokenizert::tokent next_token(); - void command_sequence(); - - virtual void command(const std::string &); - // for let/quantifier bindings, function parameters using renaming_mapt=std::map; renaming_mapt renaming_map; @@ -116,7 +114,6 @@ class smt2_parsert } }; - void ignore_command(); exprt expression(); exprt function_application(); exprt function_application_ieee_float_op( @@ -144,6 +141,14 @@ class smt2_parsert /// Apply typecast to unsignedbv to given expression exprt cast_bv_to_unsigned(const exprt &); + + // hashtable for all commands + std::unordered_map> commands; + + void command_sequence(); + void command(const std::string &); + void ignore_command(); + void setup_commands(); }; #endif // CPROVER_SOLVERS_SMT2_SMT2_PARSER_H diff --git a/src/solvers/smt2/smt2_solver.cpp b/src/solvers/smt2/smt2_solver.cpp index f30311d2990..cb78b88056f 100644 --- a/src/solvers/smt2/smt2_solver.cpp +++ b/src/solvers/smt2/smt2_solver.cpp @@ -28,12 +28,13 @@ class smt2_solvert:public smt2_parsert smt2_solvert(std::istream &_in, decision_proceduret &_solver) : smt2_parsert(_in), solver(_solver), status(NOT_SOLVED) { + setup_commands(); } protected: decision_proceduret &solver; - void command(const std::string &) override; + void setup_commands(); void define_constants(); void expand_function_applications(exprt &); @@ -118,20 +119,19 @@ void smt2_solvert::expand_function_applications(exprt &expr) } } -void smt2_solvert::command(const std::string &c) +void smt2_solvert::setup_commands() { { - if(c == "assert") - { + commands["assert"] = [this]() { exprt e = expression(); if(e.is_not_nil()) { expand_function_applications(e); solver.set_to_true(e); } - } - else if(c == "check-sat") - { + }; + + commands["check-sat"] = [this]() { // add constant definitions as constraints define_constants(); @@ -151,20 +151,20 @@ void smt2_solvert::command(const std::string &c) std::cout << "error\n"; status = NOT_SOLVED; } - } - else if(c == "check-sat-assuming") - { + }; + + commands["check-sat-assuming"] = [this]() { throw error("not yet implemented"); - } - else if(c == "display") - { + }; + + commands["display"] = [this]() { // this is a command that Z3 appears to implement exprt e = expression(); if(e.is_not_nil()) std::cout << smt2_format(e) << '\n'; - } - else if(c == "get-value") - { + }; + + commands["get-value"] = [this]() { std::vector ops; if(next_token() != smt2_tokenizert::OPEN) @@ -217,18 +217,18 @@ void smt2_solvert::command(const std::string &c) } std::cout << ")\n"; - } - else if(c == "echo") - { + }; + + commands["echo"] = [this]() { if(next_token() != smt2_tokenizert::STRING_LITERAL) throw error("expected string literal"); std::cout << smt2_format(constant_exprt( smt2_tokenizer.get_buffer(), string_typet())) << '\n'; - } - else if(c == "get-assignment") - { + }; + + commands["get-assignment"] = [this]() { // print satisfying assignment for all named expressions if(status != SAT) @@ -256,9 +256,9 @@ void smt2_solvert::command(const std::string &c) } } std::cout << ')' << '\n'; - } - else if(c == "get-model") - { + }; + + commands["get-model"] = [this]() { // print a model for all identifiers if(status != SAT) @@ -293,9 +293,9 @@ void smt2_solvert::command(const std::string &c) } } std::cout << ')' << '\n'; - } - else if(c == "simplify") - { + }; + + commands["simplify"] = [this]() { // this is a command that Z3 appears to implement exprt e = expression(); if(e.is_not_nil()) @@ -305,7 +305,9 @@ void smt2_solvert::command(const std::string &c) exprt e_simplified = simplify_expr(e, ns); std::cout << smt2_format(e) << '\n'; } - } + }; + } + #if 0 // TODO: | ( declare-const hsymboli hsorti ) @@ -330,9 +332,6 @@ void smt2_solvert::command(const std::string &c) | ( set-info hattributei ) | ( set-option hoptioni ) #endif - else - smt2_parsert::command(c); - } } class smt2_message_handlert : public message_handlert From ac3701871d1209e70ea48130de20f74a58209159 Mon Sep 17 00:00:00 2001 From: Daniel Kroening Date: Wed, 2 Oct 2019 08:25:11 +0100 Subject: [PATCH 2/3] smt2_parser: sorts are now in a hash table This refactors the SMT2 parser to use hash tables instead of chains of if()...else if()... for sorts. This enables extensions, and may have a performance benefit as the number of sorts grows. --- src/solvers/smt2/smt2_parser.cpp | 141 ++++++++++++++++--------------- src/solvers/smt2/smt2_parser.h | 7 +- 2 files changed, 78 insertions(+), 70 deletions(-) diff --git a/src/solvers/smt2/smt2_parser.cpp b/src/solvers/smt2/smt2_parser.cpp index 2987ea26af9..7b78e1de7c8 100644 --- a/src/solvers/smt2/smt2_parser.cpp +++ b/src/solvers/smt2/smt2_parser.cpp @@ -1087,99 +1087,102 @@ exprt smt2_parsert::expression() typet smt2_parsert::sort() { + // a sort is one of the following three cases: + // SYMBOL + // ( _ SYMBOL ... + // ( SYMBOL ... switch(next_token()) { case smt2_tokenizert::SYMBOL: - { - const std::string &buffer = smt2_tokenizer.get_buffer(); - - if(buffer=="Bool") - return bool_typet(); - else if(buffer=="Int") - return integer_typet(); - else if(buffer=="Real") - return real_typet(); - else - throw error() << "unexpected sort: '" << buffer << '\''; - } + break; case smt2_tokenizert::OPEN: - if(next_token() != smt2_tokenizert::SYMBOL) + if(smt2_tokenizer.next_token() != smt2_tokenizert::SYMBOL) throw error("expected symbol after '(' in a sort "); if(smt2_tokenizer.get_buffer() == "_") { - // indexed identifier if(next_token() != smt2_tokenizert::SYMBOL) throw error("expected symbol after '_' in a sort"); + } + break; - if(smt2_tokenizer.get_buffer() == "BitVec") - { - if(next_token() != smt2_tokenizert::NUMERAL) - throw error("expected numeral as bit-width"); + case smt2_tokenizert::CLOSE: + case smt2_tokenizert::NUMERAL: + case smt2_tokenizert::STRING_LITERAL: + case smt2_tokenizert::NONE: + case smt2_tokenizert::KEYWORD: + throw error() << "unexpected token in a sort: '" + << smt2_tokenizer.get_buffer() << '\''; - auto width = std::stoll(smt2_tokenizer.get_buffer()); + case smt2_tokenizert::END_OF_FILE: + throw error() << "unexpected end-of-file in a sort"; + } - // eat the ')' - if(next_token() != smt2_tokenizert::CLOSE) - throw error("expected ')' at end of sort"); + // now we have a SYMBOL + const auto &token = smt2_tokenizer.get_buffer(); - return unsignedbv_typet(width); - } - else if(smt2_tokenizer.get_buffer() == "FloatingPoint") - { - if(next_token() != smt2_tokenizert::NUMERAL) - throw error("expected numeral as bit-width"); + const auto s_it = sorts.find(token); - const auto width_e = std::stoll(smt2_tokenizer.get_buffer()); + if(s_it == sorts.end()) + throw error() << "unexpected sort: '" << token << '\''; - if(next_token() != smt2_tokenizert::NUMERAL) - throw error("expected numeral as bit-width"); + return s_it->second(); +} - const auto width_f = std::stoll(smt2_tokenizer.get_buffer()); +void smt2_parsert::setup_sorts() +{ + sorts["Bool"] = [] { return bool_typet(); }; + sorts["Int"] = [] { return integer_typet(); }; + sorts["Real"] = [] { return real_typet(); }; - // consume the ')' - if(next_token() != smt2_tokenizert::CLOSE) - throw error("expected ')' at end of sort"); + sorts["BitVec"] = [this] { + if(next_token() != smt2_tokenizert::NUMERAL) + throw error("expected numeral as bit-width"); - return ieee_float_spect(width_f - 1, width_e).to_type(); - } - else - throw error() << "unexpected sort: '" << smt2_tokenizer.get_buffer() - << '\''; - } - else if(smt2_tokenizer.get_buffer() == "Array") - { - // this gets two sorts as arguments, domain and range - auto domain = sort(); - auto range = sort(); + auto width = std::stoll(smt2_tokenizer.get_buffer()); - // eat the ')' - if(next_token() != smt2_tokenizert::CLOSE) - throw error("expected ')' at end of Array sort"); + // eat the ')' + if(next_token() != smt2_tokenizert::CLOSE) + throw error("expected ')' at end of sort"); - // we can turn arrays that map an unsigned bitvector type - // to something else into our 'array_typet' - if(domain.id() == ID_unsignedbv) - return array_typet(range, infinity_exprt(domain)); - else - throw error("unsupported array sort"); - } - else - throw error() << "unexpected sort: '" << smt2_tokenizer.get_buffer() - << '\''; + return unsignedbv_typet(width); + }; - case smt2_tokenizert::CLOSE: - case smt2_tokenizert::NUMERAL: - case smt2_tokenizert::STRING_LITERAL: - case smt2_tokenizert::END_OF_FILE: - case smt2_tokenizert::NONE: - case smt2_tokenizert::KEYWORD: - throw error() << "unexpected token in a sort: '" - << smt2_tokenizer.get_buffer() << '\''; - } + sorts["FloatingPoint"] = [this] { + if(next_token() != smt2_tokenizert::NUMERAL) + throw error("expected numeral as bit-width"); - UNREACHABLE; + const auto width_e = std::stoll(smt2_tokenizer.get_buffer()); + + if(next_token() != smt2_tokenizert::NUMERAL) + throw error("expected numeral as bit-width"); + + const auto width_f = std::stoll(smt2_tokenizer.get_buffer()); + + // consume the ')' + if(next_token() != smt2_tokenizert::CLOSE) + throw error("expected ')' at end of sort"); + + return ieee_float_spect(width_f - 1, width_e).to_type(); + }; + + sorts["Array"] = [this] { + // this gets two sorts as arguments, domain and range + auto domain = sort(); + auto range = sort(); + + // eat the ')' + if(next_token() != smt2_tokenizert::CLOSE) + throw error("expected ')' at end of Array sort"); + + // we can turn arrays that map an unsigned bitvector type + // to something else into our 'array_typet' + if(domain.id() == ID_unsignedbv) + return array_typet(range, infinity_exprt(domain)); + else + throw error("unsupported array sort"); + }; } smt2_parsert::signature_with_parameter_idst diff --git a/src/solvers/smt2/smt2_parser.h b/src/solvers/smt2/smt2_parser.h index 9b6ebde717c..959d25e7f4e 100644 --- a/src/solvers/smt2/smt2_parser.h +++ b/src/solvers/smt2/smt2_parser.h @@ -24,6 +24,7 @@ class smt2_parsert : exit(false), smt2_tokenizer(_in), parenthesis_level(0) { setup_commands(); + setup_sorts(); } virtual ~smt2_parsert() = default; @@ -121,7 +122,6 @@ class smt2_parsert const exprt::operandst &); exprt function_application_ieee_float_eq(const exprt::operandst &); exprt function_application_fp(const exprt::operandst &); - typet sort(); exprt::operandst operands(); typet function_signature_declaration(); signature_with_parameter_idst function_signature_definition(); @@ -142,6 +142,11 @@ class smt2_parsert /// Apply typecast to unsignedbv to given expression exprt cast_bv_to_unsigned(const exprt &); + // sorts + typet sort(); + std::unordered_map> sorts; + void setup_sorts(); + // hashtable for all commands std::unordered_map> commands; From a8aa59493556937347b4bb11b65bcd011109d44c Mon Sep 17 00:00:00 2001 From: Daniel Kroening Date: Wed, 2 Oct 2019 08:31:15 +0100 Subject: [PATCH 3/3] smt2_parser: expressions/functions are now in hash table This refactors the SMT2 parser to use hash tables instead of chains of if()...else if()... for expressions. This enables extensions, and may have a performance benefit as the number of expressions grows. --- src/solvers/smt2/smt2_parser.cpp | 597 +++++++++++++++---------------- src/solvers/smt2/smt2_parser.h | 6 +- 2 files changed, 283 insertions(+), 320 deletions(-) diff --git a/src/solvers/smt2/smt2_parser.cpp b/src/solvers/smt2/smt2_parser.cpp index 7b78e1de7c8..fcf85854fd0 100644 --- a/src/solvers/smt2/smt2_parser.cpp +++ b/src/solvers/smt2/smt2_parser.cpp @@ -542,295 +542,30 @@ exprt smt2_parsert::function_application() } else { - // non-indexed symbol; hash it - const irep_idt id = smt2_tokenizer.get_buffer(); + // non-indexed symbol, look up in expression table + const auto id = smt2_tokenizer.get_buffer(); + const auto e_it = expressions.find(id); + if(e_it != expressions.end()) + return e_it->second(); - if(id==ID_let) - return let_expression(); - else if(id==ID_forall || id==ID_exists) - return quantifier_expression(id); + // get the operands + auto op = operands(); - auto op=operands(); - - if(id==ID_and || - id==ID_or || - id==ID_xor) - { - return multi_ary(id, op); - } - else if(id==ID_not) - { - return unary(id, op); - } - else if(id==ID_equal || - id==ID_le || - id==ID_ge || - id==ID_lt || - id==ID_gt) - { - return binary_predicate(id, op); - } - else if(id=="bvule") - { - return binary_predicate(ID_le, op); - } - else if(id=="bvsle") - { - return binary_predicate(ID_le, cast_bv_to_signed(op)); - } - else if(id=="bvuge") - { - return binary_predicate(ID_ge, op); - } - else if(id=="bvsge") - { - return binary_predicate(ID_ge, cast_bv_to_signed(op)); - } - else if(id=="bvult") - { - return binary_predicate(ID_lt, op); - } - else if(id=="bvslt") - { - return binary_predicate(ID_lt, cast_bv_to_signed(op)); - } - else if(id=="bvugt") - { - return binary_predicate(ID_gt, op); - } - else if(id=="bvsgt") - { - return binary_predicate(ID_gt, cast_bv_to_signed(op)); - } - else if(id=="bvashr") - { - return cast_bv_to_unsigned(binary(ID_ashr, cast_bv_to_signed(op))); - } - else if(id=="bvlshr" || id=="bvshr") - { - return binary(ID_lshr, op); - } - else if(id=="bvlshr" || id=="bvashl" || id=="bvshl") - { - return binary(ID_shl, op); - } - else if(id=="bvand") - { - return multi_ary(ID_bitand, op); - } - else if(id=="bvnand") - { - return multi_ary(ID_bitnand, op); - } - else if(id=="bvor") - { - return multi_ary(ID_bitor, op); - } - else if(id=="bvnor") - { - return multi_ary(ID_bitnor, op); - } - else if(id=="bvxor") - { - return multi_ary(ID_bitxor, op); - } - else if(id=="bvxnor") - { - return multi_ary(ID_bitxnor, op); - } - else if(id=="bvnot") - { - return unary(ID_bitnot, op); - } - else if(id=="bvneg") - { - return unary(ID_unary_minus, op); - } - else if(id=="bvadd") - { - return multi_ary(ID_plus, op); - } - else if(id==ID_plus) - { - return multi_ary(id, op); - } - else if(id=="bvsub" || id=="-") - { - return binary(ID_minus, op); - } - else if(id=="bvmul" || id=="*") - { - return binary(ID_mult, op); - } - else if(id=="bvsdiv") - { - return cast_bv_to_unsigned(binary(ID_div, cast_bv_to_signed(op))); - } - else if(id=="bvudiv") - { - return binary(ID_div, op); - } - else if(id=="/" || id=="div") - { - return binary(ID_div, op); - } - else if(id=="bvsrem") - { - // 2's complement signed remainder (sign follows dividend) - // This matches our ID_mod, and what C does since C99. - return cast_bv_to_unsigned(binary(ID_mod, cast_bv_to_signed(op))); - } - else if(id=="bvsmod") - { - // 2's complement signed remainder (sign follows divisor) - // We don't have that. - return cast_bv_to_unsigned(binary(ID_mod, cast_bv_to_signed(op))); - } - else if(id=="bvurem" || id=="%") - { - return binary(ID_mod, op); - } - else if(id=="concat") - { - // add the widths - auto op_width = make_range(op).map([](const exprt &o) { - return to_unsignedbv_type(o.type()).get_width(); - }); - - const std::size_t total_width = - std::accumulate(op_width.begin(), op_width.end(), 0); - - return concatenation_exprt( - std::move(op), unsignedbv_typet(total_width)); - } - else if(id=="distinct") - { - // pair-wise different constraint, multi-ary - return multi_ary("distinct", op); - } - else if(id=="ite") - { - if(op.size()!=3) - throw error("ite takes three operands"); - - if(op[0].type().id()!=ID_bool) - throw error("ite takes a boolean as first operand"); - - if(op[1].type()!=op[2].type()) - throw error("ite needs matching types"); - - return if_exprt(op[0], op[1], op[2]); - } - else if(id=="=>" || id=="implies") - { - return binary(ID_implies, op); - } - else if(id == "select") - { - // array index - if(op.size() != 2) - throw error("select takes two operands"); - - if(op[0].type().id() != ID_array) - throw error("select expects array operand"); - - return index_exprt(op[0], op[1]); - } - else if(id == "store") - { - // array update - if(op.size() != 3) - throw error("store takes three operands"); - - if(op[0].type().id() != ID_array) - throw error("store expects array operand"); - - if(to_array_type(op[0].type()).subtype() != op[2].type()) - throw error("store expects value that matches array element type"); - - return with_exprt(op[0], op[1], op[2]); - } - else if(id == "fp.isNaN") - { - if(op.size() != 1) - throw error("fp.isNaN takes one operand"); - - if(op[0].type().id() != ID_floatbv) - throw error("fp.isNaN takes FloatingPoint operand"); - - return unary_predicate_exprt(ID_isnan, op[0]); - } - else if(id == "fp.isInf") - { - if(op.size() != 1) - throw error("fp.isInf takes one operand"); - - if(op[0].type().id() != ID_floatbv) - throw error("fp.isInf takes FloatingPoint operand"); - - return unary_predicate_exprt(ID_isinf, op[0]); - } - else if(id == "fp.isNormal") - { - if(op.size() != 1) - throw error("fp.isNormal takes one operand"); - - if(op[0].type().id() != ID_floatbv) - throw error("fp.isNormal takes FloatingPoint operand"); - - return isnormal_exprt(op[0]); - } - else if(id == "fp") - { - return function_application_fp(op); - } - else if( - id == "fp.add" || id == "fp.mul" || id == "fp.sub" || id == "fp.div") - { - return function_application_ieee_float_op(id, op); - } - else if(id == "fp.eq") - { - return function_application_ieee_float_eq(op); - } - else if(id == "fp.leq") - { - return binary_predicate(ID_le, op); - } - else if(id == "fp.lt") - { - return binary_predicate(ID_lt, op); - } - else if(id == "fp.geq") - { - return binary_predicate(ID_ge, op); - } - else if(id == "fp.gt") - { - return binary_predicate(ID_gt, op); - } - else if(id == "fp.neg") - { - return unary(ID_unary_minus, op); - } - else + // rummage through id_map + const irep_idt final_id = rename_id(id); + auto id_it = id_map.find(final_id); + if(id_it != id_map.end()) { - // rummage through id_map - const irep_idt final_id=rename_id(id); - auto id_it=id_map.find(final_id); - if(id_it!=id_map.end()) + if(id_it->second.type.id() == ID_mathematical_function) { - if(id_it->second.type.id()==ID_mathematical_function) - { - return function_application( - symbol_exprt(final_id, id_it->second.type), op); - } - else - return symbol_exprt(final_id, id_it->second.type); + return function_application( + symbol_exprt(final_id, id_it->second.type), op); } - - throw error() << "unknown function symbol '" << id << '\''; + else + return symbol_exprt(final_id, id_it->second.type); } + + throw error() << "unknown function symbol '" << id << '\''; } break; @@ -992,41 +727,14 @@ exprt smt2_parsert::expression() switch(next_token()) { case smt2_tokenizert::SYMBOL: - { - // hash it - const irep_idt identifier = smt2_tokenizer.get_buffer(); - - if(identifier == ID_true) - return true_exprt(); - else if(identifier == ID_false) - return false_exprt(); - else if(identifier == "roundNearestTiesToEven") - { - // we encode as 32-bit unsignedbv - return from_integer(ieee_floatt::ROUND_TO_EVEN, unsignedbv_typet(32)); - } - else if(identifier == "roundNearestTiesToAway") - { - throw error("unsupported rounding mode"); - } - else if(identifier == "roundTowardPositive") - { - // we encode as 32-bit unsignedbv - return from_integer(ieee_floatt::ROUND_TO_PLUS_INF, unsignedbv_typet(32)); - } - else if(identifier == "roundTowardNegative") - { - // we encode as 32-bit unsignedbv - return from_integer( - ieee_floatt::ROUND_TO_MINUS_INF, unsignedbv_typet(32)); - } - else if(identifier == "roundTowardZero") - { - // we encode as 32-bit unsignedbv - return from_integer(ieee_floatt::ROUND_TO_ZERO, unsignedbv_typet(32)); - } - else { + const auto &identifier = smt2_tokenizer.get_buffer(); + + // in the expression table? + const auto e_it = expressions.find(identifier); + if(e_it != expressions.end()) + return e_it->second(); + // rummage through id_map const irep_idt final_id = rename_id(identifier); auto id_it = id_map.find(final_id); @@ -1038,9 +746,9 @@ exprt smt2_parsert::expression() return std::move(symbol_expr); } + // don't know, give up throw error() << "unknown expression '" << identifier << '\''; } - } case smt2_tokenizert::NUMERAL: { @@ -1085,6 +793,259 @@ exprt smt2_parsert::expression() UNREACHABLE; } +void smt2_parsert::setup_expressions() +{ + expressions["true"] = [] { return true_exprt(); }; + expressions["false"] = [] { return false_exprt(); }; + + expressions["roundNearestTiesToEven"] = [] { + // we encode as 32-bit unsignedbv + return from_integer(ieee_floatt::ROUND_TO_EVEN, unsignedbv_typet(32)); + }; + + expressions["roundNearestTiesToAway"] = [this]() -> exprt { + throw error("unsupported rounding mode"); + }; + + expressions["roundTowardPositive"] = [] { + // we encode as 32-bit unsignedbv + return from_integer(ieee_floatt::ROUND_TO_PLUS_INF, unsignedbv_typet(32)); + }; + + expressions["roundTowardNegative"] = [] { + // we encode as 32-bit unsignedbv + return from_integer(ieee_floatt::ROUND_TO_MINUS_INF, unsignedbv_typet(32)); + }; + + expressions["roundTowardZero"] = [] { + // we encode as 32-bit unsignedbv + return from_integer(ieee_floatt::ROUND_TO_ZERO, unsignedbv_typet(32)); + }; + + expressions["let"] = [this] { return let_expression(); }; + expressions["exists"] = [this] { return quantifier_expression(ID_exists); }; + expressions["forall"] = [this] { return quantifier_expression(ID_forall); }; + expressions["and"] = [this] { return multi_ary(ID_and, operands()); }; + expressions["or"] = [this] { return multi_ary(ID_or, operands()); }; + expressions["xor"] = [this] { return multi_ary(ID_xor, operands()); }; + expressions["not"] = [this] { return unary(ID_not, operands()); }; + expressions["="] = [this] { return binary_predicate(ID_equal, operands()); }; + expressions["<="] = [this] { return binary_predicate(ID_le, operands()); }; + expressions[">="] = [this] { return binary_predicate(ID_ge, operands()); }; + expressions["<"] = [this] { return binary_predicate(ID_lt, operands()); }; + expressions[">"] = [this] { return binary_predicate(ID_gt, operands()); }; + + expressions["bvule"] = [this] { return binary_predicate(ID_le, operands()); }; + + expressions["bvsle"] = [this] { + return binary_predicate(ID_le, cast_bv_to_signed(operands())); + }; + + expressions["bvuge"] = [this] { return binary_predicate(ID_ge, operands()); }; + + expressions["bvsge"] = [this] { + return binary_predicate(ID_ge, cast_bv_to_signed(operands())); + }; + + expressions["bvult"] = [this] { return binary_predicate(ID_lt, operands()); }; + + expressions["bvslt"] = [this] { + return binary_predicate(ID_lt, cast_bv_to_signed(operands())); + }; + + expressions["bvugt"] = [this] { return binary_predicate(ID_gt, operands()); }; + + expressions["bvsgt"] = [this] { + return binary_predicate(ID_gt, cast_bv_to_signed(operands())); + }; + + expressions["bvashr"] = [this] { + return cast_bv_to_unsigned(binary(ID_ashr, cast_bv_to_signed(operands()))); + }; + + expressions["bvlshr"] = [this] { return binary(ID_lshr, operands()); }; + expressions["bvshr"] = [this] { return binary(ID_lshr, operands()); }; + expressions["bvlshl"] = [this] { return binary(ID_shl, operands()); }; + expressions["bvashl"] = [this] { return binary(ID_shl, operands()); }; + expressions["bvshl"] = [this] { return binary(ID_shl, operands()); }; + expressions["bvand"] = [this] { return multi_ary(ID_bitand, operands()); }; + expressions["bvnand"] = [this] { return multi_ary(ID_bitnand, operands()); }; + expressions["bvor"] = [this] { return multi_ary(ID_bitor, operands()); }; + expressions["bvnor"] = [this] { return multi_ary(ID_bitnor, operands()); }; + expressions["bvxor"] = [this] { return multi_ary(ID_bitxor, operands()); }; + expressions["bvxnor"] = [this] { return multi_ary(ID_bitxnor, operands()); }; + expressions["bvnot"] = [this] { return unary(ID_bitnot, operands()); }; + expressions["bvneg"] = [this] { return unary(ID_unary_minus, operands()); }; + expressions["bvadd"] = [this] { return multi_ary(ID_plus, operands()); }; + expressions["+"] = [this] { return multi_ary(ID_plus, operands()); }; + expressions["bvsub"] = [this] { return binary(ID_minus, operands()); }; + expressions["-"] = [this] { return binary(ID_minus, operands()); }; + expressions["bvmul"] = [this] { return binary(ID_mult, operands()); }; + expressions["*"] = [this] { return binary(ID_mult, operands()); }; + + expressions["bvsdiv"] = [this] { + return cast_bv_to_unsigned(binary(ID_div, cast_bv_to_signed(operands()))); + }; + + expressions["bvudiv"] = [this] { return binary(ID_div, operands()); }; + expressions["/"] = [this] { return binary(ID_div, operands()); }; + expressions["div"] = [this] { return binary(ID_div, operands()); }; + + expressions["bvsrem"] = [this] { + // 2's complement signed remainder (sign follows dividend) + // This matches our ID_mod, and what C does since C99. + return cast_bv_to_unsigned(binary(ID_mod, cast_bv_to_signed(operands()))); + }; + + expressions["bvsmod"] = [this] { + // 2's complement signed remainder (sign follows divisor) + // We don't have that. + return cast_bv_to_unsigned(binary(ID_mod, cast_bv_to_signed(operands()))); + }; + + expressions["bvurem"] = [this] { return binary(ID_mod, operands()); }; + + expressions["%"] = [this] { return binary(ID_mod, operands()); }; + + expressions["concat"] = [this] { + auto op = operands(); + + // add the widths + auto op_width = make_range(op).map( + [](const exprt &o) { return to_unsignedbv_type(o.type()).get_width(); }); + + const std::size_t total_width = + std::accumulate(op_width.begin(), op_width.end(), 0); + + return concatenation_exprt(std::move(op), unsignedbv_typet(total_width)); + }; + + expressions["distinct"] = [this] { + // pair-wise different constraint, multi-ary + return multi_ary("distinct", operands()); + }; + + expressions["ite"] = [this] { + auto op = operands(); + + if(op.size() != 3) + throw error("ite takes three operands"); + + if(op[0].type().id() != ID_bool) + throw error("ite takes a boolean as first operand"); + + if(op[1].type() != op[2].type()) + throw error("ite needs matching types"); + + return if_exprt(op[0], op[1], op[2]); + }; + + expressions["implies"] = [this] { return binary(ID_implies, operands()); }; + + expressions["=>"] = [this] { return binary(ID_implies, operands()); }; + + expressions["select"] = [this] { + auto op = operands(); + + // array index + if(op.size() != 2) + throw error("select takes two operands"); + + if(op[0].type().id() != ID_array) + throw error("select expects array operand"); + + return index_exprt(op[0], op[1]); + }; + + expressions["store"] = [this] { + auto op = operands(); + + // array update + if(op.size() != 3) + throw error("store takes three operands"); + + if(op[0].type().id() != ID_array) + throw error("store expects array operand"); + + if(to_array_type(op[0].type()).subtype() != op[2].type()) + throw error("store expects value that matches array element type"); + + return with_exprt(op[0], op[1], op[2]); + }; + + expressions["fp.isNaN"] = [this] { + auto op = operands(); + + if(op.size() != 1) + throw error("fp.isNaN takes one operand"); + + if(op[0].type().id() != ID_floatbv) + throw error("fp.isNaN takes FloatingPoint operand"); + + return unary_predicate_exprt(ID_isnan, op[0]); + }; + + expressions["fp.isInf"] = [this] { + auto op = operands(); + + if(op.size() != 1) + throw error("fp.isInf takes one operand"); + + if(op[0].type().id() != ID_floatbv) + throw error("fp.isInf takes FloatingPoint operand"); + + return unary_predicate_exprt(ID_isinf, op[0]); + }; + + expressions["fp.isNormal"] = [this] { + auto op = operands(); + + if(op.size() != 1) + throw error("fp.isNormal takes one operand"); + + if(op[0].type().id() != ID_floatbv) + throw error("fp.isNormal takes FloatingPoint operand"); + + return isnormal_exprt(op[0]); + }; + + expressions["fp"] = [this] { return function_application_fp(operands()); }; + + expressions["fp.add"] = [this] { + return function_application_ieee_float_op("fp.add", operands()); + }; + + expressions["fp.mul"] = [this] { + return function_application_ieee_float_op("fp.mul", operands()); + }; + + expressions["fp.sub"] = [this] { + return function_application_ieee_float_op("fp.sub", operands()); + }; + + expressions["fp.div"] = [this] { + return function_application_ieee_float_op("fp.div", operands()); + }; + + expressions["fp.eq"] = [this] { + return function_application_ieee_float_eq(operands()); + }; + + expressions["fp.leq"] = [this] { + return binary_predicate(ID_le, operands()); + }; + + expressions["fp.lt"] = [this] { return binary_predicate(ID_lt, operands()); }; + + expressions["fp.geq"] = [this] { + return binary_predicate(ID_ge, operands()); + }; + + expressions["fp.gt"] = [this] { return binary_predicate(ID_gt, operands()); }; + + expressions["fp.neg"] = [this] { return unary(ID_unary_minus, operands()); }; +} + typet smt2_parsert::sort() { // a sort is one of the following three cases: diff --git a/src/solvers/smt2/smt2_parser.h b/src/solvers/smt2/smt2_parser.h index 959d25e7f4e..29f30af8a7a 100644 --- a/src/solvers/smt2/smt2_parser.h +++ b/src/solvers/smt2/smt2_parser.h @@ -25,10 +25,9 @@ class smt2_parsert { setup_commands(); setup_sorts(); + setup_expressions(); } - virtual ~smt2_parsert() = default; - void parse() { command_sequence(); @@ -115,6 +114,9 @@ class smt2_parsert } }; + // expressions + std::unordered_map> expressions; + void setup_expressions(); exprt expression(); exprt function_application(); exprt function_application_ieee_float_op(