Head

GCC Code Coverage Report

Directory:	.		Exec	Total	Coverage
File:	src/theory/strings/theory_strings_type_rules.cpp	Lines:	97	137	70.8 %
Date:	2021-08-16	Branches:	122	462	26.4 %


/******************************************************************************
 * Top contributors (to current version):
 *   Andrew Reynolds, Aina Niemetz, Yoni Zohar
 *
 * 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.
 * ****************************************************************************
 *
 * Typing rules for the theory of strings and regexps.
 */
#include "theory/strings/theory_strings_type_rules.h"

#include <sstream>

#include "expr/node_manager.h"
#include "expr/sequence.h"
#include "options/strings_options.h"
#include "util/cardinality.h"

namespace cvc5 {
namespace theory {
namespace strings {

TypeNode StringConcatTypeRule::computeType(NodeManager* nodeManager,
                                           TNode n,
                                           bool check)
{
  TypeNode tret;
  for (const Node& nc : n)
  {
    TypeNode t = nc.getType(check);
    if (tret.isNull())
    {
      tret = t;
      if (check)
      {
        if (!t.isStringLike())
        {
          throw TypeCheckingExceptionPrivate(
              n, "expecting string-like terms in concat");
        }
      }
      else
      {
        break;
      }
    }
    else if (t != tret)
    {
      throw TypeCheckingExceptionPrivate(
          n, "expecting all children to have the same type in concat");
    }
  }
  return tret;
}

TypeNode StringSubstrTypeRule::computeType(NodeManager* nodeManager,
                                           TNode n,
                                           bool check)
{
  TypeNode t = n[0].getType(check);
  if (check)
  {
    if (!t.isStringLike())
    {
      throw TypeCheckingExceptionPrivate(
          n, "expecting a string-like term in substr");
    }
    TypeNode t2 = n[1].getType(check);
    if (!t2.isInteger())
    {
      throw TypeCheckingExceptionPrivate(
          n, "expecting an integer start term in substr");
    }
    t2 = n[2].getType(check);
    if (!t2.isInteger())
    {
      throw TypeCheckingExceptionPrivate(
          n, "expecting an integer length term in substr");
    }
  }
  return t;
}

TypeNode StringUpdateTypeRule::computeType(NodeManager* nodeManager,
                                           TNode n,
                                           bool check)
{
  TypeNode t = n[0].getType(check);
  if (check)
  {
    if (!t.isStringLike())
    {
      throw TypeCheckingExceptionPrivate(
          n, "expecting a string-like term in update");
    }
    TypeNode t2 = n[1].getType(check);
    if (!t2.isInteger())
    {
      throw TypeCheckingExceptionPrivate(
          n, "expecting an integer start term in update");
    }
    t2 = n[2].getType(check);
    if (!t2.isStringLike())
    {
      throw TypeCheckingExceptionPrivate(
          n, "expecting an string-like replace term in update");
    }
  }
  return t;
}

TypeNode StringAtTypeRule::computeType(NodeManager* nodeManager,
                                       TNode n,
                                       bool check)
{
  TypeNode t = n[0].getType(check);
  if (check)
  {
    if (!t.isStringLike())
    {
      throw TypeCheckingExceptionPrivate(
          n, "expecting a string-like term in str.at");
    }
    TypeNode t2 = n[1].getType(check);
    if (!t2.isInteger())
    {
      throw TypeCheckingExceptionPrivate(
          n, "expecting an integer start term in str.at");
    }
  }
  return t;
}

TypeNode StringIndexOfTypeRule::computeType(NodeManager* nodeManager,
                                            TNode n,
                                            bool check)
{
  if (check)
  {
    TypeNode t = n[0].getType(check);
    if (!t.isStringLike())
    {
      throw TypeCheckingExceptionPrivate(
          n, "expecting a string-like term in indexof");
    }
    TypeNode t2 = n[1].getType(check);
    if (t != t2)
    {
      throw TypeCheckingExceptionPrivate(
          n,
          "expecting a term in second argument of indexof that is the same "
          "type as the first argument");
    }
    t = n[2].getType(check);
    if (!t.isInteger())
    {
      throw TypeCheckingExceptionPrivate(
          n, "expecting an integer term in third argument of indexof");
    }
  }
  return nodeManager->integerType();
}

TypeNode StringReplaceTypeRule::computeType(NodeManager* nodeManager,
                                            TNode n,
                                            bool check)
{
  TypeNode t = n[0].getType(check);
  if (check)
  {
    if (!t.isStringLike())
    {
      throw TypeCheckingExceptionPrivate(
          n, "expecting a string-like term in replace");
    }
    TypeNode t2 = n[1].getType(check);
    if (t != t2)
    {
      throw TypeCheckingExceptionPrivate(
          n,
          "expecting a term in second argument of replace that is the same "
          "type as the first argument");
    }
    t2 = n[2].getType(check);
    if (t != t2)
    {
      throw TypeCheckingExceptionPrivate(
          n,
          "expecting a term in third argument of replace that is the same "
          "type as the first argument");
    }
  }
  return t;
}

TypeNode StringStrToBoolTypeRule::computeType(NodeManager* nodeManager,
                                              TNode n,
                                              bool check)
{
  if (check)
  {
    TypeNode t = n[0].getType(check);
    if (!t.isStringLike())
    {
      std::stringstream ss;
      ss << "expecting a string-like term in argument of " << n.getKind();
      throw TypeCheckingExceptionPrivate(n, ss.str());
    }
  }
  return nodeManager->booleanType();
}

TypeNode StringStrToIntTypeRule::computeType(NodeManager* nodeManager,
                                             TNode n,
                                             bool check)
{
  if (check)
  {
    TypeNode t = n[0].getType(check);
    if (!t.isStringLike())
    {
      std::stringstream ss;
      ss << "expecting a string-like term in argument of " << n.getKind();
      throw TypeCheckingExceptionPrivate(n, ss.str());
    }
  }
  return nodeManager->integerType();
}

TypeNode StringStrToStrTypeRule::computeType(NodeManager* nodeManager,
                                             TNode n,
                                             bool check)
{
  TypeNode t = n[0].getType(check);
  if (check)
  {
    if (!t.isStringLike())
    {
      std::stringstream ss;
      ss << "expecting a string term in argument of " << n.getKind();
      throw TypeCheckingExceptionPrivate(n, ss.str());
    }
  }
  return t;
}

TypeNode StringRelationTypeRule::computeType(NodeManager* nodeManager,
                                             TNode n,
                                             bool check)
{
  if (check)
  {
    TypeNode t = n[0].getType(check);
    if (!t.isStringLike())
    {
      throw TypeCheckingExceptionPrivate(
          n, "expecting a string-like term in relation");
    }
    TypeNode t2 = n[1].getType(check);
    if (t != t2)
    {
      throw TypeCheckingExceptionPrivate(
          n, "expecting two terms of the same string-like type in relation");
    }
  }
  return nodeManager->booleanType();
}

TypeNode RegExpRangeTypeRule::computeType(NodeManager* nodeManager,
                                          TNode n,
                                          bool check)
{
  if (check)
  {
    TNode::iterator it = n.begin();
    for (int i = 0; i < 2; ++i)
    {
      TypeNode t = (*it).getType(check);
      if (!t.isString())  // string-only
      {
        throw TypeCheckingExceptionPrivate(
            n, "expecting a string term in regexp range");
      }
      ++it;
    }
  }
  return nodeManager->regExpType();
}

TypeNode ConstSequenceTypeRule::computeType(NodeManager* nodeManager,
                                            TNode n,
                                            bool check)
{
  Assert(n.getKind() == kind::CONST_SEQUENCE);
  return nodeManager->mkSequenceType(n.getConst<Sequence>().getType());
}

TypeNode SeqUnitTypeRule::computeType(NodeManager* nodeManager,
                                      TNode n,
                                      bool check)
{
  return nodeManager->mkSequenceType(n[0].getType(check));
}

TypeNode SeqNthTypeRule::computeType(NodeManager* nodeManager,
                                     TNode n,
                                     bool check)
{
  TypeNode t = n[0].getType(check);
  TypeNode t1 = t.getSequenceElementType();
  if (check)
  {
    if (!t.isSequence())
    {
      throw TypeCheckingExceptionPrivate(n, "expecting a sequence in nth");
    }
    TypeNode t2 = n[1].getType(check);
    if (!t2.isInteger())
    {
      throw TypeCheckingExceptionPrivate(
          n, "expecting an integer start term in nth");
    }
  }
  return t1;
}

Cardinality SequenceProperties::computeCardinality(TypeNode type)
{
  Assert(type.getKind() == kind::SEQUENCE_TYPE);
  return Cardinality::INTEGERS;
}
/** A sequence is well-founded if its element type is */
bool SequenceProperties::isWellFounded(TypeNode type)
{
  return type[0].isWellFounded();
}
/** Make ground term for sequence type (return the empty sequence) */
Node SequenceProperties::mkGroundTerm(TypeNode type)
{
  Assert(type.isSequence());
  // empty sequence
  std::vector<Node> seq;
  return NodeManager::currentNM()->mkConst(
      Sequence(type.getSequenceElementType(), seq));
}
}  // 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, Aina Niemetz, Yoni Zohar
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		* Typing rules for the theory of strings and regexps.
14		*/
15		#include "theory/strings/theory_strings_type_rules.h"
16
17		#include <sstream>
18
19		#include "expr/node_manager.h"
20		#include "expr/sequence.h"
21		#include "options/strings_options.h"
22		#include "util/cardinality.h"
23
24		namespace cvc5 {
25		namespace theory {
26		namespace strings {
27
28	45845	TypeNode StringConcatTypeRule::computeType(NodeManager* nodeManager,
29		TNode n,
30		bool check)
31		{
32	45845	TypeNode tret;
33	203597	for (const Node& nc : n)
34		{
35	315504	TypeNode t = nc.getType(check);
36	157752	if (tret.isNull())
37		{
38	45845	tret = t;
39	45845	if (check)
40		{
41	45845	if (!t.isStringLike())
42		{
43		throw TypeCheckingExceptionPrivate(
44		n, "expecting string-like terms in concat");
45		}
46		}
47		else
48		{
49		break;
50		}
51		}
52	111907	else if (t != tret)
53		{
54		throw TypeCheckingExceptionPrivate(
55		n, "expecting all children to have the same type in concat");
56		}
57		}
58	45845	return tret;
59		}
60
61	37584	TypeNode StringSubstrTypeRule::computeType(NodeManager* nodeManager,
62		TNode n,
63		bool check)
64		{
65	37584	TypeNode t = n[0].getType(check);
66	37584	if (check)
67		{
68	37584	if (!t.isStringLike())
69		{
70		throw TypeCheckingExceptionPrivate(
71		n, "expecting a string-like term in substr");
72		}
73	75168	TypeNode t2 = n[1].getType(check);
74	37584	if (!t2.isInteger())
75		{
76		throw TypeCheckingExceptionPrivate(
77		n, "expecting an integer start term in substr");
78		}
79	37584	t2 = n[2].getType(check);
80	37584	if (!t2.isInteger())
81		{
82		throw TypeCheckingExceptionPrivate(
83		n, "expecting an integer length term in substr");
84		}
85		}
86	37584	return t;
87		}
88
89	136	TypeNode StringUpdateTypeRule::computeType(NodeManager* nodeManager,
90		TNode n,
91		bool check)
92		{
93	136	TypeNode t = n[0].getType(check);
94	136	if (check)
95		{
96	136	if (!t.isStringLike())
97		{
98		throw TypeCheckingExceptionPrivate(
99		n, "expecting a string-like term in update");
100		}
101	272	TypeNode t2 = n[1].getType(check);
102	136	if (!t2.isInteger())
103		{
104		throw TypeCheckingExceptionPrivate(
105		n, "expecting an integer start term in update");
106		}
107	136	t2 = n[2].getType(check);
108	136	if (!t2.isStringLike())
109		{
110		throw TypeCheckingExceptionPrivate(
111		n, "expecting an string-like replace term in update");
112		}
113		}
114	136	return t;
115		}
116
117	131	TypeNode StringAtTypeRule::computeType(NodeManager* nodeManager,
118		TNode n,
119		bool check)
120		{
121	131	TypeNode t = n[0].getType(check);
122	131	if (check)
123		{
124	131	if (!t.isStringLike())
125		{
126		throw TypeCheckingExceptionPrivate(
127		n, "expecting a string-like term in str.at");
128		}
129	262	TypeNode t2 = n[1].getType(check);
130	131	if (!t2.isInteger())
131		{
132		throw TypeCheckingExceptionPrivate(
133		n, "expecting an integer start term in str.at");
134		}
135		}
136	131	return t;
137		}
138
139	3555	TypeNode StringIndexOfTypeRule::computeType(NodeManager* nodeManager,
140		TNode n,
141		bool check)
142		{
143	3555	if (check)
144		{
145	7110	TypeNode t = n[0].getType(check);
146	3555	if (!t.isStringLike())
147		{
148		throw TypeCheckingExceptionPrivate(
149		n, "expecting a string-like term in indexof");
150		}
151	7110	TypeNode t2 = n[1].getType(check);
152	3555	if (t != t2)
153		{
154		throw TypeCheckingExceptionPrivate(
155		n,
156		"expecting a term in second argument of indexof that is the same "
157		"type as the first argument");
158		}
159	3555	t = n[2].getType(check);
160	3555	if (!t.isInteger())
161		{
162		throw TypeCheckingExceptionPrivate(
163		n, "expecting an integer term in third argument of indexof");
164		}
165		}
166	3555	return nodeManager->integerType();
167		}
168
169	3161	TypeNode StringReplaceTypeRule::computeType(NodeManager* nodeManager,
170		TNode n,
171		bool check)
172		{
173	3161	TypeNode t = n[0].getType(check);
174	3161	if (check)
175		{
176	3161	if (!t.isStringLike())
177		{
178		throw TypeCheckingExceptionPrivate(
179		n, "expecting a string-like term in replace");
180		}
181	6322	TypeNode t2 = n[1].getType(check);
182	3161	if (t != t2)
183		{
184		throw TypeCheckingExceptionPrivate(
185		n,
186		"expecting a term in second argument of replace that is the same "
187		"type as the first argument");
188		}
189	3161	t2 = n[2].getType(check);
190	3161	if (t != t2)
191		{
192		throw TypeCheckingExceptionPrivate(
193		n,
194		"expecting a term in third argument of replace that is the same "
195		"type as the first argument");
196		}
197		}
198	3161	return t;
199		}
200
201	181	TypeNode StringStrToBoolTypeRule::computeType(NodeManager* nodeManager,
202		TNode n,
203		bool check)
204		{
205	181	if (check)
206		{
207	362	TypeNode t = n[0].getType(check);
208	181	if (!t.isStringLike())
209		{
210		std::stringstream ss;
211		ss << "expecting a string-like term in argument of " << n.getKind();
212		throw TypeCheckingExceptionPrivate(n, ss.str());
213		}
214		}
215	181	return nodeManager->booleanType();
216		}
217
218	116056	TypeNode StringStrToIntTypeRule::computeType(NodeManager* nodeManager,
219		TNode n,
220		bool check)
221		{
222	116056	if (check)
223		{
224	232112	TypeNode t = n[0].getType(check);
225	116056	if (!t.isStringLike())
226		{
227		std::stringstream ss;
228		ss << "expecting a string-like term in argument of " << n.getKind();
229		throw TypeCheckingExceptionPrivate(n, ss.str());
230		}
231		}
232	116056	return nodeManager->integerType();
233		}
234
235	163	TypeNode StringStrToStrTypeRule::computeType(NodeManager* nodeManager,
236		TNode n,
237		bool check)
238		{
239	163	TypeNode t = n[0].getType(check);
240	163	if (check)
241		{
242	163	if (!t.isStringLike())
243		{
244		std::stringstream ss;
245		ss << "expecting a string term in argument of " << n.getKind();
246		throw TypeCheckingExceptionPrivate(n, ss.str());
247		}
248		}
249	163	return t;
250		}
251
252	31520	TypeNode StringRelationTypeRule::computeType(NodeManager* nodeManager,
253		TNode n,
254		bool check)
255		{
256	31520	if (check)
257		{
258	63040	TypeNode t = n[0].getType(check);
259	31520	if (!t.isStringLike())
260		{
261		throw TypeCheckingExceptionPrivate(
262		n, "expecting a string-like term in relation");
263		}
264	63040	TypeNode t2 = n[1].getType(check);
265	31520	if (t != t2)
266		{
267		throw TypeCheckingExceptionPrivate(
268		n, "expecting two terms of the same string-like type in relation");
269		}
270		}
271	31520	return nodeManager->booleanType();
272		}
273
274	181	TypeNode RegExpRangeTypeRule::computeType(NodeManager* nodeManager,
275		TNode n,
276		bool check)
277		{
278	181	if (check)
279		{
280	181	TNode::iterator it = n.begin();
281	543	for (int i = 0; i < 2; ++i)
282		{
283	724	TypeNode t = (*it).getType(check);
284	362	if (!t.isString()) // string-only
285		{
286		throw TypeCheckingExceptionPrivate(
287		n, "expecting a string term in regexp range");
288		}
289	362	++it;
290		}
291		}
292	181	return nodeManager->regExpType();
293		}
294
295	429	TypeNode ConstSequenceTypeRule::computeType(NodeManager* nodeManager,
296		TNode n,
297		bool check)
298		{
299	429	Assert(n.getKind() == kind::CONST_SEQUENCE);
300	429	return nodeManager->mkSequenceType(n.getConst<Sequence>().getType());
301		}
302
303	272	TypeNode SeqUnitTypeRule::computeType(NodeManager* nodeManager,
304		TNode n,
305		bool check)
306		{
307	272	return nodeManager->mkSequenceType(n[0].getType(check));
308		}
309
310	226	TypeNode SeqNthTypeRule::computeType(NodeManager* nodeManager,
311		TNode n,
312		bool check)
313		{
314	452	TypeNode t = n[0].getType(check);
315	226	TypeNode t1 = t.getSequenceElementType();
316	226	if (check)
317		{
318	226	if (!t.isSequence())
319		{
320		throw TypeCheckingExceptionPrivate(n, "expecting a sequence in nth");
321		}
322	452	TypeNode t2 = n[1].getType(check);
323	226	if (!t2.isInteger())
324		{
325		throw TypeCheckingExceptionPrivate(
326		n, "expecting an integer start term in nth");
327		}
328		}
329	452	return t1;
330		}
331
332		Cardinality SequenceProperties::computeCardinality(TypeNode type)
333		{
334		Assert(type.getKind() == kind::SEQUENCE_TYPE);
335		return Cardinality::INTEGERS;
336		}
337		/** A sequence is well-founded if its element type is */
338		bool SequenceProperties::isWellFounded(TypeNode type)
339		{
340		return type[0].isWellFounded();
341		}
342		/** Make ground term for sequence type (return the empty sequence) */
343		Node SequenceProperties::mkGroundTerm(TypeNode type)
344		{
345		Assert(type.isSequence());
346		// empty sequence
347		std::vector<Node> seq;
348		return NodeManager::currentNM()->mkConst(
349		Sequence(type.getSequenceElementType(), seq));
350		}
351		} // namespace strings
352		} // namespace theory
353	29340	} // namespace cvc5