GCC Code Coverage Report
Directory: . Exec Total Coverage
File: src/theory/engine_output_channel.cpp Lines: 97 118 82.2 %
Date: 2021-03-22 Branches: 120 332 36.1 %

Line Exec Source
1
/*********************                                                        */
2
/*! \file engine_output_channel.cpp
3
 ** \verbatim
4
 ** Top contributors (to current version):
5
 **   Andrew Reynolds, Tim King, Morgan Deters
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 The theory engine output channel.
13
 **/
14
15
#include "theory/engine_output_channel.h"
16
17
#include "prop/prop_engine.h"
18
#include "smt/smt_statistics_registry.h"
19
#include "theory/theory_engine.h"
20
21
using namespace CVC4::kind;
22
23
namespace CVC4 {
24
namespace theory {
25
26
116971
EngineOutputChannel::Statistics::Statistics(theory::TheoryId theory)
27
233942
    : conflicts(getStatsPrefix(theory) + "::conflicts", 0),
28
233942
      propagations(getStatsPrefix(theory) + "::propagations", 0),
29
233942
      lemmas(getStatsPrefix(theory) + "::lemmas", 0),
30
233942
      requirePhase(getStatsPrefix(theory) + "::requirePhase", 0),
31
233942
      restartDemands(getStatsPrefix(theory) + "::restartDemands", 0),
32
233942
      trustedConflicts(getStatsPrefix(theory) + "::trustedConflicts", 0),
33
1520623
      trustedLemmas(getStatsPrefix(theory) + "::trustedLemmas", 0)
34
{
35
116971
  smtStatisticsRegistry()->registerStat(&conflicts);
36
116971
  smtStatisticsRegistry()->registerStat(&propagations);
37
116971
  smtStatisticsRegistry()->registerStat(&lemmas);
38
116971
  smtStatisticsRegistry()->registerStat(&requirePhase);
39
116971
  smtStatisticsRegistry()->registerStat(&restartDemands);
40
116971
  smtStatisticsRegistry()->registerStat(&trustedConflicts);
41
116971
  smtStatisticsRegistry()->registerStat(&trustedLemmas);
42
116971
}
43
44
233864
EngineOutputChannel::Statistics::~Statistics()
45
{
46
116932
  smtStatisticsRegistry()->unregisterStat(&conflicts);
47
116932
  smtStatisticsRegistry()->unregisterStat(&propagations);
48
116932
  smtStatisticsRegistry()->unregisterStat(&lemmas);
49
116932
  smtStatisticsRegistry()->unregisterStat(&requirePhase);
50
116932
  smtStatisticsRegistry()->unregisterStat(&restartDemands);
51
116932
  smtStatisticsRegistry()->unregisterStat(&trustedConflicts);
52
116932
  smtStatisticsRegistry()->unregisterStat(&trustedLemmas);
53
116932
}
54
55
116971
EngineOutputChannel::EngineOutputChannel(TheoryEngine* engine,
56
116971
                                         theory::TheoryId theory)
57
116971
    : d_engine(engine), d_statistics(theory), d_theory(theory)
58
{
59
116971
}
60
61
21231998
void EngineOutputChannel::safePoint(ResourceManager::Resource r)
62
{
63
21231998
  spendResource(r);
64
21231998
  if (d_engine->d_interrupted)
65
  {
66
    throw theory::Interrupted();
67
  }
68
21231998
}
69
70
1103
void EngineOutputChannel::lemma(TNode lemma, LemmaProperty p)
71
{
72
2206
  Trace("theory::lemma") << "EngineOutputChannel<" << d_theory << ">::lemma("
73
1103
                         << lemma << ")"
74
1103
                         << ", properties = " << p << std::endl;
75
1103
  ++d_statistics.lemmas;
76
1103
  d_engine->d_outputChannelUsed = true;
77
78
2206
  TrustNode tlem = TrustNode::mkTrustLemma(lemma);
79
2206
  d_engine->lemma(tlem,
80
                  p,
81
1103
                  isLemmaPropertySendAtoms(p) ? d_theory : theory::THEORY_LAST,
82
                  d_theory);
83
1103
}
84
85
void EngineOutputChannel::splitLemma(TNode lemma, bool removable)
86
{
87
  Trace("theory::lemma") << "EngineOutputChannel<" << d_theory << ">::lemma("
88
                         << lemma << ")" << std::endl;
89
  ++d_statistics.lemmas;
90
  d_engine->d_outputChannelUsed = true;
91
92
  Trace("pf::explain") << "EngineOutputChannel::splitLemma( " << lemma << " )"
93
                       << std::endl;
94
  TrustNode tlem = TrustNode::mkTrustLemma(lemma);
95
  LemmaProperty p = removable ? LemmaProperty::REMOVABLE : LemmaProperty::NONE;
96
  d_engine->lemma(tlem, p, d_theory);
97
}
98
99
10866069
bool EngineOutputChannel::propagate(TNode literal)
100
{
101
21732138
  Trace("theory::propagate") << "EngineOutputChannel<" << d_theory
102
10866069
                             << ">::propagate(" << literal << ")" << std::endl;
103
10866069
  ++d_statistics.propagations;
104
10866069
  d_engine->d_outputChannelUsed = true;
105
10866069
  return d_engine->propagate(literal, d_theory);
106
}
107
108
87989
void EngineOutputChannel::conflict(TNode conflictNode)
109
{
110
175978
  Trace("theory::conflict")
111
87989
      << "EngineOutputChannel<" << d_theory << ">::conflict(" << conflictNode
112
87989
      << ")" << std::endl;
113
87989
  ++d_statistics.conflicts;
114
87989
  d_engine->d_outputChannelUsed = true;
115
175978
  TrustNode tConf = TrustNode::mkTrustConflict(conflictNode);
116
87989
  d_engine->conflict(tConf, d_theory);
117
87989
}
118
119
void EngineOutputChannel::demandRestart()
120
{
121
  NodeManager* curr = NodeManager::currentNM();
122
  Node restartVar = curr->mkSkolem(
123
      "restartVar",
124
      curr->booleanType(),
125
      "A boolean variable asserted to be true to force a restart");
126
  Trace("theory::restart") << "EngineOutputChannel<" << d_theory
127
                           << ">::restart(" << restartVar << ")" << std::endl;
128
  ++d_statistics.restartDemands;
129
  lemma(restartVar, LemmaProperty::REMOVABLE);
130
}
131
132
29199
void EngineOutputChannel::requirePhase(TNode n, bool phase)
133
{
134
58398
  Trace("theory") << "EngineOutputChannel::requirePhase(" << n << ", " << phase
135
29199
                  << ")" << std::endl;
136
29199
  ++d_statistics.requirePhase;
137
29199
  d_engine->getPropEngine()->requirePhase(n, phase);
138
29199
}
139
140
3047
void EngineOutputChannel::setIncomplete()
141
{
142
3047
  Trace("theory") << "setIncomplete()" << std::endl;
143
3047
  d_engine->setIncomplete(d_theory);
144
3047
}
145
146
27004291
void EngineOutputChannel::spendResource(ResourceManager::Resource r)
147
{
148
27004291
  d_engine->spendResource(r);
149
27004291
}
150
151
44975
void EngineOutputChannel::handleUserAttribute(const char* attr,
152
                                              theory::Theory* t)
153
{
154
44975
  d_engine->handleUserAttribute(attr, t);
155
44975
}
156
157
27365
void EngineOutputChannel::trustedConflict(TrustNode pconf)
158
{
159
27365
  Assert(pconf.getKind() == TrustNodeKind::CONFLICT);
160
54730
  Trace("theory::conflict")
161
27365
      << "EngineOutputChannel<" << d_theory << ">::trustedConflict("
162
27365
      << pconf.getNode() << ")" << std::endl;
163
27365
  if (pconf.getGenerator() != nullptr)
164
  {
165
13705
    ++d_statistics.trustedConflicts;
166
  }
167
27365
  ++d_statistics.conflicts;
168
27365
  d_engine->d_outputChannelUsed = true;
169
27365
  d_engine->conflict(pconf, d_theory);
170
27365
}
171
172
278274
void EngineOutputChannel::trustedLemma(TrustNode plem, LemmaProperty p)
173
{
174
556548
  Trace("theory::lemma") << "EngineOutputChannel<" << d_theory
175
278274
                         << ">::trustedLemma(" << plem << ")" << std::endl;
176
278274
  Assert(plem.getKind() == TrustNodeKind::LEMMA);
177
278274
  if (plem.getGenerator() != nullptr)
178
  {
179
30252
    ++d_statistics.trustedLemmas;
180
  }
181
278274
  ++d_statistics.lemmas;
182
278274
  d_engine->d_outputChannelUsed = true;
183
  // now, call the normal interface for lemma
184
556550
  d_engine->lemma(plem,
185
                  p,
186
278274
                  isLemmaPropertySendAtoms(p) ? d_theory : theory::THEORY_LAST,
187
                  d_theory);
188
278272
}
189
190
}  // namespace theory
191
26676
}  // namespace CVC4