GCC Code Coverage Report
Directory: . Exec Total Coverage
File: src/theory/combination_engine.cpp Lines: 39 41 95.1 %
Date: 2021-03-22 Branches: 20 80 25.0 %

Line Exec Source
1
/*********************                                                        */
2
/*! \file combination_engine.cpp
3
 ** \verbatim
4
 ** Top contributors (to current version):
5
 **   Andrew Reynolds
6
 ** This file is part of the CVC4 project.
7
 ** Copyright (c) 2009-2021 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
11
 **
12
 ** \brief Management of a care graph based approach for theory combination.
13
 **/
14
15
#include "theory/combination_engine.h"
16
17
#include "expr/node_visitor.h"
18
#include "theory/care_graph.h"
19
#include "theory/eager_proof_generator.h"
20
#include "theory/ee_manager_distributed.h"
21
#include "theory/model_manager.h"
22
#include "theory/model_manager_distributed.h"
23
#include "theory/shared_solver.h"
24
#include "theory/shared_solver_distributed.h"
25
#include "theory/theory_engine.h"
26
27
namespace CVC4 {
28
namespace theory {
29
30
8995
CombinationEngine::CombinationEngine(TheoryEngine& te,
31
                                     const std::vector<Theory*>& paraTheories,
32
8995
                                     ProofNodeManager* pnm)
33
    : d_te(te),
34
      d_valuation(&te),
35
      d_pnm(pnm),
36
8995
      d_logicInfo(te.getLogicInfo()),
37
      d_paraTheories(paraTheories),
38
      d_eemanager(nullptr),
39
      d_mmanager(nullptr),
40
      d_sharedSolver(nullptr),
41
1924
      d_cmbsPg(pnm ? new EagerProofGenerator(pnm, te.getUserContext())
42
19914
                   : nullptr)
43
{
44
8995
}
45
46
8992
CombinationEngine::~CombinationEngine() {}
47
48
8995
void CombinationEngine::finishInit()
49
{
50
  // create the equality engine, model manager, and shared solver
51
17990
  if (options::eeMode() == options::EqEngineMode::DISTRIBUTED)
52
  {
53
    // use the distributed shared solver
54
8995
    d_sharedSolver.reset(new SharedSolverDistributed(d_te, d_pnm));
55
    // make the distributed equality engine manager
56
17990
    d_eemanager.reset(
57
8995
        new EqEngineManagerDistributed(d_te, *d_sharedSolver.get()));
58
    // make the distributed model manager
59
8995
    d_mmanager.reset(new ModelManagerDistributed(d_te, *d_eemanager.get()));
60
  }
61
  else
62
  {
63
    Unhandled() << "CombinationEngine::finishInit: equality engine mode "
64
                << options::eeMode() << " not supported";
65
  }
66
67
8995
  Assert(d_eemanager != nullptr);
68
69
  // initialize equality engines in all theories, including quantifiers engine
70
  // and the (provided) shared solver
71
8995
  d_eemanager->initializeTheories();
72
73
8995
  Assert(d_mmanager != nullptr);
74
  // initialize the model manager, based on the notify object of this class
75
8995
  eq::EqualityEngineNotify* meen = getModelEqualityEngineNotify();
76
8995
  d_mmanager->finishInit(meen);
77
8995
}
78
79
116935
const EeTheoryInfo* CombinationEngine::getEeTheoryInfo(TheoryId tid) const
80
{
81
116935
  return d_eemanager->getEeTheoryInfo(tid);
82
}
83
84
22352
void CombinationEngine::resetModel() { d_mmanager->resetModel(); }
85
86
5953
void CombinationEngine::postProcessModel(bool incomplete)
87
{
88
5953
  d_eemanager->notifyModel(incomplete);
89
  // postprocess with the model
90
5953
  d_mmanager->postProcessModel(incomplete);
91
5953
}
92
93
286608
theory::TheoryModel* CombinationEngine::getModel()
94
{
95
286608
  return d_mmanager->getModel();
96
}
97
98
8995
SharedSolver* CombinationEngine::getSharedSolver()
99
{
100
8995
  return d_sharedSolver.get();
101
}
102
53661
bool CombinationEngine::isProofEnabled() const { return d_cmbsPg != nullptr; }
103
104
8995
eq::EqualityEngineNotify* CombinationEngine::getModelEqualityEngineNotify()
105
{
106
  // by default, no notifications from model's equality engine
107
8995
  return nullptr;
108
}
109
110
53661
void CombinationEngine::sendLemma(TrustNode trn, TheoryId atomsTo)
111
{
112
53661
  d_te.lemma(trn, LemmaProperty::NONE, atomsTo);
113
53661
}
114
115
73140
void CombinationEngine::resetRound()
116
{
117
  // compute the relevant terms?
118
73140
}
119
120
}  // namespace theory
121
26676
}  // namespace CVC4