1 |
|
/****************************************************************************** |
2 |
|
* Top contributors (to current version): |
3 |
|
* Andrew Reynolds, Mathias Preiner, Andres Noetzli |
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 skolemization utility. |
14 |
|
*/ |
15 |
|
|
16 |
|
#include "theory/quantifiers/skolemize.h" |
17 |
|
|
18 |
|
#include "expr/dtype.h" |
19 |
|
#include "expr/dtype_cons.h" |
20 |
|
#include "expr/skolem_manager.h" |
21 |
|
#include "options/quantifiers_options.h" |
22 |
|
#include "options/smt_options.h" |
23 |
|
#include "proof/proof.h" |
24 |
|
#include "proof/proof_node_manager.h" |
25 |
|
#include "theory/quantifiers/quantifiers_attributes.h" |
26 |
|
#include "theory/quantifiers/quantifiers_state.h" |
27 |
|
#include "theory/quantifiers/term_registry.h" |
28 |
|
#include "theory/quantifiers/term_util.h" |
29 |
|
#include "theory/rewriter.h" |
30 |
|
#include "theory/sort_inference.h" |
31 |
|
|
32 |
|
using namespace cvc5::kind; |
33 |
|
|
34 |
|
namespace cvc5 { |
35 |
|
namespace theory { |
36 |
|
namespace quantifiers { |
37 |
|
|
38 |
9913 |
Skolemize::Skolemize(QuantifiersState& qs, |
39 |
|
TermRegistry& tr, |
40 |
9913 |
ProofNodeManager* pnm) |
41 |
|
: d_qstate(qs), |
42 |
|
d_treg(tr), |
43 |
9913 |
d_skolemized(qs.getUserContext()), |
44 |
|
d_pnm(pnm), |
45 |
|
d_epg(pnm == nullptr ? nullptr |
46 |
|
: new EagerProofGenerator( |
47 |
19826 |
pnm, qs.getUserContext(), "Skolemize::epg")) |
48 |
|
{ |
49 |
9913 |
} |
50 |
|
|
51 |
10686 |
TrustNode Skolemize::process(Node q) |
52 |
|
{ |
53 |
10686 |
Assert(q.getKind() == FORALL); |
54 |
|
// do skolemization |
55 |
10686 |
if (d_skolemized.find(q) != d_skolemized.end()) |
56 |
|
{ |
57 |
8288 |
return TrustNode::null(); |
58 |
|
} |
59 |
4796 |
Node lem; |
60 |
2398 |
ProofGenerator* pg = nullptr; |
61 |
5134 |
if (isProofEnabled() && !options::dtStcInduction() |
62 |
2722 |
&& !options::intWfInduction()) |
63 |
|
{ |
64 |
|
// if using proofs and not using induction, we use the justified |
65 |
|
// skolemization |
66 |
323 |
NodeManager* nm = NodeManager::currentNM(); |
67 |
323 |
SkolemManager* skm = nm->getSkolemManager(); |
68 |
646 |
std::vector<Node> echildren(q.begin(), q.end()); |
69 |
323 |
echildren[1] = echildren[1].notNode(); |
70 |
646 |
Node existsq = nm->mkNode(EXISTS, echildren); |
71 |
646 |
Node res = skm->mkSkolemize(existsq, d_skolem_constants[q], "skv"); |
72 |
646 |
Node qnot = q.notNode(); |
73 |
646 |
CDProof cdp(d_pnm); |
74 |
323 |
cdp.addStep(res, PfRule::SKOLEMIZE, {qnot}, {}); |
75 |
646 |
std::shared_ptr<ProofNode> pf = cdp.getProofFor(res); |
76 |
646 |
std::vector<Node> assumps; |
77 |
323 |
assumps.push_back(qnot); |
78 |
646 |
std::shared_ptr<ProofNode> pfs = d_pnm->mkScope({pf}, assumps); |
79 |
323 |
lem = nm->mkNode(IMPLIES, qnot, res); |
80 |
323 |
d_epg->setProofFor(lem, pfs); |
81 |
323 |
pg = d_epg.get(); |
82 |
646 |
Trace("quantifiers-sk") |
83 |
323 |
<< "Skolemize (with proofs) : " << d_skolem_constants[q] << " for " |
84 |
323 |
<< std::endl; |
85 |
323 |
Trace("quantifiers-sk") << " " << q << std::endl; |
86 |
323 |
Trace("quantifiers-sk") << " " << res << std::endl; |
87 |
|
} |
88 |
|
else |
89 |
|
{ |
90 |
|
// otherwise, we use the more general skolemization with inductive |
91 |
|
// strengthening, which does not support proofs |
92 |
4150 |
Node body = getSkolemizedBody(q); |
93 |
4150 |
NodeBuilder nb(kind::OR); |
94 |
2075 |
nb << q << body.notNode(); |
95 |
2075 |
lem = nb; |
96 |
|
} |
97 |
2398 |
d_skolemized[q] = lem; |
98 |
|
// triggered when skolemizing |
99 |
2398 |
d_treg.processSkolemization(q, d_skolem_constants[q]); |
100 |
2398 |
return TrustNode::mkTrustLemma(lem, pg); |
101 |
|
} |
102 |
|
|
103 |
33 |
bool Skolemize::getSkolemConstants(Node q, std::vector<Node>& skolems) |
104 |
|
{ |
105 |
|
std::unordered_map<Node, std::vector<Node>>::iterator it = |
106 |
33 |
d_skolem_constants.find(q); |
107 |
33 |
if (it != d_skolem_constants.end()) |
108 |
|
{ |
109 |
33 |
skolems.insert(skolems.end(), it->second.begin(), it->second.end()); |
110 |
33 |
return true; |
111 |
|
} |
112 |
|
return false; |
113 |
|
} |
114 |
|
|
115 |
|
Node Skolemize::getSkolemConstant(Node q, unsigned i) |
116 |
|
{ |
117 |
|
std::unordered_map<Node, std::vector<Node>>::iterator it = |
118 |
|
d_skolem_constants.find(q); |
119 |
|
if (it != d_skolem_constants.end()) |
120 |
|
{ |
121 |
|
if (i < it->second.size()) |
122 |
|
{ |
123 |
|
return it->second[i]; |
124 |
|
} |
125 |
|
} |
126 |
|
return Node::null(); |
127 |
|
} |
128 |
|
|
129 |
114 |
void Skolemize::getSelfSel(const DType& dt, |
130 |
|
const DTypeConstructor& dc, |
131 |
|
Node n, |
132 |
|
TypeNode ntn, |
133 |
|
std::vector<Node>& selfSel) |
134 |
|
{ |
135 |
228 |
TypeNode tspec; |
136 |
114 |
if (dt.isParametric()) |
137 |
|
{ |
138 |
|
tspec = dc.getSpecializedConstructorType(n.getType()); |
139 |
|
Trace("sk-ind-debug") << "Specialized constructor type : " << tspec |
140 |
|
<< std::endl; |
141 |
|
Assert(tspec.getNumChildren() == dc.getNumArgs()); |
142 |
|
} |
143 |
228 |
Trace("sk-ind-debug") << "Check self sel " << dc.getName() << " " |
144 |
114 |
<< dt.getName() << std::endl; |
145 |
114 |
NodeManager* nm = NodeManager::currentNM(); |
146 |
219 |
for (unsigned j = 0; j < dc.getNumArgs(); j++) |
147 |
|
{ |
148 |
210 |
std::vector<Node> ssc; |
149 |
105 |
if (dt.isParametric()) |
150 |
|
{ |
151 |
|
Trace("sk-ind-debug") << "Compare " << tspec[j] << " " << ntn |
152 |
|
<< std::endl; |
153 |
|
if (tspec[j] == ntn) |
154 |
|
{ |
155 |
|
ssc.push_back(n); |
156 |
|
} |
157 |
|
} |
158 |
|
else |
159 |
|
{ |
160 |
210 |
TypeNode tn = dc[j].getRangeType(); |
161 |
105 |
Trace("sk-ind-debug") << "Compare " << tn << " " << ntn << std::endl; |
162 |
105 |
if (tn == ntn) |
163 |
|
{ |
164 |
57 |
ssc.push_back(n); |
165 |
|
} |
166 |
|
} |
167 |
162 |
for (unsigned k = 0; k < ssc.size(); k++) |
168 |
|
{ |
169 |
|
Node ss = nm->mkNode( |
170 |
114 |
APPLY_SELECTOR_TOTAL, dc.getSelectorInternal(n.getType(), j), n); |
171 |
57 |
if (std::find(selfSel.begin(), selfSel.end(), ss) == selfSel.end()) |
172 |
|
{ |
173 |
57 |
selfSel.push_back(ss); |
174 |
|
} |
175 |
|
} |
176 |
|
} |
177 |
114 |
} |
178 |
|
|
179 |
2084 |
Node Skolemize::mkSkolemizedBody(Node f, |
180 |
|
Node n, |
181 |
|
std::vector<TNode>& fvs, |
182 |
|
std::vector<Node>& sk, |
183 |
|
Node& sub, |
184 |
|
std::vector<unsigned>& sub_vars) |
185 |
|
{ |
186 |
2084 |
NodeManager* nm = NodeManager::currentNM(); |
187 |
|
// compute the argument types from the free variables |
188 |
4168 |
std::vector<TypeNode> argTypes; |
189 |
2096 |
for (TNode v : fvs) |
190 |
|
{ |
191 |
12 |
argTypes.push_back(v.getType()); |
192 |
|
} |
193 |
2084 |
SkolemManager* sm = nm->getSkolemManager(); |
194 |
2084 |
Assert(sk.empty() || sk.size() == f[0].getNumChildren()); |
195 |
|
// calculate the variables and substitution |
196 |
4168 |
std::vector<TNode> ind_vars; |
197 |
4168 |
std::vector<unsigned> ind_var_indicies; |
198 |
4168 |
std::vector<TNode> vars; |
199 |
4168 |
std::vector<unsigned> var_indicies; |
200 |
5356 |
for (unsigned i = 0; i < f[0].getNumChildren(); i++) |
201 |
|
{ |
202 |
3272 |
if (isInductionTerm(f[0][i])) |
203 |
|
{ |
204 |
86 |
ind_vars.push_back(f[0][i]); |
205 |
86 |
ind_var_indicies.push_back(i); |
206 |
|
} |
207 |
|
else |
208 |
|
{ |
209 |
3186 |
vars.push_back(f[0][i]); |
210 |
3186 |
var_indicies.push_back(i); |
211 |
|
} |
212 |
6544 |
Node s; |
213 |
|
// make the new function symbol or use existing |
214 |
3272 |
if (i >= sk.size()) |
215 |
|
{ |
216 |
3249 |
if (argTypes.empty()) |
217 |
|
{ |
218 |
9723 |
s = sm->mkDummySkolem( |
219 |
6482 |
"skv", f[0][i].getType(), "created during skolemization"); |
220 |
|
} |
221 |
|
else |
222 |
|
{ |
223 |
16 |
TypeNode typ = nm->mkFunctionType(argTypes, f[0][i].getType()); |
224 |
|
Node op = sm->mkDummySkolem( |
225 |
16 |
"skop", typ, "op created during pre-skolemization"); |
226 |
|
// DOTHIS: set attribute on op, marking that it should not be selected |
227 |
|
// as trigger |
228 |
16 |
std::vector<Node> funcArgs; |
229 |
8 |
funcArgs.push_back(op); |
230 |
8 |
funcArgs.insert(funcArgs.end(), fvs.begin(), fvs.end()); |
231 |
8 |
s = nm->mkNode(kind::APPLY_UF, funcArgs); |
232 |
|
} |
233 |
3249 |
sk.push_back(s); |
234 |
|
} |
235 |
|
else |
236 |
|
{ |
237 |
23 |
Assert(sk[i].getType() == f[0][i].getType()); |
238 |
|
} |
239 |
|
} |
240 |
2084 |
Node ret; |
241 |
2084 |
if (vars.empty()) |
242 |
|
{ |
243 |
63 |
ret = n; |
244 |
|
} |
245 |
|
else |
246 |
|
{ |
247 |
4042 |
std::vector<Node> var_sk; |
248 |
5207 |
for (unsigned i = 0; i < var_indicies.size(); i++) |
249 |
|
{ |
250 |
3186 |
var_sk.push_back(sk[var_indicies[i]]); |
251 |
|
} |
252 |
2021 |
Assert(vars.size() == var_sk.size()); |
253 |
2021 |
ret = n.substitute(vars.begin(), vars.end(), var_sk.begin(), var_sk.end()); |
254 |
|
} |
255 |
2084 |
if (!ind_vars.empty()) |
256 |
|
{ |
257 |
63 |
Trace("sk-ind") << "Ind strengthen : (not " << f << ")" << std::endl; |
258 |
63 |
Trace("sk-ind") << "Skolemized is : " << ret << std::endl; |
259 |
126 |
Node n_str_ind; |
260 |
126 |
TypeNode tn = ind_vars[0].getType(); |
261 |
126 |
Node k = sk[ind_var_indicies[0]]; |
262 |
126 |
Node nret = ret.substitute(ind_vars[0], k); |
263 |
|
// note : everything is under a negation |
264 |
|
// the following constructs ~( R( x, k ) => ~P( x ) ) |
265 |
63 |
if (options::dtStcInduction() && tn.isDatatype()) |
266 |
|
{ |
267 |
57 |
const DType& dt = tn.getDType(); |
268 |
114 |
std::vector<Node> disj; |
269 |
171 |
for (unsigned i = 0; i < dt.getNumConstructors(); i++) |
270 |
|
{ |
271 |
228 |
std::vector<Node> selfSel; |
272 |
114 |
getSelfSel(dt, dt[i], k, tn, selfSel); |
273 |
228 |
std::vector<Node> conj; |
274 |
114 |
conj.push_back(nm->mkNode(APPLY_TESTER, dt[i].getTester(), k).negate()); |
275 |
171 |
for (unsigned j = 0; j < selfSel.size(); j++) |
276 |
|
{ |
277 |
57 |
conj.push_back(ret.substitute(ind_vars[0], selfSel[j]).negate()); |
278 |
|
} |
279 |
114 |
disj.push_back(conj.size() == 1 ? conj[0] : nm->mkNode(OR, conj)); |
280 |
|
} |
281 |
57 |
Assert(!disj.empty()); |
282 |
57 |
n_str_ind = disj.size() == 1 ? disj[0] : nm->mkNode(AND, disj); |
283 |
|
} |
284 |
6 |
else if (options::intWfInduction() && tn.isInteger()) |
285 |
|
{ |
286 |
12 |
Node icond = nm->mkNode(GEQ, k, nm->mkConst(Rational(0))); |
287 |
12 |
Node iret = ret.substitute(ind_vars[0], |
288 |
12 |
nm->mkNode(MINUS, k, nm->mkConst(Rational(1)))) |
289 |
12 |
.negate(); |
290 |
6 |
n_str_ind = nm->mkNode(OR, icond.negate(), iret); |
291 |
6 |
n_str_ind = nm->mkNode(AND, icond, n_str_ind); |
292 |
|
} |
293 |
|
else |
294 |
|
{ |
295 |
|
Trace("sk-ind") << "Unknown induction for term : " << ind_vars[0] |
296 |
|
<< ", type = " << tn << std::endl; |
297 |
|
Assert(false); |
298 |
|
} |
299 |
63 |
Trace("sk-ind") << "Strengthening is : " << n_str_ind << std::endl; |
300 |
|
|
301 |
126 |
std::vector<Node> rem_ind_vars; |
302 |
63 |
rem_ind_vars.insert( |
303 |
126 |
rem_ind_vars.end(), ind_vars.begin() + 1, ind_vars.end()); |
304 |
63 |
if (!rem_ind_vars.empty()) |
305 |
|
{ |
306 |
38 |
Node bvl = nm->mkNode(BOUND_VAR_LIST, rem_ind_vars); |
307 |
19 |
nret = nm->mkNode(FORALL, bvl, nret); |
308 |
19 |
nret = Rewriter::rewrite(nret); |
309 |
19 |
sub = nret; |
310 |
19 |
sub_vars.insert( |
311 |
38 |
sub_vars.end(), ind_var_indicies.begin() + 1, ind_var_indicies.end()); |
312 |
19 |
n_str_ind = nm->mkNode(FORALL, bvl, n_str_ind.negate()).negate(); |
313 |
|
} |
314 |
63 |
ret = nm->mkNode(OR, nret, n_str_ind); |
315 |
|
} |
316 |
4168 |
Trace("quantifiers-sk-debug") << "mkSkolem body for " << f |
317 |
2084 |
<< " returns : " << ret << std::endl; |
318 |
|
// if it has an instantiation level, set the skolemized body to that level |
319 |
2084 |
if (f.hasAttribute(InstLevelAttribute())) |
320 |
|
{ |
321 |
|
QuantAttributes::setInstantiationLevelAttr( |
322 |
|
ret, f.getAttribute(InstLevelAttribute())); |
323 |
|
} |
324 |
|
|
325 |
2084 |
Trace("quantifiers-sk") << "Skolemize : " << sk << " for " << std::endl; |
326 |
2084 |
Trace("quantifiers-sk") << " " << f << std::endl; |
327 |
|
|
328 |
4168 |
return ret; |
329 |
|
} |
330 |
|
|
331 |
2075 |
Node Skolemize::getSkolemizedBody(Node f) |
332 |
|
{ |
333 |
2075 |
Assert(f.getKind() == FORALL); |
334 |
2075 |
std::unordered_map<Node, Node>::iterator it = d_skolem_body.find(f); |
335 |
2075 |
if (it == d_skolem_body.end()) |
336 |
|
{ |
337 |
4132 |
std::vector<TNode> fvs; |
338 |
4132 |
Node sub; |
339 |
4132 |
std::vector<unsigned> sub_vars; |
340 |
|
Node ret = |
341 |
4132 |
mkSkolemizedBody(f, f[1], fvs, d_skolem_constants[f], sub, sub_vars); |
342 |
2066 |
d_skolem_body[f] = ret; |
343 |
|
// store sub quantifier information |
344 |
2066 |
if (!sub.isNull()) |
345 |
|
{ |
346 |
|
// if we are skolemizing one at a time, we already know the skolem |
347 |
|
// constants of the sub-quantified formula, store them |
348 |
19 |
Assert(d_skolem_constants[sub].empty()); |
349 |
42 |
for (unsigned i = 0; i < sub_vars.size(); i++) |
350 |
|
{ |
351 |
23 |
d_skolem_constants[sub].push_back(d_skolem_constants[f][sub_vars[i]]); |
352 |
|
} |
353 |
|
} |
354 |
2066 |
Assert(d_skolem_constants[f].size() == f[0].getNumChildren()); |
355 |
2066 |
SortInference* si = d_qstate.getSortInference(); |
356 |
2066 |
if (si != nullptr) |
357 |
|
{ |
358 |
|
for (unsigned i = 0; i < d_skolem_constants[f].size(); i++) |
359 |
|
{ |
360 |
|
// carry information for sort inference |
361 |
|
si->setSkolemVar(f, f[0][i], d_skolem_constants[f][i]); |
362 |
|
} |
363 |
|
} |
364 |
2066 |
return ret; |
365 |
|
} |
366 |
9 |
return it->second; |
367 |
|
} |
368 |
|
|
369 |
9188 |
bool Skolemize::isInductionTerm(Node n) |
370 |
|
{ |
371 |
18376 |
TypeNode tn = n.getType(); |
372 |
9188 |
if (options::dtStcInduction() && tn.isDatatype()) |
373 |
|
{ |
374 |
3909 |
const DType& dt = tn.getDType(); |
375 |
3909 |
return !dt.isCodatatype(); |
376 |
|
} |
377 |
5279 |
if (options::intWfInduction() && tn.isInteger()) |
378 |
|
{ |
379 |
1324 |
return true; |
380 |
|
} |
381 |
3955 |
return false; |
382 |
|
} |
383 |
|
|
384 |
12 |
void Skolemize::getSkolemTermVectors( |
385 |
|
std::map<Node, std::vector<Node> >& sks) const |
386 |
|
{ |
387 |
12 |
std::unordered_map<Node, std::vector<Node>>::const_iterator itk; |
388 |
21 |
for (const auto& p : d_skolemized) |
389 |
|
{ |
390 |
18 |
Node q = p.first; |
391 |
9 |
itk = d_skolem_constants.find(q); |
392 |
9 |
Assert(itk != d_skolem_constants.end()); |
393 |
9 |
sks[q].insert(sks[q].end(), itk->second.begin(), itk->second.end()); |
394 |
|
} |
395 |
12 |
} |
396 |
|
|
397 |
2398 |
bool Skolemize::isProofEnabled() const { return d_epg != nullptr; } |
398 |
|
|
399 |
|
} // namespace quantifiers |
400 |
|
} // namespace theory |
401 |
29502 |
} // namespace cvc5 |