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.
This commit is contained in:
parent
00c7e3d836
commit
313e40429a
|
@ -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; };
|
||||
}
|
||||
|
|
|
@ -10,6 +10,7 @@ Author: Daniel Kroening, kroening@kroening.com
|
|||
#define CPROVER_SOLVERS_SMT2_SMT2_PARSER_H
|
||||
|
||||
#include <map>
|
||||
#include <unordered_map>
|
||||
|
||||
#include <util/mathematical_types.h>
|
||||
#include <util/std_expr.h>
|
||||
|
@ -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<irep_idt, irep_idt>;
|
||||
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<std::string, std::function<void()>> commands;
|
||||
|
||||
void command_sequence();
|
||||
void command(const std::string &);
|
||||
void ignore_command();
|
||||
void setup_commands();
|
||||
};
|
||||
|
||||
#endif // CPROVER_SOLVERS_SMT2_SMT2_PARSER_H
|
||||
|
|
|
@ -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<exprt> 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
|
||||
|
|
Loading…
Reference in New Issue