1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
|
/******************************************************************************
* Top contributors (to current version):
* Andrew Reynolds
*
* This file is part of the cvc5 project.
*
* Copyright (c) 2009-2021 by the authors listed in the file AUTHORS
* in the top-level source directory and their institutional affiliations.
* All rights reserved. See the file COPYING in the top-level source
* directory for licensing information.
* ****************************************************************************
*
* Management of a care graph based approach for theory combination.
*/
#include "theory/combination_engine.h"
#include "expr/node_visitor.h"
#include "proof/eager_proof_generator.h"
#include "theory/care_graph.h"
#include "theory/ee_manager_central.h"
#include "theory/ee_manager_distributed.h"
#include "theory/model_manager.h"
#include "theory/model_manager_distributed.h"
#include "theory/shared_solver_distributed.h"
#include "theory/theory_engine.h"
namespace cvc5 {
namespace theory {
CombinationEngine::CombinationEngine(Env& env,
TheoryEngine& te,
const std::vector<Theory*>& paraTheories)
: EnvObj(env),
d_te(te),
d_valuation(&te),
d_pnm(env.isTheoryProofProducing() ? env.getProofNodeManager() : nullptr),
d_logicInfo(te.getLogicInfo()),
d_paraTheories(paraTheories),
d_eemanager(nullptr),
d_mmanager(nullptr),
d_sharedSolver(nullptr),
d_cmbsPg(d_pnm ? new EagerProofGenerator(d_pnm, env.getUserContext())
: nullptr)
{
// create the equality engine, model manager, and shared solver
if (options::eeMode() == options::EqEngineMode::DISTRIBUTED)
{
// use the distributed shared solver
d_sharedSolver.reset(new SharedSolverDistributed(env, d_te));
// make the distributed equality engine manager
d_eemanager.reset(
new EqEngineManagerDistributed(env, d_te, *d_sharedSolver.get()));
// make the distributed model manager
d_mmanager.reset(
new ModelManagerDistributed(env, d_te, *d_eemanager.get()));
}
else if (options::eeMode() == options::EqEngineMode::CENTRAL)
{
// for now, the shared solver is the same in both approaches; use the
// distributed one for now
d_sharedSolver.reset(new SharedSolverDistributed(env, d_te));
// make the central equality engine manager
d_eemanager.reset(
new EqEngineManagerCentral(env, d_te, *d_sharedSolver.get()));
// make the distributed model manager
d_mmanager.reset(
new ModelManagerDistributed(env, d_te, *d_eemanager.get()));
}
else
{
Unhandled() << "CombinationEngine::finishInit: equality engine mode "
<< options::eeMode() << " not supported";
}
}
CombinationEngine::~CombinationEngine() {}
void CombinationEngine::finishInit()
{
Assert(d_eemanager != nullptr);
// initialize equality engines in all theories, including quantifiers engine
// and the (provided) shared solver
d_eemanager->initializeTheories();
Assert(d_mmanager != nullptr);
// initialize the model manager, based on the notify object of this class
eq::EqualityEngineNotify* meen = getModelEqualityEngineNotify();
d_mmanager->finishInit(meen);
}
const EeTheoryInfo* CombinationEngine::getEeTheoryInfo(TheoryId tid) const
{
return d_eemanager->getEeTheoryInfo(tid);
}
void CombinationEngine::resetModel() { d_mmanager->resetModel(); }
void CombinationEngine::postProcessModel(bool incomplete)
{
d_eemanager->notifyModel(incomplete);
// postprocess with the model
d_mmanager->postProcessModel(incomplete);
}
theory::TheoryModel* CombinationEngine::getModel()
{
return d_mmanager->getModel();
}
SharedSolver* CombinationEngine::getSharedSolver()
{
return d_sharedSolver.get();
}
bool CombinationEngine::isProofEnabled() const { return d_cmbsPg != nullptr; }
eq::EqualityEngineNotify* CombinationEngine::getModelEqualityEngineNotify()
{
// by default, no notifications from model's equality engine
return nullptr;
}
void CombinationEngine::resetRound()
{
// compute the relevant terms?
}
} // namespace theory
} // namespace cvc5
|
