cprover
string_exprt< child_t > Class Template Reference

#include <string_expr.h>

Inheritance diagram for string_exprt< child_t >:
[legend]

Public Member Functions

exprt operator[] (const exprt &i) const
 
index_exprt operator[] (int i) const
 
binary_relation_exprt axiom_for_length_ge (const string_exprt &rhs) const
 
binary_relation_exprt axiom_for_length_ge (const exprt &rhs) const
 
binary_relation_exprt axiom_for_length_gt (const exprt &rhs) const
 
binary_relation_exprt axiom_for_length_gt (const string_exprt &rhs) const
 
binary_relation_exprt axiom_for_length_gt (mp_integer i) const
 
binary_relation_exprt axiom_for_length_le (const string_exprt &rhs) const
 
binary_relation_exprt axiom_for_length_le (const exprt &rhs) const
 
binary_relation_exprt axiom_for_length_le (mp_integer i) const
 
binary_relation_exprt axiom_for_length_lt (const string_exprt &rhs) const
 
binary_relation_exprt axiom_for_length_lt (const exprt &rhs) const
 
equal_exprt axiom_for_has_same_length_as (const string_exprt &rhs) const
 
equal_exprt axiom_for_has_length (const exprt &rhs) const
 
equal_exprt axiom_for_has_length (mp_integer i) const
 

Protected Member Functions

 string_exprt ()=default
 

Private Member Functions

exprtlength ()
 
const exprtlength () const
 
exprtcontent ()
 
const exprtcontent () const
 

Detailed Description

template<typename child_t>
class string_exprt< child_t >

Definition at line 22 of file string_expr.h.

Constructor & Destructor Documentation

◆ string_exprt()

template<typename child_t>
string_exprt< child_t >::string_exprt ( )
protecteddefault

Member Function Documentation

◆ axiom_for_has_length() [1/2]

◆ axiom_for_has_length() [2/2]

template<typename child_t>
equal_exprt string_exprt< child_t >::axiom_for_has_length ( mp_integer  i) const
inline

Definition at line 131 of file string_expr.h.

◆ axiom_for_has_same_length_as()

template<typename child_t>
equal_exprt string_exprt< child_t >::axiom_for_has_same_length_as ( const string_exprt< child_t > &  rhs) const
inline

Definition at line 119 of file string_expr.h.

◆ axiom_for_length_ge() [1/2]

template<typename child_t>
binary_relation_exprt string_exprt< child_t >::axiom_for_length_ge ( const string_exprt< child_t > &  rhs) const
inline

◆ axiom_for_length_ge() [2/2]

template<typename child_t>
binary_relation_exprt string_exprt< child_t >::axiom_for_length_ge ( const exprt rhs) const
inline

Definition at line 63 of file string_expr.h.

◆ axiom_for_length_gt() [1/3]

◆ axiom_for_length_gt() [2/3]

template<typename child_t>
binary_relation_exprt string_exprt< child_t >::axiom_for_length_gt ( const string_exprt< child_t > &  rhs) const
inline

Definition at line 77 of file string_expr.h.

◆ axiom_for_length_gt() [3/3]

template<typename child_t>
binary_relation_exprt string_exprt< child_t >::axiom_for_length_gt ( mp_integer  i) const
inline

Definition at line 83 of file string_expr.h.

◆ axiom_for_length_le() [1/3]

◆ axiom_for_length_le() [2/3]

template<typename child_t>
binary_relation_exprt string_exprt< child_t >::axiom_for_length_le ( const exprt rhs) const
inline

Definition at line 94 of file string_expr.h.

◆ axiom_for_length_le() [3/3]

template<typename child_t>
binary_relation_exprt string_exprt< child_t >::axiom_for_length_le ( mp_integer  i) const
inline

Definition at line 101 of file string_expr.h.

◆ axiom_for_length_lt() [1/2]

template<typename child_t>
binary_relation_exprt string_exprt< child_t >::axiom_for_length_lt ( const string_exprt< child_t > &  rhs) const
inline

Definition at line 106 of file string_expr.h.

◆ axiom_for_length_lt() [2/2]

template<typename child_t>
binary_relation_exprt string_exprt< child_t >::axiom_for_length_lt ( const exprt rhs) const
inline

Definition at line 112 of file string_expr.h.

◆ content() [1/2]

template<typename child_t>
exprt& string_exprt< child_t >::content ( )
inlineprivate

◆ content() [2/2]

template<typename child_t>
const exprt& string_exprt< child_t >::content ( ) const
inlineprivate

Definition at line 37 of file string_expr.h.

◆ length() [1/2]

◆ length() [2/2]

template<typename child_t>
const exprt& string_exprt< child_t >::length ( ) const
inlineprivate

Definition at line 29 of file string_expr.h.

◆ operator[]() [1/2]

template<typename child_t>
exprt string_exprt< child_t >::operator[] ( const exprt i) const
inline

Definition at line 46 of file string_expr.h.

◆ operator[]() [2/2]

template<typename child_t>
index_exprt string_exprt< child_t >::operator[] ( int  i) const
inline

Definition at line 51 of file string_expr.h.


The documentation for this class was generated from the following file: