Head

GCC Code Coverage Report

Directory:	.		Exec	Total	Coverage
File:	src/theory/strings/word.cpp	Lines:	233	282	82.6 %
Date:	2021-09-29	Branches:	305	1026	29.7 %


/******************************************************************************
 * Top contributors (to current version):
 *   Andrew Reynolds, Andres Noetzli, Aina Niemetz
 *
 * This file is part of the cvc5 project.
 *
 * Copyright (c) 2009-2021 by the authors listed in the file AUTHORS
 * in the top-level source directory and their institutional affiliations.
 * All rights reserved.  See the file COPYING in the top-level source
 * directory for licensing information.
 * ****************************************************************************
 *
 * Implementation of utility functions for words.
 */

#include "theory/strings/word.h"

#include "expr/sequence.h"
#include "util/string.h"

using namespace cvc5::kind;

namespace cvc5 {
namespace theory {
namespace strings {

Node Word::mkEmptyWord(TypeNode tn)
{
  if (tn.isString())
  {
    std::vector<unsigned> vec;
    return NodeManager::currentNM()->mkConst(String(vec));
  }
  else if (tn.isSequence())
  {
    std::vector<Node> seq;
    return NodeManager::currentNM()->mkConst(
        Sequence(tn.getSequenceElementType(), seq));
  }
  Unimplemented();
  return Node::null();
}

Node Word::mkWordFlatten(const std::vector<Node>& xs)
{
  Assert(!xs.empty());
  NodeManager* nm = NodeManager::currentNM();
  Kind k = xs[0].getKind();
  if (k == CONST_STRING)
  {
    std::vector<unsigned> vec;
    for (TNode x : xs)
    {
      Assert(x.getKind() == CONST_STRING);
      String sx = x.getConst<String>();
      const std::vector<unsigned>& vecc = sx.getVec();
      vec.insert(vec.end(), vecc.begin(), vecc.end());
    }
    return nm->mkConst(String(vec));
  }
  else if (k == CONST_SEQUENCE)
  {
    std::vector<Node> seq;
    TypeNode tn = xs[0].getType();
    for (TNode x : xs)
    {
      Assert(x.getType() == tn);
      const Sequence& sx = x.getConst<Sequence>();
      const std::vector<Node>& vecc = sx.getVec();
      seq.insert(seq.end(), vecc.begin(), vecc.end());
    }
    return NodeManager::currentNM()->mkConst(
        Sequence(tn.getSequenceElementType(), seq));
  }
  Unimplemented();
  return Node::null();
}

size_t Word::getLength(TNode x)
{
  Kind k = x.getKind();
  if (k == CONST_STRING)
  {
    return x.getConst<String>().size();
  }
  else if (k == CONST_SEQUENCE)
  {
    return x.getConst<Sequence>().size();
  }
  Unimplemented() << "Word::getLength on " << x;
  return 0;
}

std::vector<Node> Word::getChars(TNode x)
{
  Kind k = x.getKind();
  std::vector<Node> ret;
  NodeManager* nm = NodeManager::currentNM();
  if (k == CONST_STRING)
  {
    std::vector<unsigned> ccVec;
    const std::vector<unsigned>& cvec = x.getConst<String>().getVec();
    for (unsigned chVal : cvec)
    {
      ccVec.clear();
      ccVec.push_back(chVal);
      Node ch = nm->mkConst(String(ccVec));
      ret.push_back(ch);
    }
    return ret;
  }
  else if (k == CONST_SEQUENCE)
  {
    TypeNode t = x.getConst<Sequence>().getType();
    const Sequence& sx = x.getConst<Sequence>();
    const std::vector<Node>& vec = sx.getVec();
    for (const Node& v : vec)
    {
      ret.push_back(nm->mkConst(Sequence(t, {v})));
    }
    return ret;
  }
  Unimplemented();
  return ret;
}

bool Word::isEmpty(TNode x) { return x.isConst() && getLength(x) == 0; }

bool Word::strncmp(TNode x, TNode y, std::size_t n)
{
  Kind k = x.getKind();
  if (k == CONST_STRING)
  {
    Assert(y.getKind() == CONST_STRING);
    String sx = x.getConst<String>();
    String sy = y.getConst<String>();
    return sx.strncmp(sy, n);
  }
  else if (k == CONST_SEQUENCE)
  {
    Assert(y.getKind() == CONST_SEQUENCE);
    const Sequence& sx = x.getConst<Sequence>();
    const Sequence& sy = y.getConst<Sequence>();
    return sx.strncmp(sy, n);
  }
  Unimplemented();
  return false;
}

bool Word::rstrncmp(TNode x, TNode y, std::size_t n)
{
  Kind k = x.getKind();
  if (k == CONST_STRING)
  {
    Assert(y.getKind() == CONST_STRING);
    String sx = x.getConst<String>();
    String sy = y.getConst<String>();
    return sx.rstrncmp(sy, n);
  }
  else if (k == CONST_SEQUENCE)
  {
    Assert(y.getKind() == CONST_SEQUENCE);
    const Sequence& sx = x.getConst<Sequence>();
    const Sequence& sy = y.getConst<Sequence>();
    return sx.rstrncmp(sy, n);
  }
  Unimplemented();
  return false;
}

std::size_t Word::find(TNode x, TNode y, std::size_t start)
{
  Kind k = x.getKind();
  if (k == CONST_STRING)
  {
    Assert(y.getKind() == CONST_STRING);
    String sx = x.getConst<String>();
    String sy = y.getConst<String>();
    return sx.find(sy, start);
  }
  else if (k == CONST_SEQUENCE)
  {
    Assert(y.getKind() == CONST_SEQUENCE);
    const Sequence& sx = x.getConst<Sequence>();
    const Sequence& sy = y.getConst<Sequence>();
    return sx.find(sy, start);
  }
  Unimplemented();
  return 0;
}

std::size_t Word::rfind(TNode x, TNode y, std::size_t start)
{
  Kind k = x.getKind();
  if (k == CONST_STRING)
  {
    Assert(y.getKind() == CONST_STRING);
    String sx = x.getConst<String>();
    String sy = y.getConst<String>();
    return sx.rfind(sy, start);
  }
  else if (k == CONST_SEQUENCE)
  {
    Assert(y.getKind() == CONST_SEQUENCE);
    const Sequence& sx = x.getConst<Sequence>();
    const Sequence& sy = y.getConst<Sequence>();
    return sx.rfind(sy, start);
  }
  Unimplemented();
  return 0;
}

bool Word::hasPrefix(TNode x, TNode y)
{
  Kind k = x.getKind();
  if (k == CONST_STRING)
  {
    Assert(y.getKind() == CONST_STRING);
    String sx = x.getConst<String>();
    String sy = y.getConst<String>();
    return sx.hasPrefix(sy);
  }
  else if (k == CONST_SEQUENCE)
  {
    Assert(y.getKind() == CONST_SEQUENCE);
    const Sequence& sx = x.getConst<Sequence>();
    const Sequence& sy = y.getConst<Sequence>();
    return sx.hasPrefix(sy);
  }
  Unimplemented();
  return false;
}

bool Word::hasSuffix(TNode x, TNode y)
{
  Kind k = x.getKind();
  if (k == CONST_STRING)
  {
    Assert(y.getKind() == CONST_STRING);
    String sx = x.getConst<String>();
    String sy = y.getConst<String>();
    return sx.hasSuffix(sy);
  }
  else if (k == CONST_SEQUENCE)
  {
    Assert(y.getKind() == CONST_SEQUENCE);
    const Sequence& sx = x.getConst<Sequence>();
    const Sequence& sy = y.getConst<Sequence>();
    return sx.hasSuffix(sy);
  }
  Unimplemented();
  return false;
}

Node Word::update(TNode x, std::size_t i, TNode t)
{
  NodeManager* nm = NodeManager::currentNM();
  Kind k = x.getKind();
  if (k == CONST_STRING)
  {
    Assert(t.getKind() == CONST_STRING);
    String sx = x.getConst<String>();
    String st = t.getConst<String>();
    return nm->mkConst(String(sx.update(i, st)));
  }
  else if (k == CONST_SEQUENCE)
  {
    Assert(t.getKind() == CONST_SEQUENCE);
    const Sequence& sx = x.getConst<Sequence>();
    const Sequence& st = t.getConst<Sequence>();
    Sequence res = sx.update(i, st);
    return nm->mkConst(res);
  }
  Unimplemented();
  return Node::null();
}
Node Word::replace(TNode x, TNode y, TNode t)
{
  NodeManager* nm = NodeManager::currentNM();
  Kind k = x.getKind();
  if (k == CONST_STRING)
  {
    Assert(y.getKind() == CONST_STRING);
    Assert(t.getKind() == CONST_STRING);
    String sx = x.getConst<String>();
    String sy = y.getConst<String>();
    String st = t.getConst<String>();
    return nm->mkConst(String(sx.replace(sy, st)));
  }
  else if (k == CONST_SEQUENCE)
  {
    Assert(y.getKind() == CONST_SEQUENCE);
    Assert(t.getKind() == CONST_SEQUENCE);
    const Sequence& sx = x.getConst<Sequence>();
    const Sequence& sy = y.getConst<Sequence>();
    const Sequence& st = t.getConst<Sequence>();
    Sequence res = sx.replace(sy, st);
    return nm->mkConst(res);
  }
  Unimplemented();
  return Node::null();
}
Node Word::substr(TNode x, std::size_t i)
{
  NodeManager* nm = NodeManager::currentNM();
  Kind k = x.getKind();
  if (k == CONST_STRING)
  {
    String sx = x.getConst<String>();
    return nm->mkConst(String(sx.substr(i)));
  }
  else if (k == CONST_SEQUENCE)
  {
    const Sequence& sx = x.getConst<Sequence>();
    Sequence res = sx.substr(i);
    return nm->mkConst(res);
  }
  Unimplemented();
  return Node::null();
}
Node Word::substr(TNode x, std::size_t i, std::size_t j)
{
  NodeManager* nm = NodeManager::currentNM();
  Kind k = x.getKind();
  if (k == CONST_STRING)
  {
    String sx = x.getConst<String>();
    return nm->mkConst(String(sx.substr(i, j)));
  }
  else if (k == CONST_SEQUENCE)
  {
    const Sequence& sx = x.getConst<Sequence>();
    Sequence res = sx.substr(i, j);
    return nm->mkConst(res);
  }
  Unimplemented();
  return Node::null();
}

Node Word::prefix(TNode x, std::size_t i) { return substr(x, 0, i); }

Node Word::suffix(TNode x, std::size_t i)
{
  NodeManager* nm = NodeManager::currentNM();
  Kind k = x.getKind();
  if (k == CONST_STRING)
  {
    String sx = x.getConst<String>();
    return nm->mkConst(String(sx.suffix(i)));
  }
  else if (k == CONST_SEQUENCE)
  {
    const Sequence& sx = x.getConst<Sequence>();
    Sequence res = sx.suffix(i);
    return nm->mkConst(res);
  }
  Unimplemented();
  return Node::null();
}

bool Word::noOverlapWith(TNode x, TNode y)
{
  Kind k = x.getKind();
  if (k == CONST_STRING)
  {
    Assert(y.getKind() == CONST_STRING);
    String sx = x.getConst<String>();
    String sy = y.getConst<String>();
    return sx.noOverlapWith(sy);
  }
  else if (k == CONST_SEQUENCE)
  {
    Assert(y.getKind() == CONST_SEQUENCE);
    const Sequence& sx = x.getConst<Sequence>();
    const Sequence& sy = y.getConst<Sequence>();
    return sx.noOverlapWith(sy);
  }
  Unimplemented();
  return false;
}

std::size_t Word::overlap(TNode x, TNode y)
{
  Kind k = x.getKind();
  if (k == CONST_STRING)
  {
    Assert(y.getKind() == CONST_STRING);
    String sx = x.getConst<String>();
    String sy = y.getConst<String>();
    return sx.overlap(sy);
  }
  else if (k == CONST_SEQUENCE)
  {
    Assert(y.getKind() == CONST_SEQUENCE);
    const Sequence& sx = x.getConst<Sequence>();
    const Sequence& sy = y.getConst<Sequence>();
    return sx.overlap(sy);
  }
  Unimplemented();
  return 0;
}

std::size_t Word::roverlap(TNode x, TNode y)
{
  Kind k = x.getKind();
  if (k == CONST_STRING)
  {
    Assert(y.getKind() == CONST_STRING);
    String sx = x.getConst<String>();
    String sy = y.getConst<String>();
    return sx.roverlap(sy);
  }
  else if (k == CONST_SEQUENCE)
  {
    Assert(y.getKind() == CONST_SEQUENCE);
    const Sequence& sx = x.getConst<Sequence>();
    const Sequence& sy = y.getConst<Sequence>();
    return sx.roverlap(sy);
  }
  Unimplemented();
  return 0;
}

bool Word::isRepeated(TNode x)
{
  Kind k = x.getKind();
  if (k == CONST_STRING)
  {
    return x.getConst<String>().isRepeated();
  }
  else if (k == CONST_SEQUENCE)
  {
    return x.getConst<Sequence>().isRepeated();
  }
  Unimplemented();
  return false;
}

Node Word::splitConstant(TNode x, TNode y, size_t& index, bool isRev)
{
  Assert(x.isConst() && y.isConst());
  size_t lenA = getLength(x);
  size_t lenB = getLength(y);
  index = lenA <= lenB ? 1 : 0;
  size_t lenShort = index == 1 ? lenA : lenB;
  bool cmp = isRev ? rstrncmp(x, y, lenShort) : strncmp(x, y, lenShort);
  if (cmp)
  {
    Node l = index == 0 ? x : y;
    if (isRev)
    {
      size_t new_len = getLength(l) - lenShort;
      return substr(l, 0, new_len);
    }
    else
    {
      return substr(l, lenShort);
    }
  }
  // not the same prefix/suffix
  return Node::null();
}

Node Word::reverse(TNode x)
{
  NodeManager* nm = NodeManager::currentNM();
  Kind k = x.getKind();
  if (k == CONST_STRING)
  {
    String sx = x.getConst<String>();
    std::vector<unsigned> nvec = sx.getVec();
    std::reverse(nvec.begin(), nvec.end());
    return nm->mkConst(String(nvec));
  }
  else if (k == CONST_SEQUENCE)
  {
    const Sequence& sx = x.getConst<Sequence>();
    const std::vector<Node>& vecc = sx.getVec();
    std::vector<Node> vecr(vecc.begin(), vecc.end());
    std::reverse(vecr.begin(), vecr.end());
    Sequence res(sx.getType(), vecr);
    return nm->mkConst(res);
  }
  Unimplemented();
  return Node::null();
}

}  // namespace strings
}  // namespace theory
}  // namespace cvc5


