diff options
author | Guy <katz911@gmail.com> | 2016-06-01 17:41:17 -0700 |
---|---|---|
committer | Guy <katz911@gmail.com> | 2016-06-01 17:41:17 -0700 |
commit | de0dd1dc966b05467f1a5443ff33094262f5076a (patch) | |
tree | 46a8539229fc31226b416755e6a88c18476ecffc /src/proof/proof_output_channel.cpp | |
parent | 89ba584531115b7f6d47088d7614368ea05ab9d8 (diff) |
Revert "Merging proof branch"
This reverts commit 89ba584531115b7f6d47088d7614368ea05ab9d8.
Diffstat (limited to 'src/proof/proof_output_channel.cpp')
-rw-r--r-- | src/proof/proof_output_channel.cpp | 82 |
1 files changed, 0 insertions, 82 deletions
diff --git a/src/proof/proof_output_channel.cpp b/src/proof/proof_output_channel.cpp deleted file mode 100644 index 6d729db1f..000000000 --- a/src/proof/proof_output_channel.cpp +++ /dev/null @@ -1,82 +0,0 @@ -/********************* */ -/*! \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 */ |