GCC Code Coverage Report
Directory: . Exec Total Coverage
File: src/theory/quantifiers/quantifiers_rewriter.cpp Lines: 892 1167 76.4 %
Date: 2021-03-22 Branches: 2043 5077 40.2 %

Line Exec Source
1
/*********************                                                        */
2
/*! \file quantifiers_rewriter.cpp
3
 ** \verbatim
4
 ** Top contributors (to current version):
5
 **   Andrew Reynolds, Morgan Deters, Haniel Barbosa
6
 ** This file is part of the CVC4 project.
7
 ** Copyright (c) 2009-2021 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.\endverbatim
11
 **
12
 ** \brief Implementation of QuantifiersRewriter class
13
 **/
14
15
#include "theory/quantifiers/quantifiers_rewriter.h"
16
17
#include "expr/bound_var_manager.h"
18
#include "expr/dtype.h"
19
#include "expr/dtype_cons.h"
20
#include "expr/node_algorithm.h"
21
#include "options/quantifiers_options.h"
22
#include "theory/arith/arith_msum.h"
23
#include "theory/datatypes/theory_datatypes_utils.h"
24
#include "theory/quantifiers/bv_inverter.h"
25
#include "theory/quantifiers/ematching/trigger.h"
26
#include "theory/quantifiers/extended_rewrite.h"
27
#include "theory/quantifiers/quantifiers_attributes.h"
28
#include "theory/quantifiers/skolemize.h"
29
#include "theory/quantifiers/term_database.h"
30
#include "theory/quantifiers/term_util.h"
31
#include "theory/rewriter.h"
32
#include "theory/strings/theory_strings_utils.h"
33
34
using namespace std;
35
using namespace CVC4::kind;
36
using namespace CVC4::context;
37
38
namespace CVC4 {
39
namespace theory {
40
namespace quantifiers {
41
42
/**
43
 * Attributes used for constructing bound variables in a canonical way. These
44
 * are attributes that map to bound variable, introduced for the following
45
 * purposes:
46
 * - QRewPrenexAttribute: cached on (v, body) where we are prenexing bound
47
 * variable v in a nested quantified formula within the given body.
48
 * - QRewMiniscopeAttribute: cached on (v, q, i) where q is being miniscoped
49
 * for F_i in its body (and F_1 ... F_n), and v is one of the bound variables
50
 * that q binds.
51
 * - QRewDtExpandAttribute: cached on
52
 */
53
struct QRewPrenexAttributeId
54
{
55
};
56
typedef expr::Attribute<QRewPrenexAttributeId, Node> QRewPrenexAttribute;
57
struct QRewMiniscopeAttributeId
58
{
59
};
60
typedef expr::Attribute<QRewMiniscopeAttributeId, Node> QRewMiniscopeAttribute;
61
struct QRewDtExpandAttributeId
62
{
63
};
64
typedef expr::Attribute<QRewDtExpandAttributeId, Node> QRewDtExpandAttribute;
65
66
std::ostream& operator<<(std::ostream& out, RewriteStep s)
67
{
68
  switch (s)
69
  {
70
    case COMPUTE_ELIM_SYMBOLS: out << "COMPUTE_ELIM_SYMBOLS"; break;
71
    case COMPUTE_MINISCOPING: out << "COMPUTE_MINISCOPING"; break;
72
    case COMPUTE_AGGRESSIVE_MINISCOPING:
73
      out << "COMPUTE_AGGRESSIVE_MINISCOPING";
74
      break;
75
    case COMPUTE_EXT_REWRITE: out << "COMPUTE_EXT_REWRITE"; break;
76
    case COMPUTE_PROCESS_TERMS: out << "COMPUTE_PROCESS_TERMS"; break;
77
    case COMPUTE_PRENEX: out << "COMPUTE_PRENEX"; break;
78
    case COMPUTE_VAR_ELIMINATION: out << "COMPUTE_VAR_ELIMINATION"; break;
79
    case COMPUTE_COND_SPLIT: out << "COMPUTE_COND_SPLIT"; break;
80
    default: out << "UnknownRewriteStep"; break;
81
  }
82
  return out;
83
}
84
85
14973
bool QuantifiersRewriter::isLiteral( Node n ){
86
14973
  switch( n.getKind() ){
87
  case NOT:
88
    return n[0].getKind()!=NOT && isLiteral( n[0] );
89
    break;
90
  case OR:
91
  case AND:
92
  case IMPLIES:
93
  case XOR:
94
  case ITE:
95
    return false;
96
    break;
97
8386
  case EQUAL:
98
    //for boolean terms
99
8386
    return !n[0].getType().isBoolean();
100
    break;
101
6587
  default:
102
6587
    break;
103
  }
104
6587
  return true;
105
}
106
107
void QuantifiersRewriter::addNodeToOrBuilder( Node n, NodeBuilder<>& t ){
108
  if( n.getKind()==OR ){
109
    for( int i=0; i<(int)n.getNumChildren(); i++ ){
110
      t << n[i];
111
    }
112
  }else{
113
    t << n;
114
  }
115
}
116
117
4328836
void QuantifiersRewriter::computeArgs(const std::vector<Node>& args,
118
                                      std::map<Node, bool>& activeMap,
119
                                      Node n,
120
                                      std::map<Node, bool>& visited)
121
{
122
4328836
  if( visited.find( n )==visited.end() ){
123
3092361
    visited[n] = true;
124
3092361
    if( n.getKind()==BOUND_VARIABLE ){
125
531961
      if( std::find( args.begin(), args.end(), n )!=args.end() ){
126
426383
        activeMap[ n ] = true;
127
      }
128
    }else{
129
2560400
      if (n.hasOperator())
130
      {
131
1358545
        computeArgs(args, activeMap, n.getOperator(), visited);
132
      }
133
5281431
      for( int i=0; i<(int)n.getNumChildren(); i++ ){
134
2721031
        computeArgs( args, activeMap, n[i], visited );
135
      }
136
    }
137
  }
138
4328836
}
139
140
133005
void QuantifiersRewriter::computeArgVec(const std::vector<Node>& args,
141
                                        std::vector<Node>& activeArgs,
142
                                        Node n)
143
{
144
133005
  Assert(activeArgs.empty());
145
266010
  std::map< Node, bool > activeMap;
146
266010
  std::map< Node, bool > visited;
147
133005
  computeArgs( args, activeMap, n, visited );
148
133005
  if( !activeMap.empty() ){
149
2354327
    for( unsigned i=0; i<args.size(); i++ ){
150
2222961
      if( activeMap.find( args[i] )!=activeMap.end() ){
151
312195
        activeArgs.push_back( args[i] );
152
      }
153
    }
154
  }
155
133005
}
156
157
58167
void QuantifiersRewriter::computeArgVec2(const std::vector<Node>& args,
158
                                         std::vector<Node>& activeArgs,
159
                                         Node n,
160
                                         Node ipl)
161
{
162
58167
  Assert(activeArgs.empty());
163
116334
  std::map< Node, bool > activeMap;
164
116334
  std::map< Node, bool > visited;
165
58167
  computeArgs( args, activeMap, n, visited );
166
58167
  if( !activeMap.empty() ){
167
    //collect variables in inst pattern list only if we cannot eliminate quantifier
168
58088
    computeArgs( args, activeMap, ipl, visited );
169
173229
    for( unsigned i=0; i<args.size(); i++ ){
170
115141
      if( activeMap.find( args[i] )!=activeMap.end() ){
171
114188
        activeArgs.push_back( args[i] );
172
      }
173
    }
174
  }
175
58167
}
176
177
129967
RewriteResponse QuantifiersRewriter::preRewrite(TNode in) {
178
129967
  if( in.getKind()==kind::EXISTS || in.getKind()==kind::FORALL ){
179
76650
    Trace("quantifiers-rewrite-debug") << "pre-rewriting " << in << std::endl;
180
151545
    std::vector< Node > args;
181
151545
    Node body = in;
182
76650
    bool doRewrite = false;
183
90904
    while( body.getNumChildren()==2 && body.getKind()==body[1].getKind() ){
184
14281
      for( unsigned i=0; i<body[0].getNumChildren(); i++ ){
185
7154
        args.push_back( body[0][i] );
186
      }
187
7127
      body = body[1];
188
7127
      doRewrite = true;
189
    }
190
76650
    if( doRewrite ){
191
3510
      std::vector< Node > children;
192
3525
      for( unsigned i=0; i<body[0].getNumChildren(); i++ ){
193
1770
        args.push_back( body[0][i] );
194
      }
195
1755
      children.push_back( NodeManager::currentNM()->mkNode(kind::BOUND_VAR_LIST,args) );
196
1755
      children.push_back( body[1] );
197
1755
      if( body.getNumChildren()==3 ){
198
32
        children.push_back( body[2] );
199
      }
200
3510
      Node n = NodeManager::currentNM()->mkNode( in.getKind(), children );
201
1755
      if( in!=n ){
202
1755
        Trace("quantifiers-pre-rewrite") << "*** pre-rewrite " << in << std::endl;
203
1755
        Trace("quantifiers-pre-rewrite") << " to " << std::endl;
204
1755
        Trace("quantifiers-pre-rewrite") << n << std::endl;
205
      }
206
1755
      return RewriteResponse(REWRITE_DONE, n);
207
    }
208
  }
209
128212
  return RewriteResponse(REWRITE_DONE, in);
210
}
211
212
237432
RewriteResponse QuantifiersRewriter::postRewrite(TNode in) {
213
237432
  Trace("quantifiers-rewrite-debug") << "post-rewriting " << in << std::endl;
214
237432
  RewriteStatus status = REWRITE_DONE;
215
474864
  Node ret = in;
216
237432
  RewriteStep rew_op = COMPUTE_LAST;
217
  //get the body
218
237432
  if( in.getKind()==EXISTS ){
219
6194
    std::vector< Node > children;
220
3097
    children.push_back( in[0] );
221
3097
    children.push_back( in[1].negate() );
222
3097
    if( in.getNumChildren()==3 ){
223
34
      children.push_back( in[2] );
224
    }
225
3097
    ret = NodeManager::currentNM()->mkNode( FORALL, children );
226
3097
    ret = ret.negate();
227
3097
    status = REWRITE_AGAIN_FULL;
228
234335
  }else if( in.getKind()==FORALL ){
229
128019
    if( in[1].isConst() && in.getNumChildren()==2 ){
230
634
      return RewriteResponse( status, in[1] );
231
    }else{
232
      //compute attributes
233
254770
      QAttributes qa;
234
127385
      QuantAttributes::computeQuantAttributes( in, qa );
235
1029855
      for (unsigned i = 0; i < COMPUTE_LAST; ++i)
236
      {
237
919447
        RewriteStep op = static_cast<RewriteStep>(i);
238
919447
        if( doOperation( in, op, qa ) ){
239
612999
          ret = computeOperation( in, op, qa );
240
612999
          if( ret!=in ){
241
16977
            rew_op = op;
242
16977
            status = REWRITE_AGAIN_FULL;
243
16977
            break;
244
          }
245
        }
246
      }
247
    }
248
  }
249
  //print if changed
250
236798
  if( in!=ret ){
251
20074
    Trace("quantifiers-rewrite") << "*** rewrite (op=" << rew_op << ") " << in << std::endl;
252
20074
    Trace("quantifiers-rewrite") << " to " << std::endl;
253
20074
    Trace("quantifiers-rewrite") << ret << std::endl;
254
  }
255
236798
  return RewriteResponse( status, ret );
256
}
257
258
709743
bool QuantifiersRewriter::addCheckElimChild( std::vector< Node >& children, Node c, Kind k, std::map< Node, bool >& lit_pol, bool& childrenChanged ){
259
1281337
  if( ( k==OR || k==AND ) && options::elimTautQuant() ){
260
1142983
    Node lit = c.getKind()==NOT ? c[0] : c;
261
571594
    bool pol = c.getKind()!=NOT;
262
571594
    std::map< Node, bool >::iterator it = lit_pol.find( lit );
263
571594
    if( it==lit_pol.end() ){
264
570761
      lit_pol[lit] = pol;
265
570761
      children.push_back( c );
266
    }else{
267
833
      childrenChanged = true;
268
833
      if( it->second!=pol ){
269
205
        return false;
270
      }
271
    }
272
  }else{
273
138149
    children.push_back( c );
274
  }
275
709538
  return true;
276
}
277
278
// eliminates IMPLIES/XOR, removes duplicates/infers tautologies of AND/OR, and computes NNF
279
823600
Node QuantifiersRewriter::computeElimSymbols( Node body ) {
280
823600
  Kind ok = body.getKind();
281
823600
  Kind k = ok;
282
823600
  bool negAllCh = false;
283
823600
  bool negCh1 = false;
284
823600
  if( ok==IMPLIES ){
285
11436
    k = OR;
286
11436
    negCh1 = true;
287
812164
  }else if( ok==XOR ){
288
596
    k = EQUAL;
289
596
    negCh1 = true;
290
811568
  }else if( ok==NOT ){
291
327961
    if( body[0].getKind()==NOT ){
292
      return computeElimSymbols( body[0][0] );
293
327961
    }else if( body[0].getKind()==OR || body[0].getKind()==IMPLIES ){
294
1573
      k = AND;
295
1573
      negAllCh = true;
296
1573
      negCh1 = body[0].getKind()==IMPLIES;
297
1573
      body = body[0];
298
326388
    }else if( body[0].getKind()==AND ){
299
5324
      k = OR;
300
5324
      negAllCh = true;
301
5324
      body = body[0];
302
321064
    }else if( body[0].getKind()==XOR || ( body[0].getKind()==EQUAL && body[0][0].getType().isBoolean() ) ){
303
2773
      k = EQUAL;
304
2773
      negCh1 = ( body[0].getKind()==EQUAL );
305
2773
      body = body[0];
306
318291
    }else if( body[0].getKind()==ITE ){
307
77
      k = body[0].getKind();
308
77
      negAllCh = true;
309
77
      negCh1 = true;
310
77
      body = body[0];
311
    }else{
312
318214
      return body;
313
    }
314
483607
  }else if( ( ok!=EQUAL || !body[0].getType().isBoolean() ) && ok!=ITE && ok!=AND && ok!=OR ){
315
    //a literal
316
291280
    return body;
317
  }
318
214106
  bool childrenChanged = false;
319
428212
  std::vector< Node > children;
320
428212
  std::map< Node, bool > lit_pol;
321
910116
  for( unsigned i=0; i<body.getNumChildren(); i++ ){
322
1392225
    Node c = computeElimSymbols( ( i==0 && negCh1 )!=negAllCh ? body[i].negate() : body[i] );
323
696215
    bool success = true;
324
696215
    if( c.getKind()==k && ( k==OR || k==AND ) ){
325
      //flatten
326
5060
      childrenChanged = true;
327
23647
      for( unsigned j=0; j<c.getNumChildren(); j++ ){
328
18588
        if( !addCheckElimChild( children, c[j], k, lit_pol, childrenChanged ) ){
329
1
          success = false;
330
1
          break;
331
        }
332
      }
333
    }else{
334
691155
      success = addCheckElimChild( children, c, k, lit_pol, childrenChanged );
335
    }
336
696215
    if( !success ){
337
      // tautology
338
205
      Assert(k == OR || k == AND);
339
205
      return NodeManager::currentNM()->mkConst( k==OR );
340
    }
341
696010
    childrenChanged = childrenChanged || c!=body[i];
342
  }
343
213901
  if( childrenChanged || k!=ok ){
344
24898
    return ( children.size()==1 && k!=NOT ) ? children[0] : NodeManager::currentNM()->mkNode( k, children );
345
  }else{
346
189003
    return body;
347
  }
348
}
349
350
void QuantifiersRewriter::computeDtTesterIteSplit( Node n, std::map< Node, Node >& pcons, std::map< Node, std::map< int, Node > >& ncons,
351
                                                   std::vector< Node >& conj ){
352
  if( n.getKind()==ITE && n[0].getKind()==APPLY_TESTER && n[1].getType().isBoolean() ){
353
    Trace("quantifiers-rewrite-ite-debug") << "Split tester condition : " << n << std::endl;
354
    Node x = n[0][0];
355
    std::map< Node, Node >::iterator itp = pcons.find( x );
356
    if( itp!=pcons.end() ){
357
      Trace("quantifiers-rewrite-ite-debug") << "...condition already set " << itp->second << std::endl;
358
      computeDtTesterIteSplit( n[ itp->second==n[0] ? 1 : 2 ], pcons, ncons, conj );
359
    }else{
360
      Node tester = n[0].getOperator();
361
      int index = datatypes::utils::indexOf(tester);
362
      std::map< int, Node >::iterator itn = ncons[x].find( index );
363
      if( itn!=ncons[x].end() ){
364
        Trace("quantifiers-rewrite-ite-debug") << "...condition negated " << itn->second << std::endl;
365
        computeDtTesterIteSplit( n[ 2 ], pcons, ncons, conj );
366
      }else{
367
        for( unsigned i=0; i<2; i++ ){
368
          if( i==0 ){
369
            pcons[x] = n[0];
370
          }else{
371
            pcons.erase( x );
372
            ncons[x][index] = n[0].negate();
373
          }
374
          computeDtTesterIteSplit( n[i+1], pcons, ncons, conj );
375
        }
376
        ncons[x].erase( index );
377
      }
378
    }
379
  }else{
380
    NodeManager* nm = NodeManager::currentNM();
381
    Trace("quantifiers-rewrite-ite-debug") << "Return value : " << n << std::endl;
382
    std::vector< Node > children;
383
    children.push_back( n );
384
    std::vector< Node > vars;
385
    //add all positive testers
386
    for( std::map< Node, Node >::iterator it = pcons.begin(); it != pcons.end(); ++it ){
387
      children.push_back( it->second.negate() );
388
      vars.push_back( it->first );
389
    }
390
    //add all negative testers
391
    for( std::map< Node, std::map< int, Node > >::iterator it = ncons.begin(); it != ncons.end(); ++it ){
392
      Node x = it->first;
393
      //only if we haven't settled on a positive tester
394
      if( std::find( vars.begin(), vars.end(), x )==vars.end() ){
395
        //check if we have exhausted all options but one
396
        const DType& dt = x.getType().getDType();
397
        std::vector< Node > nchildren;
398
        int pos_cons = -1;
399
        for( int i=0; i<(int)dt.getNumConstructors(); i++ ){
400
          std::map< int, Node >::iterator itt = it->second.find( i );
401
          if( itt==it->second.end() ){
402
            pos_cons = pos_cons==-1 ? i : -2;
403
          }else{
404
            nchildren.push_back( itt->second.negate() );
405
          }
406
        }
407
        if( pos_cons>=0 ){
408
          Node tester = dt[pos_cons].getTester();
409
          children.push_back(nm->mkNode(APPLY_TESTER, tester, x).negate());
410
        }else{
411
          children.insert( children.end(), nchildren.begin(), nchildren.end() );
412
        }
413
      }
414
    }
415
    //make condition/output pair
416
    Node c = children.size()==1 ? children[0] : NodeManager::currentNM()->mkNode( OR, children );
417
    conj.push_back( c );
418
  }
419
}
420
421
97332
Node QuantifiersRewriter::computeProcessTerms( Node body, std::vector< Node >& new_vars, std::vector< Node >& new_conds, Node q, QAttributes& qa ){
422
194664
  std::map< Node, Node > cache;
423
97332
  if( qa.isFunDef() ){
424
    Node h = QuantAttributes::getFunDefHead( q );
425
    Assert(!h.isNull());
426
    // if it is a function definition, rewrite the body independently
427
    Node fbody = QuantAttributes::getFunDefBody( q );
428
    Trace("quantifiers-rewrite-debug") << "Decompose " << h << " / " << fbody << " as function definition for " << q << "." << std::endl;
429
    if (!fbody.isNull())
430
    {
431
      Node r = computeProcessTerms2(fbody, cache, new_vars, new_conds);
432
      Assert(new_vars.size() == h.getNumChildren());
433
      return Rewriter::rewrite(NodeManager::currentNM()->mkNode(EQUAL, h, r));
434
    }
435
    // It can happen that we can't infer the shape of the function definition,
436
    // for example: forall xy. f( x, y ) = 1 + f( x, y ), this is rewritten to
437
    // forall xy. false.
438
  }
439
97332
  return computeProcessTerms2(body, cache, new_vars, new_conds);
440
}
441
442
2573924
Node QuantifiersRewriter::computeProcessTerms2(Node body,
443
                                               std::map<Node, Node>& cache,
444
                                               std::vector<Node>& new_vars,
445
                                               std::vector<Node>& new_conds)
446
{
447
2573924
  NodeManager* nm = NodeManager::currentNM();
448
5147848
  Trace("quantifiers-rewrite-term-debug2")
449
2573924
      << "computeProcessTerms " << body << std::endl;
450
2573924
  std::map< Node, Node >::iterator iti = cache.find( body );
451
2573924
  if( iti!=cache.end() ){
452
825152
    return iti->second;
453
  }
454
1748772
  bool changed = false;
455
3497544
  std::vector<Node> children;
456
4225364
  for (size_t i = 0; i < body.getNumChildren(); i++)
457
  {
458
    // do the recursive call on children
459
4953184
    Node nn = computeProcessTerms2(body[i], cache, new_vars, new_conds);
460
2476592
    children.push_back(nn);
461
2476592
    changed = changed || nn != body[i];
462
  }
463
464
  // make return value
465
3497544
  Node ret;
466
1748772
  if (changed)
467
  {
468
4352
    if (body.getMetaKind() == kind::metakind::PARAMETERIZED)
469
    {
470
172
      children.insert(children.begin(), body.getOperator());
471
    }
472
4352
    ret = nm->mkNode(body.getKind(), children);
473
  }
474
  else
475
  {
476
1744420
    ret = body;
477
  }
478
479
3497544
  Trace("quantifiers-rewrite-term-debug2")
480
1748772
      << "Returning " << ret << " for " << body << std::endl;
481
  // do context-independent rewriting
482
3497544
  if (ret.getKind() == EQUAL
483
1748772
      && options::iteLiftQuant() != options::IteLiftQuantMode::NONE)
484
  {
485
571536
    for (size_t i = 0; i < 2; i++)
486
    {
487
381183
      if (ret[i].getKind() == ITE)
488
      {
489
23992
        Node no = i == 0 ? ret[1] : ret[0];
490
12196
        if (no.getKind() != ITE)
491
        {
492
          bool doRewrite =
493
11068
              options::iteLiftQuant() == options::IteLiftQuantMode::ALL;
494
21736
          std::vector<Node> childrenIte;
495
11068
          childrenIte.push_back(ret[i][0]);
496
33204
          for (size_t j = 1; j <= 2; j++)
497
          {
498
            // check if it rewrites to a constant
499
44272
            Node nn = nm->mkNode(EQUAL, no, ret[i][j]);
500
22136
            nn = Rewriter::rewrite(nn);
501
22136
            childrenIte.push_back(nn);
502
22136
            if (nn.isConst())
503
            {
504
570
              doRewrite = true;
505
            }
506
          }
507
11068
          if (doRewrite)
508
          {
509
400
            ret = nm->mkNode(ITE, childrenIte);
510
400
            break;
511
          }
512
        }
513
      }
514
    }
515
  }
516
1558019
  else if (ret.getKind() == SELECT && ret[0].getKind() == STORE)
517
  {
518
94
    Node st = ret[0];
519
94
    Node index = ret[1];
520
94
    std::vector<Node> iconds;
521
94
    std::vector<Node> elements;
522
399
    while (st.getKind() == STORE)
523
    {
524
176
      iconds.push_back(index.eqNode(st[1]));
525
176
      elements.push_back(st[2]);
526
176
      st = st[0];
527
    }
528
47
    ret = nm->mkNode(SELECT, st, index);
529
    // conditions
530
223
    for (int i = (iconds.size() - 1); i >= 0; i--)
531
    {
532
176
      ret = nm->mkNode(ITE, iconds[i], elements[i], ret);
533
    }
534
  }
535
1748772
  cache[body] = ret;
536
1748772
  return ret;
537
}
538
539
29
Node QuantifiersRewriter::computeExtendedRewrite(Node q)
540
{
541
58
  Node body = q[1];
542
  // apply extended rewriter
543
58
  ExtendedRewriter er;
544
58
  Node bodyr = er.extendedRewrite(body);
545
29
  if (body != bodyr)
546
  {
547
22
    std::vector<Node> children;
548
11
    children.push_back(q[0]);
549
11
    children.push_back(bodyr);
550
11
    if (q.getNumChildren() == 3)
551
    {
552
      children.push_back(q[2]);
553
    }
554
11
    return NodeManager::currentNM()->mkNode(FORALL, children);
555
  }
556
18
  return q;
557
}
558
559
97113
Node QuantifiersRewriter::computeCondSplit(Node body,
560
                                           const std::vector<Node>& args,
561
                                           QAttributes& qa)
562
{
563
97113
  NodeManager* nm = NodeManager::currentNM();
564
97113
  Kind bk = body.getKind();
565
194536
  if (options::iteDtTesterSplitQuant() && bk == ITE
566
194234
      && body[0].getKind() == APPLY_TESTER)
567
  {
568
    Trace("quantifiers-rewrite-ite-debug") << "DTT split : " << body << std::endl;
569
    std::map< Node, Node > pcons;
570
    std::map< Node, std::map< int, Node > > ncons;
571
    std::vector< Node > conj;
572
    computeDtTesterIteSplit( body, pcons, ncons, conj );
573
    Assert(!conj.empty());
574
    if( conj.size()>1 ){
575
      Trace("quantifiers-rewrite-ite") << "*** Split ITE (datatype tester) " << body << " into : " << std::endl;
576
      for( unsigned i=0; i<conj.size(); i++ ){
577
        Trace("quantifiers-rewrite-ite") << "   " << conj[i] << std::endl;
578
      }
579
      return nm->mkNode(AND, conj);
580
    }
581
  }
582
304477
  if (!options::condVarSplitQuant())
583
  {
584
    return body;
585
  }
586
194226
  Trace("cond-var-split-debug")
587
97113
      << "Conditional var elim split " << body << "?" << std::endl;
588
589
97113
  if (bk == ITE
590
97231
      || (bk == EQUAL && body[0].getType().isBoolean()
591
39493
          && options::condVarSplitQuantAgg()))
592
  {
593
118
    Assert(!qa.isFunDef());
594
118
    bool do_split = false;
595
118
    unsigned index_max = bk == ITE ? 0 : 1;
596
220
    std::vector<Node> tmpArgs = args;
597
220
    for (unsigned index = 0; index <= index_max; index++)
598
    {
599
354
      if (hasVarElim(body[index], true, tmpArgs)
600
354
          || hasVarElim(body[index], false, tmpArgs))
601
      {
602
16
        do_split = true;
603
16
        break;
604
      }
605
    }
606
118
    if (do_split)
607
    {
608
32
      Node pos;
609
32
      Node neg;
610
16
      if (bk == ITE)
611
      {
612
16
        pos = nm->mkNode(OR, body[0].negate(), body[1]);
613
16
        neg = nm->mkNode(OR, body[0], body[2]);
614
      }
615
      else
616
      {
617
        pos = nm->mkNode(OR, body[0].negate(), body[1]);
618
        neg = nm->mkNode(OR, body[0], body[1].negate());
619
      }
620
32
      Trace("cond-var-split-debug") << "*** Split (conditional variable eq) "
621
16
                                    << body << " into : " << std::endl;
622
16
      Trace("cond-var-split-debug") << "   " << pos << std::endl;
623
16
      Trace("cond-var-split-debug") << "   " << neg << std::endl;
624
16
      return nm->mkNode(AND, pos, neg);
625
    }
626
  }
627
628
97097
  if (bk == OR)
629
  {
630
39101
    unsigned size = body.getNumChildren();
631
39101
    bool do_split = false;
632
39101
    unsigned split_index = 0;
633
160148
    for (unsigned i = 0; i < size; i++)
634
    {
635
      // check if this child is a (conditional) variable elimination
636
242231
      Node b = body[i];
637
121184
      if (b.getKind() == AND)
638
      {
639
13086
        std::vector<Node> vars;
640
13086
        std::vector<Node> subs;
641
13086
        std::vector<Node> tmpArgs = args;
642
25657
        for (unsigned j = 0, bsize = b.getNumChildren(); j < bsize; j++)
643
        {
644
19251
          if (getVarElimLit(b[j], false, tmpArgs, vars, subs))
645
          {
646
4962
            Trace("cond-var-split-debug") << "Variable elimination in child #"
647
2481
                                          << j << " under " << i << std::endl;
648
            // Figure out if we should split
649
            // Currently we split if the aggressive option is set, or
650
            // if the top-level OR is binary.
651
2481
            if (options::condVarSplitQuantAgg() || size == 2)
652
            {
653
137
              do_split = true;
654
            }
655
            // other splitting criteria go here
656
657
2481
            if (do_split)
658
            {
659
137
              split_index = i;
660
137
              break;
661
            }
662
2344
            vars.clear();
663
2344
            subs.clear();
664
2344
            tmpArgs = args;
665
          }
666
        }
667
      }
668
121184
      if (do_split)
669
      {
670
137
        break;
671
      }
672
    }
673
39101
    if (do_split)
674
    {
675
274
      std::vector<Node> children;
676
411
      for (TNode bc : body)
677
      {
678
274
        children.push_back(bc);
679
      }
680
274
      std::vector<Node> split_children;
681
551
      for (TNode bci : body[split_index])
682
      {
683
414
        children[split_index] = bci;
684
414
        split_children.push_back(nm->mkNode(OR, children));
685
      }
686
      // split the AND child, for example:
687
      //  ( x!=a ^ P(x) ) V Q(x) ---> ( x!=a V Q(x) ) ^ ( P(x) V Q(x) )
688
137
      return nm->mkNode(AND, split_children);
689
    }
690
  }
691
692
96960
  return body;
693
}
694
695
6089
bool QuantifiersRewriter::isVarElim(Node v, Node s)
696
{
697
6089
  Assert(v.getKind() == BOUND_VARIABLE);
698
6089
  return !expr::hasSubterm(s, v) && s.getType().isSubtypeOf(v.getType());
699
}
700
701
707
Node QuantifiersRewriter::getVarElimLitBv(Node lit,
702
                                          const std::vector<Node>& args,
703
                                          Node& var)
704
{
705
707
  if (Trace.isOn("quant-velim-bv"))
706
  {
707
    Trace("quant-velim-bv") << "Bv-Elim : " << lit << " varList = { ";
708
    for (const Node& v : args)
709
    {
710
      Trace("quant-velim-bv") << v << " ";
711
    }
712
    Trace("quant-velim-bv") << "} ?" << std::endl;
713
  }
714
707
  Assert(lit.getKind() == EQUAL);
715
  // TODO (#1494) : linearize the literal using utility
716
717
  // compute a subset active_args of the bound variables args that occur in lit
718
1414
  std::vector<Node> active_args;
719
707
  computeArgVec(args, active_args, lit);
720
721
1414
  BvInverter binv;
722
1512
  for (const Node& cvar : active_args)
723
  {
724
    // solve for the variable on this path using the inverter
725
1650
    std::vector<unsigned> path;
726
1650
    Node slit = binv.getPathToPv(lit, cvar, path);
727
845
    if (!slit.isNull())
728
    {
729
812
      Node slv = binv.solveBvLit(cvar, lit, path, nullptr);
730
426
      Trace("quant-velim-bv") << "...solution : " << slv << std::endl;
731
426
      if (!slv.isNull())
732
      {
733
76
        var = cvar;
734
        // if this is a proper variable elimination, that is, var = slv where
735
        // var is not in the free variables of slv, then we can return this
736
        // as the variable elimination for lit.
737
76
        if (isVarElim(var, slv))
738
        {
739
40
          return slv;
740
        }
741
      }
742
    }
743
    else
744
    {
745
419
      Trace("quant-velim-bv") << "...non-invertible path." << std::endl;
746
    }
747
  }
748
749
667
  return Node::null();
750
}
751
752
334
Node QuantifiersRewriter::getVarElimLitString(Node lit,
753
                                              const std::vector<Node>& args,
754
                                              Node& var)
755
{
756
334
  Assert(lit.getKind() == EQUAL);
757
334
  NodeManager* nm = NodeManager::currentNM();
758
998
  for (unsigned i = 0; i < 2; i++)
759
  {
760
668
    if (lit[i].getKind() == STRING_CONCAT)
761
    {
762
12
      TypeNode stype = lit[i].getType();
763
20
      for (unsigned j = 0, nchildren = lit[i].getNumChildren(); j < nchildren;
764
           j++)
765
      {
766
16
        if (std::find(args.begin(), args.end(), lit[i][j]) != args.end())
767
        {
768
12
          var = lit[i][j];
769
20
          Node slv = lit[1 - i];
770
20
          std::vector<Node> preL(lit[i].begin(), lit[i].begin() + j);
771
20
          std::vector<Node> postL(lit[i].begin() + j + 1, lit[i].end());
772
20
          Node tpre = strings::utils::mkConcat(preL, stype);
773
20
          Node tpost = strings::utils::mkConcat(postL, stype);
774
20
          Node slvL = nm->mkNode(STRING_LENGTH, slv);
775
20
          Node tpreL = nm->mkNode(STRING_LENGTH, tpre);
776
20
          Node tpostL = nm->mkNode(STRING_LENGTH, tpost);
777
12
          slv = nm->mkNode(
778
              STRING_SUBSTR,
779
              slv,
780
              tpreL,
781
24
              nm->mkNode(MINUS, slvL, nm->mkNode(PLUS, tpreL, tpostL)));
782
          // forall x. r ++ x ++ t = s => P( x )
783
          //   is equivalent to
784
          // r ++ s' ++ t = s => P( s' ) where
785
          // s' = substr( s, |r|, |s|-(|t|+|r|) ).
786
          // We apply this only if r,t,s do not contain free variables.
787
12
          if (!expr::hasFreeVar(slv))
788
          {
789
4
            return slv;
790
          }
791
        }
792
      }
793
    }
794
  }
795
796
330
  return Node::null();
797
}
798
799
208061
bool QuantifiersRewriter::getVarElimLit(Node lit,
800
                                        bool pol,
801
                                        std::vector<Node>& args,
802
                                        std::vector<Node>& vars,
803
                                        std::vector<Node>& subs)
804
{
805
208061
  if (lit.getKind() == NOT)
806
  {
807
5745
    lit = lit[0];
808
5745
    pol = !pol;
809
5745
    Assert(lit.getKind() != NOT);
810
  }
811
208061
  NodeManager* nm = NodeManager::currentNM();
812
416122
  Trace("var-elim-quant-debug")
813
208061
      << "Eliminate : " << lit << ", pol = " << pol << "?" << std::endl;
814
416734
  if (lit.getKind() == APPLY_TESTER && pol && lit[0].getKind() == BOUND_VARIABLE
815
416190
      && options::dtVarExpandQuant())
816
  {
817
68
    Trace("var-elim-dt") << "Expand datatype variable based on : " << lit
818
34
                         << std::endl;
819
    std::vector<Node>::iterator ita =
820
34
        std::find(args.begin(), args.end(), lit[0]);
821
34
    if (ita != args.end())
822
    {
823
34
      vars.push_back(lit[0]);
824
68
      Node tester = lit.getOperator();
825
34
      int index = datatypes::utils::indexOf(tester);
826
34
      const DType& dt = datatypes::utils::datatypeOf(tester);
827
34
      const DTypeConstructor& c = dt[index];
828
68
      std::vector<Node> newChildren;
829
34
      newChildren.push_back(c.getConstructor());
830
68
      std::vector<Node> newVars;
831
89
      for (unsigned j = 0, nargs = c.getNumArgs(); j < nargs; j++)
832
      {
833
110
        TypeNode tn = c[j].getRangeType();
834
110
        Node v = nm->mkBoundVar(tn);
835
55
        newChildren.push_back(v);
836
55
        newVars.push_back(v);
837
      }
838
34
      subs.push_back(nm->mkNode(APPLY_CONSTRUCTOR, newChildren));
839
68
      Trace("var-elim-dt") << "...apply substitution " << subs[0] << "/"
840
34
                           << vars[0] << std::endl;
841
34
      args.erase(ita);
842
34
      args.insert(args.end(), newVars.begin(), newVars.end());
843
34
      return true;
844
    }
845
  }
846
  // all eliminations below guarded by varElimQuant()
847
725558
  if (!options::varElimQuant())
848
  {
849
    return false;
850
  }
851
852
208027
  if (lit.getKind() == EQUAL)
853
  {
854
107789
    if (pol || lit[0].getType().isBoolean())
855
    {
856
159426
      for (unsigned i = 0; i < 2; i++)
857
      {
858
108419
        bool tpol = pol;
859
211391
        Node v_slv = lit[i];
860
108419
        if (v_slv.getKind() == NOT)
861
        {
862
4640
          v_slv = v_slv[0];
863
4640
          tpol = !tpol;
864
        }
865
        std::vector<Node>::iterator ita =
866
108419
            std::find(args.begin(), args.end(), v_slv);
867
108419
        if (ita != args.end())
868
        {
869
5744
          if (isVarElim(v_slv, lit[1 - i]))
870
          {
871
10894
            Node slv = lit[1 - i];
872
5447
            if (!tpol)
873
            {
874
85
              Assert(slv.getType().isBoolean());
875
85
              slv = slv.negate();
876
            }
877
10894
            Trace("var-elim-quant")
878
5447
                << "Variable eliminate based on equality : " << v_slv << " -> "
879
5447
                << slv << std::endl;
880
5447
            vars.push_back(v_slv);
881
5447
            subs.push_back(slv);
882
5447
            args.erase(ita);
883
5447
            return true;
884
          }
885
        }
886
      }
887
    }
888
  }
889
202580
  if (lit.getKind() == BOUND_VARIABLE)
890
  {
891
1472
    std::vector< Node >::iterator ita = std::find( args.begin(), args.end(), lit );
892
1472
    if( ita!=args.end() ){
893
1470
      Trace("var-elim-bool") << "Variable eliminate : " << lit << std::endl;
894
1470
      vars.push_back( lit );
895
1470
      subs.push_back( NodeManager::currentNM()->mkConst( pol ) );
896
1470
      args.erase( ita );
897
1470
      return true;
898
    }
899
  }
900
201110
  if (lit.getKind() == EQUAL && lit[0].getType().isReal() && pol)
901
  {
902
    // for arithmetic, solve the equality
903
19515
    std::map< Node, Node > msum;
904
9866
    if (ArithMSum::getMonomialSumLit(lit, msum))
905
    {
906
30250
      for( std::map< Node, Node >::iterator itm = msum.begin(); itm != msum.end(); ++itm ){
907
20601
        if( !itm->first.isNull() ){
908
17705
          std::vector< Node >::iterator ita = std::find( args.begin(), args.end(), itm->first );
909
17705
          if( ita!=args.end() ){
910
529
            Assert(pol);
911
841
            Node veq_c;
912
841
            Node val;
913
529
            int ires = ArithMSum::isolate(itm->first, msum, veq_c, val, EQUAL);
914
529
            if (ires != 0 && veq_c.isNull() && isVarElim(itm->first, val))
915
            {
916
434
              Trace("var-elim-quant")
917
217
                  << "Variable eliminate based on solved equality : "
918
217
                  << itm->first << " -> " << val << std::endl;
919
217
              vars.push_back(itm->first);
920
217
              subs.push_back(val);
921
217
              args.erase(ita);
922
217
              return true;
923
            }
924
          }
925
        }
926
      }
927
    }
928
  }
929
200893
  if (lit.getKind() == EQUAL && pol)
930
  {
931
62874
    Node var;
932
62874
    Node slv;
933
62874
    TypeNode tt = lit[0].getType();
934
31459
    if (tt.isBitVector())
935
    {
936
707
      slv = getVarElimLitBv(lit, args, var);
937
    }
938
30752
    else if (tt.isStringLike())
939
    {
940
334
      slv = getVarElimLitString(lit, args, var);
941
    }
942
31459
    if (!slv.isNull())
943
    {
944
44
      Assert(!var.isNull());
945
      std::vector<Node>::iterator ita =
946
44
          std::find(args.begin(), args.end(), var);
947
44
      Assert(ita != args.end());
948
88
      Trace("var-elim-quant")
949
44
          << "Variable eliminate based on theory-specific solving : " << var
950
44
          << " -> " << slv << std::endl;
951
44
      Assert(!expr::hasSubterm(slv, var));
952
44
      Assert(slv.getType().isSubtypeOf(var.getType()));
953
44
      vars.push_back(var);
954
44
      subs.push_back(slv);
955
44
      args.erase(ita);
956
44
      return true;
957
    }
958
  }
959
200849
  return false;
960
}
961
962
233046
bool QuantifiersRewriter::getVarElim(Node n,
963
                                     bool pol,
964
                                     std::vector<Node>& args,
965
                                     std::vector<Node>& vars,
966
                                     std::vector<Node>& subs)
967
{
968
233046
  Kind nk = n.getKind();
969
233046
  if (nk == NOT)
970
  {
971
86174
    n = n[0];
972
86174
    pol = !pol;
973
86174
    nk = n.getKind();
974
86174
    Assert(nk != NOT);
975
  }
976
233046
  if ((nk == AND && pol) || (nk == OR && !pol))
977
  {
978
171680
    for (const Node& cn : n)
979
    {
980
131889
      if (getVarElim(cn, pol, args, vars, subs))
981
      {
982
4445
        return true;
983
      }
984
    }
985
39791
    return false;
986
  }
987
188810
  return getVarElimLit(n, pol, args, vars, subs);
988
}
989
990
220
bool QuantifiersRewriter::hasVarElim(Node n, bool pol, std::vector<Node>& args)
991
{
992
440
  std::vector< Node > vars;
993
440
  std::vector< Node > subs;
994
440
  return getVarElim(n, pol, args, vars, subs);
995
}
996
997
96075
bool QuantifiersRewriter::getVarElimIneq(Node body,
998
                                         std::vector<Node>& args,
999
                                         std::vector<Node>& bounds,
1000
                                         std::vector<Node>& subs,
1001
                                         QAttributes& qa)
1002
{
1003
  // elimination based on inequalities
1004
192150
  std::map<Node, std::map<bool, std::map<Node, bool> > > num_bounds;
1005
192150
  QuantPhaseReq qpr(body);
1006
268186
  for (const std::pair<const Node, bool>& pr : qpr.d_phase_reqs)
1007
  {
1008
    // an inequality that is entailed with a given polarity
1009
192698
    Node lit = pr.first;
1010
172111
    if (lit.getKind() != GEQ)
1011
    {
1012
151524
      continue;
1013
    }
1014
20587
    bool pol = pr.second;
1015
41174
    Trace("var-elim-quant-debug") << "Process inequality bounds : " << lit
1016
20587
                                  << ", pol = " << pol << "..." << std::endl;
1017
    // solve the inequality
1018
41174
    std::map<Node, Node> msum;
1019
20587
    if (!ArithMSum::getMonomialSumLit(lit, msum))
1020
    {
1021
      // not an inequality, cannot use
1022
      continue;
1023
    }
1024
66194
    for (const std::pair<const Node, Node>& m : msum)
1025
    {
1026
45607
      if (!m.first.isNull())
1027
      {
1028
        std::vector<Node>::iterator ita =
1029
33558
            std::find(args.begin(), args.end(), m.first);
1030
33558
        if (ita != args.end())
1031
        {
1032
          // store that this literal is upper/lower bound for itm->first
1033
43454
          Node veq_c;
1034
43454
          Node val;
1035
          int ires =
1036
21727
              ArithMSum::isolate(m.first, msum, veq_c, val, lit.getKind());
1037
21727
          if (ires != 0 && veq_c.isNull())
1038
          {
1039
21289
            bool is_upper = pol != (ires == 1);
1040
42578
            Trace("var-elim-ineq-debug")
1041
21289
                << lit << " is a " << (is_upper ? "upper" : "lower")
1042
21289
                << " bound for " << m.first << std::endl;
1043
42578
            Trace("var-elim-ineq-debug")
1044
21289
                << "  pol/ires = " << pol << " " << ires << std::endl;
1045
21289
            num_bounds[m.first][is_upper][lit] = pol;
1046
          }
1047
          else
1048
          {
1049
876
            Trace("var-elim-ineq-debug")
1050
438
                << "...ineligible " << m.first
1051
438
                << " since it cannot be solved for (" << ires << ", " << veq_c
1052
438
                << ")." << std::endl;
1053
438
            num_bounds[m.first][true].clear();
1054
438
            num_bounds[m.first][false].clear();
1055
          }
1056
        }
1057
        else
1058
        {
1059
          // compute variables in itm->first, these are not eligible for
1060
          // elimination
1061
23662
          std::unordered_set<Node, NodeHashFunction> fvs;
1062
11831
          expr::getFreeVariables(m.first, fvs);
1063
22287
          for (const Node& v : fvs)
1064
          {
1065
20912
            Trace("var-elim-ineq-debug")
1066
10456
                << "...ineligible " << v
1067
10456
                << " since it is contained in monomial." << std::endl;
1068
10456
            num_bounds[v][true].clear();
1069
10456
            num_bounds[v][false].clear();
1070
          }
1071
        }
1072
      }
1073
    }
1074
  }
1075
1076
  // collect all variables that have only upper/lower bounds
1077
192150
  std::map<Node, bool> elig_vars;
1078
18995
  for (const std::pair<const Node, std::map<bool, std::map<Node, bool> > >& nb :
1079
96075
       num_bounds)
1080
  {
1081
18995
    if (nb.second.find(true) == nb.second.end())
1082
    {
1083
5398
      Trace("var-elim-ineq-debug")
1084
2699
          << "Variable " << nb.first << " has only lower bounds." << std::endl;
1085
2699
      elig_vars[nb.first] = false;
1086
    }
1087
16296
    else if (nb.second.find(false) == nb.second.end())
1088
    {
1089
4034
      Trace("var-elim-ineq-debug")
1090
2017
          << "Variable " << nb.first << " has only upper bounds." << std::endl;
1091
2017
      elig_vars[nb.first] = true;
1092
    }
1093
  }
1094
96075
  if (elig_vars.empty())
1095
  {
1096
92506
    return false;
1097
  }
1098
7138
  std::vector<Node> inactive_vars;
1099
7138
  std::map<Node, std::map<int, bool> > visited;
1100
7138
  std::map<Node, int> exclude;
1101
13835
  for (const std::pair<const Node, bool>& pr : qpr.d_phase_reqs)
1102
  {
1103
10266
    if (pr.first.getKind() == GEQ)
1104
    {
1105
6374
      exclude[pr.first] = pr.second ? -1 : 1;
1106
12748
      Trace("var-elim-ineq-debug")
1107
6374
          << "...exclude " << pr.first << " at polarity " << exclude[pr.first]
1108
6374
          << std::endl;
1109
    }
1110
  }
1111
  // traverse the body, invalidate variables if they occur in places other than
1112
  // the bounds they occur in
1113
  std::unordered_map<TNode, std::unordered_set<int>, TNodeHashFunction>
1114
7138
      evisited;
1115
7138
  std::vector<TNode> evisit;
1116
7138
  std::vector<int> evisit_pol;
1117
7138
  TNode ecur;
1118
  int ecur_pol;
1119
3569
  evisit.push_back(body);
1120
3569
  evisit_pol.push_back(1);
1121
3569
  if (!qa.d_ipl.isNull())
1122
  {
1123
    // do not eliminate variables that occur in the annotation
1124
    evisit.push_back(qa.d_ipl);
1125
    evisit_pol.push_back(0);
1126
  }
1127
36309
  do
1128
  {
1129
39878
    ecur = evisit.back();
1130
39878
    evisit.pop_back();
1131
39878
    ecur_pol = evisit_pol.back();
1132
39878
    evisit_pol.pop_back();
1133
39878
    std::unordered_set<int>& epp = evisited[ecur];
1134
39878
    if (epp.find(ecur_pol) == epp.end())
1135
    {
1136
37584
      epp.insert(ecur_pol);
1137
37584
      if (elig_vars.find(ecur) != elig_vars.end())
1138
      {
1139
        // variable contained in a place apart from bounds, no longer eligible
1140
        // for elimination
1141
4160
        elig_vars.erase(ecur);
1142
8320
        Trace("var-elim-ineq-debug") << "...found occurrence of " << ecur
1143
4160
                                     << ", mark ineligible" << std::endl;
1144
      }
1145
      else
1146
      {
1147
33424
        bool rec = true;
1148
33424
        bool pol = ecur_pol >= 0;
1149
33424
        bool hasPol = ecur_pol != 0;
1150
33424
        if (hasPol)
1151
        {
1152
16966
          std::map<Node, int>::iterator itx = exclude.find(ecur);
1153
16966
          if (itx != exclude.end() && itx->second == ecur_pol)
1154
          {
1155
            // already processed this literal as a bound
1156
3471
            rec = false;
1157
          }
1158
        }
1159
33424
        if (rec)
1160
        {
1161
78229
          for (unsigned j = 0, size = ecur.getNumChildren(); j < size; j++)
1162
          {
1163
            bool newHasPol;
1164
            bool newPol;
1165
48276
            QuantPhaseReq::getPolarity(ecur, j, hasPol, pol, newHasPol, newPol);
1166
48276
            evisit.push_back(ecur[j]);
1167
48276
            evisit_pol.push_back(newHasPol ? (newPol ? 1 : -1) : 0);
1168
          }
1169
        }
1170
      }
1171
    }
1172
39878
  } while (!evisit.empty() && !elig_vars.empty());
1173
1174
3569
  bool ret = false;
1175
4125
  for (const std::pair<const Node, bool>& ev : elig_vars)
1176
  {
1177
1112
    Node v = ev.first;
1178
1112
    Trace("var-elim-ineq-debug")
1179
556
        << v << " is eligible for elimination." << std::endl;
1180
    // do substitution corresponding to infinite projection, all literals
1181
    // involving unbounded variable go to true/false
1182
1283
    for (const std::pair<const Node, bool>& nb : num_bounds[v][elig_vars[v]])
1183
    {
1184
1454
      Trace("var-elim-ineq-debug")
1185
727
          << "  subs : " << nb.first << " -> " << nb.second << std::endl;
1186
727
      bounds.push_back(nb.first);
1187
727
      subs.push_back(NodeManager::currentNM()->mkConst(nb.second));
1188
    }
1189
    // eliminate from args
1190
556
    std::vector<Node>::iterator ita = std::find(args.begin(), args.end(), v);
1191
556
    Assert(ita != args.end());
1192
556
    args.erase(ita);
1193
556
    ret = true;
1194
  }
1195
3569
  return ret;
1196
}
1197
1198
96263
Node QuantifiersRewriter::computeVarElimination( Node body, std::vector< Node >& args, QAttributes& qa ){
1199
192526
  if (!options::varElimQuant() && !options::dtVarExpandQuant()
1200
192418
      && !options::varIneqElimQuant())
1201
  {
1202
    return body;
1203
  }
1204
192526
  Node prev;
1205
297827
  while (prev != body && !args.empty())
1206
  {
1207
100782
    prev = body;
1208
1209
201564
    std::vector<Node> vars;
1210
201564
    std::vector<Node> subs;
1211
    // standard variable elimination
1212
100782
    if (options::varElimQuant())
1213
    {
1214
100782
      getVarElim(body, false, args, vars, subs);
1215
    }
1216
    // variable elimination based on one-direction inequalities
1217
100782
    if (vars.empty() && options::varIneqElimQuant())
1218
    {
1219
96075
      getVarElimIneq(body, args, vars, subs, qa);
1220
    }
1221
    // if we eliminated a variable, update body and reprocess
1222
100782
    if (!vars.empty())
1223
    {
1224
10304
      Trace("var-elim-quant-debug")
1225
5152
          << "VE " << vars.size() << "/" << args.size() << std::endl;
1226
5152
      Assert(vars.size() == subs.size());
1227
      // remake with eliminated nodes
1228
5152
      body =
1229
10304
          body.substitute(vars.begin(), vars.end(), subs.begin(), subs.end());
1230
5152
      body = Rewriter::rewrite(body);
1231
5152
      if (!qa.d_ipl.isNull())
1232
      {
1233
        qa.d_ipl = qa.d_ipl.substitute(
1234
            vars.begin(), vars.end(), subs.begin(), subs.end());
1235
      }
1236
5152
      Trace("var-elim-quant") << "Return " << body << std::endl;
1237
    }
1238
  }
1239
96263
  return body;
1240
}
1241
1242
399965
Node QuantifiersRewriter::computePrenex(
1243
    Node q,
1244
    Node body,
1245
    std::unordered_set<Node, NodeHashFunction>& args,
1246
    std::unordered_set<Node, NodeHashFunction>& nargs,
1247
    bool pol,
1248
    bool prenexAgg)
1249
{
1250
399965
  NodeManager* nm = NodeManager::currentNM();
1251
399965
  Kind k = body.getKind();
1252
399965
  if (k == FORALL)
1253
  {
1254
14317
    if( ( pol || prenexAgg ) && ( options::prenexQuantUser() || body.getNumChildren()==2 ) ){
1255
2154
      std::vector< Node > terms;
1256
2154
      std::vector< Node > subs;
1257
1077
      BoundVarManager* bvm = nm->getBoundVarManager();
1258
      //for doing prenexing of same-signed quantifiers
1259
      //must rename each variable that already exists
1260
2780
      for (const Node& v : body[0])
1261
      {
1262
1703
        terms.push_back(v);
1263
3406
        TypeNode vt = v.getType();
1264
3406
        Node vv;
1265
1703
        if (!q.isNull())
1266
        {
1267
3406
          Node cacheVal = BoundVarManager::getCacheValue(q, v);
1268
1703
          vv = bvm->mkBoundVar<QRewPrenexAttribute>(cacheVal, vt);
1269
        }
1270
        else
1271
        {
1272
          // not specific to a quantified formula, use normal
1273
          vv = nm->mkBoundVar(vt);
1274
        }
1275
1703
        subs.push_back(vv);
1276
      }
1277
1077
      if (pol)
1278
      {
1279
1077
        args.insert(subs.begin(), subs.end());
1280
      }
1281
      else
1282
      {
1283
        nargs.insert(subs.begin(), subs.end());
1284
      }
1285
2154
      Node newBody = body[1];
1286
1077
      newBody = newBody.substitute( terms.begin(), terms.end(), subs.begin(), subs.end() );
1287
1077
      return newBody;
1288
    }
1289
  //must remove structure
1290
  }
1291
385648
  else if (prenexAgg && k == ITE && body.getType().isBoolean())
1292
  {
1293
    Node nn = nm->mkNode(AND,
1294
                         nm->mkNode(OR, body[0].notNode(), body[1]),
1295
                         nm->mkNode(OR, body[0], body[2]));
1296
    return computePrenex(q, nn, args, nargs, pol, prenexAgg);
1297
  }
1298
385648
  else if (prenexAgg && k == EQUAL && body[0].getType().isBoolean())
1299
  {
1300
    Node nn = nm->mkNode(AND,
1301
                         nm->mkNode(OR, body[0].notNode(), body[1]),
1302
                         nm->mkNode(OR, body[0], body[1].notNode()));
1303
    return computePrenex(q, nn, args, nargs, pol, prenexAgg);
1304
385648
  }else if( body.getType().isBoolean() ){
1305
385648
    Assert(k != EXISTS);
1306
385648
    bool childrenChanged = false;
1307
770245
    std::vector< Node > newChildren;
1308
1176561
    for (size_t i = 0, nchild = body.getNumChildren(); i < nchild; i++)
1309
    {
1310
      bool newHasPol;
1311
      bool newPol;
1312
790913
      QuantPhaseReq::getPolarity( body, i, true, pol, newHasPol, newPol );
1313
1277846
      if (!newHasPol)
1314
      {
1315
486933
        newChildren.push_back( body[i] );
1316
486933
        continue;
1317
      }
1318
607960
      Node n = computePrenex(q, body[i], args, nargs, newPol, prenexAgg);
1319
303980
      newChildren.push_back(n);
1320
303980
      childrenChanged = n != body[i] || childrenChanged;
1321
    }
1322
385648
    if( childrenChanged ){
1323
1051
      if (k == NOT && newChildren[0].getKind() == NOT)
1324
      {
1325
        return newChildren[0][0];
1326
      }
1327
1051
      return nm->mkNode(k, newChildren);
1328
    }
1329
  }
1330
397837
  return body;
1331
}
1332
1333
Node QuantifiersRewriter::computePrenexAgg(Node n,
1334
                                           std::map<Node, Node>& visited)
1335
{
1336
  std::map< Node, Node >::iterator itv = visited.find( n );
1337
  if( itv!=visited.end() ){
1338
    return itv->second;
1339
  }
1340
  if (!expr::hasClosure(n))
1341
  {
1342
    // trivial
1343
    return n;
1344
  }
1345
  NodeManager* nm = NodeManager::currentNM();
1346
  Node ret = n;
1347
  if (n.getKind() == NOT)
1348
  {
1349
    ret = computePrenexAgg(n[0], visited).negate();
1350
  }
1351
  else if (n.getKind() == FORALL)
1352
  {
1353
    std::vector<Node> children;
1354
    children.push_back(computePrenexAgg(n[1], visited));
1355
    std::vector<Node> args;
1356
    args.insert(args.end(), n[0].begin(), n[0].end());
1357
    // for each child, strip top level quant
1358
    for (unsigned i = 0; i < children.size(); i++)
1359
    {
1360
      if (children[i].getKind() == FORALL)
1361
      {
1362
        args.insert(args.end(), children[i][0].begin(), children[i][0].end());
1363
        children[i] = children[i][1];
1364
      }
1365
    }
1366
    // keep the pattern
1367
    std::vector<Node> iplc;
1368
    if (n.getNumChildren() == 3)
1369
    {
1370
      iplc.insert(iplc.end(), n[2].begin(), n[2].end());
1371
    }
1372
    Node nb = children.size() == 1 ? children[0] : nm->mkNode(OR, children);
1373
    ret = mkForall(args, nb, iplc, true);
1374
  }
1375
  else
1376
  {
1377
    std::unordered_set<Node, NodeHashFunction> argsSet;
1378
    std::unordered_set<Node, NodeHashFunction> nargsSet;
1379
    Node q;
1380
    Node nn = computePrenex(q, n, argsSet, nargsSet, true, true);
1381
    Assert(n != nn || argsSet.empty());
1382
    Assert(n != nn || nargsSet.empty());
1383
    if (n != nn)
1384
    {
1385
      Node nnn = computePrenexAgg(nn, visited);
1386
      // merge prenex
1387
      if (nnn.getKind() == FORALL)
1388
      {
1389
        argsSet.insert(nnn[0].begin(), nnn[0].end());
1390
        nnn = nnn[1];
1391
        // pos polarity variables are inner
1392
        if (!argsSet.empty())
1393
        {
1394
          nnn = mkForall({argsSet.begin(), argsSet.end()}, nnn, true);
1395
        }
1396
        argsSet.clear();
1397
      }
1398
      else if (nnn.getKind() == NOT && nnn[0].getKind() == FORALL)
1399
      {
1400
        nargsSet.insert(nnn[0][0].begin(), nnn[0][0].end());
1401
        nnn = nnn[0][1].negate();
1402
      }
1403
      if (!nargsSet.empty())
1404
      {
1405
        nnn = mkForall({nargsSet.begin(), nargsSet.end()}, nnn.negate(), true)
1406
                  .negate();
1407
      }
1408
      if (!argsSet.empty())
1409
      {
1410
        nnn = mkForall({argsSet.begin(), argsSet.end()}, nnn, true);
1411
      }
1412
      ret = nnn;
1413
    }
1414
  }
1415
  visited[n] = ret;
1416
  return ret;
1417
}
1418
1419
40013
Node QuantifiersRewriter::computeSplit( std::vector< Node >& args, Node body, QAttributes& qa ) {
1420
40013
  Assert(body.getKind() == OR);
1421
40013
  size_t var_found_count = 0;
1422
40013
  size_t eqc_count = 0;
1423
40013
  size_t eqc_active = 0;
1424
80026
  std::map< Node, int > var_to_eqc;
1425
80026
  std::map< int, std::vector< Node > > eqc_to_var;
1426
80026
  std::map< int, std::vector< Node > > eqc_to_lit;
1427
1428
80026
  std::vector<Node> lits;
1429
1430
172311
  for( unsigned i=0; i<body.getNumChildren(); i++ ){
1431
    //get variables contained in the literal
1432
264596
    Node n = body[i];
1433
264596
    std::vector< Node > lit_args;
1434
132298
    computeArgVec( args, lit_args, n );
1435
132298
    if( lit_args.empty() ){
1436
1635
      lits.push_back( n );
1437
    }else {
1438
      //collect the equivalence classes this literal belongs to, and the new variables it contributes
1439
261326
      std::vector< int > eqcs;
1440
261326
      std::vector< Node > lit_new_args;
1441
      //for each variable in literal
1442
441995
      for( unsigned j=0; j<lit_args.size(); j++) {
1443
        //see if the variable has already been found
1444
311332
        if (var_to_eqc.find(lit_args[j])!=var_to_eqc.end()) {
1445
210287
          int eqc = var_to_eqc[lit_args[j]];
1446
210287
          if (std::find(eqcs.begin(), eqcs.end(), eqc)==eqcs.end()) {
1447
90403
            eqcs.push_back(eqc);
1448
          }
1449
        }else{
1450
101045
          var_found_count++;
1451
101045
          lit_new_args.push_back(lit_args[j]);
1452
        }
1453
      }
1454
130663
      if (eqcs.empty()) {
1455
45877
        eqcs.push_back(eqc_count);
1456
45877
        eqc_count++;
1457
45877
        eqc_active++;
1458
      }
1459
1460
130663
      int eqcz = eqcs[0];
1461
      //merge equivalence classes with eqcz
1462
136280
      for (unsigned j=1; j<eqcs.size(); j++) {
1463
5617
        int eqc = eqcs[j];
1464
        //move all variables from equivalence class
1465
29239
        for (unsigned k=0; k<eqc_to_var[eqc].size(); k++) {
1466
47244
          Node v = eqc_to_var[eqc][k];
1467
23622
          var_to_eqc[v] = eqcz;
1468
23622
          eqc_to_var[eqcz].push_back(v);
1469
        }
1470
5617
        eqc_to_var.erase(eqc);
1471
        //move all literals from equivalence class
1472
28082
        for (unsigned k=0; k<eqc_to_lit[eqc].size(); k++) {
1473
44930
          Node l = eqc_to_lit[eqc][k];
1474
22465
          eqc_to_lit[eqcz].push_back(l);
1475
        }
1476
5617
        eqc_to_lit.erase(eqc);
1477
5617
        eqc_active--;
1478
      }
1479
      //add variables to equivalence class
1480
231708
      for (unsigned j=0; j<lit_new_args.size(); j++) {
1481
101045
        var_to_eqc[lit_new_args[j]] = eqcz;
1482
101045
        eqc_to_var[eqcz].push_back(lit_new_args[j]);
1483
      }
1484
      //add literal to equivalence class
1485
130663
      eqc_to_lit[eqcz].push_back(n);
1486
    }
1487
  }
1488
40013
  if ( eqc_active>1 || !lits.empty() || var_to_eqc.size()!=args.size() ){
1489
613
    NodeManager* nm = NodeManager::currentNM();
1490
613
    Trace("clause-split-debug") << "Split quantified formula with body " << body << std::endl;
1491
613
    Trace("clause-split-debug") << "   Ground literals: " << std::endl;
1492
2248
    for( size_t i=0; i<lits.size(); i++) {
1493
1635
      Trace("clause-split-debug") << "      " << lits[i] << std::endl;
1494
    }
1495
613
    Trace("clause-split-debug") << std::endl;
1496
613
    Trace("clause-split-debug") << "Equivalence classes: " << std::endl;
1497
1473
    for (std::map< int, std::vector< Node > >::iterator it = eqc_to_lit.begin(); it != eqc_to_lit.end(); ++it ){
1498
860
      Trace("clause-split-debug") << "   Literals: " << std::endl;
1499
4105
      for (size_t i=0; i<it->second.size(); i++) {
1500
3245
        Trace("clause-split-debug") << "      " << it->second[i] << std::endl;
1501
      }
1502
860
      int eqc = it->first;
1503
860
      Trace("clause-split-debug") << "   Variables: " << std::endl;
1504
3690
      for (size_t i=0; i<eqc_to_var[eqc].size(); i++) {
1505
2830
        Trace("clause-split-debug") << "      " << eqc_to_var[eqc][i] << std::endl;
1506
      }
1507
860
      Trace("clause-split-debug") << std::endl;
1508
1720
      Node bvl = NodeManager::currentNM()->mkNode( BOUND_VAR_LIST, eqc_to_var[eqc]);
1509
      Node bd =
1510
1720
          it->second.size() == 1 ? it->second[0] : nm->mkNode(OR, it->second);
1511
1720
      Node fa = nm->mkNode(FORALL, bvl, bd);
1512
860
      lits.push_back(fa);
1513
    }
1514
613
    Assert(!lits.empty());
1515
1226
    Node nf = lits.size()==1 ? lits[0] : NodeManager::currentNM()->mkNode(OR,lits);
1516
613
    Trace("clause-split-debug") << "Made node : " << nf << std::endl;
1517
613
    return nf;
1518
  }else{
1519
39400
    return mkForAll( args, body, qa );
1520
  }
1521
}
1522
1523
97668
Node QuantifiersRewriter::mkForAll(const std::vector<Node>& args,
1524
                                   Node body,
1525
                                   QAttributes& qa)
1526
{
1527
97668
  if (args.empty())
1528
  {
1529
79
    return body;
1530
  }
1531
97589
  NodeManager* nm = NodeManager::currentNM();
1532
195178
  std::vector<Node> children;
1533
97589
  children.push_back(nm->mkNode(kind::BOUND_VAR_LIST, args));
1534
97589
  children.push_back(body);
1535
97589
  if (!qa.d_ipl.isNull())
1536
  {
1537
    children.push_back(qa.d_ipl);
1538
  }
1539
97589
  return nm->mkNode(kind::FORALL, children);
1540
}
1541
1542
Node QuantifiersRewriter::mkForall(const std::vector<Node>& args,
1543
                                   Node body,
1544
                                   bool marked)
1545
{
1546
  std::vector< Node > iplc;
1547
  return mkForall( args, body, iplc, marked );
1548
}
1549
1550
Node QuantifiersRewriter::mkForall(const std::vector<Node>& args,
1551
                                   Node body,
1552
                                   std::vector<Node>& iplc,
1553
                                   bool marked)
1554
{
1555
  if (args.empty())
1556
  {
1557
    return body;
1558
  }
1559
  NodeManager* nm = NodeManager::currentNM();
1560
  std::vector<Node> children;
1561
  children.push_back(nm->mkNode(kind::BOUND_VAR_LIST, args));
1562
  children.push_back(body);
1563
  if (marked)
1564
  {
1565
    Node avar = nm->mkSkolem("id", nm->booleanType());
1566
    QuantIdNumAttribute ida;
1567
    avar.setAttribute(ida, 0);
1568
    iplc.push_back(nm->mkNode(kind::INST_ATTRIBUTE, avar));
1569
  }
1570
  if (!iplc.empty())
1571
  {
1572
    children.push_back(nm->mkNode(kind::INST_PATTERN_LIST, iplc));
1573
  }
1574
  return nm->mkNode(kind::FORALL, children);
1575
}
1576
1577
//computes miniscoping, also eliminates variables that do not occur free in body
1578
98878
Node QuantifiersRewriter::computeMiniscoping(Node q, QAttributes& qa)
1579
{
1580
98878
  NodeManager* nm = NodeManager::currentNM();
1581
197756
  std::vector<Node> args(q[0].begin(), q[0].end());
1582
197756
  Node body = q[1];
1583
98878
  if( body.getKind()==FORALL ){
1584
    //combine prenex
1585
174
    std::vector< Node > newArgs;
1586
87
    newArgs.insert(newArgs.end(), q[0].begin(), q[0].end());
1587
245
    for( unsigned i=0; i<body[0].getNumChildren(); i++ ){
1588
158
      newArgs.push_back( body[0][i] );
1589
    }
1590
87
    return mkForAll( newArgs, body[1], qa );
1591
98791
  }else if( body.getKind()==AND ){
1592
    // aggressive miniscoping implies that structural miniscoping should
1593
    // be applied first
1594
229862
    if (options::miniscopeQuant() || options::aggressiveMiniscopeQuant())
1595
    {
1596
611
      BoundVarManager* bvm = nm->getBoundVarManager();
1597
      // Break apart the quantifed formula
1598
      // forall x. P1 ^ ... ^ Pn ---> forall x. P1 ^ ... ^ forall x. Pn
1599
1222
      NodeBuilder<> t(kind::AND);
1600
1222
      std::vector<Node> argsc;
1601
3574
      for (size_t i = 0, nchild = body.getNumChildren(); i < nchild; i++)
1602
      {
1603
2963
        if (argsc.empty())
1604
        {
1605
          // If not done so, we must create fresh copy of args. This is to
1606
          // ensure that quantified formulas do not reuse variables.
1607
6312
          for (const Node& v : q[0])
1608
          {
1609
9650
            TypeNode vt = v.getType();
1610
9650
            Node cacheVal = BoundVarManager::getCacheValue(q, v, i);
1611
9650
            Node vv = bvm->mkBoundVar<QRewMiniscopeAttribute>(cacheVal, vt);
1612
4825
            argsc.push_back(vv);
1613
          }
1614
        }
1615
5926
        Node b = body[i];
1616
        Node bodyc =
1617
5926
            b.substitute(args.begin(), args.end(), argsc.begin(), argsc.end());
1618
2963
        if (b == bodyc)
1619
        {
1620
          // Did not contain variables in args, thus it is ground. Since we did
1621
          // not use them, we keep the variables argsc for the next child.
1622
1508
          t << b;
1623
        }
1624
        else
1625
        {
1626
          // make the miniscoped quantified formula
1627
2910
          Node cbvl = nm->mkNode(BOUND_VAR_LIST, argsc);
1628
2910
          Node qq = nm->mkNode(FORALL, cbvl, bodyc);
1629
1455
          t << qq;
1630
          // We used argsc, clear so we will construct a fresh copy above.
1631
1455
          argsc.clear();
1632
        }
1633
      }
1634
1222
      Node retVal = t;
1635
611
      return retVal;
1636
    }
1637
97214
  }else if( body.getKind()==OR ){
1638
41837
    if( options::quantSplit() ){
1639
      //splitting subsumes free variable miniscoping, apply it with higher priority
1640
40013
      return computeSplit( args, body, qa );
1641
    }
1642
3648
    else if (options::miniscopeQuantFreeVar()
1643
1824
             || options::aggressiveMiniscopeQuant())
1644
    {
1645
      // aggressive miniscoping implies that free variable miniscoping should
1646
      // be applied first
1647
5
      Node newBody = body;
1648
5
      NodeBuilder<> body_split(kind::OR);
1649
5
      NodeBuilder<> tb(kind::OR);
1650
15
      for (const Node& trm : body)
1651
      {
1652
10
        if (expr::hasSubterm(trm, args))
1653
        {
1654
5
          tb << trm;
1655
        }else{
1656
5
          body_split << trm;
1657
        }
1658
      }
1659
5
      if( tb.getNumChildren()==0 ){
1660
        return body_split;
1661
5
      }else if( body_split.getNumChildren()>0 ){
1662
5
        newBody = tb.getNumChildren()==1 ? tb.getChild( 0 ) : tb;
1663
10
        std::vector< Node > activeArgs;
1664
5
        computeArgVec2( args, activeArgs, newBody, qa.d_ipl );
1665
5
        body_split << mkForAll( activeArgs, newBody, qa );
1666
5
        return body_split.getNumChildren()==1 ? body_split.getChild( 0 ) : body_split;
1667
      }
1668
    }
1669
55377
  }else if( body.getKind()==NOT ){
1670
14973
    Assert(isLiteral(body[0]));
1671
  }
1672
  //remove variables that don't occur
1673
116324
  std::vector< Node > activeArgs;
1674
58162
  computeArgVec2( args, activeArgs, body, qa.d_ipl );
1675
58162
  return mkForAll( activeArgs, body, qa );
1676
}
1677
1678
14
Node QuantifiersRewriter::computeAggressiveMiniscoping( std::vector< Node >& args, Node body ){
1679
28
  std::map<Node, std::vector<Node> > varLits;
1680
28
  std::map<Node, std::vector<Node> > litVars;
1681
14
  if (body.getKind() == OR) {
1682
    Trace("ag-miniscope") << "compute aggressive miniscoping on " << body << std::endl;
1683
    for (size_t i = 0; i < body.getNumChildren(); i++) {
1684
      std::vector<Node> activeArgs;
1685
      computeArgVec(args, activeArgs, body[i]);
1686
      for (unsigned j = 0; j < activeArgs.size(); j++) {
1687
        varLits[activeArgs[j]].push_back(body[i]);
1688
      }
1689
      std::vector<Node>& lit_body_i = litVars[body[i]];
1690
      std::vector<Node>::iterator lit_body_i_begin = lit_body_i.begin();
1691
      std::vector<Node>::const_iterator active_begin = activeArgs.begin();
1692
      std::vector<Node>::const_iterator active_end = activeArgs.end();
1693
      lit_body_i.insert(lit_body_i_begin, active_begin, active_end);
1694
    }
1695
    //find the variable in the least number of literals
1696
    Node bestVar;
1697
    for( std::map< Node, std::vector<Node> >::iterator it = varLits.begin(); it != varLits.end(); ++it ){
1698
      if( bestVar.isNull() || varLits[bestVar].size()>it->second.size() ){
1699
        bestVar = it->first;
1700
      }
1701
    }
1702
    Trace("ag-miniscope-debug") << "Best variable " << bestVar << " occurs in " << varLits[bestVar].size() << "/ " << body.getNumChildren() << " literals." << std::endl;
1703
    if( !bestVar.isNull() && varLits[bestVar].size()<body.getNumChildren() ){
1704
      //we can miniscope
1705
      Trace("ag-miniscope") << "Miniscope on " << bestVar << std::endl;
1706
      //make the bodies
1707
      std::vector<Node> qlit1;
1708
      qlit1.insert( qlit1.begin(), varLits[bestVar].begin(), varLits[bestVar].end() );
1709
      std::vector<Node> qlitt;
1710
      //for all literals not containing bestVar
1711
      for( size_t i=0; i<body.getNumChildren(); i++ ){
1712
        if( std::find( qlit1.begin(), qlit1.end(), body[i] )==qlit1.end() ){
1713
          qlitt.push_back( body[i] );
1714
        }
1715
      }
1716
      //make the variable lists
1717
      std::vector<Node> qvl1;
1718
      std::vector<Node> qvl2;
1719
      std::vector<Node> qvsh;
1720
      for( unsigned i=0; i<args.size(); i++ ){
1721
        bool found1 = false;
1722
        bool found2 = false;
1723
        for( size_t j=0; j<varLits[args[i]].size(); j++ ){
1724
          if( !found1 && std::find( qlit1.begin(), qlit1.end(), varLits[args[i]][j] )!=qlit1.end() ){
1725
            found1 = true;
1726
          }else if( !found2 && std::find( qlitt.begin(), qlitt.end(), varLits[args[i]][j] )!=qlitt.end() ){
1727
            found2 = true;
1728
          }
1729
          if( found1 && found2 ){
1730
            break;
1731
          }
1732
        }
1733
        if( found1 ){
1734
          if( found2 ){
1735
            qvsh.push_back( args[i] );
1736
          }else{
1737
            qvl1.push_back( args[i] );
1738
          }
1739
        }else{
1740
          Assert(found2);
1741
          qvl2.push_back( args[i] );
1742
        }
1743
      }
1744
      Assert(!qvl1.empty());
1745
      //check for literals that only contain shared variables
1746
      std::vector<Node> qlitsh;
1747
      std::vector<Node> qlit2;
1748
      for( size_t i=0; i<qlitt.size(); i++ ){
1749
        bool hasVar2 = false;
1750
        for( size_t j=0; j<litVars[qlitt[i]].size(); j++ ){
1751
          if( std::find( qvl2.begin(), qvl2.end(), litVars[qlitt[i]][j] )!=qvl2.end() ){
1752
            hasVar2 = true;
1753
            break;
1754
          }
1755
        }
1756
        if( hasVar2 ){
1757
          qlit2.push_back( qlitt[i] );
1758
        }else{
1759
          qlitsh.push_back( qlitt[i] );
1760
        }
1761
      }
1762
      varLits.clear();
1763
      litVars.clear();
1764
      Trace("ag-miniscope-debug") << "Split into literals : " << qlit1.size() << " / " << qlit2.size() << " / " << qlitsh.size();
1765
      Trace("ag-miniscope-debug") << ", variables : " << qvl1.size() << " / " << qvl2.size() << " / " << qvsh.size() << std::endl;
1766
      Node n1 = qlit1.size()==1 ? qlit1[0] : NodeManager::currentNM()->mkNode( OR, qlit1 );
1767
      n1 = computeAggressiveMiniscoping( qvl1, n1 );
1768
      qlitsh.push_back( n1 );
1769
      if( !qlit2.empty() ){
1770
        Node n2 = qlit2.size()==1 ? qlit2[0] : NodeManager::currentNM()->mkNode( OR, qlit2 );
1771
        n2 = computeAggressiveMiniscoping( qvl2, n2 );
1772
        qlitsh.push_back( n2 );
1773
      }
1774
      Node n = NodeManager::currentNM()->mkNode( OR, qlitsh );
1775
      if( !qvsh.empty() ){
1776
        Node bvl = NodeManager::currentNM()->mkNode(kind::BOUND_VAR_LIST, qvsh);
1777
        n = NodeManager::currentNM()->mkNode( FORALL, bvl, n );
1778
      }
1779
      Trace("ag-miniscope") << "Return " << n << " for " << body << std::endl;
1780
      return n;
1781
    }
1782
  }
1783
28
  QAttributes qa;
1784
14
  return mkForAll( args, body, qa );
1785
}
1786
1787
919447
bool QuantifiersRewriter::doOperation(Node q,
1788
                                      RewriteStep computeOption,
1789
                                      QAttributes& qa)
1790
{
1791
  bool is_strict_trigger =
1792
919447
      qa.d_hasPattern
1793
919447
      && options::userPatternsQuant() == options::UserPatMode::TRUST;
1794
919447
  bool is_std = qa.isStandard() && !is_strict_trigger;
1795
919447
  if (computeOption == COMPUTE_ELIM_SYMBOLS)
1796
  {
1797
127385
    return true;
1798
  }
1799
792062
  else if (computeOption == COMPUTE_MINISCOPING)
1800
  {
1801
115074
    return is_std;
1802
  }
1803
676988
  else if (computeOption == COMPUTE_AGGRESSIVE_MINISCOPING)
1804
  {
1805
113539
    return options::aggressiveMiniscopeQuant() && is_std;
1806
  }
1807
563449
  else if (computeOption == COMPUTE_EXT_REWRITE)
1808
  {
1809
227100
    return options::extRewriteQuant();
1810
  }
1811
449910
  else if (computeOption == COMPUTE_PROCESS_TERMS)
1812
  {
1813
113528
    return is_std && options::iteLiftQuant() != options::IteLiftQuantMode::NONE;
1814
  }
1815
336382
  else if (computeOption == COMPUTE_COND_SPLIT)
1816
  {
1817
220812
    return (options::iteDtTesterSplitQuant() || options::condVarSplitQuant())
1818
221122
           && !is_strict_trigger;
1819
  }
1820
225821
  else if (computeOption == COMPUTE_PRENEX)
1821
  {
1822
113362
    return options::prenexQuant() != options::PrenexQuantMode::NONE
1823
113362
           && !options::aggressiveMiniscopeQuant() && is_std;
1824
  }
1825
112459
  else if (computeOption == COMPUTE_VAR_ELIMINATION)
1826
  {
1827
112459
    return (options::varElimQuant() || options::dtVarExpandQuant()) && is_std;
1828
  }
1829
  else
1830
  {
1831
    return false;
1832
  }
1833
}
1834
1835
//general method for computing various rewrites
1836
612999
Node QuantifiersRewriter::computeOperation(Node f,
1837
                                           RewriteStep computeOption,
1838
                                           QAttributes& qa)
1839
{
1840
612999
  Trace("quantifiers-rewrite-debug") << "Compute operation " << computeOption << " on " << f << " " << qa.d_qid_num << std::endl;
1841
612999
  if (computeOption == COMPUTE_MINISCOPING)
1842
  {
1843
98878
    if (options::prenexQuant() == options::PrenexQuantMode::NORMAL)
1844
    {
1845
      if( !qa.d_qid_num.isNull() ){
1846
        //already processed this, return self
1847
        return f;
1848
      }
1849
    }
1850
    //return directly
1851
98878
    return computeMiniscoping(f, qa);
1852
  }
1853
1028242
  std::vector<Node> args(f[0].begin(), f[0].end());
1854
1028242
  Node n = f[1];
1855
514121
  if (computeOption == COMPUTE_ELIM_SYMBOLS)
1856
  {
1857
127385
    n = computeElimSymbols(n);
1858
386736
  }else if( computeOption==COMPUTE_AGGRESSIVE_MINISCOPING ){
1859
14
    return computeAggressiveMiniscoping( args, n );
1860
  }
1861
386722
  else if (computeOption == COMPUTE_EXT_REWRITE)
1862
  {
1863
29
    return computeExtendedRewrite(f);
1864
  }
1865
386693
  else if (computeOption == COMPUTE_PROCESS_TERMS)
1866
  {
1867
194664
    std::vector< Node > new_conds;
1868
97332
    n = computeProcessTerms( n, args, new_conds, f, qa );
1869
97332
    if( !new_conds.empty() ){
1870
      new_conds.push_back( n );
1871
      n = NodeManager::currentNM()->mkNode( OR, new_conds );
1872
    }
1873
  }
1874
289361
  else if (computeOption == COMPUTE_COND_SPLIT)
1875
  {
1876
97113
    n = computeCondSplit(n, args, qa);
1877
  }
1878
192248
  else if (computeOption == COMPUTE_PRENEX)
1879
  {
1880
95985
    if (options::prenexQuant() == options::PrenexQuantMode::NORMAL)
1881
    {
1882
      //will rewrite at preprocess time
1883
      return f;
1884
    }
1885
    else
1886
    {
1887
191970
      std::unordered_set<Node, NodeHashFunction> argsSet, nargsSet;
1888
95985
      n = computePrenex(f, n, argsSet, nargsSet, true, false);
1889
95985
      Assert(nargsSet.empty());
1890
95985
      args.insert(args.end(), argsSet.begin(), argsSet.end());
1891
    }
1892
  }
1893
96263
  else if (computeOption == COMPUTE_VAR_ELIMINATION)
1894
  {
1895
96263
    n = computeVarElimination( n, args, qa );
1896
  }
1897
514078
  Trace("quantifiers-rewrite-debug") << "Compute Operation: return " << n << ", " << args.size() << std::endl;
1898
514078
  if( f[1]==n && args.size()==f[0].getNumChildren() ){
1899
498647
    return f;
1900
  }else{
1901
15431
    if( args.empty() ){
1902
633
      return n;
1903
    }else{
1904
29596
      std::vector< Node > children;
1905
14798
      children.push_back( NodeManager::currentNM()->mkNode(kind::BOUND_VAR_LIST, args ) );
1906
14798
      children.push_back( n );
1907
14798
      if( !qa.d_ipl.isNull() && args.size()==f[0].getNumChildren() ){
1908
1803
        children.push_back( qa.d_ipl );
1909
      }
1910
14798
      return NodeManager::currentNM()->mkNode(kind::FORALL, children );
1911
    }
1912
  }
1913
}
1914
1915
bool QuantifiersRewriter::isPrenexNormalForm( Node n ) {
1916
  if( n.getKind()==FORALL ){
1917
    return n[1].getKind()!=FORALL && isPrenexNormalForm( n[1] );
1918
  }else if( n.getKind()==NOT ){
1919
    return n[0].getKind()!=NOT && isPrenexNormalForm( n[0] );
1920
  }else{
1921
    return !expr::hasClosure(n);
1922
  }
1923
}
1924
1925
821
Node QuantifiersRewriter::preSkolemizeQuantifiers( Node n, bool polarity, std::vector< TypeNode >& fvTypes, std::vector< TNode >& fvs ){
1926
821
  Trace("pre-sk") << "Pre-skolem " << n << " " << polarity << " " << fvs.size() << endl;
1927
821
  if( n.getKind()==kind::NOT ){
1928
250
    Node nn = preSkolemizeQuantifiers( n[0], !polarity, fvTypes, fvs );
1929
125
    return nn.negate();
1930
696
  }else if( n.getKind()==kind::FORALL ){
1931
175
    if (n.getNumChildren() == 3)
1932
    {
1933
      // Do not pre-skolemize quantified formulas with three children.
1934
      // This includes non-standard quantified formulas
1935
      // like recursive function definitions, or sygus conjectures, and
1936
      // quantified formulas with triggers.
1937
86
      return n;
1938
    }
1939
89
    else if (polarity)
1940
    {
1941
68
      if( options::preSkolemQuant() && options::preSkolemQuantNested() ){
1942
100
        vector< Node > children;
1943
50
        children.push_back( n[0] );
1944
        //add children to current scope
1945
100
        std::vector< TypeNode > fvt;
1946
100
        std::vector< TNode > fvss;
1947
50
        fvt.insert( fvt.begin(), fvTypes.begin(), fvTypes.end() );
1948
50
        fvss.insert( fvss.begin(), fvs.begin(), fvs.end() );
1949
114
        for( int i=0; i<(int)n[0].getNumChildren(); i++ ){
1950
64
          fvt.push_back( n[0][i].getType() );
1951
64
          fvss.push_back( n[0][i] );
1952
        }
1953
        //process body
1954
50
        children.push_back( preSkolemizeQuantifiers( n[1], polarity, fvt, fvss ) );
1955
        //return processed quantifier
1956
50
        return NodeManager::currentNM()->mkNode( kind::FORALL, children );
1957
      }
1958
    }else{
1959
      //process body
1960
42
      Node nn = preSkolemizeQuantifiers( n[1], polarity, fvTypes, fvs );
1961
42
      std::vector< Node > sk;
1962
42
      Node sub;
1963
42
      std::vector< unsigned > sub_vars;
1964
      //return skolemized body
1965
      return Skolemize::mkSkolemizedBody(
1966
21
          n, nn, fvTypes, fvs, sk, sub, sub_vars);
1967
    }
1968
  }else{
1969
    //check if it contains a quantifier as a subterm
1970
    //if so, we will write this node
1971
521
    if (expr::hasClosure(n))
1972
    {
1973
89
      if( ( n.getKind()==kind::ITE && n.getType().isBoolean() ) || ( n.getKind()==kind::EQUAL && n[0].getType().isBoolean() ) ){
1974
28
        if( options::preSkolemQuantAgg() ){
1975
28
          Node nn;
1976
          //must remove structure
1977
14
          if( n.getKind()==kind::ITE ){
1978
            nn = NodeManager::currentNM()->mkNode( kind::AND,
1979
                  NodeManager::currentNM()->mkNode( kind::OR, n[0].notNode(), n[1] ),
1980
                  NodeManager::currentNM()->mkNode( kind::OR, n[0], n[2] ) );
1981
14
          }else if( n.getKind()==kind::EQUAL ){
1982
56
            nn = NodeManager::currentNM()->mkNode( kind::AND,
1983
28
                  NodeManager::currentNM()->mkNode( kind::OR, n[0].notNode(), n.getKind()==kind::XOR ? n[1].notNode() : n[1] ),
1984
28
                  NodeManager::currentNM()->mkNode( kind::OR, n[0], n.getKind()==kind::XOR ? n[1] : n[1].notNode() ) );
1985
          }
1986
14
          return preSkolemizeQuantifiers( nn, polarity, fvTypes, fvs );
1987
        }
1988
75
      }else if( n.getKind()==kind::AND || n.getKind()==kind::OR ){
1989
118
        vector< Node > children;
1990
177
        for( int i=0; i<(int)n.getNumChildren(); i++ ){
1991
118
          children.push_back( preSkolemizeQuantifiers( n[i], polarity, fvTypes, fvs ) );
1992
        }
1993
59
        return NodeManager::currentNM()->mkNode( n.getKind(), children );
1994
      }
1995
    }
1996
  }
1997
466
  return n;
1998
}
1999
2000
81176
TrustNode QuantifiersRewriter::preprocess(Node n, bool isInst)
2001
{
2002
162352
  Node prev = n;
2003
2004
81176
  if( options::preSkolemQuant() ){
2005
558
    if( !isInst || !options::preSkolemQuantNested() ){
2006
493
      Trace("quantifiers-preprocess-debug") << "Pre-skolemize " << n << "..." << std::endl;
2007
      //apply pre-skolemization to existential quantifiers
2008
986
      std::vector< TypeNode > fvTypes;
2009
986
      std::vector< TNode > fvs;
2010
493
      n = preSkolemizeQuantifiers( prev, true, fvTypes, fvs );
2011
    }
2012
  }
2013
  //pull all quantifiers globally
2014
81176
  if (options::prenexQuant() == options::PrenexQuantMode::NORMAL)
2015
  {
2016
    Trace("quantifiers-prenex") << "Prenexing : " << n << std::endl;
2017
    std::map<Node, Node> visited;
2018
    n = computePrenexAgg(n, visited);
2019
    n = Rewriter::rewrite( n );
2020
    Trace("quantifiers-prenex") << "Prenexing returned : " << n << std::endl;
2021
    //Assert( isPrenexNormalForm( n ) );
2022
  }
2023
81176
  if( n!=prev ){
2024
13
    Trace("quantifiers-preprocess") << "Preprocess " << prev << std::endl;
2025
13
    Trace("quantifiers-preprocess") << "..returned " << n << std::endl;
2026
13
    return TrustNode::mkTrustRewrite(prev, n, nullptr);
2027
  }
2028
81163
  return TrustNode::null();
2029
}
2030
2031
}/* CVC4::theory::quantifiers namespace */
2032
}/* CVC4::theory namespace */
2033
1782201
}/* CVC4 namespace */