1 /********************* */
2 /*! \file engine_output_channel.cpp
4 ** Top contributors (to current version):
5 ** Andrew Reynolds, Guy Katz, Tim King
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 "proof/cnf_proof.h"
18 #include "proof/lemma_proof.h"
19 #include "proof/proof_manager.h"
20 #include "proof/theory_proof.h"
21 #include "prop/prop_engine.h"
22 #include "smt/smt_statistics_registry.h"
23 #include "theory/theory_engine.h"
25 using namespace CVC4::kind
;
30 EngineOutputChannel::Statistics::Statistics(theory::TheoryId theory
)
31 : conflicts(getStatsPrefix(theory
) + "::conflicts", 0),
32 propagations(getStatsPrefix(theory
) + "::propagations", 0),
33 lemmas(getStatsPrefix(theory
) + "::lemmas", 0),
34 requirePhase(getStatsPrefix(theory
) + "::requirePhase", 0),
35 restartDemands(getStatsPrefix(theory
) + "::restartDemands", 0),
36 trustedConflicts(getStatsPrefix(theory
) + "::trustedConflicts", 0),
37 trustedLemmas(getStatsPrefix(theory
) + "::trustedLemmas", 0)
39 smtStatisticsRegistry()->registerStat(&conflicts
);
40 smtStatisticsRegistry()->registerStat(&propagations
);
41 smtStatisticsRegistry()->registerStat(&lemmas
);
42 smtStatisticsRegistry()->registerStat(&requirePhase
);
43 smtStatisticsRegistry()->registerStat(&restartDemands
);
44 smtStatisticsRegistry()->registerStat(&trustedConflicts
);
45 smtStatisticsRegistry()->registerStat(&trustedLemmas
);
48 EngineOutputChannel::Statistics::~Statistics()
50 smtStatisticsRegistry()->unregisterStat(&conflicts
);
51 smtStatisticsRegistry()->unregisterStat(&propagations
);
52 smtStatisticsRegistry()->unregisterStat(&lemmas
);
53 smtStatisticsRegistry()->unregisterStat(&requirePhase
);
54 smtStatisticsRegistry()->unregisterStat(&restartDemands
);
55 smtStatisticsRegistry()->unregisterStat(&trustedConflicts
);
56 smtStatisticsRegistry()->unregisterStat(&trustedLemmas
);
59 EngineOutputChannel::EngineOutputChannel(TheoryEngine
* engine
,
60 theory::TheoryId theory
)
61 : d_engine(engine
), d_statistics(theory
), d_theory(theory
)
65 void EngineOutputChannel::safePoint(ResourceManager::Resource r
)
68 if (d_engine
->d_interrupted
)
70 throw theory::Interrupted();
74 theory::LemmaStatus
EngineOutputChannel::lemma(TNode lemma
,
78 Debug("theory::lemma") << "EngineOutputChannel<" << d_theory
<< ">::lemma("
80 << ", properties = " << p
<< std::endl
;
81 ++d_statistics
.lemmas
;
82 d_engine
->d_outputChannelUsed
= true;
85 bool preprocess
= isLemmaPropertyPreprocess(p
);
86 registerLemmaRecipe(lemma
, lemma
, preprocess
, d_theory
);
89 TrustNode tlem
= TrustNode::mkTrustLemma(lemma
);
90 theory::LemmaStatus result
= d_engine
->lemma(
95 isLemmaPropertySendAtoms(p
) ? d_theory
: theory::THEORY_LAST
);
99 void EngineOutputChannel::registerLemmaRecipe(Node lemma
,
102 theory::TheoryId theoryId
)
104 // During CNF conversion, conjunctions will be broken down into
105 // multiple lemmas. In order for the recipes to match, we have to do
107 NodeManager
* nm
= NodeManager::currentNM();
109 if (preprocess
) lemma
= d_engine
->preprocess(lemma
);
111 bool negated
= (lemma
.getKind() == NOT
);
112 Node nnLemma
= negated
? lemma
[0] : lemma
;
114 switch (nnLemma
.getKind())
119 for (unsigned i
= 0; i
< nnLemma
.getNumChildren(); ++i
)
120 registerLemmaRecipe(nnLemma
[i
], originalLemma
, false, theoryId
);
124 NodeBuilder
<> builder(OR
);
125 for (unsigned i
= 0; i
< nnLemma
.getNumChildren(); ++i
)
126 builder
<< nnLemma
[i
].negate();
129 (builder
.getNumChildren() == 1) ? builder
[0] : builder
;
130 registerLemmaRecipe(disjunction
, originalLemma
, false, theoryId
);
135 if (nnLemma
[0].getType().isBoolean())
139 registerLemmaRecipe(nm
->mkNode(OR
, nnLemma
[0], nnLemma
[1].negate()),
143 registerLemmaRecipe(nm
->mkNode(OR
, nnLemma
[0].negate(), nnLemma
[1]),
150 registerLemmaRecipe(nm
->mkNode(OR
, nnLemma
[0], nnLemma
[1]),
155 nm
->mkNode(OR
, nnLemma
[0].negate(), nnLemma
[1].negate()),
166 registerLemmaRecipe(nm
->mkNode(OR
, nnLemma
[0].negate(), nnLemma
[1]),
170 registerLemmaRecipe(nm
->mkNode(OR
, nnLemma
[0], nnLemma
[2]),
178 nm
->mkNode(OR
, nnLemma
[0].negate(), nnLemma
[1].negate()),
182 registerLemmaRecipe(nm
->mkNode(OR
, nnLemma
[0], nnLemma
[2].negate()),
192 // Theory lemmas have one step that proves the empty clause
193 LemmaProofRecipe proofRecipe
;
195 LemmaProofRecipe::ProofStep
proofStep(theoryId
, emptyNode
);
197 // Remember the original lemma, so we can report this later when asked to
198 proofRecipe
.setOriginalLemma(originalLemma
);
200 // Record the assertions and rewrites
202 if (lemma
.getKind() == OR
)
204 for (unsigned i
= 0; i
< lemma
.getNumChildren(); ++i
)
206 rewritten
= theory::Rewriter::rewrite(lemma
[i
]);
207 if (rewritten
!= lemma
[i
])
209 proofRecipe
.addRewriteRule(lemma
[i
].negate(), rewritten
.negate());
211 proofStep
.addAssertion(lemma
[i
]);
212 proofRecipe
.addBaseAssertion(rewritten
);
217 rewritten
= theory::Rewriter::rewrite(lemma
);
218 if (rewritten
!= lemma
)
220 proofRecipe
.addRewriteRule(lemma
.negate(), rewritten
.negate());
222 proofStep
.addAssertion(lemma
);
223 proofRecipe
.addBaseAssertion(rewritten
);
225 proofRecipe
.addStep(proofStep
);
226 ProofManager::getCnfProof()->setProofRecipe(&proofRecipe
);
229 theory::LemmaStatus
EngineOutputChannel::splitLemma(TNode lemma
, bool removable
)
231 Debug("theory::lemma") << "EngineOutputChannel<" << d_theory
<< ">::lemma("
232 << lemma
<< ")" << std::endl
;
233 ++d_statistics
.lemmas
;
234 d_engine
->d_outputChannelUsed
= true;
236 Debug("pf::explain") << "EngineOutputChannel::splitLemma( " << lemma
<< " )"
238 TrustNode tlem
= TrustNode::mkTrustLemma(lemma
);
239 LemmaProperty p
= removable
? LemmaProperty::REMOVABLE
: LemmaProperty::NONE
;
240 theory::LemmaStatus result
=
241 d_engine
->lemma(tlem
.getNode(), RULE_SPLIT
, false, p
, d_theory
);
245 bool EngineOutputChannel::propagate(TNode literal
)
247 Debug("theory::propagate") << "EngineOutputChannel<" << d_theory
248 << ">::propagate(" << literal
<< ")" << std::endl
;
249 ++d_statistics
.propagations
;
250 d_engine
->d_outputChannelUsed
= true;
251 return d_engine
->propagate(literal
, d_theory
);
254 void EngineOutputChannel::conflict(TNode conflictNode
,
255 std::unique_ptr
<Proof
> proof
)
257 Trace("theory::conflict")
258 << "EngineOutputChannel<" << d_theory
<< ">::conflict(" << conflictNode
260 Assert(!proof
); // Theory shouldn't be producing proofs yet
261 ++d_statistics
.conflicts
;
262 d_engine
->d_outputChannelUsed
= true;
263 TrustNode tConf
= TrustNode::mkTrustConflict(conflictNode
);
264 d_engine
->conflict(tConf
.getNode(), d_theory
);
267 void EngineOutputChannel::demandRestart()
269 NodeManager
* curr
= NodeManager::currentNM();
270 Node restartVar
= curr
->mkSkolem(
273 "A boolean variable asserted to be true to force a restart");
274 Trace("theory::restart") << "EngineOutputChannel<" << d_theory
275 << ">::restart(" << restartVar
<< ")" << std::endl
;
276 ++d_statistics
.restartDemands
;
277 lemma(restartVar
, RULE_INVALID
, LemmaProperty::REMOVABLE
);
280 void EngineOutputChannel::requirePhase(TNode n
, bool phase
)
282 Debug("theory") << "EngineOutputChannel::requirePhase(" << n
<< ", " << phase
284 ++d_statistics
.requirePhase
;
285 d_engine
->getPropEngine()->requirePhase(n
, phase
);
288 void EngineOutputChannel::setIncomplete()
290 Trace("theory") << "setIncomplete()" << std::endl
;
291 d_engine
->setIncomplete(d_theory
);
294 void EngineOutputChannel::spendResource(ResourceManager::Resource r
)
296 d_engine
->spendResource(r
);
299 void EngineOutputChannel::handleUserAttribute(const char* attr
,
302 d_engine
->handleUserAttribute(attr
, t
);
305 void EngineOutputChannel::trustedConflict(TrustNode pconf
)
307 Assert(pconf
.getKind() == TrustNodeKind::CONFLICT
);
308 Trace("theory::conflict")
309 << "EngineOutputChannel<" << d_theory
<< ">::conflict(" << pconf
.getNode()
311 if (pconf
.getGenerator() != nullptr)
313 ++d_statistics
.trustedConflicts
;
315 ++d_statistics
.conflicts
;
316 d_engine
->d_outputChannelUsed
= true;
317 d_engine
->conflict(pconf
.getNode(), d_theory
);
320 LemmaStatus
EngineOutputChannel::trustedLemma(TrustNode plem
, LemmaProperty p
)
322 Assert(plem
.getKind() == TrustNodeKind::LEMMA
);
323 if (plem
.getGenerator() != nullptr)
325 ++d_statistics
.trustedLemmas
;
327 ++d_statistics
.lemmas
;
328 d_engine
->d_outputChannelUsed
= true;
329 // now, call the normal interface for lemma
330 return d_engine
->lemma(
335 isLemmaPropertySendAtoms(p
) ? d_theory
: theory::THEORY_LAST
);
338 } // namespace theory