Skip to content

Address incremental SMT2 related code review comments from PR6357 #6388

New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Merged
merged 4 commits into from
Oct 13, 2021
Merged

Address incremental SMT2 related code review comments from PR6357 #6388

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
4 commits
Select commit Hold shift + click to select a range
2ca390c
Add comment with example strings matched or not by regex
thomasspriggs Oct 11, 2021
c3f1985
Simplify regex used in `is_valid_smt_identifier`
thomasspriggs Oct 11, 2021
232ecfd
Add comment explaining why smt identifiers are checked
thomasspriggs Oct 11, 2021
200500c
Rename `dependencies_needed` to `push_dependencies_needed`
thomasspriggs Oct 11, 2021
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
8 changes: 4 additions & 4 deletions src/solvers/smt2_incremental/smt2_incremental_decision_procedure.cpp
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -49,7 +49,7 @@ void smt2_incremental_decision_proceduret::define_dependent_functions(
return expr_identifier.first;
});
std::stack<exprt> to_be_defined;
const auto dependencies_needed = [&](const exprt &expr) {
const auto push_dependencies_needed = [&](const exprt &expr) {
Copy link
Contributor

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Can the type of the return value of the lambda also be defined there? -> bool - because it made it surprising to see a lambda named push-* in a context that demands a predicate without it having an explicit book return value.

bool result = false;
for(const auto &dependency : gather_dependent_expressions(expr))
{
Expand All @@ -60,11 +60,11 @@ void smt2_incremental_decision_proceduret::define_dependent_functions(
}
return result;
};
dependencies_needed(expr);
push_dependencies_needed(expr);
while(!to_be_defined.empty())
{
const exprt current = to_be_defined.top();
if(dependencies_needed(current))
if(push_dependencies_needed(current))
continue;
if(const auto symbol_expr = expr_try_dynamic_cast<symbol_exprt>(current))
{
Expand All @@ -81,7 +81,7 @@ void smt2_incremental_decision_proceduret::define_dependent_functions(
}
else
{
if(dependencies_needed(symbol->value))
if(push_dependencies_needed(symbol->value))
continue;
const smt_define_function_commandt function{
symbol->name, {}, convert_expr_to_smt(symbol->value)};
Expand Down
8 changes: 7 additions & 1 deletion src/solvers/smt2_incremental/smt_terms.cpp
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -50,13 +50,19 @@ bool smt_bool_literal_termt::value() const

static bool is_valid_smt_identifier(irep_idt identifier)
{
static const std::regex valid{R"(^[^\|]*$)"};
// The below regex matches a complete string which does not contain the `|`
// character. So it would match the string `foo bar`, but not `|foo bar|`.
static const std::regex valid{"[^\\|]*"};
return std::regex_match(id2string(identifier), valid);
}

smt_identifier_termt::smt_identifier_termt(irep_idt identifier, smt_sortt sort)
: smt_termt(ID_smt_identifier_term, std::move(sort))
{
// The below invariant exists as a sanity check that the string being used for
// the identifier is in unescaped form. This is because the escaping and
// unescaping are implementation details of the printing to string and
// response parsing respectively, not part of the underlying data.
INVARIANT(
is_valid_smt_identifier(identifier),
R"(Identifiers may not contain | characters.)");
Expand Down