Head

GCC Code Coverage Report

Directory:	.		Exec	Total	Coverage
File:	src/theory/strings/word.cpp	Lines:	233	282	82.6 %
Date:	2021-09-10	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	2126313	Node Word::mkEmptyWord(TypeNode tn)
28		{
29	2126313	if (tn.isString())
30		{
31	4239588	std::vector<unsigned> vec;
32	2119794	return NodeManager::currentNM()->mkConst(String(vec));
33		}
34	6519	else if (tn.isSequence())
35		{
36	13038	std::vector<Node> seq;
37		return NodeManager::currentNM()->mkConst(
38	6519	Sequence(tn.getSequenceElementType(), seq));
39		}
40		Unimplemented();
41		return Node::null();
42		}
43
44	77064	Node Word::mkWordFlatten(const std::vector<Node>& xs)
45		{
46	77064	Assert(!xs.empty());
47	77064	NodeManager* nm = NodeManager::currentNM();
48	77064	Kind k = xs[0].getKind();
49	77064	if (k == CONST_STRING)
50		{
51	153622	std::vector<unsigned> vec;
52	209599	for (TNode x : xs)
53		{
54	132788	Assert(x.getKind() == CONST_STRING);
55	265576	String sx = x.getConst<String>();
56	132788	const std::vector<unsigned>& vecc = sx.getVec();
57	132788	vec.insert(vec.end(), vecc.begin(), vecc.end());
58		}
59	76811	return nm->mkConst(String(vec));
60		}
61	253	else if (k == CONST_SEQUENCE)
62		{
63	506	std::vector<Node> seq;
64	506	TypeNode tn = xs[0].getType();
65	691	for (TNode x : xs)
66		{
67	438	Assert(x.getType() == tn);
68	438	const Sequence& sx = x.getConst<Sequence>();
69	438	const std::vector<Node>& vecc = sx.getVec();
70	438	seq.insert(seq.end(), vecc.begin(), vecc.end());
71		}
72		return NodeManager::currentNM()->mkConst(
73	253	Sequence(tn.getSequenceElementType(), seq));
74		}
75		Unimplemented();
76		return Node::null();
77		}
78
79	1274423	size_t Word::getLength(TNode x)
80		{
81	1274423	Kind k = x.getKind();
82	1274423	if (k == CONST_STRING)
83		{
84	1271968	return x.getConst<String>().size();
85		}
86	2455	else if (k == CONST_SEQUENCE)
87		{
88	2455	return x.getConst<Sequence>().size();
89		}
90		Unimplemented() << "Word::getLength on " << x;
91		return 0;
92		}
93
94	189078	std::vector<Node> Word::getChars(TNode x)
95		{
96	189078	Kind k = x.getKind();
97	189078	std::vector<Node> ret;
98	189078	NodeManager* nm = NodeManager::currentNM();
99	189078	if (k == CONST_STRING)
100		{
101	377298	std::vector<unsigned> ccVec;
102	188649	const std::vector<unsigned>& cvec = x.getConst<String>().getVec();
103	449063	for (unsigned chVal : cvec)
104		{
105	260414	ccVec.clear();
106	260414	ccVec.push_back(chVal);
107	520828	Node ch = nm->mkConst(String(ccVec));
108	260414	ret.push_back(ch);
109		}
110	188649	return ret;
111		}
112	429	else if (k == CONST_SEQUENCE)
113		{
114	858	TypeNode t = x.getConst<Sequence>().getType();
115	429	const Sequence& sx = x.getConst<Sequence>();
116	429	const std::vector<Node>& vec = sx.getVec();
117	868	for (const Node& v : vec)
118		{
119	439	ret.push_back(nm->mkConst(Sequence(t, {v})));
120		}
121	429	return ret;
122		}
123		Unimplemented();
124		return ret;
125		}
126
127	323412	bool Word::isEmpty(TNode x) { return x.isConst() && getLength(x) == 0; }
128
129	31964	bool Word::strncmp(TNode x, TNode y, std::size_t n)
130		{
131	31964	Kind k = x.getKind();
132	31964	if (k == CONST_STRING)
133		{
134	31956	Assert(y.getKind() == CONST_STRING);
135	63912	String sx = x.getConst<String>();
136	63912	String sy = y.getConst<String>();
137	31956	return sx.strncmp(sy, n);
138		}
139	8	else if (k == CONST_SEQUENCE)
140		{
141	8	Assert(y.getKind() == CONST_SEQUENCE);
142	8	const Sequence& sx = x.getConst<Sequence>();
143	8	const Sequence& sy = y.getConst<Sequence>();
144	8	return sx.strncmp(sy, n);
145		}
146		Unimplemented();
147		return false;
148		}
149
150	27213	bool Word::rstrncmp(TNode x, TNode y, std::size_t n)
151		{
152	27213	Kind k = x.getKind();
153	27213	if (k == CONST_STRING)
154		{
155	27187	Assert(y.getKind() == CONST_STRING);
156	54374	String sx = x.getConst<String>();
157	54374	String sy = y.getConst<String>();
158	27187	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	96772	std::size_t Word::find(TNode x, TNode y, std::size_t start)
172		{
173	96772	Kind k = x.getKind();
174	96772	if (k == CONST_STRING)
175		{
176	96555	Assert(y.getKind() == CONST_STRING);
177	193110	String sx = x.getConst<String>();
178	193110	String sy = y.getConst<String>();
179	96555	return sx.find(sy, start);
180		}
181	217	else if (k == CONST_SEQUENCE)
182		{
183	217	Assert(y.getKind() == CONST_SEQUENCE);
184	217	const Sequence& sx = x.getConst<Sequence>();
185	217	const Sequence& sy = y.getConst<Sequence>();
186	217	return sx.find(sy, start);
187		}
188		Unimplemented();
189		return 0;
190		}
191
192	7226	std::size_t Word::rfind(TNode x, TNode y, std::size_t start)
193		{
194	7226	Kind k = x.getKind();
195	7226	if (k == CONST_STRING)
196		{
197	7214	Assert(y.getKind() == CONST_STRING);
198	14428	String sx = x.getConst<String>();
199	14428	String sy = y.getConst<String>();
200	7214	return sx.rfind(sy, start);
201		}
202	12	else if (k == CONST_SEQUENCE)
203		{
204	12	Assert(y.getKind() == CONST_SEQUENCE);
205	12	const Sequence& sx = x.getConst<Sequence>();
206	12	const Sequence& sy = y.getConst<Sequence>();
207	12	return sx.rfind(sy, start);
208		}
209		Unimplemented();
210		return 0;
211		}
212
213	10298	bool Word::hasPrefix(TNode x, TNode y)
214		{
215	10298	Kind k = x.getKind();
216	10298	if (k == CONST_STRING)
217		{
218	10298	Assert(y.getKind() == CONST_STRING);
219	20596	String sx = x.getConst<String>();
220	20596	String sy = y.getConst<String>();
221	10298	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	11568	bool Word::hasSuffix(TNode x, TNode y)
235		{
236	11568	Kind k = x.getKind();
237	11568	if (k == CONST_STRING)
238		{
239	11526	Assert(y.getKind() == CONST_STRING);
240	23052	String sx = x.getConst<String>();
241	23052	String sy = y.getConst<String>();
242	11526	return sx.hasSuffix(sy);
243		}
244	42	else if (k == CONST_SEQUENCE)
245		{
246	42	Assert(y.getKind() == CONST_SEQUENCE);
247	42	const Sequence& sx = x.getConst<Sequence>();
248	42	const Sequence& sy = y.getConst<Sequence>();
249	42	return sx.hasSuffix(sy);
250		}
251		Unimplemented();
252		return false;
253		}
254
255	102	Node Word::update(TNode x, std::size_t i, TNode t)
256		{
257	102	NodeManager* nm = NodeManager::currentNM();
258	102	Kind k = x.getKind();
259	102	if (k == CONST_STRING)
260		{
261	92	Assert(t.getKind() == CONST_STRING);
262	184	String sx = x.getConst<String>();
263	184	String st = t.getConst<String>();
264	92	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	22648	Node Word::substr(TNode x, std::size_t i)
304		{
305	22648	NodeManager* nm = NodeManager::currentNM();
306	22648	Kind k = x.getKind();
307	22648	if (k == CONST_STRING)
308		{
309	45294	String sx = x.getConst<String>();
310	22647	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	37883	Node Word::substr(TNode x, std::size_t i, std::size_t j)
322		{
323	37883	NodeManager* nm = NodeManager::currentNM();
324	37883	Kind k = x.getKind();
325	37883	if (k == CONST_STRING)
326		{
327	75660	String sx = x.getConst<String>();
328	37830	return nm->mkConst(String(sx.substr(i, j)));
329		}
330	53	else if (k == CONST_SEQUENCE)
331		{
332	53	const Sequence& sx = x.getConst<Sequence>();
333	106	Sequence res = sx.substr(i, j);
334	53	return nm->mkConst(res);
335		}
336		Unimplemented();
337		return Node::null();
338		}
339
340	12782	Node Word::prefix(TNode x, std::size_t i) { return substr(x, 0, i); }
341
342	15668	Node Word::suffix(TNode x, std::size_t i)
343		{
344	15668	NodeManager* nm = NodeManager::currentNM();
345	15668	Kind k = x.getKind();
346	15668	if (k == CONST_STRING)
347		{
348	31306	String sx = x.getConst<String>();
349	15653	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	195	bool Word::noOverlapWith(TNode x, TNode y)
362		{
363	195	Kind k = x.getKind();
364	195	if (k == CONST_STRING)
365		{
366	195	Assert(y.getKind() == CONST_STRING);
367	390	String sx = x.getConst<String>();
368	390	String sy = y.getConst<String>();
369	195	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	2208	std::size_t Word::overlap(TNode x, TNode y)
383		{
384	2208	Kind k = x.getKind();
385	2208	if (k == CONST_STRING)
386		{
387	2204	Assert(y.getKind() == CONST_STRING);
388	4408	String sx = x.getConst<String>();
389	4408	String sy = y.getConst<String>();
390	2204	return sx.overlap(sy);
391		}
392	4	else if (k == CONST_SEQUENCE)
393		{
394	4	Assert(y.getKind() == CONST_SEQUENCE);
395	4	const Sequence& sx = x.getConst<Sequence>();
396	4	const Sequence& sy = y.getConst<Sequence>();
397	4	return sx.overlap(sy);
398		}
399		Unimplemented();
400		return 0;
401		}
402
403	2195	std::size_t Word::roverlap(TNode x, TNode y)
404		{
405	2195	Kind k = x.getKind();
406	2195	if (k == CONST_STRING)
407		{
408	2195	Assert(y.getKind() == CONST_STRING);
409	4390	String sx = x.getConst<String>();
410	4390	String sy = y.getConst<String>();
411	2195	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	36830	Node Word::splitConstant(TNode x, TNode y, size_t& index, bool isRev)
440		{
441	36830	Assert(x.isConst() && y.isConst());
442	36830	size_t lenA = getLength(x);
443	36830	size_t lenB = getLength(y);
444	36830	index = lenA <= lenB ? 1 : 0;
445	36830	size_t lenShort = index == 1 ? lenA : lenB;
446	36830	bool cmp = isRev ? rstrncmp(x, y, lenShort) : strncmp(x, y, lenShort);
447	36830	if (cmp)
448		{
449	69062	Node l = index == 0 ? x : y;
450	34531	if (isRev)
451		{
452	15356	size_t new_len = getLength(l) - lenShort;
453	15356	return substr(l, 0, new_len);
454		}
455		else
456		{
457	19175	return substr(l, lenShort);
458		}
459		}
460		// not the same prefix/suffix
461	2299	return Node::null();
462		}
463
464	63	Node Word::reverse(TNode x)
465		{
466	63	NodeManager* nm = NodeManager::currentNM();
467	63	Kind k = x.getKind();
468	63	if (k == CONST_STRING)
469		{
470	118	String sx = x.getConst<String>();
471	118	std::vector<unsigned> nvec = sx.getVec();
472	59	std::reverse(nvec.begin(), nvec.end());
473	59	return nm->mkConst(String(nvec));
474		}
475	4	else if (k == CONST_SEQUENCE)
476		{
477	4	const Sequence& sx = x.getConst<Sequence>();
478	4	const std::vector<Node>& vecc = sx.getVec();
479	8	std::vector<Node> vecr(vecc.begin(), vecc.end());
480	4	std::reverse(vecr.begin(), vecr.end());
481	8	Sequence res(sx.getType(), vecr);
482	4	return nm->mkConst(res);
483		}
484		Unimplemented();
485		return Node::null();
486		}
487
488		} // namespace strings
489		} // namespace theory
490	29502	} // namespace cvc5