GCC Code Coverage Report
Directory: . Exec Total Coverage
File: src/theory/quantifiers/fmf/full_model_check.cpp Lines: 743 794 93.6 %
Date: 2021-03-22 Branches: 1614 3213 50.2 %

Line Exec Source
1
/*********************                                                        */
2
/*! \file full_model_check.cpp
3
 ** \verbatim
4
 ** Top contributors (to current version):
5
 **   Andrew Reynolds, Mathias Preiner, Morgan Deters
6
 ** This file is part of the CVC4 project.
7
 ** Copyright (c) 2009-2021 by the authors listed in the file AUTHORS
8
 ** in the top-level source directory and their institutional affiliations.
9
 ** All rights reserved.  See the file COPYING in the top-level source
10
 ** directory for licensing information.\endverbatim
11
 **
12
 ** \brief Implementation of full model check class
13
 **/
14
15
#include "theory/quantifiers/fmf/full_model_check.h"
16
17
#include "options/quantifiers_options.h"
18
#include "options/theory_options.h"
19
#include "options/uf_options.h"
20
#include "theory/quantifiers/first_order_model.h"
21
#include "theory/quantifiers/fmf/bounded_integers.h"
22
#include "theory/quantifiers/instantiate.h"
23
#include "theory/quantifiers/quant_rep_bound_ext.h"
24
#include "theory/quantifiers/quantifiers_registry.h"
25
#include "theory/quantifiers/quantifiers_state.h"
26
#include "theory/quantifiers/term_database.h"
27
#include "theory/quantifiers/term_util.h"
28
#include "theory/quantifiers_engine.h"
29
#include "theory/rewriter.h"
30
31
using namespace std;
32
using namespace CVC4;
33
using namespace CVC4::kind;
34
using namespace CVC4::context;
35
using namespace CVC4::theory;
36
using namespace CVC4::theory::quantifiers;
37
using namespace CVC4::theory::inst;
38
using namespace CVC4::theory::quantifiers::fmcheck;
39
40
210550
struct ModelBasisArgSort
41
{
42
  std::vector< Node > d_terms;
43
  // number of arguments that are model-basis terms
44
  std::unordered_map<Node, unsigned, NodeHashFunction> d_mba_count;
45
61535
  bool operator() (int i,int j) {
46
61535
    return (d_mba_count[d_terms[i]] < d_mba_count[d_terms[j]]);
47
  }
48
};
49
50
394274
bool EntryTrie::hasGeneralization( FirstOrderModelFmc * m, Node c, int index ) {
51
394274
  if (index==(int)c.getNumChildren()) {
52
16869
    return d_data!=-1;
53
  }else{
54
754810
    TypeNode tn = c[index].getType();
55
754810
    Node st = m->getStar(tn);
56
377405
    if(d_child.find(st)!=d_child.end()) {
57
38152
      if( d_child[st].hasGeneralization(m, c, index+1) ){
58
16450
        return true;
59
      }
60
    }
61
360955
    if( c[index]!=st && d_child.find( c[index] )!=d_child.end() ){
62
51330
      if( d_child[ c[index] ].hasGeneralization(m, c, index+1) ){
63
19821
        return true;
64
      }
65
    }
66
341134
    if( c[index].getType().isSort() ){
67
      //for star: check if all children are defined and have generalizations
68
288496
      if( c[index]==st ){     ///options::fmfFmcCoverSimplify()
69
        //check if all children exist and are complete
70
        unsigned num_child_def =
71
169892
            d_child.size() - (d_child.find(st) != d_child.end() ? 1 : 0);
72
169892
        if (num_child_def == m->getRepSet()->getNumRepresentatives(tn))
73
        {
74
8107
          bool complete = true;
75
13650
          for ( std::map<Node,EntryTrie>::iterator it = d_child.begin(); it != d_child.end(); ++it ){
76
11332
            if( !m->isStar(it->first) ){
77
10907
              if( !it->second.hasGeneralization(m, c, index+1) ){
78
5789
                complete = false;
79
5789
                break;
80
              }
81
            }
82
          }
83
8107
          if( complete ){
84
2318
            return true;
85
          }
86
        }
87
      }
88
    }
89
90
338816
    return false;
91
  }
92
}
93
94
123271
int EntryTrie::getGeneralizationIndex( FirstOrderModelFmc * m, std::vector<Node> & inst, int index ) {
95
123271
  Debug("fmc-entry-trie") << "Get generalization index " << inst.size() << " " << index << std::endl;
96
123271
  if (index==(int)inst.size()) {
97
36473
    return d_data;
98
  }else{
99
86798
    int minIndex = -1;
100
173596
    Node st = m->getStar(inst[index].getType());
101
86798
    if (d_child.find(st) != d_child.end())
102
    {
103
82165
      minIndex = d_child[st].getGeneralizationIndex(m, inst, index + 1);
104
    }
105
173596
    Node cc = inst[index];
106
86798
    if (cc != st && d_child.find(cc) != d_child.end())
107
    {
108
9879
      int gindex = d_child[cc].getGeneralizationIndex(m, inst, index + 1);
109
9879
      if (minIndex == -1 || (gindex != -1 && gindex < minIndex))
110
      {
111
6976
        minIndex = gindex;
112
      }
113
    }
114
86798
    return minIndex;
115
  }
116
}
117
118
729255
void EntryTrie::addEntry( FirstOrderModelFmc * m, Node c, Node v, int data, int index ) {
119
729255
  if (index==(int)c.getNumChildren()) {
120
279816
    if(d_data==-1) {
121
279816
      d_data = data;
122
    }
123
  }
124
  else {
125
449439
    d_child[ c[index] ].addEntry(m,c,v,data,index+1);
126
449439
    if( d_complete==0 ){
127
      d_complete = -1;
128
    }
129
  }
130
729255
}
131
132
313887
void EntryTrie::getEntries( FirstOrderModelFmc * m, Node c, std::vector<int> & compat, std::vector<int> & gen, int index, bool is_gen ) {
133
313887
  if (index==(int)c.getNumChildren()) {
134
74409
    if( d_data!=-1) {
135
74409
      if( is_gen ){
136
69240
        gen.push_back(d_data);
137
      }
138
74409
      compat.push_back(d_data);
139
    }
140
  }else{
141
239478
    if (m->isStar(c[index])) {
142
245865
      for ( std::map<Node,EntryTrie>::iterator it = d_child.begin(); it != d_child.end(); ++it ){
143
111038
        it->second.getEntries(m, c, compat, gen, index+1, is_gen );
144
      }
145
    }else{
146
209302
      Node st = m->getStar(c[index].getType());
147
104651
      if(d_child.find(st)!=d_child.end()) {
148
6625
        d_child[st].getEntries(m, c, compat, gen, index+1, false);
149
      }
150
104651
      if( d_child.find( c[index] )!=d_child.end() ){
151
26751
        d_child[ c[index] ].getEntries(m, c, compat, gen, index+1, is_gen);
152
      }
153
    }
154
155
  }
156
313887
}
157
158
293885
bool Def::addEntry( FirstOrderModelFmc * m, Node c, Node v) {
159
293885
  if (d_et.hasGeneralization(m, c)) {
160
14069
    Trace("fmc-debug") << "Already has generalization, skip." << std::endl;
161
14069
    return false;
162
  }
163
279816
  int newIndex = (int)d_cond.size();
164
279816
  if (!d_has_simplified) {
165
338946
    std::vector<int> compat;
166
338946
    std::vector<int> gen;
167
169473
    d_et.getEntries(m, c, compat, gen);
168
243882
    for( unsigned i=0; i<compat.size(); i++) {
169
74409
      if( d_status[compat[i]]==status_unk ){
170
66673
        if( d_value[compat[i]]!=v ){
171
42334
          d_status[compat[i]] = status_non_redundant;
172
        }
173
      }
174
    }
175
238713
    for( unsigned i=0; i<gen.size(); i++) {
176
69240
      if( d_status[gen[i]]==status_unk ){
177
20936
        if( d_value[gen[i]]==v ){
178
20936
          d_status[gen[i]] = status_redundant;
179
        }
180
      }
181
    }
182
169473
    d_status.push_back( status_unk );
183
  }
184
279816
  d_et.addEntry(m, c, v, newIndex);
185
279816
  d_cond.push_back(c);
186
279816
  d_value.push_back(v);
187
279816
  return true;
188
}
189
190
2006
Node Def::evaluate( FirstOrderModelFmc * m, std::vector<Node>& inst ) {
191
2006
  int gindex = d_et.getGeneralizationIndex(m, inst);
192
2006
  if (gindex!=-1) {
193
2002
    return d_value[gindex];
194
  }else{
195
4
    Trace("fmc-warn") << "Warning : evaluation came up null!" << std::endl;
196
4
    return Node::null();
197
  }
198
}
199
200
29221
int Def::getGeneralizationIndex( FirstOrderModelFmc * m, std::vector<Node>& inst ) {
201
29221
  return d_et.getGeneralizationIndex(m, inst);
202
}
203
204
63255
void Def::basic_simplify( FirstOrderModelFmc * m ) {
205
63255
  d_has_simplified = true;
206
126510
  std::vector< Node > cond;
207
63255
  cond.insert( cond.end(), d_cond.begin(), d_cond.end() );
208
63255
  d_cond.clear();
209
126510
  std::vector< Node > value;
210
63255
  value.insert( value.end(), d_value.begin(), d_value.end() );
211
63255
  d_value.clear();
212
63255
  d_et.reset();
213
194534
  for (unsigned i=0; i<d_status.size(); i++) {
214
131279
    if( d_status[i]!=status_redundant ){
215
110343
      addEntry(m, cond[i], value[i]);
216
    }
217
  }
218
63255
  d_status.clear();
219
63255
}
220
221
56149
void Def::simplify(FullModelChecker * mc, FirstOrderModelFmc * m) {
222
56149
  Trace("fmc-simplify") << "Simplify definition, #cond = " << d_cond.size() << std::endl;
223
56149
  basic_simplify( m );
224
56149
  Trace("fmc-simplify") << "post-basic simplify, #cond = " << d_cond.size() << std::endl;
225
226
  //check if the last entry is not all star, if so, we can make the last entry all stars
227
56149
  if( !d_cond.empty() ){
228
56149
    bool last_all_stars = true;
229
112298
    Node cc = d_cond[d_cond.size()-1];
230
130415
    for( unsigned i=0; i<cc.getNumChildren(); i++ ){
231
81372
      if (!m->isStar(cc[i]))
232
      {
233
7106
        last_all_stars = false;
234
7106
        break;
235
      }
236
    }
237
56149
    if( !last_all_stars ){
238
7106
      Trace("fmc-cover-simplify") << "Need to modify last entry to be all stars." << std::endl;
239
7106
      Trace("fmc-cover-simplify") << "Before: " << std::endl;
240
7106
      debugPrint("fmc-cover-simplify",Node::null(), mc);
241
7106
      Trace("fmc-cover-simplify") << std::endl;
242
14212
      std::vector< Node > cond;
243
7106
      cond.insert( cond.end(), d_cond.begin(), d_cond.end() );
244
7106
      d_cond.clear();
245
14212
      std::vector< Node > value;
246
7106
      value.insert( value.end(), d_value.begin(), d_value.end() );
247
7106
      d_value.clear();
248
7106
      d_et.reset();
249
7106
      d_has_simplified = false;
250
      //change the last to all star
251
14212
      std::vector< Node > nc;
252
7106
      nc.push_back( cc.getOperator() );
253
17974
      for( unsigned j=0; j< cc.getNumChildren(); j++){
254
10868
        nc.push_back(m->getStar(cc[j].getType()));
255
      }
256
7106
      cond[cond.size()-1] = NodeManager::currentNM()->mkNode( APPLY_UF, nc );
257
      //re-add the entries
258
19098
      for (unsigned i=0; i<cond.size(); i++) {
259
11992
        addEntry(m, cond[i], value[i]);
260
      }
261
7106
      Trace("fmc-cover-simplify") << "Finished re-adding entries." << std::endl;
262
7106
      basic_simplify( m );
263
7106
      Trace("fmc-cover-simplify") << "After: " << std::endl;
264
7106
      debugPrint("fmc-cover-simplify",Node::null(), mc);
265
7106
      Trace("fmc-cover-simplify") << std::endl;
266
    }
267
  }
268
56149
  Trace("fmc-simplify") << "finish simplify, #cond = " << d_cond.size() << std::endl;
269
56149
}
270
271
197877
void Def::debugPrint(const char * tr, Node op, FullModelChecker * m) {
272
197877
  if (!op.isNull()) {
273
41727
    Trace(tr) << "Model for " << op << " : " << std::endl;
274
  }
275
558575
  for( unsigned i=0; i<d_cond.size(); i++) {
276
    //print the condition
277
360698
    if (!op.isNull()) {
278
117675
      Trace(tr) << op;
279
    }
280
360698
    m->debugPrintCond(tr, d_cond[i], true);
281
360698
    Trace(tr) << " -> ";
282
360698
    m->debugPrint(tr, d_value[i]);
283
360698
    Trace(tr) << std::endl;
284
  }
285
197877
}
286
287
808
FullModelChecker::FullModelChecker(QuantifiersState& qs,
288
808
                                   QuantifiersRegistry& qr)
