From e125e8a2c45b0e648e242fad9b1a5c7b71f8aea1 Mon Sep 17 00:00:00 2001 From: Romain Brenguier Date: Fri, 29 Sep 2017 15:14:43 +0100 Subject: [PATCH 1/4] Refactor gather_indices to use for_each instead of visitor --- src/solvers/refinement/string_refinement.cpp | 34 +++++++------------- 1 file changed, 12 insertions(+), 22 deletions(-) diff --git a/src/solvers/refinement/string_refinement.cpp b/src/solvers/refinement/string_refinement.cpp index e70ea613c5c..3827e1f33cd 100644 --- a/src/solvers/refinement/string_refinement.cpp +++ b/src/solvers/refinement/string_refinement.cpp @@ -2003,31 +2003,21 @@ static optionalt find_counter_example( typedef std::map> array_index_mapt; /// \related string_constraintt -class gather_indices_visitort: public const_expr_visitort +static array_index_mapt gather_indices(const exprt &expr) { -public: array_index_mapt indices; - - gather_indices_visitort(): indices() {} - - void operator()(const exprt &expr) override - { - if(expr.id()==ID_index) + // clang-format off + std::for_each( + expr.depth_begin(), + expr.depth_end(), + [&](const exprt &expr) { - const index_exprt &index=to_index_expr(expr); - const exprt &s(index.array()); - const exprt &i(index.index()); - indices[s].push_back(i); - } - } -}; - -/// \related string_constraintt -static array_index_mapt gather_indices(const exprt &expr) -{ - gather_indices_visitort v; - expr.visit(v); - return v.indices; + const auto index_expr = expr_try_dynamic_cast(expr); + if(index_expr) + indices[index_expr->array()].push_back(index_expr->index()); + }); + // clang-format on + return indices; } /// \param expr: an expression From 9d1aa99867fc2f8f1e93994712cbbca16f1b795d Mon Sep 17 00:00:00 2001 From: Romain Brenguier Date: Thu, 2 Nov 2017 12:32:54 +0000 Subject: [PATCH 2/4] Correct constraints added for char_set The string constraint body should not contain the universal variable outside of string access. However this is allowed in the guard, which we use here. The meaning of the constraint is the same, but it is of a form accepted by the string solver. --- .../string_constraint_generator_transformation.cpp | 6 ++++-- 1 file changed, 4 insertions(+), 2 deletions(-) diff --git a/src/solvers/refinement/string_constraint_generator_transformation.cpp b/src/solvers/refinement/string_constraint_generator_transformation.cpp index 0f6d5f624a1..b4fdbd77c93 100644 --- a/src/solvers/refinement/string_constraint_generator_transformation.cpp +++ b/src/solvers/refinement/string_constraint_generator_transformation.cpp @@ -354,8 +354,10 @@ exprt string_constraint_generatort::add_axioms_for_char_set( axioms.push_back(equal_exprt(res.length(), str.length())); axioms.push_back(equal_exprt(res[position], character)); const symbol_exprt q = fresh_univ_index("QA_char_set", position.type()); - or_exprt a3_body(equal_exprt(q, position), equal_exprt(res[q], str[q])); - axioms.push_back(string_constraintt(q, res.length(), a3_body)); + equal_exprt a3_body(res[q], str[q]); + notequal_exprt a3_guard(q, position); + axioms.push_back(string_constraintt( + q, from_integer(0, q.type()), res.length(), a3_guard, a3_body)); return if_exprt( out_of_bounds, from_integer(1, f.type()), from_integer(0, f.type())); } From f5991ee53d1a2b604072b39923dbfcef47d7f123 Mon Sep 17 00:00:00 2001 From: Romain Brenguier Date: Fri, 29 Sep 2017 15:34:51 +0100 Subject: [PATCH 3/4] Refactor universal_only_in_index to use expression iterators --- src/solvers/refinement/string_refinement.cpp | 29 ++++---------------- 1 file changed, 5 insertions(+), 24 deletions(-) diff --git a/src/solvers/refinement/string_refinement.cpp b/src/solvers/refinement/string_refinement.cpp index 3827e1f33cd..11d6f6c5fba 100644 --- a/src/solvers/refinement/string_refinement.cpp +++ b/src/solvers/refinement/string_refinement.cpp @@ -2054,33 +2054,14 @@ is_linear_arithmetic_expr(const exprt &expr, const symbol_exprt &var) /// false otherwise. static bool universal_only_in_index(const string_constraintt &expr) { - // For efficiency, we do a depth-first search of the - // body. The exprt visitors do a BFS and hide the stack/queue, so we would - // need to store a map from child to parent. - - // The unsigned int represents index depth we are. For example, if we are - // considering the fragment `a[b[x]]` (not inside an index expression), then - // the stack would look something like `[..., (a, 0), (b, 1), (x, 2)]`. - typedef std::pair valuet; - std::stack stack; - // We start at 0 since expr is not an index expression, so expr.body() is not - // in an index expression. - stack.push(valuet(expr.body(), 0)); - while(!stack.empty()) + for(auto it = expr.body().depth_begin(); it != expr.body().depth_end();) { - // Inspect current value - const valuet cur=stack.top(); - stack.pop(); - const exprt e=cur.first; - const unsigned index_depth=cur.second; - const unsigned child_index_depth=index_depth+(e.id()==ID_index?0:1); - - // If we found the universal variable not in an index_exprt, fail - if(e==expr.univ_var() && index_depth==0) + if(*it == expr.univ_var()) return false; + if(it->id() == ID_index) + it.next_sibling_or_parent(); else - forall_operands(it, e) - stack.push(valuet(*it, child_index_depth)); + ++it; } return true; } From d378980cc0ae95e0a2731261d2555b0d0c83a4d6 Mon Sep 17 00:00:00 2001 From: Romain Brenguier Date: Thu, 2 Nov 2017 09:58:29 +0000 Subject: [PATCH 4/4] Style: Disabling clang-format in get This is to allow us to put brackets on a new line, as cpplint likes it. --- src/solvers/refinement/string_refinement.cpp | 6 +++++- 1 file changed, 5 insertions(+), 1 deletion(-) diff --git a/src/solvers/refinement/string_refinement.cpp b/src/solvers/refinement/string_refinement.cpp index 11d6f6c5fba..538bf728687 100644 --- a/src/solvers/refinement/string_refinement.cpp +++ b/src/solvers/refinement/string_refinement.cpp @@ -1924,9 +1924,13 @@ exprt substitute_array_lists(exprt expr, size_t string_max_length) /// \return an expression exprt string_refinementt::get(const exprt &expr) const { - const auto super_get = [this](const exprt &expr) { // NOLINT + // clang-format off + const auto super_get = [this](const exprt &expr) + { return supert::get(expr); }; + // clang-format on + exprt ecopy(expr); (void)symbol_resolve.replace_expr(ecopy);