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/theory_engine.h"
26 CombinationEngine::CombinationEngine(TheoryEngine
& te
,
27 const std::vector
<Theory
*>& paraTheories
,
28 ProofNodeManager
* pnm
)
30 d_logicInfo(te
.getLogicInfo()),
31 d_paraTheories(paraTheories
),
34 d_cmbsPg(pnm
? new EagerProofGenerator(pnm
, te
.getUserContext())
39 CombinationEngine::~CombinationEngine() {}
41 void CombinationEngine::finishInit()
43 // create the equality engine, model manager, and shared solver
44 if (options::eeMode() == options::EqEngineMode::DISTRIBUTED
)
46 // make the distributed equality engine manager
47 d_eemanager
.reset(new EqEngineManagerDistributed(d_te
));
48 // make the distributed model manager
49 d_mmanager
.reset(new ModelManagerDistributed(d_te
, *d_eemanager
.get()));
53 Unhandled() << "CombinationEngine::finishInit: equality engine mode "
54 << options::eeMode() << " not supported";
57 Assert(d_eemanager
!= nullptr);
59 // initialize equality engines in all theories, including quantifiers engine
60 // and the (provided) shared solver
61 d_eemanager
->initializeTheories();
63 Assert(d_mmanager
!= nullptr);
64 // initialize the model manager, based on the notify object of this class
65 eq::EqualityEngineNotify
* meen
= getModelEqualityEngineNotify();
66 d_mmanager
->finishInit(meen
);
69 const EeTheoryInfo
* CombinationEngine::getEeTheoryInfo(TheoryId tid
) const
71 return d_eemanager
->getEeTheoryInfo(tid
);
74 eq::EqualityEngine
* CombinationEngine::getCoreEqualityEngine()
76 return d_eemanager
->getCoreEqualityEngine();
79 void CombinationEngine::resetModel() { d_mmanager
->resetModel(); }
81 void CombinationEngine::postProcessModel(bool incomplete
)
83 // should have a consistent core equality engine
84 eq::EqualityEngine
* mee
= d_eemanager
->getCoreEqualityEngine();
87 AlwaysAssert(mee
->consistent());
89 // postprocess with the model
90 d_mmanager
->postProcessModel(incomplete
);
93 theory::TheoryModel
* CombinationEngine::getModel()
95 return d_mmanager
->getModel();
98 bool CombinationEngine::isProofEnabled() const { return d_cmbsPg
!= nullptr; }
100 eq::EqualityEngineNotify
* CombinationEngine::getModelEqualityEngineNotify()
102 // by default, no notifications from model's equality engine
106 void CombinationEngine::sendLemma(TrustNode trn
, TheoryId atomsTo
)
108 d_te
.lemma(trn
, LemmaProperty::NONE
, atomsTo
);
111 void CombinationEngine::resetRound()
113 // compute the relevant terms?
116 } // namespace theory