Head

GCC Code Coverage Report

Directory:	.		Exec	Total	Coverage
File:	src/theory/arrays/theory_arrays_type_rules.cpp	Lines:	92	138	66.7 %
Date:	2021-11-07	Branches:	179	684	26.2 %


/******************************************************************************
 * 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 "expr/array_store_all.h"
#include "theory/arrays/theory_arrays_rewriter.h"
#include "theory/builtin/theory_builtin_type_rules.h"
#include "theory/type_enumerator.h"
#include "util/cardinality.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);

  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)
{
  Assert(type.getKind() == kind::ARRAY_TYPE);
  TypeNode elemType = type.getArrayConstituentType();
  Node elem = elemType.mkGroundTerm();
  if (elem.isConst())
  {
    return NodeManager::currentNM()->mkConst(ArrayStoreAll(type, elem));
  }
  // Note the distinction between mkGroundTerm and mkGroundValue. While
  // an arbitrary value can be obtained by calling the type enumerator here,
  // that is wrong for types that are not closed enumerable since it may
  // return a term containing values that should not appear in e.g. assertions.
  // For example, arrays whose element type is an uninterpreted sort will
  // incorrectly introduce uninterpreted sort values if this is done.
  // It is currently infeasible to construct an ArrayStoreAll with the element
  // type's mkGroundTerm as an argument when that term is not constant.
  // Thus, we must simply return a fresh Skolem here, using the same utility
  // as that of uninterpreted sorts.
  return builtin::SortProperties::mkGroundTerm(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 "expr/array_store_all.h"
20		#include "theory/arrays/theory_arrays_rewriter.h"
21		#include "theory/builtin/theory_builtin_type_rules.h"
22		#include "theory/type_enumerator.h"
23		#include "util/cardinality.h"
24
25		namespace cvc5 {
26		namespace theory {
27		namespace arrays {
28
29	19262	TypeNode ArraySelectTypeRule::computeType(NodeManager* nodeManager,
30		TNode n,
31		bool check)
32		{
33	19262	Assert(n.getKind() == kind::SELECT);
34	38524	TypeNode arrayType = n[0].getType(check);
35	19262	if (check)
36		{
37	19262	if (!arrayType.isArray())
38		{
39		throw TypeCheckingExceptionPrivate(n,
40		"array select operating on non-array");
41		}
42	38524	TypeNode indexType = n[1].getType(check);
43	19262	if (!indexType.isSubtypeOf(arrayType.getArrayIndexType()))
44		{
45		throw TypeCheckingExceptionPrivate(
46		n, "array select not indexed with correct type for array");
47		}
48		}
49	38524	return arrayType.getArrayConstituentType();
50		}
51
52	12664	TypeNode ArrayStoreTypeRule::computeType(NodeManager* nodeManager,
53		TNode n,
54		bool check)
55		{
56	12664	if (n.getKind() == kind::STORE)
57		{
58	23768	TypeNode arrayType = n[0].getType(check);
59	11884	if (check)
60		{
61	11884	if (!arrayType.isArray())
62		{
63		throw TypeCheckingExceptionPrivate(
64		n, "array store operating on non-array");
65		}
66	23768	TypeNode indexType = n[1].getType(check);
67	23768	TypeNode valueType = n[2].getType(check);
68	11884	if (!indexType.isSubtypeOf(arrayType.getArrayIndexType()))
69		{
70		throw TypeCheckingExceptionPrivate(
71		n, "array store not indexed with correct type for array");
72		}
73	11884	if (!valueType.isSubtypeOf(arrayType.getArrayConstituentType()))
74		{
75		Debug("array-types")
76		<< "array type: " << arrayType.getArrayConstituentType()
77		<< std::endl;
78		Debug("array-types") << "value types: " << valueType << std::endl;
79		throw TypeCheckingExceptionPrivate(
80		n, "array store not assigned with correct type for array");
81		}
82		}
83	11884	return arrayType;
84		}
85		else
86		{
87	780	Assert(n.getKind() == kind::STORE_ALL);
88	1560	ArrayStoreAll storeAll = n.getConst<ArrayStoreAll>();
89	780	return storeAll.getType();
90		}
91		}
92
93	8339	bool ArrayStoreTypeRule::computeIsConst(NodeManager* nodeManager, TNode n)
94		{
95	8339	Assert(n.getKind() == kind::STORE);
96
97	16678	TNode store = n[0];
98	16678	TNode index = n[1];
99	16678	TNode value = n[2];
100
101		// A constant must have only constant children and be in normal form
102		// If any child is non-const, this is not a constant
103	8339	if (!store.isConst() \|\| !index.isConst() \|\| !value.isConst())
104		{
105	4800	return false;
106		}
107
108		// Normal form for nested stores is just ordering by index but also need to
109		// check that we are not writing to default value
110	3539	if (store.getKind() == kind::STORE && (!(store[1] < index)))
111		{
112	16	return false;
113		}
114
115	3523	unsigned depth = 1;
116	3523	unsigned valCount = 1;
117	7535	while (store.getKind() == kind::STORE)
118		{
119	2006	depth += 1;
120	2006	if (store[2] == value)
121		{
122	294	valCount += 1;
123		}
124	2006	store = store[0];
125		}
126	3523	Assert(store.getKind() == kind::STORE_ALL);
127	7046	ArrayStoreAll storeAll = store.getConst<ArrayStoreAll>();
128	7046	Node defaultValue = storeAll.getValue();
129	3523	if (value == defaultValue)
130		{
131	18	return false;
132		}
133
134		// Get the cardinality of the index type
135	7010	Cardinality indexCard = index.getType().getCardinality();
136
137	3505	if (indexCard.isInfinite())
138		{
139	2830	return true;
140		}
141
142		// When index sort is finite, we have to check whether there is any value
143		// that is written to more than the default value. If so, it is not in
144		// normal form.
145
146		// Get the most frequently written value for n[0]
147	1350	TNode mostFrequentValue;
148	675	unsigned mostFrequentValueCount = 0;
149	675	store = n[0];
150	675	if (store.getKind() == kind::STORE)
151		{
152	304	mostFrequentValue = getMostFrequentValue(store);
153	304	mostFrequentValueCount = getMostFrequentValueCount(store);
154		}
155
156		// Compute the most frequently written value for n
157	675	if (valCount > mostFrequentValueCount
158	675	\|\| (valCount == mostFrequentValueCount && value < mostFrequentValue))
159		{
160	503	mostFrequentValue = value;
161	503	mostFrequentValueCount = valCount;
162		}
163
164		// Need to make sure the default value count is larger, or the same and the
165		// default value is expression-order-less-than nextValue
166		Cardinality::CardinalityComparison compare =
167	675	indexCard.compare(mostFrequentValueCount + depth);
168	675	Assert(compare != Cardinality::UNKNOWN);
169	675	if (compare == Cardinality::LESS
170	679	\|\| (compare == Cardinality::EQUAL
171	232	&& (!(defaultValue < mostFrequentValue))))
172		{
173	4	return false;
174		}
175	671	setMostFrequentValue(n, mostFrequentValue);
176	671	setMostFrequentValueCount(n, mostFrequentValueCount);
177	671	return true;
178		}
179
180		TypeNode ArrayTableFunTypeRule::computeType(NodeManager* nodeManager,
181		TNode n,
182		bool check)
183		{
184		Assert(n.getKind() == kind::ARR_TABLE_FUN);
185		TypeNode arrayType = n[0].getType(check);
186		if (check)
187		{
188		if (!arrayType.isArray())
189		{
190		throw TypeCheckingExceptionPrivate(n,
191		"array table fun arg 0 is non-array");
192		}
193		TypeNode arrType2 = n[1].getType(check);
194		if (!arrayType.isArray())
195		{
196		throw TypeCheckingExceptionPrivate(n,
197		"array table fun arg 1 is non-array");
198		}
199		TypeNode indexType = n[2].getType(check);
200		if (!indexType.isComparableTo(arrayType.getArrayIndexType()))
201		{
202		throw TypeCheckingExceptionPrivate(
203		n, "array table fun arg 2 does not match type of array");
204		}
205		indexType = n[3].getType(check);
206		if (!indexType.isComparableTo(arrayType.getArrayIndexType()))
207		{
208		throw TypeCheckingExceptionPrivate(
209		n, "array table fun arg 3 does not match type of array");
210		}
211		}
212		return arrayType.getArrayIndexType();
213		}
214
215		TypeNode ArrayLambdaTypeRule::computeType(NodeManager* nodeManager,
216		TNode n,
217		bool check)
218		{
219		Assert(n.getKind() == kind::ARRAY_LAMBDA);
220		TypeNode lamType = n[0].getType(check);
221		if (check)
222		{
223		if (n[0].getKind() != kind::LAMBDA)
224		{
225		throw TypeCheckingExceptionPrivate(n, "array lambda arg is non-lambda");
226		}
227		}
228		if (lamType.getNumChildren() != 2)
229		{
230		throw TypeCheckingExceptionPrivate(n,
231		"array lambda arg is not unary lambda");
232		}
233		return nodeManager->mkArrayType(lamType[0], lamType[1]);
234		}
235
236	294	Cardinality ArraysProperties::computeCardinality(TypeNode type)
237		{
238	294	Assert(type.getKind() == kind::ARRAY_TYPE);
239
240	588	Cardinality indexCard = type[0].getCardinality();
241	588	Cardinality valueCard = type[1].getCardinality();
242
243	588	return valueCard ^ indexCard;
244		}
245
246		bool ArraysProperties::isWellFounded(TypeNode type)
247		{
248		return type[0].isWellFounded() && type[1].isWellFounded();
249		}
250
251	22	Node ArraysProperties::mkGroundTerm(TypeNode type)
252		{
253	22	Assert(type.getKind() == kind::ARRAY_TYPE);
254	44	TypeNode elemType = type.getArrayConstituentType();
255	44	Node elem = elemType.mkGroundTerm();
256	22	if (elem.isConst())
257		{
258	22	return NodeManager::currentNM()->mkConst(ArrayStoreAll(type, elem));
259		}
260		// Note the distinction between mkGroundTerm and mkGroundValue. While
261		// an arbitrary value can be obtained by calling the type enumerator here,
262		// that is wrong for types that are not closed enumerable since it may
263		// return a term containing values that should not appear in e.g. assertions.
264		// For example, arrays whose element type is an uninterpreted sort will
265		// incorrectly introduce uninterpreted sort values if this is done.
266		// It is currently infeasible to construct an ArrayStoreAll with the element
267		// type's mkGroundTerm as an argument when that term is not constant.
268		// Thus, we must simply return a fresh Skolem here, using the same utility
269		// as that of uninterpreted sorts.
270		return builtin::SortProperties::mkGroundTerm(type);
271		}
272
273		TypeNode ArrayPartialSelectTypeRule::computeType(NodeManager* nodeManager,
274		TNode n,
275		bool check)
276		{
277		Assert(n.getKind() == kind::PARTIAL_SELECT_0
278		\|\| n.getKind() == kind::PARTIAL_SELECT_1);
279		return nodeManager->integerType();
280		}
281
282	35	TypeNode ArrayEqRangeTypeRule::computeType(NodeManager* nodeManager,
283		TNode n,
284		bool check)
285		{
286	35	Assert(n.getKind() == kind::EQ_RANGE);
287	35	if (check)
288		{
289	70	TypeNode n0_type = n[0].getType(check);
290	70	TypeNode n1_type = n[1].getType(check);
291	35	if (!n0_type.isArray())
292		{
293		throw TypeCheckingExceptionPrivate(
294		n, "first operand of eqrange is not an array");
295		}
296	35	if (!n1_type.isArray())
297		{
298		throw TypeCheckingExceptionPrivate(
299		n, "second operand of eqrange is not an array");
300		}
301	35	if (n0_type != n1_type)
302		{
303		throw TypeCheckingExceptionPrivate(n, "array types do not match");
304		}
305	70	TypeNode indexType = n0_type.getArrayIndexType();
306	70	TypeNode indexRangeType1 = n[2].getType(check);
307	70	TypeNode indexRangeType2 = n[3].getType(check);
308	35	if (!indexRangeType1.isSubtypeOf(indexType))
309		{
310		throw TypeCheckingExceptionPrivate(
311		n, "eqrange lower index type does not match array index type");
312		}
313	35	if (!indexRangeType2.isSubtypeOf(indexType))
314		{
315		throw TypeCheckingExceptionPrivate(
316		n, "eqrange upper index type does not match array index type");
317		}
318	79	if (!indexType.isBitVector() && !indexType.isFloatingPoint()
319	44	&& !indexType.isInteger() && !indexType.isReal())
320		{
321		throw TypeCheckingExceptionPrivate(
322		n,
323		"eqrange only supports bit-vectors, floating-points, integers, and "
324		"reals as index type");
325		}
326		}
327	35	return nodeManager->booleanType();
328		}
329
330		} // namespace arrays
331		} // namespace theory
332	31137	} // namespace cvc5