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 |
122027 |
Node getInstCons(Node n, const DType& dt, int index) |
32 |
|
{ |
33 |
122027 |
Assert(index >= 0 && index < (int)dt.getNumConstructors()); |
34 |
244054 |
std::vector<Node> children; |
35 |
122027 |
NodeManager* nm = NodeManager::currentNM(); |
36 |
122027 |
children.push_back(dt[index].getConstructor()); |
37 |
244054 |
TypeNode tn = n.getType(); |
38 |
231472 |
for (unsigned i = 0, nargs = dt[index].getNumArgs(); i < nargs; i++) |
39 |
|
{ |
40 |
|
Node nc = nm->mkNode( |
41 |
218890 |
APPLY_SELECTOR_TOTAL, dt[index].getSelectorInternal(tn, i), n); |
42 |
109445 |
children.push_back(nc); |
43 |
|
} |
44 |
122027 |
Node n_ic = nm->mkNode(APPLY_CONSTRUCTOR, children); |
45 |
122027 |
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 |
122027 |
Assert(isInstCons(n, n_ic, dt) == index); |
66 |
|
// n_ic = Rewriter::rewrite( n_ic ); |
67 |
244054 |
return n_ic; |
68 |
|
} |
69 |
|
|
70 |
122027 |
int isInstCons(Node t, Node n, const DType& dt) |
71 |
|
{ |
72 |
122027 |
if (n.getKind() == APPLY_CONSTRUCTOR) |
73 |
|
{ |
74 |
122027 |
int index = indexOf(n.getOperator()); |
75 |
122027 |
const DTypeConstructor& c = dt[index]; |
76 |
244054 |
TypeNode tn = n.getType(); |
77 |
231472 |
for (unsigned i = 0, size = n.getNumChildren(); i < size; i++) |
78 |
|
{ |
79 |
328335 |
if (n[i].getKind() != APPLY_SELECTOR_TOTAL |
80 |
328335 |
|| n[i].getOperator() != c.getSelectorInternal(tn, i) || n[i][0] != t) |
81 |
|
{ |
82 |
|
return -1; |
83 |
|
} |
84 |
|
} |
85 |
122027 |
return index; |
86 |
|
} |
87 |
|
return -1; |
88 |
|
} |
89 |
|
|
90 |
1767163 |
int isTester(Node n, Node& a) |
91 |
|
{ |
92 |
1767163 |
if (n.getKind() == APPLY_TESTER) |
93 |
|
{ |
94 |
765075 |
a = n[0]; |
95 |
765075 |
return indexOf(n.getOperator()); |
96 |
|
} |
97 |
1002088 |
return -1; |
98 |
|
} |
99 |
|
|
100 |
108091 |
int isTester(Node n) |
101 |
|
{ |
102 |
108091 |
if (n.getKind() == APPLY_TESTER) |
103 |
|
{ |
104 |
108091 |
return indexOf(n.getOperator()); |
105 |
|
} |
106 |
|
return -1; |
107 |
|
} |
108 |
|
|
109 |
2586443 |
size_t indexOf(Node n) { return DType::indexOf(n); } |
110 |
|
|
111 |
4764 |
size_t cindexOf(Node n) { return DType::cindexOf(n); } |
112 |
|
|
113 |
501134 |
const DType& datatypeOf(Node n) |
114 |
|
{ |
115 |
1002268 |
TypeNode t = n.getType(); |
116 |
501134 |
switch (t.getKind()) |
117 |
|
{ |
118 |
297751 |
case CONSTRUCTOR_TYPE: return t[t.getNumChildren() - 1].getDType(); |
119 |
203383 |
case SELECTOR_TYPE: |
120 |
|
case TESTER_TYPE: |
121 |
203383 |
case UPDATER_TYPE: return t[0].getDType(); |
122 |
|
default: |
123 |
|
Unhandled() << "arg must be a datatype constructor, selector, or tester"; |
124 |
|
} |
125 |
|
} |
126 |
|
|
127 |
212458 |
Node mkTester(Node n, int i, const DType& dt) |
128 |
|
{ |
129 |
212458 |
return NodeManager::currentNM()->mkNode(APPLY_TESTER, dt[i].getTester(), n); |
130 |
|
} |
131 |
|
|
132 |
3651 |
Node mkSplit(Node n, const DType& dt) |
133 |
|
{ |
134 |
7302 |
std::vector<Node> splits; |
135 |
14742 |
for (unsigned i = 0, ncons = dt.getNumConstructors(); i < ncons; i++) |
136 |
|
{ |
137 |
22182 |
Node test = mkTester(n, i, dt); |
138 |
11091 |
splits.push_back(test); |
139 |
|
} |
140 |
3651 |
NodeManager* nm = NodeManager::currentNM(); |
141 |
7302 |
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 |
397573 |
bool checkClash(Node n1, Node n2, std::vector<Node>& rew) |
170 |
|
{ |
171 |
795146 |
Trace("datatypes-rewrite-debug") |
172 |
397573 |
<< "Check clash : " << n1 << " " << n2 << std::endl; |
173 |
397573 |
if (n1.getKind() == APPLY_CONSTRUCTOR && n2.getKind() == APPLY_CONSTRUCTOR) |
174 |
|
{ |
175 |
103792 |
if (n1.getOperator() != n2.getOperator()) |
176 |
|
{ |
177 |
5254 |
Trace("datatypes-rewrite-debug") |
178 |
5254 |
<< "Clash operators : " << n1 << " " << n2 << " " << n1.getOperator() |
179 |
2627 |
<< " " << n2.getOperator() << std::endl; |
180 |
2627 |
return true; |
181 |
|
} |
182 |
101165 |
Assert(n1.getNumChildren() == n2.getNumChildren()); |
183 |
251540 |
for (unsigned i = 0, size = n1.getNumChildren(); i < size; i++) |
184 |
|
{ |
185 |
164810 |
if (checkClash(n1[i], n2[i], rew)) |
186 |
|
{ |
187 |
14435 |
return true; |
188 |
|
} |
189 |
|
} |
190 |
|
} |
191 |
293781 |
else if (n1 != n2) |
192 |
|
{ |
193 |
286755 |
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 |
572920 |
Node eq = NodeManager::currentNM()->mkNode(EQUAL, n1, n2); |
202 |
286460 |
rew.push_back(eq); |
203 |
|
} |
204 |
|
} |
205 |
380216 |
return false; |
206 |
|
} |
207 |
|
|
208 |
|
} // namespace utils |
209 |
|
} // namespace datatypes |
210 |
|
} // namespace theory |
211 |
29340 |
} // namespace cvc5 |