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 |
2380205 |
int isTester(Node n, Node& a) |
97 |
|
{ |
98 |
2380205 |
if (n.getKind() == APPLY_TESTER) |
99 |
|
{ |
100 |
1219251 |
a = n[0]; |
101 |
1219251 |
return indexOf(n.getOperator()); |
102 |
|
} |
103 |
1160954 |
return -1; |
104 |
|
} |
105 |
|
|
106 |
111710 |
int isTester(Node n) |
107 |
|
{ |
108 |
111710 |
if (n.getKind() == APPLY_TESTER) |
109 |
|
{ |
110 |
111710 |
return indexOf(n.getOperator()); |
111 |
|
} |
112 |
|
return -1; |
113 |
|
} |
114 |
|
|
115 |
3437951 |
size_t indexOf(Node n) { return DType::indexOf(n); } |
116 |
|
|
117 |
4570 |
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 |
377495 |
bool checkClash(Node n1, Node n2, std::vector<Node>& rew) |
176 |
|
{ |
177 |
754990 |
Trace("datatypes-rewrite-debug") |
178 |
377495 |
<< "Check clash : " << n1 << " " << n2 << std::endl; |
179 |
377495 |
if (n1.getKind() == APPLY_CONSTRUCTOR && n2.getKind() == APPLY_CONSTRUCTOR) |
180 |
|
{ |
181 |
96452 |
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 |
93998 |
Assert(n1.getNumChildren() == n2.getNumChildren()); |
189 |
231820 |
for (unsigned i = 0, size = n1.getNumChildren(); i < size; i++) |
190 |
|
{ |
191 |
152249 |
if (checkClash(n1[i], n2[i], rew)) |
192 |
|
{ |
193 |
14427 |
return true; |
194 |
|
} |
195 |
|
} |
196 |
|
} |
197 |
281043 |
else if (n1 != n2) |
198 |
|
{ |
199 |
274167 |
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 |
547750 |
Node eq = NodeManager::currentNM()->mkNode(EQUAL, n1, n2); |
208 |
273875 |
rew.push_back(eq); |
209 |
|
} |
210 |
|
} |
211 |
360322 |
return false; |
212 |
|
} |
213 |
|
|
214 |
|
} // namespace utils |
215 |
|
} // namespace datatypes |
216 |
|
} // namespace theory |
217 |
29589 |
} // namespace cvc5 |