From 751e8f51196a62eb64658ba1b8c90b102b54ae9f Mon Sep 17 00:00:00 2001 From: "Lukasz A.J. Wrona" Date: Tue, 19 Sep 2017 10:00:23 +0100 Subject: [PATCH] Adhere to lintage --- src/solvers/refinement/bv_refinement.h | 2 +- src/solvers/refinement/string_refinement.cpp | 44 +++++++++++--------- src/solvers/refinement/string_refinement.h | 6 ++- 3 files changed, 30 insertions(+), 22 deletions(-) diff --git a/src/solvers/refinement/bv_refinement.h b/src/solvers/refinement/bv_refinement.h index 0c2b5e22b3a..99475efd8ad 100644 --- a/src/solvers/refinement/bv_refinement.h +++ b/src/solvers/refinement/bv_refinement.h @@ -32,7 +32,7 @@ class bv_refinementt:public bv_pointerst bool refine_arithmetic=true; }; public: - struct infot : public configt + struct infot:public configt { const namespacet *ns=nullptr; propt *prop=nullptr; diff --git a/src/solvers/refinement/string_refinement.cpp b/src/solvers/refinement/string_refinement.cpp index 3c34a84f4f6..c7b349a0b12 100644 --- a/src/solvers/refinement/string_refinement.cpp +++ b/src/solvers/refinement/string_refinement.cpp @@ -139,7 +139,8 @@ optionalt expr_cast(const exprt& expr) } template -T expr_cast_v(const exprt& expr) { +T expr_cast_v(const exprt& expr) +{ const auto maybe=expr_cast(expr); INVARIANT(maybe, "Bad conversion"); return *maybe; @@ -535,7 +536,8 @@ std::vector concretize_results( const std::map>& current_index_set, const std::vector &universal_axioms) { - for(const auto &it : symbol_resolve) { + for(const auto &it : symbol_resolve) + { concretize_string( get, found_length, @@ -547,7 +549,8 @@ std::vector concretize_results( ns, it.second); } - for(const auto &expr : created_strings) { + for(const auto &expr : created_strings) + { concretize_string( get, found_length, @@ -654,7 +657,7 @@ void string_refinementt::set_to(const exprt &expr, bool value) { if(is_char_array(ns, rhs.type())) { - for (const auto& lemma : set_char_array_equality(lhs, rhs)) + for(const auto& lemma : set_char_array_equality(lhs, rhs)) add_lemma(lemma, false); } const bool not_handled=add_axioms_for_string_assigns( @@ -665,7 +668,7 @@ void string_refinementt::set_to(const exprt &expr, bool value) ns, lhs, subst_rhs); - if (!not_handled) + if(!not_handled) return; } @@ -753,7 +756,7 @@ decision_proceduret::resultt string_refinementt::dec_solve() symbol_resolve); if(!success) { - for (const auto& lemma : lemmas) + for(const auto& lemma : lemmas) add_lemma(lemma); debug() << "check_SAT: got SAT but the model is not correct" << eom; } @@ -772,8 +775,8 @@ decision_proceduret::resultt string_refinementt::dec_solve() initial_index_set(index_set, current_index_set, ns, universal_axioms); update_index_set(index_set, current_index_set, ns, cur); cur.clear(); - for (const auto& lemma : - generate_instantiations(current_index_set, universal_axioms)) + for(const auto& lemma : + generate_instantiations(current_index_set, universal_axioms)) add_lemma(lemma); display_current_index_set(debug(), ns, current_index_set); @@ -781,7 +784,7 @@ decision_proceduret::resultt string_refinementt::dec_solve() { decision_proceduret::resultt res=supert::dec_solve(); - if (res == resultt::D_SATISFIABLE) + if(res==resultt::D_SATISFIABLE) { bool success; std::vector lemmas; @@ -798,7 +801,7 @@ decision_proceduret::resultt string_refinementt::dec_solve() symbol_resolve); if(!success) { - for (const auto& lemma : lemmas) + for(const auto& lemma : lemmas) add_lemma(lemma); debug() << "check_SAT: got SAT but the model is not correct" << eom; } @@ -821,7 +824,7 @@ decision_proceduret::resultt string_refinementt::dec_solve() current_index_set.clear(); update_index_set(index_set, current_index_set, ns, cur); cur.clear(); - for (const auto& lemma : + for(const auto& lemma : generate_instantiations(current_index_set, universal_axioms)) add_lemma(lemma); display_current_index_set(debug(), ns, current_index_set); @@ -843,7 +846,7 @@ decision_proceduret::resultt string_refinementt::dec_solve() generator.get_created_strings(), current_index_set, universal_axioms); - for (const auto& lemma : lemmas) + for(const auto& lemma : lemmas) add_lemma(lemma); display_current_index_set(debug(), ns, current_index_set); return resultt::D_SATISFIABLE; @@ -867,7 +870,9 @@ decision_proceduret::resultt string_refinementt::dec_solve() for(const exprt &lemma : lemmas) add_lemma(lemma); } - } else { + } + else + { debug() << "check_SAT: default return " << static_cast(res) << eom; return res; } @@ -1923,7 +1928,8 @@ class find_index_visitort: public const_expr_visitort /// \param [in] str: the string which must be indexed /// \param [in] qvar: the universal variable that must be in the index /// \return an index expression in `expr` on `str` containing `qvar` -static exprt find_index(const exprt &expr, const exprt &str, const symbol_exprt &qvar) +static exprt find_index( + const exprt &expr, const exprt &str, const symbol_exprt &qvar) { find_index_visitort v(str, qvar); expr.visit(v); @@ -1972,7 +1978,8 @@ static std::vector instantiate_not_contains( // << from_expr(ns, "", s1) << eom; const auto& i0=index_set.find(s0.content()); const auto& i1=index_set.find(s1.content()); - if (i0 != index_set.end() && i1 != index_set.end()) { + if(i0!=index_set.end() && i1!=index_set.end()) + { return ::instantiate_not_contains( axiom, i0->second, i1->second, generator); } @@ -2025,9 +2032,8 @@ 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) { - return supert::get(expr); - }; + const auto super_get=[this](const exprt& expr) + { return supert::get(expr); }; exprt ecopy(expr); replace_expr(symbol_resolve, ecopy); if(is_char_array(ns, ecopy.type())) @@ -2047,7 +2053,7 @@ exprt string_refinementt::get(const exprt &expr) const } else if(ecopy.id()==ID_struct) { - if (const auto string=expr_cast(ecopy)) + if(const auto string=expr_cast(ecopy)) { const exprt &content=string->content(); const exprt &length=string->length(); diff --git a/src/solvers/refinement/string_refinement.h b/src/solvers/refinement/string_refinement.h index 632e2bb5f83..863b4e61929 100644 --- a/src/solvers/refinement/string_refinement.h +++ b/src/solvers/refinement/string_refinement.h @@ -32,7 +32,8 @@ Author: Alberto Griggio, alberto.griggio@gmail.com class string_refinementt final: public bv_refinementt { private: - struct configt { + struct configt + { unsigned refinement_bound=0; /// Make non-deterministic character arrays have at least one character bool string_non_empty=false; @@ -98,5 +99,6 @@ class string_refinementt final: public bv_refinementt }; exprt substitute_array_lists(exprt expr, size_t string_max_length); -exprt concretize_arrays_in_expression(exprt expr, std::size_t string_max_length); +exprt concretize_arrays_in_expression( + exprt expr, std::size_t string_max_length); #endif