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-05-22	Branches:	122	464	26.3 %


/******************************************************************************
 * 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"

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