cprover
string_expr.h File Reference
#include "arith_tools.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

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_exprtto_array_string_expr (exprt &expr)
 
const array_string_exprtto_array_string_expr (const exprt &expr)
 
refined_string_exprtto_string_expr (exprt &expr)
 
const refined_string_exprtto_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 >()

template<>
bool can_cast_expr< refined_string_exprt > ( const exprt base)
inline

Definition at line 176 of file string_expr.h.

◆ length_eq() [1/2]

template<typename T >
equal_exprt length_eq ( const T &  lhs,
const exprt rhs 
)

Definition at line 54 of file string_expr.h.

◆ length_eq() [2/2]

template<typename T >
equal_exprt length_eq ( const T &  lhs,
mp_integer  i 
)

Definition at line 61 of file string_expr.h.

◆ length_ge()

template<typename T >
binary_relation_exprt length_ge ( const T &  lhs,
const exprt rhs 
)

Definition at line 21 of file string_expr.h.

◆ length_gt() [1/2]

template<typename T >
binary_relation_exprt length_gt ( const T &  lhs,
const exprt rhs 
)

Definition at line 28 of file string_expr.h.

◆ length_gt() [2/2]

template<typename T >
binary_relation_exprt length_gt ( const T &  lhs,
mp_integer  i 
)

Definition at line 35 of file string_expr.h.

◆ length_le() [1/2]

template<typename T >
binary_relation_exprt length_le ( const T &  lhs,
const exprt rhs 
)

Definition at line 41 of file string_expr.h.

◆ length_le() [2/2]

template<typename T >
binary_relation_exprt length_le ( const T &  lhs,
mp_integer  i 
)

Definition at line 48 of file string_expr.h.

◆ to_array_string_expr() [1/2]

const array_string_exprt& to_array_string_expr ( const exprt expr)
inline

Definition at line 107 of file string_expr.h.

◆ to_array_string_expr() [2/2]

array_string_exprt& to_array_string_expr ( exprt expr)
inline

Definition at line 101 of file string_expr.h.

◆ to_string_expr() [1/2]

const refined_string_exprt& to_string_expr ( const exprt expr)
inline

Definition at line 168 of file string_expr.h.

◆ to_string_expr() [2/2]

refined_string_exprt& to_string_expr ( exprt expr)
inline

Definition at line 161 of file string_expr.h.

◆ validate_expr()

void validate_expr ( const refined_string_exprt x)
inline

Definition at line 181 of file string_expr.h.