Revert "Merging proof branch"

This reverts commit 89ba584531115b7f6d47088d7614368ea05ab9d8.

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 */