1 /********************* */
2 /*! \file model_manager_distributed.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 Management of a distributed approach for model generation.
15 #include "theory/model_manager_distributed.h"
17 #include "theory/theory_engine.h"
18 #include "theory/theory_model.h"
23 ModelManagerDistributed::ModelManagerDistributed(TheoryEngine
& te
,
25 : ModelManager(te
, eem
)
29 ModelManagerDistributed::~ModelManagerDistributed()
31 // pop the model context which we pushed on initialization
32 d_modelEeContext
.pop();
35 void ModelManagerDistributed::initializeModelEqEngine(
36 eq::EqualityEngineNotify
* notify
)
38 // initialize the model equality engine, use the provided notification object,
39 // which belongs e.g. to CombinationModelBased
41 esim
.d_notify
= notify
;
42 esim
.d_name
= d_model
->getName() + "::ee";
43 esim
.d_constantsAreTriggers
= false;
44 d_modelEqualityEngineAlloc
.reset(
45 d_eem
.allocateEqualityEngine(esim
, &d_modelEeContext
));
46 d_modelEqualityEngine
= d_modelEqualityEngineAlloc
.get();
47 // finish initializing the model
48 d_model
->finishInit(d_modelEqualityEngine
);
49 // We push a context during initialization since the model is cleared during
50 // collectModelInfo using pop/push.
51 d_modelEeContext
.push();
54 bool ModelManagerDistributed::prepareModel()
56 Trace("model-builder") << "ModelManagerDistributed: reset model..."
59 // push/pop to clear the equality engine of the model
60 d_modelEeContext
.pop();
61 d_modelEeContext
.push();
63 // Collect model info from the theories
64 Trace("model-builder") << "ModelManagerDistributed: Collect model info..."
66 // Consult each active theory to get all relevant information concerning the
67 // model, which includes both dump their equality information and assigning
68 // values. Notice the order of theories here is important and is the same
69 // as the list in CVC4_FOR_EACH_THEORY in theory_engine.cpp.
70 for (TheoryId theoryId
= theory::THEORY_FIRST
; theoryId
< theory::THEORY_LAST
;
73 if (!d_logicInfo
.isTheoryEnabled(theoryId
))
75 // theory not active, skip
78 Theory
* t
= d_te
.theoryOf(theoryId
);
79 Trace("model-builder") << " CollectModelInfo on theory: " << theoryId
81 // collect the asserted terms
82 std::set
<Node
> termSet
;
83 collectAssertedTerms(theoryId
, termSet
);
84 // also get relevant terms
85 t
->computeRelevantTerms(termSet
);
86 if (!t
->collectModelInfo(d_model
, termSet
))
88 Trace("model-builder")
89 << "ModelManagerDistributed: fail collect model info" << std::endl
;
94 if (!collectModelBooleanVariables())
96 Trace("model-builder") << "ModelManagerDistributed: fail Boolean variables"
104 bool ModelManagerDistributed::finishBuildModel() const
106 // do not use relevant terms
107 if (!d_modelBuilder
->buildModel(d_model
))
109 Trace("model-builder") << "ModelManager: fail build model" << std::endl
;
115 } // namespace theory