GCC Code Coverage Report
Directory: . Exec Total Coverage
File: src/theory/quantifiers/quant_conflict_find.cpp Lines: 1157 1395 82.9 %
Date: 2021-03-23 Branches: 2475 5441 45.5 %

Line Exec Source
1
/*********************                                                        */
2
/*! \file quant_conflict_find.cpp
3
 ** \verbatim
4
 ** Top contributors (to current version):
5
 **   Andrew Reynolds, Tim King, Andres Noetzli
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 Implements conflict-based instantiation (Reynolds et al FMCAD 2014)
13
 **
14
 **/
15
16
#include "theory/quantifiers/quant_conflict_find.h"
17
18
#include "base/configuration.h"
19
#include "expr/node_algorithm.h"
20
#include "options/quantifiers_options.h"
21
#include "options/theory_options.h"
22
#include "options/uf_options.h"
23
#include "smt/smt_statistics_registry.h"
24
#include "theory/quantifiers/ematching/trigger_term_info.h"
25
#include "theory/quantifiers/first_order_model.h"
26
#include "theory/quantifiers/instantiate.h"
27
#include "theory/quantifiers/quant_util.h"
28
#include "theory/quantifiers/term_database.h"
29
#include "theory/quantifiers/term_util.h"
30
#include "theory/quantifiers_engine.h"
31
#include "theory/rewriter.h"
32
33
using namespace CVC4::kind;
34
using namespace std;
35
36
namespace CVC4 {
37
namespace theory {
38
namespace quantifiers {
39
40
21086
QuantInfo::QuantInfo() : d_unassigned_nvar(0), d_una_index(0), d_mg(nullptr) {}
41
42
42172
QuantInfo::~QuantInfo() {
43
21086
  delete d_mg;
44
99101
  for(std::map< int, MatchGen * >::iterator i = d_var_mg.begin(),
45
21086
          iend=d_var_mg.end(); i != iend; ++i) {
46
78015
    MatchGen* currentMatchGenerator = (*i).second;
47
78015
    delete currentMatchGenerator;
48
  }
49
21086
  d_var_mg.clear();
50
21086
}
51
52
53
21086
void QuantInfo::initialize( QuantConflictFind * p, Node q, Node qn ) {
54
21086
  d_q = q;
55
21086
  d_extra_var.clear();
56
70800
  for( unsigned i=0; i<q[0].getNumChildren(); i++ ){
57
49714
    d_match.push_back( TNode::null() );
58
49714
    d_match_term.push_back( TNode::null() );
59
  }
60
61
  //register the variables
62
70800
  for( unsigned i=0; i<q[0].getNumChildren(); i++ ){
63
49714
    d_var_num[q[0][i]] = i;
64
49714
    d_vars.push_back( q[0][i] );
65
49714
    d_var_types.push_back( q[0][i].getType() );
66
  }
67
68
21086
  registerNode( qn, true, true );
69
70
71
21086
  Trace("qcf-qregister") << "- Make match gen structure..." << std::endl;
72
21086
  d_mg = new MatchGen( this, qn );
73
74
21086
  if( d_mg->isValid() ){
75
    /*
76
    for( unsigned j=0; j<q[0].getNumChildren(); j++ ){
77
      if( d_inMatchConstraint.find( q[0][j] )==d_inMatchConstraint.end() ){
78
        Trace("qcf-invalid") << "QCF invalid : variable " << q[0][j] << " does not exist in a matching constraint." << std::endl;
79
        d_mg->setInvalid();
80
        break;
81
      }
82
    }
83
    */
84
100146
    for( unsigned j=q[0].getNumChildren(); j<d_vars.size(); j++ ){
85
83407
      if( d_vars[j].getKind()!=BOUND_VARIABLE ){
86
78015
        d_var_mg[j] = NULL;
87
78015
        bool is_tsym = false;
88
78015
        if( !MatchGen::isHandledUfTerm( d_vars[j] ) && d_vars[j].getKind()!=ITE ){
89
879
          is_tsym = true;
90
879
          d_tsym_vars.push_back( j );
91
        }
92
78015
        if( !is_tsym || options::qcfTConstraint() ){
93
77515
          d_var_mg[j] = new MatchGen( this, d_vars[j], true );
94
        }
95
78015
        if( !d_var_mg[j] || !d_var_mg[j]->isValid() ){
96
1630
          Trace("qcf-invalid") << "QCF invalid : cannot match for " << d_vars[j] << std::endl;
97
1630
          d_mg->setInvalid();
98
1630
          break;
99
        }else{
100
152770
          std::vector< int > bvars;
101
76385
          d_var_mg[j]->determineVariableOrder( this, bvars );
102
        }
103
      }
104
    }
105
18369
    if( d_mg->isValid() ){
106
33478
      std::vector< int > bvars;
107
16739
      d_mg->determineVariableOrder( this, bvars );
108
    }
109
  }else{
110
2717
    Trace("qcf-invalid") << "QCF invalid : body of formula cannot be processed." << std::endl;
111
  }
112
21086
  Trace("qcf-qregister-summary") << "QCF register : " << ( d_mg->isValid() ? "VALID " : "INVALID" ) << " : " << q << std::endl;
113
114
37825
  if( d_mg->isValid() && options::qcfEagerCheckRd() ){
115
    //optimization : record variable argument positions for terms that must be matched
116
33478
    std::vector< TNode > vars;
117
    //TODO: revisit this, makes QCF faster, but misses conflicts due to caring about paths that may not be relevant (starExec jobs 14136/14137)
118
33478
    if( options::qcfSkipRd() ){
119
      for( unsigned j=q[0].getNumChildren(); j<d_vars.size(); j++ ){
120
        vars.push_back( d_vars[j] );
121
      }
122
    }else{
123
      //get all variables that are always relevant
124
33478
      std::map< TNode, bool > visited;
125
16739
      getPropagateVars( p, vars, q[1], false, visited );
126
    }
127
94077
    for( unsigned j=0; j<vars.size(); j++ ){
128
154676
      Node v = vars[j];
129
154676
      TNode f = p->getTermDatabase()->getMatchOperator( v );
130
77338
      if( !f.isNull() ){
131
46798
        Trace("qcf-opt") << "Record variable argument positions in " << v << ", op=" << f << "..." << std::endl;
132
154409
        for( unsigned k=0; k<v.getNumChildren(); k++ ){
133
215222
          Node n = v[k];
134
107611
          std::map< TNode, int >::iterator itv = d_var_num.find( n );
135
107611
          if( itv!=d_var_num.end() ){
136
93506
            Trace("qcf-opt") << "  arg " << k << " is var #" << itv->second << std::endl;
137
93506
            if( std::find( d_var_rel_dom[itv->second][f].begin(), d_var_rel_dom[itv->second][f].end(), k )==d_var_rel_dom[itv->second][f].end() ){
138
88112
              d_var_rel_dom[itv->second][f].push_back( k );
139
            }
140
          }
141
        }
142
      }
143
    }
144
  }
145
21086
}
146
147
202986
void QuantInfo::getPropagateVars( QuantConflictFind * p, std::vector< TNode >& vars, TNode n, bool pol, std::map< TNode, bool >& visited ){
148
202986
  std::map< TNode, bool >::iterator itv = visited.find( n );
149
202986
  if( itv==visited.end() ){
150
146977
    visited[n] = true;
151
146977
    bool rec = true;
152
146977
    bool newPol = pol;
153
146977
    if( d_var_num.find( n )!=d_var_num.end() ){
154
77338
      Assert(std::find(vars.begin(), vars.end(), n) == vars.end());
155
77338
      vars.push_back( n );
156
154676
      TNode f = p->getTermDatabase()->getMatchOperator( n );
157
77338
      if( !f.isNull() ){
158
46798
        if( std::find( p->d_func_rel_dom[f].begin(), p->d_func_rel_dom[f].end(), d_q )==p->d_func_rel_dom[f].end() ){
159
35607
          p->d_func_rel_dom[f].push_back( d_q );
160
        }
161
      }
162
69639
    }else if( MatchGen::isHandledBoolConnective( n ) ){
163
27878
      Assert(n.getKind() != IMPLIES);
164
27878
      QuantPhaseReq::getEntailPolarity( n, 0, true, pol, rec, newPol );
165
    }
166
146977
    Trace("qcf-opt-debug") << "getPropagateVars " << n << ", pol = " << pol << ", rec = " << rec << std::endl;
167
146977
    if( rec ){
168
327115
      for( unsigned i=0; i<n.getNumChildren(); i++ ){
169
186247
        getPropagateVars( p, vars, n[i], pol, visited );
170
      }
171
    }
172
  }
173
202986
}
174
175
2585256
bool QuantInfo::isBaseMatchComplete() {
176
2585256
  return d_vars_set.size()==(d_q[0].getNumChildren()+d_extra_var.size());
177
}
178
179
111200
void QuantInfo::registerNode( Node n, bool hasPol, bool pol, bool beneathQuant ) {
180
111200
  Trace("qcf-qregister-debug2") << "Register : " << n << std::endl;
181
111200
  if( n.getKind()==FORALL ){
182
4327
    registerNode( n[1], hasPol, pol, true );
183
  }else{
184
106873
    if( !MatchGen::isHandledBoolConnective( n ) ){
185
58895
      if (expr::hasBoundVar(n))
186
      {
187
        // literals
188
58710
        if (n.getKind() == EQUAL)
189
        {
190
98319
          for (unsigned i = 0; i < n.getNumChildren(); i++)
191
          {
192
65546
            flatten(n[i], beneathQuant);
193
          }
194
        }
195
25937
        else if (MatchGen::isHandledUfTerm(n))
196
        {
197
18491
          flatten(n, beneathQuant);
198
        }
199
7446
        else if (n.getKind() == ITE)
200
        {
201
3942
          for (unsigned i = 1; i <= 2; i++)
202
          {
203
2628
            flatten(n[i], beneathQuant);
204
          }
205
1314
          registerNode(n[0], false, pol, beneathQuant);
206
        }
207
6132
        else if (options::qcfTConstraint())
208
        {
209
          // a theory-specific predicate
210
1014
          for (unsigned i = 0; i < n.getNumChildren(); i++)
211
          {
212
676
            flatten(n[i], beneathQuant);
213
          }
214
        }
215
      }
216
    }else{
217
131137
      for( unsigned i=0; i<n.getNumChildren(); i++ ){
218
        bool newHasPol;
219
        bool newPol;
220
83159
        QuantPhaseReq::getPolarity( n, i, hasPol, pol, newHasPol, newPol );
221
        //QcfNode * qcfc = new QcfNode( d_c );
222
        //qcfc->d_parent = qcf;
223
        //qcf->d_child[i] = qcfc;
224
83159
        registerNode( n[i], newHasPol, newPol, beneathQuant );
225
      }
226
    }
227
  }
228
111200
}
229
230
281601
void QuantInfo::flatten( Node n, bool beneathQuant ) {
231
281601
  Trace("qcf-qregister-debug2") << "Flatten : " << n << std::endl;
232
281601
  if (expr::hasBoundVar(n))
233
  {
234
235862
    if( n.getKind()==BOUND_VARIABLE ){
235
123542
      d_inMatchConstraint[n] = true;
236
    }
237
235862
    if( d_var_num.find( n )==d_var_num.end() ){
238
100593
      Trace("qcf-qregister-debug2") << "Add FLATTEN VAR : " << n << std::endl;
239
100593
      d_var_num[n] = d_vars.size();
240
100593
      d_vars.push_back( n );
241
100593
      d_var_types.push_back( n.getType() );
242
100593
      d_match.push_back( TNode::null() );
243
100593
      d_match_term.push_back( TNode::null() );
244
100593
      if( n.getKind()==ITE ){
245
1314
        registerNode( n, false, false );
246
99279
      }else if( n.getKind()==BOUND_VARIABLE ){
247
6271
        d_extra_var.push_back( n );
248
      }else{
249
287268
        for( unsigned i=0; i<n.getNumChildren(); i++ ){
250
194260
          flatten( n[i], beneathQuant );
251
        }
252
      }
253
    }else{
254
135269
      Trace("qcf-qregister-debug2") << "...already processed" << std::endl;
255
    }
256
  }else{
257
45739
    Trace("qcf-qregister-debug2") << "...is ground." << std::endl;
258
  }
259
281601
}
260
261
262
124291
bool QuantInfo::reset_round( QuantConflictFind * p ) {
263
947242
  for( unsigned i=0; i<d_match.size(); i++ ){
264
822951
    d_match[i] = TNode::null();
265
822951
    d_match_term[i] = TNode::null();
266
  }
267
124291
  d_vars_set.clear();
268
124291
  d_curr_var_deq.clear();
269
124291
  d_tconstraints.clear();
270
271
124291
  d_mg->reset_round( p );
272
630572
  for( std::map< int, MatchGen * >::iterator it = d_var_mg.begin(); it != d_var_mg.end(); ++it ){
273
506281
    if (!it->second->reset_round(p))
274
    {
275
      return false;
276
    }
277
  }
278
  //now, reset for matching
279
124291
  d_mg->reset( p, false, this );
280
124291
  return true;
281
}
282
283
7040430
int QuantInfo::getCurrentRepVar( int v ) {
284
7040430
  if( v!=-1 && !d_match[v].isNull() ){
285
3996777
    int vn = getVarNum( d_match[v] );
286
3996777
    if( vn!=-1 ){
287
      //int vr = getCurrentRepVar( vn );
288
      //d_match[v] = d_vars[vr];
289
      //return vr;
290
26929
      return getCurrentRepVar( vn );
291
    }
292
  }
293
7013501
  return v;
294
}
295
296
3053762
TNode QuantInfo::getCurrentValue( TNode n ) {
297
3053762
  int v = getVarNum( n );
298
3053762
  if( v==-1 ){
299
1629582
    return n;
300
  }else{
301
1424180
    if( d_match[v].isNull() ){
302
1314667
      return n;
303
    }else{
304
109513
      Assert(getVarNum(d_match[v]) != v);
305
109513
      return getCurrentValue( d_match[v] );
306
    }
307
  }
308
}
309
310
4
TNode QuantInfo::getCurrentExpValue( TNode n ) {
311
4
  int v = getVarNum( n );
312
4
  if( v==-1 ){
313
    return n;
314
  }else{
315
4
    if( d_match[v].isNull() ){
316
      return n;
317
    }else{
318
4
      Assert(getVarNum(d_match[v]) != v);
319
4
      if( d_match_term[v].isNull() ){
320
4
        return getCurrentValue( d_match[v] );
321
      }else{
322
        return d_match_term[v];
323
      }
324
    }
325
  }
326
}
327
328
7228764
bool QuantInfo::getCurrentCanBeEqual( QuantConflictFind * p, int v, TNode n, bool chDiseq ) {
329
  //check disequalities
330
7228764
  std::map< int, std::map< TNode, int > >::iterator itd = d_curr_var_deq.find( v );
331
7228764
  if( itd!=d_curr_var_deq.end() ){
332
8155214
    for( std::map< TNode, int >::iterator it = itd->second.begin(); it != itd->second.end(); ++it ){
333
2596449
      Node cv = getCurrentValue( it->first );
334
1341317
      Debug("qcf-ccbe") << "compare " << cv << " " << n << std::endl;
335
1341317
      if( cv==n ){
336
69772
        return false;
337
1271545
      }else if( chDiseq && !isVar( n ) && !isVar( cv ) ){
338
        //they must actually be disequal if we are looking for conflicts
339
35316
        if( !p->areDisequal( n, cv ) ){
340
          //TODO : check for entailed disequal
341
342
16413
          return false;
343
        }
344
      }
345
    }
346
  }
347
7142579
  return true;
348
}
349
350
int QuantInfo::addConstraint( QuantConflictFind * p, int v, TNode n, bool polarity ) {
351
  v = getCurrentRepVar( v );
352
  int vn = getVarNum( n );
353
  vn = vn==-1 ? -1 : getCurrentRepVar( vn );
354
  n = getCurrentValue( n );
355
  return addConstraint( p, v, n, vn, polarity, false );
356
}
357
358
698195
int QuantInfo::addConstraint( QuantConflictFind * p, int v, TNode n, int vn, bool polarity, bool doRemove ) {
359
  //for handling equalities between variables, and disequalities involving variables
360
698195
  Debug("qcf-match-debug") << "- " << (doRemove ? "un" : "" ) << "constrain : " << v << " -> " << n << " (cv=" << getCurrentValue( n ) << ")";
361
698195
  Debug("qcf-match-debug") << ", (vn=" << vn << "), polarity = " << polarity << std::endl;
362
698195
  Assert(doRemove || n == getCurrentValue(n));
363
698195
  Assert(doRemove || v == getCurrentRepVar(v));
364
698195
  Assert(doRemove || vn == getCurrentRepVar(getVarNum(n)));
365
698195
  if( polarity ){
366
481058
    if( vn!=v ){
367
481058
      if( doRemove ){
368
239707
        if( vn!=-1 ){
369
          //if set to this in the opposite direction, clean up opposite instead
370
          //          std::map< int, TNode >::iterator itmn = d_match.find( vn );
371
16324
          if( d_match[vn]==d_vars[v] ){
372
            return addConstraint( p, vn, d_vars[v], v, true, true );
373
          }else{
374
            //unsetting variables equal
375
16324
            std::map< int, std::map< TNode, int > >::iterator itd = d_curr_var_deq.find( vn );
376
16324
            if( itd!=d_curr_var_deq.end() ){
377
              //remove disequalities owned by this
378
16288
              std::vector< TNode > remDeq;
379
8304
              for( std::map< TNode, int >::iterator it = itd->second.begin(); it != itd->second.end(); ++it ){
380
160
                if( it->second==v ){
381
160
                  remDeq.push_back( it->first );
382
                }
383
              }
384
8304
              for( unsigned i=0; i<remDeq.size(); i++ ){
385
160
                d_curr_var_deq[vn].erase( remDeq[i] );
386
              }
387
            }
388
          }
389
        }
390
239707
        unsetMatch( p, v );
391
239707
        return 1;
392
      }else{
393
        //std::map< int, TNode >::iterator itm = d_match.find( v );
394
241351
        bool isGroundRep = false;
395
241351
        bool isGround = false;
396
241351
        if( vn!=-1 ){
397
16524
          Debug("qcf-match-debug") << "  ...Variable bound to variable" << std::endl;
398
          //std::map< int, TNode >::iterator itmn = d_match.find( vn );
399
16524
          if( d_match[v].isNull() ){
400
            //setting variables equal
401
16524
            bool alreadySet = false;
402
16524
            if( !d_match[vn].isNull() ){
403
              alreadySet = true;
404
              Assert(!isVar(d_match[vn]));
405
            }
406
407
            //copy or check disequalities
408
16524
            std::map< int, std::map< TNode, int > >::iterator itd = d_curr_var_deq.find( v );
409
16524
            if( itd!=d_curr_var_deq.end() ){
410
10769
              for( std::map< TNode, int >::iterator it = itd->second.begin(); it != itd->second.end(); ++it ){
411
320
                Node dv = getCurrentValue( it->first );
412
160
                if( !alreadySet ){
413
160
                  if( d_curr_var_deq[vn].find( dv )==d_curr_var_deq[vn].end() ){
414
160
                    d_curr_var_deq[vn][dv] = v;
415
                  }
416
                }else{
417
                  if( !p->areMatchDisequal( d_match[vn], dv ) ){
418
                    Debug("qcf-match-debug") << "  -> fail, conflicting disequality" << std::endl;
419
                    return -1;
420
                  }
421
                }
422
              }
423
            }
424
16524
            if( alreadySet ){
425
              n = getCurrentValue( n );
426
            }
427
          }else{
428
            if( d_match[vn].isNull() ){
429
              Debug("qcf-match-debug") << " ...Reverse direction" << std::endl;
430
              //set the opposite direction
431
              return addConstraint( p, vn, d_vars[v], v, true, false );
432
            }else{
433
              Debug("qcf-match-debug") << "  -> Both variables bound, compare" << std::endl;
434
              //are they currently equal
435
              return p->areMatchEqual( d_match[v], d_match[vn] ) ? 0 : -1;
436
            }
437
          }
438
        }else{
439
224827
          Debug("qcf-match-debug") << "  ...Variable bound to ground" << std::endl;
440
224827
          if( d_match[v].isNull() ){
441
            //isGroundRep = true;   ??
442
224827
            isGround = true;
443
          }else{
444
            //compare ground values
445
            Debug("qcf-match-debug") << "  -> Ground value, compare " << d_match[v] << " "<< n << std::endl;
446
            return p->areMatchEqual( d_match[v], n ) ? 0 : -1;
447
          }
448
        }
449
241351
        if( setMatch( p, v, n, isGroundRep, isGround ) ){
450
241331
          Debug("qcf-match-debug") << "  -> success" << std::endl;
451
241331
          return 1;
452
        }else{
453
20
          Debug("qcf-match-debug") << "  -> fail, conflicting disequality" << std::endl;
454
20
          return -1;
455
        }
456
      }
457
    }else{
458
      Debug("qcf-match-debug") << "  -> redundant, variable identity" << std::endl;
459
      return 0;
460
    }
461
  }else{
462
217137
    if( vn==v ){
463
      Debug("qcf-match-debug") << "  -> fail, variable identity" << std::endl;
464
      return -1;
465
    }else{
466
217137
      if( doRemove ){
467
108252
        Assert(d_curr_var_deq[v].find(n) != d_curr_var_deq[v].end());
468
108252
        d_curr_var_deq[v].erase( n );
469
108252
        return 1;
470
      }else{
471
108885
        if( d_curr_var_deq[v].find( n )==d_curr_var_deq[v].end() ){
472
          //check if it respects equality
473
          //std::map< int, TNode >::iterator itm = d_match.find( v );
474
108765
          if( !d_match[v].isNull() ){
475
            TNode nv = getCurrentValue( n );
476
            if( !p->areMatchDisequal( nv, d_match[v] ) ){
477
              Debug("qcf-match-debug") << "  -> fail, conflicting disequality" << std::endl;
478
              return -1;
479
            }
480
          }
481
108765
          d_curr_var_deq[v][n] = v;
482
108765
          Debug("qcf-match-debug") << "  -> success" << std::endl;
483
108765
          return 1;
484
        }else{
485
120
          Debug("qcf-match-debug") << "  -> redundant disequality" << std::endl;
486
120
          return 0;
487
        }
488
      }
489
    }
490
  }
491
}
492
493
88
bool QuantInfo::isConstrainedVar( int v ) {
494
88
  if( d_curr_var_deq.find( v )!=d_curr_var_deq.end() && !d_curr_var_deq[v].empty() ){
495
    return true;
496
  }else{
497
176
    Node vv = getVar( v );
498
    //for( std::map< int, TNode >::iterator it = d_match.begin(); it != d_match.end(); ++it ){
499
1200
    for( unsigned i=0; i<d_match.size(); i++ ){
500
1112
      if( d_match[i]==vv ){
501
        return true;
502
      }
503
    }
504
616
    for( std::map< int, std::map< TNode, int > >::iterator it = d_curr_var_deq.begin(); it != d_curr_var_deq.end(); ++it ){
505
592
      for( std::map< TNode, int >::iterator it2 = it->second.begin(); it2 != it->second.end(); ++it2 ){
506
64
        if( it2->first==vv ){
507
          return true;
508
        }
509
      }
510
    }
511
88
    return false;
512
  }
513
}
514
515
4509106
bool QuantInfo::setMatch( QuantConflictFind * p, int v, TNode n, bool isGroundRep, bool isGround ) {
516
4509106
  if( getCurrentCanBeEqual( p, v, n ) ){
517
4462090
    if( isGroundRep ){
518
      //fail if n does not exist in the relevant domain of each of the argument positions
519
4219455
      std::map< int, std::map< TNode, std::vector< unsigned > > >::iterator it = d_var_rel_dom.find( v );
520
4219455
      if( it!=d_var_rel_dom.end() ){
521
3310718
        for( std::map< TNode, std::vector< unsigned > >::iterator it2 = it->second.begin(); it2 != it->second.end(); ++it2 ){
522
3987439
          for( unsigned j=0; j<it2->second.size(); j++ ){
523
2138959
            Debug("qcf-match-debug2") << n << " in relevant domain " <<  it2->first << "." << it2->second[j] << "?" << std::endl;
524
2138959
            if( !p->getTermDatabase()->inRelevantDomain( it2->first, it2->second[j], n ) ){
525
216893
              Debug("qcf-match-debug") << "  -> fail, since " << n << " is not in relevant domain of " << it2->first << "." << it2->second[j] << std::endl;
526
216893
              return false;
527
            }
528
          }
529
        }
530
      }
531
    }
532
4245197
    Debug("qcf-match-debug") << "-- bind : " << v << " -> " << n << ", checked " <<  d_curr_var_deq[v].size() << " disequalities" << std::endl;
533
4245197
    if( isGround ){
534
4228673
      if( d_vars[v].getKind()==BOUND_VARIABLE ){
535
1789785
        d_vars_set[v] = true;
536
1789785
        Debug("qcf-match-debug") << "---- now bound " << d_vars_set.size() << " / " << d_q[0].getNumChildren() << " base variables." << std::endl;
537
      }
538
    }
539
4245197
    d_match[v] = n;
540
4245197
    return true;
541
  }else{
542
47016
    return false;
543
  }
544
}
545
546
2705118
void QuantInfo::unsetMatch( QuantConflictFind * p, int v ) {
547
2705118
  Debug("qcf-match-debug") << "-- unbind : " << v << std::endl;
548
2705118
  if( d_vars[v].getKind()==BOUND_VARIABLE && d_vars_set.find( v )!=d_vars_set.end() ){
549
1010743
    d_vars_set.erase( v );
550
  }
551
2705118
  d_match[ v ] = TNode::null();
552
2705118
}
553
554
494334
bool QuantInfo::isMatchSpurious( QuantConflictFind * p ) {
555
3982122
  for( int i=0; i<getNumVars(); i++ ){
556
    //std::map< int, TNode >::iterator it = d_match.find( i );
557
3526957
    if( !d_match[i].isNull() ){
558
2719658
      if (!getCurrentCanBeEqual(p, i, d_match[i], p->atConflictEffort())) {
559
39169
        return true;
560
      }
561
    }
562
  }
563
455165
  return false;
564
}
565
566
454979
bool QuantInfo::isTConstraintSpurious(QuantConflictFind* p,
567
                                      std::vector<Node>& terms)
568
{
569
1862336
  if( options::qcfEagerTest() ){
570
    //check whether the instantiation evaluates as expected
571
454979
    if (p->atConflictEffort()) {
572
268008
      Trace("qcf-instance-check") << "Possible conflict instance for " << d_q << " : " << std::endl;
573
268798
      std::map< TNode, TNode > subs;
574
1053300
      for( unsigned i=0; i<terms.size(); i++ ){
575
785292
        Trace("qcf-instance-check") << "  " << terms[i] << std::endl;
576
785292
        subs[d_q[0][i]] = terms[i];
577
      }
578
268008
      TermDb* tdb = p->getTermDatabase();
579
268012
      for( unsigned i=0; i<d_extra_var.size(); i++ ){
580
8
        Node n = getCurrentExpValue( d_extra_var[i] );
581
4
        Trace("qcf-instance-check") << "  " << d_extra_var[i] << " -> " << n << std::endl;
582
4
        subs[d_extra_var[i]] = n;
583
      }
584
268008
      if (!tdb->isEntailed(d_q[1], subs, false, false))
585
      {
586
267218
        Trace("qcf-instance-check") << "...not entailed to be false." << std::endl;
587
267218
        return true;
588
      }
589
    }else{
590
      Node inst =
591
188252
          p->d_quantEngine->getInstantiate()->getInstantiation(d_q, terms);
592
186971
      inst = Rewriter::rewrite(inst);
593
      Node inst_eval = p->getTermDatabase()->evaluateTerm(
594
188252
          inst, options::qcfTConstraint(), true);
595
186971
      if( Trace.isOn("qcf-instance-check") ){
596
        Trace("qcf-instance-check") << "Possible propagating instance for " << d_q << " : " << std::endl;
597
        for( unsigned i=0; i<terms.size(); i++ ){
598
          Trace("qcf-instance-check") << "  " << terms[i] << std::endl;
599
        }
600
        Trace("qcf-instance-check") << "...evaluates to " << inst_eval << std::endl;
601
      }
602
373942
      if (inst_eval.isNull()
603
186971
          || (inst_eval.isConst() && inst_eval.getConst<bool>()))
604
      {
605
185690
        Trace("qcf-instance-check") << "...spurious." << std::endl;
606
185690
        return true;
607
      }else{
608
1281
        if (Configuration::isDebugBuild())
609
        {
610
1281
          if (!p->isPropagatingInstance(inst_eval))
611
          {
612
            // Notice that this can happen in cases where:
613
            // (1) x = -1*y is rewritten to y = -1*x, and
614
            // (2) -1*y is a term in the master equality engine but -1*x is not.
615
            // In other words, we determined that x = -1*y is a relevant
616
            // equality to propagate since it involves two known terms, but
617
            // after rewriting, the equality y = -1*x involves an unknown term
618
            // -1*x. In this case, the equality is still relevant to propagate,
619
            // despite the above function not being precise enough to realize
620
            // it. We output a warning in debug for this. See #2993.
621
            Trace("qcf-instance-check")
622
                << "WARNING: not propagating." << std::endl;
623
          }
624
        }
625
1281
        Trace("qcf-instance-check") << "...not spurious." << std::endl;
626
      }
627
    }
628
  }
629
2071
  if( !d_tconstraints.empty() ){
630
    //check constraints
631
28
    for( std::map< Node, bool >::iterator it = d_tconstraints.begin(); it != d_tconstraints.end(); ++it ){
632
      //apply substitution to the tconstraint
633
16
      Node cons = p->getQuantifiersRegistry().substituteBoundVariables(
634
32
          it->first, d_q, terms);
635
16
      cons = it->second ? cons : cons.negate();
636
16
      if (!entailmentTest(p, cons, p->atConflictEffort())) {
637
        return true;
638
      }
639
    }
640
  }
641
  // spurious if quantifiers engine is in conflict
642
2071
  return p->d_qstate.isInConflict();
643
}
644
645
16
bool QuantInfo::entailmentTest( QuantConflictFind * p, Node lit, bool chEnt ) {
646
16
  Trace("qcf-tconstraint-debug") << "Check : " << lit << std::endl;
647
32
  Node rew = Rewriter::rewrite( lit );
648
16
  if (rew.isConst())
649
  {
650
8
    Trace("qcf-tconstraint-debug") << "...constraint " << lit << " rewrites to "
651
4
                                   << rew << "." << std::endl;
652
4
    return rew.getConst<bool>();
653
  }
654
  // if checking for conflicts, we must be sure that the (negation of)
655
  // constraint is (not) entailed
656
12
  if (!chEnt)
657
  {
658
12
    rew = Rewriter::rewrite(rew.negate());
659
  }
660
  // check if it is entailed
661
24
  Trace("qcf-tconstraint-debug")
662
12
      << "Check entailment of " << rew << "..." << std::endl;
663
12
  std::pair<bool, Node> et = p->getState().getValuation().entailmentCheck(
664
24
      options::TheoryOfMode::THEORY_OF_TYPE_BASED, rew);
665
12
  ++(p->d_statistics.d_entailment_checks);
666
24
  Trace("qcf-tconstraint-debug")
667
12
      << "ET result : " << et.first << " " << et.second << std::endl;
668
12
  if (!et.first)
669
  {
670
24
    Trace("qcf-tconstraint-debug")
671
12
        << "...cannot show entailment of " << rew << "." << std::endl;
672
12
    return !chEnt;
673
  }
674
  return chEnt;
675
}
676
677
455109
bool QuantInfo::completeMatch( QuantConflictFind * p, std::vector< int >& assigned, bool doContinue ) {
678
  //assign values for variables that were unassigned (usually not necessary, but handles corner cases)
679
455109
  bool doFail = false;
680
455109
  bool success = true;
681
455109
  if( doContinue ){
682
    doFail = true;
683
    success = false;
684
  }else{
685
455109
    if( isBaseMatchComplete() && options::qcfEagerTest() ){
686
454918
      return true;
687
    }
688
    //solve for interpreted symbol matches
689
    //   this breaks the invariant that all introduced constraints are over existing terms
690
199
    for( int i=(int)(d_tsym_vars.size()-1); i>=0; i-- ){
691
8
      int index = d_tsym_vars[i];
692
16
      TNode v = getCurrentValue( d_vars[index] );
693
8
      int slv_v = -1;
694
8
      if( v==d_vars[index] ){
695
8
        slv_v = index;
696
      }
697
8
      Trace("qcf-tconstraint-debug") << "Solve " << d_vars[index] << " = " << v << " " << d_vars[index].getKind() << std::endl;
698
8
      if( d_vars[index].getKind()==PLUS || d_vars[index].getKind()==MULT ){
699
8
        Kind k = d_vars[index].getKind();
700
16
        std::vector< TNode > children;
701
24
        for( unsigned j=0; j<d_vars[index].getNumChildren(); j++ ){
702
16
          int vn = getVarNum( d_vars[index][j] );
703
16
          if( vn!=-1 ){
704
24
            TNode vv = getCurrentValue( d_vars[index][j] );
705
12
            if( vv==d_vars[index][j] ){
706
              //we will assign this
707
8
              if( slv_v==-1 ){
708
                Trace("qcf-tconstraint-debug") << "...will solve for var #" << vn << std::endl;
709
                slv_v = vn;
710
                if (!p->atConflictEffort()) {
711
                  break;
712
                }
713
              }else{
714
16
                Node z = p->getZero( k );
715
8
                if( !z.isNull() ){
716
4
                  Trace("qcf-tconstraint-debug") << "...set " << d_vars[vn] << " = " << z << std::endl;
717
4
                  assigned.push_back( vn );
718
4
                  if( !setMatch( p, vn, z, false, true ) ){
719
                    success = false;
720
                    break;
721
                  }
722
                }
723
              }
724
            }else{
725
4
              Trace("qcf-tconstraint-debug") << "...sum value " << vv << std::endl;
726
4
              children.push_back( vv );
727
            }
728
          }else{
729
4
            Trace("qcf-tconstraint-debug") << "...sum " << d_vars[index][j] << std::endl;
730
4
            children.push_back( d_vars[index][j] );
731
          }
732
        }
733
8
        if( success ){
734
8
          if( slv_v!=-1 ){
735
16
            Node lhs;
736
8
            if( children.empty() ){
737
              lhs = p->getZero( k );
738
8
            }else if( children.size()==1 ){
739
8
              lhs = children[0];
740
            }else{
741
              lhs = NodeManager::currentNM()->mkNode( k, children );
742
            }
743
16
            Node sum;
744
8
            if( v==d_vars[index] ){
745
8
              sum = lhs;
746
            }else{
747
              if (p->atConflictEffort()) {
748
                Kind kn = k;
749
                if( d_vars[index].getKind()==PLUS ){
750
                  kn = MINUS;
751
                }
752
                if( kn!=k ){
753
                  sum = NodeManager::currentNM()->mkNode( kn, v, lhs );
754
                }
755
              }
756
            }
757
8
            if( !sum.isNull() ){
758
8
              assigned.push_back( slv_v );
759
8
              Trace("qcf-tconstraint-debug") << "...set " << d_vars[slv_v] << " = " << sum << std::endl;
760
8
              if( !setMatch( p, slv_v, sum, false, true ) ){
761
                success = false;
762
              }
763
8
              p->d_tempCache.push_back( sum );
764
            }
765
          }else{
766
            //must show that constraint is met
767
            Node sum = NodeManager::currentNM()->mkNode( k, children );
768
            Node eq = sum.eqNode( v );
769
            if( !entailmentTest( p, eq ) ){
770
              success = false;
771
            }
772
            p->d_tempCache.push_back( sum );
773
          }
774
        }
775
      }
776
777
8
      if( !success ){
778
        break;
779
      }
780
    }
781
191
    if( success ){
782
      //check what is left to assign
783
191
      d_unassigned.clear();
784
191
      d_unassigned_tn.clear();
785
382
      std::vector< int > unassigned[2];
786
382
      std::vector< TypeNode > unassigned_tn[2];
787
587
      for( int i=0; i<getNumVars(); i++ ){
788
396
        if( d_match[i].isNull() ){
789
318
          int rindex = d_var_mg.find( i )==d_var_mg.end() ? 1 : 0;
790
318
          unassigned[rindex].push_back( i );
791
318
          unassigned_tn[rindex].push_back( getVar( i ).getType() );
792
318
          assigned.push_back( i );
793
        }
794
      }
795
191
      d_unassigned_nvar = unassigned[0].size();
796
573
      for( unsigned i=0; i<2; i++ ){
797
382
        d_unassigned.insert( d_unassigned.end(), unassigned[i].begin(), unassigned[i].end() );
798
382
        d_unassigned_tn.insert( d_unassigned_tn.end(), unassigned_tn[i].begin(), unassigned_tn[i].end() );
799
      }
800
191
      d_una_eqc_count.clear();
801
191
      d_una_index = 0;
802
    }
803
  }
804
805
191
  if( !d_unassigned.empty() && ( success || doContinue ) ){
806
186
    Trace("qcf-check") << "Assign to unassigned (" << d_unassigned.size() << ")..." << std::endl;
807
184
    do {
808
370
      if( doFail ){
809
184
        Trace("qcf-check-unassign") << "Failure, try again..." << std::endl;
810
      }
811
370
      bool invalidMatch = false;
812
2822
      while( ( d_una_index>=0 && (int)d_una_index<(int)d_unassigned.size() ) || invalidMatch || doFail ){
813
1226
        invalidMatch = false;
814
1226
        if( !doFail && d_una_index==(int)d_una_eqc_count.size() ){
815
          //check if it has now been assigned
816
324
          if( d_una_index<d_unassigned_nvar ){
817
44
            if( !isConstrainedVar( d_unassigned[d_una_index] ) ){
818
44
              d_una_eqc_count.push_back( -1 );
819
            }else{
820
              d_var_mg[ d_unassigned[d_una_index] ]->reset( p, true, this );
821
              d_una_eqc_count.push_back( 0 );
822
            }
823
          }else{
824
280
            d_una_eqc_count.push_back( 0 );
825
          }
826
        }else{
827
902
          bool failed = false;
828
902
          if( !doFail ){
829
718
            if( d_una_index<d_unassigned_nvar ){
830
44
              if( !isConstrainedVar( d_unassigned[d_una_index] ) ){
831
44
                Trace("qcf-check-unassign") << "Succeeded, variable unconstrained at " << d_una_index << std::endl;
832
44
                d_una_index++;
833
              }else if( d_var_mg[d_unassigned[d_una_index]]->getNextMatch( p, this ) ){
834
                Trace("qcf-check-unassign") << "Succeeded match with mg at " << d_una_index << std::endl;
835
                d_una_index++;
836
              }else{
837
                failed = true;
838
                Trace("qcf-check-unassign") << "Failed match with mg at " << d_una_index << std::endl;
839
              }
840
            }else{
841
674
              Assert(doFail || d_una_index == (int)d_una_eqc_count.size() - 1);
842
674
              if( d_una_eqc_count[d_una_index]<(int)p->d_eqcs[d_unassigned_tn[d_una_index]].size() ){
843
471
                int currIndex = d_una_eqc_count[d_una_index];
844
471
                d_una_eqc_count[d_una_index]++;
845
471
                Trace("qcf-check-unassign") << d_unassigned[d_una_index] << "->" << p->d_eqcs[d_unassigned_tn[d_una_index]][currIndex] << std::endl;
846
471
                if( setMatch( p, d_unassigned[d_una_index], p->d_eqcs[d_unassigned_tn[d_una_index]][currIndex], true, true ) ){
847
334
                  d_match_term[d_unassigned[d_una_index]] = TNode::null();
848
334
                  Trace("qcf-check-unassign") << "Succeeded match " << d_una_index << std::endl;
849
334
                  d_una_index++;
850
                }else{
851
137
                  Trace("qcf-check-unassign") << "Failed match " << d_una_index << std::endl;
852
137
                  invalidMatch = true;
853
                }
854
              }else{
855
203
                failed = true;
856
203
                Trace("qcf-check-unassign") << "No more matches " << d_una_index << std::endl;
857
              }
858
            }
859
          }
860
902
          if( doFail || failed ){
861
            do{
862
387
              if( !doFail ){
863
203
                d_una_eqc_count.pop_back();
864
              }else{
865
184
                doFail = false;
866
              }
867
387
              d_una_index--;
868
387
            }while( d_una_index>=0 && d_una_eqc_count[d_una_index]==-1 );
869
          }
870
        }
871
      }
872
370
      success = d_una_index>=0;
873
370
      if( success ){
874
240
        doFail = true;
875
240
        Trace("qcf-check-unassign") << "  Try: " << std::endl;
876
680
        for( unsigned i=0; i<d_unassigned.size(); i++ ){
877
440
          int ui = d_unassigned[i];
878
440
          if( !d_match[ui].isNull() ){
879
396
            Trace("qcf-check-unassign") << "  Assigned #" << ui << " : " << d_vars[ui] << " -> " << d_match[ui] << std::endl;
880
          }
881
        }
882
      }
883
370
    }while( success && isMatchSpurious( p ) );
884
186
    Trace("qcf-check") << "done assigning." << std::endl;
885
  }
886
191
  if( success ){
887
182
    for( unsigned i=0; i<d_unassigned.size(); i++ ){
888
121
      int ui = d_unassigned[i];
889
121
      if( !d_match[ui].isNull() ){
890
77
        Trace("qcf-check") << "  Assigned #" << ui << " : " << d_vars[ui] << " -> " << d_match[ui] << std::endl;
891
      }
892
    }
893
61
    return true;
894
  }else{
895
130
    revertMatch( p, assigned );
896
130
    assigned.clear();
897
130
    return false;
898
  }
899
}
900
901
454979
void QuantInfo::getMatch( std::vector< Node >& terms ){
902
1769260
  for( unsigned i=0; i<d_q[0].getNumChildren(); i++ ){
903
    //Node cv = qi->getCurrentValue( qi->d_match[i] );
904
1314281
    int repVar = getCurrentRepVar( i );
905
2628562
    Node cv;
906
    //std::map< int, TNode >::iterator itmt = qi->d_match_term.find( repVar );
907
1314281
    if( !d_match_term[repVar].isNull() ){
908
1307534
      cv = d_match_term[repVar];
909
    }else{
910
6747
      cv = d_match[repVar];
911
    }
912
1314281
    Debug("qcf-check-inst") << "INST : " << i << " -> " << cv << ", from " << d_match[i] << std::endl;
913
1314281
    terms.push_back( cv );
914
  }
915
454979
}
916
917
454218
void QuantInfo::revertMatch( QuantConflictFind * p, std::vector< int >& assigned ) {
918
454504
  for( unsigned i=0; i<assigned.size(); i++ ){
919
286
    unsetMatch( p, assigned[i] );
920
  }
921
454218
}
922
923
void QuantInfo::debugPrintMatch( const char * c ) {
924
  for( int i=0; i<getNumVars(); i++ ){
925
    Trace(c) << "  " << d_vars[i] << " -> ";
926
    if( !d_match[i].isNull() ){
927
      Trace(c) << d_match[i];
928
    }else{
929
      Trace(c) << "(unassigned) ";
930
    }
931
    if( !d_curr_var_deq[i].empty() ){
932
      Trace(c) << ", DEQ{ ";
933
      for( std::map< TNode, int >::iterator it = d_curr_var_deq[i].begin(); it != d_curr_var_deq[i].end(); ++it ){
934
        Trace(c) << it->first << " ";
935
      }
936
      Trace(c) << "}";
937
    }
938
    if( !d_match_term[i].isNull() && d_match_term[i]!=d_match[i] ){
939
      Trace(c) << ", EXP : " << d_match_term[i];
940
    }
941
    Trace(c) <<  std::endl;
942
  }
943
  if( !d_tconstraints.empty() ){
944
    Trace(c) << "ADDITIONAL CONSTRAINTS : " << std::endl;
945
    for( std::map< Node, bool >::iterator it = d_tconstraints.begin(); it != d_tconstraints.end(); ++it ){
946
      Trace(c) << "   " << it->first << " -> " << it->second << std::endl;
947
    }
948
  }
949
}
950
951
MatchGen::MatchGen()
952
  : d_matched_basis(),
953
    d_binding(),
954
    d_tgt(),
955
    d_tgt_orig(),
956
    d_wasSet(),
957
    d_n(),
958
    d_type( typ_invalid ),
959
    d_type_not()
960
{
961
  d_qni_size = 0;
962
  d_child_counter = -1;
963
  d_use_children = true;
964
}
965
966
967
153387
MatchGen::MatchGen( QuantInfo * qi, Node n, bool isVar )
968
  : d_matched_basis(),
969
    d_binding(),
970
    d_tgt(),
971
    d_tgt_orig(),
972
    d_wasSet(),
973
    d_n(),
974
    d_type(),
975
153387
    d_type_not()
976
{
977
  //initialize temporary
978
153387
  d_child_counter = -1;
979
153387
  d_use_children = true;
980
981
153387
  Trace("qcf-qregister-debug") << "Make match gen for " << n << ", isVar = " << isVar << std::endl;
982
306774
  std::vector< Node > qni_apps;
983
153387
  d_qni_size = 0;
984
153387
  if( isVar ){
985
77515
    Assert(qi->d_var_num.find(n) != qi->d_var_num.end());
986
    // rare case where we have a free variable in an operator, we are invalid
987
155030
    if (n.getKind() == ITE
988
156160
        || (options::ufHo() && n.getKind() == APPLY_UF
989
90983
            && expr::hasFreeVar(n.getOperator())))
990
    {
991
1130
      d_type = typ_invalid;
992
    }else{
993
76385
      d_type = isHandledUfTerm( n ) ? typ_var : typ_tsym;
994
76385
      d_qni_var_num[0] = qi->getVarNum( n );
995
76385
      d_qni_size++;
996
76385
      d_type_not = false;
997
76385
      d_n = n;
998
      //Node f = getMatchOperator( n );
999
240503
      for( unsigned j=0; j<d_n.getNumChildren(); j++ ){
1000
328236
        Node nn = d_n[j];
1001
164118
        Trace("qcf-qregister-debug") << "  " << d_qni_size;
1002
164118
        if( qi->isVar( nn ) ){
1003
141663
          int v = qi->d_var_num[nn];
1004
141663
          Trace("qcf-qregister-debug") << " is var #" << v << std::endl;
1005
141663
          d_qni_var_num[d_qni_size] = v;
1006
          //qi->addFuncParent( v, f, j );
1007
        }else{
1008
22455
          Trace("qcf-qregister-debug") << " is gterm " << nn << std::endl;
1009
22455
          d_qni_gterm[d_qni_size] = nn;
1010
        }
1011
164118
        d_qni_size++;
1012
      }
1013
    }
1014
  }else{
1015
75872
    if (expr::hasBoundVar(n))
1016
    {
1017
75707
      d_type_not = false;
1018
75707
      d_n = n;
1019
75707
      if( d_n.getKind()==NOT ){
1020
24054
        d_n = d_n[0];
1021
24054
        d_type_not = !d_type_not;
1022
      }
1023
1024
75707
      if( isHandledBoolConnective( d_n ) ){
1025
        //non-literals
1026
24936
        d_type = typ_formula;
1027
80345
        for( unsigned i=0; i<d_n.getNumChildren(); i++ ){
1028
59007
          if( d_n.getKind()!=FORALL || i==1 ){
1029
54786
            d_children.push_back( MatchGen( qi, d_n[i], false ) );
1030
54786
            if( !d_children[d_children.size()-1].isValid() ){
1031
3598
              setInvalid();
1032
3598
              break;
1033
            }
1034
          }
1035
        }
1036
      }else{
1037
50771
        d_type = typ_invalid;
1038
        //literals
1039
50771
        if( isHandledUfTerm( d_n ) ){
1040
17602
          Assert(qi->isVar(d_n));
1041
17602
          d_type = typ_pred;
1042
33169
        }else if( d_n.getKind()==BOUND_VARIABLE ){
1043
147
          Assert(d_n.getType().isBoolean());
1044
147
          d_type = typ_bool_var;
1045
33022
        }else if( d_n.getKind()==EQUAL || options::qcfTConstraint() ){
1046
90915
          for (unsigned i = 0; i < d_n.getNumChildren(); i++)
1047
          {
1048
60610
            if (expr::hasBoundVar(d_n[i]))
1049
            {
1050
44760
              if (!qi->isVar(d_n[i]))
1051
              {
1052
                Trace("qcf-qregister-debug")
1053
                    << "ERROR : not var " << d_n[i] << std::endl;
1054
              }
1055
44760
              Assert(qi->isVar(d_n[i]));
1056
44760
              if (d_n.getKind() != EQUAL && qi->isVar(d_n[i]))
1057
              {
1058
338
                d_qni_var_num[i + 1] = qi->d_var_num[d_n[i]];
1059
              }
1060
            }
1061
            else
1062
            {
1063
15850
              d_qni_gterm[i] = d_n[i];
1064
            }
1065
          }
1066
30305
          d_type = d_n.getKind() == EQUAL ? typ_eq : typ_tconstraint;
1067
30305
          Trace("qcf-tconstraint") << "T-Constraint : " << d_n << std::endl;
1068
        }
1069
      }
1070
    }else{
1071
      //we will just evaluate
1072
165
      d_n = n;
1073
165
      d_type = typ_ground;
1074
    }
1075
  }
1076
153387
  Trace("qcf-qregister-debug")  << "Done make match gen " << n << ", type = ";
1077
153387
  debugPrintType( "qcf-qregister-debug", d_type, true );
1078
153387
  Trace("qcf-qregister-debug") << std::endl;
1079
  //Assert( d_children.size()==d_children_order.size() );
1080
1081
153387
}
1082
1083
472807
void MatchGen::collectBoundVar( QuantInfo * qi, Node n, std::vector< int >& cbvars, std::map< Node, bool >& visited, bool& hasNested ) {
1084
472807
  if( visited.find( n )==visited.end() ){
1085
404369
    visited[n] = true;
1086
404369
    if( n.getKind()==FORALL ){
1087
3582
      hasNested = true;
1088
    }
1089
404369
    int v = qi->getVarNum( n );
1090
404369
    if( v!=-1 && std::find( cbvars.begin(), cbvars.end(), v )==cbvars.end() ){
1091
260074
      cbvars.push_back( v );
1092
    }
1093
833188
    for( unsigned i=0; i<n.getNumChildren(); i++ ){
1094
428819
      collectBoundVar( qi, n[i], cbvars, visited, hasNested );
1095
    }
1096
  }
1097
472807
}
1098
1099
137112
void MatchGen::determineVariableOrder( QuantInfo * qi, std::vector< int >& bvars ) {
1100
137112
  Trace("qcf-qregister-debug") << "Determine variable order " << d_n << ", #bvars = " << bvars.size() << std::endl;
1101
137112
  bool isComm = d_type==typ_formula && ( d_n.getKind()==OR || d_n.getKind()==AND || d_n.getKind()==EQUAL );
1102
137112
  if( isComm ){
1103
31290
    std::map< int, std::vector< int > > c_to_vars;
1104
31290
    std::map< int, std::vector< int > > vars_to_c;
1105
31290
    std::map< int, int > vb_count;
1106
31290
    std::map< int, int > vu_count;
1107
31290
    std::map< int, bool > has_nested;
1108
31290
    std::vector< bool > assigned;
1109
15645
    Trace("qcf-qregister-debug") << "Calculate bound variables..." << std::endl;
1110
55552
    for( unsigned i=0; i<d_children.size(); i++ ){
1111
79814
      std::map< Node, bool > visited;
1112
39907
      has_nested[i] = false;
1113
39907
      collectBoundVar( qi, d_children[i].d_n, c_to_vars[i], visited, has_nested[i] );
1114
39907
      assigned.push_back( false );
1115
39907
      vb_count[i] = 0;
1116
39907
      vu_count[i] = 0;
1117
246399
      for( unsigned j=0; j<c_to_vars[i].size(); j++ ){
1118
206492
        int v = c_to_vars[i][j];
1119
206492
        vars_to_c[v].push_back( i );
1120
206492
        if( std::find( bvars.begin(), bvars.end(), v )==bvars.end() ){
1121
188394
          vu_count[i]++;
1122
        }else{
1123
18098
          vb_count[i]++;
1124
        }
1125
      }
1126
    }
1127
    //children that bind no unbound variable, then the most number of bound, unbound variables go first
1128
15645
    Trace("qcf-qregister-vo") << "Variable order for " << d_n << " : " << std::endl;
1129
24262
    do {
1130
39907
      int min_score0 = -1;
1131
39907
      int min_score = -1;
1132
39907
      int min_score_index = -1;
1133
747248
      for( unsigned i=0; i<d_children.size(); i++ ){
1134
707341
        if( !assigned[i] ){
1135
373624
          Trace("qcf-qregister-debug2") << "Child " << i << " has b/ub : " << vb_count[i] << "/" << vu_count[i] << std::endl;
1136
373624
          int score0 = 0;//has_nested[i] ? 0 : 1;
1137
          int score;
1138
747248
          if( !options::qcfVoExp() ){
1139
373624
            score = vu_count[i];
1140
          }else{
1141
            score =  vu_count[i]==0 ? 0 : ( 1 + qi->d_vars.size()*( qi->d_vars.size() - vb_count[i] ) + ( qi->d_vars.size() - vu_count[i] )  );
1142
          }
1143
373624
          if( min_score==-1 || score0<min_score0 || ( score0==min_score0 && score<min_score ) ){
1144
68122
            min_score0 = score0;
1145
68122
            min_score = score;
1146
68122
            min_score_index = i;
1147
          }
1148
        }
1149
      }
1150
39907
      Trace("qcf-qregister-vo") << "  " << d_children_order.size()+1 << ": " << d_children[min_score_index].d_n << " : ";
1151
39907
      Trace("qcf-qregister-vo") << vu_count[min_score_index] << " " << vb_count[min_score_index] << " " << has_nested[min_score_index] << std::endl;
1152
39907
      Trace("qcf-qregister-debug") << "...assign child " << min_score_index << std::endl;
1153
39907
      Trace("qcf-qregister-debug") << "...score : " << min_score << std::endl;
1154
39907
      Assert(min_score_index != -1);
1155
      //add to children order
1156
39907
      d_children_order.push_back( min_score_index );
1157
39907
      assigned[min_score_index] = true;
1158
      //determine order internal to children
1159
39907
      d_children[min_score_index].determineVariableOrder( qi, bvars );
1160
39907
      Trace("qcf-qregister-debug")  << "...bind variables" << std::endl;
1161
      //now, make it a bound variable
1162
39907
      if( vu_count[min_score_index]>0 ){
1163
226873
        for( unsigned i=0; i<c_to_vars[min_score_index].size(); i++ ){
1164
189390
          int v = c_to_vars[min_score_index][i];
1165
189390
          if( std::find( bvars.begin(), bvars.end(), v )==bvars.end() ){
1166
240396
            for( unsigned j=0; j<vars_to_c[v].size(); j++ ){
1167
156938
              int vc = vars_to_c[v][j];
1168
156938
              vu_count[vc]--;
1169
156938
              vb_count[vc]++;
1170
            }
1171
83458
            bvars.push_back( v );
1172
          }
1173
        }
1174
      }
1175
39907
      Trace("qcf-qregister-debug") << "...done assign child " << min_score_index << std::endl;
1176
39907
    }while( d_children_order.size()!=d_children.size() );
1177
15645
    Trace("qcf-qregister-debug") << "Done assign variable ordering for " << d_n << std::endl;
1178
  }else{
1179
125548
    for( unsigned i=0; i<d_children.size(); i++ ){
1180
4081
      d_children_order.push_back( i );
1181
4081
      d_children[i].determineVariableOrder( qi, bvars );
1182
      //now add to bvars
1183
8162
      std::map< Node, bool > visited;
1184
8162
      std::vector< int > cvars;
1185
4081
      bool has_nested = false;
1186
4081
      collectBoundVar( qi, d_children[i].d_n, cvars, visited, has_nested );
1187
57663
      for( unsigned j=0; j<cvars.size(); j++ ){
1188
53582
        if( std::find( bvars.begin(), bvars.end(), cvars[j] )==bvars.end() ){
1189
5931
          bvars.push_back( cvars[j] );
1190
        }
1191
      }
1192
    }
1193
  }
1194
137112
}
1195
1196
1010784
bool MatchGen::reset_round(QuantConflictFind* p)
1197
{
1198
1010784
  d_wasSet = false;
1199
1390996
  for( unsigned i=0; i<d_children.size(); i++ ){
1200
380212
    if (!d_children[i].reset_round(p))
1201
    {
1202
      return false;
1203
    }
1204
  }
1205
1010784
  if( d_type==typ_ground ){
1206
    // int e = p->evaluate( d_n );
1207
    // if( e==1 ){
1208
    //  d_ground_eval[0] = p->d_true;
1209
    //}else if( e==-1 ){
1210
    //  d_ground_eval[0] = p->d_false;
1211
    //}
1212
    // modified
1213
2787
    TermDb* tdb = p->getTermDatabase();
1214
2787
    QuantifiersState& qs = p->getState();
1215
8361
    for (unsigned i = 0; i < 2; i++)
1216
    {
1217
5574
      if (tdb->isEntailed(d_n, i == 0))
1218
      {
1219
680
        d_ground_eval[0] = i==0 ? p->d_true : p->d_false;
1220
      }
1221
5574
      if (qs.isInConflict())
1222
      {
1223
        return false;
1224
      }
1225
    }
1226
1007997
  }else if( d_type==typ_eq ){
1227
186551
    TermDb* tdb = p->getTermDatabase();
1228
186551
    QuantifiersState& qs = p->getState();
1229
559653
    for (unsigned i = 0, size = d_n.getNumChildren(); i < size; i++)
1230
    {
1231
373102
      if (!expr::hasBoundVar(d_n[i]))
1232
      {
1233
209044
        TNode t = tdb->getEntailedTerm(d_n[i]);
1234
104522
        if (qs.isInConflict())
1235
        {
1236
          return false;
1237
        }
1238
104522
        if (t.isNull())
1239
        {
1240
8292
          d_ground_eval[i] = d_n[i];
1241
        }
1242
        else
1243
        {
1244
96230
          d_ground_eval[i] = t;
1245
        }
1246
      }
1247
    }
1248
  }
1249
1010784
  d_qni_bound_cons.clear();
1250
1010784
  d_qni_bound_cons_var.clear();
1251
1010784
  d_qni_bound.clear();
1252
1010784
  return true;
1253
}
1254
1255
2131102
void MatchGen::reset( QuantConflictFind * p, bool tgt, QuantInfo * qi ) {
1256
2131102
  d_tgt = d_type_not ? !tgt : tgt;
1257
2131102
  Debug("qcf-match") << "     Reset for : " << d_n << ", type : ";
1258
2131102
  debugPrintType( "qcf-match", d_type );
1259
2131102
  Debug("qcf-match") << ", tgt = " << d_tgt << ", children = " << d_children.size() << " " << d_children_order.size() << std::endl;
1260
2131102
  d_qn.clear();
1261
2131102
  d_qni.clear();
1262
2131102
  d_qni_bound.clear();
1263
2131102
  d_child_counter = -1;
1264
2131102
  d_use_children = true;
1265
2131102
  d_tgt_orig = d_tgt;
1266
1267
  //set up processing matches
1268
2131102
  if( d_type==typ_invalid ){
1269
    d_use_children = false;
1270
2131102
  }else if( d_type==typ_ground ){
1271
955
    d_use_children = false;
1272
955
    if( d_ground_eval[0]==( d_tgt ? p->d_true : p->d_false ) ){
1273
4
      d_child_counter = 0;
1274
    }
1275
2130147
  }else if( qi->isBaseMatchComplete() && options::qcfEagerTest() ){
1276
497460
    d_use_children = false;
1277
497460
    d_child_counter = 0;
1278
1632687
  }else if( d_type==typ_bool_var ){
1279
    //get current value of the variable
1280
2584
    TNode n = qi->getCurrentValue( d_n );
1281
1292
    int vn = qi->getCurrentRepVar( qi->getVarNum( n ) );
1282
1292
    if( vn==-1 ){
1283
      //evaluate the value, see if it is compatible
1284
      //int e = p->evaluate( n );
1285
      //if( ( e==1 && d_tgt ) || ( e==0 && !d_tgt ) ){
1286
      //  d_child_counter = 0;
1287
      //}
1288
      //modified
1289
      if( p->getTermDatabase()->isEntailed( n, d_tgt ) ){
1290
        d_child_counter = 0;
1291
      }
1292
    }else{
1293
      //unassigned, set match to true/false
1294
1292
      d_qni_bound[0] = vn;
1295
1292
      qi->setMatch( p, vn, d_tgt ? p->d_true : p->d_false, false, true );
1296
1292
      d_child_counter = 0;
1297
    }
1298
1292
    if( d_child_counter==0 ){
1299
1292
      d_qn.push_back( NULL );
1300
    }
1301
1631395
  }else if( d_type==typ_var ){
1302
1133392
    Assert(isHandledUfTerm(d_n));
1303
2266784
    TNode f = getMatchOperator( p, d_n );
1304
1133392
    Debug("qcf-match-debug") << "       reset: Var will match operators of " << f << std::endl;
1305
1133392
    TNodeTrie* qni = p->getTermDatabase()->getTermArgTrie(Node::null(), f);
1306
1133392
    if (qni == nullptr || qni->empty())
1307
    {
1308
      //inform irrelevant quantifiers
1309
224547
      p->setIrrelevantFunction( f );
1310
    }
1311
    else
1312
    {
1313
908845
      d_qn.push_back(qni);
1314
    }
1315
1133392
    d_matched_basis = false;
1316
498003
  }else if( d_type==typ_tsym || d_type==typ_tconstraint ){
1317
3248
    for( std::map< int, int >::iterator it = d_qni_var_num.begin(); it != d_qni_var_num.end(); ++it ){
1318
1938
      int repVar = qi->getCurrentRepVar( it->second );
1319
1938
      if( qi->d_match[repVar].isNull() ){
1320
1872
        Debug("qcf-match-debug") << "Force matching on child #" << it->first << ", which is var #" << repVar << std::endl;
1321
1872
        d_qni_bound[it->first] = repVar;
1322
      }
1323
    }
1324
1310
    d_qn.push_back( NULL );
1325
496693
  }else if( d_type==typ_pred || d_type==typ_eq ){
1326
    //add initial constraint
1327
701216
    Node nn[2];
1328
    int vn[2];
1329
350608
    if( d_type==typ_pred ){
1330
148191
      nn[0] = qi->getCurrentValue( d_n );
1331
148191
      vn[0] = qi->getCurrentRepVar( qi->getVarNum( nn[0] ) );
1332
148191
      nn[1] = d_tgt ? p->d_true : p->d_false;
1333
148191
      vn[1] = -1;
1334
148191
      d_tgt = true;
1335
    }else{
1336
607251
      for( unsigned i=0; i<2; i++ ){
1337
809668
        TNode nc;
1338
404834
        std::map<int, TNode>::iterator it = d_qni_gterm.find(i);
1339
404834
        if (it != d_qni_gterm.end())
1340
        {
1341
134661
          nc = it->second;
1342
        }else{
1343
270173
          nc = d_n[i];
1344
        }
1345
404834
        nn[i] = qi->getCurrentValue( nc );
1346
404834
        vn[i] = qi->getCurrentRepVar( qi->getVarNum( nn[i] ) );
1347
      }
1348
    }
1349
    bool success;
1350
350608
    if( vn[0]==-1 && vn[1]==-1 ){
1351
      //Trace("qcf-explain") << "    reset : " << d_n << " check ground values " << nn[0] << " " << nn[1] << " (tgt=" << d_tgt << ")" << std::endl;
1352
372
      Debug("qcf-match-debug") << "       reset: check ground values " << nn[0] << " " << nn[1] << " (" << d_tgt << ")" << std::endl;
1353
      //just compare values
1354
744
      if( d_tgt ){
1355
327
        success = p->areMatchEqual( nn[0], nn[1] );
1356
      }else{
1357
45
        if (p->atConflictEffort()) {
1358
30
          success = p->areDisequal( nn[0], nn[1] );
1359
        }else{
1360
15
          success = p->areMatchDisequal( nn[0], nn[1] );
1361
        }
1362
      }
1363
    }else{
1364
      //otherwise, add a constraint to a variable  TODO: this may be over-eager at effort > conflict, since equality may be a propagation
1365
350236
      if( vn[1]!=-1 && vn[0]==-1 ){
1366
        //swap
1367
173198
        Node t = nn[1];
1368
86599
        nn[1] = nn[0];
1369
86599
        nn[0] = t;
1370
86599
        vn[0] = vn[1];
1371
86599
        vn[1] = -1;
1372
      }
1373
350236
      Debug("qcf-match-debug") << "       reset: add constraint " << vn[0] << " -> " << nn[1] << " (vn=" << vn[1] << ")" << std::endl;
1374
      //add some constraint
1375
350236
      int addc = qi->addConstraint( p, vn[0], nn[1], vn[1], d_tgt, false );
1376
350236
      success = addc!=-1;
1377
      //if successful and non-redundant, store that we need to cleanup this
1378
350236
      if( addc==1 ){
1379
        //Trace("qcf-explain") << "       reset: " << d_n << " add constraint " << vn[0] << " -> " << nn[1] << " (vn=" << vn[1] << ")" << ", d_tgt = " << d_tgt << std::endl;
1380
1050288
        for( unsigned i=0; i<2; i++ ){
1381
700192
          if( vn[i]!=-1 && std::find( d_qni_bound_except.begin(), d_qni_bound_except.end(), i )==d_qni_bound_except.end() ){
1382
412936
            d_qni_bound[vn[i]] = vn[i];
1383
          }
1384
        }
1385
350096
        d_qni_bound_cons[vn[0]] = nn[1];
1386
350096
        d_qni_bound_cons_var[vn[0]] = vn[1];
1387
      }
1388
    }
1389
    //if successful, we will bind values to variables
1390
350608
    if( success ){
1391
350238
      d_qn.push_back( NULL );
1392
350608
    }
1393
  }else{
1394
146085
    if( d_children.empty() ){
1395
      //add dummy
1396
      d_qn.push_back( NULL );
1397
    }else{
1398
146085
      if( d_tgt && d_n.getKind()==FORALL ){
1399
        //fail
1400
118886
      } else if (d_n.getKind() == FORALL && p->atConflictEffort() &&
1401
2858
                 !options::qcfNestedConflict()) {
1402
        //fail
1403
      }else{
1404
        //reset the first child to d_tgt
1405
116028
        d_child_counter = 0;
1406
116028
        getChild( d_child_counter )->reset( p, d_tgt, qi );
1407
      }
1408
    }
1409
  }
1410
2131102
  d_binding = false;
1411
2131102
  d_wasSet = true;
1412
2131102
  Debug("qcf-match") << "     reset: Finished reset for " << d_n << ", success = " << ( !d_qn.empty() || d_child_counter!=-1 ) << std::endl;
1413
2131102
}
1414
1415
4854877
bool MatchGen::getNextMatch( QuantConflictFind * p, QuantInfo * qi ) {
1416
4854877
  Debug("qcf-match") << "     Get next match for : " << d_n << ", type = ";
1417
4854877
  debugPrintType( "qcf-match", d_type );
1418
4854877
  Debug("qcf-match") << ", children = " << d_children.size() << ", binding = " << d_binding << std::endl;
1419
4854877
  if( !d_use_children ){
1420
995371
    if( d_child_counter==0 ){
1421
497464
      d_child_counter = -1;
1422
497464
      return true;
1423
    }else{
1424
497907
      d_wasSet = false;
1425
497907
      return false;
1426
    }
1427
3859506
  }else if( d_type==typ_var || d_type==typ_eq || d_type==typ_pred || d_type==typ_bool_var || d_type==typ_tconstraint || d_type==typ_tsym ){
1428
3151761
    bool success = false;
1429
3151761
    bool terminate = false;
1430
1807581
    do {
1431
4959342
      bool doReset = false;
1432
4959342
      bool doFail = false;
1433
4959342
      if( !d_binding ){
1434
3301324
        if( doMatching( p, qi ) ){
1435
1819453
          Debug("qcf-match-debug") << "     - Matching succeeded" << std::endl;
1436
1819453
          d_binding = true;
1437
1819453
          d_binding_it = d_qni_bound.begin();
1438
1819453
          doReset = true;
1439
          //for tconstraint, add constraint
1440
1819453
          if( d_type==typ_tconstraint ){
1441
883
            std::map< Node, bool >::iterator it = qi->d_tconstraints.find( d_n );
1442
883
            if( it==qi->d_tconstraints.end() ){
1443
883
              qi->d_tconstraints[d_n] = d_tgt;
1444
              //store that we added this constraint
1445
883
              d_qni_bound_cons[0] = d_n;
1446
            }else if( d_tgt!=it->second ){
1447
              success = false;
1448
              terminate = true;
1449
            }
1450
          }
1451
        }else{
1452
1481871
          Debug("qcf-match-debug") << "     - Matching failed" << std::endl;
1453
1481871
          success = false;
1454
1481871
          terminate = true;
1455
        }
1456
      }else{
1457
1658018
        doFail = true;
1458
      }
1459
4959342
      if( d_binding ){
1460
        //also need to create match for each variable we bound
1461
3477471
        success = true;
1462
3477471
        Debug("qcf-match-debug") << "     Produce matches for bound variables by " << d_n << ", type = ";
1463
3477471
        debugPrintType( "qcf-match-debug", d_type );
1464
3477471
        Debug("qcf-match-debug") << "..." << std::endl;
1465
1466
15279197
        while( ( success && d_binding_it!=d_qni_bound.end() ) || doFail ){
1467
5900863
          QuantInfo::VarMgMap::const_iterator itm;
1468
5900863
          if( !doFail ){
1469
4242845
            Debug("qcf-match-debug") << "       check variable " << d_binding_it->second << std::endl;
1470
4242845
            itm = qi->var_mg_find( d_binding_it->second );
1471
          }
1472
5900863
          if( doFail || ( d_binding_it->first!=0 && itm != qi->var_mg_end() ) ){
1473
4328354
            Debug("qcf-match-debug") << "       we had bound variable " << d_binding_it->second << ", reset = " << doReset << std::endl;
1474
4328354
            if( doReset ){
1475
1411334
              itm->second->reset( p, true, qi );
1476
            }
1477
4328354
            if( doFail || !itm->second->getNextMatch( p, qi ) ){
1478
1568525
              do {
1479
4635108
                if( d_binding_it==d_qni_bound.begin() ){
1480
1807581
                  Debug("qcf-match-debug") << "       failed." << std::endl;
1481
1807581
                  success = false;
1482
                }else{
1483
2827527
                  --d_binding_it;
1484
2827527
                  Debug("qcf-match-debug") << "       decrement..." << std::endl;
1485
                }
1486
9031160
              }while( success &&
1487
5094779
                      ( d_binding_it->first==0 ||
1488
2267252
                        (!qi->containsVarMg(d_binding_it->second))));
1489
3066583
              doReset = false;
1490
3066583
              doFail = false;
1491
            }else{
1492
1261771
              Debug("qcf-match-debug") << "       increment..." << std::endl;
1493
1261771
              ++d_binding_it;
1494
1261771
              doReset = true;
1495
            }
1496
          }else{
1497
1572509
            Debug("qcf-match-debug") << "       skip..." << d_binding_it->second << std::endl;
1498
1572509
            ++d_binding_it;
1499
1572509
            doReset = true;
1500
          }
1501
        }
1502
3477471
        if( !success ){
1503
1807581
          d_binding = false;
1504
        }else{
1505
1669890
          terminate = true;
1506
1669890
          if( d_binding_it==d_qni_bound.begin() ){
1507
7219
            d_binding = false;
1508
          }
1509
        }
1510
      }
1511
4959342
    }while( !terminate );
1512
    //if not successful, clean up the variables you bound
1513
3151761
    if( !success ){
1514
1481871
      if( d_type==typ_eq || d_type==typ_pred ){
1515
        //clean up the constraints you added
1516
696422
        for( std::map< int, TNode >::iterator it = d_qni_bound_cons.begin(); it != d_qni_bound_cons.end(); ++it ){
1517
347959
          if( !it->second.isNull() ){
1518
347959
            Debug("qcf-match") << "       Clean up bound var " << it->first << (d_tgt ? "!" : "") << " = " << it->second << std::endl;
1519
347959
            std::map< int, int >::iterator itb = d_qni_bound_cons_var.find( it->first );
1520
347959
            int vn = itb!=d_qni_bound_cons_var.end() ? itb->second : -1;
1521
            //Trace("qcf-explain") << "       cleanup: " << d_n << " remove constraint " << it->first << " -> " << it->second << " (vn=" << vn << ")" << ", d_tgt = " << d_tgt << std::endl;
1522
347959
            qi->addConstraint( p, it->first, it->second, vn, d_tgt, true );
1523
          }
1524
        }
1525
348463
        d_qni_bound_cons.clear();
1526
348463
        d_qni_bound_cons_var.clear();
1527
348463
        d_qni_bound.clear();
1528
      }else{
1529
        //clean up the matches you set
1530
1815627
        for( std::map< int, int >::iterator it = d_qni_bound.begin(); it != d_qni_bound.end(); ++it ){
1531
682219
          Debug("qcf-match") << "       Clean up bound var " << it->second << std::endl;
1532
682219
          Assert(it->second < qi->getNumVars());
1533
682219
          qi->unsetMatch( p, it->second );
1534
682219
          qi->d_match_term[ it->second ] = TNode::null();
1535
        }
1536
1133408
        d_qni_bound.clear();
1537
      }
1538
1481871
      if( d_type==typ_tconstraint ){
1539
        //remove constraint if applicable
1540
875
        if( d_qni_bound_cons.find( 0 )!=d_qni_bound_cons.end() ){
1541
875
          qi->d_tconstraints.erase( d_n );
1542
875
          d_qni_bound_cons.clear();
1543
        }
1544
      }
1545
    }
1546
3151761
    Debug("qcf-match") << "    ...finished matching for " << d_n << ", success = " << success << std::endl;
1547
3151761
    d_wasSet = success;
1548
3151761
    return success;
1549
  }
1550
707745
  else if (d_type == typ_formula)
1551
  {
1552
707745
    bool success = false;
1553
707745
    if( d_child_counter<0 ){
1554
30057
      if( d_child_counter<-1 ){
1555
        success = true;
1556
        d_child_counter = -1;
1557
      }
1558
    }else{
1559
3473960
      while( !success && d_child_counter>=0 ){
1560
        //transition system based on d_child_counter
1561
1398136
        if( d_n.getKind()==OR || d_n.getKind()==AND ){
1562
809055
          if( (d_n.getKind()==AND)==d_tgt ){
1563
            //all children must match simultaneously
1564
747956
            if( getChild( d_child_counter )->getNextMatch( p, qi ) ){
1565
453997
              if( d_child_counter<(int)(getNumChildren()-1) ){
1566
242574
                d_child_counter++;
1567
242574
                Debug("qcf-match-debug") << "       Reset child " << d_child_counter << " of " << d_n << std::endl;
1568
242574
                getChild( d_child_counter )->reset( p, d_tgt, qi );
1569
              }else{
1570
211423
                success = true;
1571
              }
1572
            }else{
1573
              //if( std::find( d_independent.begin(), d_independent.end(), d_child_counter )!=d_independent.end() ){
1574
              //  d_child_counter--;
1575
              //}else{
1576
293959
              d_child_counter--;
1577
              //}
1578
            }
1579
          }else{
1580
            //one child must match
1581
61099
            if( !getChild( d_child_counter )->getNextMatch( p, qi ) ){
1582
33412
              if( d_child_counter<(int)(getNumChildren()-1) ){
1583
18250
                d_child_counter++;
1584
18250
                Debug("qcf-match-debug") << "       Reset child " << d_child_counter << " of " << d_n << ", one match" << std::endl;
1585
18250
                getChild( d_child_counter )->reset( p, d_tgt, qi );
1586
              }else{
1587
15162
                d_child_counter = -1;
1588
              }
1589
            }else{
1590
27687
              success = true;
1591
            }
1592
          }
1593
589081
        }else if( d_n.getKind()==EQUAL ){
1594
          //construct match based on both children
1595
550205
          if( d_child_counter%2==0 ){
1596
238029
            if( getChild( 0 )->getNextMatch( p, qi ) ){
1597
151949
              d_child_counter++;
1598
151949
              getChild( 1 )->reset( p, d_child_counter==1, qi );
1599
            }else{
1600
86080
              if( d_child_counter==0 ){
1601
43110
                d_child_counter = 2;
1602
43110
                getChild( 0 )->reset( p, !d_tgt, qi );
1603
              }else{
1604
42970
                d_child_counter = -1;
1605
              }
1606
            }
1607
          }
1608
550205
          if( d_child_counter>=0 && d_child_counter%2==1 ){
1609
464125
            if( getChild( 1 )->getNextMatch( p, qi ) ){
1610
312421
              success = true;
1611
            }else{
1612
151704
              d_child_counter--;
1613
            }
1614
          }
1615
38876
        }else if( d_n.getKind()==ITE ){
1616
37548
          if( d_child_counter%2==0 ){
1617
26860
            int index1 = d_child_counter==4 ? 1 : 0;
1618
26860
            if( getChild( index1 )->getNextMatch( p, qi ) ){
1619
16962
              d_child_counter++;
1620
16962
              getChild( d_child_counter==5 ? 2 : (d_tgt==(d_child_counter==1) ? 1 : 2) )->reset( p, d_tgt, qi );
1621
            }else{
1622
9898
              if (d_child_counter == 4)
1623
              {
1624
3294
                d_child_counter = -1;
1625
              }else{
1626
6604
                d_child_counter +=2;
1627
6604
                getChild( d_child_counter==2 ? 0 : 1 )->reset( p, d_child_counter==2 ? !d_tgt : d_tgt, qi );
1628
              }
1629
            }
1630
          }
1631
37548
          if( d_child_counter>=0 && d_child_counter%2==1 ){
1632
27650
            int index2 = d_child_counter==5 ? 2 : (d_tgt==(d_child_counter==1) ? 1 : 2);
1633
27650
            if( getChild( index2 )->getNextMatch( p, qi ) ){
1634
10750
              success = true;
1635
            }else{
1636
16900
              d_child_counter--;
1637
            }
1638
          }
1639
1328
        }else if( d_n.getKind()==FORALL ){
1640
1328
          if( getChild( d_child_counter )->getNextMatch( p, qi ) ){
1641
318
            success = true;
1642
          }else{
1643
1010
            d_child_counter = -1;
1644
          }
1645
        }
1646
      }
1647
677688
        d_wasSet = success;
1648
677688
      Debug("qcf-match") << "    ...finished construct match for " << d_n << ", success = " << success << std::endl;
1649
677688
      return success;
1650
    }
1651
  }
1652
30057
  Debug("qcf-match") << "    ...already finished for " << d_n << std::endl;
1653
30057
  return false;
1654
}
1655
1656
3301324
bool MatchGen::doMatching( QuantConflictFind * p, QuantInfo * qi ) {
1657
3301324
  if( !d_qn.empty() ){
1658
2725720
    if( d_qn[0]==NULL ){
1659
352840
      d_qn.clear();
1660
352840
      return true;
1661
    }else{
1662
2372880
      Assert(d_type == typ_var);
1663
2372880
      Assert(d_qni_size > 0);
1664
      bool invalidMatch;
1665
7992753
      do {
1666
10365633
        invalidMatch = false;
1667
10365633
        Debug("qcf-match-debug") << "       Do matching " << d_n << " " << d_qn.size() << " " << d_qni.size() << std::endl;
1668
10365633
        if( d_qn.size()==d_qni.size()+1 ) {
1669
4778600
          int index = (int)d_qni.size();
1670
          //initialize
1671
9557200
          TNode val;
1672
4778600
          std::map< int, int >::iterator itv = d_qni_var_num.find( index );
1673
4778600
          if( itv!=d_qni_var_num.end() ){
1674
            //get the representative variable this variable is equal to
1675
4442493
            int repVar = qi->getCurrentRepVar( itv->second );
1676
4442493
            Debug("qcf-match-debug") << "       Match " << index << " is a variable " << itv->second << ", which is repVar " << repVar << std::endl;
1677
            //get the value the rep variable
1678
            //std::map< int, TNode >::iterator itm = qi->d_match.find( repVar );
1679
4442493
            if( !qi->d_match[repVar].isNull() ){
1680
2655501
              val = qi->d_match[repVar];
1681
2655501
              Debug("qcf-match-debug") << "       Variable is already bound to " << val << std::endl;
1682
            }else{
1683
              //binding a variable
1684
1786992
              d_qni_bound[index] = repVar;
1685
              std::map<TNode, TNodeTrie>::iterator it =
1686
1786992
                  d_qn[index]->d_data.begin();
1687
1786992
              if( it != d_qn[index]->d_data.end() ) {
1688
1786992
                d_qni.push_back( it );
1689
                //set the match
1690
1786992
                if( it->first.getType().isComparableTo( qi->d_var_types[repVar] ) && qi->setMatch( p, d_qni_bound[index], it->first, true, true ) ){
1691
1621909
                  Debug("qcf-match-debug") << "       Binding variable" << std::endl;
1692
1621909
                  if( d_qn.size()<d_qni_size ){
1693
653714
                    d_qn.push_back( &it->second );
1694
                  }
1695
                }else{
1696
165083
                  Debug("qcf-match") << "       Binding variable, currently fail." << std::endl;
1697
165083
                  invalidMatch = true;
1698
                }
1699
              }else{
1700
                Debug("qcf-match-debug") << "       Binding variable, fail, no more variables to bind" << std::endl;
1701
                d_qn.pop_back();
1702
              }
1703
            }
1704
          }else{
1705
336107
            Debug("qcf-match-debug") << "       Match " << index << " is ground term" << std::endl;
1706
336107
            Assert(d_qni_gterm.find(index) != d_qni_gterm.end());
1707
336107
            val = d_qni_gterm[index];
1708
336107
            Assert(!val.isNull());
1709
          }
1710
4778600
          if( !val.isNull() ){
1711
5983216
            Node valr = p->getRepresentative(val);
1712
            //constrained by val
1713
            std::map<TNode, TNodeTrie>::iterator it =
1714
2991608
                d_qn[index]->d_data.find(valr);
1715
2991608
            if( it!=d_qn[index]->d_data.end() ){
1716
1334140
              Debug("qcf-match-debug") << "       Match" << std::endl;
1717
1334140
              d_qni.push_back( it );
1718
1334140
              if( d_qn.size()<d_qni_size ){
1719
1121448
                d_qn.push_back( &it->second );
1720
              }
1721
            }else{
1722
1657468
              Debug("qcf-match-debug") << "       Failed to match" << std::endl;
1723
1657468
              d_qn.pop_back();
1724
            }
1725
          }
1726
        }else{
1727
5587033
          Assert(d_qn.size() == d_qni.size());
1728
5587033
          int index = d_qni.size()-1;
1729
          //increment if binding this variable
1730
5587033
          bool success = false;
1731
5587033
          std::map< int, int >::iterator itb = d_qni_bound.find( index );
1732
5587033
          if( itb!=d_qni_bound.end() ){
1733
4261894
            d_qni[index]++;
1734
4261894
            if( d_qni[index]!=d_qn[index]->d_data.end() ){
1735
2478988
              success = true;
1736
2478988
              if( qi->setMatch( p, itb->second, d_qni[index]->first, true, true ) ){
1737
2380319
                Debug("qcf-match-debug") << "       Bind next variable" << std::endl;
1738
2380319
                if( d_qn.size()<d_qni_size ){
1739
2094593
                  d_qn.push_back( &d_qni[index]->second );
1740
                }
1741
              }else{
1742
98669
                Debug("qcf-match-debug") << "       Bind next variable, currently fail" << std::endl;
1743
98669
                invalidMatch = true;
1744
              }
1745
            }else{
1746
1782906
              qi->unsetMatch( p, itb->second );
1747
1782906
              qi->d_match_term[ itb->second ] = TNode::null();
1748
1782906
              Debug("qcf-match-debug") << "       Bind next variable, no more variables to bind" << std::endl;
1749
            }
1750
          }else{
1751
            //TODO : if it equal to something else, also try that
1752
          }
1753
          //if not incrementing, move to next
1754
5587033
          if( !success ){
1755
3108045
            d_qn.pop_back();
1756
3108045
            d_qni.pop_back();
1757
          }
1758
        }
1759
10365633
      }while( ( !d_qn.empty() && d_qni.size()!=d_qni_size ) || invalidMatch );
1760
2372880
      if( d_qni.size()==d_qni_size ){
1761
        //Assert( !d_qni[d_qni.size()-1]->second.d_data.empty() );
1762
        //Debug("qcf-match-debug") << "       We matched " << d_qni[d_qni.size()-1]->second.d_children.begin()->first << std::endl;
1763
1466613
        Assert(!d_qni[d_qni.size() - 1]->second.d_data.empty());
1764
2933226
        TNode t = d_qni[d_qni.size()-1]->second.d_data.begin()->first;
1765
1466613
        Debug("qcf-match-debug") << "       " << d_n << " matched " << t << std::endl;
1766
1466613
        qi->d_match_term[d_qni_var_num[0]] = t;
1767
        //set the match terms
1768
4346183
        for( std::map< int, int >::iterator it = d_qni_bound.begin(); it != d_qni_bound.end(); ++it ){
1769
2879570
          Debug("qcf-match-debug") << "       position " << it->first << " bounded " << it->second << " / " << qi->d_q[0].getNumChildren() << std::endl;
1770
          //if( it->second<(int)qi->d_q[0].getNumChildren() ){   //if it is an actual variable, we are interested in knowing the actual term
1771
2879570
          if( it->first>0 ){
1772
2366765
            Assert(!qi->d_match[it->second].isNull());
1773
2366765
            Assert(p->areEqual(t[it->first - 1], qi->d_match[it->second]));
1774
2366765
            qi->d_match_term[it->second] = t[it->first-1];
1775
          }
1776
          //}
1777
        }
1778
      }
1779
    }
1780
  }
1781
2948484
  return !d_qn.empty();
1782
}
1783
1784
10616837
void MatchGen::debugPrintType( const char * c, short typ, bool isTrace ) {
1785
10616837
  if( isTrace ){
1786
153387
    switch( typ ){
1787
7445
    case typ_invalid: Trace(c) << "invalid";break;
1788
165
    case typ_ground: Trace(c) << "ground";break;
1789
29967
    case typ_eq: Trace(c) << "eq";break;
1790
17602
    case typ_pred: Trace(c) << "pred";break;
1791
21338
    case typ_formula: Trace(c) << "formula";break;
1792
76006
    case typ_var: Trace(c) << "var";break;
1793
147
    case typ_bool_var: Trace(c) << "bool_var";break;
1794
    }
1795
  }else{
1796
10463450
    switch( typ ){
1797
    case typ_invalid: Debug(c) << "invalid";break;
1798
1910
    case typ_ground: Debug(c) << "ground";break;
1799
1319370
    case typ_eq: Debug(c) << "eq";break;
1800
1654821
    case typ_pred: Debug(c) << "pred";break;
1801
953156
    case typ_formula: Debug(c) << "formula";break;
1802
6521780
    case typ_var: Debug(c) << "var";break;
1803
6460
    case typ_bool_var: Debug(c) << "bool_var";break;
1804
    }
1805
  }
1806
10616837
}
1807
1808
5228
void MatchGen::setInvalid() {
1809
5228
  d_type = typ_invalid;
1810
5228
  d_children.clear();
1811
5228
}
1812
1813
252219
bool MatchGen::isHandledBoolConnective( TNode n ) {
1814
252219
  return TermUtil::isBoolConnectiveTerm( n ) && n.getKind()!=SEP_STAR;
1815
}
1816
1817
2497892
bool MatchGen::isHandledUfTerm( TNode n ) {
1818
  //return n.getKind()==APPLY_UF || n.getKind()==STORE || n.getKind()==SELECT ||
1819
  //       n.getKind()==APPLY_CONSTRUCTOR || n.getKind()==APPLY_SELECTOR_TOTAL || n.getKind()==APPLY_TESTER;
1820
  //TODO : treat APPLY_TESTER as a T-constraint instead of matching (currently leads to overabundance of instantiations)
1821
  //return inst::Trigger::isAtomicTriggerKind( n.getKind() ) && ( !options::qcfTConstraint() || n.getKind()!=APPLY_TESTER );
1822
2497892
  return inst::TriggerTermInfo::isAtomicTriggerKind(n.getKind());
1823
}
1824
1825
1133392
Node MatchGen::getMatchOperator( QuantConflictFind * p, Node n ) {
1826
1133392
  if( isHandledUfTerm( n ) ){
1827
1133392
    return p->getTermDatabase()->getMatchOperator( n );
1828
  }else{
1829
    return Node::null();
1830
  }
1831
}
1832
1833
bool MatchGen::isHandled( TNode n ) {
1834
  if (n.getKind() != BOUND_VARIABLE && expr::hasBoundVar(n))
1835
  {
1836
    if( !isHandledBoolConnective( n ) && !isHandledUfTerm( n ) && n.getKind()!=EQUAL && n.getKind()!=ITE ){
1837
      return false;
1838
    }
1839
    for( unsigned i=0; i<n.getNumChildren(); i++ ){
1840
      if( !isHandled( n[i] ) ){
1841
        return false;
1842
      }
1843
    }
1844
  }
1845
  return true;
1846
}
1847
1848
3605
QuantConflictFind::QuantConflictFind(QuantifiersEngine* qe,
1849
                                     QuantifiersState& qs,
1850
                                     QuantifiersInferenceManager& qim,
1851
3605
                                     QuantifiersRegistry& qr)
1852
    : QuantifiersModule(qs, qim, qr, qe),
1853
      d_conflict(qs.getSatContext(), false),
1854
      d_true(NodeManager::currentNM()->mkConst<bool>(true)),
1855
      d_false(NodeManager::currentNM()->mkConst<bool>(false)),
1856
3605
      d_effort(EFFORT_INVALID)
1857
{
1858
3605
}
1859
1860
//-------------------------------------------------- registration
1861
1862
21870
void QuantConflictFind::registerQuantifier( Node q ) {
1863
21870
  if (d_qreg.hasOwnership(q, this))
1864
  {
1865
21086
    d_quants.push_back( q );
1866
21086
    d_quant_id[q] = d_quants.size();
1867
21086
    if( Trace.isOn("qcf-qregister") ){
1868
      Trace("qcf-qregister") << "Register ";
1869
      debugPrintQuant( "qcf-qregister", q );
1870
      Trace("qcf-qregister") << " : " << q << std::endl;
1871
    }
1872
    //make QcfNode structure
1873
21086
    Trace("qcf-qregister") << "- Get relevant equality/disequality pairs, calculate flattening..." << std::endl;
1874
21086
    d_qinfo[q].initialize( this, q, q[1] );
1875
1876
    //debug print
1877
21086
    if( Trace.isOn("qcf-qregister") ){
1878
      Trace("qcf-qregister") << "- Flattened structure is :" << std::endl;
1879
      Trace("qcf-qregister") << "    ";
1880
      debugPrintQuantBody( "qcf-qregister", q, q[1] );
1881
      Trace("qcf-qregister") << std::endl;
1882
      if( d_qinfo[q].d_vars.size()>q[0].getNumChildren() ){
1883
        Trace("qcf-qregister") << "  with additional constraints : " << std::endl;
1884
        for( unsigned j=q[0].getNumChildren(); j<d_qinfo[q].d_vars.size(); j++ ){
1885
          Trace("qcf-qregister") << "    ?x" << j << " = ";
1886
          debugPrintQuantBody( "qcf-qregister", q, d_qinfo[q].d_vars[j], false );
1887
          Trace("qcf-qregister") << std::endl;
1888
        }
1889
      }
1890
      Trace("qcf-qregister") << "Done registering quantifier." << std::endl;
1891
    }
1892
  }
1893
21870
}
1894
1895
327
bool QuantConflictFind::areMatchEqual( TNode n1, TNode n2 ) {
1896
  //if( d_effort==QuantConflictFind::effort_mc ){
1897
  //  return n1==n2 || !areDisequal( n1, n2 );
1898
  //}else{
1899
327
  return n1==n2;
1900
  //}
1901
}
1902
1903
15
bool QuantConflictFind::areMatchDisequal( TNode n1, TNode n2 ) {
1904
  // if( d_effort==QuantConflictFind::Effort::Conflict ){
1905
  //  return areDisequal( n1, n2 );
1906
  //}else{
1907
15
  return n1!=n2;
1908
  //}
1909
}
1910
1911
//-------------------------------------------------- check function
1912
1913
46862
bool QuantConflictFind::needsCheck( Theory::Effort level ) {
1914
46862
  bool performCheck = false;
1915
46862
  if( options::quantConflictFind() && !d_conflict ){
1916
46858
    if( level==Theory::EFFORT_LAST_CALL ){
1917
50692
      performCheck = options::qcfWhenMode() == options::QcfWhenMode::LAST_CALL;
1918
43024
    }else if( level==Theory::EFFORT_FULL ){
1919
13571
      performCheck = options::qcfWhenMode() == options::QcfWhenMode::DEFAULT;
1920
29453
    }else if( level==Theory::EFFORT_STANDARD ){
1921
29453
      performCheck = options::qcfWhenMode() == options::QcfWhenMode::STD;
1922
    }
1923
  }
1924
46862
  return performCheck;
1925
}
1926
1927
17407
void QuantConflictFind::reset_round( Theory::Effort level ) {
1928
17407
  Trace("qcf-check") << "QuantConflictFind::reset_round" << std::endl;
1929
17407
  Trace("qcf-check") << "Compute relevant equivalence classes..." << std::endl;
1930
17407
  d_eqcs.clear();
1931
1932
17407
  eq::EqClassesIterator eqcs_i = eq::EqClassesIterator(getEqualityEngine());
1933
17407
  TermDb* tdb = getTermDatabase();
1934
2367991
  while (!eqcs_i.isFinished())
1935
  {
1936
2350584
    Node r = (*eqcs_i);
1937
1175292
    if (tdb->hasTermCurrent(r))
1938
    {
1939
2350584
      TypeNode rtn = r.getType();
1940
1175292
      if (!options::cegqi() || !TermUtil::hasInstConstAttr(r))
1941
      {
1942
1119282
        d_eqcs[rtn].push_back(r);
1943
      }
1944
    }
1945
1175292
    ++eqcs_i;
1946
  }
1947
17407
}
1948
1949
224547
void QuantConflictFind::setIrrelevantFunction( TNode f ) {
1950
224547
  if( d_irr_func.find( f )==d_irr_func.end() ){
1951
19412
    d_irr_func[f] = true;
1952
19412
    std::map< TNode, std::vector< Node > >::iterator it = d_func_rel_dom.find( f );
1953
19412
    if( it != d_func_rel_dom.end()){
1954
70608
      for( unsigned j=0; j<it->second.size(); j++ ){
1955
55956
        d_irr_quant[it->second[j]] = true;
1956
      }
1957
    }
1958
  }
1959
224547
}
1960
1961
namespace {
1962
1963
// Returns the beginning of a range of efforts. The range can be iterated
1964
// through as unsigned using operator++.
1965
13571
inline QuantConflictFind::Effort QcfEffortStart() {
1966
13571
  return QuantConflictFind::EFFORT_CONFLICT;
1967
}
1968
1969
// Returns the beginning of a range of efforts. The value returned is included
1970
// in the range.
1971
13571
inline QuantConflictFind::Effort QcfEffortEnd() {
1972
13571
  return options::qcfMode() == options::QcfMode::PROP_EQ
1973
13571
             ? QuantConflictFind::EFFORT_PROP_EQ
1974
13571
             : QuantConflictFind::EFFORT_CONFLICT;
1975
}
1976
1977
}  // namespace
1978
1979
/** check */
1980
49725
void QuantConflictFind::check(Theory::Effort level, QEffort quant_e)
1981
{
1982
63296
  CodeTimer codeTimer(d_quantEngine->d_statistics.d_qcf_time);
1983
49725
  if (quant_e != QEFFORT_CONFLICT)
1984
  {
1985
36154
    return;
1986
  }
1987
13571
  Trace("qcf-check") << "QCF : check : " << level << std::endl;
1988
13571
  if (d_conflict)
1989
  {
1990
    Trace("qcf-check2") << "QCF : finished check : already in conflict."
1991
                        << std::endl;
1992
    if (level >= Theory::EFFORT_FULL)
1993
    {
1994
      Trace("qcf-warn") << "ALREADY IN CONFLICT? " << level << std::endl;
1995
    }
1996
    return;
1997
  }
1998
13571
  unsigned addedLemmas = 0;
1999
13571
  ++(d_statistics.d_inst_rounds);
2000
13571
  double clSet = 0;
2001
13571
  int prevEt = 0;
2002
13571
  if (Trace.isOn("qcf-engine"))
2003
  {
2004
    prevEt = d_statistics.d_entailment_checks.get();
2005
    clSet = double(clock()) / double(CLOCKS_PER_SEC);
2006
    Trace("qcf-engine") << "---Conflict Find Engine Round, effort = " << level
2007
                        << "---" << std::endl;
2008
  }
2009
2010
  // reset the round-specific information
2011
13571
  d_irr_func.clear();
2012
13571
  d_irr_quant.clear();
2013
2014
13571
  if (Trace.isOn("qcf-debug"))
2015
  {
2016
    Trace("qcf-debug") << std::endl;
2017
    debugPrint("qcf-debug");
2018
    Trace("qcf-debug") << std::endl;
2019
  }
2020
13571
  bool isConflict = false;
2021
13571
  FirstOrderModel* fm = d_quantEngine->getModel();
2022
13571
  unsigned nquant = fm->getNumAssertedQuantifiers();
2023
  // for each effort level (find conflict, find propagating)
2024
38723
  for (unsigned e = QcfEffortStart(), end = QcfEffortEnd(); e <= end; ++e)
2025
  {
2026
    // set the effort (data member for convienence of access)
2027
26346
    d_effort = static_cast<Effort>(e);
2028
52692
    Trace("qcf-check") << "Checking quantified formulas at effort " << e
2029
26346
                       << "..." << std::endl;
2030
    // for each quantified formula
2031
314761
    for (unsigned i = 0; i < nquant; i++)
2032
    {
2033
577626
      Node q = fm->getAssertedQuantifier(i, true);
2034
867633
      if (d_qreg.hasOwnership(q, this)
2035
571144
          && d_irr_quant.find(q) == d_irr_quant.end()
2036
1087218
          && fm->isQuantifierActive(q))
2037
      {
2038
        // check this quantified formula
2039
219569
        checkQuantifiedFormula(q, isConflict, addedLemmas);
2040
219569
        if (d_conflict || d_qstate.isInConflict())
2041
        {
2042
796
          break;
2043
        }
2044
      }
2045
    }
2046
    // We are done if we added a lemma, or discovered a conflict in another
2047
    // way. An example of the latter case is when two disequal congruent terms
2048
    // are discovered during term indexing.
2049
26346
    if (addedLemmas > 0 || d_qstate.isInConflict())
2050
    {
2051
1194
      break;
2052
    }
2053
  }
2054
13571
  if (isConflict)
2055
  {
2056
    d_conflict.set(true);
2057
  }
2058
13571
  if (Trace.isOn("qcf-engine"))
2059
  {
2060
    double clSet2 = double(clock()) / double(CLOCKS_PER_SEC);
2061
    Trace("qcf-engine") << "Finished conflict find engine, time = "
2062
                        << (clSet2 - clSet);
2063
    if (addedLemmas > 0)
2064
    {
2065
      Trace("qcf-engine") << ", effort = "
2066
                          << (d_effort == EFFORT_CONFLICT
2067
                                  ? "conflict"
2068
                                  : (d_effort == EFFORT_PROP_EQ ? "prop_eq"
2069
                                                                : "mc"));
2070
      Trace("qcf-engine") << ", addedLemmas = " << addedLemmas;
2071
    }
2072
    Trace("qcf-engine") << std::endl;
2073
    int currEt = d_statistics.d_entailment_checks.get();
2074
    if (currEt != prevEt)
2075
    {
2076
      Trace("qcf-engine") << "  Entailment checks = " << (currEt - prevEt)
2077
                          << std::endl;
2078
    }
2079
  }
2080
13571
  Trace("qcf-check2") << "QCF : finished check : " << level << std::endl;
2081
}
2082
2083
219569
void QuantConflictFind::checkQuantifiedFormula(Node q,
2084
                                               bool& isConflict,
2085
                                               unsigned& addedLemmas)
2086
{
2087
219569
  QuantInfo* qi = &d_qinfo[q];
2088
219569
  Assert(d_qinfo.find(q) != d_qinfo.end());
2089
219569
  if (!qi->matchGeneratorIsValid())
2090
  {
2091
    // quantified formula is not properly set up for matching
2092
95278
    return;
2093
  }
2094
124291
  if (Trace.isOn("qcf-check"))
2095
  {
2096
    Trace("qcf-check") << "Check quantified formula ";
2097
    debugPrintQuant("qcf-check", q);
2098
    Trace("qcf-check") << " : " << q << "..." << std::endl;
2099
  }
2100
2101
124291
  Trace("qcf-check-debug") << "Reset round..." << std::endl;
2102
124291
  if (!qi->reset_round(this))
2103
  {
2104
    // it is typically the case that another conflict (e.g. in the term
2105
    // database) was discovered if we fail here.
2106
    return;
2107
  }
2108
  // try to make a matches making the body false or propagating
2109
124291
  Trace("qcf-check-debug") << "Get next match..." << std::endl;
2110
124291
  Instantiate* qinst = d_quantEngine->getInstantiate();
2111
1110697
  while (qi->getNextMatch(this))
2112
  {
2113
494098
    if (d_qstate.isInConflict())
2114
    {
2115
4
      Trace("qcf-check") << "   ... Quantifiers engine discovered conflict, ";
2116
8
      Trace("qcf-check") << "probably related to disequal congruent terms in "
2117
4
                            "master equality engine"
2118
4
                         << std::endl;
2119
899
      return;
2120
    }
2121
494094
    if (Trace.isOn("qcf-inst"))
2122
    {
2123
      Trace("qcf-inst") << "*** Produced match at effort " << d_effort << " : "
2124
                        << std::endl;
2125
      qi->debugPrintMatch("qcf-inst");
2126
      Trace("qcf-inst") << std::endl;
2127
    }
2128
    // check whether internal match constraints are satisfied
2129
533079
    if (qi->isMatchSpurious(this))
2130
    {
2131
77970
      Trace("qcf-inst") << "   ... Spurious (match is inconsistent)"
2132
38985
                        << std::endl;
2133
78100
      continue;
2134
    }
2135
    // check whether match can be completed
2136
909197
    std::vector<int> assigned;
2137
455239
    if (!qi->completeMatch(this, assigned))
2138
    {
2139
260
      Trace("qcf-inst") << "   ... Spurious (cannot assign unassigned vars)"
2140
130
                        << std::endl;
2141
130
      continue;
2142
    }
2143
    // check whether the match is spurious according to (T-)entailment checks
2144
909067
    std::vector<Node> terms;
2145
454979
    qi->getMatch(terms);
2146
454979
    bool tcs = qi->isTConstraintSpurious(this, terms);
2147
454979
    if (tcs)
2148
    {
2149
905816
      Trace("qcf-inst") << "   ... Spurious (match is T-inconsistent)"
2150
452908
                        << std::endl;
2151
    }
2152
    else
2153
    {
2154
      // otherwise, we have a conflict/propagating instance
2155
      // for debugging
2156
2071
      if (Debug.isOn("qcf-check-inst"))
2157
      {
2158
        Node inst = qinst->getInstantiation(q, terms);
2159
        Debug("qcf-check-inst")
2160
            << "Check instantiation " << inst << "..." << std::endl;
2161
        Assert(!getTermDatabase()->isEntailed(inst, true));
2162
        Assert(getTermDatabase()->isEntailed(inst, false)
2163
               || d_effort > EFFORT_CONFLICT);
2164
      }
2165
      // Process the lemma: either add an instantiation or specific lemmas
2166
      // constructed during the isTConstraintSpurious call, or both.
2167
4142
      InferenceId id = (d_effort == EFFORT_CONFLICT
2168
2071
                            ? InferenceId::QUANTIFIERS_INST_CBQI_CONFLICT
2169
                            : InferenceId::QUANTIFIERS_INST_CBQI_PROP);
2170
2071
      if (!qinst->addInstantiation(q, terms, id))
2171
      {
2172
101
        Trace("qcf-inst") << "   ... Failed to add instantiation" << std::endl;
2173
        // This should only happen if the algorithm generates the same
2174
        // propagating instance twice this round. In this case, return
2175
        // to avoid exponential behavior.
2176
101
        return;
2177
      }
2178
1970
      Trace("qcf-check") << "   ... Added instantiation" << std::endl;
2179
1970
      if (Trace.isOn("qcf-inst"))
2180
      {
2181
        Trace("qcf-inst") << "*** Was from effort " << d_effort << " : "
2182
                          << std::endl;
2183
        qi->debugPrintMatch("qcf-inst");
2184
        Trace("qcf-inst") << std::endl;
2185
      }
2186
1970
      ++addedLemmas;
2187
1970
      if (d_effort == EFFORT_CONFLICT)
2188
      {
2189
        // mark relevant: this ensures that quantified formula q is
2190
        // checked first on the next round. This is an optimization to
2191
        // ensure that quantified formulas that are more likely to have
2192
        // conflicting instances are checked earlier.
2193
790
        d_quantEngine->markRelevant(q);
2194
1580
        if (options::qcfAllConflict())
2195
        {
2196
          isConflict = true;
2197
        }
2198
        else
2199
        {
2200
790
          d_conflict.set(true);
2201
        }
2202
790
        return;
2203
      }
2204
1180
      else if (d_effort == EFFORT_PROP_EQ)
2205
      {
2206
1180
        d_quantEngine->markRelevant(q);
2207
      }
2208
    }
2209
    // clean up assigned
2210
454088
    qi->revertMatch(this, assigned);
2211
454088
    d_tempCache.clear();
2212
  }
2213
123396
  Trace("qcf-check") << "Done, conflict = " << d_conflict << std::endl;
2214
}
2215
2216
//-------------------------------------------------- debugging
2217
2218
void QuantConflictFind::debugPrint( const char * c ) {
2219
  //print the equivalance classes
2220
  Trace(c) << "----------EQ classes" << std::endl;
2221
  eq::EqClassesIterator eqcs_i = eq::EqClassesIterator( getEqualityEngine() );
2222
  while( !eqcs_i.isFinished() ){
2223
    Node n = (*eqcs_i);
2224
    //if( !n.getType().isInteger() ){
2225
    Trace(c) << "  - " << n << " : {";
2226
    eq::EqClassIterator eqc_i = eq::EqClassIterator( n, getEqualityEngine() );
2227
    bool pr = false;
2228
    while( !eqc_i.isFinished() ){
2229
      Node nn = (*eqc_i);
2230
      if( nn.getKind()!=EQUAL && nn!=n ){
2231
        Trace(c) << (pr ? "," : "" ) << " " << nn;
2232
        pr = true;
2233
      }
2234
      ++eqc_i;
2235
    }
2236
    Trace(c) << (pr ? " " : "" ) << "}" << std::endl;
2237
    ++eqcs_i;
2238
  }
2239
}
2240
2241
void QuantConflictFind::debugPrintQuant( const char * c, Node q ) {
2242
  Trace(c) << "Q" << d_quant_id[q];
2243
}
2244
2245
void QuantConflictFind::debugPrintQuantBody( const char * c, Node q, Node n, bool doVarNum ) {
2246
  if( n.getNumChildren()==0 ){
2247
    Trace(c) << n;
2248
  }else if( doVarNum && d_qinfo[q].d_var_num.find( n )!=d_qinfo[q].d_var_num.end() ){
2249
    Trace(c) << "?x" << d_qinfo[q].d_var_num[n];
2250
  }else{
2251
    Trace(c) << "(";
2252
    if( n.getKind()==APPLY_UF ){
2253
      Trace(c) << n.getOperator();
2254
    }else{
2255
      Trace(c) << n.getKind();
2256
    }
2257
    for( unsigned i=0; i<n.getNumChildren(); i++ ){
2258
      Trace(c) << " ";
2259
      debugPrintQuantBody( c, q, n[i] );
2260
    }
2261
    Trace(c) << ")";
2262
  }
2263
}
2264
2265
3605
QuantConflictFind::Statistics::Statistics():
2266
  d_inst_rounds("QuantConflictFind::Inst_Rounds", 0),
2267
3605
  d_entailment_checks("QuantConflictFind::Entailment_Checks",0)
2268
{
2269
3605
  smtStatisticsRegistry()->registerStat(&d_inst_rounds);
2270
3605
  smtStatisticsRegistry()->registerStat(&d_entailment_checks);
2271
3605
}
2272
2273
7208
QuantConflictFind::Statistics::~Statistics(){
2274
3604
  smtStatisticsRegistry()->unregisterStat(&d_inst_rounds);
2275
3604
  smtStatisticsRegistry()->unregisterStat(&d_entailment_checks);
2276
3604
}
2277
2278
8
TNode QuantConflictFind::getZero( Kind k ) {
2279
8
  std::map< Kind, Node >::iterator it = d_zero.find( k );
2280
8
  if( it==d_zero.end() ){
2281
16
    Node nn;
2282
8
    if( k==PLUS ){
2283
4
      nn = NodeManager::currentNM()->mkConst( Rational(0) );
2284
    }
2285
8
    d_zero[k] = nn;
2286
8
    return nn;
2287
  }else{
2288
    return it->second;
2289
  }
2290
}
2291
2292
std::ostream& operator<<(std::ostream& os, const QuantConflictFind::Effort& e) {
2293
  switch (e) {
2294
    case QuantConflictFind::EFFORT_INVALID:
2295
      os << "Invalid";
2296
      break;
2297
    case QuantConflictFind::EFFORT_CONFLICT:
2298
      os << "Conflict";
2299
      break;
2300
    case QuantConflictFind::EFFORT_PROP_EQ:
2301
      os << "PropEq";
2302
      break;
2303
  }
2304
  return os;
2305
}
2306
2307
1281
bool QuantConflictFind::isPropagatingInstance(Node n) const
2308
{
2309
2562
  std::unordered_set<TNode, TNodeHashFunction> visited;
2310
2562
  std::vector<TNode> visit;
2311
2562
  TNode cur;
2312
1281
  visit.push_back(n);
2313
2832
  do
2314
  {
2315
4113
    cur = visit.back();
2316
4113
    visit.pop_back();
2317
4113
    if (visited.find(cur) == visited.end())
2318
    {
2319
4073
      visited.insert(cur);
2320
4073
      Kind ck = cur.getKind();
2321
4073
      if (ck == FORALL)
2322
      {
2323
        // do nothing
2324
      }
2325
3977
      else if (TermUtil::isBoolConnective(ck))
2326
      {
2327
4256
        for (TNode cc : cur)
2328
        {
2329
2832
          visit.push_back(cc);
2330
        }
2331
      }
2332
2553
      else if (!getEqualityEngine()->hasTerm(cur))
2333
      {
2334
        Trace("qcf-instance-check-debug")
2335
            << "...not propagating instance because of " << cur << " " << ck
2336
            << std::endl;
2337
        return false;
2338
      }
2339
    }
2340
4113
  } while (!visit.empty());
2341
1281
  return true;
2342
}
2343
2344
} /* namespace CVC4::theory::quantifiers */
2345
} /* namespace CVC4::theory */
2346
1890221
} /* namespace CVC4 */