289
808
    : QModelBuilder(qs, qr)
290
{
291
808
  d_true = NodeManager::currentNM()->mkConst(true);
292
808
  d_false = NodeManager::currentNM()->mkConst(false);
293
808
}
294
295
1588
bool FullModelChecker::preProcessBuildModel(TheoryModel* m) {
296
  //standard pre-process
297
1588
  if( !preProcessBuildModelStd( m ) ){
298
    return false;
299
  }
300
301
1588
  FirstOrderModelFmc* fm = (FirstOrderModelFmc*)m;
302
1588
  Trace("fmc") << "---Full Model Check preprocess() " << std::endl;
303
1588
  d_preinitialized_eqc.clear();
304
1588
  d_preinitialized_types.clear();
305
  //traverse equality engine
306
1588
  eq::EqClassesIterator eqcs_i = eq::EqClassesIterator( fm->d_equalityEngine );
307
98374
  while( !eqcs_i.isFinished() ){
308
96786
    Node r = *eqcs_i;
309
96786
    TypeNode tr = r.getType();
310
48393
    d_preinitialized_eqc[tr] = r;
311
48393
    ++eqcs_i;
312
  }
313
314
  //must ensure model basis terms exists in model for each relevant type
315
1588
  Trace("fmc") << "preInitialize types..." << std::endl;
316
1588
  fm->initialize();
317
9996
  for( std::map<Node, Def * >::iterator it = fm->d_models.begin(); it != fm->d_models.end(); ++it ) {
318
16816
    Node op = it->first;
319
8408
    Trace("fmc") << "preInitialize types for " << op << std::endl;
320
16816
    TypeNode tno = op.getType();
321
30457
    for( unsigned i=0; i<tno.getNumChildren(); i++) {
322
22049
      Trace("fmc") << "preInitializeType " << tno[i] << std::endl;
323
22049
      preInitializeType( fm, tno[i] );
324
22049
      Trace("fmc") << "finished preInitializeType " << tno[i] << std::endl;
325
    }
326
  }
327
1588
  Trace("fmc") << "Finish preInitialize types" << std::endl;
328
  //do not have to introduce terms for sorts of domains of quantified formulas if we are allowed to assume empty sorts
329
10712
  for (unsigned i = 0, nquant = fm->getNumAssertedQuantifiers(); i < nquant;
330
       i++)
331
  {
332
18248
    Node q = fm->getAssertedQuantifier(i);
333
    // make sure all types are set
334
22327
    for (const Node& v : q[0])
335
    {
336
13203
      preInitializeType(fm, v.getType());
337
    }
338
  }
339
1588
  return true;
340
}
341
342
1588
bool FullModelChecker::processBuildModel(TheoryModel* m){
343
1588
  if (!m->areFunctionValuesEnabled())
344
  {
345
    // nothing to do if no functions
346
    return true;
347
  }
348
1588
  FirstOrderModelFmc* fm = (FirstOrderModelFmc*)m;
349
1588
  Trace("fmc") << "---Full Model Check reset() " << std::endl;
350
1588
  d_quant_models.clear();
351
1588
  d_rep_ids.clear();
352
1588
  d_star_insts.clear();
353
  //process representatives
354
1588
  RepSet* rs = fm->getRepSetPtr();
355
8017
  for (std::map<TypeNode, std::vector<Node> >::iterator it =
356
1588
           rs->d_type_reps.begin();
357
9605
       it != rs->d_type_reps.end();
358
       ++it)
359
  {
360
8017
    if( it->first.isSort() ){
361
2440
      Trace("fmc") << "Cardinality( " << it->first << " )" << " = " << it->second.size() << std::endl;
362
6852
      for( size_t a=0; a<it->second.size(); a++ ){
363
8824
        Node r = fm->getRepresentative( it->second[a] );
364
4412
        if( Trace.isOn("fmc-model-debug") ){
365
          std::vector< Node > eqc;
366
          d_qstate.getEquivalenceClass(r, eqc);
367
          Trace("fmc-model-debug") << "   " << (it->second[a]==r);
368
          Trace("fmc-model-debug") << " : " << it->second[a] << " : " << r << " : ";
369
          //Trace("fmc-model-debug") << r2 << " : " << ir << " : ";
370
          Trace("fmc-model-debug") << " {";
371
          for( size_t i=0; i<eqc.size(); i++ ){
372
            Trace("fmc-model-debug") << eqc[i] << ", ";
373
          }
374
          Trace("fmc-model-debug") << "}" << std::endl;
375
        }
376
4412
        d_rep_ids[it->first][r] = (int)a;
377
      }
378
2440
      Trace("fmc-model-debug") << std::endl;
379
    }
380
  }
381
382
  //now, make models
383
9996
  for( std::map<Node, Def * >::iterator it = fm->d_models.begin(); it != fm->d_models.end(); ++it ) {
384
16816
    Node op = it->first;
385
    //reset the model
386
8408
    fm->d_models[op]->reset();
387
388
16816
    std::vector< Node > add_conds;
389
16816
    std::vector< Node > add_values;
390
8408
    bool needsDefault = true;
391
8408
    std::map< Node, std::vector< Node > >::iterator itut = fm->d_uf_terms.find( op );
392
8408
    if( itut!=fm->d_uf_terms.end() ){
393
6334
      Trace("fmc-model-debug") << itut->second.size() << " model values for " << op << " ... " << std::endl;
394
44660
      for( size_t i=0; i<itut->second.size(); i++ ){
395
76652
        Node n = itut->second[i];
396
        // only consider unique up to congruence (in model equality engine)?
397
38326
        add_conds.push_back( n );
398
38326
        add_values.push_back( n );
399
76652
        Node r = fm->getRepresentative(n);
400
38326
        Trace("fmc-model-debug") << n << " -> " << r << std::endl;
401
        //AlwaysAssert( fm->areEqual( itut->second[i], r ) );
402
      }
403
    }else{
404
2074
      Trace("fmc-model-debug") << "No model values for " << op << " ... " << std::endl;
405
    }
406
8408
    Trace("fmc-model-debug") << std::endl;
407
    //possibly get default
408
8408
    if( needsDefault ){
409
16816
      Node nmb = fm->getModelBasisOpTerm(op);
410
      //add default value if necessary
411
8408
      if( fm->hasTerm( nmb ) ){
412
4411
        Trace("fmc-model-debug") << "Add default " << nmb << std::endl;
413
4411
        add_conds.push_back( nmb );
414
4411
        add_values.push_back( nmb );
415
      }else{
416
7994
        Node vmb = getSomeDomainElement(fm, nmb.getType());
417
3997
        Trace("fmc-model-debug") << "Add default to default representative " << nmb << " ";
418
7994
        Trace("fmc-model-debug")
419
7994
            << fm->getRepSet()->getNumRepresentatives(nmb.getType())
420
3997
            << std::endl;
421
3997
        add_conds.push_back( nmb );
422
3997
        add_values.push_back( vmb );
423
      }
424
    }
425
426
16816
    std::vector< Node > conds;
427
16816
    std::vector< Node > values;
428
16816
    std::vector< Node > entry_conds;
429
    //get the entries for the model
430
55142
    for( size_t i=0; i<add_conds.size(); i++ ){
431
93468
      Node c = add_conds[i];
432
93468
      Node v = add_values[i];
433
93468
      Trace("fmc-model-debug")
434
46734
          << "Add cond/value : " << c << " -> " << v << std::endl;
435
93468
      std::vector< Node > children;
436
93468
      std::vector< Node > entry_children;
437
46734
      children.push_back(op);
438
46734
      entry_children.push_back(op);
439
46734
      bool hasNonStar = false;
440
129226
      for (const Node& ci : c)
441
      {
442
164984
        Node ri = fm->getRepresentative(ci);
443
82492
        children.push_back(ri);
444
82492
        bool isStar = false;
445
82492
        if (fm->isModelBasisTerm(ri))
446
        {
447
23597
          ri = fm->getStar(ri.getType());
448
23597
          isStar = true;
449
        }
450
        else
451
        {
452
58895
          hasNonStar = true;
453
        }
454
82492
        if( !isStar && !ri.isConst() ){
455
          Trace("fmc-warn") << "Warning : model for " << op
456
                            << " has non-constant argument in model " << ri
457
                            << " (from " << ci << ")" << std::endl;
458
          Assert(false);
459
        }
460
82492
        entry_children.push_back(ri);
461
      }
462
93468
      Node n = NodeManager::currentNM()->mkNode( APPLY_UF, children );
463
93468
      Node nv = fm->getRepresentative( v );
464
93468
      Trace("fmc-model-debug")
465
46734
          << "Representative of " << v << " is " << nv << std::endl;
466
46734
      if( !nv.isConst() ){
467
        Trace("fmc-warn") << "Warning : model for " << op << " has non-constant value in model " << nv << std::endl;
468
        Assert(false);
469
      }
470
93468
      Node en = (useSimpleModels() && hasNonStar) ? n : NodeManager::currentNM()->mkNode( APPLY_UF, entry_children );
471
46734
      if( std::find(conds.begin(), conds.end(), n )==conds.end() ){
472
26995
        Trace("fmc-model-debug") << "- add " << n << " -> " << nv << " (entry is " << en << ")" << std::endl;
473
26995
        conds.push_back(n);
474
26995
        values.push_back(nv);
475
26995
        entry_conds.push_back(en);
476
      }
477
      else {
478
19739
        Trace("fmc-model-debug") << "Already have entry for : " << n << " -> " << nv << " (entry is " << en << ")" << std::endl;
479
      }
480
    }
481
482
483
    //sort based on # default arguments
484
16816
    std::vector< int > indices;
485
16816
    ModelBasisArgSort mbas;
486
35403
    for (int i=0; i<(int)conds.size(); i++) {
487
26995
      mbas.d_terms.push_back(conds[i]);
488
26995
      mbas.d_mba_count[conds[i]] = fm->getModelBasisArg(conds[i]);
489
26995
      indices.push_back(i);
490
    }
491
8408
    std::sort( indices.begin(), indices.end(), mbas );
492
493
35403
    for (int i=0; i<(int)indices.size(); i++) {
494
26995
      fm->d_models[op]->addEntry(fm, entry_conds[indices[i]], values[indices[i]]);
495
    }
496
497
8408
    Trace("fmc-model-simplify") << "Before simplification : " << std::endl;
498
8408
    fm->d_models[op]->debugPrint("fmc-model-simplify", op, this);
499
8408
    Trace("fmc-model-simplify") << std::endl;
500
501
8408
    Trace("fmc-model-simplify") << "Simplifying " << op << "..." << std::endl;
502
8408
    fm->d_models[op]->simplify( this, fm );
503
504
8408
    fm->d_models[op]->debugPrint("fmc-model", op, this);
505
8408
    Trace("fmc-model") << std::endl;
506
507
    //for debugging
508
    /*
509
    for( size_t i=0; i<fm->d_uf_terms[op].size(); i++ ){
510
      std::vector< Node > inst;
511
      for( unsigned j=0; j<fm->d_uf_terms[op][i].getNumChildren(); j++ ){
512
        Node r = fm->getRepresentative( fm->d_uf_terms[op][i][j] );
513
        inst.push_back( r );
514
      }
515
      Node ev = fm->d_models[op]->evaluate( fm, inst );
516
      Trace("fmc-model-debug") << ".....Checking eval( " <<
517
    fm->d_uf_terms[op][i] << " ) = " << ev << std::endl; AlwaysAssert(
518
    fm->areEqual( ev, fm->d_uf_terms[op][i] ) );
519
    }
520
    */
521
  }
522
1588
  Assert(d_addedLemmas == 0);
523
524
  //make function values
525
9996
  for( std::map<Node, Def * >::iterator it = fm->d_models.begin(); it != fm->d_models.end(); ++it ){
526
16816
    Node f_def = getFunctionValue( fm, it->first, "$x" );
527
8408
    m->assignFunctionDefinition( it->first, f_def );
528
  }
529
1588
  return TheoryEngineModelBuilder::processBuildModel( m );
530
}
531
532
35252
void FullModelChecker::preInitializeType( FirstOrderModelFmc * fm, TypeNode tn ){
533
35252
  if( d_preinitialized_types.find( tn )==d_preinitialized_types.end() ){
534
5337
    d_preinitialized_types[tn] = true;
535
5337
    if (tn.isFirstClass())
536
    {
537
5331
      Trace("fmc") << "Get model basis term " << tn << "..." << std::endl;
538
10662
      Node mb = fm->getModelBasisTerm(tn);
539
5331
      Trace("fmc") << "...return " << mb << std::endl;
540
      // if the model basis term does not exist in the model,
541
      // either add it directly to the model's equality engine if no other terms
542
      // of this type exist, or otherwise assert that it is equal to the first
543
      // equivalence class of its type.
544
5331
      if (!fm->hasTerm(mb) && !mb.isConst())
545
      {
546
540
        std::map<TypeNode, Node>::iterator itpe = d_preinitialized_eqc.find(tn);
547
540
        if (itpe == d_preinitialized_eqc.end())
548
        {
549
400
          Trace("fmc") << "...add model basis term to EE of model " << mb << " "
550
200
                       << tn << std::endl;
551
200
          fm->d_equalityEngine->addTerm(mb);
552
        }
553
        else
554
        {
555
680
          Trace("fmc") << "...add model basis eqc equality to model " << mb
556
340
                       << " == " << itpe->second << " " << tn << std::endl;
557
340
          bool ret = fm->assertEquality(mb, itpe->second, true);
558
340
          AlwaysAssert(ret);
559
        }
560
      }
561
    }
562
  }
563
35252
}
564
565
364883
void FullModelChecker::debugPrintCond(const char * tr, Node n, bool dispStar) {
566
364883
  Trace(tr) << "(";
567
924223
  for( unsigned j=0; j<n.getNumChildren(); j++) {
568
559340
    if( j>0 ) Trace(tr) << ", ";
569
559340
    debugPrint(tr, n[j], dispStar);
570
  }
571
364883
  Trace(tr) << ")";
572
364883
}
573
574
1409181
void FullModelChecker::debugPrint(const char * tr, Node n, bool dispStar) {
575
1409181
  if( n.isNull() ){
576
14239
    Trace(tr) << "null";
577
  }
578
1394942
  else if (FirstOrderModelFmc::isStar(n) && dispStar)
579
  {
580
628885
    Trace(tr) << "*";
581
  }
582
  else
583
  {
584
1532114
    TypeNode tn = n.getType();
585
766057
    if( tn.isSort() && d_rep_ids.find(tn)!=d_rep_ids.end() ){
586
364376
      if (d_rep_ids[tn].find(n)!=d_rep_ids[tn].end()) {
587
343387
        Trace(tr) << d_rep_ids[tn][n];
588
      }else{
589
20989
        Trace(tr) << n;
590
      }
591
    }else{
592
401681
      Trace(tr) << n;
593
    }
594
  }
595
1409181
}
596
597
598
11036
int FullModelChecker::doExhaustiveInstantiation( FirstOrderModel * fm, Node f, int effort ) {
599
11036
  Trace("fmc") << "Full model check " << f << ", effort = " << effort << "..." << std::endl;
600
  // register the quantifier
601
11036
  registerQuantifiedFormula(f);
602
11036
  Assert(!d_qstate.isInConflict());
603
  // we do not do model-based quantifier instantiation if the option
604
  // disables it, or if the quantified formula has an unhandled type.
605
11036
  if (!optUseModel() || !isHandled(f))
606
  {
607
    return 0;
608
  }
609
11036
  FirstOrderModelFmc* fmfmc = static_cast<FirstOrderModelFmc*>(fm);
610
11036
  if (effort == 0)
611
  {
612
8846
    if (options::mbqiMode() == options::MbqiMode::NONE)
613
    {
614
      // just exhaustive instantiate
615
6694
      Node c = mkCondDefault(fmfmc, f);
616
3347
      d_quant_models[f].addEntry(fmfmc, c, d_false);
617
3347
      if (!exhaustiveInstantiate(fmfmc, f, c))
618
      {
619
22
        return 0;
620
      }
621
3325
      return 1;
622
    }
623
    // model check the quantifier
624
5499
    doCheck(fmfmc, f, d_quant_models[f], f[1]);
625
5499
    std::vector<Node>& mcond = d_quant_models[f].d_cond;
626
5499
    Trace("fmc") << "Definition for quantifier " << f << " is : " << std::endl;
627
5499
    Assert(!mcond.empty());
628
5499
    d_quant_models[f].debugPrint("fmc", Node::null(), this);
629
5499
    Trace("fmc") << std::endl;
630
631
    // consider all entries going to non-true
632
5499
    Instantiate* instq = d_qe->getInstantiate();
633
12810
    for (unsigned i = 0, msize = mcond.size(); i < msize; i++)
634
    {
635
7311
      if (d_quant_models[f].d_value[i] == d_true)
636
      {
637
        // already satisfied
638
10043
        continue;
639
      }
640
4588
      Trace("fmc-inst") << "Instantiate based on " << mcond[i] << "..."
641
2294
                        << std::endl;
642
2294
      bool hasStar = false;
643
4579
      std::vector<Node> inst;
644
5967
      for (unsigned j = 0, nchild = mcond[i].getNumChildren(); j < nchild; j++)
645
      {
646
3673
        if (fmfmc->isStar(mcond[i][j]))
647
        {
648
2904
          hasStar = true;
649
2904
          inst.push_back(fmfmc->getModelBasisTerm(mcond[i][j].getType()));
650
        }
651
        else
652
        {
653
769
          inst.push_back(mcond[i][j]);
654
        }
655
      }
656
2294
      bool addInst = true;
657
2294
      if (hasStar)
658
      {
659
        // try obvious (specified by inst)
660
4012
        Node ev = d_quant_models[f].evaluate(fmfmc, inst);
661
2006
        if (ev == d_true)
662
        {
663
9
          addInst = false;
664
18
          Trace("fmc-debug")
665
9
              << "...do not instantiate, evaluation was " << ev << std::endl;
666
        }
667
      }
668
      else
669
      {
670
        // for debugging
671
288
        if (Trace.isOn("fmc-test-inst"))
672
        {
673
          Node ev = d_quant_models[f].evaluate(fmfmc, inst);
674
          if (ev == d_true)
675
          {
676
            CVC4Message() << "WARNING: instantiation was true! " << f << " "
677
                          << mcond[i] << std::endl;
678
            AlwaysAssert(false);
679
          }
680
          else
681
          {
682
            Trace("fmc-test-inst")
683
                << "...instantiation evaluated to false." << std::endl;
684
          }
685
        }
686
      }
687
2303
      if (!addInst)
688
      {
689
18
        Trace("fmc-debug-inst")
690
9
            << "** Instantiation was already true." << std::endl;
691
        // might try it next effort level
692
9
        d_star_insts[f].push_back(i);
693
9
        continue;
694
      }
695
2285
      if (options::fmfBound())
696
      {
697
        std::vector<Node> cond;
698
        cond.push_back(d_quant_cond[f]);
699
        cond.insert(cond.end(), inst.begin(), inst.end());
700
        // need to do exhaustive instantiate algorithm to set things properly
701
        // (should only add one instance)
702
        Node c = mkCond(cond);
703
        unsigned prevInst = d_addedLemmas;
704
        exhaustiveInstantiate(fmfmc, f, c);
705
        if (d_addedLemmas == prevInst)
706
        {
707
          d_star_insts[f].push_back(i);
708
        }
709
        continue;
710
      }
711
      // just add the instance
712
2285
      d_triedLemmas++;
713
2285
      if (instq->addInstantiation(
714
              f, inst, InferenceId::QUANTIFIERS_INST_FMF_FMC, true))
715
      {
716
683
        Trace("fmc-debug-inst") << "** Added instantiation." << std::endl;
717
683
        d_addedLemmas++;
718
6493
        if (d_qstate.isInConflict() || options::fmfOneInstPerRound())
719
        {
720
          break;
721
        }
722
      }
723
      else
724
      {
725
3204
        Trace("fmc-debug-inst")
726
1602
            << "** Instantiation was duplicate." << std::endl;
727
        // might try it next effort level
728
1602
        d_star_insts[f].push_back(i);
729
      }
730
    }
731
5499
    return 1;
732
  }
733
  // Get the list of instantiation regions (described by "star entries" in the
734
  // definition) that were not tried at the previous effort level. For each
735
  // of these, we add one instantiation.
736
2190
  std::vector<Node>& mcond = d_quant_models[f].d_cond;
737
2190
  if (!d_star_insts[f].empty())
738
  {
739
766
    if (Trace.isOn("fmc-exh"))
740
    {
741
      Trace("fmc-exh") << "Exhaustive instantiate " << f << std::endl;
742
      Trace("fmc-exh") << "Definition was : " << std::endl;
743
      d_quant_models[f].debugPrint("fmc-exh", Node::null(), this);
744
      Trace("fmc-exh") << std::endl;
745
    }
746
1530
    Def temp;
747
    // simplify the exceptions?
748
1628
    for (int i = (d_star_insts[f].size() - 1); i >= 0; i--)
749
    {
750
      // get witness for d_star_insts[f][i]
751
864
      int j = d_star_insts[f][i];
752
864
      if (temp.addEntry(fmfmc, mcond[j], d_quant_models[f].d_value[j]))
753
      {
754
838
        if (!exhaustiveInstantiate(fmfmc, f, mcond[j]))
755
        {
756
          // something went wrong, resort to exhaustive instantiation
757
2
          return 0;
758
        }
759
      }
760
    }
761
  }
762
2188
  return 1;
763
}
764
765
/** Representative bound fmc entry
766
 *
767
 * This bound information corresponds to one
768
 * entry in a term definition (see terminology in
769
 * Chapter 5 of Finite Model Finding for
770
 * Satisfiability Modulo Theories thesis).
771
 * For example, a term definition for the body
772
 * of a quantified formula:
773
 *   forall xyz. P( x, y, z )
774
 * may be:
775
 *   ( 0, 0, 0 ) -> false
776
 *   ( *, 1, 2 ) -> false
777
 *   ( *, *, * ) -> true
778
 * Indicating that the quantified formula evaluates
779
 * to false in the current model for x=0, y=0, z=0,
780
 * or y=1, z=2 for any x, and evaluates to true
781
 * otherwise.
782
 * This class is used if we wish
783
 * to iterate over all values corresponding to one
784
 * of these entries. For example, for the second entry:
785
 *   (*, 1, 2 )
786
 * we iterate over all values of x, but only {1}
787
 * for y and {2} for z.
788
 */
