1
2 /*
3 * File StringUtils.cpp.
4 *
5 * This file is part of the source code of the software program
6 * Vampire. It is protected by applicable
7 * copyright laws.
8 *
9 * This source code is distributed under the licence found here
10 * https://vprover.github.io/license.html
11 * and in the source directory
12 *
13 * In summary, you are allowed to use Vampire for non-commercial
14 * purposes but not allowed to distribute, modify, copy, create derivatives,
15 * or use in competitions.
16 * For other uses of Vampire please contact developers for a different
17 * licence, which we will make an effort to provide.
18 */
19 /**
20 * @file StringUtils.cpp
21 * Implements class StringUtils.
22 */
23
24 #include "DArray.hpp"
25 #include "DHMap.hpp"
26 #include "Stack.hpp"
27
28 #include "StringUtils.hpp"
29
30 namespace Lib
31 {
32
33 using namespace std;
34
replaceChar(vstring str,char src,char target)35 vstring StringUtils::replaceChar(vstring str, char src, char target)
36 {
37 CALL("StringUtils::replaceChar");
38
39 size_t len=str.size();
40 static DArray<char> buf;
41 buf.ensure(len);
42
43 const char* sptr=str.c_str();
44 char* tptr=buf.array();
45
46 while(*sptr) {
47 if(*sptr==src) {
48 *tptr=target;
49 }
50 else {
51 *tptr=*sptr;
52 }
53 tptr++;
54 sptr++;
55 }
56 return vstring(buf.array(), len);
57 }
58
59 /**
60 * Sanitize vstring so that it can be used as a valid suffix in the
61 * Signature::addFreshFunction() and Signature::addFreshPredicate()
62 * functions.
63 */
sanitizeSuffix(vstring str)64 vstring StringUtils::sanitizeSuffix(vstring str)
65 {
66 CALL("StringUtils::sanitizeSuffix");
67
68 size_t len=str.size();
69 static DArray<char> buf;
70 buf.ensure(len);
71
72 const char* sptr=str.c_str();
73 char* tptr=buf.array();
74
75 while(*sptr) {
76 char c = *sptr;
77
78 switch(c) {
79 case '(':
80 case ')':
81 case '"':
82 case '\'':
83 case '$':
84 case '%':
85 case ',':
86 case '.':
87 c = '_';
88 break;
89 default: break;
90 }
91
92 *tptr = c;
93 tptr++;
94 sptr++;
95 }
96 return vstring(buf.array(), len);
97 }
98
isPositiveInteger(vstring str)99 bool StringUtils::isPositiveInteger(vstring str)
100 {
101 CALL("StringUtils::isPositiveInteger");
102
103 size_t sz = str.size();
104
105 if(str[0]=='0') {
106 return sz==1;
107 }
108 for(size_t i=0; i<sz; i++) {
109 if(str[i]<'0' || str[i]>'9') {
110 return false;
111 }
112 }
113 return true;
114 }
115
isPositiveDecimal(vstring str)116 bool StringUtils::isPositiveDecimal(vstring str)
117 {
118 CALL("StringUtils::isPositiveDecimal");
119
120 size_t sz = str.size();
121
122 size_t i = 0;
123 if(str[0]=='0') {
124 if(sz==1) { return true; }
125 if(str[1]!='.') { return false; }
126 i = 1;
127 }
128 bool seenPoint = false;
129 for(; i<sz; i++) {
130 if(str[i]=='.') {
131 if(i==0 || seenPoint) { return false; }
132 seenPoint = true;
133 }
134 else if(str[i]<'0' || str[i]>'9') {
135 return false;
136 }
137 }
138 return true;
139 }
140
splitStr(const char * str,char delimiter,Stack<vstring> & strings)141 void StringUtils::splitStr(const char* str, char delimiter, Stack<vstring>& strings)
142 {
143 CALL("StringUtils::splitStr");
144
145 static Stack<char> currPart;
146 currPart.reset();
147
148 const char* curr = str;
149 while(*curr) {
150 if(*curr==delimiter) {
151 currPart.push(0);
152 strings.push(currPart.begin());
153 currPart.reset();
154 }
155 else {
156 currPart.push(*curr);
157 }
158 curr++;
159 }
160 currPart.push(0);
161 strings.push(currPart.begin());
162 }
163
readEquality(const char * str,char eqChar,vstring & lhs,vstring & rhs)164 bool StringUtils::readEquality(const char* str, char eqChar, vstring& lhs, vstring& rhs)
165 {
166 CALL("StringUtils::readEquality");
167
168 static Stack<vstring> parts;
169 parts.reset();
170 splitStr(str, eqChar, parts);
171 if(parts.size()!=2) {
172 return false;
173 }
174 lhs = parts[0];
175 rhs = parts[1];
176 return true;
177 }
178
179 /**
180 * If str doesn't contain equalities, false is returned and the content of pairs is undefined.
181 */
readEqualities(const char * str,char delimiter,char eqChar,DHMap<vstring,vstring> & pairs)182 bool StringUtils::readEqualities(const char* str, char delimiter, char eqChar, DHMap<vstring,vstring>& pairs)
183 {
184 CALL("StringUtils::readEqualities");
185
186 static Stack<vstring> parts;
187 parts.reset();
188 splitStr(str, delimiter, parts);
189
190 Stack<vstring>::TopFirstIterator pit(parts);
191 while(pit.hasNext()) {
192 vstring part = pit.next();
193 vstring lhs, rhs;
194 if(!readEquality(part.c_str(), eqChar, lhs, rhs)) {
195 return false;
196 }
197 pairs.set(lhs, rhs);
198 }
199 return true;
200 }
201
202 }
203