GCC Code Coverage Report
Directory: . Exec Total Coverage
File: src/theory/model_manager.cpp Lines: 103 108 95.4 %
Date: 2021-03-22 Branches: 131 272 48.2 %

Line Exec Source
1
/*********************                                                        */
2
/*! \file model_manager.cpp
3
 ** \verbatim
4
 ** Top contributors (to current version):
5
 **   Andrew Reynolds
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 Abstract management of models for TheoryEngine.
13
 **/
14
15
#include "theory/model_manager.h"
16
17
#include "options/smt_options.h"
18
#include "options/theory_options.h"
19
#include "prop/prop_engine.h"
20
#include "theory/quantifiers_engine.h"
21
#include "theory/quantifiers/first_order_model.h"
22
#include "theory/quantifiers/fmf/model_builder.h"
23
#include "theory/theory_engine.h"
24
25
namespace CVC4 {
26
namespace theory {
27
28
8995
ModelManager::ModelManager(TheoryEngine& te, EqEngineManager& eem)
29
    : d_te(te),
30
8995
      d_logicInfo(te.getLogicInfo()),
31
      d_eem(eem),
32
      d_modelEqualityEngine(nullptr),
33
      d_modelEqualityEngineAlloc(nullptr),
34
      d_model(nullptr),
35
      d_modelBuilder(nullptr),
36
      d_modelBuilt(false),
37
17990
      d_modelBuiltSuccess(false)
38
{
39
8995
}
40
41
8992
ModelManager::~ModelManager() {}
42
43
8995
void ModelManager::finishInit(eq::EqualityEngineNotify* notify)
44
{
45
  // construct the model
46
8995
  const LogicInfo& logicInfo = d_te.getLogicInfo();
47
  // Initialize the model and model builder.
48
8995
  if (logicInfo.isQuantified())
49
  {
50
6052
    QuantifiersEngine* qe = d_te.getQuantifiersEngine();
51
6052
    Assert(qe != nullptr);
52
6052
    d_modelBuilder = qe->getModelBuilder();
53
6052
    d_model = qe->getModel();
54
  }
55
  else
56
  {
57
2943
    context::Context* u = d_te.getUserContext();
58
5886
    d_alocModel.reset(
59
2943
        new TheoryModel(u, "DefaultModel", options::assignFunctionValues()));
60
2943
    d_model = d_alocModel.get();
61
  }
62
63
  // make the default builder, e.g. in the case that the quantifiers engine does
64
  // not have a model builder
65
8995
  if (d_modelBuilder == nullptr)
66
  {
67
8173
    d_alocModelBuilder.reset(new TheoryEngineModelBuilder);
68
8173
    d_modelBuilder = d_alocModelBuilder.get();
69
  }
70
  // notice that the equality engine of the model has yet to be assigned.
71
8995
  initializeModelEqEngine(notify);
72
8995
}
73
74
22352
void ModelManager::resetModel()
75
{
76
22352
  d_modelBuilt = false;
77
22352
  d_modelBuiltSuccess = false;
78
  // Reset basic information on the model object
79
22352
  d_model->reset();
80
22352
}
81
82
33022
bool ModelManager::buildModel()
83
{
84
33022
  if (d_modelBuilt)
85
  {
86
    // already computed
87
14077
    return d_modelBuiltSuccess;
88
  }
89
  // reset the flags now
90
18945
  d_modelBuilt = true;
91
18945
  d_modelBuiltSuccess = false;
92
93
  // prepare the model, which is specific to the manager
94
18945
  if (!prepareModel())
95
  {
96
2
    Trace("model-builder") << "ModelManager: fail prepare model" << std::endl;
97
2
    return false;
98
  }
99
100
  // now, finish building the model
101
18942
  d_modelBuiltSuccess = finishBuildModel();
102
103
18942
  if (Trace.isOn("model-builder"))
104
  {
105
    Trace("model-builder") << "Final model:" << std::endl;
106
    Trace("model-builder") << d_model->debugPrintModelEqc() << std::endl;
107
  }
108
109
37884
  Trace("model-builder") << "ModelManager: model built success is "
110
18942
                         << d_modelBuiltSuccess << std::endl;
111
112
18942
  return d_modelBuiltSuccess;
113
}
114
115
bool ModelManager::isModelBuilt() const { return d_modelBuilt; }
116
117
5953
void ModelManager::postProcessModel(bool incomplete)
118
{
119
5953
  if (!d_modelBuilt)
120
  {
121
    // model not built, nothing to do
122
4691
    return;
123
  }
124
1262
  Trace("model-builder") << "ModelManager: post-process model..." << std::endl;
125
  // model construction should always succeed unless lemmas were added
126
1262
  AlwaysAssert(d_modelBuiltSuccess);
127
1262
  if (!options::produceModels())
128
  {
129
314
    return;
130
  }
131
  // Do post-processing of model from the theories (used for THEORY_SEP
132
  // to construct heap model)
133
13272
  for (TheoryId theoryId = theory::THEORY_FIRST; theoryId < theory::THEORY_LAST;
134
       ++theoryId)
135
  {
136
12324
    Theory* t = d_te.theoryOf(theoryId);
137
12324
    if (t == nullptr)
138
    {
139
      // theory not active, skip
140
      continue;
141
    }
142
24648
    Trace("model-builder-debug")
143
12324
        << "  PostProcessModel on theory: " << theoryId << std::endl;
144
12324
    t->postProcessModel(d_model);
145
  }
146
  // also call the model builder's post-process model
147
948
  d_modelBuilder->postProcessModel(incomplete, d_model);
148
}
149
150
286608
theory::TheoryModel* ModelManager::getModel() { return d_model; }
151
152
18942
bool ModelManager::collectModelBooleanVariables()
153
{
154
18942
  Trace("model-builder") << "  CollectModelInfo boolean variables" << std::endl;
155
  // Get value of the Boolean variables
156
18942
  prop::PropEngine* propEngine = d_te.getPropEngine();
157
37884
  std::vector<TNode> boolVars;
158
18942
  propEngine->getBooleanVariables(boolVars);
159
18942
  std::vector<TNode>::iterator it, iend = boolVars.end();
160
  bool hasValue, value;
161
86952
  for (it = boolVars.begin(); it != iend; ++it)
162
  {
163
136020
    TNode var = *it;
164
68010
    hasValue = propEngine->hasValue(var, value);
165
    // Should we assert that hasValue is true?
166
68010
    if (!hasValue)
167
    {
168
20560
      Trace("model-builder-assertions")
169
10280
          << "    has no value : " << var << std::endl;
170
10280
      value = false;
171
    }
172
136020
    Trace("model-builder-assertions")
173
136020
        << "(assert" << (value ? " " : " (not ") << var
174
68010
        << (value ? ");" : "));") << std::endl;
175
68010
    if (!d_model->assertPredicate(var, value))
176
    {
177
      return false;
178
    }
179
  }
180
18942
  return true;
181
}
182
183
135390
void ModelManager::collectAssertedTerms(TheoryId tid,
184
                                        std::set<Node>& termSet,
185
                                        bool includeShared) const
186
{
187
135390
  Theory* t = d_te.theoryOf(tid);
188
  // Collect all terms appearing in assertions
189
135390
  context::CDList<Assertion>::const_iterator assert_it = t->facts_begin(),
190
135390
                                             assert_it_end = t->facts_end();
191
6318242
  for (; assert_it != assert_it_end; ++assert_it)
192
  {
193
3091426
    collectTerms(tid, *assert_it, termSet);
194
  }
195
196
135390
  if (includeShared)
197
  {
198
    // Add terms that are shared terms
199
135390
    context::CDList<TNode>::const_iterator shared_it = t->shared_terms_begin(),
200
                                           shared_it_end =
201
135390
                                               t->shared_terms_end();
202
2100706
    for (; shared_it != shared_it_end; ++shared_it)
203
    {
204
982658
      collectTerms(tid, *shared_it, termSet);
205
    }
206
  }
207
135390
}
208
209
4074084
void ModelManager::collectTerms(TheoryId tid,
210
                                TNode n,
211
                                std::set<Node>& termSet) const
212
{
213
4074084
  const std::set<Kind>& irrKinds = d_model->getIrrelevantKinds();
214
8148168
  std::vector<TNode> visit;
215
8148168
  TNode cur;
216
4074084
  visit.push_back(n);
217
10130934
  do
218
  {
219
14205018
    cur = visit.back();
220
14205018
    visit.pop_back();
221
14205018
    if (termSet.find(cur) != termSet.end())
222
    {
223
      // already visited
224
7138682
      continue;
225
    }
226
7066336
    Kind k = cur.getKind();
227
    // only add to term set if a relevant kind
228
7066336
    if (irrKinds.find(k) == irrKinds.end())
229
    {
230
3144830
      termSet.insert(cur);
231
    }
232
    // traverse owned terms, don't go under quantifiers
233
19502029
    if ((k == kind::NOT || k == kind::EQUAL || Theory::theoryOf(cur) == tid)
234
20659548
        && !cur.isClosure())
235
    {
236
6492860
      visit.insert(visit.end(), cur.begin(), cur.end());
237
    }
238
14205018
  } while (!visit.empty());
239
4074084
}
240
241
}  // namespace theory
242
26676
}  // namespace CVC4