GCC Code Coverage Report
Directory: . Exec Total Coverage
File: src/theory/ee_manager_distributed.cpp Lines: 46 47 97.9 %
Date: 2021-03-22 Branches: 40 112 35.7 %

Line Exec Source
1
/*********************                                                        */
2
/*! \file ee_manager_distributed.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 distributed approach for equality sharing.
13
 **/
14
15
#include "theory/ee_manager_distributed.h"
16
17
#include "theory/quantifiers_engine.h"
18
#include "theory/shared_solver.h"
19
#include "theory/theory_engine.h"
20
#include "theory/uf/equality_engine.h"
21
22
namespace CVC4 {
23
namespace theory {
24
25
8995
EqEngineManagerDistributed::EqEngineManagerDistributed(TheoryEngine& te,
26
8995
                                                       SharedSolver& shs)
27
8995
    : EqEngineManager(te, shs), d_masterEENotify(nullptr)
28
{
29
8995
}
30
31
17984
EqEngineManagerDistributed::~EqEngineManagerDistributed()
32
{
33
17984
}
34
35
8995
void EqEngineManagerDistributed::initializeTheories()
36
{
37
8995
  context::Context* c = d_te.getSatContext();
38
  // initialize the shared solver
39
17990
  EeSetupInfo esis;
40
8995
  if (d_sharedSolver.needsEqualityEngine(esis))
41
  {
42
    // allocate an equality engine for the shared terms database
43
8995
    d_stbEqualityEngine.reset(allocateEqualityEngine(esis, c));
44
8995
    d_sharedSolver.setEqualityEngine(d_stbEqualityEngine.get());
45
  }
46
  else
47
  {
48
    Unhandled() << "Expected shared solver to use equality engine";
49
  }
50
51
8995
  const LogicInfo& logicInfo = d_te.getLogicInfo();
52
8995
  if (logicInfo.isQuantified())
53
  {
54
    // construct the master equality engine
55
6052
    Assert(d_masterEqualityEngine == nullptr);
56
6052
    QuantifiersEngine* qe = d_te.getQuantifiersEngine();
57
6052
    Assert(qe != nullptr);
58
6052
    d_masterEENotify.reset(new MasterNotifyClass(qe));
59
18156
    d_masterEqualityEngine.reset(new eq::EqualityEngine(*d_masterEENotify.get(),
60
6052
                                                        d_te.getSatContext(),
61
                                                        "theory::master",
62
6052
                                                        false));
63
  }
64
  // allocate equality engines per theory
65
125930
  for (TheoryId theoryId = theory::THEORY_FIRST;
66
125930
       theoryId != theory::THEORY_LAST;
67
       ++theoryId)
68
  {
69
116935
    Theory* t = d_te.theoryOf(theoryId);
70
116935
    if (t == nullptr)
71
    {
72
      // theory not active, skip
73
27028
      continue;
74
    }
75
    // always allocate an object in d_einfo here
76
116935
    EeTheoryInfo& eet = d_einfo[theoryId];
77
206842
    EeSetupInfo esi;
78
116935
    if (!t->needsEqualityEngine(esi))
79
    {
80
      // the theory said it doesn't need an equality engine, skip
81
18033
      continue;
82
    }
83
107897
    if (esi.d_useMaster)
84
    {
85
      // the theory said it wants to use the master equality engine
86
8995
      eet.d_usedEe = d_masterEqualityEngine.get();
87
8995
      continue;
88
    }
89
    // allocate the equality engine
90
89907
    eet.d_allocEe.reset(allocateEqualityEngine(esi, c));
91
    // the theory uses the equality engine
92
89907
    eet.d_usedEe = eet.d_allocEe.get();
93
    // if there is a master equality engine
94
89907
    if (d_masterEqualityEngine != nullptr)
95
    {
96
      // set the master equality engine of the theory's equality engine
97
60518
      eet.d_allocEe->setMasterEqualityEngine(d_masterEqualityEngine.get());
98
    }
99
  }
100
8995
}
101
102
5953
void EqEngineManagerDistributed::notifyModel(bool incomplete)
103
{
104
  // should have a consistent master equality engine
105
5953
  if (d_masterEqualityEngine.get() != nullptr)
106
  {
107
2456
    AlwaysAssert(d_masterEqualityEngine->consistent());
108
  }
109
5953
}
110
111
743568
void EqEngineManagerDistributed::MasterNotifyClass::eqNotifyNewClass(TNode t)
112
{
113
  // adds t to the quantifiers term database
114
743568
  d_quantEngine->eqNotifyNewClass(t);
115
743568
}
116
117
}  // namespace theory
118
26676
}  // namespace CVC4