Head

GCC Code Coverage Report

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