1 /********************* */
2 /*! \file engine_output_channel.cpp
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-2020 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
12 ** \brief The theory engine output channel.
15 #include "theory/engine_output_channel.h"
17 #include "prop/prop_engine.h"
18 #include "smt/smt_statistics_registry.h"
19 #include "theory/theory_engine.h"
21 using namespace CVC4::kind
;
26 EngineOutputChannel::Statistics::Statistics(theory::TheoryId theory
)
27 : conflicts(getStatsPrefix(theory
) + "::conflicts", 0),
28 propagations(getStatsPrefix(theory
) + "::propagations", 0),
29 lemmas(getStatsPrefix(theory
) + "::lemmas", 0),
30 requirePhase(getStatsPrefix(theory
) + "::requirePhase", 0),
31 restartDemands(getStatsPrefix(theory
) + "::restartDemands", 0),
32 trustedConflicts(getStatsPrefix(theory
) + "::trustedConflicts", 0),
33 trustedLemmas(getStatsPrefix(theory
) + "::trustedLemmas", 0)
35 smtStatisticsRegistry()->registerStat(&conflicts
);
36 smtStatisticsRegistry()->registerStat(&propagations
);
37 smtStatisticsRegistry()->registerStat(&lemmas
);
38 smtStatisticsRegistry()->registerStat(&requirePhase
);
39 smtStatisticsRegistry()->registerStat(&restartDemands
);
40 smtStatisticsRegistry()->registerStat(&trustedConflicts
);
41 smtStatisticsRegistry()->registerStat(&trustedLemmas
);
44 EngineOutputChannel::Statistics::~Statistics()
46 smtStatisticsRegistry()->unregisterStat(&conflicts
);
47 smtStatisticsRegistry()->unregisterStat(&propagations
);
48 smtStatisticsRegistry()->unregisterStat(&lemmas
);
49 smtStatisticsRegistry()->unregisterStat(&requirePhase
);
50 smtStatisticsRegistry()->unregisterStat(&restartDemands
);
51 smtStatisticsRegistry()->unregisterStat(&trustedConflicts
);
52 smtStatisticsRegistry()->unregisterStat(&trustedLemmas
);
55 EngineOutputChannel::EngineOutputChannel(TheoryEngine
* engine
,
56 theory::TheoryId theory
)
57 : d_engine(engine
), d_statistics(theory
), d_theory(theory
)
61 void EngineOutputChannel::safePoint(ResourceManager::Resource r
)
64 if (d_engine
->d_interrupted
)
66 throw theory::Interrupted();
70 theory::LemmaStatus
EngineOutputChannel::lemma(TNode lemma
, LemmaProperty p
)
72 Debug("theory::lemma") << "EngineOutputChannel<" << d_theory
<< ">::lemma("
74 << ", properties = " << p
<< std::endl
;
75 ++d_statistics
.lemmas
;
76 d_engine
->d_outputChannelUsed
= true;
78 TrustNode tlem
= TrustNode::mkTrustLemma(lemma
);
79 theory::LemmaStatus result
= d_engine
->lemma(
82 isLemmaPropertySendAtoms(p
) ? d_theory
: theory::THEORY_LAST
,
87 theory::LemmaStatus
EngineOutputChannel::splitLemma(TNode lemma
, bool removable
)
89 Debug("theory::lemma") << "EngineOutputChannel<" << d_theory
<< ">::lemma("
90 << lemma
<< ")" << std::endl
;
91 ++d_statistics
.lemmas
;
92 d_engine
->d_outputChannelUsed
= true;
94 Debug("pf::explain") << "EngineOutputChannel::splitLemma( " << lemma
<< " )"
96 TrustNode tlem
= TrustNode::mkTrustLemma(lemma
);
97 LemmaProperty p
= removable
? LemmaProperty::REMOVABLE
: LemmaProperty::NONE
;
98 theory::LemmaStatus result
= d_engine
->lemma(tlem
, p
, d_theory
);
102 bool EngineOutputChannel::propagate(TNode literal
)
104 Debug("theory::propagate") << "EngineOutputChannel<" << d_theory
105 << ">::propagate(" << literal
<< ")" << std::endl
;
106 ++d_statistics
.propagations
;
107 d_engine
->d_outputChannelUsed
= true;
108 return d_engine
->propagate(literal
, d_theory
);
111 void EngineOutputChannel::conflict(TNode conflictNode
)
113 Trace("theory::conflict")
114 << "EngineOutputChannel<" << d_theory
<< ">::conflict(" << conflictNode
116 ++d_statistics
.conflicts
;
117 d_engine
->d_outputChannelUsed
= true;
118 TrustNode tConf
= TrustNode::mkTrustConflict(conflictNode
);
119 d_engine
->conflict(tConf
, d_theory
);
122 void EngineOutputChannel::demandRestart()
124 NodeManager
* curr
= NodeManager::currentNM();
125 Node restartVar
= curr
->mkSkolem(
128 "A boolean variable asserted to be true to force a restart");
129 Trace("theory::restart") << "EngineOutputChannel<" << d_theory
130 << ">::restart(" << restartVar
<< ")" << std::endl
;
131 ++d_statistics
.restartDemands
;
132 lemma(restartVar
, LemmaProperty::REMOVABLE
);
135 void EngineOutputChannel::requirePhase(TNode n
, bool phase
)
137 Debug("theory") << "EngineOutputChannel::requirePhase(" << n
<< ", " << phase
139 ++d_statistics
.requirePhase
;
140 d_engine
->getPropEngine()->requirePhase(n
, phase
);
143 void EngineOutputChannel::setIncomplete()
145 Trace("theory") << "setIncomplete()" << std::endl
;
146 d_engine
->setIncomplete(d_theory
);
149 void EngineOutputChannel::spendResource(ResourceManager::Resource r
)
151 d_engine
->spendResource(r
);
154 void EngineOutputChannel::handleUserAttribute(const char* attr
,
157 d_engine
->handleUserAttribute(attr
, t
);
160 void EngineOutputChannel::trustedConflict(TrustNode pconf
)
162 Assert(pconf
.getKind() == TrustNodeKind::CONFLICT
);
163 Trace("theory::conflict")
164 << "EngineOutputChannel<" << d_theory
<< ">::trustedConflict("
165 << pconf
.getNode() << ")" << std::endl
;
166 if (pconf
.getGenerator() != nullptr)
168 ++d_statistics
.trustedConflicts
;
170 ++d_statistics
.conflicts
;
171 d_engine
->d_outputChannelUsed
= true;
172 d_engine
->conflict(pconf
, d_theory
);
175 LemmaStatus
EngineOutputChannel::trustedLemma(TrustNode plem
, LemmaProperty p
)
177 Debug("theory::lemma") << "EngineOutputChannel<" << d_theory
178 << ">::trustedLemma(" << plem
<< ")" << std::endl
;
179 Assert(plem
.getKind() == TrustNodeKind::LEMMA
);
180 if (plem
.getGenerator() != nullptr)
182 ++d_statistics
.trustedLemmas
;
184 ++d_statistics
.lemmas
;
185 d_engine
->d_outputChannelUsed
= true;
186 // now, call the normal interface for lemma
187 return d_engine
->lemma(
190 isLemmaPropertySendAtoms(p
) ? d_theory
: theory::THEORY_LAST
,
194 } // namespace theory