1 /********************* */
2 /*! \file combination_engine.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 care graph based approach for theory combination.
15 #include "theory/combination_engine.h"
17 #include "expr/node_visitor.h"
18 #include "theory/care_graph.h"
19 #include "theory/ee_manager_distributed.h"
20 #include "theory/model_manager_distributed.h"
21 #include "theory/shared_solver_distributed.h"
22 #include "theory/theory_engine.h"
27 CombinationEngine::CombinationEngine(TheoryEngine
& te
,
28 const std::vector
<Theory
*>& paraTheories
,
29 ProofNodeManager
* pnm
)
31 d_logicInfo(te
.getLogicInfo()),
32 d_paraTheories(paraTheories
),
35 d_sharedSolver(nullptr),
36 d_cmbsPg(pnm
? new EagerProofGenerator(pnm
, te
.getUserContext())
41 CombinationEngine::~CombinationEngine() {}
43 void CombinationEngine::finishInit()
45 // create the equality engine, model manager, and shared solver
46 if (options::eeMode() == options::EqEngineMode::DISTRIBUTED
)
48 // use the distributed shared solver
49 d_sharedSolver
.reset(new SharedSolverDistributed(d_te
));
50 // make the distributed equality engine manager
52 new EqEngineManagerDistributed(d_te
, *d_sharedSolver
.get()));
53 // make the distributed model manager
54 d_mmanager
.reset(new ModelManagerDistributed(d_te
, *d_eemanager
.get()));
58 Unhandled() << "CombinationEngine::finishInit: equality engine mode "
59 << options::eeMode() << " not supported";
62 Assert(d_eemanager
!= nullptr);
64 // initialize equality engines in all theories, including quantifiers engine
65 // and the (provided) shared solver
66 d_eemanager
->initializeTheories();
68 Assert(d_mmanager
!= nullptr);
69 // initialize the model manager, based on the notify object of this class
70 eq::EqualityEngineNotify
* meen
= getModelEqualityEngineNotify();
71 d_mmanager
->finishInit(meen
);
74 const EeTheoryInfo
* CombinationEngine::getEeTheoryInfo(TheoryId tid
) const
76 return d_eemanager
->getEeTheoryInfo(tid
);
79 eq::EqualityEngine
* CombinationEngine::getCoreEqualityEngine()
81 return d_eemanager
->getCoreEqualityEngine();
84 void CombinationEngine::resetModel() { d_mmanager
->resetModel(); }
86 void CombinationEngine::postProcessModel(bool incomplete
)
88 // should have a consistent core equality engine
89 eq::EqualityEngine
* mee
= d_eemanager
->getCoreEqualityEngine();
92 AlwaysAssert(mee
->consistent());
94 // postprocess with the model
95 d_mmanager
->postProcessModel(incomplete
);
98 theory::TheoryModel
* CombinationEngine::getModel()
100 return d_mmanager
->getModel();
103 SharedSolver
* CombinationEngine::getSharedSolver()
105 return d_sharedSolver
.get();
107 bool CombinationEngine::isProofEnabled() const { return d_cmbsPg
!= nullptr; }
109 eq::EqualityEngineNotify
* CombinationEngine::getModelEqualityEngineNotify()
111 // by default, no notifications from model's equality engine
115 void CombinationEngine::sendLemma(TrustNode trn
, TheoryId atomsTo
)
117 d_te
.lemma(trn
, LemmaProperty::NONE
, atomsTo
);
120 void CombinationEngine::resetRound()
122 // compute the relevant terms?
125 } // namespace theory