String expressions for the string solver. More...
#include "arith_tools.h"#include "pointer_expr.h"#include "refined_string_type.h"#include "std_expr.h"
Include dependency graph for string_expr.h: This graph shows which files directly or indirectly include this file:Go to the source code of this file.
Classes | |
| class | array_string_exprt |
| class | refined_string_exprt |
Functions | |
| binary_relation_exprt | greater_or_equal_to (exprt lhs, exprt rhs) |
| binary_relation_exprt | greater_than (exprt lhs, exprt rhs) |
| binary_relation_exprt | greater_than (const exprt &lhs, mp_integer i) |
| binary_relation_exprt | less_than_or_equal_to (exprt lhs, exprt rhs) |
| binary_relation_exprt | less_than_or_equal_to (const exprt &lhs, mp_integer i) |
| binary_relation_exprt | less_than (exprt lhs, exprt rhs) |
| equal_exprt | equal_to (exprt lhs, exprt rhs) |
| equal_exprt | equal_to (const exprt &lhs, mp_integer i) |
| array_string_exprt & | to_array_string_expr (exprt &expr) |
| const array_string_exprt & | to_array_string_expr (const exprt &expr) |
| refined_string_exprt & | to_string_expr (exprt &expr) |
| const refined_string_exprt & | to_string_expr (const exprt &expr) |
| template<> | |
| bool | can_cast_expr< refined_string_exprt > (const exprt &base) |
| void | validate_expr (const refined_string_exprt &x) |
Detailed Description
String expressions for the string solver.
Definition in file string_expr.h.
Function Documentation
◆ can_cast_expr< refined_string_exprt >()
|
inline |
Definition at line 166 of file string_expr.h.
◆ equal_to() [1/2]
|
inline |
Definition at line 61 of file string_expr.h.
◆ equal_to() [2/2]
|
inline |
Definition at line 55 of file string_expr.h.
◆ greater_or_equal_to()
|
inline |
Definition at line 20 of file string_expr.h.
◆ greater_than() [1/2]
|
inline |
Definition at line 32 of file string_expr.h.
◆ greater_than() [2/2]
|
inline |
Definition at line 26 of file string_expr.h.
◆ less_than()
|
inline |
Definition at line 49 of file string_expr.h.
◆ less_than_or_equal_to() [1/2]
|
inline |
Definition at line 44 of file string_expr.h.
◆ less_than_or_equal_to() [2/2]
|
inline |
Definition at line 37 of file string_expr.h.
◆ to_array_string_expr() [1/2]
|
inline |
Definition at line 102 of file string_expr.h.
◆ to_array_string_expr() [2/2]
|
inline |
Definition at line 96 of file string_expr.h.
◆ to_string_expr() [1/2]
|
inline |
Definition at line 158 of file string_expr.h.
◆ to_string_expr() [2/2]
|
inline |
Definition at line 151 of file string_expr.h.
◆ validate_expr()
|
inline |
Definition at line 172 of file string_expr.h.
