1 |
|
/****************************************************************************** |
2 |
|
* Top contributors (to current version): |
3 |
|
* Andrew Reynolds, Yoni Zohar, Haniel Barbosa |
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 |
|
* Utility for quantifiers macro definitions. |
14 |
|
*/ |
15 |
|
|
16 |
|
#include "theory/quantifiers/quantifiers_macros.h" |
17 |
|
|
18 |
|
#include "expr/node_algorithm.h" |
19 |
|
#include "expr/skolem_manager.h" |
20 |
|
#include "options/quantifiers_options.h" |
21 |
|
#include "theory/arith/arith_msum.h" |
22 |
|
#include "theory/quantifiers/ematching/pattern_term_selector.h" |
23 |
|
#include "theory/quantifiers/quantifiers_registry.h" |
24 |
|
#include "theory/quantifiers/term_database.h" |
25 |
|
#include "theory/quantifiers/term_util.h" |
26 |
|
#include "theory/rewriter.h" |
27 |
|
|
28 |
|
using namespace cvc5::kind; |
29 |
|
|
30 |
|
namespace cvc5 { |
31 |
|
namespace theory { |
32 |
|
namespace quantifiers { |
33 |
|
|
34 |
22 |
QuantifiersMacros::QuantifiersMacros(QuantifiersRegistry& qr) : d_qreg(qr) {} |
35 |
|
|
36 |
34 |
Node QuantifiersMacros::solve(Node lit, bool reqGround) |
37 |
|
{ |
38 |
34 |
Trace("macros-debug") << "QuantifiersMacros::solve " << lit << std::endl; |
39 |
34 |
if (lit.getKind() != FORALL) |
40 |
|
{ |
41 |
4 |
return Node::null(); |
42 |
|
} |
43 |
60 |
Node body = lit[1]; |
44 |
30 |
bool pol = body.getKind() != NOT; |
45 |
60 |
Node n = pol ? body : body[0]; |
46 |
30 |
NodeManager* nm = NodeManager::currentNM(); |
47 |
30 |
if (n.getKind() == APPLY_UF) |
48 |
|
{ |
49 |
|
// predicate case |
50 |
4 |
if (isBoundVarApplyUf(n)) |
51 |
|
{ |
52 |
8 |
Node op = n.getOperator(); |
53 |
8 |
Node n_def = nm->mkConst(pol); |
54 |
8 |
Node fdef = solveEq(n, n_def); |
55 |
4 |
Assert(!fdef.isNull()); |
56 |
4 |
return returnMacro(fdef, lit); |
57 |
|
} |
58 |
|
} |
59 |
26 |
else if (pol && n.getKind() == EQUAL) |
60 |
|
{ |
61 |
|
// literal case |
62 |
20 |
Trace("macros-debug") << "Check macro literal : " << n << std::endl; |
63 |
28 |
std::map<Node, bool> visited; |
64 |
28 |
std::vector<Node> candidates; |
65 |
60 |
for (const Node& nc : n) |
66 |
|
{ |
67 |
40 |
getMacroCandidates(nc, candidates, visited); |
68 |
|
} |
69 |
20 |
for (const Node& m : candidates) |
70 |
|
{ |
71 |
12 |
Node op = m.getOperator(); |
72 |
12 |
Trace("macros-debug") << "Check macro candidate : " << m << std::endl; |
73 |
|
// get definition and condition |
74 |
12 |
Node n_def = solveInEquality(m, n); // definition for the macro |
75 |
12 |
if (n_def.isNull()) |
76 |
|
{ |
77 |
|
continue; |
78 |
|
} |
79 |
24 |
Trace("macros-debug") |
80 |
12 |
<< m << " is possible macro in " << lit << std::endl; |
81 |
24 |
Trace("macros-debug") |
82 |
12 |
<< " corresponding definition is : " << n_def << std::endl; |
83 |
12 |
visited.clear(); |
84 |
|
// cannot contain a defined operator |
85 |
12 |
if (!containsBadOp(n_def, op, reqGround)) |
86 |
|
{ |
87 |
24 |
Trace("macros-debug") |
88 |
12 |
<< "...does not contain bad (recursive) operator." << std::endl; |
89 |
|
// must be ground UF term if mode is GROUND_UF |
90 |
24 |
if (options::macrosQuantMode() != options::MacrosQuantMode::GROUND_UF |
91 |
24 |
|| preservesTriggerVariables(body, n_def)) |
92 |
|
{ |
93 |
24 |
Trace("macros-debug") |
94 |
12 |
<< "...respects ground-uf constraint." << std::endl; |
95 |
12 |
Node fdef = solveEq(m, n_def); |
96 |
12 |
if (!fdef.isNull()) |
97 |
|
{ |
98 |
12 |
return returnMacro(fdef, lit); |
99 |
|
} |
100 |
|
} |
101 |
|
} |
102 |
|
} |
103 |
|
} |
104 |
14 |
return Node::null(); |
105 |
|
} |
106 |
|
|
107 |
12 |
bool QuantifiersMacros::containsBadOp(Node n, Node op, bool reqGround) |
108 |
|
{ |
109 |
24 |
std::unordered_set<TNode> visited; |
110 |
12 |
std::unordered_set<TNode>::iterator it; |
111 |
24 |
std::vector<TNode> visit; |
112 |
24 |
TNode cur; |
113 |
12 |
visit.push_back(n); |
114 |
12 |
do |
115 |
|
{ |
116 |
24 |
cur = visit.back(); |
117 |
24 |
visit.pop_back(); |
118 |
24 |
it = visited.find(cur); |
119 |
24 |
if (it == visited.end()) |
120 |
|
{ |
121 |
24 |
visited.insert(cur); |
122 |
24 |
if (cur.isClosure() && reqGround) |
123 |
|
{ |
124 |
|
return true; |
125 |
|
} |
126 |
24 |
else if (cur == op) |
127 |
|
{ |
128 |
|
return true; |
129 |
|
} |
130 |
24 |
else if (cur.hasOperator() && cur.getOperator() == op) |
131 |
|
{ |
132 |
|
return true; |
133 |
|
} |
134 |
24 |
visit.insert(visit.end(), cur.begin(), cur.end()); |
135 |
|
} |
136 |
24 |
} while (!visit.empty()); |
137 |
12 |
return false; |
138 |
|
} |
139 |
|
|
140 |
10 |
bool QuantifiersMacros::preservesTriggerVariables(Node q, Node n) |
141 |
|
{ |
142 |
20 |
Node icn = d_qreg.substituteBoundVariablesToInstConstants(n, q); |
143 |
10 |
Trace("macros-debug2") << "Get free variables in " << icn << std::endl; |
144 |
20 |
std::vector<Node> var; |
145 |
10 |
quantifiers::TermUtil::computeInstConstContainsForQuant(q, icn, var); |
146 |
10 |
Trace("macros-debug2") << "Get trigger variables for " << icn << std::endl; |
147 |
20 |
std::vector<Node> trigger_var; |
148 |
10 |
inst::PatternTermSelector::getTriggerVariables(icn, q, trigger_var); |
149 |
10 |
Trace("macros-debug2") << "Done." << std::endl; |
150 |
|
// only if all variables are also trigger variables |
151 |
20 |
return trigger_var.size() >= var.size(); |
152 |
|
} |
153 |
|
|
154 |
26 |
bool QuantifiersMacros::isBoundVarApplyUf(Node n) |
155 |
|
{ |
156 |
26 |
Assert(n.getKind() == APPLY_UF); |
157 |
52 |
TypeNode tno = n.getOperator().getType(); |
158 |
52 |
std::map<Node, bool> vars; |
159 |
|
// allow if a vector of unique variables of the same type as UF arguments |
160 |
44 |
for (size_t i = 0, nchild = n.getNumChildren(); i < nchild; i++) |
161 |
|
{ |
162 |
28 |
if (n[i].getKind() != BOUND_VARIABLE) |
163 |
|
{ |
164 |
8 |
return false; |
165 |
|
} |
166 |
20 |
if (n[i].getType() != tno[i]) |
167 |
|
{ |
168 |
2 |
return false; |
169 |
|
} |
170 |
18 |
if (vars.find(n[i]) == vars.end()) |
171 |
|
{ |
172 |
18 |
vars[n[i]] = true; |
173 |
|
} |
174 |
|
else |
175 |
|
{ |
176 |
|
return false; |
177 |
|
} |
178 |
|
} |
179 |
16 |
return true; |
180 |
|
} |
181 |
|
|
182 |
46 |
void QuantifiersMacros::getMacroCandidates(Node n, |
183 |
|
std::vector<Node>& candidates, |
184 |
|
std::map<Node, bool>& visited) |
185 |
|
{ |
186 |
46 |
if (visited.find(n) == visited.end()) |
187 |
|
{ |
188 |
46 |
visited[n] = true; |
189 |
46 |
if (n.getKind() == APPLY_UF) |
190 |
|
{ |
191 |
22 |
if (isBoundVarApplyUf(n)) |
192 |
|
{ |
193 |
12 |
candidates.push_back(n); |
194 |
|
} |
195 |
|
} |
196 |
24 |
else if (n.getKind() == PLUS) |
197 |
|
{ |
198 |
6 |
for (size_t i = 0; i < n.getNumChildren(); i++) |
199 |
|
{ |
200 |
4 |
getMacroCandidates(n[i], candidates, visited); |
201 |
|
} |
202 |
|
} |
203 |
22 |
else if (n.getKind() == MULT) |
204 |
|
{ |
205 |
|
// if the LHS is a constant |
206 |
2 |
if (n.getNumChildren() == 2 && n[0].isConst()) |
207 |
|
{ |
208 |
2 |
getMacroCandidates(n[1], candidates, visited); |
209 |
|
} |
210 |
|
} |
211 |
20 |
else if (n.getKind() == NOT) |
212 |
|
{ |
213 |
|
getMacroCandidates(n[0], candidates, visited); |
214 |
|
} |
215 |
|
} |
216 |
46 |
} |
217 |
|
|
218 |
12 |
Node QuantifiersMacros::solveInEquality(Node n, Node lit) |
219 |
|
{ |
220 |
12 |
if (lit.getKind() == EQUAL) |
221 |
|
{ |
222 |
|
// return the opposite side of the equality if defined that way |
223 |
20 |
for (int i = 0; i < 2; i++) |
224 |
|
{ |
225 |
16 |
if (lit[i] == n) |
226 |
|
{ |
227 |
20 |
return lit[i == 0 ? 1 : 0]; |
228 |
|
} |
229 |
8 |
else if (lit[i].getKind() == NOT && lit[i][0] == n) |
230 |
|
{ |
231 |
|
return lit[i == 0 ? 1 : 0].negate(); |
232 |
|
} |
233 |
|
} |
234 |
4 |
std::map<Node, Node> msum; |
235 |
4 |
if (ArithMSum::getMonomialSumLit(lit, msum)) |
236 |
|
{ |
237 |
4 |
Node veq_c; |
238 |
4 |
Node val; |
239 |
4 |
int res = ArithMSum::isolate(n, msum, veq_c, val, EQUAL); |
240 |
4 |
if (res != 0 && veq_c.isNull()) |
241 |
|
{ |
242 |
4 |
return val; |
243 |
|
} |
244 |
|
} |
245 |
|
} |
246 |
|
Trace("macros-debug") << "Cannot find for " << lit << " " << n << std::endl; |
247 |
|
return Node::null(); |
248 |
|
} |
249 |
|
|
250 |
16 |
Node QuantifiersMacros::solveEq(Node n, Node ndef) |
251 |
|
{ |
252 |
16 |
Assert(n.getKind() == APPLY_UF); |
253 |
16 |
NodeManager* nm = NodeManager::currentNM(); |
254 |
16 |
Trace("macros-debug") << "Add macro eq for " << n << std::endl; |
255 |
16 |
Trace("macros-debug") << " def: " << ndef << std::endl; |
256 |
32 |
std::vector<Node> vars; |
257 |
32 |
std::vector<Node> fvars; |
258 |
34 |
for (const Node& nc : n) |
259 |
|
{ |
260 |
18 |
vars.push_back(nc); |
261 |
36 |
Node v = nm->mkBoundVar(nc.getType()); |
262 |
18 |
fvars.push_back(v); |
263 |
|
} |
264 |
|
Node fdef = |
265 |
32 |
ndef.substitute(vars.begin(), vars.end(), fvars.begin(), fvars.end()); |
266 |
16 |
fdef = nm->mkNode(LAMBDA, nm->mkNode(BOUND_VAR_LIST, fvars), fdef); |
267 |
|
// If the definition has a free variable, it is malformed. This can happen |
268 |
|
// if the right hand side of a macro definition contains a variable not |
269 |
|
// contained in the left hand side |
270 |
16 |
if (expr::hasFreeVar(fdef)) |
271 |
|
{ |
272 |
|
return Node::null(); |
273 |
|
} |
274 |
32 |
TNode op = n.getOperator(); |
275 |
32 |
TNode fdeft = fdef; |
276 |
16 |
Assert(op.getType().isComparableTo(fdef.getType())); |
277 |
16 |
return op.eqNode(fdef); |
278 |
|
} |
279 |
|
|
280 |
16 |
Node QuantifiersMacros::returnMacro(Node fdef, Node lit) const |
281 |
|
{ |
282 |
32 |
Trace("macros") << "* Inferred macro " << fdef << " from " << lit |
283 |
16 |
<< std::endl; |
284 |
16 |
return fdef; |
285 |
|
} |
286 |
|
|
287 |
|
} // namespace quantifiers |
288 |
|
} // namespace theory |
289 |
29340 |
} // namespace cvc5 |