From ce4c008fda4cc8ab35aacec65157055aef48ec15 Mon Sep 17 00:00:00 2001 From: Romain Brenguier Date: Tue, 3 Apr 2018 15:01:27 +0100 Subject: [PATCH] Remove plus_exprt_with_overflow_check --- .../refinement/string_constraint_generator.h | 2 -- .../string_constraint_generator_main.cpp | 17 ----------------- 2 files changed, 19 deletions(-) diff --git a/src/solvers/refinement/string_constraint_generator.h b/src/solvers/refinement/string_constraint_generator.h index 00f9d4da6c2..bb77486bd2f 100644 --- a/src/solvers/refinement/string_constraint_generator.h +++ b/src/solvers/refinement/string_constraint_generator.h @@ -177,8 +177,6 @@ class string_constraint_generatort final array_string_exprt fresh_string(const typet &index_type, const typet &char_type); array_string_exprt get_string_expr(const exprt &expr); - plus_exprt plus_exprt_with_overflow_check(const exprt &op1, const exprt &op2); - static constant_exprt constant_char(int i, const typet &char_type); diff --git a/src/solvers/refinement/string_constraint_generator_main.cpp b/src/solvers/refinement/string_constraint_generator_main.cpp index 2e88bfdfe14..bf9c36ff0dd 100644 --- a/src/solvers/refinement/string_constraint_generator_main.cpp +++ b/src/solvers/refinement/string_constraint_generator_main.cpp @@ -145,23 +145,6 @@ exprt sum_overflows(const plus_exprt &sum) notequal_exprt(op1_negative, sum_negative)); } -/// Create a plus expression while adding extra constraints to axioms in order -/// to prevent overflows. -/// \param op1: First term of the sum -/// \param op2: Second term of the sum -/// \return A plus expression representing the sum of the arguments -/// \deprecated -plus_exprt string_constraint_generatort::plus_exprt_with_overflow_check( - const exprt &op1, const exprt &op2) -{ - const plus_exprt sum(plus_exprt(op1, op2)); - // We prevent overflows by adding the following constraint: - // If the signs of the two operands are the same, then the sign of the sum - // should also be the same. - lemmas.push_back(not_exprt(sum_overflows(sum))); - return sum; -} - /// Associate an actual finite length to infinite arrays /// \param s: array expression representing a string /// \return expression for the length of `s`