Branch data Line data Source code
1 : : /******************************************************************************
2 : : * Top contributors (to current version):
3 : : * Andrew Reynolds, Aina Niemetz, Mathias Preiner
4 : : *
5 : : * This file is part of the cvc5 project.
6 : : *
7 : : * Copyright (c) 2009-2024 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 : : #include "util/rational.h"
32 : :
33 : : using namespace cvc5::internal::kind;
34 : :
35 : : namespace cvc5::internal {
36 : : namespace theory {
37 : : namespace quantifiers {
38 : :
39 : 49691 : Skolemize::Skolemize(Env& env, QuantifiersState& qs, TermRegistry& tr)
40 : : : EnvObj(env),
41 : : d_qstate(qs),
42 : : d_treg(tr),
43 : 99382 : d_skolemized(userContext()),
44 : 99382 : d_epg(!isProofEnabled()
45 : : ? nullptr
46 : 49691 : : new EagerProofGenerator(env, userContext(), "Skolemize::epg"))
47 : : {
48 : 49691 : }
49 : :
50 : 22087 : TrustNode Skolemize::process(Node q)
51 : : {
52 [ - + ][ - + ]: 22087 : Assert(q.getKind() == Kind::FORALL);
[ - - ]
53 : : // do skolemization
54 [ + + ]: 22087 : if (d_skolemized.find(q) != d_skolemized.end())
55 : : {
56 : 16879 : return TrustNode::null();
57 : : }
58 : 5208 : Node lem;
59 : 5208 : ProofGenerator* pg = nullptr;
60 [ + + ]: 7285 : if (isProofEnabled() && !options().quantifiers.dtStcInduction
61 [ + + ][ + + ]: 7285 : && !options().quantifiers.intWfInduction)
[ + + ]
62 : : {
63 : 2025 : ProofNodeManager * pnm = d_env.getProofNodeManager();
64 : : // if using proofs and not using induction, we use the justified
65 : : // skolemization
66 : 2025 : NodeManager* nm = NodeManager::currentNM();
67 : : // cache the skolems in d_skolem_constants[q]
68 : 2025 : std::vector<Node>& skolems = d_skolem_constants[q];
69 : 2025 : skolems = getSkolemConstants(q);
70 : 6075 : std::vector<Node> vars(q[0].begin(), q[0].end());
71 : : Node res = q[1].substitute(
72 : 4050 : vars.begin(), vars.end(), skolems.begin(), skolems.end());
73 : 4050 : Node qnot = q.notNode();
74 : 6075 : CDProof cdp(d_env);
75 : 2025 : res = res.notNode();
76 : 4050 : cdp.addStep(res, ProofRule::SKOLEMIZE, {qnot}, {});
77 : 4050 : std::shared_ptr<ProofNode> pf = cdp.getProofFor(res);
78 : 4050 : std::vector<Node> assumps;
79 : 2025 : assumps.push_back(qnot);
80 : 4050 : std::shared_ptr<ProofNode> pfs = pnm->mkScope({pf}, assumps);
81 : 2025 : lem = nm->mkNode(Kind::IMPLIES, qnot, res);
82 : 2025 : d_epg->setProofFor(lem, pfs);
83 [ + - ]: 2025 : pg = d_epg.get();
84 [ + - ]: 4050 : Trace("quantifiers-sk")
85 : 0 : << "Skolemize (with proofs) : " << d_skolem_constants[q] << " for "
86 : 2025 : << std::endl;
87 [ + - ]: 2025 : Trace("quantifiers-sk") << " " << q << std::endl;
88 [ + - ]: 2025 : Trace("quantifiers-sk") << " " << res << std::endl;
89 : : }
90 : : else
91 : : {
92 : : // otherwise, we use the more general skolemization with inductive
93 : : // strengthening, which does not support proofs
94 : 6366 : Node body = getSkolemizedBodyInduction(q);
95 : 3183 : NodeBuilder nb(Kind::OR);
96 : 3183 : nb << q << body.notNode();
97 : 3183 : lem = nb;
98 : : }
99 : 5208 : d_skolemized[q] = lem;
100 : : // triggered when skolemizing
101 : 5208 : d_treg.processSkolemization(q, d_skolem_constants[q]);
102 : 5208 : return TrustNode::mkTrustLemma(lem, pg);
103 : : }
104 : :
105 : 6248 : std::vector<Node> Skolemize::getSkolemConstants(const Node& q)
106 : : {
107 [ - + ][ - + ]: 6248 : Assert(q.getKind() == Kind::FORALL);
[ - - ]
108 : 6248 : std::vector<Node> skolems;
109 [ + + ]: 17070 : for (size_t i = 0, nvars = q[0].getNumChildren(); i < nvars; i++)
110 : : {
111 : 10822 : skolems.push_back(getSkolemConstant(q, i));
112 : : }
113 : 6248 : return skolems;
114 : : }
115 : :
116 : 10822 : Node Skolemize::getSkolemConstant(const Node& q, size_t i)
117 : : {
118 [ - + ][ - + ]: 10822 : Assert(q.getKind() == Kind::FORALL);
[ - - ]
119 [ - + ][ - + ]: 10822 : Assert(i < q[0].getNumChildren());
[ - - ]
120 : 10822 : NodeManager* nm = NodeManager::currentNM();
121 : 10822 : SkolemManager* sm = nm->getSkolemManager();
122 : 64932 : std::vector<Node> cacheVals{q, nm->mkConstInt(Rational(i))};
123 : 21644 : return sm->mkSkolemFunction(SkolemId::QUANTIFIERS_SKOLEMIZE, cacheVals);
124 : : }
125 : :
126 : 178 : void Skolemize::getSelfSel(const DType& dt,
127 : : const DTypeConstructor& dc,
128 : : Node n,
129 : : TypeNode ntn,
130 : : std::vector<Node>& selfSel)
131 : : {
132 : 356 : TypeNode tspec;
133 [ - + ]: 178 : if (dt.isParametric())
134 : : {
135 : 0 : tspec = dc.getInstantiatedConstructorType(n.getType());
136 [ - - ]: 0 : Trace("sk-ind-debug") << "Instantiated constructor type : " << tspec
137 : 0 : << std::endl;
138 : 0 : Assert(tspec.getNumChildren() == dc.getNumArgs());
139 : : }
140 [ + - ]: 356 : Trace("sk-ind-debug") << "Check self sel " << dc.getName() << " "
141 [ - + ][ - - ]: 178 : << dt.getName() << std::endl;
142 : 178 : NodeManager* nm = NodeManager::currentNM();
143 [ + + ]: 340 : for (unsigned j = 0; j < dc.getNumArgs(); j++)
144 : : {
145 [ - + ]: 162 : if (dt.isParametric())
146 : : {
147 : 0 : Trace("sk-ind-debug") << "Compare " << tspec[j] << " " << ntn
148 : 0 : << std::endl;
149 [ - - ]: 0 : if (tspec[j] != ntn)
150 : : {
151 : 73 : continue;
152 : : }
153 : : }
154 : : else
155 : : {
156 : 162 : TypeNode tn = dc[j].getRangeType();
157 [ + - ]: 162 : Trace("sk-ind-debug") << "Compare " << tn << " " << ntn << std::endl;
158 [ + + ]: 162 : if (tn != ntn)
159 : : {
160 : 73 : continue;
161 : : }
162 : : }
163 : : // do not use shared selectors
164 : 267 : Node ss = nm->mkNode(Kind::APPLY_SELECTOR, dc.getSelector(j), n);
165 [ + - ]: 89 : if (std::find(selfSel.begin(), selfSel.end(), ss) == selfSel.end())
166 : : {
167 : 89 : selfSel.push_back(ss);
168 : : }
169 : : }
170 : 178 : }
171 : :
172 : 57 : bool Skolemize::getSkolemConstantsInduction(Node q, std::vector<Node>& skolems)
173 : : {
174 : : std::unordered_map<Node, std::vector<Node>>::iterator it =
175 : 57 : d_skolem_constants.find(q);
176 [ + - ]: 57 : if (it != d_skolem_constants.end())
177 : : {
178 : 57 : skolems.insert(skolems.end(), it->second.begin(), it->second.end());
179 : 57 : return true;
180 : : }
181 : 0 : return false;
182 : : }
183 : :
184 : 3187 : Node Skolemize::mkSkolemizedBodyInduction(const Options& opts,
185 : : Node f,
186 : : Node n,
187 : : std::vector<TNode>& fvs,
188 : : std::vector<Node>& sk,
189 : : Node& sub,
190 : : std::vector<unsigned>& sub_vars)
191 : : {
192 [ - + ][ - + ]: 3187 : Assert (f.getKind()==Kind::FORALL);
[ - - ]
193 : 3187 : NodeManager* nm = NodeManager::currentNM();
194 : : // compute the argument types from the free variables
195 : 6374 : std::vector<TypeNode> argTypes;
196 [ + + ]: 3195 : for (TNode v : fvs)
197 : : {
198 : 8 : argTypes.push_back(v.getType());
199 : : }
200 : 3187 : SkolemManager* sm = nm->getSkolemManager();
201 : 3187 : Assert(sk.empty() || sk.size() == f[0].getNumChildren());
202 : : // calculate the variables and substitution
203 : 6374 : std::vector<TNode> ind_vars;
204 : 6374 : std::vector<unsigned> ind_var_indicies;
205 : 6374 : std::vector<TNode> vars;
206 : 6374 : std::vector<unsigned> var_indicies;
207 : 6374 : std::vector<Node> skc = getSkolemConstants(f);
208 [ + + ]: 8895 : for (size_t i = 0, nvars = f[0].getNumChildren(); i < nvars; i++)
209 : : {
210 [ + + ]: 5708 : if (isInductionTerm(opts, f[0][i]))
211 : : {
212 : 128 : ind_vars.push_back(f[0][i]);
213 : 128 : ind_var_indicies.push_back(i);
214 : : }
215 : : else
216 : : {
217 : 5580 : vars.push_back(f[0][i]);
218 : 5580 : var_indicies.push_back(i);
219 : : }
220 : 11416 : Node s;
221 : : // make the new function symbol or use existing
222 [ + + ]: 5708 : if (i >= sk.size())
223 : : {
224 [ + + ]: 5679 : if (argTypes.empty())
225 : : {
226 : 5673 : s = skc[i];
227 : : }
228 : : else
229 : : {
230 : 18 : TypeNode typ = nm->mkFunctionType(argTypes, f[0][i].getType());
231 : : Node op = sm->mkDummySkolem(
232 : 18 : "skop", typ, "op created during pre-skolemization");
233 : : // DOTHIS: set attribute on op, marking that it should not be selected
234 : : // as trigger
235 : 6 : std::vector<Node> funcArgs;
236 : 6 : funcArgs.push_back(op);
237 : 6 : funcArgs.insert(funcArgs.end(), fvs.begin(), fvs.end());
238 : 6 : s = nm->mkNode(Kind::APPLY_UF, funcArgs);
239 : : }
240 : 5679 : sk.push_back(s);
241 : : }
242 : : else
243 : : {
244 [ - + ][ - + ]: 29 : Assert(sk[i].getType() == f[0][i].getType());
[ - - ]
245 : : }
246 : : }
247 : 3187 : Node ret;
248 [ + + ]: 3187 : if (vars.empty())
249 : : {
250 : 99 : ret = n;
251 : : }
252 : : else
253 : : {
254 : 3088 : std::vector<Node> var_sk;
255 [ + + ]: 8668 : for (unsigned i = 0; i < var_indicies.size(); i++)
256 : : {
257 : 5580 : var_sk.push_back(sk[var_indicies[i]]);
258 : : }
259 [ - + ][ - + ]: 3088 : Assert(vars.size() == var_sk.size());
[ - - ]
260 : 3088 : ret = n.substitute(vars.begin(), vars.end(), var_sk.begin(), var_sk.end());
261 : : }
262 [ + + ]: 3187 : if (!ind_vars.empty())
263 : : {
264 [ + - ]: 99 : Trace("sk-ind") << "Ind strengthen : (not " << f << ")" << std::endl;
265 [ + - ]: 99 : Trace("sk-ind") << "Skolemized is : " << ret << std::endl;
266 : 198 : Node n_str_ind;
267 : 198 : TypeNode tn = ind_vars[0].getType();
268 : 198 : Node k = sk[ind_var_indicies[0]];
269 : 297 : Node nret = ret.substitute(ind_vars[0], k);
270 : : // note : everything is under a negation
271 : : // the following constructs ~( R( x, k ) => ~P( x ) )
272 [ + + ][ + + ]: 99 : if (opts.quantifiers.dtStcInduction && tn.isDatatype())
[ + + ]
273 : : {
274 : 89 : const DType& dt = tn.getDType();
275 : 89 : std::vector<Node> disj;
276 [ + + ]: 267 : for (unsigned i = 0; i < dt.getNumConstructors(); i++)
277 : : {
278 : 356 : std::vector<Node> selfSel;
279 : 178 : getSelfSel(dt, dt[i], k, tn, selfSel);
280 : 178 : std::vector<Node> conj;
281 : 178 : conj.push_back(
282 : 356 : nm->mkNode(Kind::APPLY_TESTER, dt[i].getTester(), k).negate());
283 [ + + ]: 267 : for (unsigned j = 0; j < selfSel.size(); j++)
284 : : {
285 : 89 : conj.push_back(ret.substitute(ind_vars[0], selfSel[j]).negate());
286 : : }
287 [ + + ]: 178 : disj.push_back(conj.size() == 1 ? conj[0] : nm->mkNode(Kind::OR, conj));
288 : : }
289 [ - + ][ - + ]: 89 : Assert(!disj.empty());
[ - - ]
290 [ - + ]: 89 : n_str_ind = disj.size() == 1 ? disj[0] : nm->mkNode(Kind::AND, disj);
291 : : }
292 [ + - ][ + - ]: 10 : else if (opts.quantifiers.intWfInduction && tn.isInteger())
[ + - ]
293 : : {
294 : 30 : Node icond = nm->mkNode(Kind::GEQ, k, nm->mkConstInt(Rational(0)));
295 : : Node iret =
296 : 20 : ret.substitute(ind_vars[0],
297 : 20 : nm->mkNode(Kind::SUB, k, nm->mkConstInt(Rational(1))))
298 : 10 : .negate();
299 : 10 : n_str_ind = nm->mkNode(Kind::OR, icond.negate(), iret);
300 : 10 : n_str_ind = nm->mkNode(Kind::AND, icond, n_str_ind);
301 : : }
302 : : else
303 : : {
304 [ - - ]: 0 : Trace("sk-ind") << "Unknown induction for term : " << ind_vars[0]
305 : 0 : << ", type = " << tn << std::endl;
306 : 0 : Assert(false);
307 : : }
308 [ + - ]: 99 : Trace("sk-ind") << "Strengthening is : " << n_str_ind << std::endl;
309 : :
310 : 99 : std::vector<Node> rem_ind_vars;
311 : : rem_ind_vars.insert(
312 : 99 : rem_ind_vars.end(), ind_vars.begin() + 1, ind_vars.end());
313 [ + + ]: 99 : if (!rem_ind_vars.empty())
314 : : {
315 : 24 : Node bvl = nm->mkNode(Kind::BOUND_VAR_LIST, rem_ind_vars);
316 : 24 : nret = nm->mkNode(Kind::FORALL, bvl, nret);
317 : 24 : sub = nret;
318 : : sub_vars.insert(
319 : 24 : sub_vars.end(), ind_var_indicies.begin() + 1, ind_var_indicies.end());
320 : 24 : n_str_ind = nm->mkNode(Kind::FORALL, bvl, n_str_ind.negate()).negate();
321 : : }
322 : 99 : ret = nm->mkNode(Kind::OR, nret, n_str_ind);
323 : : }
324 [ + - ]: 6374 : Trace("quantifiers-sk-debug") << "mkSkolem body for " << f
325 : 3187 : << " returns : " << ret << std::endl;
326 : : // if it has an instantiation level, set the skolemized body to that level
327 : : uint64_t level;
328 [ - + ]: 3187 : if (QuantAttributes::getInstantiationLevel(f, level))
329 : : {
330 : 0 : QuantAttributes::setInstantiationLevelAttr(ret, level);
331 : : }
332 : :
333 [ + - ]: 3187 : Trace("quantifiers-sk") << "Skolemize : " << sk << " for " << std::endl;
334 [ + - ]: 3187 : Trace("quantifiers-sk") << " " << f << std::endl;
335 : :
336 : 6374 : return ret;
337 : : }
338 : :
339 : 3183 : Node Skolemize::getSkolemizedBodyInduction(Node f)
340 : : {
341 [ - + ][ - + ]: 3183 : Assert(f.getKind() == Kind::FORALL);
[ - - ]
342 : 3183 : std::unordered_map<Node, Node>::iterator it = d_skolem_body.find(f);
343 [ + + ]: 3183 : if (it == d_skolem_body.end())
344 : : {
345 : 6342 : std::vector<TNode> fvs;
346 : 6342 : Node sub;
347 : 6342 : std::vector<unsigned> sub_vars;
348 : : Node ret = mkSkolemizedBodyInduction(
349 : 9513 : options(), f, f[1], fvs, d_skolem_constants[f], sub, sub_vars);
350 : 3171 : d_skolem_body[f] = ret;
351 : : // store sub quantifier information
352 [ + + ]: 3171 : if (!sub.isNull())
353 : : {
354 : : // if we are skolemizing one at a time, we already know the skolem
355 : : // constants of the sub-quantified formula, store them
356 [ - + ][ - + ]: 24 : Assert(d_skolem_constants[sub].empty());
[ - - ]
357 [ + + ]: 53 : for (unsigned i = 0; i < sub_vars.size(); i++)
358 : : {
359 : 29 : d_skolem_constants[sub].push_back(d_skolem_constants[f][sub_vars[i]]);
360 : : }
361 : : }
362 [ - + ][ - + ]: 3171 : Assert(d_skolem_constants[f].size() == f[0].getNumChildren());
[ - - ]
363 : 3171 : SortInference* si = d_qstate.getSortInference();
364 [ - + ]: 3171 : if (si != nullptr)
365 : : {
366 [ - - ]: 0 : for (unsigned i = 0; i < d_skolem_constants[f].size(); i++)
367 : : {
368 : : // carry information for sort inference
369 : 0 : si->setSkolemVar(f, f[0][i], d_skolem_constants[f][i]);
370 : : }
371 : : }
372 : 3171 : return ret;
373 : : }
374 : 12 : return it->second;
375 : : }
376 : :
377 : 21376 : bool Skolemize::isInductionTerm(const Options& opts, Node n)
378 : : {
379 : 42752 : TypeNode tn = n.getType();
380 [ + + ][ + + ]: 21376 : if (opts.quantifiers.dtStcInduction && tn.isDatatype())
[ + + ]
381 : : {
382 : 11935 : const DType& dt = tn.getDType();
383 : 11935 : return !dt.isCodatatype();
384 : : }
385 [ + + ][ + + ]: 9441 : if (opts.quantifiers.intWfInduction && tn.isInteger())
[ + + ]
386 : : {
387 : 2002 : return true;
388 : : }
389 : 7439 : return false;
390 : : }
391 : :
392 : 69 : void Skolemize::getSkolemTermVectors(
393 : : std::map<Node, std::vector<Node> >& sks) const
394 : : {
395 : 69 : std::unordered_map<Node, std::vector<Node>>::const_iterator itk;
396 [ + + ]: 75 : for (const auto& p : d_skolemized)
397 : : {
398 : 6 : Node q = p.first;
399 : 6 : itk = d_skolem_constants.find(q);
400 [ - + ][ - + ]: 6 : Assert(itk != d_skolem_constants.end());
[ - - ]
401 : 6 : sks[q].insert(sks[q].end(), itk->second.begin(), itk->second.end());
402 : : }
403 : 69 : }
404 : :
405 : 54899 : bool Skolemize::isProofEnabled() const
406 : : {
407 : 54899 : return d_env.isTheoryProofProducing();
408 : : }
409 : :
410 : : } // namespace quantifiers
411 : : } // namespace theory
412 : : } // namespace cvc5::internal
|
