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/dtype.h" |
19 |
|
#include "expr/dtype_cons.h" |
20 |
|
|
21 |
|
using namespace cvc5; |
22 |
|
using namespace cvc5::kind; |
23 |
|
|
24 |
|
namespace cvc5 { |
25 |
|
namespace theory { |
26 |
|
namespace datatypes { |
27 |
|
namespace utils { |
28 |
|
|
29 |
|
/** get instantiate cons */ |
30 |
113941 |
Node getInstCons(Node n, const DType& dt, int index) |
31 |
|
{ |
32 |
113941 |
Assert(index >= 0 && index < (int)dt.getNumConstructors()); |
33 |
227882 |
std::vector<Node> children; |
34 |
113941 |
NodeManager* nm = NodeManager::currentNM(); |
35 |
113941 |
children.push_back(dt[index].getConstructor()); |
36 |
227882 |
TypeNode tn = n.getType(); |
37 |
217540 |
for (unsigned i = 0, nargs = dt[index].getNumArgs(); i < nargs; i++) |
38 |
|
{ |
39 |
|
Node nc = nm->mkNode( |
40 |
207198 |
APPLY_SELECTOR_TOTAL, dt[index].getSelectorInternal(tn, i), n); |
41 |
103599 |
children.push_back(nc); |
42 |
|
} |
43 |
113941 |
Node n_ic = nm->mkNode(APPLY_CONSTRUCTOR, children); |
44 |
113941 |
if (dt.isParametric()) |
45 |
|
{ |
46 |
|
// add type ascription for ambiguous constructor types |
47 |
2009 |
if (!n_ic.getType().isComparableTo(tn)) |
48 |
|
{ |
49 |
12 |
Debug("datatypes-parametric") |
50 |
6 |
<< "DtInstantiate: ambiguous type for " << n_ic << ", ascribe to " |
51 |
6 |
<< n.getType() << std::endl; |
52 |
12 |
Debug("datatypes-parametric") |
53 |
6 |
<< "Constructor is " << dt[index] << std::endl; |
54 |
12 |
TypeNode tspec = dt[index].getSpecializedConstructorType(n.getType()); |
55 |
12 |
Debug("datatypes-parametric") |
56 |
6 |
<< "Type specification is " << tspec << std::endl; |
57 |
18 |
children[0] = nm->mkNode(APPLY_TYPE_ASCRIPTION, |
58 |
12 |
nm->mkConst(AscriptionType(tspec)), |
59 |
6 |
children[0]); |
60 |
6 |
n_ic = nm->mkNode(APPLY_CONSTRUCTOR, children); |
61 |
6 |
Assert(n_ic.getType() == tn); |
62 |
|
} |
63 |
|
} |
64 |
113941 |
Assert(isInstCons(n, n_ic, dt) == index); |
65 |
|
// n_ic = Rewriter::rewrite( n_ic ); |
66 |
227882 |
return n_ic; |
67 |
|
} |
68 |
|
|
69 |
113941 |
int isInstCons(Node t, Node n, const DType& dt) |
70 |
|
{ |
71 |
113941 |
if (n.getKind() == APPLY_CONSTRUCTOR) |
72 |
|
{ |
73 |
113941 |
int index = indexOf(n.getOperator()); |
74 |
113941 |
const DTypeConstructor& c = dt[index]; |
75 |
227882 |
TypeNode tn = n.getType(); |
76 |
217540 |
for (unsigned i = 0, size = n.getNumChildren(); i < size; i++) |
77 |
|
{ |
78 |
310797 |
if (n[i].getKind() != APPLY_SELECTOR_TOTAL |
79 |
310797 |
|| n[i].getOperator() != c.getSelectorInternal(tn, i) || n[i][0] != t) |
80 |
|
{ |
81 |
|
return -1; |
82 |
|
} |
83 |
|
} |
84 |
113941 |
return index; |
85 |
|
} |
86 |
|
return -1; |
87 |
|
} |
88 |
|
|
89 |
1998353 |
int isTester(Node n, Node& a) |
90 |
|
{ |
91 |
1998353 |
if (n.getKind() == APPLY_TESTER) |
92 |
|
{ |
93 |
900997 |
a = n[0]; |
94 |
900997 |
return indexOf(n.getOperator()); |
95 |
|
} |
96 |
1097356 |
return -1; |
97 |
|
} |
98 |
|
|
99 |
100931 |
int isTester(Node n) |
100 |
|
{ |
101 |
100931 |
if (n.getKind() == APPLY_TESTER) |
102 |
|
{ |
103 |
100931 |
return indexOf(n.getOperator()); |
104 |
|
} |
105 |
|
return -1; |
106 |
|
} |
107 |
|
|
108 |
2820051 |
size_t indexOf(Node n) { return DType::indexOf(n); } |
109 |
|
|
110 |
3895 |
size_t cindexOf(Node n) { return DType::cindexOf(n); } |
111 |
|
|
112 |
503617 |
const DType& datatypeOf(Node n) |
113 |
|
{ |
114 |
1007234 |
TypeNode t = n.getType(); |
115 |
503617 |
switch (t.getKind()) |
116 |
|
{ |
117 |
294002 |
case CONSTRUCTOR_TYPE: return t[t.getNumChildren() - 1].getDType(); |
118 |
209615 |
case SELECTOR_TYPE: |
119 |
|
case TESTER_TYPE: |
120 |
209615 |
case UPDATER_TYPE: return t[0].getDType(); |
121 |
|
default: |
122 |
|
Unhandled() << "arg must be a datatype constructor, selector, or tester"; |
123 |
|
} |
124 |
|
} |
125 |
|
|
126 |
191889 |
Node mkTester(Node n, int i, const DType& dt) |
127 |
|
{ |
128 |
191889 |
return NodeManager::currentNM()->mkNode(APPLY_TESTER, dt[i].getTester(), n); |
129 |
|
} |
130 |
|
|
131 |
2782 |
Node mkSplit(Node n, const DType& dt) |
132 |
|
{ |
133 |
5564 |
std::vector<Node> splits; |
134 |
12288 |
for (unsigned i = 0, ncons = dt.getNumConstructors(); i < ncons; i++) |
135 |
|
{ |
136 |
19012 |
Node test = mkTester(n, i, dt); |
137 |
9506 |
splits.push_back(test); |
138 |
|
} |
139 |
2782 |
NodeManager* nm = NodeManager::currentNM(); |
140 |
5564 |
return splits.size() == 1 ? splits[0] : nm->mkNode(OR, splits); |
141 |
|
} |
142 |
|
|
143 |
|
bool isNullaryApplyConstructor(Node n) |
144 |
|
{ |
145 |
|
Assert(n.getKind() == APPLY_CONSTRUCTOR); |
146 |
|
for (const Node& nc : n) |
147 |
|
{ |
148 |
|
if (nc.getType().isDatatype()) |
149 |
|
{ |
150 |
|
return false; |
151 |
|
} |
152 |
|
} |
153 |
|
return true; |
154 |
|
} |
155 |
|
|
156 |
|
bool isNullaryConstructor(const DTypeConstructor& c) |
157 |
|
{ |
158 |
|
for (unsigned j = 0, nargs = c.getNumArgs(); j < nargs; j++) |
159 |
|
{ |
160 |
|
if (c[j].getType().getRangeType().isDatatype()) |
161 |
|
{ |
162 |
|
return false; |
163 |
|
} |
164 |
|
} |
165 |
|
return true; |
166 |
|
} |
167 |
|
|
168 |
385981 |
bool checkClash(Node n1, Node n2, std::vector<Node>& rew) |
169 |
|
{ |
170 |
771962 |
Trace("datatypes-rewrite-debug") |
171 |
385981 |
<< "Check clash : " << n1 << " " << n2 << std::endl; |
172 |
385981 |
if (n1.getKind() == APPLY_CONSTRUCTOR && n2.getKind() == APPLY_CONSTRUCTOR) |
173 |
|
{ |
174 |
100755 |
if (n1.getOperator() != n2.getOperator()) |
175 |
|
{ |
176 |
8044 |
Trace("datatypes-rewrite-debug") |
177 |
8044 |
<< "Clash operators : " << n1 << " " << n2 << " " << n1.getOperator() |
178 |
4022 |
<< " " << n2.getOperator() << std::endl; |
179 |
4022 |
return true; |
180 |
|
} |
181 |
96733 |
Assert(n1.getNumChildren() == n2.getNumChildren()); |
182 |
236398 |
for (unsigned i = 0, size = n1.getNumChildren(); i < size; i++) |
183 |
|
{ |
184 |
154195 |
if (checkClash(n1[i], n2[i], rew)) |
185 |
|
{ |
186 |
14530 |
return true; |
187 |
|
} |
188 |
|
} |
189 |
|
} |
190 |
285226 |
else if (n1 != n2) |
191 |
|
{ |
192 |
281671 |
if (n1.isConst() && n2.isConst()) |
193 |
|
{ |
194 |
368 |
Trace("datatypes-rewrite-debug") |
195 |
184 |
<< "Clash constants : " << n1 << " " << n2 << std::endl; |
196 |
184 |
return true; |
197 |
|
} |
198 |
|
else |
199 |
|
{ |
200 |
562974 |
Node eq = NodeManager::currentNM()->mkNode(EQUAL, n1, n2); |
201 |
281487 |
rew.push_back(eq); |
202 |
|
} |
203 |
|
} |
204 |
367245 |
return false; |
205 |
|
} |
206 |
|
|
207 |
|
} // namespace utils |
208 |
|
} // namespace datatypes |
209 |
|
} // namespace theory |
210 |
28191 |
} // namespace cvc5 |