cprover
string_expr.h
Go to the documentation of this file.
1 /******************************************************************\
2 
3 Module: String expressions for the string solver
4 
5 Author: Romain Brenguier, romain.brenguier@diffblue.com
6 
7 \*******************************************************************/
8 
11 
12 #ifndef CPROVER_UTIL_STRING_EXPR_H
13 #define CPROVER_UTIL_STRING_EXPR_H
14 
15 #include <util/std_expr.h>
16 #include <util/arith_tools.h>
17 
19 {
20 public:
22 
24  {
25  operands().resize(2);
26  }
27 
28  string_exprt(const exprt &_length, const exprt &_content, typet type):
29  struct_exprt(type)
30  {
31  copy_to_operands(_length, _content);
32  }
33 
34  // Expression corresponding to the length of the string
35  const exprt &length() const { return op0(); }
36  exprt &length() { return op0(); }
37 
38  // Expression corresponding to the content (array of characters) of the string
39  const exprt &content() const { return op1(); }
40  exprt &content() { return op1(); }
41 
42  static exprt within_bounds(const exprt &idx, const exprt &bound);
43 
44  // Expression of the character at position idx in the string
45  index_exprt operator[] (const exprt &idx) const
46  {
47  return index_exprt(content(), idx);
48  }
49 
50  index_exprt operator[] (int i) const
51  {
52  return index_exprt(content(), from_integer(i, length().type()));
53  }
54 
55  // Comparison on the length of the strings
57  const string_exprt &rhs) const
58  {
59  return binary_relation_exprt(length(), ID_ge, rhs.length());
60  }
61 
63  const exprt &rhs) const
64  {
65  return binary_relation_exprt(length(), ID_ge, rhs);
66  }
67 
69  const exprt &rhs) const
70  {
71  return binary_relation_exprt(rhs, ID_lt, length());
72  }
73 
75  const string_exprt &rhs) const
76  {
77  return binary_relation_exprt(rhs.length(), ID_lt, length());
78  }
79 
81  {
83  }
84 
86  const string_exprt &rhs) const
87  {
88  return binary_relation_exprt(length(), ID_le, rhs.length());
89  }
90 
92  const exprt &rhs) const
93  {
94  return binary_relation_exprt(length(), ID_le, rhs);
95  }
96 
98  {
100  }
101 
103  const string_exprt &rhs) const
104  {
105  return binary_relation_exprt(length(), ID_lt, rhs.length());
106  }
107 
109  const exprt &rhs) const
110  {
111  return binary_relation_exprt(length(), ID_lt, rhs);
112  }
113 
115  const string_exprt &rhs) const
116  {
117  return equal_exprt(length(), rhs.length());
118  }
119 
121  {
122  return equal_exprt(length(), rhs);
123  }
124 
126  {
128  }
129 
130  friend inline string_exprt &to_string_expr(exprt &expr);
131 };
132 
134 {
135  assert(expr.id()==ID_struct);
136  assert(expr.operands().size()==2);
137  return static_cast<string_exprt &>(expr);
138 }
139 
140 inline const string_exprt &to_string_expr(const exprt &expr)
141 {
142  assert(expr.id()==ID_struct);
143  assert(expr.operands().size()==2);
144  return static_cast<const string_exprt &>(expr);
145 }
146 
147 #endif
The type of an expression.
Definition: type.h:20
index_exprt operator[](const exprt &idx) const
Definition: string_expr.h:45
A generic base class for relations, i.e., binary predicates.
Definition: std_expr.h:568
string_exprt(typet type)
Definition: string_expr.h:23
exprt & op0()
Definition: expr.h:84
exprt & content()
Definition: string_expr.h:40
friend string_exprt & to_string_expr(exprt &expr)
Definition: string_expr.h:133
void copy_to_operands(const exprt &expr)
Definition: expr.cpp:61
binary_relation_exprt axiom_for_is_strictly_longer_than(int i) const
Definition: string_expr.h:80
equal_exprt axiom_for_has_length(const exprt &rhs) const
Definition: string_expr.h:120
exprt & length()
Definition: string_expr.h:36
equal_exprt axiom_for_has_same_length_as(const string_exprt &rhs) const
Definition: string_expr.h:114
typet & type()
Definition: expr.h:60
binary_relation_exprt axiom_for_is_shorter_than(const string_exprt &rhs) const
Definition: string_expr.h:85
equality
Definition: std_expr.h:1082
binary_relation_exprt axiom_for_is_strictly_shorter_than(const string_exprt &rhs) const
Definition: string_expr.h:102
const irep_idt & id() const
Definition: irep.h:189
const exprt & length() const
Definition: string_expr.h:35
API to expression classes.
exprt & op1()
Definition: expr.h:87
binary_relation_exprt axiom_for_is_longer_than(const exprt &rhs) const
Definition: string_expr.h:62
binary_relation_exprt axiom_for_is_shorter_than(const exprt &rhs) const
Definition: string_expr.h:91
equal_exprt axiom_for_has_length(int i) const
Definition: string_expr.h:125
static exprt within_bounds(const exprt &idx, const exprt &bound)
binary_relation_exprt axiom_for_is_longer_than(const string_exprt &rhs) const
Definition: string_expr.h:56
binary_relation_exprt axiom_for_is_shorter_than(int i) const
Definition: string_expr.h:97
Base class for all expressions.
Definition: expr.h:46
const exprt & content() const
Definition: string_expr.h:39
binary_relation_exprt axiom_for_is_strictly_longer_than(const exprt &rhs) const
Definition: string_expr.h:68
string_exprt(const exprt &_length, const exprt &_content, typet type)
Definition: string_expr.h:28
binary_relation_exprt axiom_for_is_strictly_shorter_than(const exprt &rhs) const
Definition: string_expr.h:108
operandst & operands()
Definition: expr.h:70
constant_exprt from_integer(const mp_integer &int_value, const typet &type)
struct constructor from list of elements
Definition: std_expr.h:1464
binary_relation_exprt axiom_for_is_strictly_longer_than(const string_exprt &rhs) const
Definition: string_expr.h:74
array index operator
Definition: std_expr.h:1170