diff --git a/jbmc/unit/solvers/refinement/string_constraint_instantiation/instantiate_not_contains.cpp b/jbmc/unit/solvers/refinement/string_constraint_instantiation/instantiate_not_contains.cpp index b5c936b32f6..86d4ec5c572 100644 --- a/jbmc/unit/solvers/refinement/string_constraint_instantiation/instantiate_not_contains.cpp +++ b/jbmc/unit/solvers/refinement/string_constraint_instantiation/instantiate_not_contains.cpp @@ -191,8 +191,7 @@ SCENARIO("instantiate_not_contains", // Generating the corresponding axioms and simplifying, recording info string_constraint_generatort generator(empty_ns); - const auto pair = generator.add_axioms_for_function_application( - generator.fresh_symbol, func); + const auto pair = generator.add_axioms_for_function_application(func); const string_constraintst &constraints = pair.second; std::string axioms; diff --git a/src/solvers/refinement/refine_arrays.cpp b/src/solvers/refinement/refine_arrays.cpp index aa67f97c625..2e713b44d39 100644 --- a/src/solvers/refinement/refine_arrays.cpp +++ b/src/solvers/refinement/refine_arrays.cpp @@ -119,9 +119,9 @@ void bv_refinementt::freeze_lazy_constraints() for(const auto &constraint : lazy_array_constraints) { - std::set symbols; - find_symbols(constraint.lazy, symbols); - for(const auto &symbol : symbols) + std::set symbols_in_constraint; + find_symbols(constraint.lazy, symbols_in_constraint); + for(const auto &symbol : symbols_in_constraint) { const bvt bv=convert_bv(symbol); forall_literals(b_it, bv) diff --git a/src/solvers/refinement/string_builtin_function.cpp b/src/solvers/refinement/string_builtin_function.cpp index 51a6e7c1fa7..e82eb5b9487 100644 --- a/src/solvers/refinement/string_builtin_function.cpp +++ b/src/solvers/refinement/string_builtin_function.cpp @@ -129,12 +129,12 @@ std::vector string_concatenation_builtin_functiont::eval( ? std::max(std::min(args_value[1], input2_size), start_index) : input2_size; - std::vector result(input1_value); - result.insert( - result.end(), + std::vector eval_result(input1_value); + eval_result.insert( + eval_result.end(), input2_value.begin() + numeric_cast_v(start_index), input2_value.begin() + numeric_cast_v(end_index)); - return result; + return eval_result; } string_constraintst string_concatenation_builtin_functiont::constraints( @@ -458,12 +458,12 @@ std::vector string_insertion_builtin_functiont::eval( ? std::max(std::min(args_value[2], input2_size), mp_integer(0)) : input2_size; - std::vector result(input1_value); - result.insert( - result.begin() + numeric_cast_v(offset), + std::vector eval_result(input1_value); + eval_result.insert( + eval_result.begin() + numeric_cast_v(offset), input2_value.begin() + numeric_cast_v(start), input2_value.begin() + numeric_cast_v(end)); - return result; + return eval_result; } optionalt string_insertion_builtin_functiont::eval( @@ -634,8 +634,8 @@ string_builtin_function_with_no_evalt::string_builtin_function_with_no_evalt( string_constraintst string_builtin_function_with_no_evalt::constraints( string_constraint_generatort &generator) const { - auto pair = generator.add_axioms_for_function_application( - generator.fresh_symbol, function_application); + auto pair = + generator.add_axioms_for_function_application(function_application); pair.second.existential.push_back(equal_exprt(pair.first, return_code)); return pair.second; } diff --git a/src/solvers/refinement/string_constraint_generator.h b/src/solvers/refinement/string_constraint_generator.h index 3846ff91c4e..3a1d6de2157 100644 --- a/src/solvers/refinement/string_constraint_generator.h +++ b/src/solvers/refinement/string_constraint_generator.h @@ -127,7 +127,6 @@ class string_constraint_generatort final explicit string_constraint_generatort(const namespacet &ns); std::pair add_axioms_for_function_application( - symbol_generatort &fresh_symbol, const function_application_exprt &expr); symbol_generatort fresh_symbol; @@ -150,7 +149,6 @@ class string_constraint_generatort final /// string pointers. /// \deprecated Not tested. std::pair add_axioms_for_intern( - symbol_generatort &fresh_symbol, const function_application_exprt &f); exprt associate_array_to_pointer(const function_application_exprt &f); @@ -161,7 +159,6 @@ class string_constraint_generatort final // The specification is partial: the actual value is not actually computed // but we ensure that hash codes of equal strings are equal. std::pair add_axioms_for_hash_code( - symbol_generatort &fresh_symbol, const function_application_exprt &f, array_poolt &pool); diff --git a/src/solvers/refinement/string_constraint_generator_comparison.cpp b/src/solvers/refinement/string_constraint_generator_comparison.cpp index 9fe1b92759a..7c956342ffb 100644 --- a/src/solvers/refinement/string_constraint_generator_comparison.cpp +++ b/src/solvers/refinement/string_constraint_generator_comparison.cpp @@ -182,18 +182,16 @@ std::pair add_axioms_for_equals_ignore_case( /// These axioms are, for each string `s` on which hash was called: /// * \f$ hash(str)=hash(s) \lor |str| \ne |s| /// \lor (|str|=|s| \land \exists i<|s|.\ s[i]\ne str[i]) \f$ -/// \param fresh_symbol: generator of fresh symbols /// \param f: function application with argument refined_string `str` /// \param pool: pool of arrays representing strings /// \return integer expression `hash(str)` std::pair string_constraint_generatort::add_axioms_for_hash_code( - symbol_generatort &fresh_symbol, const function_application_exprt &f, array_poolt &pool) { PRECONDITION(f.arguments().size() == 1); - string_constraintst constraints; + string_constraintst hash_constraints; const array_string_exprt str = get_string_expr(pool, f.arguments()[0]); const typet &return_type = f.type(); const typet &index_type = str.length().type(); @@ -212,9 +210,9 @@ string_constraint_generatort::add_axioms_for_hash_code( and_exprt( notequal_exprt(str[i], it.first[i]), and_exprt(length_gt(str, i), is_positive(i)))); - constraints.existential.push_back(or_exprt(c1, or_exprt(c2, c3))); + hash_constraints.existential.push_back(or_exprt(c1, or_exprt(c2, c3))); } - return {hash, std::move(constraints)}; + return {hash, std::move(hash_constraints)}; } /// Lexicographic comparison of two strings @@ -302,17 +300,15 @@ std::pair add_axioms_for_compare_to( /// Add axioms stating that the return value for two equal string should be the /// same /// \deprecated never tested -/// \param fresh_symbol: generator of fresh symbols /// \param f: function application with one string argument /// \return a string expression DEPRECATED("never tested") std::pair string_constraint_generatort::add_axioms_for_intern( - symbol_generatort &fresh_symbol, const function_application_exprt &f) { PRECONDITION(f.arguments().size() == 1); - string_constraintst constraints; + string_constraintst intern_constraints; const array_string_exprt str = get_string_expr(array_pool, f.arguments()[0]); // For now we only enforce content equality and not pointer equality const typet &return_type=f.type(); @@ -330,14 +326,14 @@ string_constraint_generatort::add_axioms_for_intern( exprt::operandst disj; for(auto it : intern_of_string) disj.push_back(equal_exprt(intern, it.second)); - constraints.existential.push_back(disjunction(disj)); + intern_constraints.existential.push_back(disjunction(disj)); // WARNING: the specification may be incomplete or incorrect for(auto it : intern_of_string) if(it.second!=str) { symbol_exprt i = fresh_symbol("index_intern", index_type); - constraints.existential.push_back(or_exprt( + intern_constraints.existential.push_back(or_exprt( equal_exprt(it.second, intern), or_exprt( notequal_exprt(str.length(), it.first.length()), @@ -348,5 +344,5 @@ string_constraint_generatort::add_axioms_for_intern( and_exprt(length_gt(str, i), is_positive(i))))))); } - return {intern, std::move(constraints)}; + return {intern, std::move(intern_constraints)}; } diff --git a/src/solvers/refinement/string_constraint_generator_float.cpp b/src/solvers/refinement/string_constraint_generator_float.cpp index f7937430051..6ff6d9ee240 100644 --- a/src/solvers/refinement/string_constraint_generator_float.cpp +++ b/src/solvers/refinement/string_constraint_generator_float.cpp @@ -337,14 +337,14 @@ std::pair add_axioms_for_fractional_part( /// \todo For now we only consider single precision. /// \param fresh_symbol: generator of fresh symbols /// \param res: string expression representing the float in scientific notation -/// \param f: a float expression, which is positive +/// \param float_expr: a float expression, which is positive /// \param array_pool: pool of arrays representing strings /// \param ns: namespace /// \return a integer expression different from 0 to signal an exception std::pair add_axioms_from_float_scientific_notation( symbol_generatort &fresh_symbol, const array_string_exprt &res, - const exprt &f, + const exprt &float_expr, array_poolt &array_pool, const namespacet &ns) { @@ -359,13 +359,13 @@ std::pair add_axioms_from_float_scientific_notation( exprt round_to_zero_expr=from_integer(ieee_floatt::ROUND_TO_ZERO, int_type); // `bin_exponent` is $e$ in the formulas - exprt bin_exponent=get_exponent(f, float_spec); + exprt bin_exponent = get_exponent(float_expr, float_spec); // $m$ from the formula is a value between 0.0 and 2.0 represented // with values in the range 0x000000 0xFFFFFF so 1 corresponds to 0x800000. // `bin_significand_int` represents $m * 0x800000$ - exprt bin_significand_int= - get_significand(f, float_spec, unsignedbv_typet(32)); + exprt bin_significand_int = + get_significand(float_expr, float_spec, unsignedbv_typet(32)); // `bin_significand` represents $m$ and is obtained // by multiplying `binary_significand_as_int` by // 1/0x800000 = 2^-23 = 1.1920928955078125 * 10^-7 @@ -375,7 +375,8 @@ std::pair add_axioms_from_float_scientific_notation( // This is a first approximation of the exponent that will adjust // if the fraction we get is greater than 10 - exprt dec_exponent_estimate=estimate_decimal_exponent(f, float_spec); + exprt dec_exponent_estimate = + estimate_decimal_exponent(float_expr, float_spec); // Table for values of $2^x / 10^(floor(log_10(2)*x))$ where x=Range[0,128] std::vector two_power_e_over_ten_power_d_table( @@ -422,10 +423,12 @@ std::pair add_axioms_from_float_scientific_notation( int_type); array_exprt conversion_factor_table( array_typet(float_type, conversion_factor_table_size)); - for(const auto &f : two_power_e_over_ten_power_d_table_negatives) - conversion_factor_table.copy_to_operands(constant_float(f, float_spec)); - for(const auto &f : two_power_e_over_ten_power_d_table) - conversion_factor_table.copy_to_operands(constant_float(f, float_spec)); + for(const auto &negative : two_power_e_over_ten_power_d_table_negatives) + conversion_factor_table.copy_to_operands( + constant_float(negative, float_spec)); + for(const auto &positive : two_power_e_over_ten_power_d_table) + conversion_factor_table.copy_to_operands( + constant_float(positive, float_spec)); // The index in the table, corresponding to exponent e is e+128 plus_exprt shifted_index(bin_exponent, from_integer(128, int_type)); @@ -460,7 +463,7 @@ std::pair add_axioms_from_float_scientific_notation( minus_exprt fractional_part( dec_significand, floatbv_of_int_expr(dec_significand_int, float_spec)); - // shifted_float is floor(f * 1e5) + // shifted_float is floor(float_expr * 1e5) exprt shifting=constant_float(1e5, float_spec); exprt shifted_float= round_expr_to_zero(floatbv_mult(fractional_part, shifting)); @@ -469,7 +472,7 @@ std::pair add_axioms_from_float_scientific_notation( // the exponent notation. exprt max_non_exponent_notation=from_integer(100000, shifted_float.type()); - // fractional_part_shifted is floor(f * 100000) % 100000 + // fractional_part_shifted is floor(float_expr * 100000) % 100000 const mod_exprt fractional_part_shifted( shifted_float, max_non_exponent_notation); diff --git a/src/solvers/refinement/string_constraint_generator_main.cpp b/src/solvers/refinement/string_constraint_generator_main.cpp index 5f16df11e8b..02da80879fa 100644 --- a/src/solvers/refinement/string_constraint_generator_main.cpp +++ b/src/solvers/refinement/string_constraint_generator_main.cpp @@ -363,12 +363,10 @@ optionalt string_constraint_generatort::make_array_pointer_association( /// strings contained in this call are converted to objects of type /// `string_exprt`, through adding axioms. Axioms are then added to enforce that /// the result corresponds to the function application. -/// \param fresh_symbol: generator of fresh symbols /// \param expr: an expression containing a function application /// \return expression corresponding to the result of the function application std::pair string_constraint_generatort::add_axioms_for_function_application( - symbol_generatort &fresh_symbol, const function_application_exprt &expr) { const irep_idt &id = get_function_name(expr); @@ -396,7 +394,7 @@ string_constraint_generatort::add_axioms_for_function_application( else if(id==ID_cprover_string_contains_func) return add_axioms_for_contains(fresh_symbol, expr, array_pool); else if(id==ID_cprover_string_hash_code_func) - return add_axioms_for_hash_code(fresh_symbol, expr, array_pool); + return add_axioms_for_hash_code(expr, array_pool); else if(id==ID_cprover_string_index_of_func) return add_axioms_for_index_of(fresh_symbol, expr, array_pool); else if(id==ID_cprover_string_last_index_of_func) @@ -463,7 +461,7 @@ string_constraint_generatort::add_axioms_for_function_application( else if(id==ID_cprover_string_replace_func) return add_axioms_for_replace(fresh_symbol, expr, array_pool); else if(id==ID_cprover_string_intern_func) - return add_axioms_for_intern(fresh_symbol, expr); + return add_axioms_for_intern(expr); else if(id==ID_cprover_string_format_func) return add_axioms_for_format(fresh_symbol, expr, array_pool, message, ns); else if(id == ID_cprover_string_constrain_characters_func) diff --git a/src/solvers/refinement/string_refinement.cpp b/src/solvers/refinement/string_refinement.cpp index 8aa89e992c3..3dbe59ba22b 100644 --- a/src/solvers/refinement/string_refinement.cpp +++ b/src/solvers/refinement/string_refinement.cpp @@ -738,8 +738,8 @@ decision_proceduret::resultt string_refinementt::dec_solve() // Initial try without index set const auto get = [this](const exprt &expr) { return this->get(expr); }; dependencies.clean_cache(); - const decision_proceduret::resultt res=supert::dec_solve(); - if(res==resultt::D_SATISFIABLE) + const decision_proceduret::resultt initial_result = supert::dec_solve(); + if(initial_result == resultt::D_SATISFIABLE) { bool satisfied; std::vector counter_examples; @@ -762,23 +762,23 @@ decision_proceduret::resultt string_refinementt::dec_solve() else { debug() << "check_SAT: got UNSAT or ERROR" << eom; - return res; + return initial_result; } initial_index_set(index_sets, ns, axioms); update_index_set(index_sets, ns, current_constraints); current_constraints.clear(); - const auto instances = + const auto initial_instances = generate_instantiations(index_sets, axioms, not_contain_witnesses); - for(const auto &instance : instances) + for(const auto &instance : initial_instances) add_lemma(instance); while((loop_bound_--)>0) { dependencies.clean_cache(); - const decision_proceduret::resultt res=supert::dec_solve(); + const decision_proceduret::resultt refined_result = supert::dec_solve(); - if(res==resultt::D_SATISFIABLE) + if(refined_result == resultt::D_SATISFIABLE) { bool satisfied; std::vector counter_examples; @@ -833,8 +833,9 @@ decision_proceduret::resultt string_refinementt::dec_solve() } else { - debug() << "check_SAT: default return " << static_cast(res) << eom; - return res; + debug() << "check_SAT: default return " + << static_cast(refined_result) << eom; + return refined_result; } } debug() << "string_refinementt::dec_solve reached the maximum number"