From 313e40429a534ab2c7b529c666b0c3e891b13bf4 Mon Sep 17 00:00:00 2001 From: Daniel Kroening Date: Tue, 1 Oct 2019 22:41:26 +0100 Subject: [PATCH] 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 dc79a2dcf4..2987ea26af 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 540fcabc37..9b6ebde717 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 @@ public: explicit smt2_parsert(std::istream &_in) : exit(false), smt2_tokenizer(_in), parenthesis_level(0) { + setup_commands(); } virtual ~smt2_parsert() = default; @@ -82,10 +84,6 @@ protected: 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 @@ protected: } }; - void ignore_command(); exprt expression(); exprt function_application(); exprt function_application_ieee_float_op( @@ -144,6 +141,14 @@ protected: /// 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 f30311d299..cb78b88056 100644 --- a/src/solvers/smt2/smt2_solver.cpp +++ b/src/solvers/smt2/smt2_solver.cpp @@ -28,12 +28,13 @@ public: 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