Head

GCC Code Coverage Report

Directory:	.		Exec	Total	Coverage
File:	src/theory/strings/word.cpp	Lines:	233	282	82.6 %
Date:	2021-05-22	Branches:	305	1028	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	1321374	Node Word::mkEmptyWord(TypeNode tn)
28		{
29	1321374	if (tn.isString())
30		{
31	2623892	std::vector<unsigned> vec;
32	1311946	return NodeManager::currentNM()->mkConst(String(vec));
33		}
34	9428	else if (tn.isSequence())
35		{
36	18856	std::vector<Node> seq;
37		return NodeManager::currentNM()->mkConst(
38	9428	Sequence(tn.getSequenceElementType(), seq));
39		}
40		Unimplemented();
41		return Node::null();
42		}
43
44	41631	Node Word::mkWordFlatten(const std::vector<Node>& xs)
45		{
46	41631	Assert(!xs.empty());
47	41631	NodeManager* nm = NodeManager::currentNM();
48	41631	Kind k = xs[0].getKind();
49	41631	if (k == CONST_STRING)
50		{
51	82278	std::vector<unsigned> vec;
52	104846	for (TNode x : xs)
53		{
54	63707	Assert(x.getKind() == CONST_STRING);
55	127414	String sx = x.getConst<String>();
56	63707	const std::vector<unsigned>& vecc = sx.getVec();
57	63707	vec.insert(vec.end(), vecc.begin(), vecc.end());
58		}
59	41139	return nm->mkConst(String(vec));
60		}
61	492	else if (k == CONST_SEQUENCE)
62		{
63	984	std::vector<Node> seq;
64	984	TypeNode tn = xs[0].getType();
65	1142	for (TNode x : xs)
66		{
67	650	Assert(x.getType() == tn);
68	650	const Sequence& sx = x.getConst<Sequence>();
69	650	const std::vector<Node>& vecc = sx.getVec();
70	650	seq.insert(seq.end(), vecc.begin(), vecc.end());
71		}
72		return NodeManager::currentNM()->mkConst(
73	492	Sequence(tn.getSequenceElementType(), seq));
74		}
75		Unimplemented();
76		return Node::null();
77		}
78
79	974022	size_t Word::getLength(TNode x)
80		{
81	974022	Kind k = x.getKind();
82	974022	if (k == CONST_STRING)
83		{
84	962084	return x.getConst<String>().size();
85		}
86	11938	else if (k == CONST_SEQUENCE)
87		{
88	11938	return x.getConst<Sequence>().size();
89		}
90		Unimplemented() << "Word::getLength on " << x;
91		return 0;
92		}
93
94	175387	std::vector<Node> Word::getChars(TNode x)
95		{
96	175387	Kind k = x.getKind();
97	175387	std::vector<Node> ret;
98	175387	NodeManager* nm = NodeManager::currentNM();
99	175387	if (k == CONST_STRING)
100		{
101	342522	std::vector<unsigned> ccVec;
102	171261	const std::vector<unsigned>& cvec = x.getConst<String>().getVec();
103	470602	for (unsigned chVal : cvec)
104		{
105	299341	ccVec.clear();
106	299341	ccVec.push_back(chVal);
107	598682	Node ch = nm->mkConst(String(ccVec));
108	299341	ret.push_back(ch);
109		}
110	171261	return ret;
111		}
112	4126	else if (k == CONST_SEQUENCE)
113		{
114	8252	TypeNode t = x.getConst<Sequence>().getType();
115	4126	const Sequence& sx = x.getConst<Sequence>();
116	4126	const std::vector<Node>& vec = sx.getVec();
117	6230	for (const Node& v : vec)
118		{
119	2104	ret.push_back(nm->mkConst(Sequence(t, {v})));
120		}
121	4126	return ret;
122		}
123		Unimplemented();
124		return ret;
125		}
126
127	283581	bool Word::isEmpty(TNode x) { return x.isConst() && getLength(x) == 0; }
128
129	23180	bool Word::strncmp(TNode x, TNode y, std::size_t n)
130		{
131	23180	Kind k = x.getKind();
132	23180	if (k == CONST_STRING)
133		{
134	23176	Assert(y.getKind() == CONST_STRING);
135	46352	String sx = x.getConst<String>();
136	46352	String sy = y.getConst<String>();
137	23176	return sx.strncmp(sy, n);
138		}
139	4	else if (k == CONST_SEQUENCE)
140		{
141	4	Assert(y.getKind() == CONST_SEQUENCE);
142	4	const Sequence& sx = x.getConst<Sequence>();
143	4	const Sequence& sy = y.getConst<Sequence>();
144	4	return sx.strncmp(sy, n);
145		}
146		Unimplemented();
147		return false;
148		}
149
150	24965	bool Word::rstrncmp(TNode x, TNode y, std::size_t n)
151		{
152	24965	Kind k = x.getKind();
153	24965	if (k == CONST_STRING)
154		{
155	24898	Assert(y.getKind() == CONST_STRING);
156	49796	String sx = x.getConst<String>();
157	49796	String sy = y.getConst<String>();
158	24898	return sx.rstrncmp(sy, n);
159		}
160	67	else if (k == CONST_SEQUENCE)
161		{
162	67	Assert(y.getKind() == CONST_SEQUENCE);
163	67	const Sequence& sx = x.getConst<Sequence>();
164	67	const Sequence& sy = y.getConst<Sequence>();
165	67	return sx.rstrncmp(sy, n);
166		}
167		Unimplemented();
168		return false;
169		}
170
171	72971	std::size_t Word::find(TNode x, TNode y, std::size_t start)
172		{
173	72971	Kind k = x.getKind();
174	72971	if (k == CONST_STRING)
175		{
176	72710	Assert(y.getKind() == CONST_STRING);
177	145420	String sx = x.getConst<String>();
178	145420	String sy = y.getConst<String>();
179	72710	return sx.find(sy, start);
180		}
181	261	else if (k == CONST_SEQUENCE)
182		{
183	261	Assert(y.getKind() == CONST_SEQUENCE);
184	261	const Sequence& sx = x.getConst<Sequence>();
185	261	const Sequence& sy = y.getConst<Sequence>();
186	261	return sx.find(sy, start);
187		}
188		Unimplemented();
189		return 0;
190		}
191
192	9215	std::size_t Word::rfind(TNode x, TNode y, std::size_t start)
193		{
194	9215	Kind k = x.getKind();
195	9215	if (k == CONST_STRING)
196		{
197	9121	Assert(y.getKind() == CONST_STRING);
198	18242	String sx = x.getConst<String>();
199	18242	String sy = y.getConst<String>();
200	9121	return sx.rfind(sy, start);
201		}
202	94	else if (k == CONST_SEQUENCE)
203		{
204	94	Assert(y.getKind() == CONST_SEQUENCE);
205	94	const Sequence& sx = x.getConst<Sequence>();
206	94	const Sequence& sy = y.getConst<Sequence>();
207	94	return sx.rfind(sy, start);
208		}
209		Unimplemented();
210		return 0;
211		}
212
213	4441	bool Word::hasPrefix(TNode x, TNode y)
214		{
215	4441	Kind k = x.getKind();
216	4441	if (k == CONST_STRING)
217		{
218	4441	Assert(y.getKind() == CONST_STRING);
219	8882	String sx = x.getConst<String>();
220	8882	String sy = y.getConst<String>();
221	4441	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	7028	bool Word::hasSuffix(TNode x, TNode y)
235		{
236	7028	Kind k = x.getKind();
237	7028	if (k == CONST_STRING)
238		{
239	6986	Assert(y.getKind() == CONST_STRING);
240	13972	String sx = x.getConst<String>();
241	13972	String sy = y.getConst<String>();
242	6986	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	103	Node Word::update(TNode x, std::size_t i, TNode t)
256		{
257	103	NodeManager* nm = NodeManager::currentNM();
258	103	Kind k = x.getKind();
259	103	if (k == CONST_STRING)
260		{
261	93	Assert(t.getKind() == CONST_STRING);
262	186	String sx = x.getConst<String>();
263	186	String st = t.getConst<String>();
264	93	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	13583	Node Word::substr(TNode x, std::size_t i)
304		{
305	13583	NodeManager* nm = NodeManager::currentNM();
306	13583	Kind k = x.getKind();
307	13583	if (k == CONST_STRING)
308		{
309	27164	String sx = x.getConst<String>();
310	13582	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	31943	Node Word::substr(TNode x, std::size_t i, std::size_t j)
322		{
323	31943	NodeManager* nm = NodeManager::currentNM();
324	31943	Kind k = x.getKind();
325	31943	if (k == CONST_STRING)
326		{
327	63782	String sx = x.getConst<String>();
328	31891	return nm->mkConst(String(sx.substr(i, j)));
329		}
330	52	else if (k == CONST_SEQUENCE)
331		{
332	52	const Sequence& sx = x.getConst<Sequence>();
333	104	Sequence res = sx.substr(i, j);
334	52	return nm->mkConst(res);
335		}
336		Unimplemented();
337		return Node::null();
338		}
339
340	11811	Node Word::prefix(TNode x, std::size_t i) { return substr(x, 0, i); }
341
342	15116	Node Word::suffix(TNode x, std::size_t i)
343		{
344	15116	NodeManager* nm = NodeManager::currentNM();
345	15116	Kind k = x.getKind();
346	15116	if (k == CONST_STRING)
347		{
348	30202	String sx = x.getConst<String>();
349	15101	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	413	bool Word::noOverlapWith(TNode x, TNode y)
362		{
363	413	Kind k = x.getKind();
364	413	if (k == CONST_STRING)
365		{
366	413	Assert(y.getKind() == CONST_STRING);
367	826	String sx = x.getConst<String>();
368	826	String sy = y.getConst<String>();
369	413	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	4198	std::size_t Word::overlap(TNode x, TNode y)
383		{
384	4198	Kind k = x.getKind();
385	4198	if (k == CONST_STRING)
386		{
387	4156	Assert(y.getKind() == CONST_STRING);
388	8312	String sx = x.getConst<String>();
389	8312	String sy = y.getConst<String>();
390	4156	return sx.overlap(sy);
391		}
392	42	else if (k == CONST_SEQUENCE)
393		{
394	42	Assert(y.getKind() == CONST_SEQUENCE);
395	42	const Sequence& sx = x.getConst<Sequence>();
396	42	const Sequence& sy = y.getConst<Sequence>();
397	42	return sx.overlap(sy);
398		}
399		Unimplemented();
400		return 0;
401		}
402
403	1897	std::size_t Word::roverlap(TNode x, TNode y)
404		{
405	1897	Kind k = x.getKind();
406	1897	if (k == CONST_STRING)
407		{
408	1897	Assert(y.getKind() == CONST_STRING);
409	3794	String sx = x.getConst<String>();
410	3794	String sy = y.getConst<String>();
411	1897	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	23639	Node Word::splitConstant(TNode x, TNode y, size_t& index, bool isRev)
440		{
441	23639	Assert(x.isConst() && y.isConst());
442	23639	size_t lenA = getLength(x);
443	23639	size_t lenB = getLength(y);
444	23639	index = lenA <= lenB ? 1 : 0;
445	23639	size_t lenShort = index == 1 ? lenA : lenB;
446	23639	bool cmp = isRev ? rstrncmp(x, y, lenShort) : strncmp(x, y, lenShort);
447	23639	if (cmp)
448		{
449	45834	Node l = index == 0 ? x : y;
450	22917	if (isRev)
451		{
452	12482	size_t new_len = getLength(l) - lenShort;
453	12482	return substr(l, 0, new_len);
454		}
455		else
456		{
457	10435	return substr(l, lenShort);
458		}
459		}
460		// not the same prefix/suffix
461	722	return Node::null();
462		}
463
464	65	Node Word::reverse(TNode x)
465		{
466	65	NodeManager* nm = NodeManager::currentNM();
467	65	Kind k = x.getKind();
468	65	if (k == CONST_STRING)
469		{
470	122	String sx = x.getConst<String>();
471	122	std::vector<unsigned> nvec = sx.getVec();
472	61	std::reverse(nvec.begin(), nvec.end());
473	61	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	28194	} // namespace cvc5