789
class RepBoundFmcEntry : public QRepBoundExt
790
{
791
 public:
792
4185
  RepBoundFmcEntry(QuantifiersBoundInference& qbi,
793
                   Node e,
794
                   FirstOrderModelFmc* f)
795
4185
      : QRepBoundExt(qbi, f), d_entry(e), d_fm(f)
796
  {
797
4185
  }
798
4185
  ~RepBoundFmcEntry() {}
799
  /** set bound */
800
5738
  virtual RsiEnumType setBound(Node owner,
801
                               unsigned i,
802
                               std::vector<Node>& elements) override
803
  {
804
5738
    if (!d_fm->isStar(d_entry[i]))
805
    {
806
      // only need to consider the single point
807
234
      elements.push_back(d_entry[i]);
808
234
      return ENUM_DEFAULT;
809
    }
810
5504
    return QRepBoundExt::setBound(owner, i, elements);
811
  }
812
813
 private:
814
  /** the entry for this bound */
815
  Node d_entry;
816
  /** the model builder associated with this bound */
817
  FirstOrderModelFmc* d_fm;
818
};
819
820
4185
bool FullModelChecker::exhaustiveInstantiate(FirstOrderModelFmc* fm,
821
                                             Node f,
822
                                             Node c)
823
{
824
4185
  Trace("fmc-exh") << "----Exhaustive instantiate based on " << c << " ";
825
4185
  debugPrintCond("fmc-exh", c, true);
826
4185
  Trace("fmc-exh")<< std::endl;
827
4185
  QuantifiersBoundInference& qbi = d_qreg.getQuantifiersBoundInference();
828
8370
  RepBoundFmcEntry rbfe(qbi, c, fm);
829
8370
  RepSetIterator riter(fm->getRepSet(), &rbfe);
830
4185
  Trace("fmc-exh-debug") << "Set quantifier..." << std::endl;
831
  //initialize
832
4185
  if (riter.setQuantifier(f))
833
  {
834
4185
    Trace("fmc-exh-debug") << "Set element domains..." << std::endl;
835
4185
    int addedLemmas = 0;
836
    //now do full iteration
837
62627
    while( !riter.isFinished() ){
838
29221
      d_triedLemmas++;
839
29221
      Trace("fmc-exh-debug") << "Inst : ";
840
58442
      std::vector< Node > ev_inst;
841
58442
      std::vector< Node > inst;
842
101911
      for (unsigned i = 0; i < riter.getNumTerms(); i++)
843
      {
844
145380
        TypeNode tn = riter.getTypeOf(i);
845
        // if the type is not closed enumerable (see
846
        // TypeNode::isClosedEnumerable), then we must ensure that we are
847
        // using a term and not a value. This ensures that e.g. uninterpreted
848
        // constants do not appear in instantiations.
849
145380
        Node rr = riter.getCurrentTerm(i, !tn.isClosedEnumerable());
850
145380
        Node r = fm->getRepresentative(rr);
851
72690
        debugPrint("fmc-exh-debug", r);
852
72690
        Trace("fmc-exh-debug") << " (term : " << rr << ")";
853
72690
        ev_inst.push_back( r );
854
72690
        inst.push_back( rr );
855
      }
856
29221
      int ev_index = d_quant_models[f].getGeneralizationIndex(fm, ev_inst);
857
29221
      Trace("fmc-exh-debug") << ", index = " << ev_index << " / " << d_quant_models[f].d_value.size();
858
58442
      Node ev = ev_index==-1 ? Node::null() : d_quant_models[f].d_value[ev_index];
859
29221
      if (ev!=d_true) {
860
26705
        Trace("fmc-exh-debug") << ", add!";
861
        //add as instantiation
862
26705
        if (d_qe->getInstantiate()->addInstantiation(
863
                f, inst, InferenceId::QUANTIFIERS_INST_FMF_FMC_EXH, true))
864
        {
865
4866
          Trace("fmc-exh-debug")  << " ...success.";
866
4866
          addedLemmas++;
867
4866
          if (d_qstate.isInConflict() || options::fmfOneInstPerRound())
868
          {
869
            break;
870
          }
871
        }else{
872
21839
          Trace("fmc-exh-debug") << ", failed.";
873
        }
874
      }else{
875
2516
        Trace("fmc-exh-debug") << ", already true";
876
      }
877
29221
      Trace("fmc-exh-debug") << std::endl;
878
29221
      int index = riter.increment();
879
29221
      Trace("fmc-exh-debug") << "Incremented index " << index << std::endl;
880
29221
      if( !riter.isFinished() ){
881
77793
        if (index >= 0 && riter.d_index[index] > 0 && addedLemmas > 0
882
32366
            && riter.d_enum_type[index] == ENUM_CUSTOM)
883
        {
884
2826
          Trace("fmc-exh-debug")
885
1413
              << "Since this is a custom enumeration, skip to the next..."
886
1413
              << std::endl;
887
1413
          riter.incrementAtIndex(index - 1);
888
        }
889
      }
890
    }
891
4185
    d_addedLemmas += addedLemmas;
892
4185
    Trace("fmc-exh") << "----Finished Exhaustive instantiate, lemmas = " << addedLemmas << ", incomplete=" << riter.isIncomplete() << std::endl;
893
4185
    return addedLemmas>0 || !riter.isIncomplete();
894
  }else{
895
    Trace("fmc-exh") << "----Finished Exhaustive instantiate, failed." << std::endl;
896
    return !riter.isIncomplete();
897
  }
898
}
899
900
88698
void FullModelChecker::doCheck(FirstOrderModelFmc * fm, Node f, Def & d, Node n ) {
901
88698
  Trace("fmc-debug") << "Check " << n << " " << n.getKind() << std::endl;
902
  //first check if it is a bounding literal
903
88698
  if( n.hasAttribute(BoundIntLitAttribute()) ){
904
    Trace("fmc-debug") << "It is a bounding literal, polarity = " << n.getAttribute(BoundIntLitAttribute()) << std::endl;
905
    d.addEntry(fm, mkCondDefault(fm, f), n.getAttribute(BoundIntLitAttribute())==1 ? d_false : d_true );
906
88698
  }else if( n.getKind() == kind::BOUND_VARIABLE ){
907
20998
    Trace("fmc-debug") << "Add default entry..." << std::endl;
908
20998
    d.addEntry(fm, mkCondDefault(fm, f), n);
909
  }
910
67700
  else if( n.getKind() == kind::NOT ){
911
    //just do directly
912
6948
    doCheck( fm, f, d, n[0] );
913
6948
    doNegate( d );
914
  }
915
60752
  else if( n.getKind() == kind::FORALL ){
916
2867
    d.addEntry(fm, mkCondDefault(fm, f), Node::null());
917
  }
918
57885
  else if( n.getType().isArray() ){
919
    //Trace("fmc-warn") << "WARNING : ARRAYS : Can't process base array " << r << std::endl;
920
    //Trace("fmc-warn") << "          Default value was : " << odefaultValue << std::endl;
921
    //Trace("fmc-debug") << "Can't process base array " << r << std::endl;
922
    //can't process this array
923
452
    d.reset();
924
452
    d.addEntry(fm, mkCondDefault(fm, f), Node::null());
925
  }
926
57433
  else if( n.getNumChildren()==0 ){
927
19384
    Node r = n;
928
9692
    if( !n.isConst() ){
929
5950
      if( !fm->hasTerm(n) ){
930
201
        r = getSomeDomainElement(fm, n.getType() );
931
      }
932
5950
      r = fm->getRepresentative( r );
933
    }
934
9692
    Trace("fmc-debug") << "Add constant entry..." << std::endl;
935
9692
    d.addEntry(fm, mkCondDefault(fm, f), r);
936
  }
937
  else{
938
95482
    std::vector< int > var_ch;
939
95482
    std::vector< Def > children;
940
123992
    for( int i=0; i<(int)n.getNumChildren(); i++) {
941
152502
      Def dc;
942
76251
      doCheck(fm, f, dc, n[i]);
943
76251
      children.push_back(dc);
944
76251
      if( n[i].getKind() == kind::BOUND_VARIABLE ){
945
20994
        var_ch.push_back(i);
946
      }
947
    }
948
949
47741
    if( n.getKind()==APPLY_UF ){
950
24911
      Trace("fmc-debug") << "Do uninterpreted compose " << n << std::endl;
951
      //uninterpreted compose
952
24911
      doUninterpretedCompose( fm, f, d, n.getOperator(), children );
953
      /*
954
    } else if( n.getKind()==SELECT ){
955
      Trace("fmc-debug") << "Do select compose " << n << std::endl;
956
      std::vector< Def > children2;
957
      children2.push_back( children[1] );
958
      std::vector< Node > cond;
959
      mkCondDefaultVec(fm, f, cond);
960
      std::vector< Node > val;
961
      doUninterpretedCompose(fm, f, d, children[0], children2, 0, cond, val );
962
      */
963
    } else {
964
22830
      if( !var_ch.empty() ){
965
1396
        if( n.getKind()==EQUAL && !n[0].getType().isBoolean() ){
966
773
          if( var_ch.size()==2 ){
967
344
            Trace("fmc-debug") << "Do variable equality " << n << std::endl;
968
344
            doVariableEquality( fm, f, d, n );
969
          }else{
970
429
            Trace("fmc-debug") << "Do variable relation " << n << std::endl;
971
429
            doVariableRelation( fm, f, d, var_ch[0]==0 ? children[1] : children[0], var_ch[0]==0 ? n[0] : n[1] );
972
          }
973
        }else{
974
623
          Trace("fmc-warn") << "Don't know how to check " << n << std::endl;
975
623
          d.addEntry(fm, mkCondDefault(fm, f), Node::null());
976
        }
977
      }else{
978
21434
        Trace("fmc-debug") << "Do interpreted compose " << n << std::endl;
979
42868
        std::vector< Node > cond;
980
21434
        mkCondDefaultVec(fm, f, cond);
981
42868
        std::vector< Node > val;
982
        //interpreted compose
983
21434
        doInterpretedCompose( fm, f, d, n, children, 0, cond, val );
984
      }
985
    }
986
47741
    Trace("fmc-debug") << "Simplify the definition..." << std::endl;
987
47741
    d.debugPrint("fmc-debug", Node::null(), this);
988
47741
    d.simplify(this, fm);
989
47741
    Trace("fmc-debug") << "Done simplifying" << std::endl;
990
  }
991
88698
  Trace("fmc-debug") << "Definition for " << n << " is : " << std::endl;
992
88698
  d.debugPrint("fmc-debug", Node::null(), this);
993
88698
  Trace("fmc-debug") << std::endl;
994
88698
}
995
996
6948
void FullModelChecker::doNegate( Def & dc ) {
997
15985
  for (unsigned i=0; i<dc.d_cond.size(); i++) {
998
18074
    Node v = dc.d_value[i];
999
9037
    if (!v.isNull())
1000
    {
1001
      // In the case that the value is not-constant, we cannot reason about
1002
      // its value (since the range of this must be a constant or variable).
1003
      // In particular, returning null here is important if we have (not x)
1004
      // where x is a bound variable.
1005
6080
      dc.d_value[i] =
1006
12160
          v == d_true ? d_false : (v == d_false ? d_true : Node::null());
1007
    }
1008
  }
1009
6948
}
1010
1011
344
void FullModelChecker::doVariableEquality( FirstOrderModelFmc * fm, Node f, Def & d, Node eq ) {
1012
688
  std::vector<Node> cond;
1013
344
  mkCondDefaultVec(fm, f, cond);
1014
344
  if (eq[0]==eq[1]){
1015
    d.addEntry(fm, mkCond(cond), d_true);
1016
  }else{
1017
688
    TypeNode tn = eq[0].getType();
1018
344
    if( tn.isSort() ){
1019
344
      int j = fm->getVariableId(f, eq[0]);
1020
344
      int k = fm->getVariableId(f, eq[1]);
1021
344
      const RepSet* rs = fm->getRepSet();
1022
344
      if (!rs->hasType(tn))
1023
      {
1024
        getSomeDomainElement( fm, tn );  //to verify the type is initialized
1025
      }
1026
344
      unsigned nreps = rs->getNumRepresentatives(tn);
1027
932
      for (unsigned i = 0; i < nreps; i++)
1028
      {
1029
1176
        Node r = fm->getRepresentative(rs->getRepresentative(tn, i));
1030
588
        cond[j+1] = r;
1031
588
        cond[k+1] = r;
1032
588
        d.addEntry( fm, mkCond(cond), d_true);
1033
      }
1034
344
      d.addEntry( fm, mkCondDefault(fm, f), d_false);
1035
    }else{
1036
      d.addEntry( fm, mkCondDefault(fm, f), Node::null());
1037
    }
1038
  }
1039
344
}
1040
1041
429
void FullModelChecker::doVariableRelation( FirstOrderModelFmc * fm, Node f, Def & d, Def & dc, Node v) {
1042
429
  int j = fm->getVariableId(f, v);
1043
983
  for (unsigned i=0; i<dc.d_cond.size(); i++) {
1044
1108
    Node val = dc.d_value[i];
1045
554
    if( val.isNull() ){
1046
9
      d.addEntry( fm, dc.d_cond[i], val);
1047
    }else{
1048
545
      if( dc.d_cond[i][j]!=val ){
1049
428
        if (fm->isStar(dc.d_cond[i][j])) {
1050
840
          std::vector<Node> cond;
1051
420
          mkCondVec(dc.d_cond[i],cond);
1052
420
          cond[j+1] = val;
1053
420
          d.addEntry(fm, mkCond(cond), d_true);
1054
420
          cond[j+1] = fm->getStar(val.getType());
1055
420
          d.addEntry(fm, mkCond(cond), d_false);
1056
        }else{
1057
8
          d.addEntry( fm, dc.d_cond[i], d_false);
1058
        }
1059
      }else{
1060
117
        d.addEntry( fm, dc.d_cond[i], d_true);
1061
      }
1062
    }
1063
  }
1064
429
}
1065
1066
24911
void FullModelChecker::doUninterpretedCompose( FirstOrderModelFmc * fm, Node f, Def & d, Node op, std::vector< Def > & dc ) {
1067
24911
  Trace("fmc-uf-debug") << "Definition : " << std::endl;
1068
24911
  fm->d_models[op]->debugPrint("fmc-uf-debug", op, this);
1069
24911
  Trace("fmc-uf-debug") << std::endl;
1070
1071
49822
  std::vector< Node > cond;
1072
24911
  mkCondDefaultVec(fm, f, cond);
1073
49822
  std::vector< Node > val;
1074
24911
  doUninterpretedCompose( fm, f, d, *fm->d_models[op], dc, 0, cond, val);
1075
24911
}
1076
1077
65838
void FullModelChecker::doUninterpretedCompose( FirstOrderModelFmc * fm, Node f, Def & d,
1078
                                               Def & df, std::vector< Def > & dc, int index,
1079
                                               std::vector< Node > & cond, std::vector<Node> & val ) {
1080
65838
  Trace("fmc-uf-process") << "process at " << index << std::endl;
1081
178255
  for( unsigned i=1; i<cond.size(); i++) {
1082
112417
    debugPrint("fmc-uf-process", cond[i], true);
1083
112417
    Trace("fmc-uf-process") << " ";
1084
  }
1085
65838
  Trace("fmc-uf-process") << std::endl;
1086
65838
  if (index==(int)dc.size()) {
1087
    //we have an entry, now do actual compose
1088
61922
    std::map< int, Node > entries;
1089
30961
    doUninterpretedCompose2( fm, f, entries, 0, cond, val, df.d_et);
1090
30961
    if( entries.empty() ){
1091
189
      d.addEntry(fm, mkCond(cond), Node::null());
1092
    }else{
1093
      //add them to the definition
1094
121041
      for( unsigned e=0; e<df.d_cond.size(); e++ ){
1095
90269
        if ( entries.find(e)!=entries.end() ){
1096
53257
          Trace("fmf-uf-process-debug") << "Add entry..." << std::endl;
1097
53257
          d.addEntry(fm, entries[e], df.d_value[e] );
1098
53257
          Trace("fmf-uf-process-debug") << "Done add entry." << std::endl;
1099
        }
1100
      }
1101
    }
1102
  }else{
1103
78753
    for (unsigned i=0; i<dc[index].d_cond.size(); i++) {
1104
43876
      if (isCompat(fm, cond, dc[index].d_cond[i])!=0) {
1105
81854
        std::vector< Node > new_cond;
1106
40927
        new_cond.insert(new_cond.end(), cond.begin(), cond.end());
1107
40927
        if( doMeet(fm, new_cond, dc[index].d_cond[i]) ){
1108
40927
          Trace("fmc-uf-process") << "index " << i << " succeeded meet." << std::endl;
1109
40927
          val.push_back(dc[index].d_value[i]);
1110
40927
          doUninterpretedCompose(fm, f, d, df, dc, index+1, new_cond, val);
1111
40927
          val.pop_back();
1112
        }else{
1113
          Trace("fmc-uf-process") << "index " << i << " failed meet." << std::endl;
1114
        }
1115
      }
1116
    }
1117
  }
1118
65838
}
1119
1120
102128
void FullModelChecker::doUninterpretedCompose2( FirstOrderModelFmc * fm, Node f,
1121
                                                std::map< int, Node > & entries, int index,
1122
                                                std::vector< Node > & cond, std::vector< Node > & val,
1123
                                                EntryTrie & curr ) {
1124
102128
  Trace("fmc-uf-process") << "compose " << index << " / " << val.size() << std::endl;
1125
274688
  for( unsigned i=1; i<cond.size(); i++) {
1126
172560
    debugPrint("fmc-uf-process", cond[i], true);
1127
172560
    Trace("fmc-uf-process") << " ";
1128
  }
1129
102128
  Trace("fmc-uf-process") << std::endl;
1130
102128
  if (index==(int)val.size()) {
1131
106514
    Node c = mkCond(cond);
1132
53257
    Trace("fmc-uf-entry") << "Entry : " << c << " -> index[" << curr.d_data << "]" << std::endl;
1133
53257
    entries[curr.d_data] = c;
1134
  }else{
1135
97742
    Node v = val[index];
1136
48871
    Trace("fmc-uf-process") << "Process " << v << std::endl;
1137
48871
    bool bind_var = false;
1138
48871
    if( !v.isNull() && v.getKind()==kind::BOUND_VARIABLE ){
1139
21915
      int j = fm->getVariableId(f, v);
1140
21915
      Trace("fmc-uf-process") << v << " is variable #" << j << std::endl;
1141
21915
      if (!fm->isStar(cond[j + 1]))
1142
      {
1143
38
        v = cond[j+1];
1144
      }else{
1145
21877
        bind_var = true;
1146
      }
1147
    }
1148
48871
    if (bind_var) {
1149
21877
      Trace("fmc-uf-process") << "bind variable..." << std::endl;
1150
21877
      int j = fm->getVariableId(f, v);
1151
21877
      Assert(fm->isStar(cond[j + 1]));
1152
60728
      for (std::map<Node, EntryTrie>::iterator it = curr.d_child.begin();
1153
60728
           it != curr.d_child.end();
1154
           ++it)
1155
      {
1156
38851
        cond[j + 1] = it->first;
1157
38851
        doUninterpretedCompose2(
1158
38851
            fm, f, entries, index + 1, cond, val, it->second);
1159
      }
1160
21877
      cond[j + 1] = fm->getStar(v.getType());
1161
    }else{
1162
26994
      if( !v.isNull() ){
1163
26796
        if (curr.d_child.find(v) != curr.d_child.end())
1164
        {
1165
9503
          Trace("fmc-uf-process") << "follow value..." << std::endl;
1166
9503
          doUninterpretedCompose2(
1167
9503
              fm, f, entries, index + 1, cond, val, curr.d_child[v]);
1168
        }
1169
53592
        Node st = fm->getStar(v.getType());
1170
26796
        if (curr.d_child.find(st) != curr.d_child.end())
1171
        {
1172
22813
          Trace("fmc-uf-process") << "follow star..." << std::endl;
1173
22813
          doUninterpretedCompose2(
1174
22813
              fm, f, entries, index + 1, cond, val, curr.d_child[st]);
1175
        }
1176
      }
1177
    }
1178
  }
1179
102128
}
1180
1181
92741
void FullModelChecker::doInterpretedCompose( FirstOrderModelFmc * fm, Node f, Def & d, Node n,
1182
                                             std::vector< Def > & dc, int index,
1183
                                             std::vector< Node > & cond, std::vector<Node> & val ) {
1184
92741
  Trace("fmc-if-process") << "int compose " << index << " / " << dc.size() << std::endl;
1185
224217
  for( unsigned i=1; i<cond.size(); i++) {
1186
131476
    debugPrint("fmc-if-process", cond[i], true);
1187
131476
    Trace("fmc-if-process") << " ";
1188
  }
1189
92741
  Trace("fmc-if-process") << std::endl;
1190
92741
  if ( index==(int)dc.size() ){
1191
87886
    Node c = mkCond(cond);
1192
87886
    Node v = evaluateInterpreted(n, val);
1193
43943
    d.addEntry(fm, c, v);
1194
  }
1195
  else {
1196
97596
    TypeNode vtn = n.getType();
1197
137565
    for (unsigned i=0; i<dc[index].d_cond.size(); i++) {
1198
88767
      if (isCompat(fm, cond, dc[index].d_cond[i])!=0) {
1199
155448
        std::vector< Node > new_cond;
1200
77724
        new_cond.insert(new_cond.end(), cond.begin(), cond.end());
1201
77724
        if( doMeet(fm, new_cond, dc[index].d_cond[i]) ){
1202
77724
          bool process = true;
1203
77724
          if (vtn.isBoolean()) {
1204
            //short circuit
1205
115115
            if( (n.getKind()==OR && dc[index].d_value[i]==d_true) ||
1206
55151
                (n.getKind()==AND && dc[index].d_value[i]==d_false) ){
1207
12834
              Node c = mkCond(new_cond);
1208
6417
              d.addEntry(fm, c, dc[index].d_value[i]);
1209
6417
              process = false;
1210
            }
1211
          }
1212
77724
          if (process) {
1213
71307
            val.push_back(dc[index].d_value[i]);
1214
71307
            doInterpretedCompose(fm, f, d, n, dc, index+1, new_cond, val);
1215
71307
            val.pop_back();
1216
          }
1217
        }
1218
      }
1219
    }
1220
  }
1221
92741
}
1222
1223
132643
int FullModelChecker::isCompat( FirstOrderModelFmc * fm, std::vector< Node > & cond, Node c ) {
1224
132643
  Trace("fmc-debug3") << "isCompat " << c << std::endl;
1225
132643
  Assert(cond.size() == c.getNumChildren() + 1);
1226
340486
  for (unsigned i=1; i<cond.size(); i++) {
1227
221835
    if (cond[i] != c[i - 1] && !fm->isStar(cond[i]) && !fm->isStar(c[i - 1]))
1228
    {
1229
13992
      return 0;
1230
    }
1231
  }
1232
118651
  return 1;
1233
}
1234
1235
118651
bool FullModelChecker::doMeet( FirstOrderModelFmc * fm, std::vector< Node > & cond, Node c ) {
1236
118651
  Trace("fmc-debug3") << "doMeet " << c << std::endl;
1237
118651
  Assert(cond.size() == c.getNumChildren() + 1);
1238
313356
  for (unsigned i=1; i<cond.size(); i++) {
1239
194705
    if( cond[i]!=c[i-1] ) {
1240
63076
      if (fm->isStar(cond[i]))
1241
      {
1242
37775
        cond[i] = c[i - 1];
1243
      }
1244
25301
      else if (!fm->isStar(c[i - 1]))
1245
      {
1246
        return false;
1247
      }
1248
    }
1249
  }
1250
118651
  return true;
1251
}
1252
1253
143557
Node FullModelChecker::mkCond( std::vector< Node > & cond ) {
1254
143557
  return NodeManager::currentNM()->mkNode(APPLY_UF, cond);
1255
}
1256
1257
38323
Node FullModelChecker::mkCondDefault( FirstOrderModelFmc * fm, Node f) {
1258
76646
  std::vector< Node > cond;
1259
38323
  mkCondDefaultVec(fm, f, cond);
1260
76646
  return mkCond(cond);
1261
}
1262
1263
85012
void FullModelChecker::mkCondDefaultVec( FirstOrderModelFmc * fm, Node f, std::vector< Node > & cond ) {
1264
85012
  Trace("fmc-debug") << "Make default vec" << std::endl;
1265
  //get function symbol for f
1266
85012
  cond.push_back(d_quant_cond[f]);
1267
219800
  for (unsigned i=0; i<f[0].getNumChildren(); i++) {
1268
269576
    Node ts = fm->getStar(f[0][i].getType());
1269
134788
    Assert(ts.getType() == f[0][i].getType());
1270
134788
    cond.push_back(ts);
1271
  }
1272
85012
}
1273
1274
420
void FullModelChecker::mkCondVec( Node n, std::vector< Node > & cond ) {
1275
420
  cond.push_back(n.getOperator());
1276
976
  for( unsigned i=0; i<n.getNumChildren(); i++ ){
1277
556
    cond.push_back( n[i] );
1278
  }
1279
420
}
1280
1281
43943
Node FullModelChecker::evaluateInterpreted( Node n, std::vector< Node > & vals ) {
1282
43943
  if( n.getKind()==EQUAL && !n[0].getType().isBoolean() ){
1283
11817
    if (!vals[0].isNull() && !vals[1].isNull()) {
1284
11515
      return vals[0]==vals[1] ? d_true : d_false;
1285
    }else{
1286
302
      return Node::null();
1287
    }
1288
32126
  }else if( n.getKind()==ITE ){
1289
6135
    if( vals[0]==d_true ){
1290
2673
      return vals[1];
1291
3462
    }else if( vals[0]==d_false ){
1292
3417
      return vals[2];
1293
    }else{
1294
45
      return vals[1]==vals[2] ? vals[1] : Node::null();
1295
    }
1296
25991
  }else if( n.getKind()==AND || n.getKind()==OR ){
1297
4243
    bool isNull = false;
1298
15053
    for (unsigned i=0; i<vals.size(); i++) {
1299
10810
      if((vals[i]==d_true && n.getKind()==OR) || (vals[i]==d_false && n.getKind()==AND)) {
1300
        return vals[i];
1301
10810
      }else if( vals[i].isNull() ){
1302
2479
        isNull = true;
1303
      }
1304
    }
1305
4243
    return isNull ? Node::null() : vals[0];
1306
  }else{
1307
43496
    std::vector<Node> children;
1308
21748
    if( n.getMetaKind() == kind::metakind::PARAMETERIZED ){
1309
15220
      children.push_back( n.getOperator() );
1310
    }
1311
51208
    for (unsigned i=0; i<vals.size(); i++) {
1312
29740
      if( vals[i].isNull() ){
1313
280
        return Node::null();
1314
      }else{
1315
29460
        children.push_back( vals[i] );
1316
      }
1317
    }
1318
42936
    Node nc = NodeManager::currentNM()->mkNode(n.getKind(), children);
1319
21468
    Trace("fmc-eval") << "Evaluate " << nc << " to ";
1320
21468
    nc = Rewriter::rewrite(nc);
1321
21468
    Trace("fmc-eval") << nc << std::endl;
1322
21468
    return nc;
1323
  }
1324
}
1325
1326
4198
Node FullModelChecker::getSomeDomainElement( FirstOrderModelFmc * fm, TypeNode tn ) {
1327
4198
  bool addRepId = !fm->getRepSet()->hasType(tn);
1328
4198
  Node de = fm->getSomeDomainElement(tn);
1329
4198
  if( addRepId ){
1330
127
    d_rep_ids[tn][de] = 0;
1331
  }
1332
4198
  return de;
1333
}
1334
1335
8408
Node FullModelChecker::getFunctionValue(FirstOrderModelFmc * fm, Node op, const char* argPrefix ) {
1336
8408
  return fm->getFunctionValue(op, argPrefix);
1337
}
1338
1339
1340
46734
bool FullModelChecker::useSimpleModels() {
1341
93468
  return options::fmfFmcSimple();
1342
}
1343
1344
11036
void FullModelChecker::registerQuantifiedFormula(Node q)
1345
{
1346
11036
  if (d_quant_cond.find(q) != d_quant_cond.end())
1347
  {
1348
9904
    return;
1349
  }
1350
1132
  NodeManager* nm = NodeManager::currentNM();
1351
2264
  std::vector<TypeNode> types;
1352
2711
  for (const Node& v : q[0])
1353
  {
1354
3158
    TypeNode tn = v.getType();
1355
1579
    if (tn.isFunction())
1356
    {
1357
      // we will not use model-based quantifier instantiation for q, since
1358
      // the model-based instantiation algorithm does not handle (universally
1359
      // quantified) functions
1360
      d_unhandledQuant.insert(q);
1361
    }
1362
1579
    types.push_back(tn);
1363
  }
1364
2264
  TypeNode typ = nm->mkFunctionType(types, nm->booleanType());
1365
2264
  Node op = nm->mkSkolem("qfmc", typ, "op for full-model checking");
1366
1132
  d_quant_cond[q] = op;
1367
}
1368
1369
11036
bool FullModelChecker::isHandled(Node q) const
1370
{
1371
11036
  return d_unhandledQuant.find(q) == d_unhandledQuant.end();
1372
79220
}