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
)
32 d_logicInfo(te
.getLogicInfo()),
33 d_paraTheories(paraTheories
),
36 d_sharedSolver(nullptr),
37 d_cmbsPg(pnm
? new EagerProofGenerator(pnm
, te
.getUserContext())
42 CombinationEngine::~CombinationEngine() {}
44 void CombinationEngine::finishInit()
46 // create the equality engine, model manager, and shared solver
47 if (options::eeMode() == options::EqEngineMode::DISTRIBUTED
)
49 // use the distributed shared solver
50 d_sharedSolver
.reset(new SharedSolverDistributed(d_te
, d_pnm
));
51 // make the distributed equality engine manager
53 new EqEngineManagerDistributed(d_te
, *d_sharedSolver
.get()));
54 // make the distributed model manager
55 d_mmanager
.reset(new ModelManagerDistributed(d_te
, *d_eemanager
.get()));
59 Unhandled() << "CombinationEngine::finishInit: equality engine mode "
60 << options::eeMode() << " not supported";
63 Assert(d_eemanager
!= nullptr);
65 // initialize equality engines in all theories, including quantifiers engine
66 // and the (provided) shared solver
67 d_eemanager
->initializeTheories();
69 Assert(d_mmanager
!= nullptr);
70 // initialize the model manager, based on the notify object of this class
71 eq::EqualityEngineNotify
* meen
= getModelEqualityEngineNotify();
72 d_mmanager
->finishInit(meen
);
75 const EeTheoryInfo
* CombinationEngine::getEeTheoryInfo(TheoryId tid
) const
77 return d_eemanager
->getEeTheoryInfo(tid
);
80 eq::EqualityEngine
* CombinationEngine::getCoreEqualityEngine()
82 return d_eemanager
->getCoreEqualityEngine();
85 void CombinationEngine::resetModel() { d_mmanager
->resetModel(); }
87 void CombinationEngine::postProcessModel(bool incomplete
)
89 // should have a consistent core equality engine
90 eq::EqualityEngine
* mee
= d_eemanager
->getCoreEqualityEngine();
93 AlwaysAssert(mee
->consistent());
95 // postprocess with the model
96 d_mmanager
->postProcessModel(incomplete
);
99 theory::TheoryModel
* CombinationEngine::getModel()
101 return d_mmanager
->getModel();
104 SharedSolver
* CombinationEngine::getSharedSolver()
106 return d_sharedSolver
.get();
108 bool CombinationEngine::isProofEnabled() const { return d_cmbsPg
!= nullptr; }
110 eq::EqualityEngineNotify
* CombinationEngine::getModelEqualityEngineNotify()
112 // by default, no notifications from model's equality engine
116 void CombinationEngine::sendLemma(TrustNode trn
, TheoryId atomsTo
)
118 d_te
.lemma(trn
, LemmaProperty::NONE
, atomsTo
);
121 void CombinationEngine::resetRound()
123 // compute the relevant terms?
126 } // namespace theory