Head

GCC Code Coverage Report

Directory:	.		Exec	Total	Coverage
File:	src/theory/datatypes/theory_datatypes_utils.cpp	Lines:	86	102	84.3 %
Date:	2021-09-15	Branches:	186	485	38.4 %


/******************************************************************************
 * 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, size_t index)
{
  Assert(index < dt.getNumConstructors());
  std::vector<Node> children;
  NodeManager* nm = NodeManager::currentNM();
  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 = mkApplyCons(tn, dt, index, children);
  Assert(n_ic.getType() == tn);
  Assert(static_cast<size_t>(isInstCons(n, n_ic, dt)) == index);
  return n_ic;
}

Node mkApplyCons(TypeNode tn,
                 const DType& dt,
                 size_t index,
                 const std::vector<Node>& children)
{
  Assert(tn.isDatatype());
  Assert(index < dt.getNumConstructors());
  Assert(dt[index].getNumArgs() == children.size());
  NodeManager* nm = NodeManager::currentNM();
  std::vector<Node> cchildren;
  cchildren.push_back(dt[index].getConstructor());
  cchildren.insert(cchildren.end(), children.begin(), children.end());
  if (dt.isParametric())
  {
    // add type ascription for ambiguous constructor types
    Debug("datatypes-parametric")
        << "Constructor is " << dt[index] << std::endl;
    TypeNode tspec = dt[index].getSpecializedConstructorType(tn);
    Debug("datatypes-parametric")
        << "Type specification is " << tspec << std::endl;
    cchildren[0] = nm->mkNode(APPLY_TYPE_ASCRIPTION,
                              nm->mkConst(AscriptionType(tspec)),
                              cchildren[0]);
  }
  return nm->mkNode(APPLY_CONSTRUCTOR, cchildren);
}

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	120544	Node getInstCons(Node n, const DType& dt, size_t index)
32		{
33	120544	Assert(index < dt.getNumConstructors());
34	241088	std::vector<Node> children;
35	120544	NodeManager* nm = NodeManager::currentNM();
36	241088	TypeNode tn = n.getType();
37	219864	for (unsigned i = 0, nargs = dt[index].getNumArgs(); i < nargs; i++)
38		{
39		Node nc = nm->mkNode(
40	198640	APPLY_SELECTOR_TOTAL, dt[index].getSelectorInternal(tn, i), n);
41	99320	children.push_back(nc);
42		}
43	120544	Node n_ic = mkApplyCons(tn, dt, index, children);
44	120544	Assert(n_ic.getType() == tn);
45	120544	Assert(static_cast<size_t>(isInstCons(n, n_ic, dt)) == index);
46	241088	return n_ic;
47		}
48
49	123013	Node mkApplyCons(TypeNode tn,
50		const DType& dt,
51		size_t index,
52		const std::vector<Node>& children)
53		{
54	123013	Assert(tn.isDatatype());
55	123013	Assert(index < dt.getNumConstructors());
56	123013	Assert(dt[index].getNumArgs() == children.size());
57	123013	NodeManager* nm = NodeManager::currentNM();
58	246026	std::vector<Node> cchildren;
59	123013	cchildren.push_back(dt[index].getConstructor());
60	123013	cchildren.insert(cchildren.end(), children.begin(), children.end());
61	123013	if (dt.isParametric())
62		{
63		// add type ascription for ambiguous constructor types
64	3448	Debug("datatypes-parametric")
65	1724	<< "Constructor is " << dt[index] << std::endl;
66	3448	TypeNode tspec = dt[index].getSpecializedConstructorType(tn);
67	3448	Debug("datatypes-parametric")
68	1724	<< "Type specification is " << tspec << std::endl;
69	5172	cchildren[0] = nm->mkNode(APPLY_TYPE_ASCRIPTION,
70	3448	nm->mkConst(AscriptionType(tspec)),
71	1724	cchildren[0]);
72		}
73	246026	return nm->mkNode(APPLY_CONSTRUCTOR, cchildren);
74		}
75
76	120544	int isInstCons(Node t, Node n, const DType& dt)
77		{
78	120544	if (n.getKind() == APPLY_CONSTRUCTOR)
79		{
80	120544	int index = indexOf(n.getOperator());
81	120544	const DTypeConstructor& c = dt[index];
82	241088	TypeNode tn = n.getType();
83	219864	for (unsigned i = 0, size = n.getNumChildren(); i < size; i++)
84		{
85	297960	if (n[i].getKind() != APPLY_SELECTOR_TOTAL
86	297960	\|\| n[i].getOperator() != c.getSelectorInternal(tn, i) \|\| n[i][0] != t)
87		{
88		return -1;
89		}
90		}
91	120544	return index;
92		}
93		return -1;
94		}
95
96	2380305	int isTester(Node n, Node& a)
97		{
98	2380305	if (n.getKind() == APPLY_TESTER)
99		{
100	1219279	a = n[0];
101	1219279	return indexOf(n.getOperator());
102		}
103	1161026	return -1;
104		}
105
106	111714	int isTester(Node n)
107		{
108	111714	if (n.getKind() == APPLY_TESTER)
109		{
110	111714	return indexOf(n.getOperator());
111		}
112		return -1;
113		}
114
115	3438007	size_t indexOf(Node n) { return DType::indexOf(n); }
116
117	4574	size_t cindexOf(Node n) { return DType::cindexOf(n); }
118
119	523795	const DType& datatypeOf(Node n)
120		{
121	1047590	TypeNode t = n.getType();
122	523795	switch (t.getKind())
123		{
124	293202	case CONSTRUCTOR_TYPE: return t[t.getNumChildren() - 1].getDType();
125	230593	case SELECTOR_TYPE:
126		case TESTER_TYPE:
127	230593	case UPDATER_TYPE: return t[0].getDType();
128		default:
129		Unhandled() << "arg must be a datatype constructor, selector, or tester";
130		}
131		}
132
133	185607	Node mkTester(Node n, int i, const DType& dt)
134		{
135	185607	return NodeManager::currentNM()->mkNode(APPLY_TESTER, dt[i].getTester(), n);
136		}
137
138	2859	Node mkSplit(Node n, const DType& dt)
139		{
140	5718	std::vector<Node> splits;
141	13404	for (unsigned i = 0, ncons = dt.getNumConstructors(); i < ncons; i++)
142		{
143	21090	Node test = mkTester(n, i, dt);
144	10545	splits.push_back(test);
145		}
146	2859	NodeManager* nm = NodeManager::currentNM();
147	5718	return splits.size() == 1 ? splits[0] : nm->mkNode(OR, splits);
148		}
149
150		bool isNullaryApplyConstructor(Node n)
151		{
152		Assert(n.getKind() == APPLY_CONSTRUCTOR);
153		for (const Node& nc : n)
154		{
155		if (nc.getType().isDatatype())
156		{
157		return false;
158		}
159		}
160		return true;
161		}
162
163		bool isNullaryConstructor(const DTypeConstructor& c)
164		{
165		for (unsigned j = 0, nargs = c.getNumArgs(); j < nargs; j++)
166		{
167		if (c[j].getType().getRangeType().isDatatype())
168		{
169		return false;
170		}
171		}
172		return true;
173		}
174
175	377513	bool checkClash(Node n1, Node n2, std::vector<Node>& rew)
176		{
177	755026	Trace("datatypes-rewrite-debug")
178	377513	<< "Check clash : " << n1 << " " << n2 << std::endl;
179	377513	if (n1.getKind() == APPLY_CONSTRUCTOR && n2.getKind() == APPLY_CONSTRUCTOR)
180		{
181	96450	if (n1.getOperator() != n2.getOperator())
182		{
183	4908	Trace("datatypes-rewrite-debug")
184	4908	<< "Clash operators : " << n1 << " " << n2 << " " << n1.getOperator()
185	2454	<< " " << n2.getOperator() << std::endl;
186	2454	return true;
187		}
188	93996	Assert(n1.getNumChildren() == n2.getNumChildren());
189	231814	for (unsigned i = 0, size = n1.getNumChildren(); i < size; i++)
190		{
191	152245	if (checkClash(n1[i], n2[i], rew))
192		{
193	14427	return true;
194		}
195		}
196		}
197	281063	else if (n1 != n2)
198		{
199	274191	if (n1.isConst() && n2.isConst())
200		{
201	584	Trace("datatypes-rewrite-debug")
202	292	<< "Clash constants : " << n1 << " " << n2 << std::endl;
203	292	return true;
204		}
205		else
206		{
207	547798	Node eq = NodeManager::currentNM()->mkNode(EQUAL, n1, n2);
208	273899	rew.push_back(eq);
209		}
210		}
211	360340	return false;
212		}
213
214		} // namespace utils
215		} // namespace datatypes
216		} // namespace theory
217	29577	} // namespace cvc5