GCC Code Coverage Report
Directory: . Exec Total Coverage
File: src/theory/model_manager_distributed.cpp Lines: 44 49 89.8 %
Date: 2021-03-22 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
8995
ModelManagerDistributed::ModelManagerDistributed(TheoryEngine& te,
25
8995
                                                 EqEngineManager& eem)
26
8995
    : ModelManager(te, eem)
27
{
28
8995
}
29
30
26976
ModelManagerDistributed::~ModelManagerDistributed()
31
{
32
  // pop the model context which we pushed on initialization
33
8992
  d_modelEeContext.pop();
34
17984
}
35
36
8995
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
17990
  EeSetupInfo esim;
42
8995
  esim.d_notify = notify;
43
8995
  esim.d_name = d_model->getName() + "::ee";
44
8995
  esim.d_constantsAreTriggers = false;
45
17990
  d_modelEqualityEngineAlloc.reset(
46
8995
      d_eem.allocateEqualityEngine(esim, &d_modelEeContext));
47
8995
  d_modelEqualityEngine = d_modelEqualityEngineAlloc.get();
48
  // finish initializing the model
49
8995
  d_model->finishInit(d_modelEqualityEngine);
50
  // We push a context during initialization since the model is cleared during
51
  // collectModelInfo using pop/push.
52
8995
  d_modelEeContext.push();
53
8995
}
54
55
18945
bool ModelManagerDistributed::prepareModel()
56
{
57
37890
  Trace("model-builder") << "ModelManagerDistributed: reset model..."
58
18945
                         << std::endl;
59
60
  // push/pop to clear the equality engine of the model
61
18945
  d_modelEeContext.pop();
62
18945
  d_modelEeContext.push();
63
64
  // Collect model info from the theories
65
37890
  Trace("model-builder") << "ModelManagerDistributed: Collect model info..."
66
18945
                         << 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
265208
  for (TheoryId theoryId = theory::THEORY_FIRST; theoryId < theory::THEORY_LAST;
72
       ++theoryId)
73
  {
74
246266
    if (!d_logicInfo.isTheoryEnabled(theoryId))
75
    {
76
      // theory not active, skip
77
110876
      continue;
78
    }
79
135390
    Theory* t = d_te.theoryOf(theoryId);
80
270780
    Trace("model-builder") << "  CollectModelInfo on theory: " << theoryId
81
135390
                           << std::endl;
82
    // collect the asserted terms
83
270778
    std::set<Node> termSet;
84
135390
    collectAssertedTerms(theoryId, termSet);
85
    // also get relevant terms
86
135390
    t->computeRelevantTerms(termSet);
87
135390
    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
18942
  if (!collectModelBooleanVariables())
96
  {
97
    Trace("model-builder") << "ModelManagerDistributed: fail Boolean variables"
98
                           << std::endl;
99
    return false;
100
  }
101
102
18942
  return true;
103
}
104
105
18942
bool ModelManagerDistributed::finishBuildModel() const
106
{
107
  // do not use relevant terms
108
18942
  if (!d_modelBuilder->buildModel(d_model))
109
  {
110
    Trace("model-builder") << "ModelManager: fail build model" << std::endl;
111
    return false;
112
  }
113
18942
  return true;
114
}
115
116
}  // namespace theory
117
26676
}  // namespace CVC4