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