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