From c078a69c95183bfae4ab0e7aa2c79bf69a785ce5 Mon Sep 17 00:00:00 2001 From: Michael Tautschnig Date: Sat, 10 Nov 2018 09:46:56 +0000 Subject: [PATCH] Add missing member initializers of string_constraintst-typed value add_axioms_for_char_at, add_axioms_for_is_empty, add_axioms_from_char only initialized one of the three vectors. --- .../refinement/string_constraint_generator_main.cpp | 5 +++-- .../refinement/string_constraint_generator_testing.cpp | 8 ++++---- .../refinement/string_constraint_generator_valueof.cpp | 6 ++++-- 3 files changed, 11 insertions(+), 8 deletions(-) diff --git a/src/solvers/refinement/string_constraint_generator_main.cpp b/src/solvers/refinement/string_constraint_generator_main.cpp index 325a096d931..e1d1cc411be 100644 --- a/src/solvers/refinement/string_constraint_generator_main.cpp +++ b/src/solvers/refinement/string_constraint_generator_main.cpp @@ -571,8 +571,9 @@ std::pair add_axioms_for_char_at( PRECONDITION(f.arguments().size() == 2); array_string_exprt str = get_string_expr(array_pool, f.arguments()[0]); symbol_exprt char_sym = fresh_symbol("char", str.type().subtype()); - const exprt constraint = equal_exprt(char_sym, str[f.arguments()[1]]); - return {char_sym, {{constraint}}}; + string_constraintst constraints; + constraints.existential = {equal_exprt(char_sym, str[f.arguments()[1]])}; + return {std::move(char_sym), std::move(constraints)}; } exprt minimum(const exprt &a, const exprt &b) diff --git a/src/solvers/refinement/string_constraint_generator_testing.cpp b/src/solvers/refinement/string_constraint_generator_testing.cpp index d75cdc9c641..4fbf7727a2b 100644 --- a/src/solvers/refinement/string_constraint_generator_testing.cpp +++ b/src/solvers/refinement/string_constraint_generator_testing.cpp @@ -136,10 +136,10 @@ std::pair add_axioms_for_is_empty( symbol_exprt is_empty = fresh_symbol("is_empty"); array_string_exprt s0 = get_string_expr(array_pool, f.arguments()[0]); - std::vector constraints; - constraints.push_back(implies_exprt(is_empty, length_eq(s0, 0))); - constraints.push_back(implies_exprt(length_eq(s0, 0), is_empty)); - return {typecast_exprt(is_empty, f.type()), {constraints}}; + string_constraintst constraints; + constraints.existential = {implies_exprt(is_empty, length_eq(s0, 0)), + implies_exprt(length_eq(s0, 0), is_empty)}; + return {typecast_exprt(is_empty, f.type()), std::move(constraints)}; } /// Test if the target is a suffix of the string diff --git a/src/solvers/refinement/string_constraint_generator_valueof.cpp b/src/solvers/refinement/string_constraint_generator_valueof.cpp index 4cb7e8ddb7c..e7ba1b887fa 100644 --- a/src/solvers/refinement/string_constraint_generator_valueof.cpp +++ b/src/solvers/refinement/string_constraint_generator_valueof.cpp @@ -312,8 +312,10 @@ std::pair add_axioms_from_char( const array_string_exprt &res, const exprt &c) { - const and_exprt lemma(equal_exprt(res[0], c), length_eq(res, 1)); - return {from_integer(0, get_return_code_type()), {{lemma}}}; + string_constraintst constraints; + constraints.existential = { + and_exprt(equal_exprt(res[0], c), length_eq(res, 1))}; + return {from_integer(0, get_return_code_type()), std::move(constraints)}; } /// Add axioms making the return value true if the given string is a correct