GCC Code Coverage Report
Directory: . Exec Total Coverage
File: src/theory/quantifiers/fmf/model_engine.cpp Lines: 124 177 70.1 %
Date: 2021-03-23 Branches: 218 660 33.0 %

Line Exec Source
1
/*********************                                                        */
2
/*! \file model_engine.cpp
3
 ** \verbatim
4
 ** Top contributors (to current version):
5
 **   Andrew Reynolds, Morgan Deters, Kshitij Bansal
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 model engine class
13
 **/
14
15
#include "theory/quantifiers/fmf/model_engine.h"
16
17
#include "options/quantifiers_options.h"
18
#include "theory/quantifiers/first_order_model.h"
19
#include "theory/quantifiers/fmf/full_model_check.h"
20
#include "theory/quantifiers/instantiate.h"
21
#include "theory/quantifiers/quant_rep_bound_ext.h"
22
#include "theory/quantifiers/quantifiers_attributes.h"
23
#include "theory/quantifiers/term_database.h"
24
#include "theory/quantifiers_engine.h"
25
26
using namespace std;
27
using namespace CVC4;
28
using namespace CVC4::kind;
29
using namespace CVC4::context;
30
using namespace CVC4::theory;
31
using namespace CVC4::theory::quantifiers;
32
using namespace CVC4::theory::inst;
33
34
//Model Engine constructor
35
824
ModelEngine::ModelEngine(QuantifiersEngine* qe,
36
                         QuantifiersState& qs,
37
                         QuantifiersInferenceManager& qim,
38
824
                         QuantifiersRegistry& qr)
39
    : QuantifiersModule(qs, qim, qr, qe),
40
      d_incomplete_check(true),
41
      d_addedLemmas(0),
42
      d_triedLemmas(0),
43
824
      d_totalLemmas(0)
