Branch data Line data Source code
1 : : /******************************************************************************
2 : : * This file is part of the cvc5 project.
3 : : *
4 : : * Copyright (c) 2009-2026 by the authors listed in the file AUTHORS
5 : : * in the top-level source directory and their institutional affiliations.
6 : : * All rights reserved. See the file COPYING in the top-level source
7 : : * directory for licensing information.
8 : : * ****************************************************************************
9 : : *
10 : : * Implementation of QuantifiersRewriter class.
11 : : */
12 : :
13 : : #include "theory/quantifiers/quantifiers_rewriter.h"
14 : :
15 : : #include "expr/ascription_type.h"
16 : : #include "expr/bound_var_manager.h"
17 : : #include "expr/dtype.h"
18 : : #include "expr/dtype_cons.h"
19 : : #include "expr/elim_shadow_converter.h"
20 : : #include "expr/node_algorithm.h"
21 : : #include "expr/skolem_manager.h"
22 : : #include "expr/subtype_elim_node_converter.h"
23 : : #include "options/quantifiers_options.h"
24 : : #include "proof/conv_proof_generator.h"
25 : : #include "proof/proof.h"
26 : : #include "quantifiers_rewriter.h"
27 : : #include "theory/arith/arith_msum.h"
28 : : #include "theory/arith/arith_poly_norm.h"
29 : : #include "theory/booleans/theory_bool_rewriter.h"
30 : : #include "theory/datatypes/theory_datatypes_utils.h"
31 : : #include "theory/quantifiers/ematching/trigger.h"
32 : : #include "theory/quantifiers/extended_rewrite.h"
33 : : #include "theory/quantifiers/quant_split.h"
34 : : #include "theory/quantifiers/quantifiers_attributes.h"
35 : : #include "theory/quantifiers/skolemize.h"
36 : : #include "theory/quantifiers/term_database.h"
37 : : #include "theory/quantifiers/term_util.h"
38 : : #include "theory/rewriter.h"
39 : : #include "theory/strings/theory_strings_utils.h"
40 : : #include "theory/uf/theory_uf_rewriter.h"
41 : : #include "util/rational.h"
42 : :
43 : : using namespace std;
44 : : using namespace cvc5::internal::kind;
45 : : using namespace cvc5::context;
46 : :
47 : : namespace cvc5::internal {
48 : : namespace theory {
49 : : namespace quantifiers {
50 : :
51 : 0 : std::ostream& operator<<(std::ostream& out, RewriteStep s)
52 : : {
53 [ - - ][ - - ]: 0 : switch (s)
[ - - ][ - - ]
[ - - ][ - ]
54 : : {
55 : 0 : case COMPUTE_ELIM_SHADOW: out << "COMPUTE_ELIM_SHADOW"; break;
56 : 0 : case COMPUTE_ELIM_SYMBOLS: out << "COMPUTE_ELIM_SYMBOLS"; break;
57 : 0 : case COMPUTE_MINISCOPING: out << "COMPUTE_MINISCOPING"; break;
58 : 0 : case COMPUTE_AGGRESSIVE_MINISCOPING:
59 : 0 : out << "COMPUTE_AGGRESSIVE_MINISCOPING";
60 : 0 : break;
61 : 0 : case COMPUTE_PROCESS_TERMS: out << "COMPUTE_PROCESS_TERMS"; break;
62 : 0 : case COMPUTE_PRENEX: out << "COMPUTE_PRENEX"; break;
63 : 0 : case COMPUTE_VAR_ELIMINATION: out << "COMPUTE_VAR_ELIMINATION"; break;
64 : 0 : case COMPUTE_DT_VAR_EXPAND: out << "COMPUTE_DT_VAR_EXPAND"; break;
65 : 0 : case COMPUTE_COND_SPLIT: out << "COMPUTE_COND_SPLIT"; break;
66 : 0 : case COMPUTE_EXT_REWRITE: out << "COMPUTE_EXT_REWRITE"; break;
67 : 0 : default: out << "UnknownRewriteStep"; break;
68 : : }
69 : 0 : return out;
70 : : }
71 : :
72 : 135611 : QuantifiersRewriter::QuantifiersRewriter(NodeManager* nm,
73 : : Rewriter* r,
74 : 135611 : const Options& opts)
75 : 135611 : : TheoryRewriter(nm), d_rewriter(r), d_opts(opts)
76 : : {
77 : 135611 : registerProofRewriteRule(ProofRewriteRule::EXISTS_ELIM,
78 : : TheoryRewriteCtx::PRE_DSL);
79 : 135611 : registerProofRewriteRule(ProofRewriteRule::QUANT_UNUSED_VARS,
80 : : TheoryRewriteCtx::PRE_DSL);
81 : 135611 : registerProofRewriteRule(ProofRewriteRule::MACRO_QUANT_ELIM_SHADOW,
82 : : TheoryRewriteCtx::PRE_DSL);
83 : : // QUANT_MERGE_PRENEX is part of the reconstruction for
84 : : // MACRO_QUANT_MERGE_PRENEX
85 : 135611 : registerProofRewriteRule(ProofRewriteRule::MACRO_QUANT_MERGE_PRENEX,
86 : : TheoryRewriteCtx::PRE_DSL);
87 : 135611 : registerProofRewriteRule(ProofRewriteRule::MACRO_QUANT_PRENEX,
88 : : TheoryRewriteCtx::PRE_DSL);
89 : 135611 : registerProofRewriteRule(ProofRewriteRule::MACRO_QUANT_MINISCOPE,
90 : : TheoryRewriteCtx::PRE_DSL);
91 : : // QUANT_MINISCOPE_OR is part of the reconstruction for MACRO_QUANT_MINISCOPE
92 : 135611 : registerProofRewriteRule(ProofRewriteRule::MACRO_QUANT_PARTITION_CONNECTED_FV,
93 : : TheoryRewriteCtx::PRE_DSL);
94 : : // note ProofRewriteRule::QUANT_DT_SPLIT is done by a module dynamically with
95 : : // manual proof generation thus not registered here.
96 : 135611 : registerProofRewriteRule(ProofRewriteRule::MACRO_QUANT_VAR_ELIM_EQ,
97 : : TheoryRewriteCtx::PRE_DSL);
98 : 135611 : registerProofRewriteRule(ProofRewriteRule::MACRO_QUANT_VAR_ELIM_INEQ,
99 : : TheoryRewriteCtx::PRE_DSL);
100 : 135611 : registerProofRewriteRule(ProofRewriteRule::MACRO_QUANT_DT_VAR_EXPAND,
101 : : TheoryRewriteCtx::PRE_DSL);
102 : 135611 : registerProofRewriteRule(ProofRewriteRule::MACRO_QUANT_REWRITE_BODY,
103 : : TheoryRewriteCtx::PRE_DSL);
104 : 135611 : }
105 : :
106 : 636827 : Node QuantifiersRewriter::rewriteViaRule(ProofRewriteRule id, const Node& n)
107 : : {
108 [ + + ][ + + ]: 636827 : switch (id)
[ + + ][ + + ]
[ + + ][ + + ]
[ + + ][ - ]
109 : : {
110 : 505474 : case ProofRewriteRule::MACRO_QUANT_ELIM_SHADOW:
111 : : {
112 [ + - ]: 505474 : if (n.isClosure())
113 : : {
114 : 505474 : Node ns = ElimShadowNodeConverter::eliminateShadow(n);
115 [ + + ]: 505474 : if (ns != n)
116 : : {
117 [ + - ]: 496 : Trace("quant-rewrite-proof")
118 : 248 : << "Rewrite " << n << " to " << ns << std::endl;
119 : 248 : return ns;
120 : : }
121 [ + + ]: 505474 : }
122 : 505226 : return Node::null();
123 : : }
124 : 20860 : case ProofRewriteRule::EXISTS_ELIM:
125 : : {
126 [ + + ]: 20860 : if (n.getKind() != Kind::EXISTS)
127 : : {
128 : 18067 : return Node::null();
129 : : }
130 : 2793 : std::vector<Node> fchildren;
131 : 2793 : fchildren.push_back(n[0]);
132 : 2793 : fchildren.push_back(n[1].notNode());
133 [ + + ]: 2793 : if (n.getNumChildren() == 3)
134 : : {
135 : 10 : fchildren.push_back(n[2]);
136 : : }
137 : 2793 : return d_nm->mkNode(Kind::NOT, d_nm->mkNode(Kind::FORALL, fchildren));
138 : 2793 : }
139 : 22849 : case ProofRewriteRule::QUANT_UNUSED_VARS:
140 : : {
141 [ - + ]: 22849 : if (!n.isClosure())
142 : : {
143 : 11224 : return Node::null();
144 : : }
145 : 45698 : std::vector<Node> vars(n[0].begin(), n[0].end());
146 : 22849 : std::vector<Node> activeVars;
147 : 22849 : computeArgVec(vars, activeVars, n[1]);
148 [ + + ]: 22849 : if (activeVars.size() < vars.size())
149 : : {
150 [ + + ]: 11224 : if (activeVars.empty())
151 : : {
152 : 2502 : return n[1];
153 : : }
154 : : return d_nm->mkNode(
155 : 8722 : n.getKind(), d_nm->mkNode(Kind::BOUND_VAR_LIST, activeVars), n[1]);
156 : : }
157 [ + + ][ + + ]: 34073 : }
158 : 11625 : break;
159 : 15871 : case ProofRewriteRule::MACRO_QUANT_MERGE_PRENEX:
160 : : case ProofRewriteRule::QUANT_MERGE_PRENEX:
161 : : {
162 [ - + ]: 15871 : if (!n.isClosure())
163 : : {
164 : 1559 : return Node::null();
165 : : }
166 : : // Don't check standard here, which can't be replicated in a proof checker
167 : : // without modelling the patterns.
168 : : // We remove duplicates if the macro version.
169 : : Node q = mergePrenex(
170 : 15871 : n, false, id == ProofRewriteRule::MACRO_QUANT_MERGE_PRENEX);
171 [ + + ]: 15871 : if (q != n)
172 : : {
173 : 1559 : return q;
174 : : }
175 [ + + ]: 15871 : }
176 : 14312 : break;
177 : 14557 : case ProofRewriteRule::MACRO_QUANT_PRENEX:
178 : : {
179 [ + - ]: 14557 : if (n.getKind() == Kind::FORALL)
180 : : {
181 : 14557 : std::vector<Node> args, nargs;
182 : 29114 : Node nn = computePrenex(n, n[1], args, nargs, true, false);
183 [ - + ][ - + ]: 14557 : Assert(nargs.empty());
[ - - ]
184 [ + + ]: 14557 : if (!args.empty())
185 : : {
186 : 2654 : std::vector<Node> qargs(n[0].begin(), n[0].end());
187 : 1327 : qargs.insert(qargs.end(), args.begin(), args.end());
188 : 1327 : Node bvl = d_nm->mkNode(Kind::BOUND_VAR_LIST, qargs);
189 : 1327 : return d_nm->mkNode(Kind::FORALL, bvl, nn);
190 : 1327 : }
191 [ + + ][ + + ]: 17211 : }
[ + + ]
192 : : }
193 : 13230 : break;
194 : 15447 : case ProofRewriteRule::MACRO_QUANT_MINISCOPE:
195 : : {
196 [ - + ]: 15447 : if (n.getKind() != Kind::FORALL)
197 : : {
198 : 15406 : return Node::null();
199 : : }
200 : 15447 : Kind k = n[1].getKind();
201 [ + + ][ + + ]: 15447 : if (k != Kind::AND && k != Kind::ITE)
202 : : {
203 : 10459 : return Node::null();
204 : : }
205 : : // note that qa is not needed; moreover external proofs should be agnostic
206 : : // to it
207 : 4988 : QAttributes qa;
208 : 4988 : QuantAttributes::computeQuantAttributes(n, qa);
209 : 4988 : Node nret = computeMiniscoping(n, qa, true, false);
210 [ + + ]: 4988 : if (nret != n)
211 : : {
212 : 4947 : return nret;
213 : : }
214 [ + + ][ + + ]: 9935 : }
215 : 41 : break;
216 : 2231 : case ProofRewriteRule::QUANT_MINISCOPE_AND:
217 : : {
218 [ + - ][ - + ]: 2231 : if (n.getKind() != Kind::FORALL || n[1].getKind() != Kind::AND)
[ + - ][ - + ]
[ - - ]
219 : : {
220 : 0 : return Node::null();
221 : : }
222 : 2231 : std::vector<Node> conj;
223 [ + + ]: 7986 : for (const Node& nc : n[1])
224 : : {
225 : 5755 : conj.push_back(d_nm->mkNode(Kind::FORALL, n[0], nc));
226 : 7986 : }
227 : 2231 : return d_nm->mkAnd(conj);
228 : 2231 : }
229 : : break;
230 : 12246 : case ProofRewriteRule::MACRO_QUANT_PARTITION_CONNECTED_FV:
231 : : {
232 [ + - ][ + + ]: 12246 : if (n.getKind() != Kind::FORALL || n[1].getKind() != Kind::OR)
[ + - ][ + + ]
[ - - ]
233 : : {
234 : 15358 : return Node::null();
235 : : }
236 : : // note that qa is not needed; moreover external proofs should be agnostic
237 : : // to it
238 : 7120 : QAttributes qa;
239 : 7120 : QuantAttributes::computeQuantAttributes(n, qa);
240 : 14240 : std::vector<Node> vars(n[0].begin(), n[0].end());
241 : 7120 : Node body = n[1];
242 : 7120 : Node nret = computeSplit(vars, body);
243 [ + + ]: 7120 : if (!nret.isNull())
244 : : {
245 : : // only do this rule if it is a proper split; otherwise it will be
246 : : // subsumed by QUANT_UNUSED_VARS.
247 [ + + ]: 5160 : if (nret.getKind() == Kind::OR)
248 : : {
249 : 5106 : return nret;
250 : : }
251 : : }
252 [ + + ][ + + ]: 22438 : }
[ + + ][ + + ]
253 : 2014 : break;
254 : 1001 : case ProofRewriteRule::QUANT_MINISCOPE_OR:
255 : : {
256 [ + - ][ - + ]: 1001 : if (n.getKind() != Kind::FORALL || n[1].getKind() != Kind::OR)
[ + - ][ - + ]
[ - - ]
257 : : {
258 : 0 : return Node::null();
259 : : }
260 : 1001 : size_t nvars = n[0].getNumChildren();
261 : 1001 : std::vector<Node> disj;
262 : 1001 : std::unordered_set<Node> varsUsed;
263 : 1001 : size_t varIndex = 0;
264 [ + + ]: 5623 : for (const Node& d : n[1])
265 : : {
266 : : // Note that we may apply to a nested quantified formula, in which
267 : : // case some variables in fvs may not be bound by this quantified
268 : : // formula.
269 : 4622 : std::unordered_set<Node> fvs;
270 : 4622 : expr::getFreeVariables(d, fvs);
271 : 4622 : size_t prevVarIndex = varIndex;
272 : 6924 : while (varIndex < nvars && fvs.find(n[0][varIndex]) != fvs.end())
273 : : {
274 : : // cannot have shadowing
275 [ - + ]: 2302 : if (varsUsed.find(n[0][varIndex]) != varsUsed.end())
276 : : {
277 : 0 : return Node::null();
278 : : }
279 : 2302 : varsUsed.insert(n[0][varIndex]);
280 : 2302 : varIndex++;
281 : : }
282 : 9244 : std::vector<Node> dvs(n[0].begin() + prevVarIndex,
283 : 13866 : n[0].begin() + varIndex);
284 [ + + ]: 4622 : if (dvs.empty())
285 : : {
286 : 3436 : disj.emplace_back(d);
287 : : }
288 : : else
289 : : {
290 : 1186 : Node bvl = d_nm->mkNode(Kind::BOUND_VAR_LIST, dvs);
291 : 1186 : disj.emplace_back(d_nm->mkNode(Kind::FORALL, bvl, d));
292 : 1186 : }
293 [ + - ][ + - ]: 5623 : }
[ + - ]
294 : : // must consume all variables
295 [ + + ]: 1001 : if (varIndex != nvars)
296 : : {
297 : 26 : return Node::null();
298 : : }
299 : 975 : Node ret = d_nm->mkOr(disj);
300 : : // go back and ensure all variables are bound
301 : 975 : std::unordered_set<Node> fvs;
302 : 975 : expr::getFreeVariables(ret, fvs);
303 [ + + ]: 3277 : for (const Node& v : n[0])
304 : : {
305 [ - + ]: 2302 : if (fvs.find(v) != fvs.end())
306 : : {
307 : 0 : return Node::null();
308 : : }
309 [ + - ][ + - ]: 3277 : }
310 : 975 : return ret;
311 : 1001 : }
312 : : break;
313 : 63 : case ProofRewriteRule::QUANT_MINISCOPE_ITE:
314 : : {
315 [ + - ][ - + ]: 63 : if (n.getKind() != Kind::FORALL || n[1].getKind() != Kind::ITE)
[ + - ][ - + ]
[ - - ]
316 : : {
317 : 63 : return Node::null();
318 : : }
319 : 126 : std::vector<Node> args(n[0].begin(), n[0].end());
320 : 63 : Node body = n[1];
321 [ + - ]: 63 : if (!expr::hasSubterm(body[0], args))
322 : : {
323 : 252 : return d_nm->mkNode(Kind::ITE,
324 : : {body[0],
325 : 126 : d_nm->mkNode(Kind::FORALL, n[0], body[1]),
326 [ + + ][ - - ]: 441 : d_nm->mkNode(Kind::FORALL, n[0], body[2])});
327 : : }
328 [ - + ][ - + ]: 126 : }
329 : 0 : break;
330 : 31 : case ProofRewriteRule::QUANT_DT_SPLIT:
331 : : {
332 : : // always runs split utility on the first variable
333 : 31 : if (n.getKind() != Kind::FORALL || !n[0][0].getType().isDatatype())
334 : : {
335 : 0 : return Node::null();
336 : : }
337 : 31 : return QuantDSplit::split(nodeManager(), n, 0);
338 : : }
339 : : break;
340 : 5697 : case ProofRewriteRule::MACRO_QUANT_DT_VAR_EXPAND:
341 : : {
342 [ - + ]: 5697 : if (n.getKind() != Kind::FORALL)
343 : : {
344 : 0 : return Node::null();
345 : : }
346 : : size_t index;
347 : 5697 : Node nn = computeDtVarExpand(nodeManager(), n, index);
348 [ + + ]: 5697 : if (nn != n)
349 : : {
350 : 57 : return nn;
351 : : }
352 : 5640 : return Node::null();
353 : 5697 : }
354 : : break;
355 : 14629 : case ProofRewriteRule::MACRO_QUANT_VAR_ELIM_EQ:
356 : : case ProofRewriteRule::QUANT_VAR_ELIM_EQ:
357 : : case ProofRewriteRule::MACRO_QUANT_VAR_ELIM_INEQ:
358 : : {
359 [ + - ][ + + ]: 14629 : if (n.getKind() != Kind::FORALL || n.getNumChildren() != 2)
[ + + ]
360 : : {
361 : 10943 : return Node::null();
362 : : }
363 [ + - ]: 26322 : Trace("quant-rewrite-proof")
364 : 13161 : << "Var elim rewrite " << n << ", id " << id << "?" << std::endl;
365 : 26322 : std::vector<Node> args(n[0].begin(), n[0].end());
366 : 13161 : std::vector<Node> vars;
367 : 13161 : std::vector<Node> subs;
368 : 13161 : Node body = n[1];
369 [ + + ]: 13161 : if (id == ProofRewriteRule::MACRO_QUANT_VAR_ELIM_EQ)
370 : : {
371 : 7019 : std::vector<Node> lits;
372 : 7019 : getVarElim(body, args, vars, subs, lits);
373 : 7019 : }
374 [ + + ]: 6142 : else if (id == ProofRewriteRule::QUANT_VAR_ELIM_EQ)
375 : : {
376 [ - + ]: 736 : if (args.size() != 1)
377 : : {
378 : 0 : return Node::null();
379 : : }
380 : 736 : std::vector<Node> lits;
381 [ + - ]: 736 : if (body.getKind() == Kind::OR)
382 : : {
383 : 736 : lits.insert(lits.end(), body.begin(), body.end());
384 : : }
385 : : else
386 : : {
387 : 0 : lits.push_back(body);
388 : : }
389 : 736 : if (lits[0].getKind() != Kind::NOT
390 [ + - ][ - + ]: 1472 : || lits[0][0].getKind() != Kind::EQUAL)
[ + - ][ - + ]
[ - - ]
391 : : {
392 : 0 : return Node::null();
393 : : }
394 : 736 : Node eq = lits[0][0];
395 : 736 : if (eq[0] != args[0] || expr::hasSubterm(eq[1], eq[0]))
396 : : {
397 : 0 : return Node::null();
398 : : }
399 : 736 : vars.push_back(eq[0]);
400 : 736 : subs.push_back(eq[1]);
401 : 736 : args.clear();
402 : 736 : std::vector<Node> remLits(lits.begin() + 1, lits.end());
403 : 736 : body = d_nm->mkOr(remLits);
404 [ + - ][ + - ]: 736 : }
405 : : else
406 : : {
407 [ - + ][ - + ]: 5406 : Assert(id == ProofRewriteRule::MACRO_QUANT_VAR_ELIM_INEQ);
[ - - ]
408 : : // assume empty attribute
409 : 5406 : QAttributes qa;
410 : 5406 : Node ret = getVarElimIneq(n[1], args, qa);
411 [ + + ][ + + ]: 5406 : if (!ret.isNull() && !args.empty())
[ + + ]
412 : : {
413 : 45 : Node vlist = d_nm->mkNode(Kind::BOUND_VAR_LIST, args);
414 : 45 : ret = d_nm->mkNode(Kind::FORALL, vlist, ret);
415 : 45 : }
416 : 5406 : return ret;
417 : 5406 : }
418 : : // if we eliminated a variable, update body and reprocess
419 [ + + ]: 7755 : if (!vars.empty())
420 : : {
421 : : // ensure the substitution is safe
422 [ + + ]: 5202 : for (const Node& s : subs)
423 : : {
424 [ - + ]: 2601 : if (!isSafeSubsTerm(body, s))
425 : : {
426 : 0 : return Node::null();
427 : : }
428 : : }
429 [ - + ][ - + ]: 2601 : Assert(vars.size() == subs.size());
[ - - ]
430 : 2601 : std::vector<Node> qc(n.begin(), n.end());
431 : 2601 : qc[1] =
432 : 5202 : body.substitute(vars.begin(), vars.end(), subs.begin(), subs.end());
433 [ + - ]: 5202 : Trace("quant-rewrite-proof")
434 : 2601 : << "...returns body " << qc[1] << std::endl;
435 [ + + ]: 2601 : if (args.empty())
436 : : {
437 : 1594 : return qc[1];
438 : : }
439 : 1007 : qc[0] = d_nm->mkNode(Kind::BOUND_VAR_LIST, args);
440 : 1007 : return d_nm->mkNode(Kind::FORALL, qc);
441 : 2601 : }
442 [ + + ][ + + ]: 37182 : }
[ + + ][ + + ]
443 : 5154 : break;
444 : 5871 : case ProofRewriteRule::MACRO_QUANT_REWRITE_BODY:
445 : : {
446 [ - + ]: 5871 : if (n.getKind() != Kind::FORALL)
447 : : {
448 : 888 : return Node::null();
449 : : }
450 : 5871 : Node nr = computeRewriteBody(n);
451 [ + + ]: 5871 : if (nr != n)
452 : : {
453 : 888 : return nr;
454 : : }
455 [ + + ]: 5871 : }
456 : 4983 : break;
457 : 0 : default: break;
458 : : }
459 : 51359 : return Node::null();
460 : : }
461 : :
462 : 66063 : bool QuantifiersRewriter::isLiteral(Node n)
463 : : {
464 [ - - ][ + + ]: 66063 : switch (n.getKind())
465 : : {
466 : 0 : case Kind::NOT:
467 : 0 : return n[0].getKind() != Kind::NOT && isLiteral(n[0]);
468 : : break;
469 : 0 : case Kind::OR:
470 : : case Kind::AND:
471 : : case Kind::IMPLIES:
472 : : case Kind::XOR:
473 : 0 : case Kind::ITE: return false; break;
474 : 31655 : case Kind::EQUAL:
475 : : // for boolean terms
476 : 31655 : return !n[0].getType().isBoolean();
477 : : break;
478 : 34408 : default: break;
479 : : }
480 : 34408 : return true;
481 : : }
482 : :
483 : 29273371 : void QuantifiersRewriter::computeArgs(const std::vector<Node>& args,
484 : : std::map<Node, bool>& activeMap,
485 : : Node n,
486 : : std::map<Node, bool>& visited)
487 : : {
488 [ + + ]: 29273371 : if (visited.find(n) == visited.end())
489 : : {
490 : 20360855 : visited[n] = true;
491 [ + + ]: 20360855 : if (n.getKind() == Kind::BOUND_VARIABLE)
492 : : {
493 [ + + ]: 3525326 : if (std::find(args.begin(), args.end(), n) != args.end())
494 : : {
495 : 2721036 : activeMap[n] = true;
496 : : }
497 : : }
498 : : else
499 : : {
500 [ + + ]: 16835529 : if (n.hasOperator())
501 : : {
502 : 9421533 : computeArgs(args, activeMap, n.getOperator(), visited);
503 : : }
504 [ + + ]: 35141786 : for (int i = 0; i < (int)n.getNumChildren(); i++)
505 : : {
506 : 18306257 : computeArgs(args, activeMap, n[i], visited);
507 : : }
508 : : }
509 : : }
510 : 29273371 : }
511 : :
512 : 774156 : void QuantifiersRewriter::computeArgVec(const std::vector<Node>& args,
513 : : std::vector<Node>& activeArgs,
514 : : Node n)
515 : : {
516 [ - + ][ - + ]: 774156 : Assert(activeArgs.empty());
[ - - ]
517 : 774156 : std::map<Node, bool> activeMap;
518 : 774156 : std::map<Node, bool> visited;
519 : 774156 : computeArgs(args, activeMap, n, visited);
520 [ + + ]: 774156 : if (!activeMap.empty())
521 : : {
522 : 757321 : std::map<Node, bool>::iterator it;
523 [ + + ]: 28419751 : for (const Node& v : args)
524 : : {
525 : 27662430 : it = activeMap.find(v);
526 [ + + ]: 27662430 : if (it != activeMap.end())
527 : : {
528 : 1786795 : activeArgs.emplace_back(v);
529 : : // no longer active, which accounts for deleting duplicates
530 : 1786795 : activeMap.erase(it);
531 : : }
532 : : }
533 : : }
534 : 774156 : }
535 : :
536 : 386052 : void QuantifiersRewriter::computeArgVec2(const std::vector<Node>& args,
537 : : std::vector<Node>& activeArgs,
538 : : Node n,
539 : : Node ipl)
540 : : {
541 [ - + ][ - + ]: 386052 : Assert(activeArgs.empty());
[ - - ]
542 : 386052 : std::map<Node, bool> activeMap;
543 : 386052 : std::map<Node, bool> visited;
544 : 386052 : computeArgs(args, activeMap, n, visited);
545 : : // Collect variables in inst pattern list only if we cannot eliminate
546 : : // quantifier, or if we have an add-to-pool annotation.
547 : 386052 : bool varComputePatList = !activeMap.empty();
548 [ + + ]: 387431 : for (const Node& ip : ipl)
549 : : {
550 : 1379 : Kind k = ip.getKind();
551 [ + - ][ - + ]: 1379 : if (k == Kind::INST_ADD_TO_POOL || k == Kind::SKOLEM_ADD_TO_POOL)
552 : : {
553 : 0 : varComputePatList = true;
554 : 0 : break;
555 : : }
556 [ + - ]: 1379 : }
557 [ + + ]: 386052 : if (varComputePatList)
558 : : {
559 : 385373 : computeArgs(args, activeMap, ipl, visited);
560 : : }
561 [ + + ]: 386052 : if (!activeMap.empty())
562 : : {
563 [ + + ]: 1324343 : for (const Node& a : args)
564 : : {
565 [ + + ]: 938970 : if (activeMap.find(a) != activeMap.end())
566 : : {
567 : 934241 : activeArgs.push_back(a);
568 : : }
569 : : }
570 : : }
571 : 386052 : }
572 : :
573 : 760677 : RewriteResponse QuantifiersRewriter::preRewrite(TNode q)
574 : : {
575 : 760677 : Kind k = q.getKind();
576 [ + + ][ + + ]: 760677 : if (k == Kind::FORALL || k == Kind::EXISTS)
577 : : {
578 : : // Do prenex merging now, since this may impact trigger selection.
579 : : // In particular consider:
580 : : // (forall ((x Int)) (forall ((y Int)) (! (P x) :pattern ((f x)))))
581 : : // If we wait until post-rewrite, we would rewrite the inner quantified
582 : : // formula, dropping the pattern, so the entire formula becomes:
583 : : // (forall ((x Int)) (P x))
584 : : // Instead, we merge to:
585 : : // (forall ((x Int) (y Int)) (! (P x) :pattern ((f x))))
586 : : // eagerly here, where after we would drop y to obtain:
587 : : // (forall ((x Int)) (! (P x) :pattern ((f x))))
588 : : // See issue #10303.
589 : 500079 : Node qm = mergePrenex(q, true, true);
590 [ + + ]: 500079 : if (q != qm)
591 : : {
592 : 3741 : return RewriteResponse(REWRITE_AGAIN_FULL, qm);
593 : : }
594 [ + + ]: 500079 : }
595 : 756936 : return RewriteResponse(REWRITE_DONE, q);
596 : : }
597 : :
598 : 763009 : RewriteResponse QuantifiersRewriter::postRewrite(TNode in)
599 : : {
600 [ + - ]: 763009 : Trace("quantifiers-rewrite-debug") << "post-rewriting " << in << std::endl;
601 : 763009 : RewriteStatus status = REWRITE_DONE;
602 : 763009 : Node ret = in;
603 : 763009 : RewriteStep rew_op = COMPUTE_LAST;
604 : : // get the body
605 [ + + ]: 763009 : if (in.getKind() == Kind::EXISTS)
606 : : {
607 : 8407 : std::vector<Node> children;
608 : 8407 : children.push_back(in[0]);
609 : 8407 : children.push_back(in[1].notNode());
610 [ + + ]: 8407 : if (in.getNumChildren() == 3)
611 : : {
612 : 71 : children.push_back(in[2]);
613 : : }
614 : 8407 : ret = nodeManager()->mkNode(Kind::FORALL, children);
615 : 8407 : ret = ret.negate();
616 : 8407 : status = REWRITE_AGAIN_FULL;
617 : 8407 : }
618 [ + + ]: 754602 : else if (in.getKind() == Kind::FORALL)
619 : : {
620 : : // do prenex merging
621 : 492824 : ret = mergePrenex(in, true, true);
622 [ + + ]: 492824 : if (ret != in)
623 : : {
624 : 60 : status = REWRITE_AGAIN_FULL;
625 : : }
626 [ + + ][ + + ]: 492764 : else if (in[1].isConst() && in.getNumChildren() == 2)
[ + - ][ + + ]
[ - - ]
627 : : {
628 : 2184 : return RewriteResponse(status, in[1]);
629 : : }
630 : : else
631 : : {
632 : : // compute attributes
633 : 490580 : QAttributes qa;
634 : 490580 : QuantAttributes::computeQuantAttributes(in, qa);
635 [ + + ]: 4862229 : for (unsigned i = 0; i < COMPUTE_LAST; ++i)
636 : : {
637 : 4440945 : RewriteStep op = static_cast<RewriteStep>(i);
638 [ + + ]: 4440945 : if (doOperation(in, op, qa))
639 : : {
640 : 3426352 : ret = computeOperation(in, op, qa);
641 [ + + ]: 3426352 : if (ret != in)
642 : : {
643 : 69296 : rew_op = op;
644 : 69296 : status = REWRITE_AGAIN_FULL;
645 : 69296 : break;
646 : : }
647 : : }
648 : : }
649 : 490580 : }
650 : : }
651 : : // print if changed
652 [ + + ]: 760825 : if (in != ret)
653 : : {
654 [ + - ]: 155526 : Trace("quantifiers-rewrite")
655 : 77763 : << "*** rewrite (op=" << rew_op << ") " << in << std::endl;
656 [ + - ]: 77763 : Trace("quantifiers-rewrite") << " to " << std::endl;
657 [ + - ]: 77763 : Trace("quantifiers-rewrite") << ret << std::endl;
658 : : }
659 : 760825 : return RewriteResponse(status, ret);
660 : 763009 : }
661 : :
662 : 1008774 : Node QuantifiersRewriter::mergePrenex(const Node& q, bool checkStd, bool rmDup)
663 : : {
664 [ + + ][ + - ]: 1008774 : Assert(q.getKind() == Kind::FORALL || q.getKind() == Kind::EXISTS);
[ - + ][ - + ]
[ - - ]
665 : 1008774 : Kind k = q.getKind();
666 : 1008774 : std::vector<Node> boundVars;
667 : 1008774 : Node body = q;
668 : 1008774 : bool combineQuantifiers = false;
669 : 1008774 : bool continueCombine = false;
670 [ + + ]: 1023046 : do
671 : : {
672 [ + + ]: 1023046 : if (rmDup)
673 : : {
674 [ + + ]: 3563265 : for (const Node& v : body[0])
675 : : {
676 [ + + ]: 2542316 : if (std::find(boundVars.begin(), boundVars.end(), v) == boundVars.end())
677 : : {
678 : 2542103 : boundVars.push_back(v);
679 : : }
680 : : else
681 : : {
682 : : // if duplicate variable due to shadowing, we must rewrite
683 : 213 : combineQuantifiers = true;
684 : : }
685 : 3563265 : }
686 : : }
687 : : else
688 : : {
689 : 2097 : boundVars.insert(boundVars.end(), body[0].begin(), body[0].end());
690 : : }
691 : 1023046 : continueCombine = false;
692 [ + + ][ + + ]: 1023046 : if (body.getNumChildren() == 2 && body[1].getKind() == k)
[ + + ][ + + ]
[ - - ]
693 : : {
694 : 14272 : bool process = true;
695 [ + + ]: 14272 : if (checkStd)
696 : : {
697 : : // Should never combine a quantified formula with a pool or
698 : : // non-standard quantified formula here.
699 : : // Note that we technically should check
700 : : // doOperation(body[1], COMPUTE_PRENEX, qa) here, although this
701 : : // is too restrictive, as sometimes nested patterns should just be
702 : : // applied to the top level, for example:
703 : : // (forall ((x Int)) (forall ((y Int)) (! P :pattern ((f x y)))))
704 : : // should be a pattern for the top-level quantifier here.
705 : 11175 : QAttributes qa;
706 : 11175 : QuantAttributes::computeQuantAttributes(body[1], qa);
707 : 11175 : process = qa.isStandard();
708 : 11175 : }
709 [ + - ]: 14272 : if (process)
710 : : {
711 : 14272 : body = body[1];
712 : 14272 : continueCombine = true;
713 : 14272 : combineQuantifiers = true;
714 : : }
715 : : }
716 : : } while (continueCombine);
717 [ + + ]: 1008774 : if (combineQuantifiers)
718 : : {
719 : 5360 : NodeManager* nm = nodeManager();
720 : 5360 : std::vector<Node> children;
721 : 5360 : children.push_back(nm->mkNode(Kind::BOUND_VAR_LIST, boundVars));
722 : 5360 : children.push_back(body[1]);
723 [ + + ]: 5360 : if (body.getNumChildren() == 3)
724 : : {
725 : 243 : children.push_back(body[2]);
726 : : }
727 : 5360 : return nm->mkNode(k, children);
728 : 5360 : }
729 : 1003414 : return q;
730 : 1008774 : }
731 : :
732 : 55 : void QuantifiersRewriter::computeDtTesterIteSplit(
733 : : Node n,
734 : : std::map<Node, Node>& pcons,
735 : : std::map<Node, std::map<int, Node>>& ncons,
736 : : std::vector<Node>& conj) const
737 : : {
738 [ + - ][ + + ]: 75 : if (n.getKind() == Kind::ITE && n[0].getKind() == Kind::APPLY_TESTER
[ - - ]
739 : 75 : && n[1].getType().isBoolean())
740 : : {
741 [ + - ]: 40 : Trace("quantifiers-rewrite-ite-debug")
742 : 20 : << "Split tester condition : " << n << std::endl;
743 : 20 : Node x = n[0][0];
744 : 20 : std::map<Node, Node>::iterator itp = pcons.find(x);
745 [ - + ]: 20 : if (itp != pcons.end())
746 : : {
747 [ - - ]: 0 : Trace("quantifiers-rewrite-ite-debug")
748 : 0 : << "...condition already set " << itp->second << std::endl;
749 : 0 : computeDtTesterIteSplit(
750 [ - - ]: 0 : n[itp->second == n[0] ? 1 : 2], pcons, ncons, conj);
751 : : }
752 : : else
753 : : {
754 : 20 : Node tester = n[0].getOperator();
755 : 20 : int index = datatypes::utils::indexOf(tester);
756 : 20 : std::map<int, Node>::iterator itn = ncons[x].find(index);
757 [ - + ]: 20 : if (itn != ncons[x].end())
758 : : {
759 [ - - ]: 0 : Trace("quantifiers-rewrite-ite-debug")
760 : 0 : << "...condition negated " << itn->second << std::endl;
761 : 0 : computeDtTesterIteSplit(n[2], pcons, ncons, conj);
762 : : }
763 : : else
764 : : {
765 [ + + ]: 60 : for (unsigned i = 0; i < 2; i++)
766 : : {
767 [ + + ]: 40 : if (i == 0)
768 : : {
769 : 20 : pcons[x] = n[0];
770 : : }
771 : : else
772 : : {
773 : 20 : pcons.erase(x);
774 : 20 : ncons[x][index] = n[0].negate();
775 : : }
776 : 40 : computeDtTesterIteSplit(n[i + 1], pcons, ncons, conj);
777 : : }
778 : 20 : ncons[x].erase(index);
779 : : }
780 : 20 : }
781 : 20 : }
782 : : else
783 : : {
784 : 35 : NodeManager* nm = nodeManager();
785 [ + - ]: 70 : Trace("quantifiers-rewrite-ite-debug")
786 : 35 : << "Return value : " << n << std::endl;
787 : 35 : std::vector<Node> children;
788 : 35 : children.push_back(n);
789 : 35 : std::vector<Node> vars;
790 : : // add all positive testers
791 [ + + ]: 55 : for (std::map<Node, Node>::iterator it = pcons.begin(); it != pcons.end();
792 : 20 : ++it)
793 : : {
794 : 20 : children.push_back(it->second.negate());
795 : 20 : vars.push_back(it->first);
796 : : }
797 : : // add all negative testers
798 : 35 : for (std::map<Node, std::map<int, Node>>::iterator it = ncons.begin();
799 [ + + ]: 80 : it != ncons.end();
800 : 45 : ++it)
801 : : {
802 : 45 : Node x = it->first;
803 : : // only if we haven't settled on a positive tester
804 [ + + ]: 45 : if (std::find(vars.begin(), vars.end(), x) == vars.end())
805 : : {
806 : : // check if we have exhausted all options but one
807 : 25 : const DType& dt = x.getType().getDType();
808 : 25 : std::vector<Node> nchildren;
809 : 25 : int pos_cons = -1;
810 [ + + ]: 75 : for (int i = 0; i < (int)dt.getNumConstructors(); i++)
811 : : {
812 : 50 : std::map<int, Node>::iterator itt = it->second.find(i);
813 [ + + ]: 50 : if (itt == it->second.end())
814 : : {
815 [ + - ]: 25 : pos_cons = pos_cons == -1 ? i : -2;
816 : : }
817 : : else
818 : : {
819 : 25 : nchildren.push_back(itt->second.negate());
820 : : }
821 : : }
822 [ + - ]: 25 : if (pos_cons >= 0)
823 : : {
824 : 25 : Node tester = dt[pos_cons].getTester();
825 : 25 : children.push_back(
826 : 50 : nm->mkNode(Kind::APPLY_TESTER, tester, x).negate());
827 : 25 : }
828 : : else
829 : : {
830 : 0 : children.insert(children.end(), nchildren.begin(), nchildren.end());
831 : : }
832 : 25 : }
833 : 45 : }
834 : : // make condition/output pair
835 : 35 : Node c = children.size() == 1 ? children[0]
836 [ - + ]: 35 : : nodeManager()->mkNode(Kind::OR, children);
837 : 35 : conj.push_back(c);
838 : 35 : }
839 : 55 : }
840 : :
841 : 444607 : Node QuantifiersRewriter::computeProcessTerms(const Node& q,
842 : : const std::vector<Node>& args,
843 : : Node body,
844 : : QAttributes& qa,
845 : : TConvProofGenerator* pg) const
846 : : {
847 : 444607 : options::IteLiftQuantMode iteLiftMode = options::IteLiftQuantMode::NONE;
848 [ + + ]: 444607 : if (qa.isStandard())
849 : : {
850 : 425853 : iteLiftMode = d_opts.quantifiers.iteLiftQuant;
851 : : }
852 : 444607 : std::map<Node, Node> cache;
853 : 889214 : return computeProcessTerms2(q, args, body, cache, iteLiftMode, pg);
854 : 444607 : }
855 : :
856 : 11309198 : Node QuantifiersRewriter::computeProcessTerms2(
857 : : const Node& q,
858 : : const std::vector<Node>& args,
859 : : Node body,
860 : : std::map<Node, Node>& cache,
861 : : options::IteLiftQuantMode iteLiftMode,
862 : : TConvProofGenerator* pg) const
863 : : {
864 : 11309198 : NodeManager* nm = nodeManager();
865 [ + - ]: 22618396 : Trace("quantifiers-rewrite-term-debug2")
866 : 11309198 : << "computeProcessTerms " << body << std::endl;
867 : 11309198 : std::map<Node, Node>::iterator iti = cache.find(body);
868 [ + + ]: 11309198 : if (iti != cache.end())
869 : : {
870 : 3257083 : return iti->second;
871 : : }
872 : 8052115 : bool changed = false;
873 : 8052115 : std::vector<Node> children;
874 [ + + ]: 18916706 : for (const Node& bc : body)
875 : : {
876 : : // do the recursive call on children
877 : 10864591 : Node nn = computeProcessTerms2(q, args, bc, cache, iteLiftMode, pg);
878 : 10864591 : children.push_back(nn);
879 [ + + ][ + + ]: 10864591 : changed = changed || nn != bc;
880 : 10864591 : }
881 : :
882 : : // make return value
883 : 8052115 : Node ret;
884 [ + + ]: 8052115 : if (changed)
885 : : {
886 [ + + ]: 26660 : if (body.getMetaKind() == kind::metakind::PARAMETERIZED)
887 : : {
888 : 469 : children.insert(children.begin(), body.getOperator());
889 : : }
890 : 26660 : ret = nm->mkNode(body.getKind(), children);
891 : : }
892 : : else
893 : : {
894 : 8025455 : ret = body;
895 : : }
896 : :
897 : 8052115 : Node retOrig = ret;
898 [ + - ]: 16104230 : Trace("quantifiers-rewrite-term-debug2")
899 : 8052115 : << "Returning " << ret << " for " << body << std::endl;
900 : : // do context-independent rewriting
901 : 8052115 : if (ret.getKind() == Kind::EQUAL
902 [ + + ][ + + ]: 8052115 : && iteLiftMode != options::IteLiftQuantMode::NONE)
[ + + ]
903 : : {
904 [ + + ]: 2933487 : for (size_t i = 0; i < 2; i++)
905 : : {
906 [ + + ]: 1956378 : if (ret[i].getKind() == Kind::ITE)
907 : : {
908 [ + + ]: 104785 : Node no = i == 0 ? ret[1] : ret[0];
909 [ + + ]: 104785 : if (no.getKind() != Kind::ITE)
910 : : {
911 : 96371 : bool doRewrite = (iteLiftMode == options::IteLiftQuantMode::ALL);
912 : 96371 : std::vector<Node> childrenIte;
913 : 96371 : childrenIte.push_back(ret[i][0]);
914 [ + + ]: 289113 : for (size_t j = 1; j <= 2; j++)
915 : : {
916 : : // check if it rewrites to a constant
917 : 385484 : Node nn = nm->mkNode(Kind::EQUAL, no, ret[i][j]);
918 : 192742 : childrenIte.push_back(nn);
919 : : // check if it will rewrite to a constant
920 : 192742 : if (no == ret[i][j] || (no.isConst() && ret[i][j].isConst()))
921 : : {
922 : 1681 : doRewrite = true;
923 : : }
924 : 192742 : }
925 [ + + ]: 96371 : if (doRewrite)
926 : : {
927 : 1296 : ret = nm->mkNode(Kind::ITE, childrenIte);
928 : 1296 : break;
929 : : }
930 [ + + ]: 96371 : }
931 [ + + ]: 104785 : }
932 : : }
933 : : }
934 [ + + ][ + + ]: 7073710 : else if (ret.getKind() == Kind::SELECT && ret[0].getKind() == Kind::STORE)
[ + + ][ + + ]
[ - - ]
935 : : {
936 : 385 : Node st = ret[0];
937 : 385 : Node index = ret[1];
938 : 385 : std::vector<Node> iconds;
939 : 385 : std::vector<Node> elements;
940 [ + + ]: 1292 : while (st.getKind() == Kind::STORE)
941 : : {
942 : 907 : iconds.push_back(index.eqNode(st[1]));
943 : 907 : elements.push_back(st[2]);
944 : 907 : st = st[0];
945 : : }
946 : 385 : ret = nm->mkNode(Kind::SELECT, st, index);
947 : : // conditions
948 [ + + ]: 1292 : for (int i = (iconds.size() - 1); i >= 0; i--)
949 : : {
950 : 907 : ret = nm->mkNode(Kind::ITE, iconds[i], elements[i], ret);
951 : : }
952 : 385 : }
953 [ + + ][ + + ]: 7073325 : else if (ret.getKind() == Kind::HO_APPLY && !ret.getType().isFunction())
[ + + ][ + + ]
[ - - ]
954 : : {
955 : : // fully applied functions are converted to APPLY_UF here.
956 : 17083 : Node fullApp = uf::TheoryUfRewriter::getApplyUfForHoApply(ret);
957 : : // it may not be possible to convert e.g. if the head is not a variable
958 [ + + ]: 17083 : if (!fullApp.isNull())
959 : : {
960 : 17077 : ret = fullApp;
961 : : }
962 : 17083 : }
963 [ + + ]: 8052115 : if (pg != nullptr)
964 : : {
965 [ + + ]: 4679 : if (retOrig != ret)
966 : : {
967 : 446 : pg->addRewriteStep(retOrig,
968 : : ret,
969 : : nullptr,
970 : : false,
971 : : TrustId::MACRO_THEORY_REWRITE_RCONS_SIMPLE);
972 : : }
973 : : }
974 : 8052115 : cache[body] = ret;
975 : 8052115 : return ret;
976 : 8052115 : }
977 : :
978 : 34 : Node QuantifiersRewriter::computeExtendedRewrite(TNode q,
979 : : const QAttributes& qa) const
980 : : {
981 : : // do not apply to recursive functions
982 [ + + ]: 34 : if (qa.isFunDef())
983 : : {
984 : 8 : return q;
985 : : }
986 : 26 : Node body = q[1];
987 : : // apply extended rewriter
988 : 26 : Node bodyr = d_rewriter->extendedRewrite(body);
989 [ + + ]: 26 : if (body != bodyr)
990 : : {
991 : 6 : std::vector<Node> children;
992 : 6 : children.push_back(q[0]);
993 : 6 : children.push_back(bodyr);
994 [ - + ]: 6 : if (q.getNumChildren() == 3)
995 : : {
996 : 0 : children.push_back(q[2]);
997 : : }
998 : 6 : return nodeManager()->mkNode(Kind::FORALL, children);
999 : 6 : }
1000 : 20 : return q;
1001 : 26 : }
1002 : :
1003 : 421971 : Node QuantifiersRewriter::computeCondSplit(Node body,
1004 : : const std::vector<Node>& args,
1005 : : QAttributes& qa) const
1006 : : {
1007 : 421971 : NodeManager* nm = nodeManager();
1008 : 421971 : Kind bk = body.getKind();
1009 [ + + ]: 5206 : if (d_opts.quantifiers.iteDtTesterSplitQuant && bk == Kind::ITE
1010 [ + + ][ + + ]: 427177 : && body[0].getKind() == Kind::APPLY_TESTER)
[ + + ][ + + ]
[ - - ]
1011 : : {
1012 [ + - ]: 30 : Trace("quantifiers-rewrite-ite-debug")
1013 : 15 : << "DTT split : " << body << std::endl;
1014 : 15 : std::map<Node, Node> pcons;
1015 : 15 : std::map<Node, std::map<int, Node>> ncons;
1016 : 15 : std::vector<Node> conj;
1017 : 15 : computeDtTesterIteSplit(body, pcons, ncons, conj);
1018 [ - + ][ - + ]: 15 : Assert(!conj.empty());
[ - - ]
1019 [ + - ]: 15 : if (conj.size() > 1)
1020 : : {
1021 [ + - ]: 30 : Trace("quantifiers-rewrite-ite") << "*** Split ITE (datatype tester) "
1022 : 15 : << body << " into : " << std::endl;
1023 [ + + ]: 50 : for (unsigned i = 0; i < conj.size(); i++)
1024 : : {
1025 [ + - ]: 35 : Trace("quantifiers-rewrite-ite") << " " << conj[i] << std::endl;
1026 : : }
1027 : 15 : return nm->mkNode(Kind::AND, conj);
1028 : : }
1029 [ - + ][ - + ]: 45 : }
[ - + ]
1030 [ - + ]: 421956 : if (d_opts.quantifiers.condVarSplitQuant
1031 : : == options::CondVarSplitQuantMode::OFF)
1032 : : {
1033 : 0 : return body;
1034 : : }
1035 [ + - ]: 843912 : Trace("cond-var-split-debug")
1036 : 421956 : << "Conditional var elim split " << body << "?" << std::endl;
1037 : : // we only do this splitting if miniscoping is enabled, as this is
1038 : : // required to eliminate variables in conjuncts below. We also never
1039 : : // miniscope non-standard quantifiers, so this is also guarded here.
1040 [ + + ][ + + ]: 421956 : if (!doMiniscopeConj(d_opts) || !qa.isStandard())
[ + + ]
1041 : : {
1042 : 30278 : return body;
1043 : : }
1044 : :
1045 : 391678 : bool aggCondSplit = (d_opts.quantifiers.condVarSplitQuant
1046 : : == options::CondVarSplitQuantMode::AGG);
1047 : 391678 : if (bk == Kind::ITE
1048 : 391678 : || (bk == Kind::EQUAL && body[0].getType().isBoolean() && aggCondSplit))
1049 : : {
1050 [ - + ][ - + ]: 446 : Assert(!qa.isFunDef());
[ - - ]
1051 : 446 : bool do_split = false;
1052 : 446 : unsigned index_max = bk == Kind::ITE ? 0 : 1;
1053 : 446 : std::vector<Node> tmpArgs = args;
1054 [ + + ]: 778 : for (unsigned index = 0; index <= index_max; index++)
1055 : : {
1056 [ + + ][ - - ]: 446 : if (hasVarElim(body[index], true, tmpArgs)
1057 [ + + ][ - + ]: 446 : || hasVarElim(body[index], false, tmpArgs))
[ + + ][ + - ]
[ - - ]
1058 : : {
1059 : 114 : do_split = true;
1060 : 114 : break;
1061 : : }
1062 : : }
1063 [ + + ]: 446 : if (do_split)
1064 : : {
1065 : 114 : Node pos;
1066 : 114 : Node neg;
1067 [ + - ]: 114 : if (bk == Kind::ITE)
1068 : : {
1069 : 114 : pos = nm->mkNode(Kind::OR, body[0].negate(), body[1]);
1070 : 114 : neg = nm->mkNode(Kind::OR, body[0], body[2]);
1071 : : }
1072 : : else
1073 : : {
1074 : 0 : pos = nm->mkNode(Kind::OR, body[0].negate(), body[1]);
1075 : 0 : neg = nm->mkNode(Kind::OR, body[0], body[1].negate());
1076 : : }
1077 [ + - ]: 228 : Trace("cond-var-split-debug") << "*** Split (conditional variable eq) "
1078 : 114 : << body << " into : " << std::endl;
1079 [ + - ]: 114 : Trace("cond-var-split-debug") << " " << pos << std::endl;
1080 [ + - ]: 114 : Trace("cond-var-split-debug") << " " << neg << std::endl;
1081 : 114 : return nm->mkNode(Kind::AND, pos, neg);
1082 : 114 : }
1083 [ + + ]: 446 : }
1084 : :
1085 [ + + ]: 391564 : if (bk == Kind::OR)
1086 : : {
1087 : 186222 : unsigned size = body.getNumChildren();
1088 : 186222 : bool do_split = false;
1089 : 186222 : unsigned split_index = 0;
1090 [ + + ]: 750924 : for (unsigned i = 0; i < size; i++)
1091 : : {
1092 : : // check if this child is a (conditional) variable elimination
1093 : 565290 : Node b = body[i];
1094 [ + + ]: 565290 : if (b.getKind() == Kind::AND)
1095 : : {
1096 : 36644 : std::vector<Node> vars;
1097 : 36644 : std::vector<Node> subs;
1098 : 36644 : std::vector<Node> tmpArgs = args;
1099 [ + + ]: 140798 : for (unsigned j = 0, bsize = b.getNumChildren(); j < bsize; j++)
1100 : : {
1101 : 104742 : bool pol = b[j].getKind() == Kind::NOT;
1102 [ + + ][ + + ]: 104742 : Node batom = pol ? b[j][0] : b[j];
[ - - ]
1103 [ + + ]: 104742 : if (getVarElimLit(body, batom, pol, tmpArgs, vars, subs))
1104 : : {
1105 [ + - ]: 29084 : Trace("cond-var-split-debug") << "Variable elimination in child #"
1106 : 14542 : << j << " under " << i << std::endl;
1107 : : // Figure out if we should split
1108 : : // Currently we split if the aggressive option is set, or
1109 : : // if the top-level OR is binary.
1110 [ + - ][ + + ]: 14542 : if (aggCondSplit || size == 2)
1111 : : {
1112 : 588 : do_split = true;
1113 : : }
1114 : : // other splitting criteria go here
1115 : :
1116 [ + + ]: 14542 : if (do_split)
1117 : : {
1118 : 588 : split_index = i;
1119 : 588 : break;
1120 : : }
1121 : 13954 : vars.clear();
1122 : 13954 : subs.clear();
1123 : 13954 : tmpArgs = args;
1124 : : }
1125 [ + + ]: 104742 : }
1126 : 36644 : }
1127 [ + + ]: 565290 : if (do_split)
1128 : : {
1129 : 588 : break;
1130 : : }
1131 [ + + ]: 565290 : }
1132 [ + + ]: 186222 : if (do_split)
1133 : : {
1134 : : // For the sake of proofs, if we are not splitting the first child,
1135 : : // we first rearrange so that it is first, which can be proven by
1136 : : // ACI_NORM.
1137 : 588 : std::vector<Node> splitChildren;
1138 [ + + ]: 588 : if (split_index != 0)
1139 : : {
1140 : 110 : splitChildren.push_back(body[split_index]);
1141 [ + + ]: 330 : for (size_t i = 0; i < size; i++)
1142 : : {
1143 [ + + ]: 220 : if (i != split_index)
1144 : : {
1145 : 110 : splitChildren.push_back(body[i]);
1146 : : }
1147 : : }
1148 : 110 : return nm->mkNode(Kind::OR, splitChildren);
1149 : : }
1150 : : // This is expected to be proven by the RARE rule bool-or-and-distrib.
1151 : 478 : std::vector<Node> children;
1152 [ + + ]: 1434 : for (TNode bc : body)
1153 : : {
1154 : 956 : children.push_back(bc);
1155 : 956 : }
1156 [ + + ]: 3826 : for (TNode bci : body[split_index])
1157 : : {
1158 : 3348 : children[split_index] = bci;
1159 : 3348 : splitChildren.push_back(nm->mkNode(Kind::OR, children));
1160 : 3826 : }
1161 : : // split the AND child, for example:
1162 : : // ( x!=a ^ P(x) ) V Q(x) ---> ( x!=a V Q(x) ) ^ ( P(x) V Q(x) )
1163 : 478 : return nm->mkNode(Kind::AND, splitChildren);
1164 : 588 : }
1165 : : }
1166 : :
1167 : 390976 : return body;
1168 : : }
1169 : :
1170 : 20542 : bool QuantifiersRewriter::isVarElim(Node v, Node s)
1171 : : {
1172 [ - + ][ - + ]: 20542 : Assert(v.getKind() == Kind::BOUND_VARIABLE);
[ - - ]
1173 : 56780 : return !expr::hasSubterm(s, v) && CVC5_EQUAL(s.getType(), v.getType());
1174 : : }
1175 : :
1176 : 20477 : bool QuantifiersRewriter::isSafeSubsTerm(const Node& body, const Node& s)
1177 : : {
1178 : 20477 : std::unordered_set<Node> fvs;
1179 : 20477 : expr::getFreeVariables(s, fvs);
1180 : 40954 : return !expr::hasBoundVar(body, fvs);
1181 : 20477 : }
1182 : :
1183 : 154552 : Node QuantifiersRewriter::getVarElimEq(Node lit,
1184 : : const std::vector<Node>& args,
1185 : : Node& var,
1186 : : CDProof* cdp) const
1187 : : {
1188 [ - + ][ - + ]: 154552 : Assert(lit.getKind() == Kind::EQUAL);
[ - - ]
1189 : 154552 : Node slv;
1190 : 154552 : TypeNode tt = lit[0].getType();
1191 [ + + ]: 154552 : if (tt.isRealOrInt())
1192 : : {
1193 : 60985 : slv = getVarElimEqReal(lit, args, var, cdp);
1194 : : }
1195 [ + + ]: 93567 : else if (tt.isBitVector())
1196 : : {
1197 : 35067 : slv = getVarElimEqBv(lit, args, var, cdp);
1198 : : }
1199 [ + + ]: 58500 : else if (tt.isStringLike())
1200 : : {
1201 : 319 : slv = getVarElimEqString(lit, args, var, cdp);
1202 : : }
1203 : 309104 : return slv;
1204 : 154552 : }
1205 : :
1206 : 60985 : Node QuantifiersRewriter::getVarElimEqReal(Node lit,
1207 : : const std::vector<Node>& args,
1208 : : Node& var,
1209 : : CDProof* cdp) const
1210 : : {
1211 : : // for arithmetic, solve the equality
1212 : 60985 : std::map<Node, Node> msum;
1213 [ - + ]: 60985 : if (!ArithMSum::getMonomialSumLit(lit, msum))
1214 : : {
1215 : 0 : return Node::null();
1216 : : }
1217 : 60985 : std::vector<Node>::const_iterator ita;
1218 [ + + ]: 183842 : for (std::map<Node, Node>::iterator itm = msum.begin(); itm != msum.end();
1219 : 122857 : ++itm)
1220 : : {
1221 [ + + ]: 123694 : if (itm->first.isNull())
1222 : : {
1223 : 9907 : continue;
1224 : : }
1225 : 113787 : ita = std::find(args.begin(), args.end(), itm->first);
1226 [ + + ]: 113787 : if (ita != args.end())
1227 : : {
1228 : 1836 : Node veq_c;
1229 : 1836 : Node val;
1230 : 1836 : int ires = ArithMSum::isolate(itm->first, msum, veq_c, val, Kind::EQUAL);
1231 : 1836 : if (ires != 0 && veq_c.isNull() && isVarElim(itm->first, val))
1232 : : {
1233 : 837 : var = itm->first;
1234 [ + + ]: 837 : if (cdp != nullptr)
1235 : : {
1236 : 66 : Node eq = var.eqNode(val);
1237 : 66 : Node eqslv = lit.eqNode(eq);
1238 : 66 : cdp->addTrustedStep(
1239 : : eqslv, TrustId::MACRO_THEORY_REWRITE_RCONS_SIMPLE, {}, {});
1240 : 66 : }
1241 : 837 : return val;
1242 : : }
1243 [ + + ][ + + ]: 2673 : }
1244 : : }
1245 : 60148 : return Node::null();
1246 : 60985 : }
1247 : :
1248 : 35067 : Node QuantifiersRewriter::getVarElimEqBv(Node lit,
1249 : : const std::vector<Node>& args,
1250 : : Node& var,
1251 : : CDProof* cdp) const
1252 : : {
1253 [ - + ]: 35067 : if (TraceIsOn("quant-velim-bv"))
1254 : : {
1255 [ - - ]: 0 : Trace("quant-velim-bv") << "Bv-Elim : " << lit << " varList = { ";
1256 [ - - ]: 0 : for (const Node& v : args)
1257 : : {
1258 [ - - ]: 0 : Trace("quant-velim-bv") << v << " ";
1259 : : }
1260 [ - - ]: 0 : Trace("quant-velim-bv") << "} ?" << std::endl;
1261 : : }
1262 [ - + ][ - + ]: 35067 : Assert(lit.getKind() == Kind::EQUAL);
[ - - ]
1263 : : // TODO (#1494) : linearize the literal using utility
1264 : :
1265 : : // if the option varEntEqElimQuant is disabled, we must preserve equivalence
1266 : : // when solving the variable, meaning that BITVECTOR_CONCAT cannot be
1267 : : // on the path to the variable.
1268 : 35067 : std::unordered_set<Kind> disallowedKinds;
1269 [ - + ]: 35067 : if (!d_opts.quantifiers.varEntEqElimQuant)
1270 : : {
1271 : : // concatenation does not perserve equivalence i.e.
1272 : : // (concat x y) = z is not equivalent to x = ((_ extract n m) z)
1273 : 0 : disallowedKinds.insert(Kind::BITVECTOR_CONCAT);
1274 : : }
1275 [ + + ]: 35067 : else if (cdp != nullptr)
1276 : : {
1277 : : // does not support proofs
1278 : 60 : return Node::null();
1279 : : }
1280 : :
1281 : : // compute a subset active_args of the bound variables args that occur in lit
1282 : 35007 : std::vector<Node> active_args;
1283 : 35007 : computeArgVec(args, active_args, lit);
1284 : :
1285 [ + + ]: 70206 : for (const Node& cvar : active_args)
1286 : : {
1287 : : Node slv = booleans::TheoryBoolRewriter::getBvInvertSolve(
1288 : 35524 : d_nm, lit, cvar, disallowedKinds);
1289 [ + + ]: 35524 : if (!slv.isNull())
1290 : : {
1291 : : // if this is a proper variable elimination, that is, var = slv where
1292 : : // var is not in the free variables of slv, then we can return this
1293 : : // as the variable elimination for lit.
1294 [ + + ]: 749 : if (isVarElim(cvar, slv))
1295 : : {
1296 : 325 : var = cvar;
1297 : : // If we require a proof...
1298 [ - + ]: 325 : if (cdp != nullptr)
1299 : : {
1300 : 0 : Node eq = var.eqNode(slv);
1301 : 0 : Node eqslv = lit.eqNode(eq);
1302 : : // usually just arith poly norm, e.g. if
1303 : : // (= (bvadd x s) t) = (= x (bvsub t s))
1304 : 0 : Rational rx, ry;
1305 [ - - ]: 0 : if (arith::PolyNorm::isArithPolyNormRel(lit, eq, rx, ry))
1306 : : {
1307 : : // will elaborate with BV_POLY_NORM_EQ
1308 : 0 : cdp->addTrustedStep(
1309 : : eqslv, TrustId::MACRO_THEORY_REWRITE_RCONS_SIMPLE, {}, {});
1310 : : }
1311 : : else
1312 : : {
1313 : : // Otherwise we add (= (= t s) (= x r)) = true as a step
1314 : : // with MACRO_BOOL_BV_INVERT_SOLVE. This ensures that further
1315 : : // elaboration can replay the proof, knowing which variable we
1316 : : // solved for. This is used if arith poly norm does not suffice,
1317 : : // e.g. (= t (bvxor x s)) = (= x (bvxor t s)).
1318 : 0 : Node truen = nodeManager()->mkConst(true);
1319 : 0 : Node eqslvti = eqslv.eqNode(truen);
1320 : : // use trusted step, will elaborate
1321 : 0 : cdp->addTrustedStep(
1322 : : eqslvti, TrustId::MACRO_THEORY_REWRITE_RCONS, {}, {});
1323 : 0 : cdp->addStep(eqslv, ProofRule::TRUE_ELIM, {eqslvti}, {});
1324 : 0 : }
1325 : 0 : }
1326 : 325 : return slv;
1327 : : }
1328 : : }
1329 [ + + ]: 35524 : }
1330 : :
1331 : 34682 : return Node::null();
1332 : 35067 : }
1333 : :
1334 : 319 : Node QuantifiersRewriter::getVarElimEqString(Node lit,
1335 : : const std::vector<Node>& args,
1336 : : Node& var,
1337 : : CDProof* cdp) const
1338 : : {
1339 [ - + ][ - + ]: 319 : Assert(lit.getKind() == Kind::EQUAL);
[ - - ]
1340 : : // The reasoning below involves equality entailment as
1341 : : // (= (str.++ s x t) r) entails (= x (str.substr r (str.len s) _)),
1342 : : // but these equalities are not equivalent.
1343 [ + - ][ + + ]: 319 : if (!d_opts.quantifiers.varEntEqElimQuant || cdp != nullptr)
1344 : : {
1345 : 6 : return Node::null();
1346 : : }
1347 : 313 : NodeManager* nm = nodeManager();
1348 [ + + ]: 919 : for (unsigned i = 0; i < 2; i++)
1349 : : {
1350 [ + + ]: 626 : if (lit[i].getKind() == Kind::STRING_CONCAT)
1351 : : {
1352 : 49 : TypeNode stype = lit[i].getType();
1353 [ + + ]: 127 : for (unsigned j = 0, nchildren = lit[i].getNumChildren(); j < nchildren;
1354 : : j++)
1355 : : {
1356 [ + + ]: 98 : if (std::find(args.begin(), args.end(), lit[i][j]) != args.end())
1357 : : {
1358 : 62 : var = lit[i][j];
1359 : 62 : Node slv = lit[1 - i];
1360 : 124 : std::vector<Node> preL(lit[i].begin(), lit[i].begin() + j);
1361 : 62 : std::vector<Node> postL(lit[i].begin() + j + 1, lit[i].end());
1362 : 62 : Node tpre = strings::utils::mkConcat(preL, stype);
1363 : 62 : Node tpost = strings::utils::mkConcat(postL, stype);
1364 : 62 : Node slvL = nm->mkNode(Kind::STRING_LENGTH, slv);
1365 : 62 : Node tpreL = nm->mkNode(Kind::STRING_LENGTH, tpre);
1366 : 62 : Node tpostL = nm->mkNode(Kind::STRING_LENGTH, tpost);
1367 : 124 : slv = nm->mkNode(
1368 : : Kind::STRING_SUBSTR,
1369 : : slv,
1370 : : tpreL,
1371 : 124 : nm->mkNode(
1372 : 186 : Kind::SUB, slvL, nm->mkNode(Kind::ADD, tpreL, tpostL)));
1373 : : // forall x. r ++ x ++ t = s => P( x )
1374 : : // is equivalent to
1375 : : // r ++ s' ++ t = s => P( s' ) where
1376 : : // s' = substr( s, |r|, |s|-(|t|+|r|) ).
1377 : : // We apply this only if r,t,s do not contain free variables.
1378 [ + + ]: 62 : if (!expr::hasFreeVar(slv))
1379 : : {
1380 : 20 : return slv;
1381 : : }
1382 [ + + ][ + + ]: 202 : }
[ + + ][ + + ]
[ + + ][ + + ]
[ + + ][ + + ]
1383 : : }
1384 [ + + ]: 49 : }
1385 : : }
1386 : :
1387 : 293 : return Node::null();
1388 : : }
1389 : :
1390 : 928748 : bool QuantifiersRewriter::getVarElimLit(Node body,
1391 : : Node lit,
1392 : : bool pol,
1393 : : std::vector<Node>& args,
1394 : : std::vector<Node>& vars,
1395 : : std::vector<Node>& subs,
1396 : : CDProof* cdp) const
1397 : : {
1398 [ - + ][ - + ]: 928748 : Assert(lit.getKind() != Kind::NOT);
[ - - ]
1399 [ + - ]: 1857496 : Trace("var-elim-quant-debug")
1400 : 928748 : << "Eliminate : " << lit << ", pol = " << pol << "?" << std::endl;
1401 : : // all eliminations below guarded by varElimQuant()
1402 [ + + ]: 928748 : if (!d_opts.quantifiers.varElimQuant)
1403 : : {
1404 : 39 : return false;
1405 : : }
1406 : :
1407 [ + + ]: 928709 : if (lit.getKind() == Kind::EQUAL)
1408 : : {
1409 : 476658 : if (pol || lit[0].getType().isBoolean())
1410 : : {
1411 : : // In the loop below, we try solving for *both* sides to
1412 : : // maximize the determinism of the rewriter. For example,
1413 : : // given 2 Boolean variables x and y, when we construct
1414 : : // (not (= (not x) (not y))), the rewriter may order them in
1415 : : // either direction. Taking the first solved side leads to
1416 : : // nondeterminism based on when (not x) and (not y) are constructed.
1417 : : // However, if we compare the variables we will always solve
1418 : : // x -> y or vice versa based on when x,y are constructed.
1419 : 237812 : Node solvedVar;
1420 : 237812 : Node solvedSubs;
1421 [ + + ]: 701882 : for (unsigned i = 0; i < 2; i++)
1422 : : {
1423 : 475624 : bool tpol = pol;
1424 : 475624 : Node v_slv = lit[i];
1425 [ + + ]: 475624 : if (v_slv.getKind() == Kind::NOT)
1426 : : {
1427 : 12692 : v_slv = v_slv[0];
1428 : 12692 : tpol = !tpol;
1429 : : }
1430 : : // don't solve if we solved the opposite side
1431 : : // and it was smaller.
1432 [ + + ][ + + ]: 475624 : if (!solvedVar.isNull() && v_slv > solvedVar)
[ + + ]
1433 : : {
1434 : 11554 : break;
1435 : : }
1436 : : std::vector<Node>::iterator ita =
1437 : 464070 : std::find(args.begin(), args.end(), v_slv);
1438 [ + + ]: 464070 : if (ita != args.end())
1439 : : {
1440 [ + + ]: 18434 : if (isVarElim(v_slv, lit[1 - i]))
1441 : : {
1442 : 16957 : solvedVar = v_slv;
1443 : 16957 : solvedSubs = lit[1 - i];
1444 [ + + ]: 16957 : if (!tpol)
1445 : : {
1446 [ - + ][ - + ]: 456 : Assert(solvedSubs.getType().isBoolean());
[ - - ]
1447 : 456 : solvedSubs = solvedSubs.negate();
1448 : : }
1449 : : }
1450 : : }
1451 [ + + ]: 475624 : }
1452 [ + + ][ + + ]: 237812 : if (!solvedVar.isNull() && isSafeSubsTerm(body, solvedSubs))
[ + + ]
1453 : : {
1454 [ + + ]: 16654 : if (cdp != nullptr)
1455 : : {
1456 : 400 : Node eq = solvedVar.eqNode(solvedSubs);
1457 [ + + ]: 400 : Node litn = pol ? lit : lit.notNode();
1458 : 400 : Node eqslv = litn.eqNode(eq);
1459 : 400 : cdp->addTrustedStep(
1460 : : eqslv, TrustId::MACRO_THEORY_REWRITE_RCONS_SIMPLE, {}, {});
1461 [ + - ]: 800 : Trace("var-elim-quant")
1462 : 400 : << "...add trusted step " << eqslv << std::endl;
1463 : 400 : }
1464 : : std::vector<Node>::iterator ita =
1465 : 16654 : std::find(args.begin(), args.end(), solvedVar);
1466 [ + - ]: 33308 : Trace("var-elim-quant")
1467 : 0 : << "Variable eliminate based on equality : " << solvedVar << " -> "
1468 : 16654 : << solvedSubs << std::endl;
1469 : 16654 : vars.push_back(solvedVar);
1470 : 16654 : subs.push_back(solvedSubs);
1471 : 16654 : args.erase(ita);
1472 : 16654 : return true;
1473 : : }
1474 [ + + ][ + + ]: 254466 : }
1475 : : }
1476 [ + + ]: 912055 : if (lit.getKind() == Kind::BOUND_VARIABLE)
1477 : : {
1478 : 5008 : std::vector<Node>::iterator ita = std::find(args.begin(), args.end(), lit);
1479 [ + + ]: 5008 : if (ita != args.end())
1480 : : {
1481 [ + - ]: 4991 : Trace("var-elim-bool") << "Variable eliminate : " << lit << std::endl;
1482 : 4991 : Node c = nodeManager()->mkConst(pol);
1483 [ + + ]: 4991 : if (cdp != nullptr)
1484 : : {
1485 : : // x = (x=true) or (not x) = (x = false)
1486 : 83 : Node eq = lit.eqNode(c);
1487 [ + + ]: 83 : Node litn = pol ? lit : lit.notNode();
1488 : 83 : Node eqslv = litn.eqNode(eq);
1489 : 83 : cdp->addTrustedStep(
1490 : : eqslv, TrustId::MACRO_THEORY_REWRITE_RCONS_SIMPLE, {}, {});
1491 : 83 : }
1492 : 4991 : vars.push_back(lit);
1493 : 4991 : subs.push_back(c);
1494 : 4991 : args.erase(ita);
1495 : 4991 : return true;
1496 : 4991 : }
1497 : : }
1498 [ + + ][ + + ]: 907064 : if (lit.getKind() == Kind::EQUAL && pol)
[ + + ]
1499 : : {
1500 : 154552 : Node var;
1501 : 154552 : Node slv = getVarElimEq(lit, args, var, cdp);
1502 [ + + ][ + - ]: 154552 : if (!slv.isNull() && isSafeSubsTerm(body, slv))
[ + + ]
1503 : : {
1504 [ - + ][ - + ]: 1182 : Assert(!var.isNull());
[ - - ]
1505 : : std::vector<Node>::iterator ita =
1506 : 1182 : std::find(args.begin(), args.end(), var);
1507 [ - + ][ - + ]: 1182 : Assert(ita != args.end());
[ - - ]
1508 [ + - ]: 2364 : Trace("var-elim-quant")
1509 : 0 : << "Variable eliminate based on theory-specific solving : " << var
1510 : 1182 : << " -> " << slv << std::endl;
1511 [ - + ][ - + ]: 1182 : Assert(!expr::hasSubterm(slv, var));
[ - - ]
1512 [ - + ][ - + ]: 3546 : AssertEqual(slv.getType(), var.getType());
[ - - ]
1513 : 1182 : vars.push_back(var);
1514 : 1182 : subs.push_back(slv);
1515 : 1182 : args.erase(ita);
1516 : 1182 : return true;
1517 : : }
1518 [ + + ][ + + ]: 155734 : }
1519 : 905882 : return false;
1520 : : }
1521 : :
1522 : 418190 : bool QuantifiersRewriter::getVarElim(Node body,
1523 : : std::vector<Node>& args,
1524 : : std::vector<Node>& vars,
1525 : : std::vector<Node>& subs,
1526 : : std::vector<Node>& lits,
1527 : : CDProof* cdp) const
1528 : : {
1529 : 418190 : return getVarElimInternal(body, body, false, args, vars, subs, lits, cdp);
1530 : : }
1531 : :
1532 : 1024812 : bool QuantifiersRewriter::getVarElimInternal(Node body,
1533 : : Node n,
1534 : : bool pol,
1535 : : std::vector<Node>& args,
1536 : : std::vector<Node>& vars,
1537 : : std::vector<Node>& subs,
1538 : : std::vector<Node>& lits,
1539 : : CDProof* cdp) const
1540 : : {
1541 : 1024812 : Kind nk = n.getKind();
1542 [ + + ]: 1410337 : while (nk == Kind::NOT)
1543 : : {
1544 : 385525 : n = n[0];
1545 : 385525 : pol = !pol;
1546 : 385525 : nk = n.getKind();
1547 : : }
1548 [ + + ][ + + ]: 1024812 : if ((nk == Kind::AND && pol) || (nk == Kind::OR && !pol))
[ + + ][ + + ]
1549 : : {
1550 [ + + ]: 800108 : for (const Node& cn : n)
1551 : : {
1552 [ + + ]: 605844 : if (getVarElimInternal(body, cn, pol, args, vars, subs, lits, cdp))
1553 : : {
1554 : 6542 : return true;
1555 : : }
1556 [ + + ]: 605844 : }
1557 : 194264 : return false;
1558 : : }
1559 [ + + ]: 824006 : if (getVarElimLit(body, n, pol, args, vars, subs, cdp))
1560 : : {
1561 [ + + ]: 8285 : lits.emplace_back(pol ? n : n.notNode());
1562 : 8285 : return true;
1563 : : }
1564 : 815721 : return false;
1565 : : }
1566 : :
1567 : 778 : bool QuantifiersRewriter::hasVarElim(Node n,
1568 : : bool pol,
1569 : : std::vector<Node>& args) const
1570 : : {
1571 : 778 : std::vector<Node> vars;
1572 : 778 : std::vector<Node> subs;
1573 : 778 : std::vector<Node> lits;
1574 : 1556 : return getVarElimInternal(n, n, pol, args, vars, subs, lits);
1575 : 778 : }
1576 : :
1577 : 410073 : Node QuantifiersRewriter::getVarElimIneq(Node body,
1578 : : std::vector<Node>& args,
1579 : : QAttributes& qa) const
1580 : : {
1581 [ + - ]: 410073 : Trace("var-elim-quant-debug") << "getVarElimIneq " << body << std::endl;
1582 : : // For each variable v, we compute a set of implied bounds in the body
1583 : : // of the quantified formula.
1584 : : // num_bounds[x][-1] stores the entailed lower bounds for x
1585 : : // num_bounds[x][1] stores the entailed upper bounds for x
1586 : : // num_bounds[x][0] stores the entailed disequalities for x
1587 : : // These bounds are stored in a map that maps the literal for the bound to
1588 : : // its required polarity. For example, for quantified formula
1589 : : // (forall ((x Int)) (or (= x 0) (>= x a)))
1590 : : // we have:
1591 : : // num_bounds[x][0] contains { x -> { (= x 0) -> false } }
1592 : : // num_bounds[x][-1] contains { x -> { (>= x a) -> false } }
1593 : : // This method succeeds in eliminating x if its only occurrences are in
1594 : : // entailed disequalities, and one kind of bound. This is the case for the
1595 : : // above quantified formula, which can be rewritten to false. The reason
1596 : : // is that we can always chose a value for x that is arbitrarily large (resp.
1597 : : // small) to satisfy all disequalities and inequalities for x.
1598 : 410073 : std::map<Node, std::map<int, std::map<Node, bool>>> num_bounds;
1599 : : // The set of variables that we know we can not eliminate
1600 : 410073 : std::unordered_set<Node> ineligVars;
1601 : : // compute the entailed literals
1602 : 410073 : std::vector<Node> lits;
1603 [ + + ]: 410073 : if (body.getKind() == Kind::OR)
1604 : : {
1605 : 193866 : lits.insert(lits.begin(), body.begin(), body.end());
1606 : : }
1607 : : else
1608 : : {
1609 : 216207 : lits.push_back(body);
1610 : : }
1611 [ + + ]: 1219051 : for (const Node& l : lits)
1612 : : {
1613 : : // an inequality that is entailed with a given polarity
1614 : 808978 : bool pol = l.getKind() == Kind::NOT;
1615 [ + + ]: 808978 : Node lit = pol ? l[0] : l;
1616 [ + - ]: 1617956 : Trace("var-elim-quant-debug") << "Process inequality bounds : " << lit
1617 : 808978 : << ", pol = " << pol << "..." << std::endl;
1618 : 808978 : std::map<Node, Node> msum;
1619 : 1617956 : bool canSolve = lit.getKind() == Kind::GEQ
1620 [ + + ][ + + ]: 1237460 : || (lit.getKind() == Kind::EQUAL
1621 : 1237460 : && lit[0].getType().isRealOrInt() && !pol);
1622 [ + + ][ - + ]: 808978 : if (!canSolve || !ArithMSum::getMonomialSumLit(lit, msum))
[ + + ][ + + ]
[ - - ]
1623 : : {
1624 : : // not an inequality, or failed to compute, we cannot use this and all
1625 : : // variables in it are ineligible.
1626 : 656898 : expr::getFreeVariables(lit, ineligVars);
1627 : 656898 : continue;
1628 : : }
1629 [ + + ]: 465591 : for (const std::pair<const Node, Node>& m : msum)
1630 : : {
1631 [ + + ][ + + ]: 313511 : if (!m.first.isNull() && ineligVars.find(m.first) == ineligVars.end())
[ + + ]
1632 : : {
1633 : : std::vector<Node>::iterator ita =
1634 : 217417 : std::find(args.begin(), args.end(), m.first);
1635 [ + + ]: 217417 : if (ita != args.end())
1636 : : {
1637 : : // store that this literal is upper/lower bound for itm->first
1638 : 87818 : Node veq_c;
1639 : 87818 : Node val;
1640 : : int ires =
1641 : 87818 : ArithMSum::isolate(m.first, msum, veq_c, val, lit.getKind());
1642 [ + - ][ + + ]: 87818 : if (ires != 0 && veq_c.isNull())
[ + + ]
1643 : : {
1644 [ + + ]: 87078 : if (lit.getKind() == Kind::GEQ)
1645 : : {
1646 : 58998 : bool is_upper = pol != (ires == 1);
1647 [ + - ]: 117996 : Trace("var-elim-ineq-debug")
1648 [ - - ]: 0 : << lit << " is a " << (is_upper ? "upper" : "lower")
1649 : 58998 : << " bound for " << m.first << std::endl;
1650 [ + - ]: 117996 : Trace("var-elim-ineq-debug")
1651 : 58998 : << " pol/ires = " << pol << " " << ires << std::endl;
1652 [ + + ]: 58998 : num_bounds[m.first][is_upper ? 1 : -1][lit] = pol;
1653 : : }
1654 : : else
1655 : : {
1656 [ + - ]: 56160 : Trace("var-elim-ineq-debug")
1657 : 28080 : << lit << " is a disequality for " << m.first << std::endl;
1658 : 28080 : num_bounds[m.first][0][lit] = pol;
1659 : : }
1660 : : }
1661 : : else
1662 : : {
1663 [ + - ]: 1480 : Trace("var-elim-ineq-debug")
1664 : 0 : << "...ineligible " << m.first
1665 : 0 : << " since it cannot be solved for (" << ires << ", " << veq_c
1666 : 740 : << ")." << std::endl;
1667 : 740 : num_bounds.erase(m.first);
1668 : 740 : ineligVars.insert(m.first);
1669 : : }
1670 : 87818 : }
1671 : : else
1672 : : {
1673 : : // compute variables in itm->first, these are not eligible for
1674 : : // elimination
1675 : 129599 : expr::getFreeVariables(m.first, ineligVars);
1676 : : }
1677 : : }
1678 : : }
1679 [ + + ][ + + ]: 1465876 : }
1680 [ + + ]: 410073 : if (!qa.d_ipl.isNull())
1681 : : {
1682 : : // do not eliminate variables that occur in the annotation
1683 : 39871 : expr::getFreeVariables(qa.d_ipl, ineligVars);
1684 : : }
1685 : : // collect all variables that have only upper/lower bounds
1686 : 410073 : std::map<Node, bool> elig_vars;
1687 : : // the variable to eliminate
1688 : 410073 : Node v;
1689 : 410073 : bool vIsUpper = true;
1690 : 410073 : for (const std::pair<const Node, std::map<int, std::map<Node, bool>>>& nb :
1691 [ + + ]: 880992 : num_bounds)
1692 : : {
1693 [ + + ]: 62833 : if (ineligVars.find(nb.first) != ineligVars.end())
1694 : : {
1695 : 56918 : continue;
1696 : : }
1697 [ + + ]: 5915 : if (nb.second.find(1) == nb.second.end())
1698 : : {
1699 [ + - ]: 3152 : Trace("var-elim-ineq-debug")
1700 : 1576 : << "Variable " << nb.first << " has only lower bounds." << std::endl;
1701 : 1576 : v = nb.first;
1702 : 1576 : vIsUpper = false;
1703 : 1576 : break;
1704 : : }
1705 [ + + ]: 4339 : else if (nb.second.find(-1) == nb.second.end())
1706 : : {
1707 [ + - ]: 822 : Trace("var-elim-ineq-debug")
1708 : 411 : << "Variable " << nb.first << " has only upper bounds." << std::endl;
1709 : 411 : v = nb.first;
1710 : 411 : vIsUpper = true;
1711 : 411 : break;
1712 : : }
1713 : : }
1714 [ + + ]: 410073 : if (v.isNull())
1715 : : {
1716 : : // no eligible variables
1717 : 408086 : return Node::null();
1718 : : }
1719 : 1987 : NodeManager* nm = nodeManager();
1720 [ + - ]: 3974 : Trace("var-elim-ineq-debug")
1721 : 1987 : << v << " is eligible for elimination." << std::endl;
1722 : : // Get the literals that corresponded to bounds for the given variable.
1723 : : // These can be dropped from the disjunction of the quantified formula,
1724 : : // which is justified based on an infinite projection of the eliminated
1725 : : // variable.
1726 : 1987 : std::map<int, std::map<Node, bool>>& nbv = num_bounds[v];
1727 : 1987 : std::unordered_set<Node> boundLits;
1728 [ + + ]: 5961 : for (size_t i = 0; i < 2; i++)
1729 : : {
1730 [ + + ][ + + ]: 3974 : size_t nindex = i == 0 ? (vIsUpper ? 1 : -1) : 0;
1731 [ + + ]: 6300 : for (const std::pair<const Node, bool>& nb : nbv[nindex])
1732 : : {
1733 [ + - ]: 4652 : Trace("var-elim-ineq-debug")
1734 : 2326 : << " subs : " << nb.first << " -> " << nb.second << std::endl;
1735 : 2326 : boundLits.insert(nb.first);
1736 : : }
1737 : : }
1738 : : // eliminate from args
1739 : 1987 : std::vector<Node>::iterator ita = std::find(args.begin(), args.end(), v);
1740 [ - + ][ - + ]: 1987 : Assert(ita != args.end());
[ - - ]
1741 : 1987 : args.erase(ita);
1742 : : // we leave the literals that did not involve the variable we eliminated
1743 : 1987 : std::vector<Node> remLits;
1744 [ + + ]: 5545 : for (const Node& l : lits)
1745 : : {
1746 [ + + ]: 3558 : Node atom = l.getKind() == Kind::NOT ? l[0] : l;
1747 [ + + ]: 3558 : if (boundLits.find(atom) == boundLits.end())
1748 : : {
1749 : 1232 : remLits.push_back(l);
1750 : : }
1751 : 3558 : }
1752 : 1987 : return nm->mkOr(remLits);
1753 : 410073 : }
1754 : :
1755 : 410393 : Node QuantifiersRewriter::computeVarElimination(Node body,
1756 : : std::vector<Node>& args,
1757 : : QAttributes& qa) const
1758 : : {
1759 [ - + ][ - - ]: 410393 : if (!d_opts.quantifiers.varElimQuant && !d_opts.quantifiers.varIneqElimQuant
1760 [ - - ]: 0 : && !d_opts.quantifiers.leibnizEqElim)
1761 : : {
1762 : 0 : return body;
1763 : : }
1764 [ + - ]: 820786 : Trace("var-elim-quant-debug")
1765 : 410393 : << "computeVarElimination " << body << std::endl;
1766 : 410393 : std::vector<Node> vars;
1767 : 410393 : std::vector<Node> subs;
1768 : : // standard variable elimination
1769 [ + - ]: 410393 : if (d_opts.quantifiers.varElimQuant)
1770 : : {
1771 : 410393 : std::vector<Node> lits;
1772 : 410393 : getVarElim(body, args, vars, subs, lits);
1773 : 410393 : }
1774 : : // variable elimination based on one-direction inequalities
1775 [ + + ][ + + ]: 410393 : if (vars.empty() && d_opts.quantifiers.varIneqElimQuant)
[ + + ]
1776 : : {
1777 : 404667 : Node vibBody = getVarElimIneq(body, args, qa);
1778 [ + + ]: 404667 : if (!vibBody.isNull())
1779 : : {
1780 [ + - ]: 1525 : Trace("var-elim-quant-debug") << "...returns " << vibBody << std::endl;
1781 : 1525 : return vibBody;
1782 : : }
1783 [ + + ]: 404667 : }
1784 : : // if we eliminated a variable, update body and reprocess
1785 [ + + ]: 408868 : if (!vars.empty())
1786 : : {
1787 [ + - ]: 11316 : Trace("var-elim-quant-debug")
1788 : 5658 : << "VE " << vars.size() << "/" << args.size() << std::endl;
1789 [ - + ][ - + ]: 5658 : Assert(vars.size() == subs.size());
[ - - ]
1790 : : // remake with eliminated nodes
1791 : 5658 : body = body.substitute(vars.begin(), vars.end(), subs.begin(), subs.end());
1792 [ + + ]: 5658 : if (!qa.d_ipl.isNull())
1793 : : {
1794 : 152 : qa.d_ipl = qa.d_ipl.substitute(
1795 : 76 : vars.begin(), vars.end(), subs.begin(), subs.end());
1796 : : }
1797 [ + - ]: 5658 : Trace("var-elim-quant") << "Return " << body << std::endl;
1798 : : }
1799 : : // Leibniz equality elimination
1800 [ + + ]: 408868 : if (d_opts.quantifiers.leibnizEqElim)
1801 : : {
1802 : 186 : if (body.getKind() == Kind::OR
1803 [ + + ][ + - ]: 186 : && body.getNumChildren() == 2) // the body must have exactly 2 children
[ + + ]
1804 : : {
1805 : 30 : Node termA = body[0];
1806 : 30 : Node termB = body[1];
1807 : 30 : Node opA, opB;
1808 : 30 : std::vector<Node> argsA, argsB;
1809 : 30 : bool negA = false, negB = false;
1810 [ - + ][ - - ]: 30 : if (!matchUfLiteral(termA, opA, argsA, negA)
1811 [ + - ][ - + ]: 30 : || !matchUfLiteral(termB, opB, argsB, negB))
[ + - ][ + - ]
[ - - ]
1812 : : {
1813 : 0 : return body;
1814 : : }
1815 : :
1816 : : // need pattern (not P(t1)) or P(t2) (either child can be the negated one)
1817 : 30 : if (opA != opB || !((negA && !negB) || (negB && !negA)))
1818 : : {
1819 : 0 : return body;
1820 : : }
1821 : : // identify which side is t1 and which is t2
1822 [ + - ]: 30 : std::vector<Node> t1 = negA ? argsA : argsB;
1823 [ + - ]: 30 : std::vector<Node> t2 = negA ? argsB : argsA;
1824 : :
1825 : : // operator P must be one of the quantifier's bound variables (otherwise
1826 : : // this is not Leibniz)
1827 : 30 : auto it = std::find(args.begin(), args.end(), opA);
1828 [ - + ]: 30 : if (it == args.end())
1829 : : {
1830 : 0 : return body;
1831 : : }
1832 : : // arity must match
1833 [ - + ]: 30 : if (t1.size() != t2.size())
1834 : : {
1835 : 0 : return body;
1836 : : }
1837 : : // ensure P does not occur inside the argument terms
1838 [ + + ]: 60 : for (size_t i = 0; i < t1.size(); ++i)
1839 : : {
1840 : 60 : if (expr::hasSubterm(t1[i], opA, false)
1841 : 60 : || expr::hasSubterm(t2[i], opA, false))
1842 : : {
1843 : 0 : return body;
1844 : : }
1845 : : }
1846 : : // check operator type: it should be a predicate
1847 : 30 : TypeNode ptype = opA.getType();
1848 [ + - ][ - + ]: 30 : if (!ptype.isFunction() || !ptype.getRangeType().isBoolean()) return body;
[ + - ][ - + ]
[ - - ]
1849 [ - + ]: 30 : if (size_t(ptype.getNumChildren()) != t1.size() + 1) return body;
1850 : :
1851 : 30 : NodeManager* nm = nodeManager();
1852 : 30 : std::vector<Node> eqs;
1853 [ + + ]: 60 : for (size_t i = 0; i < t1.size(); ++i)
1854 : : {
1855 : 30 : eqs.push_back(nm->mkNode(Kind::EQUAL, t1[i], t2[i]));
1856 : : }
1857 [ + - ]: 30 : Node eq = (eqs.size() == 1) ? eqs[0] : nm->mkNode(Kind::AND, eqs);
1858 : :
1859 : : // remove the predicate variable from the quantifier variable list
1860 : 30 : args.erase(it);
1861 : :
1862 [ + - ]: 60 : Trace("var-elim-quant") << "Detected Leibniz equality in " << body
1863 : 30 : << ", returning: " << eq << std::endl;
1864 : 30 : return eq;
1865 : 30 : }
1866 : : }
1867 : 408838 : return body;
1868 : 410393 : }
1869 : :
1870 : : // This function is used by the Leibniz-equality elimination step to check
1871 : : // whether a term has the shape P(t1, ..., tn) or ¬P(t1, ..., tn).
1872 : 60 : bool QuantifiersRewriter::matchUfLiteral(Node lit,
1873 : : Node& op,
1874 : : std::vector<Node>& argsOut,
1875 : : bool& neg) const
1876 : : {
1877 : 60 : neg = (lit.getKind() == Kind::NOT);
1878 [ + + ]: 60 : Node atom = neg ? lit[0] : lit;
1879 : :
1880 [ - + ]: 60 : if (atom.getKind() != Kind::APPLY_UF)
1881 : : {
1882 : 0 : return false;
1883 : : }
1884 : :
1885 : 60 : op = atom.getOperator();
1886 : 60 : argsOut.assign(atom.begin(), atom.end());
1887 : 60 : return true;
1888 : 60 : }
1889 : :
1890 : 409170 : Node QuantifiersRewriter::computeDtVarExpand(NodeManager* nm,
1891 : : const Node& q,
1892 : : size_t& index)
1893 : : {
1894 : 409170 : std::vector<Node> lits;
1895 [ + + ]: 409170 : if (q[1].getKind() == Kind::OR)
1896 : : {
1897 : 193615 : lits.insert(lits.end(), q[1].begin(), q[1].end());
1898 : : }
1899 : : else
1900 : : {
1901 : 215555 : lits.push_back(q[1]);
1902 : : }
1903 [ + + ]: 1215502 : for (const Node& lit : lits)
1904 : : {
1905 [ + + ][ + + ]: 1180932 : if (lit.getKind() == Kind::NOT && lit[0].getKind() == Kind::APPLY_TESTER
[ - - ]
1906 : 1180932 : && lit[0][0].getKind() == Kind::BOUND_VARIABLE)
1907 : : {
1908 [ + - ]: 195 : for (size_t i = 0, nvars = q[0].getNumChildren(); i < nvars; i++)
1909 : : {
1910 [ + + ]: 195 : if (q[0][i] == lit[0][0])
1911 : : {
1912 : 163 : index = i;
1913 : : // quant dt split for the given variable
1914 : 326 : return QuantDSplit::split(nm, q, i);
1915 : : }
1916 : : }
1917 : : }
1918 : : }
1919 : 409007 : return q;
1920 : 409170 : }
1921 : :
1922 : 2185962 : Node QuantifiersRewriter::computePrenex(Node q,
1923 : : Node body,
1924 : : std::vector<Node>& args,
1925 : : std::vector<Node>& nargs,
1926 : : bool pol,
1927 : : bool prenexAgg) const
1928 : : {
1929 : 2185962 : NodeManager* nm = nodeManager();
1930 : 2185962 : Kind k = body.getKind();
1931 [ + + ]: 2185962 : if (k == Kind::FORALL)
1932 : : {
1933 [ + + ]: 73424 : if ((pol || prenexAgg)
1934 [ + + ][ + - ]: 157218 : && (d_opts.quantifiers.prenexQuantUser
1935 [ + + ][ + + ]: 83794 : || !QuantAttributes::hasPattern(body)))
[ + + ][ - - ]
1936 : : {
1937 : 4992 : std::vector<Node> terms;
1938 : 4992 : std::vector<Node> subs;
1939 : 4992 : BoundVarManager* bvm = nm->getBoundVarManager();
1940 [ + + ]: 4992 : std::vector<Node>& argVec = pol ? args : nargs;
1941 : : // for doing prenexing of same-signed quantifiers
1942 : : // must rename each variable that already exists
1943 : 4992 : SubtypeElimNodeConverter senc(nodeManager());
1944 [ + + ]: 14864 : for (const Node& v : body[0])
1945 : : {
1946 : 9872 : terms.push_back(v);
1947 : 9872 : TypeNode vt = v.getType();
1948 : 9872 : Node vv;
1949 [ + + ]: 9872 : if (!q.isNull())
1950 : : {
1951 : : // We cache based on the original quantified formula, the subformula
1952 : : // that we are pulling variables from (body), the variable v and an
1953 : : // index ii.
1954 : : // The argument body is required since in rare cases, two subformulas
1955 : : // may share the same variables. This is the case for define-fun
1956 : : // or inferred substitutions that contain quantified formulas.
1957 : : // The argument ii is required in case we are prenexing the same
1958 : : // subformula multiple times, e.g.
1959 : : // forall x. (forall y. P(y) or forall y. P(y)) --->
1960 : : // forall x z w. (P(z) or P(w)).
1961 : 9855 : size_t index = 0;
1962 : : do
1963 : : {
1964 : 9928 : Node ii = nm->mkConstInt(index);
1965 : 49640 : Node cacheVal = nm->mkNode(Kind::SEXPR, {q, body, v, ii});
1966 : 9928 : cacheVal = senc.convert(cacheVal);
1967 : 9928 : vv = bvm->mkBoundVar(BoundVarId::QUANT_REW_PRENEX, cacheVal, vt);
1968 : 9928 : index++;
1969 [ + + ]: 9928 : } while (std::find(argVec.begin(), argVec.end(), vv) != argVec.end());
1970 : : }
1971 : : else
1972 : : {
1973 : : // not specific to a quantified formula, use normal
1974 : 17 : vv = NodeManager::mkBoundVar(vt);
1975 : : }
1976 : 9872 : subs.push_back(vv);
1977 : 14864 : }
1978 : 4992 : argVec.insert(argVec.end(), subs.begin(), subs.end());
1979 : 4992 : Node newBody = body[1];
1980 : 9984 : newBody = newBody.substitute(
1981 : 4992 : terms.begin(), terms.end(), subs.begin(), subs.end());
1982 : 4992 : return newBody;
1983 : 4992 : }
1984 : : // must remove structure
1985 : : }
1986 [ + + ][ - + ]: 2107354 : else if (prenexAgg && k == Kind::ITE && body.getType().isBoolean())
[ - - ][ - + ]
[ - + ][ - - ]
1987 : : {
1988 : 0 : Node nn = nm->mkNode(Kind::AND,
1989 : 0 : {nm->mkNode(Kind::OR, body[0].notNode(), body[1]),
1990 : 0 : nm->mkNode(Kind::OR, body[0], body[2])});
1991 : 0 : return computePrenex(q, nn, args, nargs, pol, prenexAgg);
1992 : 0 : }
1993 : 2107354 : else if (prenexAgg && k == Kind::EQUAL && body[0].getType().isBoolean())
1994 : : {
1995 : 0 : Node nn = nm->mkNode(Kind::AND,
1996 : 0 : {nm->mkNode(Kind::OR, body[0].notNode(), body[1]),
1997 : 0 : nm->mkNode(Kind::OR, body[0], body[1].notNode())});
1998 : 0 : return computePrenex(q, nn, args, nargs, pol, prenexAgg);
1999 : 0 : }
2000 [ + - ]: 2107354 : else if (body.getType().isBoolean())
2001 : : {
2002 [ - + ][ - + ]: 2107354 : Assert(k != Kind::EXISTS);
[ - - ]
2003 : 2107354 : bool childrenChanged = false;
2004 : 2107354 : std::vector<Node> newChildren;
2005 [ + + ]: 6055165 : for (size_t i = 0, nchild = body.getNumChildren(); i < nchild; i++)
2006 : : {
2007 : : bool newHasPol;
2008 : : bool newPol;
2009 : 3947811 : QuantPhaseReq::getPolarity(body, i, true, pol, newHasPol, newPol);
2010 [ + + ]: 3947811 : if (!newHasPol)
2011 : : {
2012 : 2147833 : newChildren.push_back(body[i]);
2013 : 2147833 : continue;
2014 : : }
2015 : 3599956 : Node n = computePrenex(q, body[i], args, nargs, newPol, prenexAgg);
2016 : 1799978 : newChildren.push_back(n);
2017 [ + + ][ + + ]: 1799978 : childrenChanged = n != body[i] || childrenChanged;
[ + - ][ - - ]
2018 : 1799978 : }
2019 [ + + ]: 2107354 : if (childrenChanged)
2020 : : {
2021 [ + + ][ + + ]: 5059 : if (k == Kind::NOT && newChildren[0].getKind() == Kind::NOT)
[ + + ]
2022 : : {
2023 : 208 : return newChildren[0][0];
2024 : : }
2025 : 4851 : return nm->mkNode(k, newChildren);
2026 : : }
2027 [ + + ]: 2107354 : }
2028 : 2175911 : return body;
2029 : : }
2030 : :
2031 : 191058 : Node QuantifiersRewriter::computeSplit(std::vector<Node>& args, Node body) const
2032 : : {
2033 [ - + ][ - + ]: 191058 : Assert(body.getKind() == Kind::OR);
[ - - ]
2034 : 191058 : size_t eqc_count = 0;
2035 : 191058 : size_t eqc_active = 0;
2036 : 191058 : std::map<Node, int> var_to_eqc;
2037 : 191058 : std::map<int, std::vector<Node>> eqc_to_var;
2038 : 191058 : std::map<int, std::vector<Node>> eqc_to_lit;
2039 : :
2040 : 191058 : std::vector<Node> lits;
2041 : :
2042 [ + + ]: 907140 : for (unsigned i = 0; i < body.getNumChildren(); i++)
2043 : : {
2044 : : // get variables contained in the literal
2045 : 716082 : Node n = body[i];
2046 : 716082 : std::vector<Node> lit_args;
2047 : 716082 : computeArgVec(args, lit_args, n);
2048 [ + + ]: 716082 : if (lit_args.empty())
2049 : : {
2050 : 14333 : lits.push_back(n);
2051 : : }
2052 : : else
2053 : : {
2054 : : // collect the equivalence classes this literal belongs to, and the new
2055 : : // variables it contributes
2056 : 701749 : std::vector<int> eqcs;
2057 : 701749 : std::vector<Node> lit_new_args;
2058 : : // for each variable in literal
2059 [ + + ]: 2413263 : for (unsigned j = 0; j < lit_args.size(); j++)
2060 : : {
2061 : : // see if the variable has already been found
2062 [ + + ]: 1711514 : if (var_to_eqc.find(lit_args[j]) != var_to_eqc.end())
2063 : : {
2064 : 1109703 : int eqc = var_to_eqc[lit_args[j]];
2065 [ + + ]: 1109703 : if (std::find(eqcs.begin(), eqcs.end(), eqc) == eqcs.end())
2066 : : {
2067 : 509593 : eqcs.push_back(eqc);
2068 : : }
2069 : : }
2070 : : else
2071 : : {
2072 : 601811 : lit_new_args.push_back(lit_args[j]);
2073 : : }
2074 : : }
2075 [ + + ]: 701749 : if (eqcs.empty())
2076 : : {
2077 : 252433 : eqcs.push_back(eqc_count);
2078 : 252433 : eqc_count++;
2079 : 252433 : eqc_active++;
2080 : : }
2081 : :
2082 : 701749 : int eqcz = eqcs[0];
2083 : : // merge equivalence classes with eqcz
2084 [ + + ]: 762026 : for (unsigned j = 1; j < eqcs.size(); j++)
2085 : : {
2086 : 60277 : int eqc = eqcs[j];
2087 : : // move all variables from equivalence class
2088 [ + + ]: 245797 : for (unsigned k = 0; k < eqc_to_var[eqc].size(); k++)
2089 : : {
2090 : 185520 : Node v = eqc_to_var[eqc][k];
2091 : 185520 : var_to_eqc[v] = eqcz;
2092 : 185520 : eqc_to_var[eqcz].push_back(v);
2093 : 185520 : }
2094 : 60277 : eqc_to_var.erase(eqc);
2095 : : // move all literals from equivalence class
2096 [ + + ]: 223351 : for (unsigned k = 0; k < eqc_to_lit[eqc].size(); k++)
2097 : : {
2098 : 163074 : Node l = eqc_to_lit[eqc][k];
2099 : 163074 : eqc_to_lit[eqcz].push_back(l);
2100 : 163074 : }
2101 : 60277 : eqc_to_lit.erase(eqc);
2102 : 60277 : eqc_active--;
2103 : : }
2104 : : // add variables to equivalence class
2105 [ + + ]: 1303560 : for (unsigned j = 0; j < lit_new_args.size(); j++)
2106 : : {
2107 : 601811 : var_to_eqc[lit_new_args[j]] = eqcz;
2108 : 601811 : eqc_to_var[eqcz].push_back(lit_new_args[j]);
2109 : : }
2110 : : // add literal to equivalence class
2111 : 701749 : eqc_to_lit[eqcz].push_back(n);
2112 : 701749 : }
2113 : 716082 : }
2114 [ + + ][ + + ]: 191058 : if (eqc_active > 1 || !lits.empty() || var_to_eqc.size() != args.size())
[ + + ][ + + ]
2115 : : {
2116 : 11922 : NodeManager* nm = nodeManager();
2117 [ - + ]: 11922 : if (TraceIsOn("clause-split-debug"))
2118 : : {
2119 [ - - ]: 0 : Trace("clause-split-debug")
2120 : 0 : << "Split quantified formula with body " << body << std::endl;
2121 [ - - ]: 0 : Trace("clause-split-debug") << " Ground literals: " << std::endl;
2122 [ - - ]: 0 : for (size_t i = 0; i < lits.size(); i++)
2123 : : {
2124 [ - - ]: 0 : Trace("clause-split-debug") << " " << lits[i] << std::endl;
2125 : : }
2126 [ - - ]: 0 : Trace("clause-split-debug") << std::endl;
2127 [ - - ]: 0 : Trace("clause-split-debug") << "Equivalence classes: " << std::endl;
2128 : : }
2129 : 11922 : for (std::map<int, std::vector<Node>>::iterator it = eqc_to_lit.begin();
2130 [ + + ]: 24942 : it != eqc_to_lit.end();
2131 : 13020 : ++it)
2132 : : {
2133 : 13020 : int eqc = it->first;
2134 [ - + ]: 13020 : if (TraceIsOn("clause-split-debug"))
2135 : : {
2136 [ - - ]: 0 : Trace("clause-split-debug") << " Literals: " << std::endl;
2137 [ - - ]: 0 : for (size_t i = 0; i < it->second.size(); i++)
2138 : : {
2139 [ - - ]: 0 : Trace("clause-split-debug") << " " << it->second[i] << std::endl;
2140 : : }
2141 [ - - ]: 0 : Trace("clause-split-debug") << " Variables: " << std::endl;
2142 [ - - ]: 0 : for (size_t i = 0; i < eqc_to_var[eqc].size(); i++)
2143 : : {
2144 [ - - ]: 0 : Trace("clause-split-debug")
2145 : 0 : << " " << eqc_to_var[eqc][i] << std::endl;
2146 : : }
2147 [ - - ]: 0 : Trace("clause-split-debug") << std::endl;
2148 : : }
2149 : 13020 : std::vector<Node>& evars = eqc_to_var[eqc];
2150 : : // for the sake of proofs, we provide the variables in the order
2151 : : // they appear in the original quantified formula
2152 : 13020 : std::vector<Node> ovars;
2153 [ + + ]: 65461 : for (const Node& v : args)
2154 : : {
2155 [ + + ]: 52441 : if (std::find(evars.begin(), evars.end(), v) != evars.end())
2156 : : {
2157 : 28634 : ovars.emplace_back(v);
2158 : : }
2159 : : }
2160 : 13020 : Node bvl = nodeManager()->mkNode(Kind::BOUND_VAR_LIST, ovars);
2161 : 23636 : Node bd = it->second.size() == 1 ? it->second[0]
2162 [ + + ]: 23636 : : nm->mkNode(Kind::OR, it->second);
2163 : 26040 : Node fa = nm->mkNode(Kind::FORALL, bvl, bd);
2164 : 13020 : lits.push_back(fa);
2165 : 13020 : }
2166 [ - + ][ - + ]: 11922 : Assert(!lits.empty());
[ - - ]
2167 : 11922 : Node nf = nodeManager()->mkOr(lits);
2168 [ + - ]: 11922 : Trace("clause-split-debug") << "Made node : " << nf << std::endl;
2169 : 11922 : return nf;
2170 : 11922 : }
2171 : 179136 : return Node::null();
2172 : 191058 : }
2173 : :
2174 : 386390 : Node QuantifiersRewriter::mkForAll(const std::vector<Node>& args,
2175 : : Node body,
2176 : : QAttributes& qa) const
2177 : : {
2178 [ + + ]: 386390 : if (args.empty())
2179 : : {
2180 : 679 : return body;
2181 : : }
2182 : 385711 : NodeManager* nm = nodeManager();
2183 : 385711 : std::vector<Node> children;
2184 : 385711 : children.push_back(nm->mkNode(Kind::BOUND_VAR_LIST, args));
2185 : 385711 : children.push_back(body);
2186 [ + + ]: 385711 : if (!qa.d_ipl.isNull())
2187 : : {
2188 : 1091 : children.push_back(qa.d_ipl);
2189 : : }
2190 : 385711 : return nm->mkNode(Kind::FORALL, children);
2191 : 385711 : }
2192 : :
2193 : 17 : Node QuantifiersRewriter::mkForall(const std::vector<Node>& args,
2194 : : Node body,
2195 : : bool marked) const
2196 : : {
2197 : 17 : std::vector<Node> iplc;
2198 : 34 : return mkForall(args, body, iplc, marked);
2199 : 17 : }
2200 : :
2201 : 19 : Node QuantifiersRewriter::mkForall(const std::vector<Node>& args,
2202 : : Node body,
2203 : : std::vector<Node>& iplc,
2204 : : bool marked) const
2205 : : {
2206 [ - + ]: 19 : if (args.empty())
2207 : : {
2208 : 0 : return body;
2209 : : }
2210 : 19 : NodeManager* nm = nodeManager();
2211 : 19 : std::vector<Node> children;
2212 : 19 : children.push_back(nm->mkNode(Kind::BOUND_VAR_LIST, args));
2213 : 19 : children.push_back(body);
2214 [ + - ]: 19 : if (marked)
2215 : : {
2216 : 38 : Node avar = NodeManager::mkDummySkolem("id", nm->booleanType());
2217 : : QuantIdNumAttribute ida;
2218 : 19 : avar.setAttribute(ida, 0);
2219 : 19 : iplc.push_back(nm->mkNode(Kind::INST_ATTRIBUTE, avar));
2220 : 19 : }
2221 [ + - ]: 19 : if (!iplc.empty())
2222 : : {
2223 : 19 : children.push_back(nm->mkNode(Kind::INST_PATTERN_LIST, iplc));
2224 : : }
2225 : 19 : return nm->mkNode(Kind::FORALL, children);
2226 : 19 : }
2227 : :
2228 : : // computes miniscoping, also eliminates variables that do not occur free in
2229 : : // body
2230 : 404069 : Node QuantifiersRewriter::computeMiniscoping(Node q,
2231 : : QAttributes& qa,
2232 : : bool miniscopeConj,
2233 : : bool miniscopeFv) const
2234 : : {
2235 : 404069 : NodeManager* nm = nodeManager();
2236 : 808138 : std::vector<Node> args(q[0].begin(), q[0].end());
2237 : 404069 : Node body = q[1];
2238 : 404069 : Kind k = body.getKind();
2239 [ + + ][ + + ]: 404069 : if (k == Kind::AND || k == Kind::ITE)
2240 : : {
2241 : 15377 : bool doRewrite = miniscopeConj;
2242 [ + + ]: 15377 : if (k == Kind::ITE)
2243 : : {
2244 : : // ITE miniscoping is only valid if condition contains no variables
2245 [ + + ]: 483 : if (expr::hasSubterm(body[0], args))
2246 : : {
2247 : 456 : doRewrite = false;
2248 : : }
2249 : : }
2250 : : // aggressive miniscoping implies that structural miniscoping should
2251 : : // be applied first
2252 [ + + ]: 15377 : if (doRewrite)
2253 : : {
2254 : 11255 : BoundVarManager* bvm = nm->getBoundVarManager();
2255 : : // Break apart the quantifed formula
2256 : : // forall x. P1 ^ ... ^ Pn ---> forall x. P1 ^ ... ^ forall x. Pn
2257 : 11255 : NodeBuilder t(nm, k);
2258 : 11255 : std::vector<Node> argsc;
2259 : 11255 : SubtypeElimNodeConverter senc(nodeManager());
2260 [ + + ]: 40795 : for (size_t i = 0, nchild = body.getNumChildren(); i < nchild; i++)
2261 : : {
2262 [ + + ]: 29540 : if (argsc.empty())
2263 : : {
2264 : : // If not done so, we must create fresh copy of args. This is to
2265 : : // ensure that quantified formulas do not reuse variables.
2266 [ + + ]: 71544 : for (const Node& v : q[0])
2267 : : {
2268 : 48734 : TypeNode vt = v.getType();
2269 : 97468 : Node cacheVal = BoundVarManager::getCacheValue(q, v, i);
2270 : 48734 : cacheVal = senc.convert(cacheVal);
2271 : : Node vv =
2272 : 97468 : bvm->mkBoundVar(BoundVarId::QUANT_REW_MINISCOPE, cacheVal, vt);
2273 : 48734 : argsc.push_back(vv);
2274 : 71544 : }
2275 : : }
2276 : 29540 : Node b = body[i];
2277 : : Node bodyc =
2278 : 29540 : b.substitute(args.begin(), args.end(), argsc.begin(), argsc.end());
2279 [ + + ]: 29540 : if (b == bodyc)
2280 : : {
2281 : : // Did not contain variables in args, thus it is ground. Since we did
2282 : : // not use them, we keep the variables argsc for the next child.
2283 : 6938 : t << b;
2284 : : }
2285 : : else
2286 : : {
2287 : : // make the miniscoped quantified formula
2288 : 22602 : Node cbvl = nm->mkNode(Kind::BOUND_VAR_LIST, argsc);
2289 : 45204 : Node qq = nm->mkNode(Kind::FORALL, cbvl, bodyc);
2290 : 22602 : t << qq;
2291 : : // We used argsc, clear so we will construct a fresh copy above.
2292 : 22602 : argsc.clear();
2293 : 22602 : }
2294 : 29540 : }
2295 : 11255 : Node retVal = t;
2296 : 11255 : return retVal;
2297 : 11255 : }
2298 : 4122 : }
2299 [ + + ]: 388692 : else if (body.getKind() == Kind::OR)
2300 : : {
2301 [ + + ]: 191058 : if (miniscopeFv)
2302 : : {
2303 : : // splitting subsumes free variable miniscoping, apply it with higher
2304 : : // priority
2305 : 183938 : Node ret = computeSplit(args, body);
2306 [ + + ]: 183938 : if (!ret.isNull())
2307 : : {
2308 : 6762 : return ret;
2309 : : }
2310 [ + + ]: 183938 : }
2311 : : }
2312 [ + + ]: 197634 : else if (body.getKind() == Kind::NOT)
2313 : : {
2314 [ - + ][ - + ]: 66063 : Assert(isLiteral(body[0]));
[ - - ]
2315 : : }
2316 : : // remove variables that don't occur
2317 : 386052 : std::vector<Node> activeArgs;
2318 : 386052 : computeArgVec2(args, activeArgs, body, qa.d_ipl);
2319 : 386052 : return mkForAll(activeArgs, body, qa);
2320 : 404069 : }
2321 : :
2322 : 360 : Node QuantifiersRewriter::computeAggressiveMiniscoping(std::vector<Node>& args,
2323 : : Node body) const
2324 : : {
2325 : 360 : std::map<Node, std::vector<Node>> varLits;
2326 : 360 : std::map<Node, std::vector<Node>> litVars;
2327 [ + + ]: 360 : if (body.getKind() == Kind::OR)
2328 : : {
2329 [ + - ]: 208 : Trace("ag-miniscope") << "compute aggressive miniscoping on " << body
2330 : 104 : << std::endl;
2331 [ + + ]: 322 : for (size_t i = 0; i < body.getNumChildren(); i++)
2332 : : {
2333 : 218 : std::vector<Node> activeArgs;
2334 : 218 : computeArgVec(args, activeArgs, body[i]);
2335 [ + + ]: 480 : for (unsigned j = 0; j < activeArgs.size(); j++)
2336 : : {
2337 : 262 : varLits[activeArgs[j]].push_back(body[i]);
2338 : : }
2339 : 218 : std::vector<Node>& lit_body_i = litVars[body[i]];
2340 : 218 : std::vector<Node>::iterator lit_body_i_begin = lit_body_i.begin();
2341 : 218 : std::vector<Node>::const_iterator active_begin = activeArgs.begin();
2342 : 218 : std::vector<Node>::const_iterator active_end = activeArgs.end();
2343 : 218 : lit_body_i.insert(lit_body_i_begin, active_begin, active_end);
2344 : 218 : }
2345 : : // find the variable in the least number of literals
2346 : 104 : Node bestVar;
2347 : 104 : for (std::map<Node, std::vector<Node>>::iterator it = varLits.begin();
2348 [ + + ]: 252 : it != varLits.end();
2349 : 148 : ++it)
2350 : : {
2351 [ + + ][ + + ]: 148 : if (bestVar.isNull() || varLits[bestVar].size() > it->second.size())
[ + + ]
2352 : : {
2353 : 124 : bestVar = it->first;
2354 : : }
2355 : : }
2356 [ + - ]: 208 : Trace("ag-miniscope-debug")
2357 : 0 : << "Best variable " << bestVar << " occurs in "
2358 : 104 : << varLits[bestVar].size() << "/ " << body.getNumChildren()
2359 : 104 : << " literals." << std::endl;
2360 [ + - ][ + + ]: 104 : if (!bestVar.isNull() && varLits[bestVar].size() < body.getNumChildren())
[ + + ]
2361 : : {
2362 : : // we can miniscope
2363 [ + - ]: 22 : Trace("ag-miniscope") << "Miniscope on " << bestVar << std::endl;
2364 : : // make the bodies
2365 : 22 : std::vector<Node> qlit1;
2366 : 22 : qlit1.insert(
2367 : 22 : qlit1.begin(), varLits[bestVar].begin(), varLits[bestVar].end());
2368 : 22 : std::vector<Node> qlitt;
2369 : : // for all literals not containing bestVar
2370 [ + + ]: 76 : for (size_t i = 0; i < body.getNumChildren(); i++)
2371 : : {
2372 [ + + ]: 54 : if (std::find(qlit1.begin(), qlit1.end(), body[i]) == qlit1.end())
2373 : : {
2374 : 32 : qlitt.push_back(body[i]);
2375 : : }
2376 : : }
2377 : : // make the variable lists
2378 : 22 : std::vector<Node> qvl1;
2379 : 22 : std::vector<Node> qvl2;
2380 : 22 : std::vector<Node> qvsh;
2381 [ + + ]: 88 : for (unsigned i = 0; i < args.size(); i++)
2382 : : {
2383 : 66 : bool found1 = false;
2384 : 66 : bool found2 = false;
2385 [ + + ]: 142 : for (size_t j = 0; j < varLits[args[i]].size(); j++)
2386 : : {
2387 : 196 : if (!found1
2388 [ + + ][ + + ]: 250 : && std::find(qlit1.begin(), qlit1.end(), varLits[args[i]][j])
2389 [ + + ]: 250 : != qlit1.end())
2390 : : {
2391 : 44 : found1 = true;
2392 : : }
2393 : 108 : else if (!found2
2394 [ + + ][ + - ]: 142 : && std::find(qlitt.begin(), qlitt.end(), varLits[args[i]][j])
2395 [ + + ]: 142 : != qlitt.end())
2396 : : {
2397 : 44 : found2 = true;
2398 : : }
2399 [ + + ][ + + ]: 98 : if (found1 && found2)
2400 : : {
2401 : 22 : break;
2402 : : }
2403 : : }
2404 [ + + ]: 66 : if (found1)
2405 : : {
2406 [ + + ]: 44 : if (found2)
2407 : : {
2408 : 22 : qvsh.push_back(args[i]);
2409 : : }
2410 : : else
2411 : : {
2412 : 22 : qvl1.push_back(args[i]);
2413 : : }
2414 : : }
2415 : : else
2416 : : {
2417 [ - + ][ - + ]: 22 : Assert(found2);
[ - - ]
2418 : 22 : qvl2.push_back(args[i]);
2419 : : }
2420 : : }
2421 [ - + ][ - + ]: 22 : Assert(!qvl1.empty());
[ - - ]
2422 : : // check for literals that only contain shared variables
2423 : 22 : std::vector<Node> qlitsh;
2424 : 22 : std::vector<Node> qlit2;
2425 [ + + ]: 54 : for (size_t i = 0; i < qlitt.size(); i++)
2426 : : {
2427 : 32 : bool hasVar2 = false;
2428 [ + + ]: 44 : for (size_t j = 0; j < litVars[qlitt[i]].size(); j++)
2429 : : {
2430 : 34 : if (std::find(qvl2.begin(), qvl2.end(), litVars[qlitt[i]][j])
2431 [ + + ]: 68 : != qvl2.end())
2432 : : {
2433 : 22 : hasVar2 = true;
2434 : 22 : break;
2435 : : }
2436 : : }
2437 [ + + ]: 32 : if (hasVar2)
2438 : : {
2439 : 22 : qlit2.push_back(qlitt[i]);
2440 : : }
2441 : : else
2442 : : {
2443 : 10 : qlitsh.push_back(qlitt[i]);
2444 : : }
2445 : : }
2446 : 22 : varLits.clear();
2447 : 22 : litVars.clear();
2448 [ + - ]: 44 : Trace("ag-miniscope-debug")
2449 : 0 : << "Split into literals : " << qlit1.size() << " / " << qlit2.size()
2450 : 22 : << " / " << qlitsh.size();
2451 [ + - ]: 44 : Trace("ag-miniscope-debug")
2452 : 0 : << ", variables : " << qvl1.size() << " / " << qvl2.size() << " / "
2453 : 22 : << qvsh.size() << std::endl;
2454 : : Node n1 =
2455 [ + - ]: 22 : qlit1.size() == 1 ? qlit1[0] : nodeManager()->mkNode(Kind::OR, qlit1);
2456 : 22 : n1 = computeAggressiveMiniscoping(qvl1, n1);
2457 : 22 : qlitsh.push_back(n1);
2458 [ + + ]: 22 : if (!qlit2.empty())
2459 : : {
2460 : 14 : Node n2 = qlit2.size() == 1 ? qlit2[0]
2461 [ + + ]: 14 : : nodeManager()->mkNode(Kind::OR, qlit2);
2462 : 12 : n2 = computeAggressiveMiniscoping(qvl2, n2);
2463 : 12 : qlitsh.push_back(n2);
2464 : 12 : }
2465 : 22 : Node n = nodeManager()->mkNode(Kind::OR, qlitsh);
2466 [ + - ]: 22 : if (!qvsh.empty())
2467 : : {
2468 : 22 : Node bvl = nodeManager()->mkNode(Kind::BOUND_VAR_LIST, qvsh);
2469 : 22 : n = nodeManager()->mkNode(Kind::FORALL, bvl, n);
2470 : 22 : }
2471 [ + - ]: 22 : Trace("ag-miniscope") << "Return " << n << " for " << body << std::endl;
2472 : 22 : return n;
2473 : 22 : }
2474 [ + + ]: 104 : }
2475 : 338 : QAttributes qa;
2476 : 338 : return mkForAll(args, body, qa);
2477 : 360 : }
2478 : :
2479 : 2 : bool QuantifiersRewriter::isStandard(const Node& q, const Options& opts)
2480 : : {
2481 : 2 : QAttributes qa;
2482 : 2 : QuantAttributes::computeQuantAttributes(q, qa);
2483 : 4 : return isStandard(qa, opts);
2484 : 2 : }
2485 : :
2486 : 4440947 : bool QuantifiersRewriter::isStandard(QAttributes& qa, const Options& opts)
2487 : : {
2488 : 4440947 : bool is_strict_trigger =
2489 : 4440947 : qa.d_hasPattern
2490 [ + + ][ + + ]: 4440947 : && opts.quantifiers.userPatternsQuant == options::UserPatMode::STRICT;
2491 [ + + ][ + - ]: 4440947 : return qa.isStandard() && !is_strict_trigger;
2492 : : }
2493 : :
2494 : 6102 : Node QuantifiersRewriter::computeRewriteBody(const Node& n,
2495 : : TConvProofGenerator* pg) const
2496 : : {
2497 [ - + ][ - + ]: 6102 : Assert(n.getKind() == Kind::FORALL);
[ - - ]
2498 : 6102 : QAttributes qa;
2499 : 6102 : QuantAttributes::computeQuantAttributes(n, qa);
2500 : 12204 : std::vector<Node> args(n[0].begin(), n[0].end());
2501 : 6102 : Node body = computeProcessTerms(n, args, n[1], qa, pg);
2502 [ + + ]: 6102 : if (body != n[1])
2503 : : {
2504 : 1119 : std::vector<Node> children;
2505 : 1119 : children.push_back(n[0]);
2506 : 1119 : children.push_back(body);
2507 [ + + ]: 1119 : if (n.getNumChildren() == 3)
2508 : : {
2509 : 39 : children.push_back(n[2]);
2510 : : }
2511 : 1119 : return d_nm->mkNode(Kind::FORALL, children);
2512 : 1119 : }
2513 : 4983 : return n;
2514 : 6102 : }
2515 : :
2516 : 4440945 : bool QuantifiersRewriter::doOperation(Node q,
2517 : : RewriteStep computeOption,
2518 : : QAttributes& qa) const
2519 : : {
2520 : 4440945 : bool is_strict_trigger =
2521 : 4440945 : qa.d_hasPattern
2522 [ + + ][ + + ]: 4440945 : && d_opts.quantifiers.userPatternsQuant == options::UserPatMode::STRICT;
2523 : 4440945 : bool is_std = isStandard(qa, d_opts);
2524 [ + + ]: 4440945 : if (computeOption == COMPUTE_ELIM_SHADOW
2525 [ + + ]: 3950365 : || computeOption == COMPUTE_ELIM_SYMBOLS)
2526 : : {
2527 : 981055 : return true;
2528 : : }
2529 [ + + ]: 3459890 : else if (computeOption == COMPUTE_MINISCOPING
2530 [ + + ]: 3003212 : || computeOption == COMPUTE_AGGRESSIVE_MINISCOPING)
2531 : : {
2532 : : // in the rare case the body is ground, we always eliminate unless it
2533 : : // is truly a non-standard quantified formula (e.g. one for QE).
2534 [ + + ]: 895202 : if (!expr::hasBoundVar(q[1]))
2535 : : {
2536 : : // This returns true if q is a non-standard quantified formula. Note that
2537 : : // is_std is additionally true if user-pat is strict and q has user
2538 : : // patterns.
2539 : 2849 : return qa.isStandard();
2540 : : }
2541 [ + + ]: 892353 : if (!is_std)
2542 : : {
2543 : 35004 : return false;
2544 : : }
2545 : : // do not miniscope if we have user patterns unless option is set
2546 [ + - ][ + + ]: 857349 : if (!d_opts.quantifiers.miniscopeQuantUser && qa.d_hasPattern)
2547 : : {
2548 : 77834 : return false;
2549 : : }
2550 [ + + ]: 779515 : if (computeOption == COMPUTE_AGGRESSIVE_MINISCOPING)
2551 : : {
2552 : 380958 : return d_opts.quantifiers.miniscopeQuant
2553 : 380958 : == options::MiniscopeQuantMode::AGG;
2554 : : }
2555 : 398557 : return true;
2556 : : }
2557 [ + + ]: 2564688 : else if (computeOption == COMPUTE_EXT_REWRITE)
2558 : : {
2559 : 421290 : return d_opts.quantifiers.extRewriteQuant;
2560 : : }
2561 [ + + ]: 2143398 : else if (computeOption == COMPUTE_PROCESS_TERMS)
2562 : : {
2563 : 438505 : return true;
2564 : : }
2565 [ + + ]: 1704893 : else if (computeOption == COMPUTE_COND_SPLIT)
2566 : : {
2567 : 422007 : return (d_opts.quantifiers.iteDtTesterSplitQuant
2568 [ + - ]: 416801 : || d_opts.quantifiers.condVarSplitQuant
2569 : : != options::CondVarSplitQuantMode::OFF)
2570 [ + + ][ + + ]: 838808 : && !is_strict_trigger;
2571 : : }
2572 [ + + ]: 1282886 : else if (computeOption == COMPUTE_PRENEX)
2573 : : {
2574 : : // do not prenex to pull variables into those with user patterns
2575 [ + + ][ + + ]: 431485 : if (!d_opts.quantifiers.prenexQuantUser && qa.d_hasPattern)
2576 : : {
2577 : 38917 : return false;
2578 : : }
2579 [ + + ]: 392568 : if (qa.d_hasPool)
2580 : : {
2581 : 340 : return false;
2582 : : }
2583 : 392228 : return d_opts.quantifiers.prenexQuant != options::PrenexQuantMode::NONE
2584 [ + + ]: 389699 : && d_opts.quantifiers.miniscopeQuant
2585 : : != options::MiniscopeQuantMode::AGG
2586 [ + + ][ + + ]: 781927 : && is_std;
2587 : : }
2588 [ + + ]: 851401 : else if (computeOption == COMPUTE_VAR_ELIMINATION)
2589 : : {
2590 [ + + ][ + + ]: 429307 : return d_opts.quantifiers.varElimQuant && is_std && !is_strict_trigger;
[ + - ]
2591 : : }
2592 [ + - ]: 422094 : else if (computeOption == COMPUTE_DT_VAR_EXPAND)
2593 : : {
2594 [ + - ][ + + ]: 422094 : return d_opts.quantifiers.dtVarExpandQuant && is_std && !is_strict_trigger;
[ + - ]
2595 : : }
2596 : : else
2597 : : {
2598 : 0 : return false;
2599 : : }
2600 : : }
2601 : :
2602 : : // general method for computing various rewrites
2603 : 3426352 : Node QuantifiersRewriter::computeOperation(Node f,
2604 : : RewriteStep computeOption,
2605 : : QAttributes& qa)
2606 : : {
2607 [ + - ]: 6852704 : Trace("quantifiers-rewrite-debug")
2608 : 0 : << "Compute operation " << computeOption << " on " << f << " "
2609 : 3426352 : << qa.d_qid_num << std::endl;
2610 [ + + ]: 3426352 : if (computeOption == COMPUTE_ELIM_SHADOW)
2611 : : {
2612 : 490580 : Node qr = rewriteViaRule(ProofRewriteRule::MACRO_QUANT_ELIM_SHADOW, f);
2613 [ + + ]: 490580 : return qr.isNull() ? f : qr;
2614 : 490580 : }
2615 [ + + ]: 2935772 : else if (computeOption == COMPUTE_MINISCOPING)
2616 : : {
2617 [ + + ]: 399119 : if (d_opts.quantifiers.prenexQuant == options::PrenexQuantMode::NORMAL)
2618 : : {
2619 [ + + ]: 117 : if (!qa.d_qid_num.isNull())
2620 : : {
2621 : : // already processed this, return self
2622 : 38 : return f;
2623 : : }
2624 : : }
2625 : 399081 : bool miniscopeConj = doMiniscopeConj(d_opts);
2626 : 399081 : bool miniscopeFv = doMiniscopeFv(d_opts);
2627 : : // return directly
2628 : 399081 : return computeMiniscoping(f, qa, miniscopeConj, miniscopeFv);
2629 : : }
2630 : 5073306 : std::vector<Node> args(f[0].begin(), f[0].end());
2631 : 2536653 : Node n = f[1];
2632 [ + + ]: 2536653 : if (computeOption == COMPUTE_ELIM_SYMBOLS)
2633 : : {
2634 : : // relies on external utility
2635 : 490475 : n = booleans::TheoryBoolRewriter::computeNnfNorm(nodeManager(), n);
2636 : : }
2637 [ + + ]: 2046178 : else if (computeOption == COMPUTE_AGGRESSIVE_MINISCOPING)
2638 : : {
2639 : 326 : return computeAggressiveMiniscoping(args, n);
2640 : : }
2641 [ + + ]: 2045852 : else if (computeOption == COMPUTE_EXT_REWRITE)
2642 : : {
2643 : 34 : return computeExtendedRewrite(f, qa);
2644 : : }
2645 [ + + ]: 2045818 : else if (computeOption == COMPUTE_PROCESS_TERMS)
2646 : : {
2647 : 438505 : n = computeProcessTerms(f, args, n, qa);
2648 : : }
2649 [ + + ]: 1607313 : else if (computeOption == COMPUTE_COND_SPLIT)
2650 : : {
2651 : 421971 : n = computeCondSplit(n, args, qa);
2652 : : }
2653 [ + + ]: 1185342 : else if (computeOption == COMPUTE_PRENEX)
2654 : : {
2655 [ + + ]: 371495 : if (d_opts.quantifiers.prenexQuant == options::PrenexQuantMode::NORMAL)
2656 : : {
2657 : : // will rewrite at preprocess time
2658 : 85 : return f;
2659 : : }
2660 : : else
2661 : : {
2662 : 371410 : std::vector<Node> argsSet, nargsSet;
2663 : 371410 : n = computePrenex(f, n, argsSet, nargsSet, true, false);
2664 [ - + ][ - + ]: 371410 : Assert(nargsSet.empty());
[ - - ]
2665 : 371410 : args.insert(args.end(), argsSet.begin(), argsSet.end());
2666 : 371410 : }
2667 : : }
2668 [ + + ]: 813847 : else if (computeOption == COMPUTE_VAR_ELIMINATION)
2669 : : {
2670 : 410393 : n = computeVarElimination(n, args, qa);
2671 : : }
2672 [ + - ]: 403454 : else if (computeOption == COMPUTE_DT_VAR_EXPAND)
2673 : : {
2674 : : size_t index;
2675 : 403454 : return computeDtVarExpand(nodeManager(), f, index);
2676 : : }
2677 [ + - ]: 4265508 : Trace("quantifiers-rewrite-debug")
2678 : 2132754 : << "Compute Operation: return " << n << ", " << args.size() << std::endl;
2679 : 2132754 : if (f[1] == n && args.size() == f[0].getNumChildren())
2680 : : {
2681 : 2081829 : return f;
2682 : : }
2683 : : else
2684 : : {
2685 [ + + ]: 50925 : if (args.empty())
2686 : : {
2687 : 2432 : return n;
2688 : : }
2689 : : else
2690 : : {
2691 : 48493 : std::vector<Node> children;
2692 : 48493 : children.push_back(nodeManager()->mkNode(Kind::BOUND_VAR_LIST, args));
2693 : 48493 : children.push_back(n);
2694 [ + + ][ + + ]: 48493 : if (!qa.d_ipl.isNull() && args.size() == f[0].getNumChildren())
[ + + ][ + + ]
[ - - ]
2695 : : {
2696 : 4846 : children.push_back(qa.d_ipl);
2697 : : }
2698 : 48493 : return nodeManager()->mkNode(Kind::FORALL, children);
2699 : 48493 : }
2700 : : }
2701 : 2536653 : }
2702 : 821037 : bool QuantifiersRewriter::doMiniscopeConj(const Options& opts)
2703 : : {
2704 : 821037 : options::MiniscopeQuantMode mqm = opts.quantifiers.miniscopeQuant;
2705 : : return mqm == options::MiniscopeQuantMode::CONJ_AND_FV
2706 [ + - ]: 31753 : || mqm == options::MiniscopeQuantMode::CONJ
2707 [ + + ][ + + ]: 852790 : || mqm == options::MiniscopeQuantMode::AGG;
2708 : : }
2709 : :
2710 : 399081 : bool QuantifiersRewriter::doMiniscopeFv(const Options& opts)
2711 : : {
2712 : 399081 : options::MiniscopeQuantMode mqm = opts.quantifiers.miniscopeQuant;
2713 : : return mqm == options::MiniscopeQuantMode::CONJ_AND_FV
2714 [ + + ]: 14007 : || mqm == options::MiniscopeQuantMode::FV
2715 [ + + ][ + + ]: 413088 : || mqm == options::MiniscopeQuantMode::AGG;
2716 : : }
2717 : :
2718 : 0 : bool QuantifiersRewriter::isPrenexNormalForm(Node n)
2719 : : {
2720 [ - - ]: 0 : if (n.getKind() == Kind::FORALL)
2721 : : {
2722 : 0 : return n[1].getKind() != Kind::FORALL && isPrenexNormalForm(n[1]);
2723 : : }
2724 [ - - ]: 0 : else if (n.getKind() == Kind::NOT)
2725 : : {
2726 : 0 : return n[0].getKind() != Kind::NOT && isPrenexNormalForm(n[0]);
2727 : : }
2728 : : else
2729 : : {
2730 : 0 : return !expr::hasClosure(n);
2731 : : }
2732 : : }
2733 : :
2734 : : } // namespace quantifiers
2735 : : } // namespace theory
2736 : : } // namespace cvc5::internal
|
