diff options
Diffstat (limited to 'src/proof/proof_output_channel.cpp')
-rw-r--r-- | src/proof/proof_output_channel.cpp | 82 |
1 files changed, 82 insertions, 0 deletions
diff --git a/src/proof/proof_output_channel.cpp b/src/proof/proof_output_channel.cpp new file mode 100644 index 000000000..6d729db1f --- /dev/null +++ b/src/proof/proof_output_channel.cpp @@ -0,0 +1,82 @@ +/********************* */ +/*! \file proof_output_channel.cpp +** \verbatim +** \brief [[ Add one-line brief description here ]] +** +** [[ Add lengthier description here ]] +** \todo document this file +**/ + +#include "base/cvc4_assert.h" +#include "proof_output_channel.h" +#include "theory/term_registration_visitor.h" +#include "theory/valuation.h" + +namespace CVC4 { + +ProofOutputChannel::ProofOutputChannel() : d_conflict(), d_proof(NULL) {} + +void ProofOutputChannel::conflict(TNode n, Proof* pf) throw() { + Trace("pf::tp") << "ProofOutputChannel: CONFLICT: " << n << std::endl; + Assert(d_conflict.isNull()); + Assert(!n.isNull()); + d_conflict = n; + Assert(pf != NULL); + d_proof = pf; +} + +bool ProofOutputChannel::propagate(TNode x) throw() { + Trace("pf::tp") << "ProofOutputChannel: got a propagation: " << x << std::endl; + d_propagations.insert(x); + return true; +} + +theory::LemmaStatus ProofOutputChannel::lemma(TNode n, ProofRule rule, bool, bool, bool) throw() { + Trace("pf::tp") << "ProofOutputChannel: new lemma: " << n << std::endl; + d_lemma = n; + return theory::LemmaStatus(TNode::null(), 0); +} + +theory::LemmaStatus ProofOutputChannel::splitLemma(TNode, bool) throw() { + AlwaysAssert(false); + return theory::LemmaStatus(TNode::null(), 0); +} + +void ProofOutputChannel::requirePhase(TNode n, bool b) throw() { + Debug("pf::tp") << "ProofOutputChannel::requirePhase called" << std::endl; + Trace("pf::tp") << "requirePhase " << n << " " << b << std::endl; +} + +bool ProofOutputChannel::flipDecision() throw() { + Debug("pf::tp") << "ProofOutputChannel::flipDecision called" << std::endl; + AlwaysAssert(false); + return false; +} + +void ProofOutputChannel::setIncomplete() throw() { + Debug("pf::tp") << "ProofOutputChannel::setIncomplete called" << std::endl; + AlwaysAssert(false); +} + + +MyPreRegisterVisitor::MyPreRegisterVisitor(theory::Theory* theory) + : d_theory(theory) + , d_visited() { +} + +bool MyPreRegisterVisitor::alreadyVisited(TNode current, TNode parent) { + return d_visited.find(current) != d_visited.end(); +} + +void MyPreRegisterVisitor::visit(TNode current, TNode parent) { + d_theory->preRegisterTerm(current); + d_visited.insert(current); +} + +void MyPreRegisterVisitor::start(TNode node) { +} + +void MyPreRegisterVisitor::done(TNode node) { +} + +} /* namespace CVC4 */ |