cprover
string_expr.h File Reference

String expressions for the string solver. More...

#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  string_exprt< child_t >
 
class  array_string_exprt
 
class  refined_string_exprt
 

Functions

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 245 of file string_expr.h.

◆ to_array_string_expr() [1/2]

◆ to_array_string_expr() [2/2]

const array_string_exprt& to_array_string_expr ( const exprt expr)
inline

Definition at line 168 of file string_expr.h.

References irept::id(), PRECONDITION, and exprt::type().

◆ to_string_expr() [1/2]

◆ to_string_expr() [2/2]

const refined_string_exprt& to_string_expr ( const exprt expr)
inline

Definition at line 237 of file string_expr.h.

References irept::id(), exprt::operands(), and PRECONDITION.

◆ validate_expr()

void validate_expr ( const refined_string_exprt x)
inline