Generated by: GCOVR (Version 3.2)

Line	Exec	Source
1		/******************************************************************************
2		* Top contributors (to current version):
3		* Andrew Reynolds, Andres Noetzli, Aina Niemetz
4		*
5		* This file is part of the cvc5 project.
6		*
7		* Copyright (c) 2009-2021 by the authors listed in the file AUTHORS
8		* in the top-level source directory and their institutional affiliations.
9		* All rights reserved. See the file COPYING in the top-level source
10		* directory for licensing information.
11		* ****************************************************************************
12		*
13		* Implementation of utility functions for words.
14		*/
15
16		#include "theory/strings/word.h"
17
18		#include "expr/sequence.h"
19		#include "util/string.h"
20
21		using namespace cvc5::kind;
22
23		namespace cvc5 {
24		namespace theory {
25		namespace strings {
26
27	1578308	Node Word::mkEmptyWord(TypeNode tn)
28		{
29	1578308	if (tn.isString())
30		{
31	3148252	std::vector<unsigned> vec;
32	1574126	return NodeManager::currentNM()->mkConst(String(vec));
33		}
34	4182	else if (tn.isSequence())
35		{
36	8364	std::vector<Node> seq;
37		return NodeManager::currentNM()->mkConst(
38	4182	Sequence(tn.getSequenceElementType(), seq));
39		}
40		Unimplemented();
41		return Node::null();
42		}
43
44	66435	Node Word::mkWordFlatten(const std::vector<Node>& xs)
45		{
46	66435	Assert(!xs.empty());
47	66435	NodeManager* nm = NodeManager::currentNM();
48	66435	Kind k = xs[0].getKind();
49	66435	if (k == CONST_STRING)
50		{
51	132512	std::vector<unsigned> vec;
52	182420	for (TNode x : xs)
53		{
54	116164	Assert(x.getKind() == CONST_STRING);
55	232328	String sx = x.getConst<String>();
56	116164	const std::vector<unsigned>& vecc = sx.getVec();
57	116164	vec.insert(vec.end(), vecc.begin(), vecc.end());
58		}
59	66256	return nm->mkConst(String(vec));
60		}
61	179	else if (k == CONST_SEQUENCE)
62		{
63	358	std::vector<Node> seq;
64	358	TypeNode tn = xs[0].getType();
65	502	for (TNode x : xs)
66		{
67	323	Assert(x.getType() == tn);
68	323	const Sequence& sx = x.getConst<Sequence>();
69	323	const std::vector<Node>& vecc = sx.getVec();
70	323	seq.insert(seq.end(), vecc.begin(), vecc.end());
71		}
72		return NodeManager::currentNM()->mkConst(
73	179	Sequence(tn.getSequenceElementType(), seq));
74		}
75		Unimplemented();
76		return Node::null();
77		}
78
79	976762	size_t Word::getLength(TNode x)
80		{
81	976762	Kind k = x.getKind();
82	976762	if (k == CONST_STRING)
83		{
84	975205	return x.getConst<String>().size();
85		}
86	1557	else if (k == CONST_SEQUENCE)
87		{
88	1557	return x.getConst<Sequence>().size();
89		}
90		Unimplemented() << "Word::getLength on " << x;
91		return 0;
92		}
93
94	148228	std::vector<Node> Word::getChars(TNode x)
95		{
96	148228	Kind k = x.getKind();
97	148228	std::vector<Node> ret;
98	148228	NodeManager* nm = NodeManager::currentNM();
99	148228	if (k == CONST_STRING)
100		{
101	296002	std::vector<unsigned> ccVec;
102	148001	const std::vector<unsigned>& cvec = x.getConst<String>().getVec();
103	368056	for (unsigned chVal : cvec)
104		{
105	220055	ccVec.clear();
106	220055	ccVec.push_back(chVal);
107	440110	Node ch = nm->mkConst(String(ccVec));
108	220055	ret.push_back(ch);
109		}
110	148001	return ret;
111		}
112	227	else if (k == CONST_SEQUENCE)
113		{
114	454	TypeNode t = x.getConst<Sequence>().getType();
115	227	const Sequence& sx = x.getConst<Sequence>();
116	227	const std::vector<Node>& vec = sx.getVec();
117	445	for (const Node& v : vec)
118		{
119	218	ret.push_back(nm->mkConst(Sequence(t, {v})));
120		}
121	227	return ret;
122		}
123		Unimplemented();
124		return ret;
125		}
126
127	246799	bool Word::isEmpty(TNode x) { return x.isConst() && getLength(x) == 0; }
128
129	30251	bool Word::strncmp(TNode x, TNode y, std::size_t n)
130		{
131	30251	Kind k = x.getKind();
132	30251	if (k == CONST_STRING)
133		{
134	30250	Assert(y.getKind() == CONST_STRING);
135	60500	String sx = x.getConst<String>();
136	60500	String sy = y.getConst<String>();
137	30250	return sx.strncmp(sy, n);
138		}
139	1	else if (k == CONST_SEQUENCE)
140		{
141	1	Assert(y.getKind() == CONST_SEQUENCE);
142	1	const Sequence& sx = x.getConst<Sequence>();
143	1	const Sequence& sy = y.getConst<Sequence>();
144	1	return sx.strncmp(sy, n);
145		}
146		Unimplemented();
147		return false;
148		}
149
150	23476	bool Word::rstrncmp(TNode x, TNode y, std::size_t n)
151		{
152	23476	Kind k = x.getKind();
153	23476	if (k == CONST_STRING)
154		{
155	23450	Assert(y.getKind() == CONST_STRING);
156	46900	String sx = x.getConst<String>();
157	46900	String sy = y.getConst<String>();
158	23450	return sx.rstrncmp(sy, n);
159		}
160	26	else if (k == CONST_SEQUENCE)
161		{
162	26	Assert(y.getKind() == CONST_SEQUENCE);
163	26	const Sequence& sx = x.getConst<Sequence>();
164	26	const Sequence& sy = y.getConst<Sequence>();
165	26	return sx.rstrncmp(sy, n);
166		}
167		Unimplemented();
168		return false;
169		}
170
171	69792	std::size_t Word::find(TNode x, TNode y, std::size_t start)
172		{
173	69792	Kind k = x.getKind();
174	69792	if (k == CONST_STRING)
175		{
176	69610	Assert(y.getKind() == CONST_STRING);
177	139220	String sx = x.getConst<String>();
178	139220	String sy = y.getConst<String>();
179	69610	return sx.find(sy, start);
180		}
181	182	else if (k == CONST_SEQUENCE)
182		{
183	182	Assert(y.getKind() == CONST_SEQUENCE);
184	182	const Sequence& sx = x.getConst<Sequence>();
185	182	const Sequence& sy = y.getConst<Sequence>();
186	182	return sx.find(sy, start);
187		}
188		Unimplemented();
189		return 0;
190		}
191
192	5980	std::size_t Word::rfind(TNode x, TNode y, std::size_t start)
193		{
194	5980	Kind k = x.getKind();
195	5980	if (k == CONST_STRING)
196		{
197	5971	Assert(y.getKind() == CONST_STRING);
198	11942	String sx = x.getConst<String>();
199	11942	String sy = y.getConst<String>();
200	5971	return sx.rfind(sy, start);
201		}
202	9	else if (k == CONST_SEQUENCE)
203		{
204	9	Assert(y.getKind() == CONST_SEQUENCE);
205	9	const Sequence& sx = x.getConst<Sequence>();
206	9	const Sequence& sy = y.getConst<Sequence>();
207	9	return sx.rfind(sy, start);
208		}
209		Unimplemented();
210		return 0;
211		}
212
213	6498	bool Word::hasPrefix(TNode x, TNode y)
214		{
215	6498	Kind k = x.getKind();
216	6498	if (k == CONST_STRING)
217		{
218	6498	Assert(y.getKind() == CONST_STRING);
219	12996	String sx = x.getConst<String>();
220	12996	String sy = y.getConst<String>();
221	6498	return sx.hasPrefix(sy);
222		}
223		else if (k == CONST_SEQUENCE)
224		{
225		Assert(y.getKind() == CONST_SEQUENCE);
226		const Sequence& sx = x.getConst<Sequence>();
227		const Sequence& sy = y.getConst<Sequence>();
228		return sx.hasPrefix(sy);
229		}
230		Unimplemented();
231		return false;
232		}
233
234	7530	bool Word::hasSuffix(TNode x, TNode y)
235		{
236	7530	Kind k = x.getKind();
237	7530	if (k == CONST_STRING)
238		{
239	7510	Assert(y.getKind() == CONST_STRING);
240	15020	String sx = x.getConst<String>();
241	15020	String sy = y.getConst<String>();
242	7510	return sx.hasSuffix(sy);
243		}
244	20	else if (k == CONST_SEQUENCE)
245		{
246	20	Assert(y.getKind() == CONST_SEQUENCE);
247	20	const Sequence& sx = x.getConst<Sequence>();
248	20	const Sequence& sy = y.getConst<Sequence>();
249	20	return sx.hasSuffix(sy);
250		}
251		Unimplemented();
252		return false;
253		}
254
255	99	Node Word::update(TNode x, std::size_t i, TNode t)
256		{
257	99	NodeManager* nm = NodeManager::currentNM();
258	99	Kind k = x.getKind();
259	99	if (k == CONST_STRING)
260		{
261	89	Assert(t.getKind() == CONST_STRING);
262	178	String sx = x.getConst<String>();
263	178	String st = t.getConst<String>();
264	89	return nm->mkConst(String(sx.update(i, st)));
265		}
266	10	else if (k == CONST_SEQUENCE)
267		{
268	10	Assert(t.getKind() == CONST_SEQUENCE);
269	10	const Sequence& sx = x.getConst<Sequence>();
270	10	const Sequence& st = t.getConst<Sequence>();
271	20	Sequence res = sx.update(i, st);
272	10	return nm->mkConst(res);
273		}
274		Unimplemented();
275		return Node::null();
276		}
277	6	Node Word::replace(TNode x, TNode y, TNode t)
278		{
279	6	NodeManager* nm = NodeManager::currentNM();
280	6	Kind k = x.getKind();
281	6	if (k == CONST_STRING)
282		{
283	6	Assert(y.getKind() == CONST_STRING);
284	6	Assert(t.getKind() == CONST_STRING);
285	12	String sx = x.getConst<String>();
286	12	String sy = y.getConst<String>();
287	12	String st = t.getConst<String>();
288	6	return nm->mkConst(String(sx.replace(sy, st)));
289		}
290		else if (k == CONST_SEQUENCE)
291		{
292		Assert(y.getKind() == CONST_SEQUENCE);
293		Assert(t.getKind() == CONST_SEQUENCE);
294		const Sequence& sx = x.getConst<Sequence>();
295		const Sequence& sy = y.getConst<Sequence>();
296		const Sequence& st = t.getConst<Sequence>();
297		Sequence res = sx.replace(sy, st);
298		return nm->mkConst(res);
299		}
300		Unimplemented();
301		return Node::null();
302		}
303	20615	Node Word::substr(TNode x, std::size_t i)
304		{
305	20615	NodeManager* nm = NodeManager::currentNM();
306	20615	Kind k = x.getKind();
307	20615	if (k == CONST_STRING)
308		{
309	41228	String sx = x.getConst<String>();
310	20614	return nm->mkConst(String(sx.substr(i)));
311		}
312	1	else if (k == CONST_SEQUENCE)
313		{
314	1	const Sequence& sx = x.getConst<Sequence>();
315	2	Sequence res = sx.substr(i);
316	1	return nm->mkConst(res);
317		}
318		Unimplemented();
319		return Node::null();
320		}
321	32802	Node Word::substr(TNode x, std::size_t i, std::size_t j)
322		{
323	32802	NodeManager* nm = NodeManager::currentNM();
324	32802	Kind k = x.getKind();
325	32802	if (k == CONST_STRING)
326		{
327	65510	String sx = x.getConst<String>();
328	32755	return nm->mkConst(String(sx.substr(i, j)));
329		}
330	47	else if (k == CONST_SEQUENCE)
331		{
332	47	const Sequence& sx = x.getConst<Sequence>();
333	94	Sequence res = sx.substr(i, j);
334	47	return nm->mkConst(res);
335		}
336		Unimplemented();
337		return Node::null();
338		}
339
340	11697	Node Word::prefix(TNode x, std::size_t i) { return substr(x, 0, i); }
341
342	14785	Node Word::suffix(TNode x, std::size_t i)
343		{
344	14785	NodeManager* nm = NodeManager::currentNM();
345	14785	Kind k = x.getKind();
346	14785	if (k == CONST_STRING)
347		{
348	29540	String sx = x.getConst<String>();
349	14770	return nm->mkConst(String(sx.suffix(i)));
350		}
351	15	else if (k == CONST_SEQUENCE)
352		{
353	15	const Sequence& sx = x.getConst<Sequence>();
354	30	Sequence res = sx.suffix(i);
355	15	return nm->mkConst(res);
356		}
357		Unimplemented();
358		return Node::null();
359		}
360
361	140	bool Word::noOverlapWith(TNode x, TNode y)
362		{
363	140	Kind k = x.getKind();
364	140	if (k == CONST_STRING)
365		{
366	140	Assert(y.getKind() == CONST_STRING);
367	280	String sx = x.getConst<String>();
368	280	String sy = y.getConst<String>();
369	140	return sx.noOverlapWith(sy);
370		}
371		else if (k == CONST_SEQUENCE)
372		{
373		Assert(y.getKind() == CONST_SEQUENCE);
374		const Sequence& sx = x.getConst<Sequence>();
375		const Sequence& sy = y.getConst<Sequence>();
376		return sx.noOverlapWith(sy);
377		}
378		Unimplemented();
379		return false;
380		}
381
382	1855	std::size_t Word::overlap(TNode x, TNode y)
383		{
384	1855	Kind k = x.getKind();
385	1855	if (k == CONST_STRING)
386		{
387	1854	Assert(y.getKind() == CONST_STRING);
388	3708	String sx = x.getConst<String>();
389	3708	String sy = y.getConst<String>();
390	1854	return sx.overlap(sy);
391		}
392	1	else if (k == CONST_SEQUENCE)
393		{
394	1	Assert(y.getKind() == CONST_SEQUENCE);
395	1	const Sequence& sx = x.getConst<Sequence>();
396	1	const Sequence& sy = y.getConst<Sequence>();
397	1	return sx.overlap(sy);
398		}
399		Unimplemented();
400		return 0;
401		}
402
403	1777	std::size_t Word::roverlap(TNode x, TNode y)
404		{
405	1777	Kind k = x.getKind();
406	1777	if (k == CONST_STRING)
407		{
408	1777	Assert(y.getKind() == CONST_STRING);
409	3554	String sx = x.getConst<String>();
410	3554	String sy = y.getConst<String>();
411	1777	return sx.roverlap(sy);
412		}
413		else if (k == CONST_SEQUENCE)
414		{
415		Assert(y.getKind() == CONST_SEQUENCE);
416		const Sequence& sx = x.getConst<Sequence>();
417		const Sequence& sy = y.getConst<Sequence>();
418		return sx.roverlap(sy);
419		}
420		Unimplemented();
421		return 0;
422		}
423
424		bool Word::isRepeated(TNode x)
425		{
426		Kind k = x.getKind();
427		if (k == CONST_STRING)
428		{
429		return x.getConst<String>().isRepeated();
430		}
431		else if (k == CONST_SEQUENCE)
432		{
433		return x.getConst<Sequence>().isRepeated();
434		}
435		Unimplemented();
436		return false;
437		}
438
439	32337	Node Word::splitConstant(TNode x, TNode y, size_t& index, bool isRev)
440		{
441	32337	Assert(x.isConst() && y.isConst());
442	32337	size_t lenA = getLength(x);
443	32337	size_t lenB = getLength(y);
444	32337	index = lenA <= lenB ? 1 : 0;
445	32337	size_t lenShort = index == 1 ? lenA : lenB;
446	32337	bool cmp = isRev ? rstrncmp(x, y, lenShort) : strncmp(x, y, lenShort);
447	32337	if (cmp)
448		{
449	60380	Node l = index == 0 ? x : y;
450	30190	if (isRev)
451		{
452	12379	size_t new_len = getLength(l) - lenShort;
453	12379	return substr(l, 0, new_len);
454		}
455		else
456		{
457	17811	return substr(l, lenShort);
458		}
459		}
460		// not the same prefix/suffix
461	2147	return Node::null();
462		}
463
464	46	Node Word::reverse(TNode x)
465		{
466	46	NodeManager* nm = NodeManager::currentNM();
467	46	Kind k = x.getKind();
468	46	if (k == CONST_STRING)
469		{
470	90	String sx = x.getConst<String>();
471	90	std::vector<unsigned> nvec = sx.getVec();
472	45	std::reverse(nvec.begin(), nvec.end());
473	45	return nm->mkConst(String(nvec));
474		}
475	1	else if (k == CONST_SEQUENCE)
476		{
477	1	const Sequence& sx = x.getConst<Sequence>();
478	1	const std::vector<Node>& vecc = sx.getVec();
479	2	std::vector<Node> vecr(vecc.begin(), vecc.end());
480	1	std::reverse(vecr.begin(), vecr.end());
481	2	Sequence res(sx.getType(), vecr);
482	1	return nm->mkConst(res);
483		}
484		Unimplemented();
485		return Node::null();
486		}
487
488		} // namespace strings
489		} // namespace theory
490	22746	} // namespace cvc5