Head

GCC Code Coverage Report

Directory:	.		Exec	Total	Coverage
File:	src/theory/datatypes/theory_datatypes_utils.cpp	Lines:	83	99	83.8 %
Date:	2021-08-01	Branches:	188	453	41.5 %


/******************************************************************************
 * Top contributors (to current version):
 *   Andrew Reynolds, Aina Niemetz, Morgan Deters
 *
 * 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.
 * ****************************************************************************
 *
 * Implementation of rewriter for the theory of (co)inductive datatypes.
 */

#include "theory/datatypes/theory_datatypes_utils.h"

#include "expr/ascription_type.h"
#include "expr/dtype.h"
#include "expr/dtype_cons.h"

using namespace cvc5;
using namespace cvc5::kind;

namespace cvc5 {
namespace theory {
namespace datatypes {
namespace utils {

/** get instantiate cons */
Node getInstCons(Node n, const DType& dt, int index)
{
  Assert(index >= 0 && index < (int)dt.getNumConstructors());
  std::vector<Node> children;
  NodeManager* nm = NodeManager::currentNM();
  children.push_back(dt[index].getConstructor());
  TypeNode tn = n.getType();
  for (unsigned i = 0, nargs = dt[index].getNumArgs(); i < nargs; i++)
  {
    Node nc = nm->mkNode(
        APPLY_SELECTOR_TOTAL, dt[index].getSelectorInternal(tn, i), n);
    children.push_back(nc);
  }
  Node n_ic = nm->mkNode(APPLY_CONSTRUCTOR, children);
  if (dt.isParametric())
  {
    // add type ascription for ambiguous constructor types
    if (!n_ic.getType().isComparableTo(tn))
    {
      Debug("datatypes-parametric")
          << "DtInstantiate: ambiguous type for " << n_ic << ", ascribe to "
          << n.getType() << std::endl;
      Debug("datatypes-parametric")
          << "Constructor is " << dt[index] << std::endl;
      TypeNode tspec = dt[index].getSpecializedConstructorType(n.getType());
      Debug("datatypes-parametric")
          << "Type specification is " << tspec << std::endl;
      children[0] = nm->mkNode(APPLY_TYPE_ASCRIPTION,
                               nm->mkConst(AscriptionType(tspec)),
                               children[0]);
      n_ic = nm->mkNode(APPLY_CONSTRUCTOR, children);
      Assert(n_ic.getType() == tn);
    }
  }
  Assert(isInstCons(n, n_ic, dt) == index);
  // n_ic = Rewriter::rewrite( n_ic );
  return n_ic;
}

int isInstCons(Node t, Node n, const DType& dt)
{
  if (n.getKind() == APPLY_CONSTRUCTOR)
  {
    int index = indexOf(n.getOperator());
    const DTypeConstructor& c = dt[index];
    TypeNode tn = n.getType();
    for (unsigned i = 0, size = n.getNumChildren(); i < size; i++)
    {
      if (n[i].getKind() != APPLY_SELECTOR_TOTAL
          || n[i].getOperator() != c.getSelectorInternal(tn, i) || n[i][0] != t)
      {
        return -1;
      }
    }
    return index;
  }
  return -1;
}

int isTester(Node n, Node& a)
{
  if (n.getKind() == APPLY_TESTER)
  {
    a = n[0];
    return indexOf(n.getOperator());
  }
  return -1;
}

int isTester(Node n)
{
  if (n.getKind() == APPLY_TESTER)
  {
    return indexOf(n.getOperator());
  }
  return -1;
}

size_t indexOf(Node n) { return DType::indexOf(n); }

size_t cindexOf(Node n) { return DType::cindexOf(n); }

const DType& datatypeOf(Node n)
{
  TypeNode t = n.getType();
  switch (t.getKind())
  {
    case CONSTRUCTOR_TYPE: return t[t.getNumChildren() - 1].getDType();
    case SELECTOR_TYPE:
    case TESTER_TYPE:
    case UPDATER_TYPE: return t[0].getDType();
    default:
      Unhandled() << "arg must be a datatype constructor, selector, or tester";
  }
}

Node mkTester(Node n, int i, const DType& dt)
{
  return NodeManager::currentNM()->mkNode(APPLY_TESTER, dt[i].getTester(), n);
}

Node mkSplit(Node n, const DType& dt)
{
  std::vector<Node> splits;
  for (unsigned i = 0, ncons = dt.getNumConstructors(); i < ncons; i++)
  {
    Node test = mkTester(n, i, dt);
    splits.push_back(test);
  }
  NodeManager* nm = NodeManager::currentNM();
  return splits.size() == 1 ? splits[0] : nm->mkNode(OR, splits);
}

bool isNullaryApplyConstructor(Node n)
{
  Assert(n.getKind() == APPLY_CONSTRUCTOR);
  for (const Node& nc : n)
  {
    if (nc.getType().isDatatype())
    {
      return false;
    }
  }
  return true;
}

bool isNullaryConstructor(const DTypeConstructor& c)
{
  for (unsigned j = 0, nargs = c.getNumArgs(); j < nargs; j++)
  {
    if (c[j].getType().getRangeType().isDatatype())
    {
      return false;
    }
  }
  return true;
}

bool checkClash(Node n1, Node n2, std::vector<Node>& rew)
{
  Trace("datatypes-rewrite-debug")
      << "Check clash : " << n1 << " " << n2 << std::endl;
  if (n1.getKind() == APPLY_CONSTRUCTOR && n2.getKind() == APPLY_CONSTRUCTOR)
  {
    if (n1.getOperator() != n2.getOperator())
    {
      Trace("datatypes-rewrite-debug")
          << "Clash operators : " << n1 << " " << n2 << " " << n1.getOperator()
          << " " << n2.getOperator() << std::endl;
      return true;
    }
    Assert(n1.getNumChildren() == n2.getNumChildren());
    for (unsigned i = 0, size = n1.getNumChildren(); i < size; i++)
    {
      if (checkClash(n1[i], n2[i], rew))
      {
        return true;
      }
    }
  }
  else if (n1 != n2)
  {
    if (n1.isConst() && n2.isConst())
    {
      Trace("datatypes-rewrite-debug")
          << "Clash constants : " << n1 << " " << n2 << std::endl;
      return true;
    }
    else
    {
      Node eq = NodeManager::currentNM()->mkNode(EQUAL, n1, n2);
      rew.push_back(eq);
    }
  }
  return false;
}

}  // namespace utils
}  // namespace datatypes
}  // 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, Morgan Deters
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		* Implementation of rewriter for the theory of (co)inductive datatypes.
14		*/
15
16		#include "theory/datatypes/theory_datatypes_utils.h"
17
18		#include "expr/ascription_type.h"
19		#include "expr/dtype.h"
20		#include "expr/dtype_cons.h"
21
22		using namespace cvc5;
23		using namespace cvc5::kind;
24
25		namespace cvc5 {
26		namespace theory {
27		namespace datatypes {
28		namespace utils {
29
30		/** get instantiate cons */
31	122774	Node getInstCons(Node n, const DType& dt, int index)
32		{
33	122774	Assert(index >= 0 && index < (int)dt.getNumConstructors());
34	245548	std::vector<Node> children;
35	122774	NodeManager* nm = NodeManager::currentNM();
36	122774	children.push_back(dt[index].getConstructor());
37	245548	TypeNode tn = n.getType();
38	233528	for (unsigned i = 0, nargs = dt[index].getNumArgs(); i < nargs; i++)
39		{
40		Node nc = nm->mkNode(
41	221508	APPLY_SELECTOR_TOTAL, dt[index].getSelectorInternal(tn, i), n);
42	110754	children.push_back(nc);
43		}
44	122774	Node n_ic = nm->mkNode(APPLY_CONSTRUCTOR, children);
45	122774	if (dt.isParametric())
46		{
47		// add type ascription for ambiguous constructor types
48	1714	if (!n_ic.getType().isComparableTo(tn))
49		{
50	12	Debug("datatypes-parametric")
51	6	<< "DtInstantiate: ambiguous type for " << n_ic << ", ascribe to "
52	6	<< n.getType() << std::endl;
53	12	Debug("datatypes-parametric")
54	6	<< "Constructor is " << dt[index] << std::endl;
55	12	TypeNode tspec = dt[index].getSpecializedConstructorType(n.getType());
56	12	Debug("datatypes-parametric")
57	6	<< "Type specification is " << tspec << std::endl;
58	18	children[0] = nm->mkNode(APPLY_TYPE_ASCRIPTION,
59	12	nm->mkConst(AscriptionType(tspec)),
60	6	children[0]);
61	6	n_ic = nm->mkNode(APPLY_CONSTRUCTOR, children);
62	6	Assert(n_ic.getType() == tn);
63		}
64		}
65	122774	Assert(isInstCons(n, n_ic, dt) == index);
66		// n_ic = Rewriter::rewrite( n_ic );
67	245548	return n_ic;
68		}
69
70	122774	int isInstCons(Node t, Node n, const DType& dt)
71		{
72	122774	if (n.getKind() == APPLY_CONSTRUCTOR)
73		{
74	122774	int index = indexOf(n.getOperator());
75	122774	const DTypeConstructor& c = dt[index];
76	245548	TypeNode tn = n.getType();
77	233528	for (unsigned i = 0, size = n.getNumChildren(); i < size; i++)
78		{
79	332262	if (n[i].getKind() != APPLY_SELECTOR_TOTAL
80	332262	\|\| n[i].getOperator() != c.getSelectorInternal(tn, i) \|\| n[i][0] != t)
81		{
82		return -1;
83		}
84		}
85	122774	return index;
86		}
87		return -1;
88		}
89
90	1787205	int isTester(Node n, Node& a)
91		{
92	1787205	if (n.getKind() == APPLY_TESTER)
93		{
94	766404	a = n[0];
95	766404	return indexOf(n.getOperator());
96		}
97	1020801	return -1;
98		}
99
100	108371	int isTester(Node n)
101		{
102	108371	if (n.getKind() == APPLY_TESTER)
103		{
104	108371	return indexOf(n.getOperator());
105		}
106		return -1;
107		}
108
109	2592786	size_t indexOf(Node n) { return DType::indexOf(n); }
110
111	4836	size_t cindexOf(Node n) { return DType::cindexOf(n); }
112
113	502751	const DType& datatypeOf(Node n)
114		{
115	1005502	TypeNode t = n.getType();
116	502751	switch (t.getKind())
117		{
118	297746	case CONSTRUCTOR_TYPE: return t[t.getNumChildren() - 1].getDType();
119	205005	case SELECTOR_TYPE:
120		case TESTER_TYPE:
121	205005	case UPDATER_TYPE: return t[0].getDType();
122		default:
123		Unhandled() << "arg must be a datatype constructor, selector, or tester";
124		}
125		}
126
127	211835	Node mkTester(Node n, int i, const DType& dt)
128		{
129	211835	return NodeManager::currentNM()->mkNode(APPLY_TESTER, dt[i].getTester(), n);
130		}
131
132	3413	Node mkSplit(Node n, const DType& dt)
133		{
134	6826	std::vector<Node> splits;
135	14009	for (unsigned i = 0, ncons = dt.getNumConstructors(); i < ncons; i++)
136		{
137	21192	Node test = mkTester(n, i, dt);
138	10596	splits.push_back(test);
139		}
140	3413	NodeManager* nm = NodeManager::currentNM();
141	6826	return splits.size() == 1 ? splits[0] : nm->mkNode(OR, splits);
142		}
143
144		bool isNullaryApplyConstructor(Node n)
145		{
146		Assert(n.getKind() == APPLY_CONSTRUCTOR);
147		for (const Node& nc : n)
148		{
149		if (nc.getType().isDatatype())
150		{
151		return false;
152		}
153		}
154		return true;
155		}
156
157		bool isNullaryConstructor(const DTypeConstructor& c)
158		{
159		for (unsigned j = 0, nargs = c.getNumArgs(); j < nargs; j++)
160		{
161		if (c[j].getType().getRangeType().isDatatype())
162		{
163		return false;
164		}
165		}
166		return true;
167		}
168
169	404334	bool checkClash(Node n1, Node n2, std::vector<Node>& rew)
170		{
171	808668	Trace("datatypes-rewrite-debug")
172	404334	<< "Check clash : " << n1 << " " << n2 << std::endl;
173	404334	if (n1.getKind() == APPLY_CONSTRUCTOR && n2.getKind() == APPLY_CONSTRUCTOR)
174		{
175	104514	if (n1.getOperator() != n2.getOperator())
176		{
177	5148	Trace("datatypes-rewrite-debug")
178	5148	<< "Clash operators : " << n1 << " " << n2 << " " << n1.getOperator()
179	2574	<< " " << n2.getOperator() << std::endl;
180	2574	return true;
181		}
182	101940	Assert(n1.getNumChildren() == n2.getNumChildren());
183	253691	for (unsigned i = 0, size = n1.getNumChildren(); i < size; i++)
184		{
185	166186	if (checkClash(n1[i], n2[i], rew))
186		{
187	14435	return true;
188		}
189		}
190		}
191	299820	else if (n1 != n2)
192		{
193	292642	if (n1.isConst() && n2.isConst())
194		{
195	590	Trace("datatypes-rewrite-debug")
196	295	<< "Clash constants : " << n1 << " " << n2 << std::endl;
197	295	return true;
198		}
199		else
200		{
201	584694	Node eq = NodeManager::currentNM()->mkNode(EQUAL, n1, n2);
202	292347	rew.push_back(eq);
203		}
204		}
205	387030	return false;
206		}
207
208		} // namespace utils
209		} // namespace datatypes
210		} // namespace theory
211	29280	} // namespace cvc5