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 "options/quantifiers_options.h"
26 : : #include "proof/conv_proof_generator.h"
27 : : #include "theory/arith/arith_msum.h"
28 : : #include "theory/booleans/theory_bool_rewriter.h"
29 : : #include "theory/datatypes/theory_datatypes_utils.h"
30 : : #include "theory/quantifiers/bv_inverter.h"
31 : : #include "theory/quantifiers/ematching/trigger.h"
32 : : #include "theory/quantifiers/extended_rewrite.h"
33 : : #include "theory/quantifiers/quant_split.h"
34 : : #include "theory/quantifiers/quantifiers_attributes.h"
35 : : #include "theory/quantifiers/skolemize.h"
36 : : #include "theory/quantifiers/term_database.h"
37 : : #include "theory/quantifiers/term_util.h"
38 : : #include "theory/rewriter.h"
39 : : #include "theory/strings/theory_strings_utils.h"
40 : : #include "theory/uf/theory_uf_rewriter.h"
41 : : #include "util/rational.h"
42 : :
43 : : using namespace std;
44 : : using namespace cvc5::internal::kind;
45 : : using namespace cvc5::context;
46 : :
47 : : namespace cvc5::internal {
48 : : namespace theory {
49 : : namespace quantifiers {
50 : :
51 : : /**
52 : : * Attributes used for constructing bound variables in a canonical way. These
53 : : * are attributes that map to bound variable, introduced for the following
54 : : * purposes:
55 : : * - QRewPrenexAttribute: cached on (v, body) where we are prenexing bound
56 : : * variable v in a nested quantified formula within the given body.
57 : : * - QRewMiniscopeAttribute: cached on (v, q, i) where q is being miniscoped
58 : : * for F_i in its body (and F_1 ... F_n), and v is one of the bound variables
59 : : * that q binds.
60 : : * - QRewDtExpandAttribute: cached on (F, lit, a) where lit is the tested
61 : : * literal used for expanding a quantified datatype variable in quantified
62 : : * formula with body F, and a is the rational corresponding to the argument
63 : : * position of the variable, e.g. lit is ((_ is C) x) and x is
64 : : * replaced by (C y1 ... yn), where the argument position of yi is i.
65 : : */
66 : : struct QRewPrenexAttributeId
67 : : {
68 : : };
69 : : using QRewPrenexAttribute = expr::Attribute<QRewPrenexAttributeId, Node>;
70 : : struct QRewMiniscopeAttributeId
71 : : {
72 : : };
73 : : using QRewMiniscopeAttribute = expr::Attribute<QRewMiniscopeAttributeId, Node>;
74 : : struct QRewDtExpandAttributeId
75 : : {
76 : : };
77 : : using QRewDtExpandAttribute = expr::Attribute<QRewDtExpandAttributeId, Node>;
78 : :
79 : 0 : std::ostream& operator<<(std::ostream& out, RewriteStep s)
80 : : {
81 [ - - ][ - - ]: 0 : switch (s)
[ - - ][ - - ]
[ - ]
82 : : {
83 : 0 : case COMPUTE_ELIM_SYMBOLS: out << "COMPUTE_ELIM_SYMBOLS"; break;
84 : 0 : case COMPUTE_MINISCOPING: out << "COMPUTE_MINISCOPING"; break;
85 : 0 : case COMPUTE_AGGRESSIVE_MINISCOPING:
86 : 0 : out << "COMPUTE_AGGRESSIVE_MINISCOPING";
87 : 0 : break;
88 : 0 : case COMPUTE_PROCESS_TERMS: out << "COMPUTE_PROCESS_TERMS"; break;
89 : 0 : case COMPUTE_PRENEX: out << "COMPUTE_PRENEX"; break;
90 : 0 : case COMPUTE_VAR_ELIMINATION: out << "COMPUTE_VAR_ELIMINATION"; break;
91 : 0 : case COMPUTE_COND_SPLIT: out << "COMPUTE_COND_SPLIT"; break;
92 : 0 : case COMPUTE_EXT_REWRITE: out << "COMPUTE_EXT_REWRITE"; break;
93 : 0 : default: out << "UnknownRewriteStep"; break;
94 : : }
95 : 0 : return out;
96 : : }
97 : :
98 : 134633 : QuantifiersRewriter::QuantifiersRewriter(NodeManager* nm,
99 : : Rewriter* r,
100 : 134633 : const Options& opts)
101 : 134633 : : TheoryRewriter(nm), d_rewriter(r), d_opts(opts)
102 : : {
103 : 134633 : registerProofRewriteRule(ProofRewriteRule::EXISTS_ELIM,
104 : : TheoryRewriteCtx::PRE_DSL);
105 : 134633 : registerProofRewriteRule(ProofRewriteRule::QUANT_UNUSED_VARS,
106 : : TheoryRewriteCtx::PRE_DSL);
107 : : // QUANT_MERGE_PRENEX is part of the reconstruction for
108 : : // MACRO_QUANT_MERGE_PRENEX
109 : 134633 : registerProofRewriteRule(ProofRewriteRule::MACRO_QUANT_MERGE_PRENEX,
110 : : TheoryRewriteCtx::PRE_DSL);
111 : 134633 : registerProofRewriteRule(ProofRewriteRule::MACRO_QUANT_PRENEX,
112 : : TheoryRewriteCtx::PRE_DSL);
113 : 134633 : registerProofRewriteRule(ProofRewriteRule::MACRO_QUANT_MINISCOPE,
114 : : TheoryRewriteCtx::PRE_DSL);
115 : : // QUANT_MINISCOPE_OR is part of the reconstruction for MACRO_QUANT_MINISCOPE
116 : 134633 : registerProofRewriteRule(ProofRewriteRule::MACRO_QUANT_PARTITION_CONNECTED_FV,
117 : : TheoryRewriteCtx::PRE_DSL);
118 : : // note ProofRewriteRule::QUANT_DT_SPLIT is done by a module dynamically with
119 : : // manual proof generation thus not registered here.
120 : 134633 : registerProofRewriteRule(ProofRewriteRule::MACRO_QUANT_VAR_ELIM_EQ,
121 : : TheoryRewriteCtx::PRE_DSL);
122 : 134633 : registerProofRewriteRule(ProofRewriteRule::MACRO_QUANT_VAR_ELIM_INEQ,
123 : : TheoryRewriteCtx::PRE_DSL);
124 : 134633 : registerProofRewriteRule(ProofRewriteRule::MACRO_QUANT_REWRITE_BODY,
125 : : TheoryRewriteCtx::PRE_DSL);
126 : 134633 : }
127 : :
128 : 40330 : Node QuantifiersRewriter::rewriteViaRule(ProofRewriteRule id, const Node& n)
129 : : {
130 [ + + ][ + + ]: 40330 : switch (id)
[ + + ][ + + ]
[ + + ][ + + ]
[ - ]
131 : : {
132 : 5665 : case ProofRewriteRule::EXISTS_ELIM:
133 : : {
134 [ + + ]: 5665 : if (n.getKind() != Kind::EXISTS)
135 : : {
136 : 4481 : return Node::null();
137 : : }
138 : 1184 : std::vector<Node> fchildren;
139 : 1184 : fchildren.push_back(n[0]);
140 : 1184 : fchildren.push_back(n[1].notNode());
141 [ + + ]: 1184 : if (n.getNumChildren() == 3)
142 : : {
143 : 5 : fchildren.push_back(n[2]);
144 : : }
145 : 1184 : return d_nm->mkNode(Kind::NOT, d_nm->mkNode(Kind::FORALL, fchildren));
146 : : }
147 : 5244 : case ProofRewriteRule::QUANT_UNUSED_VARS:
148 : : {
149 [ - + ]: 5244 : if (!n.isClosure())
150 : : {
151 : 990 : return Node::null();
152 : : }
153 : 10488 : std::vector<Node> vars(n[0].begin(), n[0].end());
154 : 5244 : std::vector<Node> activeVars;
155 : 5244 : computeArgVec(vars, activeVars, n[1]);
156 [ + + ]: 5244 : if (activeVars.size() < vars.size())
157 : : {
158 [ + + ]: 990 : if (activeVars.empty())
159 : : {
160 : 699 : return n[1];
161 : : }
162 : : return d_nm->mkNode(
163 : 291 : n.getKind(), d_nm->mkNode(Kind::BOUND_VAR_LIST, activeVars), n[1]);
164 : : }
165 : : }
166 : 4254 : break;
167 : 4983 : case ProofRewriteRule::MACRO_QUANT_MERGE_PRENEX:
168 : : case ProofRewriteRule::QUANT_MERGE_PRENEX:
169 : : {
170 [ - + ]: 4983 : if (!n.isClosure())
171 : : {
172 : 801 : return Node::null();
173 : : }
174 : : // Don't check standard here, which can't be replicated in a proof checker
175 : : // without modelling the patterns.
176 : : // We remove duplicates if the macro version.
177 : : Node q = mergePrenex(
178 : 4983 : n, false, id == ProofRewriteRule::MACRO_QUANT_MERGE_PRENEX);
179 [ + + ]: 4983 : if (q != n)
180 : : {
181 : 801 : return q;
182 : : }
183 : : }
184 : 4182 : break;
185 : 4355 : case ProofRewriteRule::MACRO_QUANT_PRENEX:
186 : : {
187 [ + - ]: 4355 : if (n.getKind() == Kind::FORALL)
188 : : {
189 : 4355 : std::vector<Node> args, nargs;
190 : 8710 : Node nn = computePrenex(n, n[1], args, nargs, true, false);
191 [ - + ][ - + ]: 4355 : Assert(nargs.empty());
[ - - ]
192 [ + + ]: 4355 : if (!args.empty())
193 : : {
194 : 2088 : std::vector<Node> qargs(n[0].begin(), n[0].end());
195 : 696 : qargs.insert(qargs.end(), args.begin(), args.end());
196 : 696 : Node bvl = d_nm->mkNode(Kind::BOUND_VAR_LIST, qargs);
197 : 696 : return d_nm->mkNode(Kind::FORALL, bvl, nn);
198 : : }
199 : : }
200 : : }
201 : 3659 : break;
202 : 4172 : case ProofRewriteRule::MACRO_QUANT_MINISCOPE:
203 : : {
204 [ - + ]: 4172 : if (n.getKind() != Kind::FORALL)
205 : : {
206 : 4148 : return Node::null();
207 : : }
208 : 4172 : Kind k = n[1].getKind();
209 [ + + ][ + + ]: 4172 : if (k != Kind::AND && k != Kind::ITE)
210 : : {
211 : 3803 : return Node::null();
212 : : }
213 : : // note that qa is not needed; moreover external proofs should be agnostic
214 : : // to it
215 : 369 : QAttributes qa;
216 : 369 : QuantAttributes::computeQuantAttributes(n, qa);
217 : 369 : Node nret = computeMiniscoping(n, qa, true, false);
218 [ + + ]: 369 : if (nret != n)
219 : : {
220 : 345 : return nret;
221 : : }
222 : : }
223 : 24 : break;
224 : 275 : case ProofRewriteRule::QUANT_MINISCOPE_AND:
225 : : {
226 [ + - ][ - + ]: 275 : if (n.getKind() != Kind::FORALL || n[1].getKind() != Kind::AND)
[ + - ][ - + ]
[ - - ]
227 : : {
228 : 0 : return Node::null();
229 : : }
230 : 550 : std::vector<Node> conj;
231 [ + + ]: 1165 : for (const Node& nc : n[1])
232 : : {
233 : 890 : conj.push_back(d_nm->mkNode(Kind::FORALL, n[0], nc));
234 : : }
235 : 275 : return d_nm->mkAnd(conj);
236 : : }
237 : : break;
238 : 4057 : case ProofRewriteRule::MACRO_QUANT_PARTITION_CONNECTED_FV:
239 : : {
240 [ + - ][ + + ]: 4057 : if (n.getKind() != Kind::FORALL || n[1].getKind() != Kind::OR)
[ + - ][ + + ]
[ - - ]
241 : : {
242 : 5768 : return Node::null();
243 : : }
244 : : // note that qa is not needed; moreover external proofs should be agnostic
245 : : // to it
246 : 1385 : QAttributes qa;
247 : 1385 : QuantAttributes::computeQuantAttributes(n, qa);
248 : 2770 : std::vector<Node> vars(n[0].begin(), n[0].end());
249 : 1385 : Node body = n[1];
250 : 1385 : Node nret = computeSplit(vars, body, qa);
251 [ + + ]: 1385 : if (!nret.isNull())
252 : : {
253 : : // only do this rule if it is a proper split; otherwise it will be
254 : : // subsumed by QUANT_UNUSED_VARS.
255 [ + + ]: 432 : if (nret.getKind() == Kind::OR)
256 : : {
257 : 424 : return nret;
258 : : }
259 : : }
260 : : }
261 : 961 : break;
262 : 394 : case ProofRewriteRule::QUANT_MINISCOPE_OR:
263 : : {
264 [ + - ][ - + ]: 394 : if (n.getKind() != Kind::FORALL || n[1].getKind() != Kind::OR)
[ + - ][ - + ]
[ - - ]
265 : : {
266 : 0 : return Node::null();
267 : : }
268 : 394 : size_t nvars = n[0].getNumChildren();
269 : 788 : std::vector<Node> disj;
270 : 788 : std::unordered_set<Node> varsUsed;
271 : 394 : size_t varIndex = 0;
272 [ + + ]: 1629 : for (const Node& d : n[1])
273 : : {
274 : : // Note that we may apply to a nested quantified formula, in which
275 : : // case some variables in fvs may not be bound by this quantified
276 : : // formula.
277 : 1235 : std::unordered_set<Node> fvs;
278 : 1235 : expr::getFreeVariables(d, fvs);
279 : 1235 : size_t prevVarIndex = varIndex;
280 : 2203 : while (varIndex < nvars && fvs.find(n[0][varIndex]) != fvs.end())
281 : : {
282 : : // cannot have shadowing
283 [ - + ]: 968 : if (varsUsed.find(n[0][varIndex]) != varsUsed.end())
284 : : {
285 : 0 : return Node::null();
286 : : }
287 : 968 : varsUsed.insert(n[0][varIndex]);
288 : 968 : varIndex++;
289 : : }
290 : 2470 : std::vector<Node> dvs(n[0].begin() + prevVarIndex,
291 : 4940 : n[0].begin() + varIndex);
292 [ + + ]: 1235 : if (dvs.empty())
293 : : {
294 : 732 : disj.emplace_back(d);
295 : : }
296 : : else
297 : : {
298 : 503 : Node bvl = d_nm->mkNode(Kind::BOUND_VAR_LIST, dvs);
299 : 503 : disj.emplace_back(d_nm->mkNode(Kind::FORALL, bvl, d));
300 : : }
301 : : }
302 : : // must consume all variables
303 [ + + ]: 394 : if (varIndex != nvars)
304 : : {
305 : 18 : return Node::null();
306 : : }
307 : 752 : Node ret = d_nm->mkOr(disj);
308 : : // go back and ensure all variables are bound
309 : 752 : std::unordered_set<Node> fvs;
310 : 376 : expr::getFreeVariables(ret, fvs);
311 [ + + ]: 1344 : for (const Node& v : n[0])
312 : : {
313 [ - + ]: 968 : if (fvs.find(v) != fvs.end())
314 : : {
315 : 0 : return Node::null();
316 : : }
317 : : }
318 : 376 : return ret;
319 : : }
320 : : break;
321 : 54 : case ProofRewriteRule::QUANT_MINISCOPE_ITE:
322 : : {
323 [ + - ][ - + ]: 54 : if (n.getKind() != Kind::FORALL || n[1].getKind() != Kind::ITE)
[ + - ][ - + ]
[ - - ]
324 : : {
325 : 54 : return Node::null();
326 : : }
327 : 108 : std::vector<Node> args(n[0].begin(), n[0].end());
328 : 54 : Node body = n[1];
329 [ + - ]: 54 : if (!expr::hasSubterm(body[0], args))
330 : : {
331 : : return d_nm->mkNode(Kind::ITE,
332 : : body[0],
333 : 108 : d_nm->mkNode(Kind::FORALL, n[0], body[1]),
334 : 162 : d_nm->mkNode(Kind::FORALL, n[0], body[2]));
335 : : }
336 : : }
337 : 0 : break;
338 : 21 : case ProofRewriteRule::QUANT_DT_SPLIT:
339 : : {
340 : : // always runs split utility on the first variable
341 : 21 : if (n.getKind() != Kind::FORALL || !n[0][0].getType().isDatatype())
342 : : {
343 : 0 : return Node::null();
344 : : }
345 : 21 : return QuantDSplit::split(nodeManager(), n, 0);
346 : : }
347 : : break;
348 : 7565 : case ProofRewriteRule::MACRO_QUANT_VAR_ELIM_EQ:
349 : : case ProofRewriteRule::QUANT_VAR_ELIM_EQ:
350 : : case ProofRewriteRule::MACRO_QUANT_VAR_ELIM_INEQ:
351 : : {
352 [ + - ][ + + ]: 7565 : if (n.getKind() != Kind::FORALL || n.getNumChildren() != 2)
[ + + ]
353 : : {
354 : 1204 : return Node::null();
355 : : }
356 : 15010 : std::vector<Node> args(n[0].begin(), n[0].end());
357 : 7505 : std::vector<Node> vars;
358 : 7505 : std::vector<Node> subs;
359 : 7505 : Node body = n[1];
360 [ + + ]: 7505 : if (id == ProofRewriteRule::MACRO_QUANT_VAR_ELIM_EQ)
361 : : {
362 : 3954 : std::vector<Node> lits;
363 : 3954 : getVarElim(body, args, vars, subs, lits);
364 : : }
365 [ + + ]: 3551 : else if (id == ProofRewriteRule::QUANT_VAR_ELIM_EQ)
366 : : {
367 [ - + ]: 148 : if (args.size() != 1)
368 : : {
369 : 0 : return Node::null();
370 : : }
371 : 148 : std::vector<Node> lits;
372 [ + - ]: 148 : if (body.getKind() == Kind::OR)
373 : : {
374 : 148 : lits.insert(lits.end(), body.begin(), body.end());
375 : : }
376 : : else
377 : : {
378 : 0 : lits.push_back(body);
379 : : }
380 : 148 : if (lits[0].getKind() != Kind::NOT
381 [ + - ][ - + ]: 296 : || lits[0][0].getKind() != Kind::EQUAL)
[ + - ][ - + ]
[ - - ]
382 : : {
383 : 0 : return Node::null();
384 : : }
385 : 148 : Node eq = lits[0][0];
386 : 148 : if (eq[0] != args[0] || expr::hasSubterm(eq[1], eq[0]))
387 : : {
388 : 0 : return Node::null();
389 : : }
390 : 148 : vars.push_back(eq[0]);
391 : 148 : subs.push_back(eq[1]);
392 : 148 : args.clear();
393 : 148 : std::vector<Node> remLits(lits.begin() + 1, lits.end());
394 : 148 : body = d_nm->mkOr(remLits);
395 : : }
396 : : else
397 : : {
398 : : // assume empty attribute
399 : 3403 : QAttributes qa;
400 : 3403 : getVarElimIneq(n[1], args, vars, subs, qa);
401 : : }
402 : : // if we eliminated a variable, update body and reprocess
403 [ + + ]: 7505 : if (!vars.empty())
404 : : {
405 [ - + ][ - + ]: 1084 : Assert(vars.size() == subs.size());
[ - - ]
406 : 2168 : std::vector<Node> qc(n.begin(), n.end());
407 : 1084 : qc[1] =
408 : 2168 : body.substitute(vars.begin(), vars.end(), subs.begin(), subs.end());
409 [ + + ]: 1084 : if (args.empty())
410 : : {
411 : 596 : return qc[1];
412 : : }
413 : 488 : qc[0] = d_nm->mkNode(Kind::BOUND_VAR_LIST, args);
414 : 488 : return d_nm->mkNode(Kind::FORALL, qc);
415 : : }
416 : : }
417 : 6421 : break;
418 : 3545 : case ProofRewriteRule::MACRO_QUANT_REWRITE_BODY:
419 : : {
420 [ - + ]: 3545 : if (n.getKind() != Kind::FORALL)
421 : : {
422 : 1189 : return Node::null();
423 : : }
424 : 3545 : Node nr = computeRewriteBody(n);
425 [ + + ]: 3545 : if (nr != n)
426 : : {
427 : 1189 : return nr;
428 : : }
429 : : }
430 : 2356 : break;
431 : 0 : default: break;
432 : : }
433 : 21857 : return Node::null();
434 : : }
435 : :
436 : 40375 : bool QuantifiersRewriter::isLiteral( Node n ){
437 [ - - ][ + + ]: 40375 : switch( n.getKind() ){
438 : 0 : case Kind::NOT:
439 : 0 : return n[0].getKind() != Kind::NOT && isLiteral(n[0]);
440 : : break;
441 : 0 : case Kind::OR:
442 : : case Kind::AND:
443 : : case Kind::IMPLIES:
444 : : case Kind::XOR:
445 : 0 : case Kind::ITE: return false; break;
446 : 19704 : case Kind::EQUAL:
447 : : // for boolean terms
448 : 19704 : return !n[0].getType().isBoolean();
449 : : break;
450 : 20671 : default: break;
451 : : }
452 : 20671 : return true;
453 : : }
454 : :
455 : 27812900 : void QuantifiersRewriter::computeArgs(const std::vector<Node>& args,
456 : : std::map<Node, bool>& activeMap,
457 : : Node n,
458 : : std::map<Node, bool>& visited)
459 : : {
460 [ + + ]: 27812900 : if( visited.find( n )==visited.end() ){
461 : 18749800 : visited[n] = true;
462 [ + + ]: 18749800 : if (n.getKind() == Kind::BOUND_VARIABLE)
463 : : {
464 [ + + ]: 3924490 : if( std::find( args.begin(), args.end(), n )!=args.end() ){
465 : 3206870 : activeMap[ n ] = true;
466 : : }
467 : : }
468 : : else
469 : : {
470 [ + + ]: 14825300 : if (n.hasOperator())
471 : : {
472 : 8844820 : computeArgs(args, activeMap, n.getOperator(), visited);
473 : : }
474 [ + + ]: 32396400 : for( int i=0; i<(int)n.getNumChildren(); i++ ){
475 : 17571100 : computeArgs( args, activeMap, n[i], visited );
476 : : }
477 : : }
478 : : }
479 : 27812900 : }
480 : :
481 : 784929 : void QuantifiersRewriter::computeArgVec(const std::vector<Node>& args,
482 : : std::vector<Node>& activeArgs,
483 : : Node n)
484 : : {
485 [ - + ][ - + ]: 784929 : Assert(activeArgs.empty());
[ - - ]
486 : 1569860 : std::map< Node, bool > activeMap;
487 : 1569860 : std::map< Node, bool > visited;
488 : 784929 : computeArgs( args, activeMap, n, visited );
489 [ + + ]: 784929 : if( !activeMap.empty() ){
490 : 778608 : std::map<Node, bool>::iterator it;
491 [ + + ]: 74018400 : for (const Node& v : args)
492 : : {
493 : 73239800 : it = activeMap.find(v);
494 [ + + ]: 73239800 : if (it != activeMap.end())
495 : : {
496 : 2166110 : activeArgs.emplace_back(v);
497 : : // no longer active, which accounts for deleting duplicates
498 : 2166110 : activeMap.erase(it);
499 : : }
500 : : }
501 : : }
502 : 784929 : }
503 : :
504 : 306361 : void QuantifiersRewriter::computeArgVec2(const std::vector<Node>& args,
505 : : std::vector<Node>& activeArgs,
506 : : Node n,
507 : : Node ipl)
508 : : {
509 [ - + ][ - + ]: 306361 : Assert(activeArgs.empty());
[ - - ]
510 : 612722 : std::map< Node, bool > activeMap;
511 : 612722 : std::map< Node, bool > visited;
512 : 306361 : computeArgs( args, activeMap, n, visited );
513 : : // Collect variables in inst pattern list only if we cannot eliminate
514 : : // quantifier, or if we have an add-to-pool annotation.
515 : 306361 : bool varComputePatList = !activeMap.empty();
516 [ + + ]: 307502 : for (const Node& ip : ipl)
517 : : {
518 : 1141 : Kind k = ip.getKind();
519 [ + - ][ - + ]: 1141 : if (k == Kind::INST_ADD_TO_POOL || k == Kind::SKOLEM_ADD_TO_POOL)
520 : : {
521 : 0 : varComputePatList = true;
522 : 0 : break;
523 : : }
524 : : }
525 [ + + ]: 306361 : if (varComputePatList)
526 : : {
527 : 305706 : computeArgs( args, activeMap, ipl, visited );
528 : : }
529 [ + + ]: 306361 : if (!activeMap.empty())
530 : : {
531 [ + + ]: 1347880 : for (const Node& a : args)
532 : : {
533 [ + + ]: 1042170 : if (activeMap.find(a) != activeMap.end())
534 : : {
535 : 1040760 : activeArgs.push_back(a);
536 : : }
537 : : }
538 : : }
539 : 306361 : }
540 : :
541 : 750328 : RewriteResponse QuantifiersRewriter::preRewrite(TNode q)
542 : : {
543 : 750328 : Kind k = q.getKind();
544 [ + + ][ + + ]: 750328 : if (k == Kind::FORALL || k == Kind::EXISTS)
545 : : {
546 : : // Do prenex merging now, since this may impact trigger selection.
547 : : // In particular consider:
548 : : // (forall ((x Int)) (forall ((y Int)) (! (P x) :pattern ((f x)))))
549 : : // If we wait until post-rewrite, we would rewrite the inner quantified
550 : : // formula, dropping the pattern, so the entire formula becomes:
551 : : // (forall ((x Int)) (P x))
552 : : // Instead, we merge to:
553 : : // (forall ((x Int) (y Int)) (! (P x) :pattern ((f x))))
554 : : // eagerly here, where after we would drop y to obtain:
555 : : // (forall ((x Int)) (! (P x) :pattern ((f x))))
556 : : // See issue #10303.
557 : 493876 : Node qm = mergePrenex(q, true, true);
558 [ + + ]: 493876 : if (q != qm)
559 : : {
560 : 3824 : return RewriteResponse(REWRITE_AGAIN_FULL, qm);
561 : : }
562 : : }
563 : 746504 : return RewriteResponse(REWRITE_DONE, q);
564 : : }
565 : :
566 : 667140 : RewriteResponse QuantifiersRewriter::postRewrite(TNode in)
567 : : {
568 [ + - ]: 667140 : Trace("quantifiers-rewrite-debug") << "post-rewriting " << in << std::endl;
569 : 667140 : RewriteStatus status = REWRITE_DONE;
570 : 1334280 : Node ret = in;
571 : 667140 : RewriteStep rew_op = COMPUTE_LAST;
572 : : // get the body
573 [ + + ]: 667140 : if (in.getKind() == Kind::EXISTS)
574 : : {
575 : 9308 : std::vector<Node> children;
576 : 9308 : children.push_back(in[0]);
577 : 9308 : children.push_back(in[1].notNode());
578 [ + + ]: 9308 : if (in.getNumChildren() == 3)
579 : : {
580 : 79 : children.push_back(in[2]);
581 : : }
582 : 9308 : ret = nodeManager()->mkNode(Kind::FORALL, children);
583 : 9308 : ret = ret.negate();
584 : 9308 : status = REWRITE_AGAIN_FULL;
585 : : }
586 [ + + ]: 657832 : else if (in.getKind() == Kind::FORALL)
587 : : {
588 : : // do prenex merging
589 : 401380 : ret = mergePrenex(in, true, true);
590 [ + + ]: 401380 : if (ret != in)
591 : : {
592 : 60 : status = REWRITE_AGAIN_FULL;
593 : : }
594 [ + + ][ + + ]: 401320 : else if (in[1].isConst() && in.getNumChildren() == 2)
[ + - ][ + + ]
[ - - ]
595 : : {
596 : 2045 : return RewriteResponse( status, in[1] );
597 : : }
598 : : else
599 : : {
600 : : //compute attributes
601 : 798550 : QAttributes qa;
602 : 399275 : QuantAttributes::computeQuantAttributes( in, qa );
603 [ + + ]: 3188480 : for (unsigned i = 0; i < COMPUTE_LAST; ++i)
604 : : {
605 : 2851680 : RewriteStep op = static_cast<RewriteStep>(i);
606 [ + + ]: 2851680 : if( doOperation( in, op, qa ) ){
607 : 2031070 : ret = computeOperation( in, op, qa );
608 [ + + ]: 2031070 : if( ret!=in ){
609 : 62475 : rew_op = op;
610 : 62475 : status = REWRITE_AGAIN_FULL;
611 : 62475 : break;
612 : : }
613 : : }
614 : : }
615 : : }
616 : : }
617 : : //print if changed
618 [ + + ]: 665095 : if( in!=ret ){
619 [ + - ]: 71843 : Trace("quantifiers-rewrite") << "*** rewrite (op=" << rew_op << ") " << in << std::endl;
620 [ + - ]: 71843 : Trace("quantifiers-rewrite") << " to " << std::endl;
621 [ + - ]: 71843 : Trace("quantifiers-rewrite") << ret << std::endl;
622 : : }
623 : 665095 : return RewriteResponse( status, ret );
624 : : }
625 : :
626 : 900239 : Node QuantifiersRewriter::mergePrenex(const Node& q, bool checkStd, bool rmDup)
627 : : {
628 [ + + ][ - + ]: 900239 : Assert(q.getKind() == Kind::FORALL || q.getKind() == Kind::EXISTS);
[ - + ][ - - ]
629 : 900239 : Kind k = q.getKind();
630 : 1800480 : std::vector<Node> boundVars;
631 : 1800480 : Node body = q;
632 : 900239 : bool combineQuantifiers = false;
633 : 900239 : bool continueCombine = false;
634 [ + + ]: 915128 : do
635 : : {
636 [ + + ]: 915128 : if (rmDup)
637 : : {
638 [ + + ]: 4201030 : for (const Node& v : body[0])
639 : : {
640 [ + + ]: 3287220 : if (std::find(boundVars.begin(), boundVars.end(), v) == boundVars.end())
641 : : {
642 : 3287080 : boundVars.push_back(v);
643 : : }
644 : : else
645 : : {
646 : : // if duplicate variable due to shadowing, we must rewrite
647 : 141 : combineQuantifiers = true;
648 : : }
649 : : }
650 : : }
651 : : else
652 : : {
653 : 1318 : boundVars.insert(boundVars.end(), body[0].begin(), body[0].end());
654 : : }
655 : 915128 : continueCombine = false;
656 [ + + ][ + + ]: 915128 : if (body.getNumChildren() == 2 && body[1].getKind() == k)
[ + + ][ + + ]
[ - - ]
657 : : {
658 : 14889 : bool process = true;
659 [ + + ]: 14889 : if (checkStd)
660 : : {
661 : : // Should never combine a quantified formula with a pool or
662 : : // non-standard quantified formula here.
663 : : // Note that we technically should check
664 : : // doOperation(body[1], COMPUTE_PRENEX, qa) here, although this
665 : : // is too restrictive, as sometimes nested patterns should just be
666 : : // applied to the top level, for example:
667 : : // (forall ((x Int)) (forall ((y Int)) (! P :pattern ((f x y)))))
668 : : // should be a pattern for the top-level quantifier here.
669 : 13484 : QAttributes qa;
670 : 13484 : QuantAttributes::computeQuantAttributes(body[1], qa);
671 : 13484 : process = qa.isStandard();
672 : : }
673 [ + - ]: 14889 : if (process)
674 : : {
675 : 14889 : body = body[1];
676 : 14889 : continueCombine = true;
677 : 14889 : combineQuantifiers = true;
678 : : }
679 : : }
680 : : } while (continueCombine);
681 [ + + ]: 900239 : if (combineQuantifiers)
682 : : {
683 : 4685 : NodeManager* nm = nodeManager();
684 : 9370 : std::vector<Node> children;
685 : 4685 : children.push_back(nm->mkNode(Kind::BOUND_VAR_LIST, boundVars));
686 : 4685 : children.push_back(body[1]);
687 [ + + ]: 4685 : if (body.getNumChildren() == 3)
688 : : {
689 : 224 : children.push_back(body[2]);
690 : : }
691 : 4685 : return nm->mkNode(k, children);
692 : : }
693 : 895554 : return q;
694 : : }
695 : :
696 : 71 : void QuantifiersRewriter::computeDtTesterIteSplit(
697 : : Node n,
698 : : std::map<Node, Node>& pcons,
699 : : std::map<Node, std::map<int, Node>>& ncons,
700 : : std::vector<Node>& conj) const
701 : : {
702 [ + - ][ + + ]: 97 : if (n.getKind() == Kind::ITE && n[0].getKind() == Kind::APPLY_TESTER
[ - - ]
703 : 97 : && n[1].getType().isBoolean())
704 : : {
705 [ + - ]: 26 : Trace("quantifiers-rewrite-ite-debug") << "Split tester condition : " << n << std::endl;
706 : 52 : Node x = n[0][0];
707 : 26 : std::map< Node, Node >::iterator itp = pcons.find( x );
708 [ - + ]: 26 : if( itp!=pcons.end() ){
709 [ - - ]: 0 : Trace("quantifiers-rewrite-ite-debug") << "...condition already set " << itp->second << std::endl;
710 [ - - ]: 0 : computeDtTesterIteSplit( n[ itp->second==n[0] ? 1 : 2 ], pcons, ncons, conj );
711 : : }else{
712 : 52 : Node tester = n[0].getOperator();
713 : 26 : int index = datatypes::utils::indexOf(tester);
714 : 26 : std::map< int, Node >::iterator itn = ncons[x].find( index );
715 [ - + ]: 26 : if( itn!=ncons[x].end() ){
716 [ - - ]: 0 : Trace("quantifiers-rewrite-ite-debug") << "...condition negated " << itn->second << std::endl;
717 : 0 : computeDtTesterIteSplit( n[ 2 ], pcons, ncons, conj );
718 : : }else{
719 [ + + ]: 78 : for( unsigned i=0; i<2; i++ ){
720 [ + + ]: 52 : if( i==0 ){
721 : 26 : pcons[x] = n[0];
722 : : }else{
723 : 26 : pcons.erase( x );
724 : 26 : ncons[x][index] = n[0].negate();
725 : : }
726 : 52 : computeDtTesterIteSplit( n[i+1], pcons, ncons, conj );
727 : : }
728 : 26 : ncons[x].erase( index );
729 : : }
730 : : }
731 : : }
732 : : else
733 : : {
734 : 45 : NodeManager* nm = nodeManager();
735 [ + - ]: 45 : Trace("quantifiers-rewrite-ite-debug") << "Return value : " << n << std::endl;
736 : 90 : std::vector< Node > children;
737 : 45 : children.push_back( n );
738 : 90 : std::vector< Node > vars;
739 : : //add all positive testers
740 [ + + ]: 71 : for( std::map< Node, Node >::iterator it = pcons.begin(); it != pcons.end(); ++it ){
741 : 26 : children.push_back( it->second.negate() );
742 : 26 : vars.push_back( it->first );
743 : : }
744 : : //add all negative testers
745 [ + + ]: 104 : for( std::map< Node, std::map< int, Node > >::iterator it = ncons.begin(); it != ncons.end(); ++it ){
746 : 118 : Node x = it->first;
747 : : //only if we haven't settled on a positive tester
748 [ + + ]: 59 : if( std::find( vars.begin(), vars.end(), x )==vars.end() ){
749 : : //check if we have exhausted all options but one
750 : 33 : const DType& dt = x.getType().getDType();
751 : 66 : std::vector< Node > nchildren;
752 : 33 : int pos_cons = -1;
753 [ + + ]: 99 : for( int i=0; i<(int)dt.getNumConstructors(); i++ ){
754 : 66 : std::map< int, Node >::iterator itt = it->second.find( i );
755 [ + + ]: 66 : if( itt==it->second.end() ){
756 [ + - ]: 33 : pos_cons = pos_cons==-1 ? i : -2;
757 : : }else{
758 : 33 : nchildren.push_back( itt->second.negate() );
759 : : }
760 : : }
761 [ + - ]: 33 : if( pos_cons>=0 ){
762 : 33 : Node tester = dt[pos_cons].getTester();
763 : 33 : children.push_back(
764 : 66 : nm->mkNode(Kind::APPLY_TESTER, tester, x).negate());
765 : : }else{
766 : 0 : children.insert( children.end(), nchildren.begin(), nchildren.end() );
767 : : }
768 : : }
769 : : }
770 : : //make condition/output pair
771 : 45 : Node c = children.size() == 1 ? children[0]
772 [ - + ]: 90 : : nodeManager()->mkNode(Kind::OR, children);
773 : 45 : conj.push_back( c );
774 : : }
775 : 71 : }
776 : :
777 : 362418 : Node QuantifiersRewriter::computeProcessTerms(const Node& q,
778 : : const std::vector<Node>& args,
779 : : Node body,
780 : : QAttributes& qa,
781 : : TConvProofGenerator* pg) const
782 : : {
783 : 362418 : options::IteLiftQuantMode iteLiftMode = options::IteLiftQuantMode::NONE;
784 [ + + ]: 362418 : if (qa.isStandard())
785 : : {
786 : 345802 : iteLiftMode = d_opts.quantifiers.iteLiftQuant;
787 : : }
788 : 362418 : std::map<Node, Node> cache;
789 : 724836 : return computeProcessTerms2(q, args, body, cache, iteLiftMode, pg);
790 : : }
791 : :
792 : 11220700 : Node QuantifiersRewriter::computeProcessTerms2(
793 : : const Node& q,
794 : : const std::vector<Node>& args,
795 : : Node body,
796 : : std::map<Node, Node>& cache,
797 : : options::IteLiftQuantMode iteLiftMode,
798 : : TConvProofGenerator* pg) const
799 : : {
800 : 11220700 : NodeManager* nm = nodeManager();
801 [ + - ]: 22441300 : Trace("quantifiers-rewrite-term-debug2")
802 : 11220700 : << "computeProcessTerms " << body << std::endl;
803 : 11220700 : std::map< Node, Node >::iterator iti = cache.find( body );
804 [ + + ]: 11220700 : if( iti!=cache.end() ){
805 : 3459940 : return iti->second;
806 : : }
807 : 7760720 : bool changed = false;
808 : 15521400 : std::vector<Node> children;
809 [ + + ]: 18619000 : for (const Node& bc : body)
810 : : {
811 : : // do the recursive call on children
812 : 10858200 : Node nn = computeProcessTerms2(q, args, bc, cache, iteLiftMode, pg);
813 : 10858200 : children.push_back(nn);
814 [ + + ][ + + ]: 10858200 : changed = changed || nn != bc;
815 : : }
816 : :
817 : : // make return value
818 : 15521400 : Node ret;
819 [ + + ]: 7760720 : if (changed)
820 : : {
821 [ + + ]: 35360 : if (body.getMetaKind() == kind::metakind::PARAMETERIZED)
822 : : {
823 : 888 : children.insert(children.begin(), body.getOperator());
824 : : }
825 : 35360 : ret = nm->mkNode(body.getKind(), children);
826 : : }
827 : : else
828 : : {
829 : 7725360 : ret = body;
830 : : }
831 : :
832 : 15521400 : Node retOrig = ret;
833 [ + - ]: 15521400 : Trace("quantifiers-rewrite-term-debug2")
834 : 7760720 : << "Returning " << ret << " for " << body << std::endl;
835 : : // do context-independent rewriting
836 [ + + ]: 7760720 : if (ret.isClosure())
837 : : {
838 : : // Ensure no shadowing. If this term is a closure quantifying a variable
839 : : // in args, then we introduce fresh variable(s) and replace this closure
840 : : // to be over the fresh variables instead.
841 : 186130 : std::vector<Node> oldVars;
842 : 186130 : std::vector<Node> newVars;
843 [ + + ]: 227057 : for (size_t i = 0, nvars = ret[0].getNumChildren(); i < nvars; i++)
844 : : {
845 : 267984 : const Node& v = ret[0][i];
846 [ + + ]: 133992 : if (std::find(args.begin(), args.end(), v) != args.end())
847 : : {
848 [ + - ]: 278 : Trace("quantifiers-rewrite-unshadow")
849 : 139 : << "Found shadowed variable " << v << " in " << q << std::endl;
850 : 139 : oldVars.push_back(v);
851 : 278 : Node nv = ElimShadowNodeConverter::getElimShadowVar(q, ret, i);
852 : 139 : newVars.push_back(nv);
853 : : }
854 : : }
855 [ + + ]: 93065 : if (!oldVars.empty())
856 : : {
857 [ - + ][ - + ]: 139 : Assert(oldVars.size() == newVars.size());
[ - - ]
858 : : Node sbody = ret.substitute(
859 : 278 : oldVars.begin(), oldVars.end(), newVars.begin(), newVars.end());
860 : 139 : ret = sbody;
861 : : }
862 : : }
863 : 7667660 : else if (ret.getKind() == Kind::EQUAL
864 [ + + ][ + + ]: 7667660 : && iteLiftMode != options::IteLiftQuantMode::NONE)
[ + + ]
865 : : {
866 [ + + ]: 3565100 : for (size_t i = 0; i < 2; i++)
867 : : {
868 [ + + ]: 2377440 : if (ret[i].getKind() == Kind::ITE)
869 : : {
870 [ + + ]: 74456 : Node no = i == 0 ? ret[1] : ret[0];
871 [ + + ]: 74456 : if (no.getKind() != Kind::ITE)
872 : : {
873 : 68086 : bool doRewrite = (iteLiftMode == options::IteLiftQuantMode::ALL);
874 : 68086 : std::vector<Node> childrenIte;
875 : 68086 : childrenIte.push_back(ret[i][0]);
876 [ + + ]: 204258 : for (size_t j = 1; j <= 2; j++)
877 : : {
878 : : // check if it rewrites to a constant
879 : 408516 : Node nn = nm->mkNode(Kind::EQUAL, no, ret[i][j]);
880 : 136172 : childrenIte.push_back(nn);
881 : : // check if it will rewrite to a constant
882 : 136172 : if (no == ret[i][j] || (no.isConst() && ret[i][j].isConst()))
883 : : {
884 : 1674 : doRewrite = true;
885 : : }
886 : : }
887 [ + + ]: 68086 : if (doRewrite)
888 : : {
889 : 1276 : ret = nm->mkNode(Kind::ITE, childrenIte);
890 : 1276 : break;
891 : : }
892 : : }
893 : : }
894 : : }
895 : : }
896 [ + + ][ + + ]: 6478720 : else if (ret.getKind() == Kind::SELECT && ret[0].getKind() == Kind::STORE)
[ + + ][ + + ]
[ - - ]
897 : : {
898 : 716 : Node st = ret[0];
899 : 716 : Node index = ret[1];
900 : 716 : std::vector<Node> iconds;
901 : 716 : std::vector<Node> elements;
902 [ + + ]: 1328 : while (st.getKind() == Kind::STORE)
903 : : {
904 : 970 : iconds.push_back(index.eqNode(st[1]));
905 : 970 : elements.push_back(st[2]);
906 : 970 : st = st[0];
907 : : }
908 : 358 : ret = nm->mkNode(Kind::SELECT, st, index);
909 : : // conditions
910 [ + + ]: 1328 : for (int i = (iconds.size() - 1); i >= 0; i--)
911 : : {
912 : 970 : ret = nm->mkNode(Kind::ITE, iconds[i], elements[i], ret);
913 : : }
914 : : }
915 [ + + ][ + + ]: 6478370 : else if (ret.getKind() == Kind::HO_APPLY && !ret.getType().isFunction())
[ + + ][ + + ]
[ - - ]
916 : : {
917 : : // fully applied functions are converted to APPLY_UF here.
918 : 46442 : Node fullApp = uf::TheoryUfRewriter::getApplyUfForHoApply(ret);
919 : : // it may not be possible to convert e.g. if the head is not a variable
920 [ + - ]: 23221 : if (!fullApp.isNull())
921 : : {
922 : 23221 : ret = fullApp;
923 : : }
924 : : }
925 [ + + ]: 7760720 : if (pg != nullptr)
926 : : {
927 [ + + ]: 5995 : if (retOrig != ret)
928 : : {
929 : 777 : pg->addRewriteStep(retOrig,
930 : : ret,
931 : : nullptr,
932 : : false,
933 : : TrustId::MACRO_THEORY_REWRITE_RCONS_SIMPLE);
934 : : }
935 : : }
936 : 7760720 : cache[body] = ret;
937 : 7760720 : return ret;
938 : : }
939 : :
940 : 28 : Node QuantifiersRewriter::computeExtendedRewrite(TNode q,
941 : : const QAttributes& qa) const
942 : : {
943 : : // do not apply to recursive functions
944 [ + + ]: 28 : if (qa.isFunDef())
945 : : {
946 : 8 : return q;
947 : : }
948 : 40 : Node body = q[1];
949 : : // apply extended rewriter
950 : 40 : Node bodyr = d_rewriter->extendedRewrite(body);
951 [ + + ]: 20 : if (body != bodyr)
952 : : {
953 : 12 : std::vector<Node> children;
954 : 6 : children.push_back(q[0]);
955 : 6 : children.push_back(bodyr);
956 [ - + ]: 6 : if (q.getNumChildren() == 3)
957 : : {
958 : 0 : children.push_back(q[2]);
959 : : }
960 : 6 : return nodeManager()->mkNode(Kind::FORALL, children);
961 : : }
962 : 14 : return q;
963 : : }
964 : :
965 : 337418 : Node QuantifiersRewriter::computeCondSplit(Node body,
966 : : const std::vector<Node>& args,
967 : : QAttributes& qa) const
968 : : {
969 : 337418 : NodeManager* nm = nodeManager();
970 : 337418 : Kind bk = body.getKind();
971 [ + + ]: 5329 : if (d_opts.quantifiers.iteDtTesterSplitQuant && bk == Kind::ITE
972 [ + + ][ + + ]: 342747 : && body[0].getKind() == Kind::APPLY_TESTER)
[ + + ][ + + ]
[ - - ]
973 : : {
974 [ + - ]: 19 : Trace("quantifiers-rewrite-ite-debug") << "DTT split : " << body << std::endl;
975 : 19 : std::map< Node, Node > pcons;
976 : 19 : std::map< Node, std::map< int, Node > > ncons;
977 : 19 : std::vector< Node > conj;
978 : 19 : computeDtTesterIteSplit( body, pcons, ncons, conj );
979 [ - + ][ - + ]: 19 : Assert(!conj.empty());
[ - - ]
980 [ + - ]: 19 : if( conj.size()>1 ){
981 [ + - ]: 19 : Trace("quantifiers-rewrite-ite") << "*** Split ITE (datatype tester) " << body << " into : " << std::endl;
982 [ + + ]: 64 : for( unsigned i=0; i<conj.size(); i++ ){
983 [ + - ]: 45 : Trace("quantifiers-rewrite-ite") << " " << conj[i] << std::endl;
984 : : }
985 : 19 : return nm->mkNode(Kind::AND, conj);
986 : : }
987 : : }
988 [ - + ]: 337399 : if (d_opts.quantifiers.condVarSplitQuant
989 : : == options::CondVarSplitQuantMode::OFF)
990 : : {
991 : 0 : return body;
992 : : }
993 [ + - ]: 674798 : Trace("cond-var-split-debug")
994 : 337399 : << "Conditional var elim split " << body << "?" << std::endl;
995 : : // we only do this splitting if miniscoping is enabled, as this is
996 : : // required to eliminate variables in conjuncts below. We also never
997 : : // miniscope non-standard quantifiers, so this is also guarded here.
998 [ + + ][ + + ]: 337399 : if (!doMiniscopeConj(d_opts) || !qa.isStandard())
[ + + ]
999 : : {
1000 : 26146 : return body;
1001 : : }
1002 : :
1003 : 311253 : bool aggCondSplit = (d_opts.quantifiers.condVarSplitQuant
1004 : : == options::CondVarSplitQuantMode::AGG);
1005 : 311253 : if (bk == Kind::ITE
1006 : 311253 : || (bk == Kind::EQUAL && body[0].getType().isBoolean() && aggCondSplit))
1007 : : {
1008 [ - + ][ - + ]: 445 : Assert(!qa.isFunDef());
[ - - ]
1009 : 445 : bool do_split = false;
1010 : 445 : unsigned index_max = bk == Kind::ITE ? 0 : 1;
1011 : 445 : std::vector<Node> tmpArgs = args;
1012 [ + + ]: 759 : for (unsigned index = 0; index <= index_max; index++)
1013 : : {
1014 [ + + ][ - - ]: 445 : if (hasVarElim(body[index], true, tmpArgs)
1015 [ + + ][ - + ]: 445 : || hasVarElim(body[index], false, tmpArgs))
[ + + ][ + - ]
[ - - ]
1016 : : {
1017 : 131 : do_split = true;
1018 : 131 : break;
1019 : : }
1020 : : }
1021 [ + + ]: 445 : if (do_split)
1022 : : {
1023 : 262 : Node pos;
1024 : 131 : Node neg;
1025 [ + - ]: 131 : if (bk == Kind::ITE)
1026 : : {
1027 : 131 : pos = nm->mkNode(Kind::OR, body[0].negate(), body[1]);
1028 : 131 : neg = nm->mkNode(Kind::OR, body[0], body[2]);
1029 : : }
1030 : : else
1031 : : {
1032 : 0 : pos = nm->mkNode(Kind::OR, body[0].negate(), body[1]);
1033 : 0 : neg = nm->mkNode(Kind::OR, body[0], body[1].negate());
1034 : : }
1035 [ + - ]: 262 : Trace("cond-var-split-debug") << "*** Split (conditional variable eq) "
1036 : 131 : << body << " into : " << std::endl;
1037 [ + - ]: 131 : Trace("cond-var-split-debug") << " " << pos << std::endl;
1038 [ + - ]: 131 : Trace("cond-var-split-debug") << " " << neg << std::endl;
1039 : 131 : return nm->mkNode(Kind::AND, pos, neg);
1040 : : }
1041 : : }
1042 : :
1043 [ + + ]: 311122 : if (bk == Kind::OR)
1044 : : {
1045 : 130194 : unsigned size = body.getNumChildren();
1046 : 130194 : bool do_split = false;
1047 : 130194 : unsigned split_index = 0;
1048 [ + + ]: 514644 : for (unsigned i = 0; i < size; i++)
1049 : : {
1050 : : // check if this child is a (conditional) variable elimination
1051 : 384956 : Node b = body[i];
1052 [ + + ]: 384956 : if (b.getKind() == Kind::AND)
1053 : : {
1054 : 44004 : std::vector<Node> vars;
1055 : 44004 : std::vector<Node> subs;
1056 : 44004 : std::vector<Node> tmpArgs = args;
1057 [ + + ]: 80255 : for (unsigned j = 0, bsize = b.getNumChildren(); j < bsize; j++)
1058 : : {
1059 [ + + ]: 58759 : if (getVarElimLit(body, b[j], false, tmpArgs, vars, subs))
1060 : : {
1061 [ + - ]: 13048 : Trace("cond-var-split-debug") << "Variable elimination in child #"
1062 : 6524 : << j << " under " << i << std::endl;
1063 : : // Figure out if we should split
1064 : : // Currently we split if the aggressive option is set, or
1065 : : // if the top-level OR is binary.
1066 [ + - ][ + + ]: 6524 : if (aggCondSplit || size == 2)
1067 : : {
1068 : 506 : do_split = true;
1069 : : }
1070 : : // other splitting criteria go here
1071 : :
1072 [ + + ]: 6524 : if (do_split)
1073 : : {
1074 : 506 : split_index = i;
1075 : 506 : break;
1076 : : }
1077 : 6018 : vars.clear();
1078 : 6018 : subs.clear();
1079 : 6018 : tmpArgs = args;
1080 : : }
1081 : : }
1082 : : }
1083 [ + + ]: 384956 : if (do_split)
1084 : : {
1085 : 506 : break;
1086 : : }
1087 : : }
1088 [ + + ]: 130194 : if (do_split)
1089 : : {
1090 : : // For the sake of proofs, if we are not splitting the first child,
1091 : : // we first rearrange so that it is first, which can be proven by
1092 : : // ACI_NORM.
1093 : 1012 : std::vector<Node> splitChildren;
1094 [ + + ]: 506 : if (split_index != 0)
1095 : : {
1096 : 132 : splitChildren.push_back(body[split_index]);
1097 [ + + ]: 396 : for (size_t i = 0; i < size; i++)
1098 : : {
1099 [ + + ]: 264 : if (i != split_index)
1100 : : {
1101 : 132 : splitChildren.push_back(body[i]);
1102 : : }
1103 : : }
1104 : 132 : return nm->mkNode(Kind::OR, splitChildren);
1105 : : }
1106 : : // This is expected to be proven by the RARE rule bool-or-and-distrib.
1107 : 748 : std::vector<Node> children;
1108 [ + + ]: 1122 : for (TNode bc : body)
1109 : : {
1110 : 748 : children.push_back(bc);
1111 : : }
1112 [ + + ]: 1495 : for (TNode bci : body[split_index])
1113 : : {
1114 : 1121 : children[split_index] = bci;
1115 : 1121 : splitChildren.push_back(nm->mkNode(Kind::OR, children));
1116 : : }
1117 : : // split the AND child, for example:
1118 : : // ( x!=a ^ P(x) ) V Q(x) ---> ( x!=a V Q(x) ) ^ ( P(x) V Q(x) )
1119 : 374 : return nm->mkNode(Kind::AND, splitChildren);
1120 : : }
1121 : : }
1122 : :
1123 : 310616 : return body;
1124 : : }
1125 : :
1126 : 14796 : bool QuantifiersRewriter::isVarElim(Node v, Node s)
1127 : : {
1128 [ - + ][ - + ]: 14796 : Assert(v.getKind() == Kind::BOUND_VARIABLE);
[ - - ]
1129 : 14796 : return !expr::hasSubterm(s, v) && s.getType() == v.getType();
1130 : : }
1131 : :
1132 : 100251 : Node QuantifiersRewriter::getVarElimEq(Node lit,
1133 : : const std::vector<Node>& args,
1134 : : Node& var) const
1135 : : {
1136 [ - + ][ - + ]: 100251 : Assert(lit.getKind() == Kind::EQUAL);
[ - - ]
1137 : 100251 : Node slv;
1138 : 200502 : TypeNode tt = lit[0].getType();
1139 [ + + ]: 100251 : if (tt.isRealOrInt())
1140 : : {
1141 : 50838 : slv = getVarElimEqReal(lit, args, var);
1142 : : }
1143 [ + + ]: 49413 : else if (tt.isBitVector())
1144 : : {
1145 : 1679 : slv = getVarElimEqBv(lit, args, var);
1146 : : }
1147 [ + + ]: 47734 : else if (tt.isStringLike())
1148 : : {
1149 : 221 : slv = getVarElimEqString(lit, args, var);
1150 : : }
1151 : 200502 : return slv;
1152 : : }
1153 : :
1154 : 50838 : Node QuantifiersRewriter::getVarElimEqReal(Node lit,
1155 : : const std::vector<Node>& args,
1156 : : Node& var) const
1157 : : {
1158 : : // for arithmetic, solve the equality
1159 : 101676 : std::map<Node, Node> msum;
1160 [ - + ]: 50838 : if (!ArithMSum::getMonomialSumLit(lit, msum))
1161 : : {
1162 : 0 : return Node::null();
1163 : : }
1164 : 50838 : std::vector<Node>::const_iterator ita;
1165 [ + + ]: 153183 : for (std::map<Node, Node>::iterator itm = msum.begin(); itm != msum.end();
1166 : 102345 : ++itm)
1167 : : {
1168 [ + + ]: 103033 : if (itm->first.isNull())
1169 : : {
1170 : 10024 : continue;
1171 : : }
1172 : 93009 : ita = std::find(args.begin(), args.end(), itm->first);
1173 [ + + ]: 93009 : if (ita != args.end())
1174 : : {
1175 : 1586 : Node veq_c;
1176 : 1586 : Node val;
1177 : 1586 : int ires = ArithMSum::isolate(itm->first, msum, veq_c, val, Kind::EQUAL);
1178 : 1586 : if (ires != 0 && veq_c.isNull() && isVarElim(itm->first, val))
1179 : : {
1180 : 688 : var = itm->first;
1181 : 688 : return val;
1182 : : }
1183 : : }
1184 : : }
1185 : 50150 : return Node::null();
1186 : : }
1187 : :
1188 : 1679 : Node QuantifiersRewriter::getVarElimEqBv(Node lit,
1189 : : const std::vector<Node>& args,
1190 : : Node& var) const
1191 : : {
1192 [ - + ]: 1679 : if (TraceIsOn("quant-velim-bv"))
1193 : : {
1194 [ - - ]: 0 : Trace("quant-velim-bv") << "Bv-Elim : " << lit << " varList = { ";
1195 [ - - ]: 0 : for (const Node& v : args)
1196 : : {
1197 [ - - ]: 0 : Trace("quant-velim-bv") << v << " ";
1198 : : }
1199 [ - - ]: 0 : Trace("quant-velim-bv") << "} ?" << std::endl;
1200 : : }
1201 [ - + ][ - + ]: 1679 : Assert(lit.getKind() == Kind::EQUAL);
[ - - ]
1202 : : // TODO (#1494) : linearize the literal using utility
1203 : :
1204 : : // compute a subset active_args of the bound variables args that occur in lit
1205 : 3358 : std::vector<Node> active_args;
1206 : 1679 : computeArgVec(args, active_args, lit);
1207 : :
1208 : 3358 : BvInverter binv(d_opts);
1209 [ + + ]: 3573 : for (const Node& cvar : active_args)
1210 : : {
1211 : : // solve for the variable on this path using the inverter
1212 : 2019 : std::vector<unsigned> path;
1213 : 4038 : Node slit = binv.getPathToPv(lit, cvar, path);
1214 [ + + ]: 2019 : if (!slit.isNull())
1215 : : {
1216 : 1856 : Node slv = binv.solveBvLit(cvar, lit, path, nullptr);
1217 [ + - ]: 928 : Trace("quant-velim-bv") << "...solution : " << slv << std::endl;
1218 [ + + ]: 928 : if (!slv.isNull())
1219 : : {
1220 : 375 : var = cvar;
1221 : : // if this is a proper variable elimination, that is, var = slv where
1222 : : // var is not in the free variables of slv, then we can return this
1223 : : // as the variable elimination for lit.
1224 [ + + ]: 375 : if (isVarElim(var, slv))
1225 : : {
1226 : 125 : return slv;
1227 : : }
1228 : : }
1229 : : }
1230 : : else
1231 : : {
1232 [ + - ]: 1091 : Trace("quant-velim-bv") << "...non-invertible path." << std::endl;
1233 : : }
1234 : : }
1235 : :
1236 : 1554 : return Node::null();
1237 : : }
1238 : :
1239 : 221 : Node QuantifiersRewriter::getVarElimEqString(Node lit,
1240 : : const std::vector<Node>& args,
1241 : : Node& var) const
1242 : : {
1243 [ - + ][ - + ]: 221 : Assert(lit.getKind() == Kind::EQUAL);
[ - - ]
1244 : : // The reasoning below involves equality entailment as
1245 : : // (= (str.++ s x t) r) entails (= x (str.substr r (str.len s) _)),
1246 : : // but these equalities are not equivalent.
1247 [ + + ]: 221 : if (!d_opts.quantifiers.varEntEqElimQuant)
1248 : : {
1249 : 184 : return Node::null();
1250 : : }
1251 : 37 : NodeManager* nm = nodeManager();
1252 [ + + ]: 92 : for (unsigned i = 0; i < 2; i++)
1253 : : {
1254 [ + + ]: 74 : if (lit[i].getKind() == Kind::STRING_CONCAT)
1255 : : {
1256 : 37 : TypeNode stype = lit[i].getType();
1257 [ + + ]: 92 : for (unsigned j = 0, nchildren = lit[i].getNumChildren(); j < nchildren;
1258 : : j++)
1259 : : {
1260 [ + + ]: 74 : if (std::find(args.begin(), args.end(), lit[i][j]) != args.end())
1261 : : {
1262 : 55 : var = lit[i][j];
1263 : 55 : Node slv = lit[1 - i];
1264 : 110 : std::vector<Node> preL(lit[i].begin(), lit[i].begin() + j);
1265 : 55 : std::vector<Node> postL(lit[i].begin() + j + 1, lit[i].end());
1266 : 55 : Node tpre = strings::utils::mkConcat(preL, stype);
1267 : 55 : Node tpost = strings::utils::mkConcat(postL, stype);
1268 : 55 : Node slvL = nm->mkNode(Kind::STRING_LENGTH, slv);
1269 : 55 : Node tpreL = nm->mkNode(Kind::STRING_LENGTH, tpre);
1270 : 55 : Node tpostL = nm->mkNode(Kind::STRING_LENGTH, tpost);
1271 : 110 : slv = nm->mkNode(
1272 : : Kind::STRING_SUBSTR,
1273 : : slv,
1274 : : tpreL,
1275 : 110 : nm->mkNode(
1276 : 165 : Kind::SUB, slvL, nm->mkNode(Kind::ADD, tpreL, tpostL)));
1277 : : // forall x. r ++ x ++ t = s => P( x )
1278 : : // is equivalent to
1279 : : // r ++ s' ++ t = s => P( s' ) where
1280 : : // s' = substr( s, |r|, |s|-(|t|+|r|) ).
1281 : : // We apply this only if r,t,s do not contain free variables.
1282 [ + + ]: 55 : if (!expr::hasFreeVar(slv))
1283 : : {
1284 : 19 : return slv;
1285 : : }
1286 : : }
1287 : : }
1288 : : }
1289 : : }
1290 : :
1291 : 18 : return Node::null();
1292 : : }
1293 : :
1294 : 671653 : bool QuantifiersRewriter::getVarElimLit(Node body,
1295 : : Node lit,
1296 : : bool pol,
1297 : : std::vector<Node>& args,
1298 : : std::vector<Node>& vars,
1299 : : std::vector<Node>& subs) const
1300 : : {
1301 [ + + ]: 671653 : if (lit.getKind() == Kind::NOT)
1302 : : {
1303 : 17730 : lit = lit[0];
1304 : 17730 : pol = !pol;
1305 [ - + ][ - + ]: 17730 : Assert(lit.getKind() != Kind::NOT);
[ - - ]
1306 : : }
1307 : 671653 : NodeManager* nm = nodeManager();
1308 [ + - ]: 1343310 : Trace("var-elim-quant-debug")
1309 : 671653 : << "Eliminate : " << lit << ", pol = " << pol << "?" << std::endl;
1310 [ + + ]: 1559 : if (lit.getKind() == Kind::APPLY_TESTER && pol
1311 [ + + ][ + + ]: 672638 : && lit[0].getKind() == Kind::BOUND_VARIABLE
[ - - ]
1312 [ + + ][ + - ]: 673212 : && d_opts.quantifiers.dtVarExpandQuant)
[ + + ]
1313 : : {
1314 [ + - ]: 358 : Trace("var-elim-dt") << "Expand datatype variable based on : " << lit
1315 : 179 : << std::endl;
1316 : : std::vector<Node>::iterator ita =
1317 : 179 : std::find(args.begin(), args.end(), lit[0]);
1318 [ + - ]: 179 : if (ita != args.end())
1319 : : {
1320 : 179 : vars.push_back(lit[0]);
1321 : 358 : Node tester = lit.getOperator();
1322 : 179 : int index = datatypes::utils::indexOf(tester);
1323 : 179 : const DType& dt = datatypes::utils::datatypeOf(tester);
1324 : 179 : const DTypeConstructor& c = dt[index];
1325 : 358 : std::vector<Node> newChildren;
1326 : 358 : Node cons = c.getConstructor();
1327 : 358 : TypeNode tspec;
1328 : : // take into account if parametric
1329 [ + + ]: 179 : if (dt.isParametric())
1330 : : {
1331 : 2 : TypeNode ltn = lit[0].getType();
1332 : 2 : tspec = c.getInstantiatedConstructorType(ltn);
1333 : 2 : cons = c.getInstantiatedConstructor(ltn);
1334 : : }
1335 : : else
1336 : : {
1337 : 177 : tspec = cons.getType();
1338 : : }
1339 : 179 : newChildren.push_back(cons);
1340 : 179 : std::vector<Node> newVars;
1341 : 179 : BoundVarManager* bvm = nm->getBoundVarManager();
1342 [ + + ]: 483 : for (size_t j = 0, nargs = c.getNumArgs(); j < nargs; j++)
1343 : : {
1344 : 608 : TypeNode tn = tspec[j];
1345 : 608 : Node rn = nm->mkConstInt(Rational(j));
1346 : 912 : Node cacheVal = BoundVarManager::getCacheValue(body, lit, rn);
1347 : 912 : Node v = bvm->mkBoundVar<QRewDtExpandAttribute>(cacheVal, tn);
1348 : 304 : newChildren.push_back(v);
1349 : 304 : newVars.push_back(v);
1350 : : }
1351 : 179 : subs.push_back(nm->mkNode(Kind::APPLY_CONSTRUCTOR, newChildren));
1352 [ + - ]: 358 : Trace("var-elim-dt") << "...apply substitution " << subs[0] << "/"
1353 : 179 : << vars[0] << std::endl;
1354 : 179 : args.erase(ita);
1355 : 179 : args.insert(args.end(), newVars.begin(), newVars.end());
1356 : 179 : return true;
1357 : : }
1358 : : }
1359 : : // all eliminations below guarded by varElimQuant()
1360 [ + + ]: 671474 : if (!d_opts.quantifiers.varElimQuant)
1361 : : {
1362 : 18 : return false;
1363 : : }
1364 : :
1365 [ + + ]: 671456 : if (lit.getKind() == Kind::EQUAL)
1366 : : {
1367 : 360589 : if (pol || lit[0].getType().isBoolean())
1368 : : {
1369 [ + + ]: 527858 : for (unsigned i = 0; i < 2; i++)
1370 : : {
1371 : 357141 : bool tpol = pol;
1372 : 357141 : Node v_slv = lit[i];
1373 [ + + ]: 357141 : if (v_slv.getKind() == Kind::NOT)
1374 : : {
1375 : 13530 : v_slv = v_slv[0];
1376 : 13530 : tpol = !tpol;
1377 : : }
1378 : : std::vector<Node>::iterator ita =
1379 : 357141 : std::find(args.begin(), args.end(), v_slv);
1380 [ + + ]: 357141 : if (ita != args.end())
1381 : : {
1382 [ + + ]: 13313 : if (isVarElim(v_slv, lit[1 - i]))
1383 : : {
1384 : 11993 : Node slv = lit[1 - i];
1385 [ + + ]: 11993 : if (!tpol)
1386 : : {
1387 [ - + ][ - + ]: 956 : Assert(slv.getType().isBoolean());
[ - - ]
1388 : 956 : slv = slv.negate();
1389 : : }
1390 [ + - ]: 23986 : Trace("var-elim-quant")
1391 : 0 : << "Variable eliminate based on equality : " << v_slv << " -> "
1392 : 11993 : << slv << std::endl;
1393 : 11993 : vars.push_back(v_slv);
1394 : 11993 : subs.push_back(slv);
1395 : 11993 : args.erase(ita);
1396 : 11993 : return true;
1397 : : }
1398 : : }
1399 : : }
1400 : : }
1401 : : }
1402 [ + + ]: 659463 : if (lit.getKind() == Kind::BOUND_VARIABLE)
1403 : : {
1404 : 2895 : std::vector< Node >::iterator ita = std::find( args.begin(), args.end(), lit );
1405 [ + + ]: 2895 : if( ita!=args.end() ){
1406 [ + - ]: 2886 : Trace("var-elim-bool") << "Variable eliminate : " << lit << std::endl;
1407 : 2886 : vars.push_back( lit );
1408 : 2886 : subs.push_back(nodeManager()->mkConst(pol));
1409 : 2886 : args.erase( ita );
1410 : 2886 : return true;
1411 : : }
1412 : : }
1413 [ + + ][ + + ]: 656577 : if (lit.getKind() == Kind::EQUAL && pol)
[ + + ]
1414 : : {
1415 : 100251 : Node var;
1416 : 100251 : Node slv = getVarElimEq(lit, args, var);
1417 [ + + ]: 100251 : if (!slv.isNull())
1418 : : {
1419 [ - + ][ - + ]: 832 : Assert(!var.isNull());
[ - - ]
1420 : : std::vector<Node>::iterator ita =
1421 : 832 : std::find(args.begin(), args.end(), var);
1422 [ - + ][ - + ]: 832 : Assert(ita != args.end());
[ - - ]
1423 [ + - ]: 1664 : Trace("var-elim-quant")
1424 : 0 : << "Variable eliminate based on theory-specific solving : " << var
1425 : 832 : << " -> " << slv << std::endl;
1426 [ - + ][ - + ]: 832 : Assert(!expr::hasSubterm(slv, var));
[ - - ]
1427 [ - + ][ - + ]: 832 : Assert(slv.getType() == var.getType());
[ - - ]
1428 : 832 : vars.push_back(var);
1429 : 832 : subs.push_back(slv);
1430 : 832 : args.erase(ita);
1431 : 832 : return true;
1432 : : }
1433 : : }
1434 : 655745 : return false;
1435 : : }
1436 : :
1437 : 334889 : bool QuantifiersRewriter::getVarElim(Node body,
1438 : : std::vector<Node>& args,
1439 : : std::vector<Node>& vars,
1440 : : std::vector<Node>& subs,
1441 : : std::vector<Node>& lits) const
1442 : : {
1443 : 334889 : return getVarElimInternal(body, body, false, args, vars, subs, lits);
1444 : : }
1445 : :
1446 : 757835 : bool QuantifiersRewriter::getVarElimInternal(Node body,
1447 : : Node n,
1448 : : bool pol,
1449 : : std::vector<Node>& args,
1450 : : std::vector<Node>& vars,
1451 : : std::vector<Node>& subs,
1452 : : std::vector<Node>& lits) const
1453 : : {
1454 : 757835 : Kind nk = n.getKind();
1455 [ + + ]: 1026270 : while (nk == Kind::NOT)
1456 : : {
1457 : 268435 : n = n[0];
1458 : 268435 : pol = !pol;
1459 : 268435 : nk = n.getKind();
1460 : : }
1461 [ + + ][ + + ]: 757835 : if ((nk == Kind::AND && pol) || (nk == Kind::OR && !pol))
[ + + ][ + + ]
1462 : : {
1463 [ + + ]: 558930 : for (const Node& cn : n)
1464 : : {
1465 [ + + ]: 422187 : if (getVarElimInternal(body, cn, pol, args, vars, subs, lits))
1466 : : {
1467 : 8198 : return true;
1468 : : }
1469 : : }
1470 : 136743 : return false;
1471 : : }
1472 [ + + ]: 612894 : if (getVarElimLit(body, n, pol, args, vars, subs))
1473 : : {
1474 [ + + ]: 9366 : lits.emplace_back(pol ? n : n.notNode());
1475 : 9366 : return true;
1476 : : }
1477 : 603528 : return false;
1478 : : }
1479 : :
1480 : 759 : bool QuantifiersRewriter::hasVarElim(Node n,
1481 : : bool pol,
1482 : : std::vector<Node>& args) const
1483 : : {
1484 : 1518 : std::vector< Node > vars;
1485 : 1518 : std::vector< Node > subs;
1486 : 759 : std::vector<Node> lits;
1487 : 1518 : return getVarElimInternal(n, n, pol, args, vars, subs, lits);
1488 : : }
1489 : :
1490 : 325947 : bool QuantifiersRewriter::getVarElimIneq(Node body,
1491 : : std::vector<Node>& args,
1492 : : std::vector<Node>& bounds,
1493 : : std::vector<Node>& subs,
1494 : : QAttributes& qa) const
1495 : : {
1496 [ + - ]: 325947 : Trace("var-elim-quant-debug") << "getVarElimIneq " << body << std::endl;
1497 : : // For each variable v, we compute a set of implied bounds in the body
1498 : : // of the quantified formula.
1499 : : // num_bounds[x][-1] stores the entailed lower bounds for x
1500 : : // num_bounds[x][1] stores the entailed upper bounds for x
1501 : : // num_bounds[x][0] stores the entailed disequalities for x
1502 : : // These bounds are stored in a map that maps the literal for the bound to
1503 : : // its required polarity. For example, for quantified formula
1504 : : // (forall ((x Int)) (or (= x 0) (>= x a)))
1505 : : // we have:
1506 : : // num_bounds[x][0] contains { x -> { (= x 0) -> false } }
1507 : : // num_bounds[x][-1] contains { x -> { (>= x a) -> false } }
1508 : : // This method succeeds in eliminating x if its only occurrences are in
1509 : : // entailed disequalities, and one kind of bound. This is the case for the
1510 : : // above quantified formula, which can be rewritten to false. The reason
1511 : : // is that we can always chose a value for x that is arbitrarily large (resp.
1512 : : // small) to satisfy all disequalities and inequalities for x.
1513 : 651894 : std::map<Node, std::map<int, std::map<Node, bool>>> num_bounds;
1514 : : // The set of variables that we know we can not eliminate
1515 : 651894 : std::unordered_set<Node> ineligVars;
1516 : : // compute the entailed literals
1517 : 651894 : QuantPhaseReq qpr(body);
1518 : : // map to track which literals we have already processed, and hence can be
1519 : : // excluded from the free variables check in the latter half of this method.
1520 : 651894 : std::map<Node, int> processed;
1521 [ + + ]: 897739 : for (const std::pair<const Node, bool>& pr : qpr.d_phase_reqs)
1522 : : {
1523 : : // an inequality that is entailed with a given polarity
1524 : 571792 : Node lit = pr.first;
1525 : 571792 : bool pol = pr.second;
1526 [ + - ]: 1143580 : Trace("var-elim-quant-debug") << "Process inequality bounds : " << lit
1527 : 571792 : << ", pol = " << pol << "..." << std::endl;
1528 : 1143580 : bool canSolve = lit.getKind() == Kind::GEQ
1529 [ + + ][ + + ]: 901058 : || (lit.getKind() == Kind::EQUAL
1530 : 901058 : && lit[0].getType().isRealOrInt() && !pol);
1531 [ + + ]: 571792 : if (!canSolve)
1532 : : {
1533 : 449912 : continue;
1534 : : }
1535 : : // solve the inequality
1536 : 121880 : std::map<Node, Node> msum;
1537 [ - + ]: 121880 : if (!ArithMSum::getMonomialSumLit(lit, msum))
1538 : : {
1539 : : // not an inequality, cannot use
1540 : 0 : continue;
1541 : : }
1542 [ + + ]: 121880 : processed[lit] = pol ? -1 : 1;
1543 [ + + ]: 377110 : for (const std::pair<const Node, Node>& m : msum)
1544 : : {
1545 [ + + ][ + + ]: 255230 : if (!m.first.isNull() && ineligVars.find(m.first) == ineligVars.end())
[ + + ]
1546 : : {
1547 : : std::vector<Node>::iterator ita =
1548 : 203741 : std::find(args.begin(), args.end(), m.first);
1549 [ + + ]: 203741 : if (ita != args.end())
1550 : : {
1551 : : // store that this literal is upper/lower bound for itm->first
1552 : 188588 : Node veq_c;
1553 : 188588 : Node val;
1554 : : int ires =
1555 : 94294 : ArithMSum::isolate(m.first, msum, veq_c, val, lit.getKind());
1556 [ + - ][ + + ]: 94294 : if (ires != 0 && veq_c.isNull())
[ + + ]
1557 : : {
1558 [ + + ]: 93560 : if (lit.getKind() == Kind::GEQ)
1559 : : {
1560 : 58969 : bool is_upper = pol != (ires == 1);
1561 [ + - ]: 117938 : Trace("var-elim-ineq-debug")
1562 [ - - ]: 0 : << lit << " is a " << (is_upper ? "upper" : "lower")
1563 : 58969 : << " bound for " << m.first << std::endl;
1564 [ + - ]: 117938 : Trace("var-elim-ineq-debug")
1565 : 58969 : << " pol/ires = " << pol << " " << ires << std::endl;
1566 [ + + ]: 58969 : num_bounds[m.first][is_upper ? 1 : -1][lit] = pol;
1567 : : }
1568 : : else
1569 : : {
1570 [ + - ]: 69182 : Trace("var-elim-ineq-debug")
1571 : 34591 : << lit << " is a disequality for " << m.first << std::endl;
1572 : 34591 : num_bounds[m.first][0][lit] = pol;
1573 : : }
1574 : : }
1575 : : else
1576 : : {
1577 [ + - ]: 1468 : Trace("var-elim-ineq-debug")
1578 : 0 : << "...ineligible " << m.first
1579 : 0 : << " since it cannot be solved for (" << ires << ", " << veq_c
1580 : 734 : << ")." << std::endl;
1581 : 734 : num_bounds.erase(m.first);
1582 : 734 : ineligVars.insert(m.first);
1583 : : }
1584 : : }
1585 : : else
1586 : : {
1587 : : // compute variables in itm->first, these are not eligible for
1588 : : // elimination
1589 : 218894 : std::unordered_set<Node> fvs;
1590 : 109447 : expr::getFreeVariables(m.first, fvs);
1591 [ + + ]: 230303 : for (const Node& v : fvs)
1592 : : {
1593 [ + - ]: 241712 : Trace("var-elim-ineq-debug")
1594 : 0 : << "...ineligible " << v
1595 : 120856 : << " since it is contained in monomial." << std::endl;
1596 : 120856 : num_bounds.erase(v);
1597 : 120856 : ineligVars.insert(v);
1598 : : }
1599 : : }
1600 : : }
1601 : : }
1602 : : }
1603 : :
1604 : : // collect all variables that have only upper/lower bounds
1605 : 651894 : std::map<Node, bool> elig_vars;
1606 : 50511 : for (const std::pair<const Node, std::map<int, std::map<Node, bool>>>& nb :
1607 [ + + ]: 426969 : num_bounds)
1608 : : {
1609 [ + + ]: 50511 : if (nb.second.find(1) == nb.second.end())
1610 : : {
1611 [ + - ]: 60566 : Trace("var-elim-ineq-debug")
1612 : 30283 : << "Variable " << nb.first << " has only lower bounds." << std::endl;
1613 : 30283 : elig_vars[nb.first] = false;
1614 : : }
1615 [ + + ]: 20228 : else if (nb.second.find(-1) == nb.second.end())
1616 : : {
1617 [ + - ]: 18860 : Trace("var-elim-ineq-debug")
1618 : 9430 : << "Variable " << nb.first << " has only upper bounds." << std::endl;
1619 : 9430 : elig_vars[nb.first] = true;
1620 : : }
1621 : : }
1622 [ + + ]: 325947 : if (elig_vars.empty())
1623 : : {
1624 : 293688 : return false;
1625 : : }
1626 : 64518 : std::vector<Node> inactive_vars;
1627 : 64518 : std::map<Node, std::map<int, bool> > visited;
1628 : : // traverse the body, invalidate variables if they occur in places other than
1629 : : // the bounds they occur in
1630 : 64518 : std::unordered_map<TNode, std::unordered_set<int>> evisited;
1631 : 64518 : std::vector<TNode> evisit;
1632 : 64518 : std::vector<int> evisit_pol;
1633 : 32259 : TNode ecur;
1634 : : int ecur_pol;
1635 : 32259 : evisit.push_back(body);
1636 : 32259 : evisit_pol.push_back(1);
1637 [ + + ]: 32259 : if (!qa.d_ipl.isNull())
1638 : : {
1639 : : // do not eliminate variables that occur in the annotation
1640 : 4168 : evisit.push_back(qa.d_ipl);
1641 : 4168 : evisit_pol.push_back(0);
1642 : : }
1643 : 270337 : do
1644 : : {
1645 : 302596 : ecur = evisit.back();
1646 : 302596 : evisit.pop_back();
1647 : 302596 : ecur_pol = evisit_pol.back();
1648 : 302596 : evisit_pol.pop_back();
1649 : 302596 : std::unordered_set<int>& epp = evisited[ecur];
1650 [ + + ]: 302596 : if (epp.find(ecur_pol) == epp.end())
1651 : : {
1652 : 278039 : epp.insert(ecur_pol);
1653 [ + + ]: 278039 : if (elig_vars.find(ecur) != elig_vars.end())
1654 : : {
1655 : : // variable contained in a place apart from bounds, no longer eligible
1656 : : // for elimination
1657 : 37351 : elig_vars.erase(ecur);
1658 [ + - ]: 74702 : Trace("var-elim-ineq-debug") << "...found occurrence of " << ecur
1659 : 37351 : << ", mark ineligible" << std::endl;
1660 : : }
1661 : : else
1662 : : {
1663 : 240688 : bool rec = true;
1664 : 240688 : bool pol = ecur_pol >= 0;
1665 : 240688 : bool hasPol = ecur_pol != 0;
1666 [ + + ]: 240688 : if (hasPol)
1667 : : {
1668 : 126171 : std::map<Node, int>::iterator itx = processed.find(ecur);
1669 [ + + ][ + + ]: 126171 : if (itx != processed.end() && itx->second == ecur_pol)
[ + + ]
1670 : : {
1671 : : // already processed this literal as a bound
1672 : 17086 : rec = false;
1673 : : }
1674 : : }
1675 [ + + ]: 240688 : if (rec)
1676 : : {
1677 [ + + ]: 578115 : for (unsigned j = 0, size = ecur.getNumChildren(); j < size; j++)
1678 : : {
1679 : : bool newHasPol;
1680 : : bool newPol;
1681 : 354513 : QuantPhaseReq::getPolarity(ecur, j, hasPol, pol, newHasPol, newPol);
1682 : 354513 : evisit.push_back(ecur[j]);
1683 [ + + ][ + + ]: 354513 : evisit_pol.push_back(newHasPol ? (newPol ? 1 : -1) : 0);
1684 : : }
1685 : : }
1686 : : }
1687 : : }
1688 [ + + ][ + + ]: 302596 : } while (!evisit.empty() && !elig_vars.empty());
[ + + ]
1689 : :
1690 : 32259 : bool ret = false;
1691 : 32259 : NodeManager* nm = nodeManager();
1692 [ + + ]: 34621 : for (const std::pair<const Node, bool>& ev : elig_vars)
1693 : : {
1694 : 2362 : Node v = ev.first;
1695 [ + - ]: 4724 : Trace("var-elim-ineq-debug")
1696 : 2362 : << v << " is eligible for elimination." << std::endl;
1697 : : // do substitution corresponding to infinite projection, all literals
1698 : : // involving unbounded variable go to true/false
1699 : : // disequalities of eligible variables are also eliminated
1700 : 2362 : std::map<int, std::map<Node, bool>>& nbv = num_bounds[v];
1701 [ + + ]: 7086 : for (size_t i = 0; i < 2; i++)
1702 : : {
1703 [ + + ][ + + ]: 4724 : size_t nindex = i == 0 ? (elig_vars[v] ? 1 : -1) : 0;
1704 [ + + ]: 7428 : for (const std::pair<const Node, bool>& nb : nbv[nindex])
1705 : : {
1706 [ + - ]: 5408 : Trace("var-elim-ineq-debug")
1707 : 2704 : << " subs : " << nb.first << " -> " << nb.second << std::endl;
1708 : 2704 : bounds.push_back(nb.first);
1709 : 2704 : subs.push_back(nm->mkConst(nb.second));
1710 : : }
1711 : : }
1712 : : // eliminate from args
1713 : 2362 : std::vector<Node>::iterator ita = std::find(args.begin(), args.end(), v);
1714 [ - + ][ - + ]: 2362 : Assert(ita != args.end());
[ - - ]
1715 : 2362 : args.erase(ita);
1716 : 2362 : ret = true;
1717 : : }
1718 : 32259 : return ret;
1719 : : }
1720 : :
1721 : 330688 : Node QuantifiersRewriter::computeVarElimination(Node body,
1722 : : std::vector<Node>& args,
1723 : : QAttributes& qa) const
1724 : : {
1725 [ + + ][ - + ]: 330688 : if (!d_opts.quantifiers.varElimQuant && !d_opts.quantifiers.dtVarExpandQuant
1726 [ - - ]: 0 : && !d_opts.quantifiers.varIneqElimQuant)
1727 : : {
1728 : 0 : return body;
1729 : : }
1730 [ + - ]: 661376 : Trace("var-elim-quant-debug")
1731 : 330688 : << "computeVarElimination " << body << std::endl;
1732 : 661376 : std::vector<Node> vars;
1733 : 661376 : std::vector<Node> subs;
1734 : : // standard variable elimination
1735 [ + + ]: 330688 : if (d_opts.quantifiers.varElimQuant)
1736 : : {
1737 : 330418 : std::vector<Node> lits;
1738 : 330418 : getVarElim(body, args, vars, subs, lits);
1739 : : }
1740 : : // variable elimination based on one-direction inequalities
1741 [ + + ][ + + ]: 330688 : if (vars.empty() && d_opts.quantifiers.varIneqElimQuant)
[ + + ]
1742 : : {
1743 : 322544 : getVarElimIneq(body, args, vars, subs, qa);
1744 : : }
1745 : : // if we eliminated a variable, update body and reprocess
1746 [ + + ]: 330688 : if (!vars.empty())
1747 : : {
1748 [ + - ]: 19652 : Trace("var-elim-quant-debug")
1749 : 9826 : << "VE " << vars.size() << "/" << args.size() << std::endl;
1750 [ - + ][ - + ]: 9826 : Assert(vars.size() == subs.size());
[ - - ]
1751 : : // remake with eliminated nodes
1752 : 9826 : body = body.substitute(vars.begin(), vars.end(), subs.begin(), subs.end());
1753 [ + + ]: 9826 : if (!qa.d_ipl.isNull())
1754 : : {
1755 : 152 : qa.d_ipl = qa.d_ipl.substitute(
1756 : 76 : vars.begin(), vars.end(), subs.begin(), subs.end());
1757 : : }
1758 [ + - ]: 9826 : Trace("var-elim-quant") << "Return " << body << std::endl;
1759 : : }
1760 : 330688 : return body;
1761 : : }
1762 : :
1763 : 2293020 : Node QuantifiersRewriter::computePrenex(Node q,
1764 : : Node body,
1765 : : std::vector<Node>& args,
1766 : : std::vector<Node>& nargs,
1767 : : bool pol,
1768 : : bool prenexAgg) const
1769 : : {
1770 : 2293020 : NodeManager* nm = nodeManager();
1771 : 2293020 : Kind k = body.getKind();
1772 [ + + ]: 2293020 : if (k == Kind::FORALL)
1773 : : {
1774 [ - + ]: 48210 : if ((pol || prenexAgg)
1775 [ + + ][ + - ]: 104840 : && (d_opts.quantifiers.prenexQuantUser
1776 [ + + ][ + + ]: 56630 : || !QuantAttributes::hasPattern(body)))
[ + + ][ - - ]
1777 : : {
1778 : 8304 : std::vector< Node > terms;
1779 : 8304 : std::vector< Node > subs;
1780 : 4152 : BoundVarManager* bvm = nm->getBoundVarManager();
1781 [ + - ]: 4152 : std::vector<Node>& argVec = pol ? args : nargs;
1782 : : //for doing prenexing of same-signed quantifiers
1783 : : //must rename each variable that already exists
1784 [ + + ]: 11187 : for (const Node& v : body[0])
1785 : : {
1786 : 7035 : terms.push_back(v);
1787 : 14070 : TypeNode vt = v.getType();
1788 : 14070 : Node vv;
1789 [ + + ]: 7035 : if (!q.isNull())
1790 : : {
1791 : : // We cache based on the original quantified formula, the subformula
1792 : : // that we are pulling variables from (body), the variable v and an
1793 : : // index ii.
1794 : : // The argument body is required since in rare cases, two subformulas
1795 : : // may share the same variables. This is the case for define-fun
1796 : : // or inferred substitutions that contain quantified formulas.
1797 : : // The argument ii is required in case we are prenexing the same
1798 : : // subformula multiple times, e.g.
1799 : : // forall x. (forall y. P(y) or forall y. P(y)) --->
1800 : : // forall x z w. (P(z) or P(w)).
1801 : 7034 : size_t index = 0;
1802 : 64 : do
1803 : : {
1804 : 14196 : Node ii = nm->mkConstInt(index);
1805 : 35490 : Node cacheVal = nm->mkNode(Kind::SEXPR, {q, body, v, ii});
1806 : 7098 : vv = bvm->mkBoundVar<QRewPrenexAttribute>(cacheVal, vt);
1807 : 7098 : index++;
1808 [ + + ]: 7098 : } while (std::find(argVec.begin(), argVec.end(), vv) != argVec.end());
1809 : : }
1810 : : else
1811 : : {
1812 : : // not specific to a quantified formula, use normal
1813 : 1 : vv = NodeManager::mkBoundVar(vt);
1814 : : }
1815 : 7035 : subs.push_back(vv);
1816 : : }
1817 : 4152 : argVec.insert(argVec.end(), subs.begin(), subs.end());
1818 : 8304 : Node newBody = body[1];
1819 : 4152 : newBody = newBody.substitute( terms.begin(), terms.end(), subs.begin(), subs.end() );
1820 : 4152 : return newBody;
1821 : : }
1822 : : //must remove structure
1823 : : }
1824 [ + + ][ - + ]: 2240600 : else if (prenexAgg && k == Kind::ITE && body.getType().isBoolean())
[ - - ][ - + ]
[ - + ][ - - ]
1825 : : {
1826 : : Node nn = nm->mkNode(Kind::AND,
1827 : 0 : nm->mkNode(Kind::OR, body[0].notNode(), body[1]),
1828 : 0 : nm->mkNode(Kind::OR, body[0], body[2]));
1829 : 0 : return computePrenex(q, nn, args, nargs, pol, prenexAgg);
1830 : : }
1831 : 2240600 : else if (prenexAgg && k == Kind::EQUAL && body[0].getType().isBoolean())
1832 : : {
1833 : : Node nn = nm->mkNode(Kind::AND,
1834 : 0 : nm->mkNode(Kind::OR, body[0].notNode(), body[1]),
1835 : 0 : nm->mkNode(Kind::OR, body[0], body[1].notNode()));
1836 : 0 : return computePrenex(q, nn, args, nargs, pol, prenexAgg);
1837 [ + - ]: 2240600 : }else if( body.getType().isBoolean() ){
1838 [ - + ][ - + ]: 2240600 : Assert(k != Kind::EXISTS);
[ - - ]
1839 : 2240600 : bool childrenChanged = false;
1840 : 2240600 : std::vector< Node > newChildren;
1841 [ + + ]: 6546790 : for (size_t i = 0, nchild = body.getNumChildren(); i < nchild; i++)
1842 : : {
1843 : : bool newHasPol;
1844 : : bool newPol;
1845 : 4306180 : QuantPhaseReq::getPolarity( body, i, true, pol, newHasPol, newPol );
1846 [ + + ]: 4306180 : if (!newHasPol)
1847 : : {
1848 : 2311850 : newChildren.push_back( body[i] );
1849 : 2311850 : continue;
1850 : : }
1851 : 3988670 : Node n = computePrenex(q, body[i], args, nargs, newPol, prenexAgg);
1852 : 1994330 : newChildren.push_back(n);
1853 [ + + ][ + + ]: 1994330 : childrenChanged = n != body[i] || childrenChanged;
[ + - ][ - - ]
1854 : : }
1855 [ + + ]: 2240600 : if( childrenChanged ){
1856 [ + + ][ + + ]: 4313 : if (k == Kind::NOT && newChildren[0].getKind() == Kind::NOT)
[ + + ]
1857 : : {
1858 : 140 : return newChildren[0][0];
1859 : : }
1860 : 4173 : return nm->mkNode(k, newChildren);
1861 : : }
1862 : : }
1863 : 2284560 : return body;
1864 : : }
1865 : :
1866 : 132784 : Node QuantifiersRewriter::computeSplit(std::vector<Node>& args,
1867 : : Node body,
1868 : : QAttributes& qa) const
1869 : : {
1870 [ - + ][ - + ]: 132784 : Assert(body.getKind() == Kind::OR);
[ - - ]
1871 : 132784 : size_t eqc_count = 0;
1872 : 132784 : size_t eqc_active = 0;
1873 : 265568 : std::map< Node, int > var_to_eqc;
1874 : 265568 : std::map< int, std::vector< Node > > eqc_to_var;
1875 : 265568 : std::map< int, std::vector< Node > > eqc_to_lit;
1876 : :
1877 : 265568 : std::vector<Node> lits;
1878 : :
1879 [ + + ]: 910578 : for( unsigned i=0; i<body.getNumChildren(); i++ ){
1880 : : //get variables contained in the literal
1881 : 1555590 : Node n = body[i];
1882 : 1555590 : std::vector< Node > lit_args;
1883 : 777794 : computeArgVec( args, lit_args, n );
1884 [ + + ]: 777794 : if( lit_args.empty() ){
1885 : 5622 : lits.push_back( n );
1886 : : }else {
1887 : : //collect the equivalence classes this literal belongs to, and the new variables it contributes
1888 : 1544340 : std::vector< int > eqcs;
1889 : 1544340 : std::vector< Node > lit_new_args;
1890 : : //for each variable in literal
1891 [ + + ]: 2924940 : for( unsigned j=0; j<lit_args.size(); j++) {
1892 : : //see if the variable has already been found
1893 [ + + ]: 2152770 : if (var_to_eqc.find(lit_args[j])!=var_to_eqc.end()) {
1894 : 1417440 : int eqc = var_to_eqc[lit_args[j]];
1895 [ + + ]: 1417440 : if (std::find(eqcs.begin(), eqcs.end(), eqc)==eqcs.end()) {
1896 : 638701 : eqcs.push_back(eqc);
1897 : : }
1898 : : }else{
1899 : 735325 : lit_new_args.push_back(lit_args[j]);
1900 : : }
1901 : : }
1902 [ + + ]: 772172 : if (eqcs.empty()) {
1903 : 257529 : eqcs.push_back(eqc_count);
1904 : 257529 : eqc_count++;
1905 : 257529 : eqc_active++;
1906 : : }
1907 : :
1908 : 772172 : int eqcz = eqcs[0];
1909 : : //merge equivalence classes with eqcz
1910 [ + + ]: 896230 : for (unsigned j=1; j<eqcs.size(); j++) {
1911 : 124058 : int eqc = eqcs[j];
1912 : : //move all variables from equivalence class
1913 [ + + ]: 583636 : for (unsigned k=0; k<eqc_to_var[eqc].size(); k++) {
1914 : 919156 : Node v = eqc_to_var[eqc][k];
1915 : 459578 : var_to_eqc[v] = eqcz;
1916 : 459578 : eqc_to_var[eqcz].push_back(v);
1917 : : }
1918 : 124058 : eqc_to_var.erase(eqc);
1919 : : //move all literals from equivalence class
1920 [ + + ]: 519042 : for (unsigned k=0; k<eqc_to_lit[eqc].size(); k++) {
1921 : 789968 : Node l = eqc_to_lit[eqc][k];
1922 : 394984 : eqc_to_lit[eqcz].push_back(l);
1923 : : }
1924 : 124058 : eqc_to_lit.erase(eqc);
1925 : 124058 : eqc_active--;
1926 : : }
1927 : : //add variables to equivalence class
1928 [ + + ]: 1507500 : for (unsigned j=0; j<lit_new_args.size(); j++) {
1929 : 735325 : var_to_eqc[lit_new_args[j]] = eqcz;
1930 : 735325 : eqc_to_var[eqcz].push_back(lit_new_args[j]);
1931 : : }
1932 : : //add literal to equivalence class
1933 : 772172 : eqc_to_lit[eqcz].push_back(n);
1934 : : }
1935 : : }
1936 [ + + ][ + + ]: 132784 : if ( eqc_active>1 || !lits.empty() || var_to_eqc.size()!=args.size() ){
[ + + ][ + + ]
1937 : 2679 : NodeManager* nm = nodeManager();
1938 [ - + ]: 2679 : if (TraceIsOn("clause-split-debug"))
1939 : : {
1940 [ - - ]: 0 : Trace("clause-split-debug")
1941 : 0 : << "Split quantified formula with body " << body << std::endl;
1942 [ - - ]: 0 : Trace("clause-split-debug") << " Ground literals: " << std::endl;
1943 [ - - ]: 0 : for (size_t i = 0; i < lits.size(); i++)
1944 : : {
1945 [ - - ]: 0 : Trace("clause-split-debug") << " " << lits[i] << std::endl;
1946 : : }
1947 [ - - ]: 0 : Trace("clause-split-debug") << std::endl;
1948 [ - - ]: 0 : Trace("clause-split-debug") << "Equivalence classes: " << std::endl;
1949 : : }
1950 [ + + ]: 6045 : for (std::map< int, std::vector< Node > >::iterator it = eqc_to_lit.begin(); it != eqc_to_lit.end(); ++it ){
1951 : 3366 : int eqc = it->first;
1952 [ - + ]: 3366 : if (TraceIsOn("clause-split-debug"))
1953 : : {
1954 [ - - ]: 0 : Trace("clause-split-debug") << " Literals: " << std::endl;
1955 [ - - ]: 0 : for (size_t i = 0; i < it->second.size(); i++)
1956 : : {
1957 [ - - ]: 0 : Trace("clause-split-debug") << " " << it->second[i] << std::endl;
1958 : : }
1959 [ - - ]: 0 : Trace("clause-split-debug") << " Variables: " << std::endl;
1960 [ - - ]: 0 : for (size_t i = 0; i < eqc_to_var[eqc].size(); i++)
1961 : : {
1962 [ - - ]: 0 : Trace("clause-split-debug")
1963 : 0 : << " " << eqc_to_var[eqc][i] << std::endl;
1964 : : }
1965 [ - - ]: 0 : Trace("clause-split-debug") << std::endl;
1966 : : }
1967 : 3366 : std::vector<Node>& evars = eqc_to_var[eqc];
1968 : : // for the sake of proofs, we provide the variables in the order
1969 : : // they appear in the original quantified formula
1970 : 6732 : std::vector<Node> ovars;
1971 [ + + ]: 71893 : for (const Node& v : args)
1972 : : {
1973 [ + + ]: 68527 : if (std::find(evars.begin(), evars.end(), v) != evars.end())
1974 : : {
1975 : 29608 : ovars.emplace_back(v);
1976 : : }
1977 : : }
1978 : 6732 : Node bvl = nodeManager()->mkNode(Kind::BOUND_VAR_LIST, ovars);
1979 : 4863 : Node bd = it->second.size() == 1 ? it->second[0]
1980 [ + + ]: 8229 : : nm->mkNode(Kind::OR, it->second);
1981 : 10098 : Node fa = nm->mkNode(Kind::FORALL, bvl, bd);
1982 : 3366 : lits.push_back(fa);
1983 : : }
1984 [ - + ][ - + ]: 2679 : Assert(!lits.empty());
[ - - ]
1985 : 5358 : Node nf = nodeManager()->mkOr(lits);
1986 [ + - ]: 2679 : Trace("clause-split-debug") << "Made node : " << nf << std::endl;
1987 : 2679 : return nf;
1988 : : }
1989 : 130105 : return Node::null();
1990 : : }
1991 : :
1992 : 306681 : Node QuantifiersRewriter::mkForAll(const std::vector<Node>& args,
1993 : : Node body,
1994 : : QAttributes& qa) const
1995 : : {
1996 [ + + ]: 306681 : if (args.empty())
1997 : : {
1998 : 655 : return body;
1999 : : }
2000 : 306026 : NodeManager* nm = nodeManager();
2001 : 612052 : std::vector<Node> children;
2002 : 306026 : children.push_back(nm->mkNode(Kind::BOUND_VAR_LIST, args));
2003 : 306026 : children.push_back(body);
2004 [ + + ]: 306026 : if (!qa.d_ipl.isNull())
2005 : : {
2006 : 833 : children.push_back(qa.d_ipl);
2007 : : }
2008 : 306026 : return nm->mkNode(Kind::FORALL, children);
2009 : : }
2010 : :
2011 : 2 : Node QuantifiersRewriter::mkForall(const std::vector<Node>& args,
2012 : : Node body,
2013 : : bool marked) const
2014 : : {
2015 : 2 : std::vector< Node > iplc;
2016 : 4 : return mkForall( args, body, iplc, marked );
2017 : : }
2018 : :
2019 : 5 : Node QuantifiersRewriter::mkForall(const std::vector<Node>& args,
2020 : : Node body,
2021 : : std::vector<Node>& iplc,
2022 : : bool marked) const
2023 : : {
2024 [ - + ]: 5 : if (args.empty())
2025 : : {
2026 : 0 : return body;
2027 : : }
2028 : 5 : NodeManager* nm = nodeManager();
2029 : 10 : std::vector<Node> children;
2030 : 5 : children.push_back(nm->mkNode(Kind::BOUND_VAR_LIST, args));
2031 : 5 : children.push_back(body);
2032 [ + - ]: 5 : if (marked)
2033 : : {
2034 : 10 : Node avar = NodeManager::mkDummySkolem("id", nm->booleanType());
2035 : : QuantIdNumAttribute ida;
2036 : 5 : avar.setAttribute(ida, 0);
2037 : 5 : iplc.push_back(nm->mkNode(Kind::INST_ATTRIBUTE, avar));
2038 : : }
2039 [ + - ]: 5 : if (!iplc.empty())
2040 : : {
2041 : 5 : children.push_back(nm->mkNode(Kind::INST_PATTERN_LIST, iplc));
2042 : : }
2043 : 5 : return nm->mkNode(Kind::FORALL, children);
2044 : : }
2045 : :
2046 : : //computes miniscoping, also eliminates variables that do not occur free in body
2047 : 310770 : Node QuantifiersRewriter::computeMiniscoping(Node q,
2048 : : QAttributes& qa,
2049 : : bool miniscopeConj,
2050 : : bool miniscopeFv) const
2051 : : {
2052 : 310770 : NodeManager* nm = nodeManager();
2053 : 932310 : std::vector<Node> args(q[0].begin(), q[0].end());
2054 : 621540 : Node body = q[1];
2055 : 310770 : Kind k = body.getKind();
2056 [ + + ][ + + ]: 310770 : if (k == Kind::AND || k == Kind::ITE)
2057 : : {
2058 : 5374 : bool doRewrite = miniscopeConj;
2059 [ + + ]: 5374 : if (k == Kind::ITE)
2060 : : {
2061 : : // ITE miniscoping is only valid if condition contains no variables
2062 [ + + ]: 455 : if (expr::hasSubterm(body[0], args))
2063 : : {
2064 : 437 : doRewrite = false;
2065 : : }
2066 : : }
2067 : : // aggressive miniscoping implies that structural miniscoping should
2068 : : // be applied first
2069 [ + + ]: 5374 : if (doRewrite)
2070 : : {
2071 : 2162 : BoundVarManager* bvm = nm->getBoundVarManager();
2072 : : // Break apart the quantifed formula
2073 : : // forall x. P1 ^ ... ^ Pn ---> forall x. P1 ^ ... ^ forall x. Pn
2074 : 4324 : NodeBuilder t(nm, k);
2075 : 4324 : std::vector<Node> argsc;
2076 [ + + ]: 10387 : for (size_t i = 0, nchild = body.getNumChildren(); i < nchild; i++)
2077 : : {
2078 [ + + ]: 8225 : if (argsc.empty())
2079 : : {
2080 : : // If not done so, we must create fresh copy of args. This is to
2081 : : // ensure that quantified formulas do not reuse variables.
2082 [ + + ]: 15787 : for (const Node& v : q[0])
2083 : : {
2084 : 21516 : TypeNode vt = v.getType();
2085 : 32274 : Node cacheVal = BoundVarManager::getCacheValue(q, v, i);
2086 : 32274 : Node vv = bvm->mkBoundVar<QRewMiniscopeAttribute>(cacheVal, vt);
2087 : 10758 : argsc.push_back(vv);
2088 : : }
2089 : : }
2090 : 16450 : Node b = body[i];
2091 : : Node bodyc =
2092 : 16450 : b.substitute(args.begin(), args.end(), argsc.begin(), argsc.end());
2093 [ + + ]: 8225 : if (b == bodyc)
2094 : : {
2095 : : // Did not contain variables in args, thus it is ground. Since we did
2096 : : // not use them, we keep the variables argsc for the next child.
2097 : 3362 : t << b;
2098 : : }
2099 : : else
2100 : : {
2101 : : // make the miniscoped quantified formula
2102 : 9726 : Node cbvl = nm->mkNode(Kind::BOUND_VAR_LIST, argsc);
2103 : 14589 : Node qq = nm->mkNode(Kind::FORALL, cbvl, bodyc);
2104 : 4863 : t << qq;
2105 : : // We used argsc, clear so we will construct a fresh copy above.
2106 : 4863 : argsc.clear();
2107 : : }
2108 : : }
2109 : 4324 : Node retVal = t;
2110 : 2162 : return retVal;
2111 : 3212 : }
2112 : : }
2113 [ + + ]: 305396 : else if (body.getKind() == Kind::OR)
2114 : : {
2115 [ + + ]: 137791 : if (miniscopeFv)
2116 : : {
2117 : : //splitting subsumes free variable miniscoping, apply it with higher priority
2118 : 131399 : Node ret = computeSplit(args, body, qa);
2119 [ + + ]: 131399 : if (!ret.isNull())
2120 : : {
2121 : 2247 : return ret;
2122 : : }
2123 : : }
2124 : : }
2125 [ + + ]: 167605 : else if (body.getKind() == Kind::NOT)
2126 : : {
2127 [ - + ][ - + ]: 40375 : Assert(isLiteral(body[0]));
[ - - ]
2128 : : }
2129 : : //remove variables that don't occur
2130 : 306361 : std::vector< Node > activeArgs;
2131 : 306361 : computeArgVec2( args, activeArgs, body, qa.d_ipl );
2132 : 306361 : return mkForAll( activeArgs, body, qa );
2133 : : }
2134 : :
2135 : 346 : Node QuantifiersRewriter::computeAggressiveMiniscoping(std::vector<Node>& args,
2136 : : Node body) const
2137 : : {
2138 : 692 : std::map<Node, std::vector<Node> > varLits;
2139 : 692 : std::map<Node, std::vector<Node> > litVars;
2140 [ + + ]: 346 : if (body.getKind() == Kind::OR)
2141 : : {
2142 [ + - ]: 100 : Trace("ag-miniscope") << "compute aggressive miniscoping on " << body << std::endl;
2143 [ + + ]: 312 : for (size_t i = 0; i < body.getNumChildren(); i++) {
2144 : 212 : std::vector<Node> activeArgs;
2145 : 212 : computeArgVec(args, activeArgs, body[i]);
2146 [ + + ]: 476 : for (unsigned j = 0; j < activeArgs.size(); j++) {
2147 : 264 : varLits[activeArgs[j]].push_back(body[i]);
2148 : : }
2149 : 212 : std::vector<Node>& lit_body_i = litVars[body[i]];
2150 : 212 : std::vector<Node>::iterator lit_body_i_begin = lit_body_i.begin();
2151 : 212 : std::vector<Node>::const_iterator active_begin = activeArgs.begin();
2152 : 212 : std::vector<Node>::const_iterator active_end = activeArgs.end();
2153 : 212 : lit_body_i.insert(lit_body_i_begin, active_begin, active_end);
2154 : : }
2155 : : //find the variable in the least number of literals
2156 : 100 : Node bestVar;
2157 [ + + ]: 252 : for( std::map< Node, std::vector<Node> >::iterator it = varLits.begin(); it != varLits.end(); ++it ){
2158 [ + + ][ + + ]: 152 : if( bestVar.isNull() || varLits[bestVar].size()>it->second.size() ){
[ + + ]
2159 : 124 : bestVar = it->first;
2160 : : }
2161 : : }
2162 [ + - ]: 100 : Trace("ag-miniscope-debug") << "Best variable " << bestVar << " occurs in " << varLits[bestVar].size() << "/ " << body.getNumChildren() << " literals." << std::endl;
2163 [ + - ][ + + ]: 100 : if( !bestVar.isNull() && varLits[bestVar].size()<body.getNumChildren() ){
[ + + ]
2164 : : //we can miniscope
2165 [ + - ]: 26 : Trace("ag-miniscope") << "Miniscope on " << bestVar << std::endl;
2166 : : //make the bodies
2167 : 52 : std::vector<Node> qlit1;
2168 : 26 : qlit1.insert( qlit1.begin(), varLits[bestVar].begin(), varLits[bestVar].end() );
2169 : 52 : std::vector<Node> qlitt;
2170 : : //for all literals not containing bestVar
2171 [ + + ]: 90 : for( size_t i=0; i<body.getNumChildren(); i++ ){
2172 [ + + ]: 64 : if( std::find( qlit1.begin(), qlit1.end(), body[i] )==qlit1.end() ){
2173 : 38 : qlitt.push_back( body[i] );
2174 : : }
2175 : : }
2176 : : //make the variable lists
2177 : 52 : std::vector<Node> qvl1;
2178 : 52 : std::vector<Node> qvl2;
2179 : 52 : std::vector<Node> qvsh;
2180 [ + + ]: 104 : for( unsigned i=0; i<args.size(); i++ ){
2181 : 78 : bool found1 = false;
2182 : 78 : bool found2 = false;
2183 [ + + ]: 168 : for( size_t j=0; j<varLits[args[i]].size(); j++ ){
2184 [ + + ][ + + ]: 116 : if( !found1 && std::find( qlit1.begin(), qlit1.end(), varLits[args[i]][j] )!=qlit1.end() ){
[ + + ]
2185 : 52 : found1 = true;
2186 [ + + ][ + - ]: 64 : }else if( !found2 && std::find( qlitt.begin(), qlitt.end(), varLits[args[i]][j] )!=qlitt.end() ){
[ + + ]
2187 : 52 : found2 = true;
2188 : : }
2189 [ + + ][ + + ]: 116 : if( found1 && found2 ){
2190 : 26 : break;
2191 : : }
2192 : : }
2193 [ + + ]: 78 : if( found1 ){
2194 [ + + ]: 52 : if( found2 ){
2195 : 26 : qvsh.push_back( args[i] );
2196 : : }else{
2197 : 26 : qvl1.push_back( args[i] );
2198 : : }
2199 : : }else{
2200 [ - + ][ - + ]: 26 : Assert(found2);
[ - - ]
2201 : 26 : qvl2.push_back( args[i] );
2202 : : }
2203 : : }
2204 [ - + ][ - + ]: 26 : Assert(!qvl1.empty());
[ - - ]
2205 : : //check for literals that only contain shared variables
2206 : 52 : std::vector<Node> qlitsh;
2207 : 52 : std::vector<Node> qlit2;
2208 [ + + ]: 64 : for( size_t i=0; i<qlitt.size(); i++ ){
2209 : 38 : bool hasVar2 = false;
2210 [ + + ]: 52 : for( size_t j=0; j<litVars[qlitt[i]].size(); j++ ){
2211 [ + + ]: 40 : if( std::find( qvl2.begin(), qvl2.end(), litVars[qlitt[i]][j] )!=qvl2.end() ){
2212 : 26 : hasVar2 = true;
2213 : 26 : break;
2214 : : }
2215 : : }
2216 [ + + ]: 38 : if( hasVar2 ){
2217 : 26 : qlit2.push_back( qlitt[i] );
2218 : : }else{
2219 : 12 : qlitsh.push_back( qlitt[i] );
2220 : : }
2221 : : }
2222 : 26 : varLits.clear();
2223 : 26 : litVars.clear();
2224 [ + - ]: 26 : Trace("ag-miniscope-debug") << "Split into literals : " << qlit1.size() << " / " << qlit2.size() << " / " << qlitsh.size();
2225 [ + - ]: 26 : Trace("ag-miniscope-debug") << ", variables : " << qvl1.size() << " / " << qvl2.size() << " / " << qvsh.size() << std::endl;
2226 : : Node n1 =
2227 [ + - ]: 52 : qlit1.size() == 1 ? qlit1[0] : nodeManager()->mkNode(Kind::OR, qlit1);
2228 : 26 : n1 = computeAggressiveMiniscoping( qvl1, n1 );
2229 : 26 : qlitsh.push_back( n1 );
2230 [ + + ]: 26 : if( !qlit2.empty() ){
2231 : 16 : Node n2 = qlit2.size() == 1 ? qlit2[0]
2232 [ + + ]: 30 : : nodeManager()->mkNode(Kind::OR, qlit2);
2233 : 14 : n2 = computeAggressiveMiniscoping( qvl2, n2 );
2234 : 14 : qlitsh.push_back( n2 );
2235 : : }
2236 : 52 : Node n = nodeManager()->mkNode(Kind::OR, qlitsh);
2237 [ + - ]: 26 : if( !qvsh.empty() ){
2238 : 26 : Node bvl = nodeManager()->mkNode(Kind::BOUND_VAR_LIST, qvsh);
2239 : 26 : n = nodeManager()->mkNode(Kind::FORALL, bvl, n);
2240 : : }
2241 [ + - ]: 26 : Trace("ag-miniscope") << "Return " << n << " for " << body << std::endl;
2242 : 26 : return n;
2243 : : }
2244 : : }
2245 : 320 : QAttributes qa;
2246 : 320 : return mkForAll( args, body, qa );
2247 : : }
2248 : :
2249 : 3 : bool QuantifiersRewriter::isStandard(const Node& q, const Options& opts)
2250 : : {
2251 : 6 : QAttributes qa;
2252 : 3 : QuantAttributes::computeQuantAttributes(q, qa);
2253 : 6 : return isStandard(qa, opts);
2254 : : }
2255 : :
2256 : 2851680 : bool QuantifiersRewriter::isStandard(QAttributes& qa, const Options& opts)
2257 : : {
2258 : 2851680 : bool is_strict_trigger =
2259 : 2851680 : qa.d_hasPattern
2260 [ + + ][ + + ]: 2851680 : && opts.quantifiers.userPatternsQuant == options::UserPatMode::STRICT;
2261 [ + + ][ + - ]: 2851680 : return qa.isStandard() && !is_strict_trigger;
2262 : : }
2263 : :
2264 : 3865 : Node QuantifiersRewriter::computeRewriteBody(const Node& n,
2265 : : TConvProofGenerator* pg) const
2266 : : {
2267 [ - + ][ - + ]: 3865 : Assert(n.getKind() == Kind::FORALL);
[ - - ]
2268 : 7730 : QAttributes qa;
2269 : 3865 : QuantAttributes::computeQuantAttributes(n, qa);
2270 : 11595 : std::vector<Node> args(n[0].begin(), n[0].end());
2271 : 7730 : Node body = computeProcessTerms(n, args, n[1], qa, pg);
2272 [ + + ]: 3865 : if (body != n[1])
2273 : : {
2274 : 3018 : std::vector<Node> children;
2275 : 1509 : children.push_back(n[0]);
2276 : 1509 : children.push_back(body);
2277 [ + + ]: 1509 : if (n.getNumChildren() == 3)
2278 : : {
2279 : 18 : children.push_back(n[2]);
2280 : : }
2281 : 1509 : return d_nm->mkNode(Kind::FORALL, children);
2282 : : }
2283 : 2356 : return n;
2284 : : }
2285 : :
2286 : 2851680 : bool QuantifiersRewriter::doOperation(Node q,
2287 : : RewriteStep computeOption,
2288 : : QAttributes& qa) const
2289 : : {
2290 : 2851680 : bool is_strict_trigger =
2291 : 2851680 : qa.d_hasPattern
2292 [ + + ][ + + ]: 2851680 : && d_opts.quantifiers.userPatternsQuant == options::UserPatMode::STRICT;
2293 : 2851680 : bool is_std = isStandard(qa, d_opts);
2294 [ + + ]: 2851680 : if (computeOption == COMPUTE_ELIM_SYMBOLS)
2295 : : {
2296 : 399275 : return true;
2297 : : }
2298 [ + + ]: 2452400 : else if (computeOption == COMPUTE_MINISCOPING
2299 [ + + ]: 2088410 : || computeOption == COMPUTE_AGGRESSIVE_MINISCOPING)
2300 : : {
2301 : : // in the rare case the body is ground, we always eliminate unless it
2302 : : // is truly a non-standard quantified formula (e.g. one for QE).
2303 [ + + ]: 722563 : if (!expr::hasBoundVar(q[1]))
2304 : : {
2305 : : // This returns true if q is a non-standard quantified formula. Note that
2306 : : // is_std is additionally true if user-pat is strict and q has user
2307 : : // patterns.
2308 : 3198 : return qa.isStandard();
2309 : : }
2310 [ + + ]: 719365 : if (!is_std)
2311 : : {
2312 : 30560 : return false;
2313 : : }
2314 : : // do not miniscope if we have user patterns unless option is set
2315 [ + - ][ + + ]: 688805 : if (!d_opts.quantifiers.miniscopeQuantUser && qa.d_hasPattern)
2316 : : {
2317 : 73916 : return false;
2318 : : }
2319 [ + + ]: 614889 : if (computeOption == COMPUTE_AGGRESSIVE_MINISCOPING)
2320 : : {
2321 : 305007 : return d_opts.quantifiers.miniscopeQuant
2322 : 305007 : == options::MiniscopeQuantMode::AGG;
2323 : : }
2324 : 309882 : return true;
2325 : : }
2326 [ + + ]: 1729840 : else if (computeOption == COMPUTE_EXT_REWRITE)
2327 : : {
2328 : 336806 : return d_opts.quantifiers.extRewriteQuant;
2329 : : }
2330 [ + + ]: 1393030 : else if (computeOption == COMPUTE_PROCESS_TERMS)
2331 : : {
2332 : 358553 : return true;
2333 : : }
2334 [ + + ]: 1034480 : else if (computeOption == COMPUTE_COND_SPLIT)
2335 : : {
2336 : 337462 : return (d_opts.quantifiers.iteDtTesterSplitQuant
2337 [ + - ]: 332133 : || d_opts.quantifiers.condVarSplitQuant
2338 : : != options::CondVarSplitQuantMode::OFF)
2339 [ + + ][ + + ]: 669595 : && !is_strict_trigger;
2340 : : }
2341 [ + + ]: 697016 : else if (computeOption == COMPUTE_PRENEX)
2342 : : {
2343 : : // do not prenex to pull variables into those with user patterns
2344 [ + + ][ + + ]: 349728 : if (!d_opts.quantifiers.prenexQuantUser && qa.d_hasPattern)
2345 : : {
2346 : 36959 : return false;
2347 : : }
2348 [ + + ]: 312769 : if (qa.d_hasPool)
2349 : : {
2350 : 328 : return false;
2351 : : }
2352 : 312441 : return d_opts.quantifiers.prenexQuant != options::PrenexQuantMode::NONE
2353 [ + + ]: 310688 : && d_opts.quantifiers.miniscopeQuant
2354 : : != options::MiniscopeQuantMode::AGG
2355 [ + + ][ + + ]: 623129 : && is_std;
2356 : : }
2357 [ + - ]: 347288 : else if (computeOption == COMPUTE_VAR_ELIMINATION)
2358 : : {
2359 : 347288 : return (d_opts.quantifiers.varElimQuant
2360 [ + - ]: 270 : || d_opts.quantifiers.dtVarExpandQuant)
2361 [ + + ][ + + ]: 347558 : && is_std && !is_strict_trigger;
[ + - ]
2362 : : }
2363 : : else
2364 : : {
2365 : 0 : return false;
2366 : : }
2367 : : }
2368 : :
2369 : : //general method for computing various rewrites
2370 : 2031070 : Node QuantifiersRewriter::computeOperation(Node f,
2371 : : RewriteStep computeOption,
2372 : : QAttributes& qa) const
2373 : : {
2374 [ + - ]: 2031070 : Trace("quantifiers-rewrite-debug") << "Compute operation " << computeOption << " on " << f << " " << qa.d_qid_num << std::endl;
2375 [ + + ]: 2031070 : if (computeOption == COMPUTE_MINISCOPING)
2376 : : {
2377 [ + + ]: 310434 : if (d_opts.quantifiers.prenexQuant == options::PrenexQuantMode::NORMAL)
2378 : : {
2379 [ + + ]: 35 : if( !qa.d_qid_num.isNull() ){
2380 : : //already processed this, return self
2381 : 33 : return f;
2382 : : }
2383 : : }
2384 : 310401 : bool miniscopeConj = doMiniscopeConj(d_opts);
2385 : 310401 : bool miniscopeFv = doMiniscopeFv(d_opts);
2386 : : //return directly
2387 : 310401 : return computeMiniscoping(f, qa, miniscopeConj, miniscopeFv);
2388 : : }
2389 : 5161900 : std::vector<Node> args(f[0].begin(), f[0].end());
2390 : 3441270 : Node n = f[1];
2391 [ + + ]: 1720630 : if (computeOption == COMPUTE_ELIM_SYMBOLS)
2392 : : {
2393 : : // relies on external utility
2394 : 399275 : n = booleans::TheoryBoolRewriter::computeNnfNorm(nodeManager(), n);
2395 : : }
2396 [ + + ]: 1321360 : else if (computeOption == COMPUTE_AGGRESSIVE_MINISCOPING)
2397 : : {
2398 : 306 : return computeAggressiveMiniscoping( args, n );
2399 : : }
2400 [ + + ]: 1321050 : else if (computeOption == COMPUTE_EXT_REWRITE)
2401 : : {
2402 : 28 : return computeExtendedRewrite(f, qa);
2403 : : }
2404 [ + + ]: 1321020 : else if (computeOption == COMPUTE_PROCESS_TERMS)
2405 : : {
2406 : 358553 : n = computeProcessTerms(f, args, n, qa);
2407 : : }
2408 [ + + ]: 962472 : else if (computeOption == COMPUTE_COND_SPLIT)
2409 : : {
2410 : 337418 : n = computeCondSplit(n, args, qa);
2411 : : }
2412 [ + + ]: 625054 : else if (computeOption == COMPUTE_PRENEX)
2413 : : {
2414 [ + + ]: 294366 : if (d_opts.quantifiers.prenexQuant == options::PrenexQuantMode::NORMAL)
2415 : : {
2416 : : //will rewrite at preprocess time
2417 : 32 : return f;
2418 : : }
2419 : : else
2420 : : {
2421 : 588668 : std::vector<Node> argsSet, nargsSet;
2422 : 294334 : n = computePrenex(f, n, argsSet, nargsSet, true, false);
2423 [ - + ][ - + ]: 294334 : Assert(nargsSet.empty());
[ - - ]
2424 : 294334 : args.insert(args.end(), argsSet.begin(), argsSet.end());
2425 : : }
2426 : : }
2427 [ + - ]: 330688 : else if (computeOption == COMPUTE_VAR_ELIMINATION)
2428 : : {
2429 : 330688 : n = computeVarElimination( n, args, qa );
2430 : : }
2431 [ + - ]: 1720270 : Trace("quantifiers-rewrite-debug") << "Compute Operation: return " << n << ", " << args.size() << std::endl;
2432 : 1720270 : if( f[1]==n && args.size()==f[0].getNumChildren() ){
2433 : 1663240 : return f;
2434 : : }else{
2435 [ + + ]: 57028 : if( args.empty() ){
2436 : 2676 : return n;
2437 : : }else{
2438 : 108704 : std::vector< Node > children;
2439 : 54352 : children.push_back(nodeManager()->mkNode(Kind::BOUND_VAR_LIST, args));
2440 : 54352 : children.push_back( n );
2441 [ + + ][ + + ]: 54352 : if( !qa.d_ipl.isNull() && args.size()==f[0].getNumChildren() ){
[ + + ][ + + ]
[ - - ]
2442 : 5736 : children.push_back( qa.d_ipl );
2443 : : }
2444 : 54352 : return nodeManager()->mkNode(Kind::FORALL, children);
2445 : : }
2446 : : }
2447 : : }
2448 : 647800 : bool QuantifiersRewriter::doMiniscopeConj(const Options& opts)
2449 : : {
2450 : 647800 : options::MiniscopeQuantMode mqm = opts.quantifiers.miniscopeQuant;
2451 : : return mqm == options::MiniscopeQuantMode::CONJ_AND_FV
2452 [ + - ]: 28769 : || mqm == options::MiniscopeQuantMode::CONJ
2453 [ + + ][ + + ]: 676569 : || mqm == options::MiniscopeQuantMode::AGG;
2454 : : }
2455 : :
2456 : 310401 : bool QuantifiersRewriter::doMiniscopeFv(const Options& opts)
2457 : : {
2458 : 310401 : options::MiniscopeQuantMode mqm = opts.quantifiers.miniscopeQuant;
2459 : : return mqm == options::MiniscopeQuantMode::CONJ_AND_FV
2460 [ + + ]: 12373 : || mqm == options::MiniscopeQuantMode::FV
2461 [ + + ][ + + ]: 322774 : || mqm == options::MiniscopeQuantMode::AGG;
2462 : : }
2463 : :
2464 : 0 : bool QuantifiersRewriter::isPrenexNormalForm( Node n ) {
2465 [ - - ]: 0 : if (n.getKind() == Kind::FORALL)
2466 : : {
2467 : 0 : return n[1].getKind() != Kind::FORALL && isPrenexNormalForm(n[1]);
2468 : : }
2469 [ - - ]: 0 : else if (n.getKind() == Kind::NOT)
2470 : : {
2471 : 0 : return n[0].getKind() != Kind::NOT && isPrenexNormalForm(n[0]);
2472 : : }
2473 : : else
2474 : : {
2475 : 0 : return !expr::hasClosure(n);
2476 : : }
2477 : : }
2478 : :
2479 : : } // namespace quantifiers
2480 : : } // namespace theory
2481 : : } // namespace cvc5::internal
|