44
{
45
46
824
}
47
48
1648
ModelEngine::~ModelEngine() {
49
50
1648
}
51
52
32822
bool ModelEngine::needsCheck( Theory::Effort e ) {
53
32822
  return e==Theory::EFFORT_LAST_CALL;
54
}
55
56
1526
QuantifiersModule::QEffort ModelEngine::needsModel(Theory::Effort e)
57
{
58
7542
  if( options::mbqiInterleave() ){
59
    return QEFFORT_STANDARD;
60
  }else{
61
1526
    return QEFFORT_MODEL;
62
  }
63
}
64
65
10158
void ModelEngine::reset_round( Theory::Effort e ) {
66
10158
  d_incomplete_check = true;
67
10158
}
68
4490
void ModelEngine::check(Theory::Effort e, QEffort quant_e)
69
{
70
4490
  bool doCheck = false;
71
4490
  if( options::mbqiInterleave() ){
72
    doCheck = quant_e == QEFFORT_STANDARD && d_qim.hasPendingLemma();
73
  }
74
4490
  if( !doCheck ){
75
4490
    doCheck = quant_e == QEFFORT_MODEL;
76
  }
77
4490
  if( doCheck ){
78
1421
    Assert(!d_qstate.isInConflict());
79
1421
    int addedLemmas = 0;
80
81
    //the following will test that the model satisfies all asserted universal quantifiers by
82
    // (model-based) exhaustive instantiation.
83
1421
    double clSet = 0;
84
1421
    if( Trace.isOn("model-engine") ){
85
      Trace("model-engine") << "---Model Engine Round---" << std::endl;
86
      clSet = double(clock())/double(CLOCKS_PER_SEC);
87
    }
88
1421
    Trace("model-engine-debug") << "Check model..." << std::endl;
89
1421
    d_incomplete_check = false;
90
    // print debug
91
1421
    if (Trace.isOn("fmf-model-complete"))
92
    {
93
      Trace("fmf-model-complete") << std::endl;
94
      debugPrint("fmf-model-complete");
95
    }
96
    // successfully built an acceptable model, now check it
97
1421
    addedLemmas += checkModel();
98
99
1421
    if( Trace.isOn("model-engine") ){
100
      double clSet2 = double(clock())/double(CLOCKS_PER_SEC);
101
      Trace("model-engine") << "Finished model engine, time = " << (clSet2-clSet) << std::endl;
102
    }
103
104
1421
    if( addedLemmas==0 ){
105
346
      Trace("model-engine-debug") << "No lemmas added, incomplete = " << ( d_incomplete_check || !d_incomplete_quants.empty() ) << std::endl;
106
      //CVC4 will answer SAT or unknown
107
346
      if( Trace.isOn("fmf-consistent") ){
108
        Trace("fmf-consistent") << std::endl;
109
        debugPrint("fmf-consistent");
110
      }
111
    }
112
  }
113
4490
}
114
115
335
bool ModelEngine::checkComplete() {
116
335
  return !d_incomplete_check;
117
}
118
119
1111
bool ModelEngine::checkCompleteFor( Node q ) {
120
1111
  return std::find( d_incomplete_quants.begin(), d_incomplete_quants.end(), q )==d_incomplete_quants.end();
121
}
122
123
2669
void ModelEngine::registerQuantifier( Node f ){
124
2669
  if( Trace.isOn("fmf-warn") ){
125
    bool canHandle = true;
126
    for( unsigned i=0; i<f[0].getNumChildren(); i++ ){
127
      TypeNode tn = f[0][i].getType();
128
      if( !tn.isSort() ){
129
        if (!tn.isInterpretedFinite())
130
        {
131
          if( tn.isInteger() ){
132
            if( !options::fmfBound() ){
133
              canHandle = false;
134
            }
135
          }else{
136
            canHandle = false;
137
          }
138
        }
139
      }
140
    }
141
    if( !canHandle ){
142
      Trace("fmf-warn") << "Warning : Model Engine : may not be able to answer SAT because of formula : " << f << std::endl;
143
    }
144
  }
145
2669
}
146
147
13773
void ModelEngine::assertNode( Node f ){
148
149
13773
}
150
151
1421
int ModelEngine::checkModel(){
152
1421
  FirstOrderModel* fm = d_quantEngine->getModel();
153
154
  //for debugging, setup
155
7684
  for (std::map<TypeNode, std::vector<Node> >::iterator it =
156
1421
           fm->getRepSetPtr()->d_type_reps.begin();
157
9105
       it != fm->getRepSetPtr()->d_type_reps.end();
158
       ++it)
159
  {
160
7684
    if( it->first.isSort() ){
161
2425
      Trace("model-engine") << "Cardinality( " << it->first << " )" << " = " << it->second.size() << std::endl;
162
2425
      Trace("model-engine-debug") << "        Reps : ";
163
6792
      for( size_t i=0; i<it->second.size(); i++ ){
164
4367
        Trace("model-engine-debug") << it->second[i] << "  ";
165
      }
166
2425
      Trace("model-engine-debug") << std::endl;
167
2425
      Trace("model-engine-debug") << "   Term reps : ";
168
6792
      for( size_t i=0; i<it->second.size(); i++ ){
169
8734
        Node r = fm->getInternalRepresentative(it->second[i], Node::null(), 0);
170
4367
        if (r.isNull())
171
        {
172
          // there was an invalid equivalence class
173
          d_incomplete_check = true;
174
        }
175
4367
        Trace("model-engine-debug") << r << " ";
176
      }
177
2425
      Trace("model-engine-debug") << std::endl;
178
4850
      Node mbt = fm->getModelBasisTerm(it->first);
179
2425
      Trace("model-engine-debug") << "  Basis term : " << mbt << std::endl;
180
    }
181
  }
182
183
1421
  d_triedLemmas = 0;
184
1421
  d_addedLemmas = 0;
185
1421
  d_totalLemmas = 0;
186
  //for statistics
187
1421
  if( Trace.isOn("model-engine") ){
188
    for( unsigned i=0; i<fm->getNumAssertedQuantifiers(); i++ ){
189
      Node f = fm->getAssertedQuantifier( i );
190
      if (fm->isQuantifierActive(f) && d_qreg.hasOwnership(f, this))
191
      {
192
        int totalInst = 1;
193
        for( unsigned j=0; j<f[0].getNumChildren(); j++ ){
194
          TypeNode tn = f[0][j].getType();
195
          if (fm->getRepSet()->hasType(tn))
196
          {
197
            totalInst =
198
                totalInst * (int)fm->getRepSet()->getNumRepresentatives(tn);
199
          }
200
        }
201
        d_totalLemmas += totalInst;
202
      }
203
    }
204
  }
205
206
1421
  Trace("model-engine-debug") << "Do exhaustive instantiation..." << std::endl;
207
  // FMC uses two sub-effort levels
208
1421
  int e_max = options::mbqiMode() == options::MbqiMode::FMC
209
2228
                  ? 2
210
2228
                  : (options::mbqiMode() == options::MbqiMode::TRUST ? 0 : 1);
211
2096
  for( int e=0; e<e_max; e++) {
212
1750
    d_incomplete_quants.clear();
213
13140
    for( unsigned i=0; i<fm->getNumAssertedQuantifiers(); i++ ){
214
22780
      Node q = fm->getAssertedQuantifier( i, true );
215
11390
      Trace("fmf-exh-inst") << "-> Exhaustive instantiate " << q << ", effort = " << e << "..." << std::endl;
216
      //determine if we should check this quantifier
217
11390
      if (fm->isQuantifierActive(q) && d_qreg.hasOwnership(q, this))
218
      {
219
11208
        exhaustiveInstantiate( q, e );
220
11208
        if (d_qstate.isInConflict())
221
        {
222
          break;
223
        }
224
      }else{
225
182
        Trace("fmf-exh-inst") << "-> Inactive : " << q << std::endl;
226
      }
227
    }
228
1750
    if( d_addedLemmas>0 ){
229
1075
      break;
230
    }else{
231
675
      Assert(!d_qstate.isInConflict());
232
    }
233
  }
234
235
  //print debug information
236
1421
  if (d_qstate.isInConflict())
237
  {
238
    Trace("model-engine") << "Conflict, added lemmas = ";
239
  }else{
240
1421
    Trace("model-engine") << "Added Lemmas = ";
241
  }
242
1421
  Trace("model-engine") << d_addedLemmas << " / " << d_triedLemmas << " / ";
243
1421
  Trace("model-engine") << d_totalLemmas << std::endl;
244
1421
  return d_addedLemmas;
245
}
246
247
248
249
11208
void ModelEngine::exhaustiveInstantiate( Node f, int effort ){
250
  //first check if the builder can do the exhaustive instantiation
251
11208
  quantifiers::QModelBuilder * mb = d_quantEngine->getModelBuilder();
252
11208
  unsigned prev_alem = mb->getNumAddedLemmas();
253
11208
  unsigned prev_tlem = mb->getNumTriedLemmas();
254
11208
  FirstOrderModel* fm = d_quantEngine->getModel();
255
11208
  int retEi = mb->doExhaustiveInstantiation(fm, f, effort);
256
11208
  if( retEi!=0 ){
257
11016
    if( retEi<0 ){
258
      Trace("fmf-exh-inst") << "-> Builder determined complete instantiation was impossible." << std::endl;
259
      d_incomplete_quants.push_back( f );
260
    }else{
261
11016
      Trace("fmf-exh-inst") << "-> Builder determined instantiation(s)." << std::endl;
262
    }
263
11016
    d_triedLemmas += mb->getNumTriedLemmas()-prev_tlem;
264
11016
    d_addedLemmas += mb->getNumAddedLemmas()-prev_alem;
265
  }else{
266
192
    if( Trace.isOn("fmf-exh-inst-debug") ){
267
      Trace("fmf-exh-inst-debug") << "   Instantiation Constants: ";
268
      for( size_t i=0; i<f[0].getNumChildren(); i++ ){
269
        Trace("fmf-exh-inst-debug")
270
            << d_qreg.getInstantiationConstant(f, i) << " ";
271
      }
272
      Trace("fmf-exh-inst-debug") << std::endl;
273
    }
274
192
    QuantifiersBoundInference& qbi = d_qreg.getQuantifiersBoundInference();
275
    //create a rep set iterator and iterate over the (relevant) domain of the quantifier
276
384
    QRepBoundExt qrbe(qbi, fm);
277
384
    RepSetIterator riter(fm->getRepSet(), &qrbe);
278
192
    if( riter.setQuantifier( f ) ){
279
192
      Trace("fmf-exh-inst") << "...exhaustive instantiation set, incomplete=" << riter.isIncomplete() << "..." << std::endl;
280
192
      if( !riter.isIncomplete() ){
281
176
        int triedLemmas = 0;
282
176
        int addedLemmas = 0;
283
176
        Instantiate* inst = d_quantEngine->getInstantiate();
284
1370
        while( !riter.isFinished() && ( addedLemmas==0 || !options::fmfOneInstPerRound() ) ){
285
          //instantiation was not shown to be true, construct the match
286
1194
          InstMatch m( f );
287
1779
          for (unsigned i = 0; i < riter.getNumTerms(); i++)
288
          {
289
1182
            m.set(d_qstate, i, riter.getCurrentTerm(i));
290
          }
291
597
          Debug("fmf-model-eval") << "* Add instantiation " << m << std::endl;
292
597
          triedLemmas++;
293
          //add as instantiation
294
597
          if (inst->addInstantiation(
295
                  f, m.d_vals, InferenceId::QUANTIFIERS_INST_FMF_EXH, true))
296
          {
297
262
            addedLemmas++;
298
262
            if (d_qstate.isInConflict())
299
            {
300
              break;
301
            }
302
          }else{
303
335
            Debug("fmf-model-eval") << "* Failed Add instantiation " << m << std::endl;
304
          }
305
597
          riter.increment();
306
        }
307
176
        d_addedLemmas += addedLemmas;
308
176
        d_triedLemmas += triedLemmas;
309
      }
310
    }else{
311
      Trace("fmf-exh-inst") << "...exhaustive instantiation did set, incomplete=" << riter.isIncomplete() << "..." << std::endl;
312
    }
313
    //if the iterator is incomplete, we will return unknown instead of sat if no instantiations are added this round
314
192
    if( riter.isIncomplete() ){
315
22
      d_incomplete_quants.push_back( f );
316
    }
317
  }
318
11208
}
319
320
void ModelEngine::debugPrint( const char* c ){
321
  Trace( c ) << "Quantifiers: " << std::endl;
322
  for( unsigned i=0; i<d_quantEngine->getModel()->getNumAssertedQuantifiers(); i++ ){
323
    Node q = d_quantEngine->getModel()->getAssertedQuantifier( i );
324
    if (d_qreg.hasOwnership(q, this))
325
    {
326
      Trace( c ) << "   ";
327
      if( !d_quantEngine->getModel()->isQuantifierActive( q ) ){
328
        Trace( c ) << "*Inactive* ";
329
      }else{
330
        Trace( c ) << "           ";
331
      }
332
      Trace( c ) << q << std::endl;
333
    }
334
  }
335
  //d_quantEngine->getModel()->debugPrint( c );
336
32701
}
337