cprover
|
Go to the source code of this file.
Classes | |
class | array_string_exprt |
class | refined_string_exprt |
Functions | |
template<typename T > | |
binary_relation_exprt | length_ge (const T &lhs, const exprt &rhs) |
template<typename T > | |
binary_relation_exprt | length_gt (const T &lhs, const exprt &rhs) |
template<typename T > | |
binary_relation_exprt | length_gt (const T &lhs, mp_integer i) |
template<typename T > | |
binary_relation_exprt | length_le (const T &lhs, const exprt &rhs) |
template<typename T > | |
binary_relation_exprt | length_le (const T &lhs, mp_integer i) |
template<typename T > | |
equal_exprt | length_eq (const T &lhs, const exprt &rhs) |
template<typename T > | |
equal_exprt | length_eq (const T &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) |
String expressions for the string solver
Definition in file string_expr.h.
|
inline |
Definition at line 176 of file string_expr.h.
equal_exprt length_eq | ( | const T & | lhs, |
const exprt & | rhs | ||
) |
Definition at line 54 of file string_expr.h.
equal_exprt length_eq | ( | const T & | lhs, |
mp_integer | i | ||
) |
Definition at line 61 of file string_expr.h.
binary_relation_exprt length_ge | ( | const T & | lhs, |
const exprt & | rhs | ||
) |
Definition at line 21 of file string_expr.h.
binary_relation_exprt length_gt | ( | const T & | lhs, |
const exprt & | rhs | ||
) |
Definition at line 28 of file string_expr.h.
binary_relation_exprt length_gt | ( | const T & | lhs, |
mp_integer | i | ||
) |
Definition at line 35 of file string_expr.h.
binary_relation_exprt length_le | ( | const T & | lhs, |
const exprt & | rhs | ||
) |
Definition at line 41 of file string_expr.h.
binary_relation_exprt length_le | ( | const T & | lhs, |
mp_integer | i | ||
) |
Definition at line 48 of file string_expr.h.
|
inline |
Definition at line 107 of file string_expr.h.
|
inline |
Definition at line 101 of file string_expr.h.
|
inline |
Definition at line 168 of file string_expr.h.
|
inline |
Definition at line 161 of file string_expr.h.
|
inline |
Definition at line 181 of file string_expr.h.