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-2024 by the authors listed in the file AUTHORS
8 : : * in the top-level source directory and their institutional affiliations.
9 : : * All rights reserved. See the file COPYING in the top-level source
10 : : * directory for licensing information.
11 : : * ****************************************************************************
12 : : *
13 : : * Implementation of 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 "theory/arith/arith_msum.h"
27 : : #include "theory/booleans/theory_bool_rewriter.h"
28 : : #include "theory/datatypes/theory_datatypes_utils.h"
29 : : #include "theory/quantifiers/bv_inverter.h"
30 : : #include "theory/quantifiers/ematching/trigger.h"
31 : : #include "theory/quantifiers/extended_rewrite.h"
32 : : #include "theory/quantifiers/quantifiers_attributes.h"
33 : : #include "theory/quantifiers/skolemize.h"
34 : : #include "theory/quantifiers/term_database.h"
35 : : #include "theory/quantifiers/term_util.h"
36 : : #include "theory/rewriter.h"
37 : : #include "theory/strings/theory_strings_utils.h"
38 : : #include "theory/uf/theory_uf_rewriter.h"
39 : : #include "util/rational.h"
40 : :
41 : : using namespace std;
42 : : using namespace cvc5::internal::kind;
43 : : using namespace cvc5::context;
44 : :
45 : : namespace cvc5::internal {
46 : : namespace theory {
47 : : namespace quantifiers {
48 : :
49 : : /**
50 : : * Attributes used for constructing bound variables in a canonical way. These
51 : : * are attributes that map to bound variable, introduced for the following
52 : : * purposes:
53 : : * - QRewPrenexAttribute: cached on (v, body) where we are prenexing bound
54 : : * variable v in a nested quantified formula within the given body.
55 : : * - QRewMiniscopeAttribute: cached on (v, q, i) where q is being miniscoped
56 : : * for F_i in its body (and F_1 ... F_n), and v is one of the bound variables
57 : : * that q binds.
58 : : * - QRewDtExpandAttribute: cached on (F, lit, a) where lit is the tested
59 : : * literal used for expanding a quantified datatype variable in quantified
60 : : * formula with body F, and a is the rational corresponding to the argument
61 : : * position of the variable, e.g. lit is ((_ is C) x) and x is
62 : : * replaced by (C y1 ... yn), where the argument position of yi is i.
63 : : */
64 : : struct QRewPrenexAttributeId
65 : : {
66 : : };
67 : : using QRewPrenexAttribute = expr::Attribute<QRewPrenexAttributeId, Node>;
68 : : struct QRewMiniscopeAttributeId
69 : : {
70 : : };
71 : : using QRewMiniscopeAttribute = expr::Attribute<QRewMiniscopeAttributeId, Node>;
72 : : struct QRewDtExpandAttributeId
73 : : {
74 : : };
75 : : using QRewDtExpandAttribute = expr::Attribute<QRewDtExpandAttributeId, Node>;
76 : :
77 : 0 : std::ostream& operator<<(std::ostream& out, RewriteStep s)
78 : : {
79 [ - - ][ - - ]: 0 : switch (s)
[ - - ][ - - ]
[ - ]
80 : : {
81 : 0 : case COMPUTE_ELIM_SYMBOLS: out << "COMPUTE_ELIM_SYMBOLS"; break;
82 : 0 : case COMPUTE_MINISCOPING: out << "COMPUTE_MINISCOPING"; break;
83 : 0 : case COMPUTE_AGGRESSIVE_MINISCOPING:
84 : 0 : out << "COMPUTE_AGGRESSIVE_MINISCOPING";
85 : 0 : break;
86 : 0 : case COMPUTE_PROCESS_TERMS: out << "COMPUTE_PROCESS_TERMS"; break;
87 : 0 : case COMPUTE_PRENEX: out << "COMPUTE_PRENEX"; break;
88 : 0 : case COMPUTE_VAR_ELIMINATION: out << "COMPUTE_VAR_ELIMINATION"; break;
89 : 0 : case COMPUTE_COND_SPLIT: out << "COMPUTE_COND_SPLIT"; break;
90 : 0 : case COMPUTE_EXT_REWRITE: out << "COMPUTE_EXT_REWRITE"; break;
91 : 0 : default: out << "UnknownRewriteStep"; break;
92 : : }
93 : 0 : return out;
94 : : }
95 : :
96 : 131308 : QuantifiersRewriter::QuantifiersRewriter(NodeManager* nm,
97 : : Rewriter* r,
98 : 131308 : const Options& opts)
99 : 131308 : : TheoryRewriter(nm), d_rewriter(r), d_opts(opts)
100 : : {
101 : 131308 : registerProofRewriteRule(ProofRewriteRule::EXISTS_ELIM,
102 : : TheoryRewriteCtx::PRE_DSL);
103 : 131308 : registerProofRewriteRule(ProofRewriteRule::QUANT_UNUSED_VARS,
104 : : TheoryRewriteCtx::PRE_DSL);
105 : 131308 : registerProofRewriteRule(ProofRewriteRule::QUANT_MERGE_PRENEX,
106 : : TheoryRewriteCtx::PRE_DSL);
107 : 131308 : registerProofRewriteRule(ProofRewriteRule::QUANT_MINISCOPE,
108 : : TheoryRewriteCtx::PRE_DSL);
109 : 131308 : registerProofRewriteRule(ProofRewriteRule::MACRO_QUANT_PARTITION_CONNECTED_FV,
110 : : TheoryRewriteCtx::PRE_DSL);
111 : 131308 : registerProofRewriteRule(ProofRewriteRule::MACRO_QUANT_VAR_ELIM_EQ,
112 : : TheoryRewriteCtx::PRE_DSL);
113 : 131308 : registerProofRewriteRule(ProofRewriteRule::MACRO_QUANT_VAR_ELIM_INEQ,
114 : : TheoryRewriteCtx::PRE_DSL);
115 : 131308 : }
116 : :
117 : 7625 : Node QuantifiersRewriter::rewriteViaRule(ProofRewriteRule id, const Node& n)
118 : : {
119 [ + + ][ + + ]: 7625 : switch (id)
[ + + ][ + - ]
120 : : {
121 : 2020 : case ProofRewriteRule::EXISTS_ELIM:
122 : : {
123 [ + + ]: 2020 : if (n.getKind() != Kind::EXISTS)
124 : : {
125 : 1029 : return Node::null();
126 : : }
127 : 991 : std::vector<Node> fchildren;
128 : 991 : fchildren.push_back(n[0]);
129 : 991 : fchildren.push_back(n[1].notNode());
130 [ + + ]: 991 : if (n.getNumChildren() == 3)
131 : : {
132 : 5 : fchildren.push_back(n[2]);
133 : : }
134 : 991 : return d_nm->mkNode(Kind::NOT, d_nm->mkNode(Kind::FORALL, fchildren));
135 : : }
136 : 1307 : case ProofRewriteRule::QUANT_UNUSED_VARS:
137 : : {
138 [ - + ]: 1307 : if (!n.isClosure())
139 : : {
140 : 443 : return Node::null();
141 : : }
142 : 2614 : std::vector<Node> vars(n[0].begin(), n[0].end());
143 : 1307 : std::vector<Node> activeVars;
144 : 1307 : computeArgVec(vars, activeVars, n[1]);
145 [ + + ]: 1307 : if (activeVars.size() < vars.size())
146 : : {
147 [ + + ]: 443 : if (activeVars.empty())
148 : : {
149 : 320 : return n[1];
150 : : }
151 : 123 : return d_nm->mkNode(
152 : 123 : n.getKind(), d_nm->mkNode(Kind::BOUND_VAR_LIST, activeVars), n[1]);
153 : : }
154 : : }
155 : 864 : break;
156 : 1114 : case ProofRewriteRule::QUANT_MERGE_PRENEX:
157 : : {
158 [ - + ]: 1114 : if (!n.isClosure())
159 : : {
160 : 322 : return Node::null();
161 : : }
162 : : // Don't check standard here, which can't be replicated in a proof checker
163 : : // without modelling the patterns.
164 : 1114 : Node q = mergePrenex(n, false);
165 [ + + ]: 1114 : if (q != n)
166 : : {
167 : 322 : return q;
168 : : }
169 : : }
170 : 792 : break;
171 : 961 : case ProofRewriteRule::QUANT_MINISCOPE:
172 : : {
173 [ + - ][ + + ]: 961 : if (n.getKind() != Kind::FORALL || n[1].getKind() != Kind::AND)
[ + - ][ + + ]
[ - - ]
174 : : {
175 : 682 : return Node::null();
176 : : }
177 : : // note that qa is not needed; moreover external proofs should be agnostic
178 : : // to it
179 : 558 : QAttributes qa;
180 : 279 : QuantAttributes::computeQuantAttributes(n, qa);
181 : 558 : Node nret = computeMiniscoping(n, qa, true, false);
182 [ - + ][ - + ]: 279 : Assert(nret != n);
[ - - ]
183 : 279 : return nret;
184 : : }
185 : : break;
186 : 819 : case ProofRewriteRule::MACRO_QUANT_PARTITION_CONNECTED_FV:
187 : : {
188 [ + - ][ + + ]: 819 : if (n.getKind() != Kind::FORALL || n[1].getKind() != Kind::OR)
[ + - ][ + + ]
[ - - ]
189 : : {
190 : 698 : return Node::null();
191 : : }
192 : : // note that qa is not needed; moreover external proofs should be agnostic
193 : : // to it
194 : 607 : QAttributes qa;
195 : 607 : QuantAttributes::computeQuantAttributes(n, qa);
196 : 1214 : std::vector<Node> vars(n[0].begin(), n[0].end());
197 : 607 : Node body = n[1];
198 : 607 : Node nret = computeSplit(vars, body, qa);
199 [ + + ]: 607 : if (!nret.isNull())
200 : : {
201 : : // only do this rule if it is a proper split; otherwise it will be
202 : : // subsumed by QUANT_UNUSED_VARS.
203 [ + + ]: 278 : if (nret.getKind() == Kind::OR)
204 : : {
205 : 274 : return nret;
206 : : }
207 : : }
208 : : }
209 : 333 : break;
210 : 72 : case ProofRewriteRule::QUANT_MINISCOPE_FV:
211 : : {
212 [ + - ][ - + ]: 72 : if (n.getKind() != Kind::FORALL || n[1].getKind() != Kind::OR)
[ + - ][ - + ]
[ - - ]
213 : : {
214 : 0 : return Node::null();
215 : : }
216 : 72 : size_t nvars = n[0].getNumChildren();
217 : 144 : std::vector<Node> disj;
218 : 144 : std::unordered_set<Node> varsUsed;
219 : 72 : size_t varIndex = 0;
220 [ + + ]: 314 : for (const Node& d : n[1])
221 : : {
222 : : // Note that we may apply to a nested quantified formula, in which
223 : : // case some variables in fvs may not be bound by this quantified
224 : : // formula.
225 : 484 : std::unordered_set<Node> fvs;
226 : 242 : expr::getFreeVariables(d, fvs);
227 : 242 : size_t prevVarIndex = varIndex;
228 : 424 : while (varIndex < nvars && fvs.find(n[0][varIndex]) != fvs.end())
229 : : {
230 : 182 : varIndex++;
231 : : }
232 : 484 : std::vector<Node> dvs(n[0].begin() + prevVarIndex,
233 : 968 : n[0].begin() + varIndex);
234 [ + + ]: 242 : if (dvs.empty())
235 : : {
236 : 153 : disj.emplace_back(d);
237 : : }
238 : : else
239 : : {
240 : 89 : Node bvl = d_nm->mkNode(Kind::BOUND_VAR_LIST, dvs);
241 : 89 : disj.emplace_back(d_nm->mkNode(Kind::FORALL, bvl, d));
242 : : }
243 : : }
244 : : // must consume all variables
245 [ - + ]: 72 : if (varIndex != nvars)
246 : : {
247 : 0 : return Node::null();
248 : : }
249 : 144 : Node ret = d_nm->mkOr(disj);
250 : : // go back and ensure all variables are bound
251 : 144 : std::unordered_set<Node> fvs;
252 : 72 : expr::getFreeVariables(ret, fvs);
253 [ + + ]: 254 : for (const Node& v : n[0])
254 : : {
255 [ - + ]: 182 : if (fvs.find(v) != fvs.end())
256 : : {
257 : 0 : return Node::null();
258 : : }
259 : : }
260 : 72 : return ret;
261 : : }
262 : : break;
263 : 1332 : case ProofRewriteRule::MACRO_QUANT_VAR_ELIM_EQ:
264 : : case ProofRewriteRule::QUANT_VAR_ELIM_EQ:
265 : : case ProofRewriteRule::MACRO_QUANT_VAR_ELIM_INEQ:
266 : : {
267 [ + - ][ + + ]: 1332 : if (n.getKind() != Kind::FORALL || n.getNumChildren() != 2)
[ + + ]
268 : : {
269 : 909 : return Node::null();
270 : : }
271 : 2576 : std::vector<Node> args(n[0].begin(), n[0].end());
272 : 1288 : std::vector<Node> vars;
273 : 1288 : std::vector<Node> subs;
274 : 1288 : Node body = n[1];
275 [ + + ]: 1288 : if (id == ProofRewriteRule::MACRO_QUANT_VAR_ELIM_EQ)
276 : : {
277 : 774 : std::vector<Node> lits;
278 : 774 : getVarElim(body, args, vars, subs, lits);
279 : : }
280 [ + + ]: 514 : else if (id == ProofRewriteRule::QUANT_VAR_ELIM_EQ)
281 : : {
282 [ - + ]: 124 : if (args.size() != 1)
283 : : {
284 : 0 : return Node::null();
285 : : }
286 : 124 : std::vector<Node> lits;
287 [ + - ]: 124 : if (body.getKind() == Kind::OR)
288 : : {
289 : 124 : lits.insert(lits.end(), body.begin(), body.end());
290 : : }
291 : : else
292 : : {
293 : 0 : lits.push_back(body);
294 : : }
295 : 124 : if (lits[0].getKind() != Kind::NOT
296 [ + - ][ - + ]: 248 : || lits[0][0].getKind() != Kind::EQUAL)
[ + - ][ - + ]
[ - - ]
297 : : {
298 : 0 : return Node::null();
299 : : }
300 : 124 : Node eq = lits[0][0];
301 : 124 : if (eq[0] != args[0] || expr::hasSubterm(eq[1], eq[0]))
302 : : {
303 : 0 : return Node::null();
304 : : }
305 : 124 : vars.push_back(eq[0]);
306 : 124 : subs.push_back(eq[1]);
307 : 124 : args.clear();
308 : 124 : std::vector<Node> remLits(lits.begin() + 1, lits.end());
309 : 124 : body = d_nm->mkOr(remLits);
310 : : }
311 : : else
312 : : {
313 : : // assume empty attribute
314 : 390 : QAttributes qa;
315 : 390 : getVarElimIneq(n[1], args, vars, subs, qa);
316 : : }
317 : : // if we eliminated a variable, update body and reprocess
318 [ + + ]: 1288 : if (!vars.empty())
319 : : {
320 [ - + ][ - + ]: 821 : Assert(vars.size() == subs.size());
[ - - ]
321 : 1642 : std::vector<Node> qc(n.begin(), n.end());
322 : 821 : qc[1] =
323 : 1642 : body.substitute(vars.begin(), vars.end(), subs.begin(), subs.end());
324 [ + + ]: 821 : if (args.empty())
325 : : {
326 : 500 : return qc[1];
327 : : }
328 : 321 : qc[0] = d_nm->mkNode(Kind::BOUND_VAR_LIST, args);
329 : 321 : return d_nm->mkNode(Kind::FORALL, qc);
330 : : }
331 : : }
332 : 467 : break;
333 : 0 : default: break;
334 : : }
335 : 2456 : return Node::null();
336 : : }
337 : :
338 : 39055 : bool QuantifiersRewriter::isLiteral( Node n ){
339 [ - - ][ + + ]: 39055 : switch( n.getKind() ){
340 : 0 : case Kind::NOT:
341 : 0 : return n[0].getKind() != Kind::NOT && isLiteral(n[0]);
342 : : break;
343 : 0 : case Kind::OR:
344 : : case Kind::AND:
345 : : case Kind::IMPLIES:
346 : : case Kind::XOR:
347 : 0 : case Kind::ITE: return false; break;
348 : 18537 : case Kind::EQUAL:
349 : : // for boolean terms
350 : 18537 : return !n[0].getType().isBoolean();
351 : : break;
352 : 20518 : default: break;
353 : : }
354 : 20518 : return true;
355 : : }
356 : :
357 : 26759400 : void QuantifiersRewriter::computeArgs(const std::vector<Node>& args,
358 : : std::map<Node, bool>& activeMap,
359 : : Node n,
360 : : std::map<Node, bool>& visited)
361 : : {
362 [ + + ]: 26759400 : if( visited.find( n )==visited.end() ){
363 : 18032200 : visited[n] = true;
364 [ + + ]: 18032200 : if (n.getKind() == Kind::BOUND_VARIABLE)
365 : : {
366 [ + + ]: 3825970 : if( std::find( args.begin(), args.end(), n )!=args.end() ){
367 : 3155390 : activeMap[ n ] = true;
368 : : }
369 : : }
370 : : else
371 : : {
372 [ + + ]: 14206200 : if (n.hasOperator())
373 : : {
374 : 8472310 : computeArgs(args, activeMap, n.getOperator(), visited);
375 : : }
376 [ + + ]: 31136200 : for( int i=0; i<(int)n.getNumChildren(); i++ ){
377 : 16930000 : computeArgs( args, activeMap, n[i], visited );
378 : : }
379 : : }
380 : : }
381 : 26759400 : }
382 : :
383 : 760804 : void QuantifiersRewriter::computeArgVec(const std::vector<Node>& args,
384 : : std::vector<Node>& activeArgs,
385 : : Node n)
386 : : {
387 [ - + ][ - + ]: 760804 : Assert(activeArgs.empty());
[ - - ]
388 : 1521610 : std::map< Node, bool > activeMap;
389 : 1521610 : std::map< Node, bool > visited;
390 : 760804 : computeArgs( args, activeMap, n, visited );
391 [ + + ]: 760804 : if( !activeMap.empty() ){
392 [ + + ]: 73868200 : for( unsigned i=0; i<args.size(); i++ ){
393 [ + + ]: 73111900 : if( activeMap.find( args[i] )!=activeMap.end() ){
394 : 2130860 : activeArgs.push_back( args[i] );
395 : : }
396 : : }
397 : : }
398 : 760804 : }
399 : :
400 : 298464 : void QuantifiersRewriter::computeArgVec2(const std::vector<Node>& args,
401 : : std::vector<Node>& activeArgs,
402 : : Node n,
403 : : Node ipl)
404 : : {
405 [ - + ][ - + ]: 298464 : Assert(activeArgs.empty());
[ - - ]
406 : 596928 : std::map< Node, bool > activeMap;
407 : 596928 : std::map< Node, bool > visited;
408 : 298464 : computeArgs( args, activeMap, n, visited );
409 : : // Collect variables in inst pattern list only if we cannot eliminate
410 : : // quantifier, or if we have an add-to-pool annotation.
411 : 298464 : bool varComputePatList = !activeMap.empty();
412 [ + + ]: 299612 : for (const Node& ip : ipl)
413 : : {
414 : 1148 : Kind k = ip.getKind();
415 [ + - ][ - + ]: 1148 : if (k == Kind::INST_ADD_TO_POOL || k == Kind::SKOLEM_ADD_TO_POOL)
416 : : {
417 : 0 : varComputePatList = true;
418 : 0 : break;
419 : : }
420 : : }
421 [ + + ]: 298464 : if (varComputePatList)
422 : : {
423 : 297841 : computeArgs( args, activeMap, ipl, visited );
424 : : }
425 [ + + ]: 298464 : if (!activeMap.empty())
426 : : {
427 [ + + ]: 1323530 : for (const Node& a : args)
428 : : {
429 [ + + ]: 1025690 : if (activeMap.find(a) != activeMap.end())
430 : : {
431 : 1024530 : activeArgs.push_back(a);
432 : : }
433 : : }
434 : : }
435 : 298464 : }
436 : :
437 : 741682 : RewriteResponse QuantifiersRewriter::preRewrite(TNode q)
438 : : {
439 : 741682 : Kind k = q.getKind();
440 [ + + ][ + + ]: 741682 : if (k == Kind::FORALL || k == Kind::EXISTS)
441 : : {
442 : : // Do prenex merging now, since this may impact trigger selection.
443 : : // In particular consider:
444 : : // (forall ((x Int)) (forall ((y Int)) (! (P x) :pattern ((f x)))))
445 : : // If we wait until post-rewrite, we would rewrite the inner quantified
446 : : // formula, dropping the pattern, so the entire formula becomes:
447 : : // (forall ((x Int)) (P x))
448 : : // Instead, we merge to:
449 : : // (forall ((x Int) (y Int)) (! (P x) :pattern ((f x))))
450 : : // eagerly here, where after we would drop y to obtain:
451 : : // (forall ((x Int)) (! (P x) :pattern ((f x))))
452 : : // See issue #10303.
453 : 477528 : Node qm = mergePrenex(q, true);
454 [ + + ]: 477528 : if (q != qm)
455 : : {
456 : 3648 : return RewriteResponse(REWRITE_AGAIN_FULL, qm);
457 : : }
458 : : }
459 : 738034 : return RewriteResponse(REWRITE_DONE, q);
460 : : }
461 : :
462 : 661672 : RewriteResponse QuantifiersRewriter::postRewrite(TNode in)
463 : : {
464 [ + - ]: 661672 : Trace("quantifiers-rewrite-debug") << "post-rewriting " << in << std::endl;
465 : 661672 : RewriteStatus status = REWRITE_DONE;
466 : 1323340 : Node ret = in;
467 : 661672 : RewriteStep rew_op = COMPUTE_LAST;
468 : : // get the body
469 [ + + ]: 661672 : if (in.getKind() == Kind::EXISTS)
470 : : {
471 : 8885 : std::vector<Node> children;
472 : 8885 : children.push_back(in[0]);
473 : 8885 : children.push_back(in[1].notNode());
474 [ + + ]: 8885 : if (in.getNumChildren() == 3)
475 : : {
476 : 75 : children.push_back(in[2]);
477 : : }
478 : 8885 : ret = nodeManager()->mkNode(Kind::FORALL, children);
479 : 8885 : ret = ret.negate();
480 : 8885 : status = REWRITE_AGAIN_FULL;
481 : : }
482 [ + + ]: 652787 : else if (in.getKind() == Kind::FORALL)
483 : : {
484 : : // do prenex merging
485 : 388633 : ret = mergePrenex(in, true);
486 [ + + ]: 388633 : if (ret != in)
487 : : {
488 : 48 : status = REWRITE_AGAIN_FULL;
489 : : }
490 [ + + ][ + + ]: 388585 : else if (in[1].isConst() && in.getNumChildren() == 2)
[ + - ][ + + ]
[ - - ]
491 : : {
492 : 1994 : return RewriteResponse( status, in[1] );
493 : : }
494 : : else
495 : : {
496 : : //compute attributes
497 : 773182 : QAttributes qa;
498 : 386591 : QuantAttributes::computeQuantAttributes( in, qa );
499 [ + + ]: 3090300 : for (unsigned i = 0; i < COMPUTE_LAST; ++i)
500 : : {
501 : 2763420 : RewriteStep op = static_cast<RewriteStep>(i);
502 [ + + ]: 2763420 : if( doOperation( in, op, qa ) ){
503 : 1972040 : ret = computeOperation( in, op, qa );
504 [ + + ]: 1972040 : if( ret!=in ){
505 : 59711 : rew_op = op;
506 : 59711 : status = REWRITE_AGAIN_FULL;
507 : 59711 : break;
508 : : }
509 : : }
510 : : }
511 : : }
512 : : }
513 : : //print if changed
514 [ + + ]: 659678 : if( in!=ret ){
515 [ + - ]: 68644 : Trace("quantifiers-rewrite") << "*** rewrite (op=" << rew_op << ") " << in << std::endl;
516 [ + - ]: 68644 : Trace("quantifiers-rewrite") << " to " << std::endl;
517 [ + - ]: 68644 : Trace("quantifiers-rewrite") << ret << std::endl;
518 : : }
519 : 659678 : return RewriteResponse( status, ret );
520 : : }
521 : :
522 : 867275 : Node QuantifiersRewriter::mergePrenex(const Node& q, bool checkStd)
523 : : {
524 [ + + ][ - + ]: 867275 : Assert(q.getKind() == Kind::FORALL || q.getKind() == Kind::EXISTS);
[ - + ][ - - ]
525 : 867275 : Kind k = q.getKind();
526 : 1734550 : std::vector<Node> boundVars;
527 : 1734550 : Node body = q;
528 : 867275 : bool combineQuantifiers = false;
529 : 867275 : bool continueCombine = false;
530 [ + + ]: 881122 : do
531 : : {
532 [ + + ]: 4106140 : for (const Node& v : body[0])
533 : : {
534 [ + + ]: 3225020 : if (std::find(boundVars.begin(), boundVars.end(), v) == boundVars.end())
535 : : {
536 : 3225000 : boundVars.push_back(v);
537 : : }
538 : : else
539 : : {
540 : : // if duplicate variable due to shadowing, we must rewrite
541 : 21 : combineQuantifiers = true;
542 : : }
543 : : }
544 : 881122 : continueCombine = false;
545 [ + + ][ + + ]: 881122 : if (body.getNumChildren() == 2 && body[1].getKind() == k)
[ + + ][ + + ]
[ - - ]
546 : : {
547 : 13847 : bool process = true;
548 [ + + ]: 13847 : if (checkStd)
549 : : {
550 : : // Should never combine a quantified formula with a pool or
551 : : // non-standard quantified formula here.
552 : : // Note that we technically should check
553 : : // doOperation(body[1], COMPUTE_PRENEX, qa) here, although this
554 : : // is too restrictive, as sometimes nested patterns should just be
555 : : // applied to the top level, for example:
556 : : // (forall ((x Int)) (forall ((y Int)) (! P :pattern ((f x y)))))
557 : : // should be a pattern for the top-level quantifier here.
558 : 13153 : QAttributes qa;
559 : 13153 : QuantAttributes::computeQuantAttributes(body[1], qa);
560 : 13153 : process = qa.isStandard();
561 : : }
562 [ + - ]: 13847 : if (process)
563 : : {
564 : 13847 : body = body[1];
565 : 13847 : continueCombine = true;
566 : 13847 : combineQuantifiers = true;
567 : : }
568 : : }
569 : : } while (continueCombine);
570 [ + + ]: 867275 : if (combineQuantifiers)
571 : : {
572 : 4018 : NodeManager* nm = nodeManager();
573 : 8036 : std::vector<Node> children;
574 : 4018 : children.push_back(nm->mkNode(Kind::BOUND_VAR_LIST, boundVars));
575 : 4018 : children.push_back(body[1]);
576 [ + + ]: 4018 : if (body.getNumChildren() == 3)
577 : : {
578 : 158 : children.push_back(body[2]);
579 : : }
580 : 4018 : return nm->mkNode(k, children);
581 : : }
582 : 863257 : return q;
583 : : }
584 : :
585 : 0 : void QuantifiersRewriter::computeDtTesterIteSplit(
586 : : Node n,
587 : : std::map<Node, Node>& pcons,
588 : : std::map<Node, std::map<int, Node>>& ncons,
589 : : std::vector<Node>& conj) const
590 : : {
591 : 0 : if (n.getKind() == Kind::ITE && n[0].getKind() == Kind::APPLY_TESTER
592 : 0 : && n[1].getType().isBoolean())
593 : : {
594 [ - - ]: 0 : Trace("quantifiers-rewrite-ite-debug") << "Split tester condition : " << n << std::endl;
595 : 0 : Node x = n[0][0];
596 : 0 : std::map< Node, Node >::iterator itp = pcons.find( x );
597 [ - - ]: 0 : if( itp!=pcons.end() ){
598 [ - - ]: 0 : Trace("quantifiers-rewrite-ite-debug") << "...condition already set " << itp->second << std::endl;
599 [ - - ]: 0 : computeDtTesterIteSplit( n[ itp->second==n[0] ? 1 : 2 ], pcons, ncons, conj );
600 : : }else{
601 : 0 : Node tester = n[0].getOperator();
602 : 0 : int index = datatypes::utils::indexOf(tester);
603 : 0 : std::map< int, Node >::iterator itn = ncons[x].find( index );
604 [ - - ]: 0 : if( itn!=ncons[x].end() ){
605 [ - - ]: 0 : Trace("quantifiers-rewrite-ite-debug") << "...condition negated " << itn->second << std::endl;
606 : 0 : computeDtTesterIteSplit( n[ 2 ], pcons, ncons, conj );
607 : : }else{
608 [ - - ]: 0 : for( unsigned i=0; i<2; i++ ){
609 [ - - ]: 0 : if( i==0 ){
610 : 0 : pcons[x] = n[0];
611 : : }else{
612 : 0 : pcons.erase( x );
613 : 0 : ncons[x][index] = n[0].negate();
614 : : }
615 : 0 : computeDtTesterIteSplit( n[i+1], pcons, ncons, conj );
616 : : }
617 : 0 : ncons[x].erase( index );
618 : : }
619 : : }
620 : : }
621 : : else
622 : : {
623 : 0 : NodeManager* nm = nodeManager();
624 [ - - ]: 0 : Trace("quantifiers-rewrite-ite-debug") << "Return value : " << n << std::endl;
625 : 0 : std::vector< Node > children;
626 : 0 : children.push_back( n );
627 : 0 : std::vector< Node > vars;
628 : : //add all positive testers
629 [ - - ]: 0 : for( std::map< Node, Node >::iterator it = pcons.begin(); it != pcons.end(); ++it ){
630 : 0 : children.push_back( it->second.negate() );
631 : 0 : vars.push_back( it->first );
632 : : }
633 : : //add all negative testers
634 [ - - ]: 0 : for( std::map< Node, std::map< int, Node > >::iterator it = ncons.begin(); it != ncons.end(); ++it ){
635 : 0 : Node x = it->first;
636 : : //only if we haven't settled on a positive tester
637 [ - - ]: 0 : if( std::find( vars.begin(), vars.end(), x )==vars.end() ){
638 : : //check if we have exhausted all options but one
639 : 0 : const DType& dt = x.getType().getDType();
640 : 0 : std::vector< Node > nchildren;
641 : 0 : int pos_cons = -1;
642 [ - - ]: 0 : for( int i=0; i<(int)dt.getNumConstructors(); i++ ){
643 : 0 : std::map< int, Node >::iterator itt = it->second.find( i );
644 [ - - ]: 0 : if( itt==it->second.end() ){
645 [ - - ]: 0 : pos_cons = pos_cons==-1 ? i : -2;
646 : : }else{
647 : 0 : nchildren.push_back( itt->second.negate() );
648 : : }
649 : : }
650 [ - - ]: 0 : if( pos_cons>=0 ){
651 : 0 : Node tester = dt[pos_cons].getTester();
652 : 0 : children.push_back(
653 : 0 : nm->mkNode(Kind::APPLY_TESTER, tester, x).negate());
654 : : }else{
655 : 0 : children.insert( children.end(), nchildren.begin(), nchildren.end() );
656 : : }
657 : : }
658 : : }
659 : : //make condition/output pair
660 : 0 : Node c = children.size() == 1 ? children[0]
661 [ - - ]: 0 : : nodeManager()->mkNode(Kind::OR, children);
662 : 0 : conj.push_back( c );
663 : : }
664 : 0 : }
665 : :
666 : 347619 : Node QuantifiersRewriter::computeProcessTerms(const Node& q,
667 : : const std::vector<Node>& args,
668 : : Node body,
669 : : QAttributes& qa) const
670 : : {
671 : 347619 : options::IteLiftQuantMode iteLiftMode = options::IteLiftQuantMode::NONE;
672 [ + + ]: 347619 : if (qa.isStandard())
673 : : {
674 : 333073 : iteLiftMode = d_opts.quantifiers.iteLiftQuant;
675 : : }
676 : 695238 : std::vector<Node> new_conds;
677 : 695238 : std::map<Node, Node> cache;
678 : 347619 : Node n = computeProcessTerms2(q, args, body, cache, new_conds, iteLiftMode);
679 [ - + ]: 347619 : if (!new_conds.empty())
680 : : {
681 : 0 : new_conds.push_back(n);
682 : 0 : n = nodeManager()->mkNode(Kind::OR, new_conds);
683 : : }
684 : 695238 : return n;
685 : : }
686 : :
687 : 10776000 : Node QuantifiersRewriter::computeProcessTerms2(
688 : : const Node& q,
689 : : const std::vector<Node>& args,
690 : : Node body,
691 : : std::map<Node, Node>& cache,
692 : : std::vector<Node>& new_conds,
693 : : options::IteLiftQuantMode iteLiftMode) const
694 : : {
695 : 10776000 : NodeManager* nm = nodeManager();
696 [ + - ]: 21552000 : Trace("quantifiers-rewrite-term-debug2")
697 : 10776000 : << "computeProcessTerms " << body << std::endl;
698 : 10776000 : std::map< Node, Node >::iterator iti = cache.find( body );
699 [ + + ]: 10776000 : if( iti!=cache.end() ){
700 : 3335430 : return iti->second;
701 : : }
702 [ + + ]: 7440580 : if (body.isClosure())
703 : : {
704 : : // Ensure no shadowing. If this term is a closure quantifying a variable
705 : : // in args, then we introduce fresh variable(s) and replace this closure
706 : : // to be over the fresh variables instead.
707 : 87880 : std::vector<Node> oldVars;
708 : 87880 : std::vector<Node> newVars;
709 [ + + ]: 212527 : for (size_t i = 0, nvars = body[0].getNumChildren(); i < nvars; i++)
710 : : {
711 : 249294 : const Node& v = body[0][i];
712 [ + + ]: 124647 : if (std::find(args.begin(), args.end(), v) != args.end())
713 : : {
714 [ + - ]: 164 : Trace("quantifiers-rewrite-unshadow")
715 : 82 : << "Found shadowed variable " << v << " in " << q << std::endl;
716 : 82 : oldVars.push_back(v);
717 : 164 : Node nv = ElimShadowNodeConverter::getElimShadowVar(q, body, i);
718 : 82 : newVars.push_back(nv);
719 : : }
720 : : }
721 [ + + ]: 87880 : if (!oldVars.empty())
722 : : {
723 [ - + ][ - + ]: 82 : Assert(oldVars.size() == newVars.size());
[ - - ]
724 : : Node sbody = body.substitute(
725 : 164 : oldVars.begin(), oldVars.end(), newVars.begin(), newVars.end());
726 : 82 : cache[body] = sbody;
727 : 82 : return sbody;
728 : : }
729 : : }
730 : 7440500 : bool changed = false;
731 : 14881000 : std::vector<Node> children;
732 [ + + ]: 17868900 : for (const Node& bc : body)
733 : : {
734 : : // do the recursive call on children
735 : 10428400 : Node nn = computeProcessTerms2(q, args, bc, cache, new_conds, iteLiftMode);
736 : 10428400 : children.push_back(nn);
737 [ + + ][ + + ]: 10428400 : changed = changed || nn != bc;
738 : : }
739 : :
740 : : // make return value
741 : 14881000 : Node ret;
742 [ + + ]: 7440500 : if (changed)
743 : : {
744 [ + + ]: 31334 : if (body.getMetaKind() == kind::metakind::PARAMETERIZED)
745 : : {
746 : 942 : children.insert(children.begin(), body.getOperator());
747 : : }
748 : 31334 : ret = nm->mkNode(body.getKind(), children);
749 : : }
750 : : else
751 : : {
752 : 7409160 : ret = body;
753 : : }
754 : :
755 [ + - ]: 14881000 : Trace("quantifiers-rewrite-term-debug2")
756 : 7440500 : << "Returning " << ret << " for " << body << std::endl;
757 : : // do context-independent rewriting
758 : 7440500 : if (ret.getKind() == Kind::EQUAL
759 [ + + ][ + + ]: 7440500 : && iteLiftMode != options::IteLiftQuantMode::NONE)
[ + + ]
760 : : {
761 [ + + ]: 3462840 : for (size_t i = 0; i < 2; i++)
762 : : {
763 [ + + ]: 2309110 : if (ret[i].getKind() == Kind::ITE)
764 : : {
765 [ + + ]: 73549 : Node no = i == 0 ? ret[1] : ret[0];
766 [ + + ]: 73549 : if (no.getKind() != Kind::ITE)
767 : : {
768 : 67291 : bool doRewrite = (iteLiftMode == options::IteLiftQuantMode::ALL);
769 : 67291 : std::vector<Node> childrenIte;
770 : 67291 : childrenIte.push_back(ret[i][0]);
771 [ + + ]: 201873 : for (size_t j = 1; j <= 2; j++)
772 : : {
773 : : // check if it rewrites to a constant
774 : 403746 : Node nn = nm->mkNode(Kind::EQUAL, no, ret[i][j]);
775 : 134582 : childrenIte.push_back(nn);
776 : : // check if it will rewrite to a constant
777 : 134582 : if (no == ret[i][j] || (no.isConst() && ret[i][j].isConst()))
778 : : {
779 : 1479 : doRewrite = true;
780 : : }
781 : : }
782 [ + + ]: 67291 : if (doRewrite)
783 : : {
784 : 1018 : ret = nm->mkNode(Kind::ITE, childrenIte);
785 : 1018 : break;
786 : : }
787 : : }
788 : : }
789 : : }
790 : : }
791 [ + + ][ + + ]: 6285750 : else if (ret.getKind() == Kind::SELECT && ret[0].getKind() == Kind::STORE)
[ + + ][ + + ]
[ - - ]
792 : : {
793 : 376 : Node st = ret[0];
794 : 376 : Node index = ret[1];
795 : 376 : std::vector<Node> iconds;
796 : 376 : std::vector<Node> elements;
797 [ + + ]: 784 : while (st.getKind() == Kind::STORE)
798 : : {
799 : 596 : iconds.push_back(index.eqNode(st[1]));
800 : 596 : elements.push_back(st[2]);
801 : 596 : st = st[0];
802 : : }
803 : 188 : ret = nm->mkNode(Kind::SELECT, st, index);
804 : : // conditions
805 [ + + ]: 784 : for (int i = (iconds.size() - 1); i >= 0; i--)
806 : : {
807 : 596 : ret = nm->mkNode(Kind::ITE, iconds[i], elements[i], ret);
808 : : }
809 : : }
810 [ + + ][ + + ]: 6285560 : else if (ret.getKind() == Kind::HO_APPLY && !ret.getType().isFunction())
[ + + ][ + + ]
[ - - ]
811 : : {
812 : : // fully applied functions are converted to APPLY_UF here.
813 : 40528 : Node fullApp = uf::TheoryUfRewriter::getApplyUfForHoApply(ret);
814 : : // it may not be possible to convert e.g. if the head is not a variable
815 [ + - ]: 20264 : if (!fullApp.isNull())
816 : : {
817 : 20264 : ret = fullApp;
818 : : }
819 : : }
820 : 7440500 : cache[body] = ret;
821 : 7440500 : return ret;
822 : : }
823 : :
824 : 28 : Node QuantifiersRewriter::computeExtendedRewrite(TNode q,
825 : : const QAttributes& qa) const
826 : : {
827 : : // do not apply to recursive functions
828 [ + + ]: 28 : if (qa.isFunDef())
829 : : {
830 : 8 : return q;
831 : : }
832 : 40 : Node body = q[1];
833 : : // apply extended rewriter
834 : 40 : Node bodyr = d_rewriter->extendedRewrite(body);
835 [ + + ]: 20 : if (body != bodyr)
836 : : {
837 : 12 : std::vector<Node> children;
838 : 6 : children.push_back(q[0]);
839 : 6 : children.push_back(bodyr);
840 [ - + ]: 6 : if (q.getNumChildren() == 3)
841 : : {
842 : 0 : children.push_back(q[2]);
843 : : }
844 : 6 : return nodeManager()->mkNode(Kind::FORALL, children);
845 : : }
846 : 14 : return q;
847 : : }
848 : :
849 : 327277 : Node QuantifiersRewriter::computeCondSplit(Node body,
850 : : const std::vector<Node>& args,
851 : : QAttributes& qa) const
852 : : {
853 : 327277 : NodeManager* nm = nodeManager();
854 : 327277 : Kind bk = body.getKind();
855 [ + + ]: 696 : if (d_opts.quantifiers.iteDtTesterSplitQuant && bk == Kind::ITE
856 [ + + ][ - + ]: 327973 : && body[0].getKind() == Kind::APPLY_TESTER)
[ + + ][ - + ]
[ - - ]
857 : : {
858 [ - - ]: 0 : Trace("quantifiers-rewrite-ite-debug") << "DTT split : " << body << std::endl;
859 : 0 : std::map< Node, Node > pcons;
860 : 0 : std::map< Node, std::map< int, Node > > ncons;
861 : 0 : std::vector< Node > conj;
862 : 0 : computeDtTesterIteSplit( body, pcons, ncons, conj );
863 : 0 : Assert(!conj.empty());
864 [ - - ]: 0 : if( conj.size()>1 ){
865 [ - - ]: 0 : Trace("quantifiers-rewrite-ite") << "*** Split ITE (datatype tester) " << body << " into : " << std::endl;
866 [ - - ]: 0 : for( unsigned i=0; i<conj.size(); i++ ){
867 [ - - ]: 0 : Trace("quantifiers-rewrite-ite") << " " << conj[i] << std::endl;
868 : : }
869 : 0 : return nm->mkNode(Kind::AND, conj);
870 : : }
871 : : }
872 [ - + ]: 327277 : if (d_opts.quantifiers.condVarSplitQuant
873 : : == options::CondVarSplitQuantMode::OFF)
874 : : {
875 : 0 : return body;
876 : : }
877 [ + - ]: 654554 : Trace("cond-var-split-debug")
878 : 327277 : << "Conditional var elim split " << body << "?" << std::endl;
879 : : // we only do this splitting if miniscoping is enabled, as this is
880 : : // required to eliminate variables in conjuncts below. We also never
881 : : // miniscope non-standard quantifiers, so this is also guarded here.
882 [ + + ][ + + ]: 327277 : if (!doMiniscopeConj(d_opts) || !qa.isStandard())
[ + + ]
883 : : {
884 : 23848 : return body;
885 : : }
886 : :
887 : 303429 : bool aggCondSplit = (d_opts.quantifiers.condVarSplitQuant
888 : : == options::CondVarSplitQuantMode::AGG);
889 : 303429 : if (bk == Kind::ITE
890 : 303429 : || (bk == Kind::EQUAL && body[0].getType().isBoolean() && aggCondSplit))
891 : : {
892 [ - + ][ - + ]: 344 : Assert(!qa.isFunDef());
[ - - ]
893 : 344 : bool do_split = false;
894 : 344 : unsigned index_max = bk == Kind::ITE ? 0 : 1;
895 : 344 : std::vector<Node> tmpArgs = args;
896 [ + + ]: 614 : for (unsigned index = 0; index <= index_max; index++)
897 : : {
898 [ + + ][ - - ]: 344 : if (hasVarElim(body[index], true, tmpArgs)
899 [ + + ][ - + ]: 344 : || hasVarElim(body[index], false, tmpArgs))
[ + + ][ + - ]
[ - - ]
900 : : {
901 : 74 : do_split = true;
902 : 74 : break;
903 : : }
904 : : }
905 [ + + ]: 344 : if (do_split)
906 : : {
907 : 148 : Node pos;
908 : 74 : Node neg;
909 [ + - ]: 74 : if (bk == Kind::ITE)
910 : : {
911 : 74 : pos = nm->mkNode(Kind::OR, body[0].negate(), body[1]);
912 : 74 : neg = nm->mkNode(Kind::OR, body[0], body[2]);
913 : : }
914 : : else
915 : : {
916 : 0 : pos = nm->mkNode(Kind::OR, body[0].negate(), body[1]);
917 : 0 : neg = nm->mkNode(Kind::OR, body[0], body[1].negate());
918 : : }
919 [ + - ]: 148 : Trace("cond-var-split-debug") << "*** Split (conditional variable eq) "
920 : 74 : << body << " into : " << std::endl;
921 [ + - ]: 74 : Trace("cond-var-split-debug") << " " << pos << std::endl;
922 [ + - ]: 74 : Trace("cond-var-split-debug") << " " << neg << std::endl;
923 : 74 : return nm->mkNode(Kind::AND, pos, neg);
924 : : }
925 : : }
926 : :
927 [ + + ]: 303355 : if (bk == Kind::OR)
928 : : {
929 : 127805 : unsigned size = body.getNumChildren();
930 : 127805 : bool do_split = false;
931 : 127805 : unsigned split_index = 0;
932 [ + + ]: 499963 : for (unsigned i = 0; i < size; i++)
933 : : {
934 : : // check if this child is a (conditional) variable elimination
935 : 372519 : Node b = body[i];
936 [ + + ]: 372519 : if (b.getKind() == Kind::AND)
937 : : {
938 : 41366 : std::vector<Node> vars;
939 : 41366 : std::vector<Node> subs;
940 : 41366 : std::vector<Node> tmpArgs = args;
941 [ + + ]: 76608 : for (unsigned j = 0, bsize = b.getNumChildren(); j < bsize; j++)
942 : : {
943 [ + + ]: 56286 : if (getVarElimLit(body, b[j], false, tmpArgs, vars, subs))
944 : : {
945 [ + - ]: 9302 : Trace("cond-var-split-debug") << "Variable elimination in child #"
946 : 4651 : << j << " under " << i << std::endl;
947 : : // Figure out if we should split
948 : : // Currently we split if the aggressive option is set, or
949 : : // if the top-level OR is binary.
950 [ + - ][ + + ]: 4651 : if (aggCondSplit || size == 2)
951 : : {
952 : 361 : do_split = true;
953 : : }
954 : : // other splitting criteria go here
955 : :
956 [ + + ]: 4651 : if (do_split)
957 : : {
958 : 361 : split_index = i;
959 : 361 : break;
960 : : }
961 : 4290 : vars.clear();
962 : 4290 : subs.clear();
963 : 4290 : tmpArgs = args;
964 : : }
965 : : }
966 : : }
967 [ + + ]: 372519 : if (do_split)
968 : : {
969 : 361 : break;
970 : : }
971 : : }
972 [ + + ]: 127805 : if (do_split)
973 : : {
974 : 722 : std::vector<Node> children;
975 [ + + ]: 1083 : for (TNode bc : body)
976 : : {
977 : 722 : children.push_back(bc);
978 : : }
979 : 722 : std::vector<Node> split_children;
980 [ + + ]: 1454 : for (TNode bci : body[split_index])
981 : : {
982 : 1093 : children[split_index] = bci;
983 : 1093 : split_children.push_back(nm->mkNode(Kind::OR, children));
984 : : }
985 : : // split the AND child, for example:
986 : : // ( x!=a ^ P(x) ) V Q(x) ---> ( x!=a V Q(x) ) ^ ( P(x) V Q(x) )
987 : 361 : return nm->mkNode(Kind::AND, split_children);
988 : : }
989 : : }
990 : :
991 : 302994 : return body;
992 : : }
993 : :
994 : 12392 : bool QuantifiersRewriter::isVarElim(Node v, Node s)
995 : : {
996 [ - + ][ - + ]: 12392 : Assert(v.getKind() == Kind::BOUND_VARIABLE);
[ - - ]
997 : 12392 : return !expr::hasSubterm(s, v) && s.getType() == v.getType();
998 : : }
999 : :
1000 : 95225 : Node QuantifiersRewriter::getVarElimEq(Node lit,
1001 : : const std::vector<Node>& args,
1002 : : Node& var) const
1003 : : {
1004 [ - + ][ - + ]: 95225 : Assert(lit.getKind() == Kind::EQUAL);
[ - - ]
1005 : 95225 : Node slv;
1006 : 190450 : TypeNode tt = lit[0].getType();
1007 [ + + ]: 95225 : if (tt.isRealOrInt())
1008 : : {
1009 : 47654 : slv = getVarElimEqReal(lit, args, var);
1010 : : }
1011 [ + + ]: 47571 : else if (tt.isBitVector())
1012 : : {
1013 : 1331 : slv = getVarElimEqBv(lit, args, var);
1014 : : }
1015 [ + + ]: 46240 : else if (tt.isStringLike())
1016 : : {
1017 : 206 : slv = getVarElimEqString(lit, args, var);
1018 : : }
1019 : 190450 : return slv;
1020 : : }
1021 : :
1022 : 47654 : Node QuantifiersRewriter::getVarElimEqReal(Node lit,
1023 : : const std::vector<Node>& args,
1024 : : Node& var) const
1025 : : {
1026 : : // for arithmetic, solve the equality
1027 : 95308 : std::map<Node, Node> msum;
1028 [ - + ]: 47654 : if (!ArithMSum::getMonomialSumLit(lit, msum))
1029 : : {
1030 : 0 : return Node::null();
1031 : : }
1032 : 47654 : std::vector<Node>::const_iterator ita;
1033 [ + + ]: 143633 : for (std::map<Node, Node>::iterator itm = msum.begin(); itm != msum.end();
1034 : 95979 : ++itm)
1035 : : {
1036 [ + + ]: 96658 : if (itm->first.isNull())
1037 : : {
1038 : 9345 : continue;
1039 : : }
1040 : 87313 : ita = std::find(args.begin(), args.end(), itm->first);
1041 [ + + ]: 87313 : if (ita != args.end())
1042 : : {
1043 : 1551 : Node veq_c;
1044 : 1551 : Node val;
1045 : 1551 : int ires = ArithMSum::isolate(itm->first, msum, veq_c, val, Kind::EQUAL);
1046 : 1551 : if (ires != 0 && veq_c.isNull() && isVarElim(itm->first, val))
1047 : : {
1048 : 679 : var = itm->first;
1049 : 679 : return val;
1050 : : }
1051 : : }
1052 : : }
1053 : 46975 : return Node::null();
1054 : : }
1055 : :
1056 : 1331 : Node QuantifiersRewriter::getVarElimEqBv(Node lit,
1057 : : const std::vector<Node>& args,
1058 : : Node& var) const
1059 : : {
1060 [ - + ]: 1331 : if (TraceIsOn("quant-velim-bv"))
1061 : : {
1062 [ - - ]: 0 : Trace("quant-velim-bv") << "Bv-Elim : " << lit << " varList = { ";
1063 [ - - ]: 0 : for (const Node& v : args)
1064 : : {
1065 [ - - ]: 0 : Trace("quant-velim-bv") << v << " ";
1066 : : }
1067 [ - - ]: 0 : Trace("quant-velim-bv") << "} ?" << std::endl;
1068 : : }
1069 [ - + ][ - + ]: 1331 : Assert(lit.getKind() == Kind::EQUAL);
[ - - ]
1070 : : // TODO (#1494) : linearize the literal using utility
1071 : :
1072 : : // compute a subset active_args of the bound variables args that occur in lit
1073 : 2662 : std::vector<Node> active_args;
1074 : 1331 : computeArgVec(args, active_args, lit);
1075 : :
1076 : 2662 : BvInverter binv(d_opts);
1077 [ + + ]: 2763 : for (const Node& cvar : active_args)
1078 : : {
1079 : : // solve for the variable on this path using the inverter
1080 : 1551 : std::vector<unsigned> path;
1081 : 3102 : Node slit = binv.getPathToPv(lit, cvar, path);
1082 [ + + ]: 1551 : if (!slit.isNull())
1083 : : {
1084 : 1878 : Node slv = binv.solveBvLit(cvar, lit, path, nullptr);
1085 [ + - ]: 939 : Trace("quant-velim-bv") << "...solution : " << slv << std::endl;
1086 [ + + ]: 939 : if (!slv.isNull())
1087 : : {
1088 : 369 : var = cvar;
1089 : : // if this is a proper variable elimination, that is, var = slv where
1090 : : // var is not in the free variables of slv, then we can return this
1091 : : // as the variable elimination for lit.
1092 [ + + ]: 369 : if (isVarElim(var, slv))
1093 : : {
1094 : 119 : return slv;
1095 : : }
1096 : : }
1097 : : }
1098 : : else
1099 : : {
1100 [ + - ]: 612 : Trace("quant-velim-bv") << "...non-invertible path." << std::endl;
1101 : : }
1102 : : }
1103 : :
1104 : 1212 : return Node::null();
1105 : : }
1106 : :
1107 : 206 : Node QuantifiersRewriter::getVarElimEqString(Node lit,
1108 : : const std::vector<Node>& args,
1109 : : Node& var) const
1110 : : {
1111 [ - + ][ - + ]: 206 : Assert(lit.getKind() == Kind::EQUAL);
[ - - ]
1112 : 206 : NodeManager* nm = nodeManager();
1113 [ + + ]: 600 : for (unsigned i = 0; i < 2; i++)
1114 : : {
1115 [ + + ]: 412 : if (lit[i].getKind() == Kind::STRING_CONCAT)
1116 : : {
1117 : 46 : TypeNode stype = lit[i].getType();
1118 [ + + ]: 120 : for (unsigned j = 0, nchildren = lit[i].getNumChildren(); j < nchildren;
1119 : : j++)
1120 : : {
1121 [ + + ]: 92 : if (std::find(args.begin(), args.end(), lit[i][j]) != args.end())
1122 : : {
1123 : 58 : var = lit[i][j];
1124 : 58 : Node slv = lit[1 - i];
1125 : 116 : std::vector<Node> preL(lit[i].begin(), lit[i].begin() + j);
1126 : 58 : std::vector<Node> postL(lit[i].begin() + j + 1, lit[i].end());
1127 : 58 : Node tpre = strings::utils::mkConcat(preL, stype);
1128 : 58 : Node tpost = strings::utils::mkConcat(postL, stype);
1129 : 58 : Node slvL = nm->mkNode(Kind::STRING_LENGTH, slv);
1130 : 58 : Node tpreL = nm->mkNode(Kind::STRING_LENGTH, tpre);
1131 : 58 : Node tpostL = nm->mkNode(Kind::STRING_LENGTH, tpost);
1132 : 116 : slv = nm->mkNode(
1133 : : Kind::STRING_SUBSTR,
1134 : : slv,
1135 : : tpreL,
1136 : 116 : nm->mkNode(
1137 : 174 : Kind::SUB, slvL, nm->mkNode(Kind::ADD, tpreL, tpostL)));
1138 : : // forall x. r ++ x ++ t = s => P( x )
1139 : : // is equivalent to
1140 : : // r ++ s' ++ t = s => P( s' ) where
1141 : : // s' = substr( s, |r|, |s|-(|t|+|r|) ).
1142 : : // We apply this only if r,t,s do not contain free variables.
1143 [ + + ]: 58 : if (!expr::hasFreeVar(slv))
1144 : : {
1145 : 18 : return slv;
1146 : : }
1147 : : }
1148 : : }
1149 : : }
1150 : : }
1151 : :
1152 : 188 : return Node::null();
1153 : : }
1154 : :
1155 : 644757 : bool QuantifiersRewriter::getVarElimLit(Node body,
1156 : : Node lit,
1157 : : bool pol,
1158 : : std::vector<Node>& args,
1159 : : std::vector<Node>& vars,
1160 : : std::vector<Node>& subs) const
1161 : : {
1162 [ + + ]: 644757 : if (lit.getKind() == Kind::NOT)
1163 : : {
1164 : 15739 : lit = lit[0];
1165 : 15739 : pol = !pol;
1166 [ - + ][ - + ]: 15739 : Assert(lit.getKind() != Kind::NOT);
[ - - ]
1167 : : }
1168 : 644757 : NodeManager* nm = nodeManager();
1169 [ + - ]: 1289510 : Trace("var-elim-quant-debug")
1170 : 644757 : << "Eliminate : " << lit << ", pol = " << pol << "?" << std::endl;
1171 [ + + ]: 1277 : if (lit.getKind() == Kind::APPLY_TESTER && pol
1172 [ + + ][ + + ]: 645460 : && lit[0].getKind() == Kind::BOUND_VARIABLE
[ - - ]
1173 [ + + ][ + - ]: 646034 : && d_opts.quantifiers.dtVarExpandQuant)
[ + + ]
1174 : : {
1175 [ + - ]: 186 : Trace("var-elim-dt") << "Expand datatype variable based on : " << lit
1176 : 93 : << std::endl;
1177 : : std::vector<Node>::iterator ita =
1178 : 93 : std::find(args.begin(), args.end(), lit[0]);
1179 [ + - ]: 93 : if (ita != args.end())
1180 : : {
1181 : 93 : vars.push_back(lit[0]);
1182 : 186 : Node tester = lit.getOperator();
1183 : 93 : int index = datatypes::utils::indexOf(tester);
1184 : 93 : const DType& dt = datatypes::utils::datatypeOf(tester);
1185 : 93 : const DTypeConstructor& c = dt[index];
1186 : 186 : std::vector<Node> newChildren;
1187 : 186 : Node cons = c.getConstructor();
1188 : 186 : TypeNode tspec;
1189 : : // take into account if parametric
1190 [ + + ]: 93 : if (dt.isParametric())
1191 : : {
1192 : 2 : TypeNode ltn = lit[0].getType();
1193 : 2 : tspec = c.getInstantiatedConstructorType(ltn);
1194 : 2 : cons = c.getInstantiatedConstructor(ltn);
1195 : : }
1196 : : else
1197 : : {
1198 : 91 : tspec = cons.getType();
1199 : : }
1200 : 93 : newChildren.push_back(cons);
1201 : 93 : std::vector<Node> newVars;
1202 : 93 : BoundVarManager* bvm = nm->getBoundVarManager();
1203 [ + + ]: 292 : for (size_t j = 0, nargs = c.getNumArgs(); j < nargs; j++)
1204 : : {
1205 : 398 : TypeNode tn = tspec[j];
1206 : 398 : Node rn = nm->mkConstInt(Rational(j));
1207 : 597 : Node cacheVal = BoundVarManager::getCacheValue(body, lit, rn);
1208 : 597 : Node v = bvm->mkBoundVar<QRewDtExpandAttribute>(cacheVal, tn);
1209 : 199 : newChildren.push_back(v);
1210 : 199 : newVars.push_back(v);
1211 : : }
1212 : 93 : subs.push_back(nm->mkNode(Kind::APPLY_CONSTRUCTOR, newChildren));
1213 [ + - ]: 186 : Trace("var-elim-dt") << "...apply substitution " << subs[0] << "/"
1214 : 93 : << vars[0] << std::endl;
1215 : 93 : args.erase(ita);
1216 : 93 : args.insert(args.end(), newVars.begin(), newVars.end());
1217 : 93 : return true;
1218 : : }
1219 : : }
1220 : : // all eliminations below guarded by varElimQuant()
1221 [ + + ]: 644664 : if (!d_opts.quantifiers.varElimQuant)
1222 : : {
1223 : 8 : return false;
1224 : : }
1225 : :
1226 [ + + ]: 644656 : if (lit.getKind() == Kind::EQUAL)
1227 : : {
1228 : 347351 : if (pol || lit[0].getType().isBoolean())
1229 : : {
1230 [ + + ]: 507267 : for (unsigned i = 0; i < 2; i++)
1231 : : {
1232 : 342168 : bool tpol = pol;
1233 : 342168 : Node v_slv = lit[i];
1234 [ + + ]: 342168 : if (v_slv.getKind() == Kind::NOT)
1235 : : {
1236 : 13252 : v_slv = v_slv[0];
1237 : 13252 : tpol = !tpol;
1238 : : }
1239 : : std::vector<Node>::iterator ita =
1240 : 342168 : std::find(args.begin(), args.end(), v_slv);
1241 [ + + ]: 342168 : if (ita != args.end())
1242 : : {
1243 [ + + ]: 10924 : if (isVarElim(v_slv, lit[1 - i]))
1244 : : {
1245 : 9546 : Node slv = lit[1 - i];
1246 [ + + ]: 9546 : if (!tpol)
1247 : : {
1248 [ - + ][ - + ]: 956 : Assert(slv.getType().isBoolean());
[ - - ]
1249 : 956 : slv = slv.negate();
1250 : : }
1251 [ + - ]: 19092 : Trace("var-elim-quant")
1252 : 0 : << "Variable eliminate based on equality : " << v_slv << " -> "
1253 : 9546 : << slv << std::endl;
1254 : 9546 : vars.push_back(v_slv);
1255 : 9546 : subs.push_back(slv);
1256 : 9546 : args.erase(ita);
1257 : 9546 : return true;
1258 : : }
1259 : : }
1260 : : }
1261 : : }
1262 : : }
1263 [ + + ]: 635110 : if (lit.getKind() == Kind::BOUND_VARIABLE)
1264 : : {
1265 : 2760 : std::vector< Node >::iterator ita = std::find( args.begin(), args.end(), lit );
1266 [ + + ]: 2760 : if( ita!=args.end() ){
1267 [ + - ]: 2747 : Trace("var-elim-bool") << "Variable eliminate : " << lit << std::endl;
1268 : 2747 : vars.push_back( lit );
1269 : 2747 : subs.push_back(nodeManager()->mkConst(pol));
1270 : 2747 : args.erase( ita );
1271 : 2747 : return true;
1272 : : }
1273 : : }
1274 [ + + ][ + + ]: 632363 : if (lit.getKind() == Kind::EQUAL && pol)
[ + + ]
1275 : : {
1276 : 95225 : Node var;
1277 : 95225 : Node slv = getVarElimEq(lit, args, var);
1278 [ + + ]: 95225 : if (!slv.isNull())
1279 : : {
1280 [ - + ][ - + ]: 816 : Assert(!var.isNull());
[ - - ]
1281 : : std::vector<Node>::iterator ita =
1282 : 816 : std::find(args.begin(), args.end(), var);
1283 [ - + ][ - + ]: 816 : Assert(ita != args.end());
[ - - ]
1284 [ + - ]: 1632 : Trace("var-elim-quant")
1285 : 0 : << "Variable eliminate based on theory-specific solving : " << var
1286 : 816 : << " -> " << slv << std::endl;
1287 [ - + ][ - + ]: 816 : Assert(!expr::hasSubterm(slv, var));
[ - - ]
1288 [ - + ][ - + ]: 816 : Assert(slv.getType() == var.getType());
[ - - ]
1289 : 816 : vars.push_back(var);
1290 : 816 : subs.push_back(slv);
1291 : 816 : args.erase(ita);
1292 : 816 : return true;
1293 : : }
1294 : : }
1295 : 631547 : return false;
1296 : : }
1297 : :
1298 : 323027 : bool QuantifiersRewriter::getVarElim(Node body,
1299 : : std::vector<Node>& args,
1300 : : std::vector<Node>& vars,
1301 : : std::vector<Node>& subs,
1302 : : std::vector<Node>& lits) const
1303 : : {
1304 : 323027 : return getVarElimInternal(body, body, false, args, vars, subs, lits);
1305 : : }
1306 : :
1307 : 729398 : bool QuantifiersRewriter::getVarElimInternal(Node body,
1308 : : Node n,
1309 : : bool pol,
1310 : : std::vector<Node>& args,
1311 : : std::vector<Node>& vars,
1312 : : std::vector<Node>& subs,
1313 : : std::vector<Node>& lits) const
1314 : : {
1315 : 729398 : Kind nk = n.getKind();
1316 [ + + ]: 988113 : while (nk == Kind::NOT)
1317 : : {
1318 : 258715 : n = n[0];
1319 : 258715 : pol = !pol;
1320 : 258715 : nk = n.getKind();
1321 : : }
1322 [ + + ][ + + ]: 729398 : if ((nk == Kind::AND && pol) || (nk == Kind::OR && !pol))
[ + + ][ + - ]
1323 : : {
1324 [ + + ]: 539111 : for (const Node& cn : n)
1325 : : {
1326 [ + + ]: 405757 : if (getVarElimInternal(body, cn, pol, args, vars, subs, lits))
1327 : : {
1328 : 7573 : return true;
1329 : : }
1330 : : }
1331 : 133354 : return false;
1332 : : }
1333 [ + + ]: 588471 : if (getVarElimLit(body, n, pol, args, vars, subs))
1334 : : {
1335 [ + + ]: 8551 : lits.emplace_back(pol ? n : n.notNode());
1336 : 8551 : return true;
1337 : : }
1338 : 579920 : return false;
1339 : : }
1340 : :
1341 : 614 : bool QuantifiersRewriter::hasVarElim(Node n,
1342 : : bool pol,
1343 : : std::vector<Node>& args) const
1344 : : {
1345 : 1228 : std::vector< Node > vars;
1346 : 1228 : std::vector< Node > subs;
1347 : 614 : std::vector<Node> lits;
1348 : 1228 : return getVarElimInternal(n, n, pol, args, vars, subs, lits);
1349 : : }
1350 : :
1351 : 314797 : bool QuantifiersRewriter::getVarElimIneq(Node body,
1352 : : std::vector<Node>& args,
1353 : : std::vector<Node>& bounds,
1354 : : std::vector<Node>& subs,
1355 : : QAttributes& qa) const
1356 : : {
1357 [ + - ]: 314797 : Trace("var-elim-quant-debug") << "getVarElimIneq " << body << std::endl;
1358 : : // For each variable v, we compute a set of implied bounds in the body
1359 : : // of the quantified formula.
1360 : : // num_bounds[x][-1] stores the entailed lower bounds for x
1361 : : // num_bounds[x][1] stores the entailed upper bounds for x
1362 : : // num_bounds[x][0] stores the entailed disequalities for x
1363 : : // These bounds are stored in a map that maps the literal for the bound to
1364 : : // its required polarity. For example, for quantified formula
1365 : : // (forall ((x Int)) (or (= x 0) (>= x a)))
1366 : : // we have:
1367 : : // num_bounds[x][0] contains { x -> { (= x 0) -> false } }
1368 : : // num_bounds[x][-1] contains { x -> { (>= x a) -> false } }
1369 : : // This method succeeds in eliminating x if its only occurrences are in
1370 : : // entailed disequalities, and one kind of bound. This is the case for the
1371 : : // above quantified formula, which can be rewritten to false. The reason
1372 : : // is that we can always chose a value for x that is arbitrarily large (resp.
1373 : : // small) to satisfy all disequalities and inequalities for x.
1374 : 629594 : std::map<Node, std::map<int, std::map<Node, bool>>> num_bounds;
1375 : : // The set of variables that we know we can not eliminate
1376 : 629594 : std::unordered_set<Node> ineligVars;
1377 : : // compute the entailed literals
1378 : 629594 : QuantPhaseReq qpr(body);
1379 : : // map to track which literals we have already processed, and hence can be
1380 : : // excluded from the free variables check in the latter half of this method.
1381 : 629594 : std::map<Node, int> processed;
1382 [ + + ]: 862410 : for (const std::pair<const Node, bool>& pr : qpr.d_phase_reqs)
1383 : : {
1384 : : // an inequality that is entailed with a given polarity
1385 : 547613 : Node lit = pr.first;
1386 : 547613 : bool pol = pr.second;
1387 [ + - ]: 1095230 : Trace("var-elim-quant-debug") << "Process inequality bounds : " << lit
1388 : 547613 : << ", pol = " << pol << "..." << std::endl;
1389 : 1095230 : bool canSolve = lit.getKind() == Kind::GEQ
1390 [ + + ][ + + ]: 863690 : || (lit.getKind() == Kind::EQUAL
1391 : 863690 : && lit[0].getType().isRealOrInt() && !pol);
1392 [ + + ]: 547613 : if (!canSolve)
1393 : : {
1394 : 434389 : continue;
1395 : : }
1396 : : // solve the inequality
1397 : 113224 : std::map<Node, Node> msum;
1398 [ - + ]: 113224 : if (!ArithMSum::getMonomialSumLit(lit, msum))
1399 : : {
1400 : : // not an inequality, cannot use
1401 : 0 : continue;
1402 : : }
1403 [ + + ]: 113224 : processed[lit] = pol ? -1 : 1;
1404 [ + + ]: 350096 : for (const std::pair<const Node, Node>& m : msum)
1405 : : {
1406 [ + + ][ + + ]: 236872 : if (!m.first.isNull() && ineligVars.find(m.first) == ineligVars.end())
[ + + ]
1407 : : {
1408 : : std::vector<Node>::iterator ita =
1409 : 190715 : std::find(args.begin(), args.end(), m.first);
1410 [ + + ]: 190715 : if (ita != args.end())
1411 : : {
1412 : : // store that this literal is upper/lower bound for itm->first
1413 : 175010 : Node veq_c;
1414 : 175010 : Node val;
1415 : : int ires =
1416 : 87505 : ArithMSum::isolate(m.first, msum, veq_c, val, lit.getKind());
1417 [ + - ][ + + ]: 87505 : if (ires != 0 && veq_c.isNull())
[ + + ]
1418 : : {
1419 [ + + ]: 86785 : if (lit.getKind() == Kind::GEQ)
1420 : : {
1421 : 54164 : bool is_upper = pol != (ires == 1);
1422 [ + - ]: 108328 : Trace("var-elim-ineq-debug")
1423 [ - - ]: 0 : << lit << " is a " << (is_upper ? "upper" : "lower")
1424 : 54164 : << " bound for " << m.first << std::endl;
1425 [ + - ]: 108328 : Trace("var-elim-ineq-debug")
1426 : 54164 : << " pol/ires = " << pol << " " << ires << std::endl;
1427 [ + + ]: 54164 : num_bounds[m.first][is_upper ? 1 : -1][lit] = pol;
1428 : : }
1429 : : else
1430 : : {
1431 [ + - ]: 65242 : Trace("var-elim-ineq-debug")
1432 : 32621 : << lit << " is a disequality for " << m.first << std::endl;
1433 : 32621 : num_bounds[m.first][0][lit] = pol;
1434 : : }
1435 : : }
1436 : : else
1437 : : {
1438 [ + - ]: 1440 : Trace("var-elim-ineq-debug")
1439 : 0 : << "...ineligible " << m.first
1440 : 0 : << " since it cannot be solved for (" << ires << ", " << veq_c
1441 : 720 : << ")." << std::endl;
1442 : 720 : num_bounds.erase(m.first);
1443 : 720 : ineligVars.insert(m.first);
1444 : : }
1445 : : }
1446 : : else
1447 : : {
1448 : : // compute variables in itm->first, these are not eligible for
1449 : : // elimination
1450 : 206420 : std::unordered_set<Node> fvs;
1451 : 103210 : expr::getFreeVariables(m.first, fvs);
1452 [ + + ]: 214499 : for (const Node& v : fvs)
1453 : : {
1454 [ + - ]: 222578 : Trace("var-elim-ineq-debug")
1455 : 0 : << "...ineligible " << v
1456 : 111289 : << " since it is contained in monomial." << std::endl;
1457 : 111289 : num_bounds.erase(v);
1458 : 111289 : ineligVars.insert(v);
1459 : : }
1460 : : }
1461 : : }
1462 : : }
1463 : : }
1464 : :
1465 : : // collect all variables that have only upper/lower bounds
1466 : 629594 : std::map<Node, bool> elig_vars;
1467 : 46841 : for (const std::pair<const Node, std::map<int, std::map<Node, bool>>>& nb :
1468 [ + + ]: 408479 : num_bounds)
1469 : : {
1470 [ + + ]: 46841 : if (nb.second.find(1) == nb.second.end())
1471 : : {
1472 [ + - ]: 58844 : Trace("var-elim-ineq-debug")
1473 : 29422 : << "Variable " << nb.first << " has only lower bounds." << std::endl;
1474 : 29422 : elig_vars[nb.first] = false;
1475 : : }
1476 [ + + ]: 17419 : else if (nb.second.find(-1) == nb.second.end())
1477 : : {
1478 [ + - ]: 13736 : Trace("var-elim-ineq-debug")
1479 : 6868 : << "Variable " << nb.first << " has only upper bounds." << std::endl;
1480 : 6868 : elig_vars[nb.first] = true;
1481 : : }
1482 : : }
1483 [ + + ]: 314797 : if (elig_vars.empty())
1484 : : {
1485 : 285105 : return false;
1486 : : }
1487 : 59384 : std::vector<Node> inactive_vars;
1488 : 59384 : std::map<Node, std::map<int, bool> > visited;
1489 : : // traverse the body, invalidate variables if they occur in places other than
1490 : : // the bounds they occur in
1491 : 59384 : std::unordered_map<TNode, std::unordered_set<int>> evisited;
1492 : 59384 : std::vector<TNode> evisit;
1493 : 59384 : std::vector<int> evisit_pol;
1494 : 29692 : TNode ecur;
1495 : : int ecur_pol;
1496 : 29692 : evisit.push_back(body);
1497 : 29692 : evisit_pol.push_back(1);
1498 [ + + ]: 29692 : if (!qa.d_ipl.isNull())
1499 : : {
1500 : : // do not eliminate variables that occur in the annotation
1501 : 4154 : evisit.push_back(qa.d_ipl);
1502 : 4154 : evisit_pol.push_back(0);
1503 : : }
1504 : 184758 : do
1505 : : {
1506 : 214450 : ecur = evisit.back();
1507 : 214450 : evisit.pop_back();
1508 : 214450 : ecur_pol = evisit_pol.back();
1509 : 214450 : evisit_pol.pop_back();
1510 : 214450 : std::unordered_set<int>& epp = evisited[ecur];
1511 [ + + ]: 214450 : if (epp.find(ecur_pol) == epp.end())
1512 : : {
1513 : 210971 : epp.insert(ecur_pol);
1514 [ + + ]: 210971 : if (elig_vars.find(ecur) != elig_vars.end())
1515 : : {
1516 : : // variable contained in a place apart from bounds, no longer eligible
1517 : : // for elimination
1518 : 34013 : elig_vars.erase(ecur);
1519 [ + - ]: 68026 : Trace("var-elim-ineq-debug") << "...found occurrence of " << ecur
1520 : 34013 : << ", mark ineligible" << std::endl;
1521 : : }
1522 : : else
1523 : : {
1524 : 176958 : bool rec = true;
1525 : 176958 : bool pol = ecur_pol >= 0;
1526 : 176958 : bool hasPol = ecur_pol != 0;
1527 [ + + ]: 176958 : if (hasPol)
1528 : : {
1529 : 100059 : std::map<Node, int>::iterator itx = processed.find(ecur);
1530 [ + + ][ + + ]: 100059 : if (itx != processed.end() && itx->second == ecur_pol)
[ + + ]
1531 : : {
1532 : : // already processed this literal as a bound
1533 : 16885 : rec = false;
1534 : : }
1535 : : }
1536 [ + + ]: 176958 : if (rec)
1537 : : {
1538 [ + + ]: 418301 : for (unsigned j = 0, size = ecur.getNumChildren(); j < size; j++)
1539 : : {
1540 : : bool newHasPol;
1541 : : bool newPol;
1542 : 258228 : QuantPhaseReq::getPolarity(ecur, j, hasPol, pol, newHasPol, newPol);
1543 : 258228 : evisit.push_back(ecur[j]);
1544 [ + + ][ + + ]: 258228 : evisit_pol.push_back(newHasPol ? (newPol ? 1 : -1) : 0);
1545 : : }
1546 : : }
1547 : : }
1548 : : }
1549 [ + + ][ + + ]: 214450 : } while (!evisit.empty() && !elig_vars.empty());
[ + + ]
1550 : :
1551 : 29692 : bool ret = false;
1552 : 29692 : NodeManager* nm = nodeManager();
1553 [ + + ]: 31969 : for (const std::pair<const Node, bool>& ev : elig_vars)
1554 : : {
1555 : 2277 : Node v = ev.first;
1556 [ + - ]: 4554 : Trace("var-elim-ineq-debug")
1557 : 2277 : << v << " is eligible for elimination." << std::endl;
1558 : : // do substitution corresponding to infinite projection, all literals
1559 : : // involving unbounded variable go to true/false
1560 : : // disequalities of eligible variables are also eliminated
1561 : 2277 : std::map<int, std::map<Node, bool>>& nbv = num_bounds[v];
1562 [ + + ]: 6831 : for (size_t i = 0; i < 2; i++)
1563 : : {
1564 [ + + ][ + + ]: 4554 : size_t nindex = i == 0 ? (elig_vars[v] ? 1 : -1) : 0;
1565 [ + + ]: 7167 : for (const std::pair<const Node, bool>& nb : nbv[nindex])
1566 : : {
1567 [ + - ]: 5226 : Trace("var-elim-ineq-debug")
1568 : 2613 : << " subs : " << nb.first << " -> " << nb.second << std::endl;
1569 : 2613 : bounds.push_back(nb.first);
1570 : 2613 : subs.push_back(nm->mkConst(nb.second));
1571 : : }
1572 : : }
1573 : : // eliminate from args
1574 : 2277 : std::vector<Node>::iterator ita = std::find(args.begin(), args.end(), v);
1575 [ - + ][ - + ]: 2277 : Assert(ita != args.end());
[ - - ]
1576 : 2277 : args.erase(ita);
1577 : 2277 : ret = true;
1578 : : }
1579 : 29692 : return ret;
1580 : : }
1581 : :
1582 : 322086 : Node QuantifiersRewriter::computeVarElimination(Node body,
1583 : : std::vector<Node>& args,
1584 : : QAttributes& qa) const
1585 : : {
1586 [ + + ][ - + ]: 322086 : if (!d_opts.quantifiers.varElimQuant && !d_opts.quantifiers.dtVarExpandQuant
1587 [ - - ]: 0 : && !d_opts.quantifiers.varIneqElimQuant)
1588 : : {
1589 : 0 : return body;
1590 : : }
1591 [ + - ]: 644172 : Trace("var-elim-quant-debug")
1592 : 322086 : << "computeVarElimination " << body << std::endl;
1593 : 644172 : std::vector<Node> vars;
1594 : 644172 : std::vector<Node> subs;
1595 : : // standard variable elimination
1596 [ + + ]: 322086 : if (d_opts.quantifiers.varElimQuant)
1597 : : {
1598 : 321816 : std::vector<Node> lits;
1599 : 321816 : getVarElim(body, args, vars, subs, lits);
1600 : : }
1601 : : // variable elimination based on one-direction inequalities
1602 [ + + ][ + + ]: 322086 : if (vars.empty() && d_opts.quantifiers.varIneqElimQuant)
[ + + ]
1603 : : {
1604 : 314407 : getVarElimIneq(body, args, vars, subs, qa);
1605 : : }
1606 : : // if we eliminated a variable, update body and reprocess
1607 [ + + ]: 322086 : if (!vars.empty())
1608 : : {
1609 [ + - ]: 18618 : Trace("var-elim-quant-debug")
1610 : 9309 : << "VE " << vars.size() << "/" << args.size() << std::endl;
1611 [ - + ][ - + ]: 9309 : Assert(vars.size() == subs.size());
[ - - ]
1612 : : // remake with eliminated nodes
1613 : 9309 : body = body.substitute(vars.begin(), vars.end(), subs.begin(), subs.end());
1614 [ + + ]: 9309 : if (!qa.d_ipl.isNull())
1615 : : {
1616 : 138 : qa.d_ipl = qa.d_ipl.substitute(
1617 : 69 : vars.begin(), vars.end(), subs.begin(), subs.end());
1618 : : }
1619 [ + - ]: 9309 : Trace("var-elim-quant") << "Return " << body << std::endl;
1620 : : }
1621 : 322086 : return body;
1622 : : }
1623 : :
1624 : 2207600 : Node QuantifiersRewriter::computePrenex(Node q,
1625 : : Node body,
1626 : : std::unordered_set<Node>& args,
1627 : : std::unordered_set<Node>& nargs,
1628 : : bool pol,
1629 : : bool prenexAgg) const
1630 : : {
1631 : 2207600 : NodeManager* nm = nodeManager();
1632 : 2207600 : Kind k = body.getKind();
1633 [ + + ]: 2207600 : if (k == Kind::FORALL)
1634 : : {
1635 [ - + ]: 44366 : if ((pol || prenexAgg)
1636 [ + + ][ + - ]: 94100 : && (d_opts.quantifiers.prenexQuantUser
1637 [ + + ][ + + ]: 49734 : || !QuantAttributes::hasPattern(body)))
[ + + ][ - - ]
1638 : : {
1639 : 5288 : std::vector< Node > terms;
1640 : 5288 : std::vector< Node > subs;
1641 : 2644 : BoundVarManager* bvm = nm->getBoundVarManager();
1642 : : //for doing prenexing of same-signed quantifiers
1643 : : //must rename each variable that already exists
1644 [ + + ]: 6401 : for (const Node& v : body[0])
1645 : : {
1646 : 3757 : terms.push_back(v);
1647 : 7514 : TypeNode vt = v.getType();
1648 : 7514 : Node vv;
1649 [ + + ]: 3757 : if (!q.isNull())
1650 : : {
1651 : : // We cache based on the original quantified formula, the subformula
1652 : : // that we are pulling variables from (body), and the variable v.
1653 : : // The argument body is required since in rare cases, two subformulas
1654 : : // may share the same variables. This is the case for define-fun
1655 : : // or inferred substitutions that contain quantified formulas.
1656 : 7512 : Node cacheVal = BoundVarManager::getCacheValue(q, body, v);
1657 : 3756 : vv = bvm->mkBoundVar<QRewPrenexAttribute>(cacheVal, vt);
1658 : : }
1659 : : else
1660 : : {
1661 : : // not specific to a quantified formula, use normal
1662 : 1 : vv = nm->mkBoundVar(vt);
1663 : : }
1664 : 3757 : subs.push_back(vv);
1665 : : }
1666 [ + - ]: 2644 : if (pol)
1667 : : {
1668 : 2644 : args.insert(subs.begin(), subs.end());
1669 : : }
1670 : : else
1671 : : {
1672 : 0 : nargs.insert(subs.begin(), subs.end());
1673 : : }
1674 : 5288 : Node newBody = body[1];
1675 : 2644 : newBody = newBody.substitute( terms.begin(), terms.end(), subs.begin(), subs.end() );
1676 : 2644 : return newBody;
1677 : : }
1678 : : //must remove structure
1679 : : }
1680 [ + + ][ - + ]: 2160550 : else if (prenexAgg && k == Kind::ITE && body.getType().isBoolean())
[ - - ][ - + ]
[ - + ][ - - ]
1681 : : {
1682 : : Node nn = nm->mkNode(Kind::AND,
1683 : 0 : nm->mkNode(Kind::OR, body[0].notNode(), body[1]),
1684 : 0 : nm->mkNode(Kind::OR, body[0], body[2]));
1685 : 0 : return computePrenex(q, nn, args, nargs, pol, prenexAgg);
1686 : : }
1687 : 2160550 : else if (prenexAgg && k == Kind::EQUAL && body[0].getType().isBoolean())
1688 : : {
1689 : : Node nn = nm->mkNode(Kind::AND,
1690 : 0 : nm->mkNode(Kind::OR, body[0].notNode(), body[1]),
1691 : 0 : nm->mkNode(Kind::OR, body[0], body[1].notNode()));
1692 : 0 : return computePrenex(q, nn, args, nargs, pol, prenexAgg);
1693 [ + - ]: 2160550 : }else if( body.getType().isBoolean() ){
1694 [ - + ][ - + ]: 2160550 : Assert(k != Kind::EXISTS);
[ - - ]
1695 : 2160550 : bool childrenChanged = false;
1696 : 2160550 : std::vector< Node > newChildren;
1697 [ + + ]: 6319330 : for (size_t i = 0, nchild = body.getNumChildren(); i < nchild; i++)
1698 : : {
1699 : : bool newHasPol;
1700 : : bool newPol;
1701 : 4158780 : QuantPhaseReq::getPolarity( body, i, true, pol, newHasPol, newPol );
1702 [ + + ]: 4158780 : if (!newHasPol)
1703 : : {
1704 : 2237760 : newChildren.push_back( body[i] );
1705 : 2237760 : continue;
1706 : : }
1707 : 3842040 : Node n = computePrenex(q, body[i], args, nargs, newPol, prenexAgg);
1708 : 1921020 : newChildren.push_back(n);
1709 [ + + ][ + + ]: 1921020 : childrenChanged = n != body[i] || childrenChanged;
[ + - ][ - - ]
1710 : : }
1711 [ + + ]: 2160550 : if( childrenChanged ){
1712 [ - + ][ - - ]: 2560 : if (k == Kind::NOT && newChildren[0].getKind() == Kind::NOT)
[ - + ]
1713 : : {
1714 : 0 : return newChildren[0][0];
1715 : : }
1716 : 2560 : return nm->mkNode(k, newChildren);
1717 : : }
1718 : : }
1719 : 2202400 : return body;
1720 : : }
1721 : :
1722 : 129064 : Node QuantifiersRewriter::computeSplit(std::vector<Node>& args,
1723 : : Node body,
1724 : : QAttributes& qa) const
1725 : : {
1726 [ - + ][ - + ]: 129064 : Assert(body.getKind() == Kind::OR);
[ - - ]
1727 : 129064 : size_t eqc_count = 0;
1728 : 129064 : size_t eqc_active = 0;
1729 : 258128 : std::map< Node, int > var_to_eqc;
1730 : 258128 : std::map< int, std::vector< Node > > eqc_to_var;
1731 : 258128 : std::map< int, std::vector< Node > > eqc_to_lit;
1732 : :
1733 : 258128 : std::vector<Node> lits;
1734 : :
1735 [ + + ]: 887018 : for( unsigned i=0; i<body.getNumChildren(); i++ ){
1736 : : //get variables contained in the literal
1737 : 1515910 : Node n = body[i];
1738 : 1515910 : std::vector< Node > lit_args;
1739 : 757954 : computeArgVec( args, lit_args, n );
1740 [ + + ]: 757954 : if( lit_args.empty() ){
1741 : 4206 : lits.push_back( n );
1742 : : }else {
1743 : : //collect the equivalence classes this literal belongs to, and the new variables it contributes
1744 : 1507500 : std::vector< int > eqcs;
1745 : 1507500 : std::vector< Node > lit_new_args;
1746 : : //for each variable in literal
1747 [ + + ]: 2878740 : for( unsigned j=0; j<lit_args.size(); j++) {
1748 : : //see if the variable has already been found
1749 [ + + ]: 2124990 : if (var_to_eqc.find(lit_args[j])!=var_to_eqc.end()) {
1750 : 1400750 : int eqc = var_to_eqc[lit_args[j]];
1751 [ + + ]: 1400750 : if (std::find(eqcs.begin(), eqcs.end(), eqc)==eqcs.end()) {
1752 : 624086 : eqcs.push_back(eqc);
1753 : : }
1754 : : }else{
1755 : 724235 : lit_new_args.push_back(lit_args[j]);
1756 : : }
1757 : : }
1758 [ + + ]: 753748 : if (eqcs.empty()) {
1759 : 250677 : eqcs.push_back(eqc_count);
1760 : 250677 : eqc_count++;
1761 : 250677 : eqc_active++;
1762 : : }
1763 : :
1764 : 753748 : int eqcz = eqcs[0];
1765 : : //merge equivalence classes with eqcz
1766 [ + + ]: 874763 : for (unsigned j=1; j<eqcs.size(); j++) {
1767 : 121015 : int eqc = eqcs[j];
1768 : : //move all variables from equivalence class
1769 [ + + ]: 575863 : for (unsigned k=0; k<eqc_to_var[eqc].size(); k++) {
1770 : 909696 : Node v = eqc_to_var[eqc][k];
1771 : 454848 : var_to_eqc[v] = eqcz;
1772 : 454848 : eqc_to_var[eqcz].push_back(v);
1773 : : }
1774 : 121015 : eqc_to_var.erase(eqc);
1775 : : //move all literals from equivalence class
1776 [ + + ]: 510472 : for (unsigned k=0; k<eqc_to_lit[eqc].size(); k++) {
1777 : 778914 : Node l = eqc_to_lit[eqc][k];
1778 : 389457 : eqc_to_lit[eqcz].push_back(l);
1779 : : }
1780 : 121015 : eqc_to_lit.erase(eqc);
1781 : 121015 : eqc_active--;
1782 : : }
1783 : : //add variables to equivalence class
1784 [ + + ]: 1477980 : for (unsigned j=0; j<lit_new_args.size(); j++) {
1785 : 724235 : var_to_eqc[lit_new_args[j]] = eqcz;
1786 : 724235 : eqc_to_var[eqcz].push_back(lit_new_args[j]);
1787 : : }
1788 : : //add literal to equivalence class
1789 : 753748 : eqc_to_lit[eqcz].push_back(n);
1790 : : }
1791 : : }
1792 [ + + ][ + + ]: 129064 : if ( eqc_active>1 || !lits.empty() || var_to_eqc.size()!=args.size() ){
[ + + ][ + + ]
1793 : 1923 : NodeManager* nm = nodeManager();
1794 [ - + ]: 1923 : if (TraceIsOn("clause-split-debug"))
1795 : : {
1796 [ - - ]: 0 : Trace("clause-split-debug")
1797 : 0 : << "Split quantified formula with body " << body << std::endl;
1798 [ - - ]: 0 : Trace("clause-split-debug") << " Ground literals: " << std::endl;
1799 [ - - ]: 0 : for (size_t i = 0; i < lits.size(); i++)
1800 : : {
1801 [ - - ]: 0 : Trace("clause-split-debug") << " " << lits[i] << std::endl;
1802 : : }
1803 [ - - ]: 0 : Trace("clause-split-debug") << std::endl;
1804 [ - - ]: 0 : Trace("clause-split-debug") << "Equivalence classes: " << std::endl;
1805 : : }
1806 [ + + ]: 4444 : for (std::map< int, std::vector< Node > >::iterator it = eqc_to_lit.begin(); it != eqc_to_lit.end(); ++it ){
1807 : 2521 : int eqc = it->first;
1808 [ - + ]: 2521 : if (TraceIsOn("clause-split-debug"))
1809 : : {
1810 [ - - ]: 0 : Trace("clause-split-debug") << " Literals: " << std::endl;
1811 [ - - ]: 0 : for (size_t i = 0; i < it->second.size(); i++)
1812 : : {
1813 [ - - ]: 0 : Trace("clause-split-debug") << " " << it->second[i] << std::endl;
1814 : : }
1815 [ - - ]: 0 : Trace("clause-split-debug") << " Variables: " << std::endl;
1816 [ - - ]: 0 : for (size_t i = 0; i < eqc_to_var[eqc].size(); i++)
1817 : : {
1818 [ - - ]: 0 : Trace("clause-split-debug")
1819 : 0 : << " " << eqc_to_var[eqc][i] << std::endl;
1820 : : }
1821 [ - - ]: 0 : Trace("clause-split-debug") << std::endl;
1822 : : }
1823 : 2521 : std::vector<Node>& evars = eqc_to_var[eqc];
1824 : : // for the sake of proofs, we provide the variables in the order
1825 : : // they appear in the original quantified formula
1826 : 5042 : std::vector<Node> ovars;
1827 [ + + ]: 68571 : for (const Node& v : args)
1828 : : {
1829 [ + + ]: 66050 : if (std::find(evars.begin(), evars.end(), v) != evars.end())
1830 : : {
1831 : 28292 : ovars.emplace_back(v);
1832 : : }
1833 : : }
1834 : 5042 : Node bvl = nodeManager()->mkNode(Kind::BOUND_VAR_LIST, ovars);
1835 : 3485 : Node bd = it->second.size() == 1 ? it->second[0]
1836 [ + + ]: 6006 : : nm->mkNode(Kind::OR, it->second);
1837 : 7563 : Node fa = nm->mkNode(Kind::FORALL, bvl, bd);
1838 : 2521 : lits.push_back(fa);
1839 : : }
1840 [ - + ][ - + ]: 1923 : Assert(!lits.empty());
[ - - ]
1841 : 3846 : Node nf = nodeManager()->mkOr(lits);
1842 [ + - ]: 1923 : Trace("clause-split-debug") << "Made node : " << nf << std::endl;
1843 : 1923 : return nf;
1844 : : }
1845 : 127141 : return Node::null();
1846 : : }
1847 : :
1848 : 298782 : Node QuantifiersRewriter::mkForAll(const std::vector<Node>& args,
1849 : : Node body,
1850 : : QAttributes& qa) const
1851 : : {
1852 [ + + ]: 298782 : if (args.empty())
1853 : : {
1854 : 623 : return body;
1855 : : }
1856 : 298159 : NodeManager* nm = nodeManager();
1857 : 596318 : std::vector<Node> children;
1858 : 298159 : children.push_back(nm->mkNode(Kind::BOUND_VAR_LIST, args));
1859 : 298159 : children.push_back(body);
1860 [ + + ]: 298159 : if (!qa.d_ipl.isNull())
1861 : : {
1862 : 845 : children.push_back(qa.d_ipl);
1863 : : }
1864 : 298159 : return nm->mkNode(Kind::FORALL, children);
1865 : : }
1866 : :
1867 : 1 : Node QuantifiersRewriter::mkForall(const std::vector<Node>& args,
1868 : : Node body,
1869 : : bool marked) const
1870 : : {
1871 : 1 : std::vector< Node > iplc;
1872 : 2 : return mkForall( args, body, iplc, marked );
1873 : : }
1874 : :
1875 : 2 : Node QuantifiersRewriter::mkForall(const std::vector<Node>& args,
1876 : : Node body,
1877 : : std::vector<Node>& iplc,
1878 : : bool marked) const
1879 : : {
1880 [ - + ]: 2 : if (args.empty())
1881 : : {
1882 : 0 : return body;
1883 : : }
1884 : 2 : NodeManager* nm = nodeManager();
1885 : 4 : std::vector<Node> children;
1886 : 2 : children.push_back(nm->mkNode(Kind::BOUND_VAR_LIST, args));
1887 : 2 : children.push_back(body);
1888 [ + - ]: 2 : if (marked)
1889 : : {
1890 : 2 : SkolemManager* sm = nm->getSkolemManager();
1891 : 4 : Node avar = sm->mkDummySkolem("id", nm->booleanType());
1892 : : QuantIdNumAttribute ida;
1893 : 2 : avar.setAttribute(ida, 0);
1894 : 2 : iplc.push_back(nm->mkNode(Kind::INST_ATTRIBUTE, avar));
1895 : : }
1896 [ + - ]: 2 : if (!iplc.empty())
1897 : : {
1898 : 2 : children.push_back(nm->mkNode(Kind::INST_PATTERN_LIST, iplc));
1899 : : }
1900 : 2 : return nm->mkNode(Kind::FORALL, children);
1901 : : }
1902 : :
1903 : : //computes miniscoping, also eliminates variables that do not occur free in body
1904 : 301815 : Node QuantifiersRewriter::computeMiniscoping(Node q,
1905 : : QAttributes& qa,
1906 : : bool miniscopeConj,
1907 : : bool miniscopeFv) const
1908 : : {
1909 : 301815 : NodeManager* nm = nodeManager();
1910 : 905445 : std::vector<Node> args(q[0].begin(), q[0].end());
1911 : 603630 : Node body = q[1];
1912 [ + + ]: 301815 : if (body.getKind() == Kind::AND)
1913 : : {
1914 : : // aggressive miniscoping implies that structural miniscoping should
1915 : : // be applied first
1916 [ + + ]: 4446 : if (miniscopeConj)
1917 : : {
1918 : 1706 : BoundVarManager* bvm = nm->getBoundVarManager();
1919 : : // Break apart the quantifed formula
1920 : : // forall x. P1 ^ ... ^ Pn ---> forall x. P1 ^ ... ^ forall x. Pn
1921 : 3412 : NodeBuilder t(Kind::AND);
1922 : 3412 : std::vector<Node> argsc;
1923 [ + + ]: 9061 : for (size_t i = 0, nchild = body.getNumChildren(); i < nchild; i++)
1924 : : {
1925 [ + + ]: 7355 : if (argsc.empty())
1926 : : {
1927 : : // If not done so, we must create fresh copy of args. This is to
1928 : : // ensure that quantified formulas do not reuse variables.
1929 [ + + ]: 14323 : for (const Node& v : q[0])
1930 : : {
1931 : 19762 : TypeNode vt = v.getType();
1932 : 29643 : Node cacheVal = BoundVarManager::getCacheValue(q, v, i);
1933 : 29643 : Node vv = bvm->mkBoundVar<QRewMiniscopeAttribute>(cacheVal, vt);
1934 : 9881 : argsc.push_back(vv);
1935 : : }
1936 : : }
1937 : 14710 : Node b = body[i];
1938 : : Node bodyc =
1939 : 14710 : b.substitute(args.begin(), args.end(), argsc.begin(), argsc.end());
1940 [ + + ]: 7355 : if (b == bodyc)
1941 : : {
1942 : : // Did not contain variables in args, thus it is ground. Since we did
1943 : : // not use them, we keep the variables argsc for the next child.
1944 : 3055 : t << b;
1945 : : }
1946 : : else
1947 : : {
1948 : : // make the miniscoped quantified formula
1949 : 8600 : Node cbvl = nm->mkNode(Kind::BOUND_VAR_LIST, argsc);
1950 : 12900 : Node qq = nm->mkNode(Kind::FORALL, cbvl, bodyc);
1951 : 4300 : t << qq;
1952 : : // We used argsc, clear so we will construct a fresh copy above.
1953 : 4300 : argsc.clear();
1954 : : }
1955 : : }
1956 : 3412 : Node retVal = t;
1957 : 1706 : return retVal;
1958 : : }
1959 : : }
1960 [ + + ]: 297369 : else if (body.getKind() == Kind::OR)
1961 : : {
1962 [ + + ]: 134606 : if (miniscopeFv)
1963 : : {
1964 : : //splitting subsumes free variable miniscoping, apply it with higher priority
1965 : 128457 : Node ret = computeSplit(args, body, qa);
1966 [ + + ]: 128457 : if (!ret.isNull())
1967 : : {
1968 : 1645 : return ret;
1969 : : }
1970 : : }
1971 : : }
1972 [ + + ]: 162763 : else if (body.getKind() == Kind::NOT)
1973 : : {
1974 [ - + ][ - + ]: 39055 : Assert(isLiteral(body[0]));
[ - - ]
1975 : : }
1976 : : //remove variables that don't occur
1977 : 298464 : std::vector< Node > activeArgs;
1978 : 298464 : computeArgVec2( args, activeArgs, body, qa.d_ipl );
1979 : 298464 : return mkForAll( activeArgs, body, qa );
1980 : : }
1981 : :
1982 : 344 : Node QuantifiersRewriter::computeAggressiveMiniscoping(std::vector<Node>& args,
1983 : : Node body) const
1984 : : {
1985 : 688 : std::map<Node, std::vector<Node> > varLits;
1986 : 688 : std::map<Node, std::vector<Node> > litVars;
1987 [ + + ]: 344 : if (body.getKind() == Kind::OR)
1988 : : {
1989 [ + - ]: 100 : Trace("ag-miniscope") << "compute aggressive miniscoping on " << body << std::endl;
1990 [ + + ]: 312 : for (size_t i = 0; i < body.getNumChildren(); i++) {
1991 : 212 : std::vector<Node> activeArgs;
1992 : 212 : computeArgVec(args, activeArgs, body[i]);
1993 [ + + ]: 476 : for (unsigned j = 0; j < activeArgs.size(); j++) {
1994 : 264 : varLits[activeArgs[j]].push_back(body[i]);
1995 : : }
1996 : 212 : std::vector<Node>& lit_body_i = litVars[body[i]];
1997 : 212 : std::vector<Node>::iterator lit_body_i_begin = lit_body_i.begin();
1998 : 212 : std::vector<Node>::const_iterator active_begin = activeArgs.begin();
1999 : 212 : std::vector<Node>::const_iterator active_end = activeArgs.end();
2000 : 212 : lit_body_i.insert(lit_body_i_begin, active_begin, active_end);
2001 : : }
2002 : : //find the variable in the least number of literals
2003 : 100 : Node bestVar;
2004 [ + + ]: 252 : for( std::map< Node, std::vector<Node> >::iterator it = varLits.begin(); it != varLits.end(); ++it ){
2005 [ + + ][ + + ]: 152 : if( bestVar.isNull() || varLits[bestVar].size()>it->second.size() ){
[ + + ]
2006 : 124 : bestVar = it->first;
2007 : : }
2008 : : }
2009 [ + - ]: 100 : Trace("ag-miniscope-debug") << "Best variable " << bestVar << " occurs in " << varLits[bestVar].size() << "/ " << body.getNumChildren() << " literals." << std::endl;
2010 [ + - ][ + + ]: 100 : if( !bestVar.isNull() && varLits[bestVar].size()<body.getNumChildren() ){
[ + + ]
2011 : : //we can miniscope
2012 [ + - ]: 26 : Trace("ag-miniscope") << "Miniscope on " << bestVar << std::endl;
2013 : : //make the bodies
2014 : 52 : std::vector<Node> qlit1;
2015 : 26 : qlit1.insert( qlit1.begin(), varLits[bestVar].begin(), varLits[bestVar].end() );
2016 : 52 : std::vector<Node> qlitt;
2017 : : //for all literals not containing bestVar
2018 [ + + ]: 90 : for( size_t i=0; i<body.getNumChildren(); i++ ){
2019 [ + + ]: 64 : if( std::find( qlit1.begin(), qlit1.end(), body[i] )==qlit1.end() ){
2020 : 38 : qlitt.push_back( body[i] );
2021 : : }
2022 : : }
2023 : : //make the variable lists
2024 : 52 : std::vector<Node> qvl1;
2025 : 52 : std::vector<Node> qvl2;
2026 : 52 : std::vector<Node> qvsh;
2027 [ + + ]: 104 : for( unsigned i=0; i<args.size(); i++ ){
2028 : 78 : bool found1 = false;
2029 : 78 : bool found2 = false;
2030 [ + + ]: 168 : for( size_t j=0; j<varLits[args[i]].size(); j++ ){
2031 [ + + ][ + + ]: 116 : if( !found1 && std::find( qlit1.begin(), qlit1.end(), varLits[args[i]][j] )!=qlit1.end() ){
[ + + ]
2032 : 52 : found1 = true;
2033 [ + + ][ + - ]: 64 : }else if( !found2 && std::find( qlitt.begin(), qlitt.end(), varLits[args[i]][j] )!=qlitt.end() ){
[ + + ]
2034 : 52 : found2 = true;
2035 : : }
2036 [ + + ][ + + ]: 116 : if( found1 && found2 ){
2037 : 26 : break;
2038 : : }
2039 : : }
2040 [ + + ]: 78 : if( found1 ){
2041 [ + + ]: 52 : if( found2 ){
2042 : 26 : qvsh.push_back( args[i] );
2043 : : }else{
2044 : 26 : qvl1.push_back( args[i] );
2045 : : }
2046 : : }else{
2047 [ - + ][ - + ]: 26 : Assert(found2);
[ - - ]
2048 : 26 : qvl2.push_back( args[i] );
2049 : : }
2050 : : }
2051 [ - + ][ - + ]: 26 : Assert(!qvl1.empty());
[ - - ]
2052 : : //check for literals that only contain shared variables
2053 : 52 : std::vector<Node> qlitsh;
2054 : 52 : std::vector<Node> qlit2;
2055 [ + + ]: 64 : for( size_t i=0; i<qlitt.size(); i++ ){
2056 : 38 : bool hasVar2 = false;
2057 [ + + ]: 52 : for( size_t j=0; j<litVars[qlitt[i]].size(); j++ ){
2058 [ + + ]: 40 : if( std::find( qvl2.begin(), qvl2.end(), litVars[qlitt[i]][j] )!=qvl2.end() ){
2059 : 26 : hasVar2 = true;
2060 : 26 : break;
2061 : : }
2062 : : }
2063 [ + + ]: 38 : if( hasVar2 ){
2064 : 26 : qlit2.push_back( qlitt[i] );
2065 : : }else{
2066 : 12 : qlitsh.push_back( qlitt[i] );
2067 : : }
2068 : : }
2069 : 26 : varLits.clear();
2070 : 26 : litVars.clear();
2071 [ + - ]: 26 : Trace("ag-miniscope-debug") << "Split into literals : " << qlit1.size() << " / " << qlit2.size() << " / " << qlitsh.size();
2072 [ + - ]: 26 : Trace("ag-miniscope-debug") << ", variables : " << qvl1.size() << " / " << qvl2.size() << " / " << qvsh.size() << std::endl;
2073 : : Node n1 =
2074 [ + - ]: 52 : qlit1.size() == 1 ? qlit1[0] : nodeManager()->mkNode(Kind::OR, qlit1);
2075 : 26 : n1 = computeAggressiveMiniscoping( qvl1, n1 );
2076 : 26 : qlitsh.push_back( n1 );
2077 [ + + ]: 26 : if( !qlit2.empty() ){
2078 : 16 : Node n2 = qlit2.size() == 1 ? qlit2[0]
2079 [ + + ]: 30 : : nodeManager()->mkNode(Kind::OR, qlit2);
2080 : 14 : n2 = computeAggressiveMiniscoping( qvl2, n2 );
2081 : 14 : qlitsh.push_back( n2 );
2082 : : }
2083 : 52 : Node n = nodeManager()->mkNode(Kind::OR, qlitsh);
2084 [ + - ]: 26 : if( !qvsh.empty() ){
2085 : 26 : Node bvl = nodeManager()->mkNode(Kind::BOUND_VAR_LIST, qvsh);
2086 : 26 : n = nodeManager()->mkNode(Kind::FORALL, bvl, n);
2087 : : }
2088 [ + - ]: 26 : Trace("ag-miniscope") << "Return " << n << " for " << body << std::endl;
2089 : 26 : return n;
2090 : : }
2091 : : }
2092 : 318 : QAttributes qa;
2093 : 318 : return mkForAll( args, body, qa );
2094 : : }
2095 : :
2096 : 1 : bool QuantifiersRewriter::isStandard(const Node& q, const Options& opts)
2097 : : {
2098 : 2 : QAttributes qa;
2099 : 1 : QuantAttributes::computeQuantAttributes(q, qa);
2100 : 2 : return isStandard(qa, opts);
2101 : : }
2102 : :
2103 : 2763420 : bool QuantifiersRewriter::isStandard(QAttributes& qa, const Options& opts)
2104 : : {
2105 : 2763420 : bool is_strict_trigger =
2106 : 2763420 : qa.d_hasPattern
2107 [ + + ][ + + ]: 2763420 : && opts.quantifiers.userPatternsQuant == options::UserPatMode::STRICT;
2108 [ + + ][ + - ]: 2763420 : return qa.isStandard() && !is_strict_trigger;
2109 : : }
2110 : :
2111 : 2763420 : bool QuantifiersRewriter::doOperation(Node q,
2112 : : RewriteStep computeOption,
2113 : : QAttributes& qa) const
2114 : : {
2115 : 2763420 : bool is_strict_trigger =
2116 : 2763420 : qa.d_hasPattern
2117 [ + + ][ + + ]: 2763420 : && d_opts.quantifiers.userPatternsQuant == options::UserPatMode::STRICT;
2118 : 2763420 : bool is_std = isStandard(qa, d_opts);
2119 [ + + ]: 2763420 : if (computeOption == COMPUTE_ELIM_SYMBOLS)
2120 : : {
2121 : 386591 : return true;
2122 : : }
2123 [ + + ]: 2376830 : else if (computeOption == COMPUTE_MINISCOPING
2124 [ + + ]: 2024880 : || computeOption == COMPUTE_AGGRESSIVE_MINISCOPING)
2125 : : {
2126 : : // in the rare case the body is ground, we always eliminate unless it
2127 : : // is truly a non-standard quantified formula (e.g. one for QE).
2128 [ + + ]: 699589 : if (!expr::hasBoundVar(q[1]))
2129 : : {
2130 : : // This returns true if q is a non-standard quantified formula. Note that
2131 : : // is_std is additionally true if user-pat is strict and q has user
2132 : : // patterns.
2133 : 3142 : return qa.isStandard();
2134 : : }
2135 [ + + ]: 696447 : if (!is_std)
2136 : : {
2137 : 26456 : return false;
2138 : : }
2139 : : // do not miniscope if we have user patterns unless option is set
2140 [ + - ][ + + ]: 669991 : if (!d_opts.quantifiers.miniscopeQuantUser && qa.d_hasPattern)
2141 : : {
2142 : 71734 : return false;
2143 : : }
2144 [ + + ]: 598257 : if (computeOption == COMPUTE_AGGRESSIVE_MINISCOPING)
2145 : : {
2146 : 297220 : return d_opts.quantifiers.miniscopeQuant
2147 : 297220 : == options::MiniscopeQuantMode::AGG;
2148 : : }
2149 : 301037 : return true;
2150 : : }
2151 [ + + ]: 1677240 : else if (computeOption == COMPUTE_EXT_REWRITE)
2152 : : {
2153 : 326886 : return d_opts.quantifiers.extRewriteQuant;
2154 : : }
2155 [ + + ]: 1350360 : else if (computeOption == COMPUTE_PROCESS_TERMS)
2156 : : {
2157 : 347619 : return true;
2158 : : }
2159 [ + + ]: 1002740 : else if (computeOption == COMPUTE_COND_SPLIT)
2160 : : {
2161 : 327321 : return (d_opts.quantifiers.iteDtTesterSplitQuant
2162 [ + - ]: 326625 : || d_opts.quantifiers.condVarSplitQuant
2163 : : != options::CondVarSplitQuantMode::OFF)
2164 [ + + ][ + + ]: 653946 : && !is_strict_trigger;
2165 : : }
2166 [ + + ]: 675418 : else if (computeOption == COMPUTE_PRENEX)
2167 : : {
2168 : : // do not prenex to pull variables into those with user patterns
2169 [ + + ][ + + ]: 338788 : if (!d_opts.quantifiers.prenexQuantUser && qa.d_hasPattern)
2170 : : {
2171 : 35871 : return false;
2172 : : }
2173 [ + + ]: 302917 : if (qa.d_hasPool)
2174 : : {
2175 : 314 : return false;
2176 : : }
2177 : 302603 : return d_opts.quantifiers.prenexQuant != options::PrenexQuantMode::NONE
2178 [ + + ]: 300920 : && d_opts.quantifiers.miniscopeQuant
2179 : : != options::MiniscopeQuantMode::AGG
2180 [ + + ][ + + ]: 603523 : && is_std;
2181 : : }
2182 [ + - ]: 336630 : else if (computeOption == COMPUTE_VAR_ELIMINATION)
2183 : : {
2184 : 336630 : return (d_opts.quantifiers.varElimQuant
2185 [ + - ]: 270 : || d_opts.quantifiers.dtVarExpandQuant)
2186 [ + + ][ + + ]: 336900 : && is_std && !is_strict_trigger;
[ + - ]
2187 : : }
2188 : : else
2189 : : {
2190 : 0 : return false;
2191 : : }
2192 : : }
2193 : :
2194 : : //general method for computing various rewrites
2195 : 1972040 : Node QuantifiersRewriter::computeOperation(Node f,
2196 : : RewriteStep computeOption,
2197 : : QAttributes& qa) const
2198 : : {
2199 [ + - ]: 1972040 : Trace("quantifiers-rewrite-debug") << "Compute operation " << computeOption << " on " << f << " " << qa.d_qid_num << std::endl;
2200 [ + + ]: 1972040 : if (computeOption == COMPUTE_MINISCOPING)
2201 : : {
2202 [ + + ]: 301543 : if (d_opts.quantifiers.prenexQuant == options::PrenexQuantMode::NORMAL)
2203 : : {
2204 [ + + ]: 9 : if( !qa.d_qid_num.isNull() ){
2205 : : //already processed this, return self
2206 : 7 : return f;
2207 : : }
2208 : : }
2209 : 301536 : bool miniscopeConj = doMiniscopeConj(d_opts);
2210 : 301536 : bool miniscopeFv = doMiniscopeFv(d_opts);
2211 : : //return directly
2212 : 301536 : return computeMiniscoping(f, qa, miniscopeConj, miniscopeFv);
2213 : : }
2214 : 5011490 : std::vector<Node> args(f[0].begin(), f[0].end());
2215 : 3340990 : Node n = f[1];
2216 [ + + ]: 1670500 : if (computeOption == COMPUTE_ELIM_SYMBOLS)
2217 : : {
2218 : : // relies on external utility
2219 : 386591 : n = booleans::TheoryBoolRewriter::computeNnfNorm(nodeManager(), n);
2220 : : }
2221 [ + + ]: 1283910 : else if (computeOption == COMPUTE_AGGRESSIVE_MINISCOPING)
2222 : : {
2223 : 304 : return computeAggressiveMiniscoping( args, n );
2224 : : }
2225 [ + + ]: 1283600 : else if (computeOption == COMPUTE_EXT_REWRITE)
2226 : : {
2227 : 28 : return computeExtendedRewrite(f, qa);
2228 : : }
2229 [ + + ]: 1283570 : else if (computeOption == COMPUTE_PROCESS_TERMS)
2230 : : {
2231 : 347619 : n = computeProcessTerms(f, args, n, qa);
2232 : : }
2233 [ + + ]: 935955 : else if (computeOption == COMPUTE_COND_SPLIT)
2234 : : {
2235 : 327277 : n = computeCondSplit(n, args, qa);
2236 : : }
2237 [ + + ]: 608678 : else if (computeOption == COMPUTE_PRENEX)
2238 : : {
2239 [ + + ]: 286592 : if (d_opts.quantifiers.prenexQuant == options::PrenexQuantMode::NORMAL)
2240 : : {
2241 : : //will rewrite at preprocess time
2242 : 9 : return f;
2243 : : }
2244 : : else
2245 : : {
2246 : 573166 : std::unordered_set<Node> argsSet, nargsSet;
2247 : 286583 : n = computePrenex(f, n, argsSet, nargsSet, true, false);
2248 [ - + ][ - + ]: 286583 : Assert(nargsSet.empty());
[ - - ]
2249 : 286583 : args.insert(args.end(), argsSet.begin(), argsSet.end());
2250 : : }
2251 : : }
2252 [ + - ]: 322086 : else if (computeOption == COMPUTE_VAR_ELIMINATION)
2253 : : {
2254 : 322086 : n = computeVarElimination( n, args, qa );
2255 : : }
2256 [ + - ]: 1670160 : Trace("quantifiers-rewrite-debug") << "Compute Operation: return " << n << ", " << args.size() << std::endl;
2257 : 1670160 : if( f[1]==n && args.size()==f[0].getNumChildren() ){
2258 : 1614790 : return f;
2259 : : }else{
2260 [ + + ]: 55368 : if( args.empty() ){
2261 : 2538 : return n;
2262 : : }else{
2263 : 105660 : std::vector< Node > children;
2264 : 52830 : children.push_back(nodeManager()->mkNode(Kind::BOUND_VAR_LIST, args));
2265 : 52830 : children.push_back( n );
2266 [ + + ][ + + ]: 52830 : if( !qa.d_ipl.isNull() && args.size()==f[0].getNumChildren() ){
[ + + ][ + + ]
[ - - ]
2267 : 5909 : children.push_back( qa.d_ipl );
2268 : : }
2269 : 52830 : return nodeManager()->mkNode(Kind::FORALL, children);
2270 : : }
2271 : : }
2272 : : }
2273 : 628813 : bool QuantifiersRewriter::doMiniscopeConj(const Options& opts)
2274 : : {
2275 : 628813 : options::MiniscopeQuantMode mqm = opts.quantifiers.miniscopeQuant;
2276 : : return mqm == options::MiniscopeQuantMode::CONJ_AND_FV
2277 [ + - ]: 28218 : || mqm == options::MiniscopeQuantMode::CONJ
2278 [ + + ][ + + ]: 657031 : || mqm == options::MiniscopeQuantMode::AGG;
2279 : : }
2280 : :
2281 : 301536 : bool QuantifiersRewriter::doMiniscopeFv(const Options& opts)
2282 : : {
2283 : 301536 : options::MiniscopeQuantMode mqm = opts.quantifiers.miniscopeQuant;
2284 : : return mqm == options::MiniscopeQuantMode::CONJ_AND_FV
2285 [ + + ]: 12084 : || mqm == options::MiniscopeQuantMode::FV
2286 [ + + ][ + + ]: 313620 : || mqm == options::MiniscopeQuantMode::AGG;
2287 : : }
2288 : :
2289 : 0 : bool QuantifiersRewriter::isPrenexNormalForm( Node n ) {
2290 [ - - ]: 0 : if (n.getKind() == Kind::FORALL)
2291 : : {
2292 : 0 : return n[1].getKind() != Kind::FORALL && isPrenexNormalForm(n[1]);
2293 : : }
2294 [ - - ]: 0 : else if (n.getKind() == Kind::NOT)
2295 : : {
2296 : 0 : return n[0].getKind() != Kind::NOT && isPrenexNormalForm(n[0]);
2297 : : }
2298 : : else
2299 : : {
2300 : 0 : return !expr::hasClosure(n);
2301 : : }
2302 : : }
2303 : :
2304 : : } // namespace quantifiers
2305 : : } // namespace theory
2306 : : } // namespace cvc5::internal
|
