GCC Code Coverage Report
Directory: . Exec Total Coverage
File: src/theory/model_manager_distributed.cpp Lines: 44 49 89.8 %
Date: 2021-03-23 Branches: 41 90 45.6 %

Line Exec Source
1
/*********************                                                        */
2
/*! \file model_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 model generation.
13
 **/
14
15
#include "theory/model_manager_distributed.h"
16
17
#include "theory/theory_engine.h"
18
#include "theory/theory_model.h"
19
#include "theory/theory_model_builder.h"
20
21
namespace CVC4 {
22
namespace theory {
23
24
8997
ModelManagerDistributed::ModelManagerDistributed(TheoryEngine& te,
25
8997
                                                 EqEngineManager& eem)
26
8997
    : ModelManager(te, eem)
27
{
28
8997
}
29
30
26982
ModelManagerDistributed::~ModelManagerDistributed()
31
{
32
  // pop the model context which we pushed on initialization
33
8994
  d_modelEeContext.pop();
34
17988
}
35
36
8997
void ModelManagerDistributed::initializeModelEqEngine(
37
    eq::EqualityEngineNotify* notify)
38
{
39
  // initialize the model equality engine, use the provided notification object,
40
  // which belongs e.g. to CombinationModelBased
41
17994
  EeSetupInfo esim;
42
8997
  esim.d_notify = notify;
43
8997
  esim.d_name = d_model->getName() + "::ee";
44
8997
  esim.d_constantsAreTriggers = false;
45
17994
  d_modelEqualityEngineAlloc.reset(
46
8997
      d_eem.allocateEqualityEngine(esim, &d_modelEeContext));
47
8997
  d_modelEqualityEngine = d_modelEqualityEngineAlloc.get();
48
  // finish initializing the model
49
8997
  d_model->finishInit(d_modelEqualityEngine);
50
  // We push a context during initialization since the model is cleared during
51
  // collectModelInfo using pop/push.
52
8997
  d_modelEeContext.push();
53
8997
}
54
55
18953
bool ModelManagerDistributed::prepareModel()
56
{
57
37906
  Trace("model-builder") << "ModelManagerDistributed: reset model..."
58
18953
                         << std::endl;
59
60
  // push/pop to clear the equality engine of the model
61
18953
  d_modelEeContext.pop();
62
18953
  d_modelEeContext.push();
63
64
  // Collect model info from the theories
65
37906
  Trace("model-builder") << "ModelManagerDistributed: Collect model info..."
66
18953
                         << std::endl;
67
  // Consult each active theory to get all relevant information concerning the
68
  // model, which includes both dump their equality information and assigning
69
  // values. Notice the order of theories here is important and is the same
70
  // as the list in CVC4_FOR_EACH_THEORY in theory_engine.cpp.
71
265320
  for (TheoryId theoryId = theory::THEORY_FIRST; theoryId < theory::THEORY_LAST;
72
       ++theoryId)
73
  {
74
246370
    if (!d_logicInfo.isTheoryEnabled(theoryId))
75
    {
76
      // theory not active, skip
77
110912
      continue;
78
    }
79
135458
    Theory* t = d_te.theoryOf(theoryId);
80
270916
    Trace("model-builder") << "  CollectModelInfo on theory: " << theoryId
81
135458
                           << std::endl;
82
    // collect the asserted terms
83
270914
    std::set<Node> termSet;
84
135458
    collectAssertedTerms(theoryId, termSet);
85
    // also get relevant terms
86
135458
    t->computeRelevantTerms(termSet);
87
135458
    if (!t->collectModelInfo(d_model, termSet))
88
    {
89
4
      Trace("model-builder")
90
2
          << "ModelManagerDistributed: fail collect model info" << std::endl;
91
2
      return false;
92
    }
93
  }
94
95
18950
  if (!collectModelBooleanVariables())
96
  {
97
    Trace("model-builder") << "ModelManagerDistributed: fail Boolean variables"
98
                           << std::endl;
99
    return false;
100
  }
101
102
18950
  return true;
103
}
104
105
18950
bool ModelManagerDistributed::finishBuildModel() const
106
{
107
  // do not use relevant terms
108
18950
  if (!d_modelBuilder->buildModel(d_model))
109
  {
110
    Trace("model-builder") << "ModelManager: fail build model" << std::endl;
111
    return false;
112
  }
113
18950
  return true;
114
}
115
116
}  // namespace theory
117
26685
}  // namespace CVC4