Loading...

Searching...

No Matches

Classes | Functions

string_expr.h File Reference

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 >()

template<>

bool can_cast_expr< refined_string_exprt > ( const exprt & base )

inline

Definition at line 166 of file string_expr.h.

◆ equal_to() [1/2]

equal_exprt equal_to ( const exprt & lhs,

mp_integer i

)

inline

Definition at line 61 of file string_expr.h.

◆ equal_to() [2/2]

equal_exprt equal_to ( exprt lhs,

exprt rhs

)

inline

Definition at line 55 of file string_expr.h.

◆ greater_or_equal_to()

binary_relation_exprt greater_or_equal_to ( exprt lhs,

exprt rhs

)

inline

Definition at line 20 of file string_expr.h.

◆ greater_than() [1/2]

binary_relation_exprt greater_than ( const exprt & lhs,

mp_integer i

)

inline

Definition at line 32 of file string_expr.h.

◆ greater_than() [2/2]

binary_relation_exprt greater_than ( exprt lhs,

exprt rhs

)

inline

Definition at line 26 of file string_expr.h.

◆ less_than()

binary_relation_exprt less_than ( exprt lhs,

exprt rhs

)

inline

Definition at line 49 of file string_expr.h.

◆ less_than_or_equal_to() [1/2]

binary_relation_exprt less_than_or_equal_to ( const exprt & lhs,

mp_integer i

)

inline

Definition at line 44 of file string_expr.h.

◆ less_than_or_equal_to() [2/2]

binary_relation_exprt less_than_or_equal_to ( exprt lhs,

exprt rhs

)

inline

Definition at line 37 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 102 of file string_expr.h.

◆ to_array_string_expr() [2/2]

array_string_exprt & to_array_string_expr ( exprt & expr )

inline

Definition at line 96 of file string_expr.h.

◆ to_string_expr() [1/2]

const refined_string_exprt & to_string_expr ( const exprt & expr )

inline

Definition at line 158 of file string_expr.h.

◆ to_string_expr() [2/2]

refined_string_exprt & to_string_expr ( exprt & expr )

inline

Definition at line 151 of file string_expr.h.

◆ validate_expr()

void validate_expr ( const refined_string_exprt & x )

inline

Definition at line 172 of file string_expr.h.