1 |
|
/****************************************************************************** |
2 |
|
* Top contributors (to current version): |
3 |
|
* Andrew Reynolds |
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 |
|
* Theory UF rewriter |
14 |
|
*/ |
15 |
|
|
16 |
|
#include "theory/uf/theory_uf_rewriter.h" |
17 |
|
|
18 |
|
#include "expr/node_algorithm.h" |
19 |
|
#include "theory/rewriter.h" |
20 |
|
#include "theory/substitutions.h" |
21 |
|
|
22 |
|
namespace cvc5 { |
23 |
|
namespace theory { |
24 |
|
namespace uf { |
25 |
|
|
26 |
6271 |
TheoryUfRewriter::TheoryUfRewriter(bool isHigherOrder) |
27 |
6271 |
: d_isHigherOrder(isHigherOrder) |
28 |
|
{ |
29 |
6271 |
} |
30 |
|
|
31 |
401968 |
RewriteResponse TheoryUfRewriter::postRewrite(TNode node) |
32 |
|
{ |
33 |
401968 |
if (node.getKind() == kind::EQUAL) |
34 |
|
{ |
35 |
78328 |
if (node[0] == node[1]) |
36 |
|
{ |
37 |
|
return RewriteResponse(REWRITE_DONE, |
38 |
34 |
NodeManager::currentNM()->mkConst(true)); |
39 |
|
} |
40 |
78294 |
else if (node[0].isConst() && node[1].isConst()) |
41 |
|
{ |
42 |
|
// uninterpreted constants are all distinct |
43 |
|
return RewriteResponse(REWRITE_DONE, |
44 |
30 |
NodeManager::currentNM()->mkConst(false)); |
45 |
|
} |
46 |
78264 |
if (node[0] > node[1]) |
47 |
|
{ |
48 |
|
Node newNode = |
49 |
31934 |
NodeManager::currentNM()->mkNode(node.getKind(), node[1], node[0]); |
50 |
15967 |
return RewriteResponse(REWRITE_DONE, newNode); |
51 |
|
} |
52 |
|
} |
53 |
385937 |
if (node.getKind() == kind::APPLY_UF) |
54 |
|
{ |
55 |
302277 |
if (node.getOperator().getKind() == kind::LAMBDA) |
56 |
|
{ |
57 |
19482 |
Trace("uf-ho-beta") << "uf-ho-beta : beta-reducing all args of : " << node |
58 |
9741 |
<< "\n"; |
59 |
19482 |
TNode lambda = node.getOperator(); |
60 |
19482 |
Node ret; |
61 |
|
// build capture-avoiding substitution since in HOL shadowing may have |
62 |
|
// been introduced |
63 |
9741 |
if (d_isHigherOrder) |
64 |
|
{ |
65 |
376 |
std::vector<Node> vars; |
66 |
376 |
std::vector<Node> subs; |
67 |
550 |
for (const Node& v : lambda[0]) |
68 |
|
{ |
69 |
362 |
vars.push_back(v); |
70 |
|
} |
71 |
550 |
for (const Node& s : node) |
72 |
|
{ |
73 |
362 |
subs.push_back(s); |
74 |
|
} |
75 |
188 |
if (Trace.isOn("uf-ho-beta")) |
76 |
|
{ |
77 |
|
Trace("uf-ho-beta") << "uf-ho-beta: ..sub of " << subs.size() |
78 |
|
<< " vars into " << subs.size() << " terms :\n"; |
79 |
|
for (unsigned i = 0, size = subs.size(); i < size; ++i) |
80 |
|
{ |
81 |
|
Trace("uf-ho-beta") |
82 |
|
<< "uf-ho-beta: .... " << vars[i] << " |-> " << subs[i] << "\n"; |
83 |
|
} |
84 |
|
} |
85 |
188 |
ret = expr::substituteCaptureAvoiding(lambda[1], vars, subs); |
86 |
188 |
Trace("uf-ho-beta") << "uf-ho-beta : ..result : " << ret << "\n"; |
87 |
|
} |
88 |
|
else |
89 |
|
{ |
90 |
19106 |
std::vector<TNode> vars(lambda[0].begin(), lambda[0].end()); |
91 |
19106 |
std::vector<TNode> subs(node.begin(), node.end()); |
92 |
9553 |
ret = lambda[1].substitute( |
93 |
|
vars.begin(), vars.end(), subs.begin(), subs.end()); |
94 |
|
} |
95 |
9741 |
return RewriteResponse(REWRITE_AGAIN_FULL, ret); |
96 |
|
} |
97 |
292536 |
else if (!canUseAsApplyUfOperator(node.getOperator())) |
98 |
|
{ |
99 |
22 |
return RewriteResponse(REWRITE_AGAIN_FULL, getHoApplyForApplyUf(node)); |
100 |
|
} |
101 |
|
} |
102 |
83660 |
else if (node.getKind() == kind::HO_APPLY) |
103 |
|
{ |
104 |
17773 |
if (node[0].getKind() == kind::LAMBDA) |
105 |
|
{ |
106 |
|
// resolve one argument of the lambda |
107 |
278 |
Trace("uf-ho-beta") << "uf-ho-beta : beta-reducing one argument of : " |
108 |
139 |
<< node[0] << " with " << node[1] << "\n"; |
109 |
|
|
110 |
|
// reconstruct the lambda first to avoid variable shadowing |
111 |
278 |
Node new_body = node[0][1]; |
112 |
139 |
if (node[0][0].getNumChildren() > 1) |
113 |
|
{ |
114 |
172 |
std::vector<Node> new_vars(node[0][0].begin() + 1, node[0][0].end()); |
115 |
172 |
std::vector<Node> largs; |
116 |
86 |
largs.push_back( |
117 |
172 |
NodeManager::currentNM()->mkNode(kind::BOUND_VAR_LIST, new_vars)); |
118 |
86 |
largs.push_back(new_body); |
119 |
86 |
new_body = NodeManager::currentNM()->mkNode(kind::LAMBDA, largs); |
120 |
172 |
Trace("uf-ho-beta") |
121 |
86 |
<< "uf-ho-beta : ....new lambda : " << new_body << "\n"; |
122 |
|
} |
123 |
|
|
124 |
|
// build capture-avoiding substitution since in HOL shadowing may have |
125 |
|
// been introduced |
126 |
139 |
if (d_isHigherOrder) |
127 |
|
{ |
128 |
278 |
Node arg = Rewriter::rewrite(node[1]); |
129 |
278 |
Node var = node[0][0][0]; |
130 |
139 |
new_body = expr::substituteCaptureAvoiding(new_body, var, arg); |
131 |
|
} |
132 |
|
else |
133 |
|
{ |
134 |
|
TNode arg = Rewriter::rewrite(node[1]); |
135 |
|
TNode var = node[0][0][0]; |
136 |
|
new_body = new_body.substitute(var, arg); |
137 |
|
} |
138 |
139 |
Trace("uf-ho-beta") << "uf-ho-beta : ..new body : " << new_body << "\n"; |
139 |
139 |
return RewriteResponse(REWRITE_AGAIN_FULL, new_body); |
140 |
|
} |
141 |
|
} |
142 |
376035 |
return RewriteResponse(REWRITE_DONE, node); |
143 |
|
} |
144 |
|
|
145 |
214971 |
RewriteResponse TheoryUfRewriter::preRewrite(TNode node) |
146 |
|
{ |
147 |
214971 |
if (node.getKind() == kind::EQUAL) |
148 |
|
{ |
149 |
47232 |
if (node[0] == node[1]) |
150 |
|
{ |
151 |
|
return RewriteResponse(REWRITE_DONE, |
152 |
1619 |
NodeManager::currentNM()->mkConst(true)); |
153 |
|
} |
154 |
45613 |
else if (node[0].isConst() && node[1].isConst()) |
155 |
|
{ |
156 |
|
// uninterpreted constants are all distinct |
157 |
|
return RewriteResponse(REWRITE_DONE, |
158 |
6371 |
NodeManager::currentNM()->mkConst(false)); |
159 |
|
} |
160 |
|
} |
161 |
206981 |
return RewriteResponse(REWRITE_DONE, node); |
162 |
|
} |
163 |
|
|
164 |
682049 |
Node TheoryUfRewriter::getHoApplyForApplyUf(TNode n) |
165 |
|
{ |
166 |
682049 |
Assert(n.getKind() == kind::APPLY_UF); |
167 |
682049 |
Node curr = n.getOperator(); |
168 |
2044447 |
for (unsigned i = 0; i < n.getNumChildren(); i++) |
169 |
|
{ |
170 |
1362398 |
curr = NodeManager::currentNM()->mkNode(kind::HO_APPLY, curr, n[i]); |
171 |
|
} |
172 |
682049 |
return curr; |
173 |
|
} |
174 |
|
Node TheoryUfRewriter::getApplyUfForHoApply(TNode n) |
175 |
|
{ |
176 |
|
Assert(n.getType().getNumChildren() == 2); |
177 |
|
std::vector<TNode> children; |
178 |
|
TNode curr = decomposeHoApply(n, children, true); |
179 |
|
// if operator is standard |
180 |
|
if (canUseAsApplyUfOperator(curr)) |
181 |
|
{ |
182 |
|
return NodeManager::currentNM()->mkNode(kind::APPLY_UF, children); |
183 |
|
} |
184 |
|
// cannot construct APPLY_UF if operator is partially applied or is not |
185 |
|
// standard |
186 |
|
return Node::null(); |
187 |
|
} |
188 |
142 |
Node TheoryUfRewriter::decomposeHoApply(TNode n, |
189 |
|
std::vector<TNode>& args, |
190 |
|
bool opInArgs) |
191 |
|
{ |
192 |
284 |
TNode curr = n; |
193 |
632 |
while (curr.getKind() == kind::HO_APPLY) |
194 |
|
{ |
195 |
245 |
args.push_back(curr[1]); |
196 |
245 |
curr = curr[0]; |
197 |
|
} |
198 |
142 |
if (opInArgs) |
199 |
|
{ |
200 |
96 |
args.push_back(curr); |
201 |
|
} |
202 |
142 |
std::reverse(args.begin(), args.end()); |
203 |
284 |
return curr; |
204 |
|
} |
205 |
292728 |
bool TheoryUfRewriter::canUseAsApplyUfOperator(TNode n) { return n.isVar(); } |
206 |
|
|
207 |
|
} // namespace uf |
208 |
|
} // namespace theory |
209 |
22746 |
} // namespace cvc5 |