Head

GCC Code Coverage Report

Directory:	.		Exec	Total	Coverage
File:	src/theory/arrays/theory_arrays_type_rules.cpp	Lines:	89	134	66.4 %
Date:	2021-05-22	Branches:	173	658	26.3 %


/******************************************************************************
 * Top contributors (to current version):
 *   Morgan Deters, Clark Barrett, Mathias Preiner
 *
 * 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 and cardinality rules for the theory of arrays.
 */

#include "theory/arrays/theory_arrays_type_rules.h"

// for array-constant attributes
#include "theory/arrays/theory_arrays_rewriter.h"
#include "theory/type_enumerator.h"

namespace cvc5 {
namespace theory {
namespace arrays {

TypeNode ArraySelectTypeRule::computeType(NodeManager* nodeManager,
                                          TNode n,
                                          bool check)
{
  Assert(n.getKind() == kind::SELECT);
  TypeNode arrayType = n[0].getType(check);
  if (check)
  {
    if (!arrayType.isArray())
    {
      throw TypeCheckingExceptionPrivate(n,
                                         "array select operating on non-array");
    }
    TypeNode indexType = n[1].getType(check);
    if (!indexType.isSubtypeOf(arrayType.getArrayIndexType()))
    {
      throw TypeCheckingExceptionPrivate(
          n, "array select not indexed with correct type for array");
    }
  }
  return arrayType.getArrayConstituentType();
}

TypeNode ArrayStoreTypeRule::computeType(NodeManager* nodeManager,
                                         TNode n,
                                         bool check)
{
  if (n.getKind() == kind::STORE)
  {
    TypeNode arrayType = n[0].getType(check);
    if (check)
    {
      if (!arrayType.isArray())
      {
        throw TypeCheckingExceptionPrivate(
            n, "array store operating on non-array");
      }
      TypeNode indexType = n[1].getType(check);
      TypeNode valueType = n[2].getType(check);
      if (!indexType.isSubtypeOf(arrayType.getArrayIndexType()))
      {
        throw TypeCheckingExceptionPrivate(
            n, "array store not indexed with correct type for array");
      }
      if (!valueType.isSubtypeOf(arrayType.getArrayConstituentType()))
      {
        Debug("array-types")
            << "array type: " << arrayType.getArrayConstituentType()
            << std::endl;
        Debug("array-types") << "value types: " << valueType << std::endl;
        throw TypeCheckingExceptionPrivate(
            n, "array store not assigned with correct type for array");
      }
    }
    return arrayType;
  }
  else
  {
    Assert(n.getKind() == kind::STORE_ALL);
    ArrayStoreAll storeAll = n.getConst<ArrayStoreAll>();
    return storeAll.getType();
  }
}

bool ArrayStoreTypeRule::computeIsConst(NodeManager* nodeManager, TNode n)
{
  Assert(n.getKind() == kind::STORE);
  NodeManagerScope nms(nodeManager);

  TNode store = n[0];
  TNode index = n[1];
  TNode value = n[2];

  // A constant must have only constant children and be in normal form
  // If any child is non-const, this is not a constant
  if (!store.isConst() || !index.isConst() || !value.isConst())
  {
    return false;
  }

  // Normal form for nested stores is just ordering by index but also need to
  // check that we are not writing to default value
  if (store.getKind() == kind::STORE && (!(store[1] < index)))
  {
    return false;
  }

  unsigned depth = 1;
  unsigned valCount = 1;
  while (store.getKind() == kind::STORE)
  {
    depth += 1;
    if (store[2] == value)
    {
      valCount += 1;
    }
    store = store[0];
  }
  Assert(store.getKind() == kind::STORE_ALL);
  ArrayStoreAll storeAll = store.getConst<ArrayStoreAll>();
  Node defaultValue = storeAll.getValue();
  if (value == defaultValue)
  {
    return false;
  }

  // Get the cardinality of the index type
  Cardinality indexCard = index.getType().getCardinality();

  if (indexCard.isInfinite())
  {
    return true;
  }

  // When index sort is finite, we have to check whether there is any value
  // that is written to more than the default value.  If so, it is not in
  // normal form.

  // Get the most frequently written value for n[0]
  TNode mostFrequentValue;
  unsigned mostFrequentValueCount = 0;
  store = n[0];
  if (store.getKind() == kind::STORE)
  {
    mostFrequentValue = getMostFrequentValue(store);
    mostFrequentValueCount = getMostFrequentValueCount(store);
  }

  // Compute the most frequently written value for n
  if (valCount > mostFrequentValueCount
      || (valCount == mostFrequentValueCount && value < mostFrequentValue))
  {
    mostFrequentValue = value;
    mostFrequentValueCount = valCount;
  }

  // Need to make sure the default value count is larger, or the same and the
  // default value is expression-order-less-than nextValue
  Cardinality::CardinalityComparison compare =
      indexCard.compare(mostFrequentValueCount + depth);
  Assert(compare != Cardinality::UNKNOWN);
  if (compare == Cardinality::LESS
      || (compare == Cardinality::EQUAL
          && (!(defaultValue < mostFrequentValue))))
  {
    return false;
  }
  setMostFrequentValue(n, mostFrequentValue);
  setMostFrequentValueCount(n, mostFrequentValueCount);
  return true;
}

TypeNode ArrayTableFunTypeRule::computeType(NodeManager* nodeManager,
                                            TNode n,
                                            bool check)
{
  Assert(n.getKind() == kind::ARR_TABLE_FUN);
  TypeNode arrayType = n[0].getType(check);
  if (check)
  {
    if (!arrayType.isArray())
    {
      throw TypeCheckingExceptionPrivate(n,
                                         "array table fun arg 0 is non-array");
    }
    TypeNode arrType2 = n[1].getType(check);
    if (!arrayType.isArray())
    {
      throw TypeCheckingExceptionPrivate(n,
                                         "array table fun arg 1 is non-array");
    }
    TypeNode indexType = n[2].getType(check);
    if (!indexType.isComparableTo(arrayType.getArrayIndexType()))
    {
      throw TypeCheckingExceptionPrivate(
          n, "array table fun arg 2 does not match type of array");
    }
    indexType = n[3].getType(check);
    if (!indexType.isComparableTo(arrayType.getArrayIndexType()))
    {
      throw TypeCheckingExceptionPrivate(
          n, "array table fun arg 3 does not match type of array");
    }
  }
  return arrayType.getArrayIndexType();
}

TypeNode ArrayLambdaTypeRule::computeType(NodeManager* nodeManager,
                                          TNode n,
                                          bool check)
{
  Assert(n.getKind() == kind::ARRAY_LAMBDA);
  TypeNode lamType = n[0].getType(check);
  if (check)
  {
    if (n[0].getKind() != kind::LAMBDA)
    {
      throw TypeCheckingExceptionPrivate(n, "array lambda arg is non-lambda");
    }
  }
  if (lamType.getNumChildren() != 2)
  {
    throw TypeCheckingExceptionPrivate(n,
                                       "array lambda arg is not unary lambda");
  }
  return nodeManager->mkArrayType(lamType[0], lamType[1]);
}

Cardinality ArraysProperties::computeCardinality(TypeNode type)
{
  Assert(type.getKind() == kind::ARRAY_TYPE);

  Cardinality indexCard = type[0].getCardinality();
  Cardinality valueCard = type[1].getCardinality();

  return valueCard ^ indexCard;
}

bool ArraysProperties::isWellFounded(TypeNode type)
{
  return type[0].isWellFounded() && type[1].isWellFounded();
}

Node ArraysProperties::mkGroundTerm(TypeNode type)
{
  return *TypeEnumerator(type);
}

TypeNode ArrayPartialSelectTypeRule::computeType(NodeManager* nodeManager,
                                                 TNode n,
                                                 bool check)
{
  Assert(n.getKind() == kind::PARTIAL_SELECT_0
         || n.getKind() == kind::PARTIAL_SELECT_1);
  return nodeManager->integerType();
}

TypeNode ArrayEqRangeTypeRule::computeType(NodeManager* nodeManager,
                                           TNode n,
                                           bool check)
{
  Assert(n.getKind() == kind::EQ_RANGE);
  if (check)
  {
    TypeNode n0_type = n[0].getType(check);
    TypeNode n1_type = n[1].getType(check);
    if (!n0_type.isArray())
    {
      throw TypeCheckingExceptionPrivate(
          n, "first operand of eqrange is not an array");
    }
    if (!n1_type.isArray())
    {
      throw TypeCheckingExceptionPrivate(
          n, "second operand of eqrange is not an array");
    }
    if (n0_type != n1_type)
    {
      throw TypeCheckingExceptionPrivate(n, "array types do not match");
    }
    TypeNode indexType = n0_type.getArrayIndexType();
    TypeNode indexRangeType1 = n[2].getType(check);
    TypeNode indexRangeType2 = n[3].getType(check);
    if (!indexRangeType1.isSubtypeOf(indexType))
    {
      throw TypeCheckingExceptionPrivate(
          n, "eqrange lower index type does not match array index type");
    }
    if (!indexRangeType2.isSubtypeOf(indexType))
    {
      throw TypeCheckingExceptionPrivate(
          n, "eqrange upper index type does not match array index type");
    }
    if (!indexType.isBitVector() && !indexType.isFloatingPoint()
        && !indexType.isInteger() && !indexType.isReal())
    {
      throw TypeCheckingExceptionPrivate(
          n,
          "eqrange only supports bit-vectors, floating-points, integers, and "
          "reals as index type");
    }
  }
  return nodeManager->booleanType();
}

}  // namespace arrays
}  // namespace theory
}  // namespace cvc5


