GCC Code Coverage Report
Directory: . Exec Total Coverage
File: src/theory/quantifiers/ematching/instantiation_engine.cpp Lines: 114 132 86.4 %
Date: 2021-03-22 Branches: 178 414 43.0 %

Line Exec Source
1
/*********************                                                        */
2
/*! \file instantiation_engine.cpp
3
 ** \verbatim
4
 ** Top contributors (to current version):
5
 **   Andrew Reynolds, Morgan Deters, Tim King
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 instantiation engine class
13
 **/
14
15
#include "theory/quantifiers/ematching/instantiation_engine.h"
16
17
#include "options/quantifiers_options.h"
18
#include "theory/quantifiers/ematching/inst_strategy_e_matching.h"
19
#include "theory/quantifiers/ematching/inst_strategy_e_matching_user.h"
20
#include "theory/quantifiers/ematching/trigger.h"
21
#include "theory/quantifiers/first_order_model.h"
22
#include "theory/quantifiers/quantifiers_attributes.h"
23
#include "theory/quantifiers/term_database.h"
24
#include "theory/quantifiers/term_util.h"
25
#include "theory/quantifiers_engine.h"
26
27
using namespace std;
28
using namespace CVC4::kind;
29
using namespace CVC4::context;
30
using namespace CVC4::theory::inst;
31
32
namespace CVC4 {
33
namespace theory {
34
namespace quantifiers {
35
36
5826
InstantiationEngine::InstantiationEngine(QuantifiersEngine* qe,
37
                                         QuantifiersState& qs,
38
                                         QuantifiersInferenceManager& qim,
39
5826
                                         QuantifiersRegistry& qr)
40
    : QuantifiersModule(qs, qim, qr, qe),
41
      d_instStrategies(),
42
      d_isup(),
43
      d_i_ag(),
44
      d_quants(),
45
5826
      d_quant_rel(nullptr)
46
{
47
5826
  if (options::relevantTriggers())
48
  {
49
4
    d_quant_rel.reset(new quantifiers::QuantRelevance);
50
  }
51
5826
  if (options::eMatching()) {
52
    // these are the instantiation strategies for E-matching
53
    // user-provided patterns
54
5823
    if (options::userPatternsQuant() != options::UserPatMode::IGNORE)
55
    {
56
5823
      d_isup.reset(new InstStrategyUserPatterns(d_quantEngine, qs, qim, qr));
57
5823
      d_instStrategies.push_back(d_isup.get());
58
    }
59
60
    // auto-generated patterns
61
11646
    d_i_ag.reset(new InstStrategyAutoGenTriggers(
62
5823
        d_quantEngine, qs, qim, qr, d_quant_rel.get()));
63
5823
    d_instStrategies.push_back(d_i_ag.get());
64
  }
65
5826
}
66
67
11646
InstantiationEngine::~InstantiationEngine() {}
68
69
6162
void InstantiationEngine::presolve() {
70
18480
  for( unsigned i=0; i<d_instStrategies.size(); ++i ){
71
12318
    d_instStrategies[i]->presolve();
72
  }
73
6162
}
74
75
2578
void InstantiationEngine::doInstantiationRound( Theory::Effort effort ){
76
2578
  size_t lastWaiting = d_qim.numPendingLemmas();
77
  //iterate over an internal effort level e
78
2578
  int e = 0;
79
2578
  int eLimit = effort==Theory::EFFORT_LAST_CALL ? 10 : 2;
80
2578
  bool finished = false;
81
  //while unfinished, try effort level=0,1,2....
82
12890
  while( !finished && e<=eLimit ){
83
5156
    Debug("inst-engine") << "IE: Prepare instantiation (" << e << ")." << std::endl;
84
5156
    finished = true;
85
    //instantiate each quantifier
86
85788
    for( unsigned i=0; i<d_quants.size(); i++ ){
87
161264
      Node q = d_quants[i];
88
80632
      Debug("inst-engine-debug") << "IE: Instantiate " << q << "..." << std::endl;
89
      //int e_use = d_quantEngine->getRelevance( q )==-1 ? e - 1 : e;
90
80632
      int e_use = e;
91
80632
      if( e_use>=0 ){
92
80632
        Trace("inst-engine-debug") << "inst-engine : " << q << std::endl;
93
        //check each instantiation strategy
94
241896
        for( unsigned j=0; j<d_instStrategies.size(); j++ ){
95
161264
          InstStrategy* is = d_instStrategies[j];
96
161264
          Trace("inst-engine-debug") << "Do " << is->identify() << " " << e_use << std::endl;
97
161264
          InstStrategyStatus quantStatus = is->process(q, effort, e_use);
98
322528
          Trace("inst-engine-debug")
99
161264
              << " -> unfinished= "
100
322528
              << (quantStatus == InstStrategyStatus::STATUS_UNFINISHED)
101
161264
              << ", conflict=" << d_qstate.isInConflict() << std::endl;
102
161264
          if (d_qstate.isInConflict())
103
          {
104
            return;
105
          }
106
161264
          else if (quantStatus == InstStrategyStatus::STATUS_UNFINISHED)
107
          {
108
67921
            finished = false;
109
          }
110
        }
111
      }
112
    }
113
    //do not consider another level if already added lemma at this level
114
5156
    if (d_qim.numPendingLemmas() > lastWaiting)
115
    {
116
1015
      finished = true;
117
    }
118
5156
    e++;
119
  }
120
}
121
122
46962
bool InstantiationEngine::needsCheck( Theory::Effort e ){
123
46962
  return d_qstate.getInstWhenNeedsCheck(e);
124
}
125
126
24171
void InstantiationEngine::reset_round( Theory::Effort e ){
127
  //if not, proceed to instantiation round
128
  //reset the instantiation strategies
129
72501
  for( unsigned i=0; i<d_instStrategies.size(); ++i ){
130
48330
    InstStrategy* is = d_instStrategies[i];
131
48330
    is->processResetInstantiationRound( e );
132
  }
133
24171
}
134
135
46610
void InstantiationEngine::check(Theory::Effort e, QEffort quant_e)
136
{
137
62024
  CodeTimer codeTimer(d_quantEngine->d_statistics.d_ematching_time);
138
46610
  if (quant_e != QEFFORT_STANDARD)
139
  {
140
31196
    return;
141
  }
142
15414
  double clSet = 0;
143
15414
  if (Trace.isOn("inst-engine"))
144
  {
145
    clSet = double(clock()) / double(CLOCKS_PER_SEC);
146
    Trace("inst-engine") << "---Instantiation Engine Round, effort = " << e
147
                         << "---" << std::endl;
148
  }
149
  // collect all active quantified formulas belonging to this
150
15414
  bool quantActive = false;
151
15414
  d_quants.clear();
152
15414
  FirstOrderModel* m = d_quantEngine->getModel();
153
15414
  size_t nquant = m->getNumAssertedQuantifiers();
154
70947
  for (size_t i = 0; i < nquant; i++)
155
  {
156
111066
    Node q = d_quantEngine->getModel()->getAssertedQuantifier(i, true);
157
55533
    if (shouldProcess(q) && m->isQuantifierActive(q))
158
    {
159
40316
      quantActive = true;
160
40316
      d_quants.push_back(q);
161
    }
162
  }
163
30828
  Trace("inst-engine-debug")
164
15414
      << "InstEngine: check: # asserted quantifiers " << d_quants.size() << "/";
165
15414
  Trace("inst-engine-debug") << nquant << " " << quantActive << std::endl;
166
15414
  if (quantActive)
167
  {
168
2578
    size_t lastWaiting = d_qim.numPendingLemmas();
169
2578
    doInstantiationRound(e);
170
2578
    if (d_qstate.isInConflict())
171
    {
172
      Assert(d_qim.numPendingLemmas() > lastWaiting);
173
      Trace("inst-engine") << "Conflict, added lemmas = "
174
                           << (d_qim.numPendingLemmas() - lastWaiting)
175
                           << std::endl;
176
    }
177
2578
    else if (d_qim.hasPendingLemma())
178
    {
179
2030
      Trace("inst-engine") << "Added lemmas = "
180
2030
                           << (d_qim.numPendingLemmas() - lastWaiting)
181
1015
                           << std::endl;
182
    }
183
  }
184
  else
185
  {
186
12836
    d_quants.clear();
187
  }
188
15414
  if (Trace.isOn("inst-engine"))
189
  {
190
    double clSet2 = double(clock()) / double(CLOCKS_PER_SEC);
191
    Trace("inst-engine") << "Finished instantiation engine, time = "
192
                         << (clSet2 - clSet) << std::endl;
193
  }
194
}
195
196
410
bool InstantiationEngine::checkCompleteFor( Node q ) {
197
  //TODO?
198
410
  return false;
199
}
200
201
21295
void InstantiationEngine::checkOwnership(Node q)
202
{
203
21295
  if( options::strictTriggers() && q.getNumChildren()==3 ){
204
    //if strict triggers, take ownership of this quantified formula
205
    bool hasPat = false;
206
    for( unsigned i=0; i<q[2].getNumChildren(); i++ ){
207
      if( q[2][i].getKind()==INST_PATTERN || q[2][i].getKind()==INST_NO_PATTERN  ){
208
        hasPat = true;
209
        break;
210
      }
211
    }
212
    if( hasPat ){
213
      d_qreg.setOwner(q, this, 1);
214
    }
215
  }
216
21295
}
217
218
21295
void InstantiationEngine::registerQuantifier(Node q)
219
{
220
21295
  if (!shouldProcess(q))
221
  {
222
2365
    return;
223
  }
224
18930
  if (d_quant_rel)
225
  {
226
344
    d_quant_rel->registerQuantifier(q);
227
  }
228
  // take into account user patterns
229
18930
  if (q.getNumChildren() == 3)
230
  {
231
7516
    Node subsPat = d_qreg.substituteBoundVariablesToInstConstants(q[2], q);
232
    // add patterns
233
7658
    for (const Node& p : subsPat)
234
    {
235
3900
      if (p.getKind() == INST_PATTERN)
236
      {
237
3748
        addUserPattern(q, p);
238
      }
239
152
      else if (p.getKind() == INST_NO_PATTERN)
240
      {
241
8
        addUserNoPattern(q, p);
242
      }
243
    }
244
  }
245
}
246
247
3748
void InstantiationEngine::addUserPattern(Node q, Node pat) {
248
3748
  if (d_isup) {
249
3748
    d_isup->addUserPattern(q, pat);
250
  }
251
3748
}
252
253
8
void InstantiationEngine::addUserNoPattern(Node q, Node pat) {
254
8
  if (d_i_ag) {
255
8
    d_i_ag->addUserNoPattern(q, pat);
256
  }
257
8
}
258
259
76828
bool InstantiationEngine::shouldProcess(Node q)
260
{
261
76828
  if (!d_qreg.hasOwnership(q, this))
262
  {
263
16972
    return false;
264
  }
265
  // also ignore internal quantifiers
266
59856
  QuantAttributes& qattr = d_qreg.getQuantAttributes();
267
59856
  if (qattr.isInternal(q))
268
  {
269
598
    return false;
270
  }
271
59258
  return true;
272
}
273
274
}  // namespace quantifiers
275
}  // namespace theory
276
26676
}  // namespace CVC4