Merge from proof branch

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