Generated by: GCOVR (Version 3.2)

Line	Exec	Source
1		/******************************************************************************
2		* Top contributors (to current version):
3		* Morgan Deters, Clark Barrett, Mathias Preiner
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 and cardinality rules for the theory of arrays.
14		*/
15
16		#include "theory/arrays/theory_arrays_type_rules.h"
17
18		// for array-constant attributes
19		#include "theory/arrays/theory_arrays_rewriter.h"
20		#include "theory/type_enumerator.h"
21
22		namespace cvc5 {
23		namespace theory {
24		namespace arrays {
25
26	17991	TypeNode ArraySelectTypeRule::computeType(NodeManager* nodeManager,
27		TNode n,
28		bool check)
29		{
30	17991	Assert(n.getKind() == kind::SELECT);
31	35982	TypeNode arrayType = n[0].getType(check);
32	17991	if (check)
33		{
34	17991	if (!arrayType.isArray())
35		{
36		throw TypeCheckingExceptionPrivate(n,
37		"array select operating on non-array");
38		}
39	35982	TypeNode indexType = n[1].getType(check);
40	17991	if (!indexType.isSubtypeOf(arrayType.getArrayIndexType()))
41		{
42		throw TypeCheckingExceptionPrivate(
43		n, "array select not indexed with correct type for array");
44		}
45		}
46	35982	return arrayType.getArrayConstituentType();
47		}
48
49	11990	TypeNode ArrayStoreTypeRule::computeType(NodeManager* nodeManager,
50		TNode n,
51		bool check)
52		{
53	11990	if (n.getKind() == kind::STORE)
54		{
55	22800	TypeNode arrayType = n[0].getType(check);
56	11400	if (check)
57		{
58	11400	if (!arrayType.isArray())
59		{
60		throw TypeCheckingExceptionPrivate(
61		n, "array store operating on non-array");
62		}
63	22800	TypeNode indexType = n[1].getType(check);
64	22800	TypeNode valueType = n[2].getType(check);
65	11400	if (!indexType.isSubtypeOf(arrayType.getArrayIndexType()))
66		{
67		throw TypeCheckingExceptionPrivate(
68		n, "array store not indexed with correct type for array");
69		}
70	11400	if (!valueType.isSubtypeOf(arrayType.getArrayConstituentType()))
71		{
72		Debug("array-types")
73		<< "array type: " << arrayType.getArrayConstituentType()
74		<< std::endl;
75		Debug("array-types") << "value types: " << valueType << std::endl;
76		throw TypeCheckingExceptionPrivate(
77		n, "array store not assigned with correct type for array");
78		}
79		}
80	11400	return arrayType;
81		}
82		else
83		{
84	590	Assert(n.getKind() == kind::STORE_ALL);
85	1180	ArrayStoreAll storeAll = n.getConst<ArrayStoreAll>();
86	590	return storeAll.getType();
87		}
88		}
89
90	8482	bool ArrayStoreTypeRule::computeIsConst(NodeManager* nodeManager, TNode n)
91		{
92	8482	Assert(n.getKind() == kind::STORE);
93	16964	NodeManagerScope nms(nodeManager);
94
95	16964	TNode store = n[0];
96	16964	TNode index = n[1];
97	16964	TNode value = n[2];
98
99		// A constant must have only constant children and be in normal form
100		// If any child is non-const, this is not a constant
101	8482	if (!store.isConst() \|\| !index.isConst() \|\| !value.isConst())
102		{
103	5077	return false;
104		}
105
106		// Normal form for nested stores is just ordering by index but also need to
107		// check that we are not writing to default value
108	3405	if (store.getKind() == kind::STORE && (!(store[1] < index)))
109		{
110	17	return false;
111		}
112
113	3388	unsigned depth = 1;
114	3388	unsigned valCount = 1;
115	7008	while (store.getKind() == kind::STORE)
116		{
117	1810	depth += 1;
118	1810	if (store[2] == value)
119		{
120	245	valCount += 1;
121		}
122	1810	store = store[0];
123		}
124	3388	Assert(store.getKind() == kind::STORE_ALL);
125	6776	ArrayStoreAll storeAll = store.getConst<ArrayStoreAll>();
126	6776	Node defaultValue = storeAll.getValue();
127	3388	if (value == defaultValue)
128		{
129	17	return false;
130		}
131
132		// Get the cardinality of the index type
133	6742	Cardinality indexCard = index.getType().getCardinality();
134
135	3371	if (indexCard.isInfinite())
136		{
137	2867	return true;
138		}
139
140		// When index sort is finite, we have to check whether there is any value
141		// that is written to more than the default value. If so, it is not in
142		// normal form.
143
144		// Get the most frequently written value for n[0]
145	1008	TNode mostFrequentValue;
146	504	unsigned mostFrequentValueCount = 0;
147	504	store = n[0];
148	504	if (store.getKind() == kind::STORE)
149		{
150	246	mostFrequentValue = getMostFrequentValue(store);
151	246	mostFrequentValueCount = getMostFrequentValueCount(store);
152		}
153
154		// Compute the most frequently written value for n
155	504	if (valCount > mostFrequentValueCount
156	504	\|\| (valCount == mostFrequentValueCount && value < mostFrequentValue))
157		{
158	365	mostFrequentValue = value;
159	365	mostFrequentValueCount = valCount;
160		}
161
162		// Need to make sure the default value count is larger, or the same and the
163		// default value is expression-order-less-than nextValue
164		Cardinality::CardinalityComparison compare =
165	504	indexCard.compare(mostFrequentValueCount + depth);
166	504	Assert(compare != Cardinality::UNKNOWN);
167	504	if (compare == Cardinality::LESS
168	508	\|\| (compare == Cardinality::EQUAL
169	131	&& (!(defaultValue < mostFrequentValue))))
170		{
171	4	return false;
172		}
173	500	setMostFrequentValue(n, mostFrequentValue);
174	500	setMostFrequentValueCount(n, mostFrequentValueCount);
175	500	return true;
176		}
177
178		TypeNode ArrayTableFunTypeRule::computeType(NodeManager* nodeManager,
179		TNode n,
180		bool check)
181		{
182		Assert(n.getKind() == kind::ARR_TABLE_FUN);
183		TypeNode arrayType = n[0].getType(check);
184		if (check)
185		{
186		if (!arrayType.isArray())
187		{
188		throw TypeCheckingExceptionPrivate(n,
189		"array table fun arg 0 is non-array");
190		}
191		TypeNode arrType2 = n[1].getType(check);
192		if (!arrayType.isArray())
193		{
194		throw TypeCheckingExceptionPrivate(n,
195		"array table fun arg 1 is non-array");
196		}
197		TypeNode indexType = n[2].getType(check);
198		if (!indexType.isComparableTo(arrayType.getArrayIndexType()))
199		{
200		throw TypeCheckingExceptionPrivate(
201		n, "array table fun arg 2 does not match type of array");
202		}
203		indexType = n[3].getType(check);
204		if (!indexType.isComparableTo(arrayType.getArrayIndexType()))
205		{
206		throw TypeCheckingExceptionPrivate(
207		n, "array table fun arg 3 does not match type of array");
208		}
209		}
210		return arrayType.getArrayIndexType();
211		}
212
213		TypeNode ArrayLambdaTypeRule::computeType(NodeManager* nodeManager,
214		TNode n,
215		bool check)
216		{
217		Assert(n.getKind() == kind::ARRAY_LAMBDA);
218		TypeNode lamType = n[0].getType(check);
219		if (check)
220		{
221		if (n[0].getKind() != kind::LAMBDA)
222		{
223		throw TypeCheckingExceptionPrivate(n, "array lambda arg is non-lambda");
224		}
225		}
226		if (lamType.getNumChildren() != 2)
227		{
228		throw TypeCheckingExceptionPrivate(n,
229		"array lambda arg is not unary lambda");
230		}
231		return nodeManager->mkArrayType(lamType[0], lamType[1]);
232		}
233
234	292	Cardinality ArraysProperties::computeCardinality(TypeNode type)
235		{
236	292	Assert(type.getKind() == kind::ARRAY_TYPE);
237
238	584	Cardinality indexCard = type[0].getCardinality();
239	584	Cardinality valueCard = type[1].getCardinality();
240
241	584	return valueCard ^ indexCard;
242		}
243
244		bool ArraysProperties::isWellFounded(TypeNode type)
245		{
246		return type[0].isWellFounded() && type[1].isWellFounded();
247		}
248
249	15	Node ArraysProperties::mkGroundTerm(TypeNode type)
250		{
251	15	return *TypeEnumerator(type);
252		}
253
254		TypeNode ArrayPartialSelectTypeRule::computeType(NodeManager* nodeManager,
255		TNode n,
256		bool check)
257		{
258		Assert(n.getKind() == kind::PARTIAL_SELECT_0
259		\|\| n.getKind() == kind::PARTIAL_SELECT_1);
260		return nodeManager->integerType();
261		}
262
263	33	TypeNode ArrayEqRangeTypeRule::computeType(NodeManager* nodeManager,
264		TNode n,
265		bool check)
266		{
267	33	Assert(n.getKind() == kind::EQ_RANGE);
268	33	if (check)
269		{
270	66	TypeNode n0_type = n[0].getType(check);
271	66	TypeNode n1_type = n[1].getType(check);
272	33	if (!n0_type.isArray())
273		{
274		throw TypeCheckingExceptionPrivate(
275		n, "first operand of eqrange is not an array");
276		}
277	33	if (!n1_type.isArray())
278		{
279		throw TypeCheckingExceptionPrivate(
280		n, "second operand of eqrange is not an array");
281		}
282	33	if (n0_type != n1_type)
283		{
284		throw TypeCheckingExceptionPrivate(n, "array types do not match");
285		}
286	66	TypeNode indexType = n0_type.getArrayIndexType();
287	66	TypeNode indexRangeType1 = n[2].getType(check);
288	66	TypeNode indexRangeType2 = n[3].getType(check);
289	33	if (!indexRangeType1.isSubtypeOf(indexType))
290		{
291		throw TypeCheckingExceptionPrivate(
292		n, "eqrange lower index type does not match array index type");
293		}
294	33	if (!indexRangeType2.isSubtypeOf(indexType))
295		{
296		throw TypeCheckingExceptionPrivate(
297		n, "eqrange upper index type does not match array index type");
298		}
299	74	if (!indexType.isBitVector() && !indexType.isFloatingPoint()
300	41	&& !indexType.isInteger() && !indexType.isReal())
301		{
302		throw TypeCheckingExceptionPrivate(
303		n,
304		"eqrange only supports bit-vectors, floating-points, integers, and "
305		"reals as index type");
306		}
307		}
308	33	return nodeManager->booleanType();
309		}
310
311		} // namespace arrays
312		} // namespace theory
313	28191	} // namespace cvc5