cprover
|
#include <string_expr.h>
Public Member Functions | |
exprt | operator[] (const exprt &i) const |
index_exprt | operator[] (int i) const |
binary_relation_exprt | axiom_for_length_ge (const string_exprt &rhs) const |
binary_relation_exprt | axiom_for_length_ge (const exprt &rhs) const |
binary_relation_exprt | axiom_for_length_gt (const exprt &rhs) const |
binary_relation_exprt | axiom_for_length_gt (const string_exprt &rhs) const |
binary_relation_exprt | axiom_for_length_gt (mp_integer i) const |
binary_relation_exprt | axiom_for_length_le (const string_exprt &rhs) const |
binary_relation_exprt | axiom_for_length_le (const exprt &rhs) const |
binary_relation_exprt | axiom_for_length_le (mp_integer i) const |
binary_relation_exprt | axiom_for_length_lt (const string_exprt &rhs) const |
binary_relation_exprt | axiom_for_length_lt (const exprt &rhs) const |
equal_exprt | axiom_for_has_same_length_as (const string_exprt &rhs) const |
equal_exprt | axiom_for_has_length (const exprt &rhs) const |
equal_exprt | axiom_for_has_length (mp_integer i) const |
Protected Member Functions | |
string_exprt ()=default | |
Private Member Functions | |
exprt & | length () |
const exprt & | length () const |
exprt & | content () |
const exprt & | content () const |
Definition at line 22 of file string_expr.h.
|
protecteddefault |
|
inline |
Definition at line 125 of file string_expr.h.
Referenced by string_constraint_generatort::add_axioms_for_characters_in_integer_string(), string_constraint_generatort::add_axioms_for_code_point(), string_constraint_generatort::add_axioms_for_correct_number_format(), string_constraint_generatort::add_axioms_for_is_empty(), string_constraint_generatort::add_axioms_from_char(), and string_exprt< array_string_exprt >::axiom_for_has_length().
|
inline |
Definition at line 131 of file string_expr.h.
|
inline |
Definition at line 119 of file string_expr.h.
|
inline |
Definition at line 57 of file string_expr.h.
Referenced by string_constraint_generatort::add_axioms_for_correct_number_format(), and string_constraint_generatort::add_axioms_for_is_prefix().
|
inline |
Definition at line 63 of file string_expr.h.
|
inline |
Definition at line 70 of file string_expr.h.
Referenced by string_constraint_generatort::add_axioms_for_fractional_part(), string_constraint_generatort::add_axioms_for_is_prefix(), and string_exprt< array_string_exprt >::axiom_for_length_gt().
|
inline |
Definition at line 77 of file string_expr.h.
|
inline |
Definition at line 83 of file string_expr.h.
|
inline |
Definition at line 88 of file string_expr.h.
Referenced by string_constraint_generatort::add_axioms_for_correct_number_format(), string_constraint_generatort::add_axioms_for_fractional_part(), and string_exprt< array_string_exprt >::axiom_for_length_le().
|
inline |
Definition at line 94 of file string_expr.h.
|
inline |
Definition at line 101 of file string_expr.h.
|
inline |
Definition at line 106 of file string_expr.h.
|
inline |
Definition at line 112 of file string_expr.h.
|
inlineprivate |
Definition at line 33 of file string_expr.h.
Referenced by string_exprt< array_string_exprt >::content(), and string_exprt< array_string_exprt >::operator[]().
|
inlineprivate |
Definition at line 37 of file string_expr.h.
|
inlineprivate |
Definition at line 25 of file string_expr.h.
Referenced by string_exprt< array_string_exprt >::axiom_for_has_length(), string_exprt< array_string_exprt >::axiom_for_has_same_length_as(), string_exprt< array_string_exprt >::axiom_for_length_ge(), string_exprt< array_string_exprt >::axiom_for_length_gt(), string_exprt< array_string_exprt >::axiom_for_length_le(), string_exprt< array_string_exprt >::axiom_for_length_lt(), string_exprt< array_string_exprt >::length(), and string_exprt< array_string_exprt >::operator[]().
|
inlineprivate |
Definition at line 29 of file string_expr.h.
|
inline |
Definition at line 46 of file string_expr.h.
|
inline |
Definition at line 51 of file string_expr.h.