From e0475561a89bfd97f14589eec712c063e5ead803 Mon Sep 17 00:00:00 2001 From: Romain Brenguier Date: Mon, 21 Aug 2017 14:36:05 +0100 Subject: [PATCH 1/2] Making is_refined_string_type a non-member function Writing refined_string_typet::is_refined_string_type was long and had redundant information. The new version is more succinct and contains as much information. --- .../string_constraint_generator_concat.cpp | 4 ++-- .../string_constraint_generator_constants.cpp | 2 +- .../string_constraint_generator_indexof.cpp | 2 +- .../string_constraint_generator_main.cpp | 10 ++++----- src/solvers/refinement/string_refinement.cpp | 21 ++++++++----------- src/util/refined_string_type.cpp | 12 ----------- src/util/refined_string_type.h | 21 ++++++++++--------- 7 files changed, 28 insertions(+), 44 deletions(-) diff --git a/src/solvers/refinement/string_constraint_generator_concat.cpp b/src/solvers/refinement/string_constraint_generator_concat.cpp index 7f183071a9a..40a59265c89 100644 --- a/src/solvers/refinement/string_constraint_generator_concat.cpp +++ b/src/solvers/refinement/string_constraint_generator_concat.cpp @@ -171,7 +171,7 @@ string_exprt string_constraint_generatort::add_axioms_for_concat_double( const function_application_exprt &f) { string_exprt s1=get_string_expr(args(f, 2)[0]); - PRECONDITION(refined_string_typet::is_refined_string_type(f.type())); + PRECONDITION(is_refined_string_type(f.type())); refined_string_typet ref_type=to_refined_string_type(f.type()); string_exprt s2=add_axioms_for_string_of_float(args(f, 2)[1], ref_type); return add_axioms_for_concat(s1, s2); @@ -184,7 +184,7 @@ string_exprt string_constraint_generatort::add_axioms_for_concat_float( const function_application_exprt &f) { string_exprt s1=get_string_expr(args(f, 2)[0]); - PRECONDITION(refined_string_typet::is_refined_string_type(f.type())); + PRECONDITION(is_refined_string_type(f.type())); refined_string_typet ref_type=to_refined_string_type(f.type()); string_exprt s2=add_axioms_for_string_of_float(args(f, 2)[1], ref_type); return add_axioms_for_concat(s1, s2); diff --git a/src/solvers/refinement/string_constraint_generator_constants.cpp b/src/solvers/refinement/string_constraint_generator_constants.cpp index 5798702ea56..13fea55161c 100644 --- a/src/solvers/refinement/string_constraint_generator_constants.cpp +++ b/src/solvers/refinement/string_constraint_generator_constants.cpp @@ -56,7 +56,7 @@ string_exprt string_constraint_generatort::add_axioms_for_empty_string( const function_application_exprt &f) { PRECONDITION(f.arguments().empty()); - PRECONDITION(refined_string_typet::is_refined_string_type(f.type())); + PRECONDITION(is_refined_string_type(f.type())); const refined_string_typet &ref_type=to_refined_string_type(f.type()); return empty_string(ref_type); } diff --git a/src/solvers/refinement/string_constraint_generator_indexof.cpp b/src/solvers/refinement/string_constraint_generator_indexof.cpp index 5990fc4c9ee..1dc54698bce 100644 --- a/src/solvers/refinement/string_constraint_generator_indexof.cpp +++ b/src/solvers/refinement/string_constraint_generator_indexof.cpp @@ -252,7 +252,7 @@ exprt string_constraint_generatort::add_axioms_for_index_of( else { INVARIANT( - refined_string_typet::is_refined_string_type(c.type()), + is_refined_string_type(c.type()), string_refinement_invariantt("c can only be a (un)signedbv or a refined " "string and the (un)signedbv case is already handled")); string_exprt sub=get_string_expr(c); diff --git a/src/solvers/refinement/string_constraint_generator_main.cpp b/src/solvers/refinement/string_constraint_generator_main.cpp index c9a9f4e4943..07e974d2a7e 100644 --- a/src/solvers/refinement/string_constraint_generator_main.cpp +++ b/src/solvers/refinement/string_constraint_generator_main.cpp @@ -131,7 +131,7 @@ string_exprt string_constraint_generatort::fresh_string( /// \return a string expression string_exprt string_constraint_generatort::get_string_expr(const exprt &expr) { - PRECONDITION(refined_string_typet::is_refined_string_type(expr.type())); + PRECONDITION(is_refined_string_type(expr.type())); if(expr.id()==ID_symbol) { @@ -180,7 +180,7 @@ void string_constraint_generatort::add_default_axioms( string_exprt string_constraint_generatort::add_axioms_for_refined_string( const exprt &string) { - PRECONDITION(refined_string_typet::is_refined_string_type(string.type())); + PRECONDITION(is_refined_string_type(string.type())); refined_string_typet type=to_refined_string_type(string.type()); // Function applications should have been removed before @@ -246,11 +246,9 @@ string_exprt string_constraint_generatort::add_axioms_for_refined_string( string_exprt string_constraint_generatort::add_axioms_for_if( const if_exprt &expr) { - PRECONDITION( - refined_string_typet::is_refined_string_type(expr.true_case().type())); + PRECONDITION(is_refined_string_type(expr.true_case().type())); string_exprt t=get_string_expr(expr.true_case()); - PRECONDITION( - refined_string_typet::is_refined_string_type(expr.false_case().type())); + PRECONDITION(is_refined_string_type(expr.false_case().type())); string_exprt f=get_string_expr(expr.false_case()); const refined_string_typet &ref_type=to_refined_string_type(t.type()); const typet &index_type=ref_type.get_index_type(); diff --git a/src/solvers/refinement/string_refinement.cpp b/src/solvers/refinement/string_refinement.cpp index c6afe3af184..6b8966c7d6f 100644 --- a/src/solvers/refinement/string_refinement.cpp +++ b/src/solvers/refinement/string_refinement.cpp @@ -162,7 +162,7 @@ void string_refinementt::add_symbol_to_symbol_map( rhs.id()==ID_array_of || rhs.id()==ID_if || (rhs.id()==ID_struct && - refined_string_typet::is_refined_string_type(rhs.type()))); + is_refined_string_type(rhs.type()))); // We insert the mapped value of the rhs, if it exists. auto it=symbol_resolve.find(rhs); @@ -279,7 +279,7 @@ bool string_refinementt::add_axioms_for_string_assigns( return true; } } - if(refined_string_typet::is_refined_string_type(rhs.type())) + if(is_refined_string_type(rhs.type())) { exprt refined_rhs=generator.add_axioms_for_refined_string(rhs); add_symbol_to_symbol_map(lhs, refined_rhs); @@ -302,7 +302,7 @@ bool string_refinementt::add_axioms_for_string_assigns( /// last value that has been initialized. void string_refinementt::concretize_string(const exprt &expr) { - if(refined_string_typet::is_refined_string_type(expr.type())) + if(is_refined_string_type(expr.type())) { string_exprt str=to_string_expr(expr); exprt length=get(str.length()); @@ -392,7 +392,7 @@ void string_refinementt::concretize_lengths() { for(const auto &it : symbol_resolve) { - if(refined_string_typet::is_refined_string_type(it.second.type())) + if(is_refined_string_type(it.second.type())) { string_exprt str=to_string_expr(it.second); exprt length=get(str.length()); @@ -403,7 +403,7 @@ void string_refinementt::concretize_lengths() } for(const auto &it : generator.created_strings) { - if(refined_string_typet::is_refined_string_type(it.type())) + if(is_refined_string_type(it.type())) { string_exprt str=to_string_expr(it); exprt length=get(str.length()); @@ -429,12 +429,10 @@ void string_refinementt::set_to(const exprt &expr, bool value) // The assignment of a string equality to false is not supported. PRECONDITION(value || !is_char_array(rhs.type())); - PRECONDITION(value || - !refined_string_typet::is_refined_string_type(rhs.type())); + PRECONDITION(value || !is_refined_string_type(rhs.type())); PRECONDITION(lhs.id()==ID_symbol || !is_char_array(rhs.type())); - PRECONDITION(lhs.id()==ID_symbol || - !refined_string_typet::is_refined_string_type(rhs.type())); + PRECONDITION(lhs.id()==ID_symbol || !is_refined_string_type(rhs.type())); // If lhs is not a symbol, let supert::set_to() handle it. if(lhs.id()!=ID_symbol) @@ -811,7 +809,7 @@ void string_refinementt::debug_model() const std::string indent(" "); for(auto it : symbol_resolve) { - if(refined_string_typet::is_refined_string_type(it.second.type())) + if(is_refined_string_type(it.second.type())) { debug() << "- " << from_expr(ns, "", to_symbol_expr(it.first)) << ":\n"; string_exprt refined=to_string_expr(it.second); @@ -1684,8 +1682,7 @@ exprt string_refinementt::get(const exprt &expr) const if(it!=found_length.end()) return get_array(ecopy, it->second); } - else if(refined_string_typet::is_refined_string_type(ecopy.type()) && - ecopy.id()==ID_struct) + else if(is_refined_string_type(ecopy.type()) && ecopy.id()==ID_struct) { const string_exprt &string=to_string_expr(ecopy); const exprt &content=string.content(); diff --git a/src/util/refined_string_type.cpp b/src/util/refined_string_type.cpp index 29f73f88da6..91ac2e4661d 100644 --- a/src/util/refined_string_type.cpp +++ b/src/util/refined_string_type.cpp @@ -16,8 +16,6 @@ Author: Romain Brenguier, romain.brenguier@diffblue.com /// `content` of type `content_type`. This module also defines functions to /// recognise the C and java string types. -#include - #include "refined_string_type.h" refined_string_typet::refined_string_typet( @@ -29,13 +27,3 @@ refined_string_typet::refined_string_typet( components().emplace_back("content", char_array); set_tag(CPROVER_PREFIX"refined_string_type"); } - -/// \par parameters: a type -/// \return Boolean telling whether the input is a refined string type -bool refined_string_typet::is_refined_string_type(const typet &type) -{ - return - type.id()==ID_struct && - to_struct_type(type).get_tag()==CPROVER_PREFIX"refined_string_type"; -} - diff --git a/src/util/refined_string_type.h b/src/util/refined_string_type.h index efa8a0987ec..f20f0048151 100644 --- a/src/util/refined_string_type.h +++ b/src/util/refined_string_type.h @@ -22,6 +22,7 @@ Author: Romain Brenguier, romain.brenguier@diffblue.com #include #include #include +#include #include // Internal type used for string refinement @@ -33,7 +34,7 @@ class refined_string_typet: public struct_typet // Type for the content (list of characters) of a string const array_typet &get_content_type() const { - assert(components().size()==2); + PRECONDITION(components().size()==2); return to_array_type(components()[1].type()); } @@ -44,22 +45,22 @@ class refined_string_typet: public struct_typet const typet &get_index_type() const { - assert(components().size()==2); + PRECONDITION(components().size()==2); return components()[0].type(); } - - static bool is_refined_string_type(const typet &type); - - constant_exprt index_of_int(int i) const - { - return from_integer(i, get_index_type()); - } }; +inline bool is_refined_string_type(const typet &type) +{ + return + type.id()==ID_struct && + to_struct_type(type).get_tag()==CPROVER_PREFIX"refined_string_type"; +} + extern inline const refined_string_typet &to_refined_string_type( const typet &type) { - assert(refined_string_typet::is_refined_string_type(type)); + PRECONDITION(is_refined_string_type(type)); return static_cast(type); } From a86ed4adabddab7dadccb444728da61893217f0f Mon Sep 17 00:00:00 2001 From: Romain Brenguier Date: Mon, 21 Aug 2017 14:37:22 +0100 Subject: [PATCH 2/2] Renaming string length comparing functions MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit The previous name used (like `axioms_for_is_longer_than`) could be ambiguous and sometimes misleading. --- ...string_constraint_generator_comparison.cpp | 16 ++++------ .../string_constraint_generator_float.cpp | 4 +-- .../string_constraint_generator_main.cpp | 4 +-- .../string_constraint_generator_testing.cpp | 16 +++++----- ...ng_constraint_generator_transformation.cpp | 14 ++++---- .../string_constraint_generator_valueof.cpp | 13 ++++---- src/util/string_expr.h | 32 +++++++++---------- 7 files changed, 47 insertions(+), 52 deletions(-) diff --git a/src/solvers/refinement/string_constraint_generator_comparison.cpp b/src/solvers/refinement/string_constraint_generator_comparison.cpp index c5021b107e3..aa14d4192e8 100644 --- a/src/solvers/refinement/string_constraint_generator_comparison.cpp +++ b/src/solvers/refinement/string_constraint_generator_comparison.cpp @@ -175,7 +175,7 @@ exprt string_constraint_generatort::add_axioms_for_hash_code( and_exprt( not_exprt(equal_exprt(str[i], it.first[i])), and_exprt( - str.axiom_for_is_strictly_longer_than(i), + str.axiom_for_length_gt(i), axiom_for_is_positive_index(i)))); axioms.push_back(or_exprt(c1, or_exprt(c2, c3))); } @@ -229,16 +229,12 @@ exprt string_constraint_generatort::add_axioms_for_compare_to( typecast_exprt(s1.length(), return_type), typecast_exprt(s2.length(), return_type))); or_exprt guard1( - and_exprt(s1.axiom_for_is_shorter_than(s2), - s1.axiom_for_is_strictly_longer_than(x)), - and_exprt(s1.axiom_for_is_longer_than(s2), - s2.axiom_for_is_strictly_longer_than(x))); + and_exprt(s1.axiom_for_length_le(s2), s1.axiom_for_length_gt(x)), + and_exprt(s1.axiom_for_length_ge(s2), s2.axiom_for_length_gt(x))); and_exprt cond1(ret_char_diff, guard1); or_exprt guard2( - and_exprt(s2.axiom_for_is_strictly_longer_than(s1), - s1.axiom_for_has_length(x)), - and_exprt(s1.axiom_for_is_strictly_longer_than(s2), - s2.axiom_for_has_length(x))); + and_exprt(s2.axiom_for_length_gt(s1), s1.axiom_for_has_length(x)), + and_exprt(s1.axiom_for_length_gt(s2), s2.axiom_for_has_length(x))); and_exprt cond2(ret_length_diff, guard2); implies_exprt a3( @@ -300,7 +296,7 @@ symbol_exprt string_constraint_generatort::add_axioms_for_intern( str.axiom_for_has_same_length_as(it.first), and_exprt( not_exprt(equal_exprt(str[i], it.first[i])), - and_exprt(str.axiom_for_is_strictly_longer_than(i), + and_exprt(str.axiom_for_length_gt(i), axiom_for_is_positive_index(i))))))); } diff --git a/src/solvers/refinement/string_constraint_generator_float.cpp b/src/solvers/refinement/string_constraint_generator_float.cpp index 826a9d5b38b..d164ad54264 100644 --- a/src/solvers/refinement/string_constraint_generator_float.cpp +++ b/src/solvers/refinement/string_constraint_generator_float.cpp @@ -235,8 +235,8 @@ string_exprt string_constraint_generatort::add_axioms_for_fractional_part( // no_trailing_zero: forall j:[2, max_size[. !(|res| = j+1 && res[j] = '0') // a3 : int_expr = sum_j 10^j (j < |res| ? res[j] - '0' : 0) - and_exprt a1(res.axiom_for_is_strictly_longer_than(1), - res.axiom_for_is_shorter_than(max)); + and_exprt a1(res.axiom_for_length_gt(1), + res.axiom_for_length_le(max)); axioms.push_back(a1); equal_exprt starts_with_dot(res[0], from_integer('.', char_type)); diff --git a/src/solvers/refinement/string_constraint_generator_main.cpp b/src/solvers/refinement/string_constraint_generator_main.cpp index 07e974d2a7e..71de1f136a2 100644 --- a/src/solvers/refinement/string_constraint_generator_main.cpp +++ b/src/solvers/refinement/string_constraint_generator_main.cpp @@ -156,9 +156,9 @@ void string_constraint_generatort::add_default_axioms( const string_exprt &s) { axioms.push_back( - s.axiom_for_is_longer_than(from_integer(0, s.length().type()))); + s.axiom_for_length_ge(from_integer(0, s.length().type()))); if(max_string_length!=std::numeric_limits::max()) - axioms.push_back(s.axiom_for_is_shorter_than(max_string_length)); + axioms.push_back(s.axiom_for_length_le(max_string_length)); if(force_printable_characters) { diff --git a/src/solvers/refinement/string_constraint_generator_testing.cpp b/src/solvers/refinement/string_constraint_generator_testing.cpp index afb758afbb4..69ee6e40cbc 100644 --- a/src/solvers/refinement/string_constraint_generator_testing.cpp +++ b/src/solvers/refinement/string_constraint_generator_testing.cpp @@ -32,7 +32,7 @@ exprt string_constraint_generatort::add_axioms_for_is_prefix( implies_exprt a1( isprefix, - str.axiom_for_is_longer_than(plus_exprt_with_overflow_check( + str.axiom_for_length_ge(plus_exprt_with_overflow_check( prefix.length(), offset))); axioms.push_back(a1); @@ -49,12 +49,12 @@ exprt string_constraint_generatort::add_axioms_for_is_prefix( and_exprt witness_diff( axiom_for_is_positive_index(witness), and_exprt( - prefix.axiom_for_is_strictly_longer_than(witness), + prefix.axiom_for_length_gt(witness), notequal_exprt(str[plus_exprt_with_overflow_check(witness, offset)], prefix[witness]))); or_exprt s0_notpref_s1( not_exprt( - str.axiom_for_is_longer_than( + str.axiom_for_length_ge( plus_exprt_with_overflow_check(prefix.length(), offset))), witness_diff); @@ -132,7 +132,7 @@ exprt string_constraint_generatort::add_axioms_for_is_suffix( // || (s1.length > witness>=0 // &&s1[witness]!=s0[witness + s0.length-s1.length] - implies_exprt a1(issuffix, s1.axiom_for_is_longer_than(s0)); + implies_exprt a1(issuffix, s1.axiom_for_length_ge(s0)); axioms.push_back(a1); symbol_exprt qvar=fresh_univ_index("QA_suffix", index_type); @@ -146,12 +146,12 @@ exprt string_constraint_generatort::add_axioms_for_is_suffix( exprt shifted=plus_exprt( witness, minus_exprt(s1.length(), s0.length())); or_exprt constr3( - and_exprt(s0.axiom_for_is_strictly_longer_than(s1), + and_exprt(s0.axiom_for_length_gt(s1), equal_exprt(witness, from_integer(-1, index_type))), and_exprt( notequal_exprt(s0[witness], s1[shifted]), and_exprt( - s0.axiom_for_is_strictly_longer_than(witness), + s0.axiom_for_length_gt(witness), axiom_for_is_positive_index(witness)))); implies_exprt a3(not_exprt(issuffix), constr3); @@ -201,7 +201,7 @@ exprt string_constraint_generatort::add_axioms_for_contains( // (forall startpos <= |s0| - |s1|. // exists witness < |s1|. s1[witness] != s0[witness + startpos]) - implies_exprt a1(contains, s0.axiom_for_is_longer_than(s1)); + implies_exprt a1(contains, s0.axiom_for_length_ge(s1)); axioms.push_back(a1); symbol_exprt startpos=fresh_exist_index("startpos_contains", index_type); @@ -229,7 +229,7 @@ exprt string_constraint_generatort::add_axioms_for_contains( string_not_contains_constraintt a5( from_integer(0, index_type), plus_exprt(from_integer(1, index_type), length_diff), - and_exprt(not_exprt(contains), s0.axiom_for_is_longer_than(s1)), + and_exprt(not_exprt(contains), s0.axiom_for_length_ge(s1)), from_integer(0, index_type), s1.length(), s0, diff --git a/src/solvers/refinement/string_constraint_generator_transformation.cpp b/src/solvers/refinement/string_constraint_generator_transformation.cpp index f835ec5b646..b2566bab396 100644 --- a/src/solvers/refinement/string_constraint_generator_transformation.cpp +++ b/src/solvers/refinement/string_constraint_generator_transformation.cpp @@ -42,7 +42,7 @@ string_exprt string_constraint_generatort::add_axioms_for_set_length( string_constraintt a2( idx, res.length(), - s1.axiom_for_is_strictly_longer_than(idx), + s1.axiom_for_length_gt(idx), equal_exprt(s1[idx], res[idx])); axioms.push_back(a2); @@ -51,7 +51,7 @@ string_exprt string_constraint_generatort::add_axioms_for_set_length( string_constraintt a3( idx2, res.length(), - s1.axiom_for_is_shorter_than(idx2), + s1.axiom_for_length_le(idx2), equal_exprt(res[idx2], constant_char(0, ref_type.get_char_type()))); axioms.push_back(a3); @@ -120,7 +120,7 @@ string_exprt string_constraint_generatort::add_axioms_for_substring( axioms.push_back(a2); // Warning: check what to do if the string is not long enough - axioms.push_back(str.axiom_for_is_longer_than(end)); + axioms.push_back(str.axiom_for_length_ge(end)); symbol_exprt idx=fresh_univ_index("QA_index_substring", index_type); string_constraintt a4(idx, @@ -156,21 +156,21 @@ string_exprt string_constraint_generatort::add_axioms_for_trim( // a8 : forall n<|s1|, s[idx+n]=s1[n] // a9 : (s[m]>' ' &&s[m+|s1|-1]>' ') || m=|s| - exprt a1=str.axiom_for_is_longer_than( + exprt a1=str.axiom_for_length_ge( plus_exprt_with_overflow_check(idx, res.length())); axioms.push_back(a1); binary_relation_exprt a2(idx, ID_ge, from_integer(0, index_type)); axioms.push_back(a2); - exprt a3=str.axiom_for_is_longer_than(idx); + exprt a3=str.axiom_for_length_ge(idx); axioms.push_back(a3); - exprt a4=res.axiom_for_is_longer_than( + exprt a4=res.axiom_for_length_ge( from_integer(0, index_type)); axioms.push_back(a4); - exprt a5=res.axiom_for_is_shorter_than(str); + exprt a5=res.axiom_for_length_le(str); axioms.push_back(a5); symbol_exprt n=fresh_univ_index("QA_index_trim", index_type); diff --git a/src/solvers/refinement/string_constraint_generator_valueof.cpp b/src/solvers/refinement/string_constraint_generator_valueof.cpp index 91e2d09ec18..1c215db583b 100644 --- a/src/solvers/refinement/string_constraint_generator_valueof.cpp +++ b/src/solvers/refinement/string_constraint_generator_valueof.cpp @@ -222,8 +222,8 @@ string_exprt string_constraint_generatort::add_axioms_from_int_hex( size_t max_size=8; axioms.push_back( - and_exprt(res.axiom_for_is_strictly_longer_than(0), - res.axiom_for_is_shorter_than(max_size))); + and_exprt(res.axiom_for_length_gt(0), + res.axiom_for_length_le(max_size))); for(size_t size=1; size<=max_size; size++) { @@ -322,8 +322,7 @@ void string_constraint_generatort::add_axioms_for_correct_number_format( is_digit_with_radix(chr, strict_formatting, radix_as_char, radix_ul); // |str| > 0 - const exprt non_empty= - str.axiom_for_is_longer_than(from_integer(1, index_type)); + const exprt non_empty=str.axiom_for_length_ge(from_integer(1, index_type)); axioms.push_back(non_empty); if(strict_formatting) @@ -343,11 +342,11 @@ void string_constraint_generatort::add_axioms_for_correct_number_format( // str[0]='+' or '-' ==> |str| > 1 const implies_exprt contains_digit( or_exprt(starts_with_minus, starts_with_plus), - str.axiom_for_is_longer_than(from_integer(2, index_type))); + str.axiom_for_length_ge(from_integer(2, index_type))); axioms.push_back(contains_digit); // |str| <= max_size - axioms.push_back(str.axiom_for_is_shorter_than(max_size)); + axioms.push_back(str.axiom_for_length_le(max_size)); // forall 1 <= i < |str| . is_digit_with_radix(str[i], radix) // We unfold the above because we know that it will be used for all i up to @@ -356,7 +355,7 @@ void string_constraint_generatort::add_axioms_for_correct_number_format( { /// index < length => is_digit_with_radix(str[index], radix) const implies_exprt character_at_index_is_digit( - str.axiom_for_is_longer_than(from_integer(index+1, index_type)), + str.axiom_for_length_ge(from_integer(index+1, index_type)), is_digit_with_radix( str[index], strict_formatting, radix_as_char, radix_ul)); axioms.push_back(character_at_index_is_digit); diff --git a/src/util/string_expr.h b/src/util/string_expr.h index cdb801988ae..693df01d87f 100644 --- a/src/util/string_expr.h +++ b/src/util/string_expr.h @@ -53,59 +53,59 @@ class string_exprt: public struct_exprt } // Comparison on the length of the strings - binary_relation_exprt axiom_for_is_longer_than( + binary_relation_exprt axiom_for_length_ge( const string_exprt &rhs) const { return binary_relation_exprt(length(), ID_ge, rhs.length()); } - binary_relation_exprt axiom_for_is_longer_than( + binary_relation_exprt axiom_for_length_ge( const exprt &rhs) const { return binary_relation_exprt(length(), ID_ge, rhs); } - binary_relation_exprt axiom_for_is_strictly_longer_than( + binary_relation_exprt axiom_for_length_gt( const exprt &rhs) const { return binary_relation_exprt(rhs, ID_lt, length()); } - binary_relation_exprt axiom_for_is_strictly_longer_than( + binary_relation_exprt axiom_for_length_gt( const string_exprt &rhs) const { return binary_relation_exprt(rhs.length(), ID_lt, length()); } - binary_relation_exprt axiom_for_is_strictly_longer_than(mp_integer i) const + binary_relation_exprt axiom_for_length_gt(mp_integer i) const { - return axiom_for_is_strictly_longer_than(from_integer(i, length().type())); + return axiom_for_length_gt(from_integer(i, length().type())); } - binary_relation_exprt axiom_for_is_shorter_than( + binary_relation_exprt axiom_for_length_le( const string_exprt &rhs) const { return binary_relation_exprt(length(), ID_le, rhs.length()); } - binary_relation_exprt axiom_for_is_shorter_than( + binary_relation_exprt axiom_for_length_le( const exprt &rhs) const { return binary_relation_exprt(length(), ID_le, rhs); } - binary_relation_exprt axiom_for_is_shorter_than(mp_integer i) const + binary_relation_exprt axiom_for_length_le(mp_integer i) const { - return axiom_for_is_shorter_than(from_integer(i, length().type())); + return axiom_for_length_le(from_integer(i, length().type())); } - binary_relation_exprt axiom_for_is_strictly_shorter_than( + binary_relation_exprt axiom_for_length_lt( const string_exprt &rhs) const { return binary_relation_exprt(length(), ID_lt, rhs.length()); } - binary_relation_exprt axiom_for_is_strictly_shorter_than( + binary_relation_exprt axiom_for_length_lt( const exprt &rhs) const { return binary_relation_exprt(length(), ID_lt, rhs); @@ -132,15 +132,15 @@ class string_exprt: public struct_exprt inline string_exprt &to_string_expr(exprt &expr) { - assert(expr.id()==ID_struct); - assert(expr.operands().size()==2); + PRECONDITION(expr.id()==ID_struct); + PRECONDITION(expr.operands().size()==2); return static_cast(expr); } inline const string_exprt &to_string_expr(const exprt &expr) { - assert(expr.id()==ID_struct); - assert(expr.operands().size()==2); + PRECONDITION(expr.id()==ID_struct); + PRECONDITION(expr.operands().size()==2); return static_cast(expr); }