1 /********************* */
2 /*! \file model_manager.cpp
4 ** Top contributors (to current version):
6 ** This file is part of the CVC4 project.
7 ** Copyright (c) 2009-2020 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
12 ** \brief Abstract management of models for TheoryEngine.
15 #include "theory/model_manager.h"
17 #include "options/theory_options.h"
18 #include "theory/quantifiers_engine.h"
19 #include "theory/theory_engine.h"
24 ModelManager::ModelManager(TheoryEngine
& te
, EqEngineManager
& eem
)
26 d_logicInfo(te
.getLogicInfo()),
28 d_modelEqualityEngine(nullptr),
29 d_modelEqualityEngineAlloc(nullptr),
31 d_modelBuilder(nullptr),
33 d_modelBuiltSuccess(false)
37 ModelManager::~ModelManager() {}
39 void ModelManager::finishInit(eq::EqualityEngineNotify
* notify
)
41 // construct the model
42 const LogicInfo
& logicInfo
= d_te
.getLogicInfo();
43 // Initialize the model and model builder.
44 if (logicInfo
.isQuantified())
46 QuantifiersEngine
* qe
= d_te
.getQuantifiersEngine();
47 Assert(qe
!= nullptr);
48 d_modelBuilder
= qe
->getModelBuilder();
49 d_model
= qe
->getModel();
53 context::Context
* u
= d_te
.getUserContext();
55 new TheoryModel(u
, "DefaultModel", options::assignFunctionValues()));
56 d_model
= d_alocModel
.get();
59 // make the default builder, e.g. in the case that the quantifiers engine does
60 // not have a model builder
61 if (d_modelBuilder
== nullptr)
63 d_alocModelBuilder
.reset(new TheoryEngineModelBuilder(&d_te
));
64 d_modelBuilder
= d_alocModelBuilder
.get();
66 // notice that the equality engine of the model has yet to be assigned.
67 initializeModelEqEngine(notify
);
70 void ModelManager::resetModel()
73 d_modelBuiltSuccess
= false;
74 // Reset basic information on the model object
78 bool ModelManager::buildModel()
83 return d_modelBuiltSuccess
;
85 // reset the flags now
87 d_modelBuiltSuccess
= false;
89 // prepare the model, which is specific to the manager
92 Trace("model-builder") << "ModelManager: fail prepare model" << std::endl
;
96 // now, finish building the model
97 d_modelBuiltSuccess
= finishBuildModel();
98 return d_modelBuiltSuccess
;
101 bool ModelManager::isModelBuilt() const { return d_modelBuilt
; }
103 void ModelManager::postProcessModel(bool incomplete
)
107 // model not built, nothing to do
110 Trace("model-builder") << "ModelManager: post-process model..." << std::endl
;
111 // model construction should always succeed unless lemmas were added
112 AlwaysAssert(d_modelBuiltSuccess
);
113 if (!options::produceModels())
117 // Do post-processing of model from the theories (used for THEORY_SEP
118 // to construct heap model)
119 for (TheoryId theoryId
= theory::THEORY_FIRST
; theoryId
< theory::THEORY_LAST
;
122 Theory
* t
= d_te
.theoryOf(theoryId
);
125 // theory not active, skip
128 Trace("model-builder-debug")
129 << " PostProcessModel on theory: " << theoryId
<< std::endl
;
130 t
->postProcessModel(d_model
);
132 // also call the model builder's post-process model
133 d_modelBuilder
->postProcessModel(incomplete
, d_model
);
136 theory::TheoryModel
* ModelManager::getModel() { return d_model
; }
138 bool ModelManager::collectModelBooleanVariables()
140 Trace("model-builder") << " CollectModelInfo boolean variables" << std::endl
;
141 // Get value of the Boolean variables
142 prop::PropEngine
* propEngine
= d_te
.getPropEngine();
143 std::vector
<TNode
> boolVars
;
144 propEngine
->getBooleanVariables(boolVars
);
145 std::vector
<TNode
>::iterator it
, iend
= boolVars
.end();
146 bool hasValue
, value
;
147 for (it
= boolVars
.begin(); it
!= iend
; ++it
)
150 hasValue
= propEngine
->hasValue(var
, value
);
151 // Should we assert that hasValue is true?
154 Trace("model-builder-assertions")
155 << " has no value : " << var
<< std::endl
;
158 Trace("model-builder-assertions")
159 << "(assert" << (value
? " " : " (not ") << var
160 << (value
? ");" : "));") << std::endl
;
161 if (!d_model
->assertPredicate(var
, value
))
169 void ModelManager::collectAssertedTerms(TheoryId tid
,
170 std::set
<Node
>& termSet
,
171 bool includeShared
) const
173 Theory
* t
= d_te
.theoryOf(tid
);
174 // Collect all terms appearing in assertions
175 context::CDList
<Assertion
>::const_iterator assert_it
= t
->facts_begin(),
176 assert_it_end
= t
->facts_end();
177 for (; assert_it
!= assert_it_end
; ++assert_it
)
179 collectTerms(tid
, *assert_it
, termSet
);
184 // Add terms that are shared terms
185 context::CDList
<TNode
>::const_iterator shared_it
= t
->shared_terms_begin(),
187 t
->shared_terms_end();
188 for (; shared_it
!= shared_it_end
; ++shared_it
)
190 collectTerms(tid
, *shared_it
, termSet
);
195 void ModelManager::collectTerms(TheoryId tid
,
197 std::set
<Node
>& termSet
) const
199 const std::set
<Kind
>& irrKinds
= d_model
->getIrrelevantKinds();
200 std::vector
<TNode
> visit
;
207 if (termSet
.find(cur
) != termSet
.end())
212 Kind k
= cur
.getKind();
213 // only add to term set if a relevant kind
214 if (irrKinds
.find(k
) == irrKinds
.end())
218 // traverse owned terms, don't go under quantifiers
219 if ((k
== kind::NOT
|| k
== kind::EQUAL
|| Theory::theoryOf(cur
) == tid
)
222 visit
.insert(visit
.end(), cur
.begin(), cur
.end());
224 } while (!visit
.empty());
227 } // namespace theory