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-09-07	Branches:	173	656	26.4 %


/******************************************************************************
 * 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);
  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 "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	17807	TypeNode ArraySelectTypeRule::computeType(NodeManager* nodeManager,
29		TNode n,
30		bool check)
31		{
32	17807	Assert(n.getKind() == kind::SELECT);
33	35614	TypeNode arrayType = n[0].getType(check);
34	17807	if (check)
35		{
36	17807	if (!arrayType.isArray())
37		{
38		throw TypeCheckingExceptionPrivate(n,
39		"array select operating on non-array");
40		}
41	35614	TypeNode indexType = n[1].getType(check);
42	17807	if (!indexType.isSubtypeOf(arrayType.getArrayIndexType()))
43		{
44		throw TypeCheckingExceptionPrivate(
45		n, "array select not indexed with correct type for array");
46		}
47		}
48	35614	return arrayType.getArrayConstituentType();
49		}
50
51	11841	TypeNode ArrayStoreTypeRule::computeType(NodeManager* nodeManager,
52		TNode n,
53		bool check)
54		{
55	11841	if (n.getKind() == kind::STORE)
56		{
57	22332	TypeNode arrayType = n[0].getType(check);
58	11166	if (check)
59		{
60	11166	if (!arrayType.isArray())
61		{
62		throw TypeCheckingExceptionPrivate(
63		n, "array store operating on non-array");
64		}
65	22332	TypeNode indexType = n[1].getType(check);
66	22332	TypeNode valueType = n[2].getType(check);
67	11166	if (!indexType.isSubtypeOf(arrayType.getArrayIndexType()))
68		{
69		throw TypeCheckingExceptionPrivate(
70		n, "array store not indexed with correct type for array");
71		}
72	11166	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	11166	return arrayType;
83		}
84		else
85		{
86	675	Assert(n.getKind() == kind::STORE_ALL);
87	1350	ArrayStoreAll storeAll = n.getConst<ArrayStoreAll>();
88	675	return storeAll.getType();
89		}
90		}
91
92	8377	bool ArrayStoreTypeRule::computeIsConst(NodeManager* nodeManager, TNode n)
93		{
94	8377	Assert(n.getKind() == kind::STORE);
95	16754	NodeManagerScope nms(nodeManager);
96
97	16754	TNode store = n[0];
98	16754	TNode index = n[1];
99	16754	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	8377	if (!store.isConst() \|\| !index.isConst() \|\| !value.isConst())
104		{
105	4889	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	3488	if (store.getKind() == kind::STORE && (!(store[1] < index)))
111		{
112	15	return false;
113		}
114
115	3473	unsigned depth = 1;
116	3473	unsigned valCount = 1;
117	7357	while (store.getKind() == kind::STORE)
118		{
119	1942	depth += 1;
120	1942	if (store[2] == value)
121		{
122	249	valCount += 1;
123		}
124	1942	store = store[0];
125		}
126	3473	Assert(store.getKind() == kind::STORE_ALL);
127	6946	ArrayStoreAll storeAll = store.getConst<ArrayStoreAll>();
128	6946	Node defaultValue = storeAll.getValue();
129	3473	if (value == defaultValue)
130		{
131	15	return false;
132		}
133
134		// Get the cardinality of the index type
135	6916	Cardinality indexCard = index.getType().getCardinality();
136
137	3458	if (indexCard.isInfinite())
138		{
139	2879	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	1158	TNode mostFrequentValue;
148	579	unsigned mostFrequentValueCount = 0;
149	579	store = n[0];
150	579	if (store.getKind() == kind::STORE)
151		{
152	295	mostFrequentValue = getMostFrequentValue(store);
153	295	mostFrequentValueCount = getMostFrequentValueCount(store);
154		}
155
156		// Compute the most frequently written value for n
157	579	if (valCount > mostFrequentValueCount
158	579	\|\| (valCount == mostFrequentValueCount && value < mostFrequentValue))
159		{
160	402	mostFrequentValue = value;
161	402	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	579	indexCard.compare(mostFrequentValueCount + depth);
168	579	Assert(compare != Cardinality::UNKNOWN);
169	579	if (compare == Cardinality::LESS
170	583	\|\| (compare == Cardinality::EQUAL
171	152	&& (!(defaultValue < mostFrequentValue))))
172		{
173	4	return false;
174		}
175	575	setMostFrequentValue(n, mostFrequentValue);
176	575	setMostFrequentValueCount(n, mostFrequentValueCount);
177	575	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	15	Node ArraysProperties::mkGroundTerm(TypeNode type)
252		{
253	15	return *TypeEnumerator(type);
254		}
255
256		TypeNode ArrayPartialSelectTypeRule::computeType(NodeManager* nodeManager,
257		TNode n,
258		bool check)
259		{
260		Assert(n.getKind() == kind::PARTIAL_SELECT_0
261		\|\| n.getKind() == kind::PARTIAL_SELECT_1);
262		return nodeManager->integerType();
263		}
264
265	33	TypeNode ArrayEqRangeTypeRule::computeType(NodeManager* nodeManager,
266		TNode n,
267		bool check)
268		{
269	33	Assert(n.getKind() == kind::EQ_RANGE);
270	33	if (check)
271		{
272	66	TypeNode n0_type = n[0].getType(check);
273	66	TypeNode n1_type = n[1].getType(check);
274	33	if (!n0_type.isArray())
275		{
276		throw TypeCheckingExceptionPrivate(
277		n, "first operand of eqrange is not an array");
278		}
279	33	if (!n1_type.isArray())
280		{
281		throw TypeCheckingExceptionPrivate(
282		n, "second operand of eqrange is not an array");
283		}
284	33	if (n0_type != n1_type)
285		{
286		throw TypeCheckingExceptionPrivate(n, "array types do not match");
287		}
288	66	TypeNode indexType = n0_type.getArrayIndexType();
289	66	TypeNode indexRangeType1 = n[2].getType(check);
290	66	TypeNode indexRangeType2 = n[3].getType(check);
291	33	if (!indexRangeType1.isSubtypeOf(indexType))
292		{
293		throw TypeCheckingExceptionPrivate(
294		n, "eqrange lower index type does not match array index type");
295		}
296	33	if (!indexRangeType2.isSubtypeOf(indexType))
297		{
298		throw TypeCheckingExceptionPrivate(
299		n, "eqrange upper index type does not match array index type");
300		}
301	74	if (!indexType.isBitVector() && !indexType.isFloatingPoint()
302	41	&& !indexType.isInteger() && !indexType.isReal())
303		{
304		throw TypeCheckingExceptionPrivate(
305		n,
306		"eqrange only supports bit-vectors, floating-points, integers, and "
307		"reals as index type");
308		}
309		}
310	33	return nodeManager->booleanType();
311		}
312
313		} // namespace arrays
314		} // namespace theory
315	29502	} // namespace cvc5