1 files changed, 111 insertions, 0 deletions
diff --git a/src/theory/output_channel.cpp b/src/theory/output_channel.cpp
new file mode 100644
index 000000000..9fe973569
--- /dev/null
+++ b/src/theory/output_channel.cpp
@@ -0,0 +1,111 @@
+/*********************                                                        */
+/*! \file output_channel.h
+ ** \verbatim
+ ** Top contributors (to current version):
+ **   Andrew Reynolds
+ ** This file is part of the CVC4 project.
+ ** Copyright (c) 2009-2020 by the authors listed in the file AUTHORS
+ ** in the top-level source directory) and their institutional affiliations.
+ ** All rights reserved.  See the file COPYING in the top-level source
+ ** directory for licensing information.\endverbatim
+ **
+ ** \brief The theory output channel interface
+ **/
+
+#include "theory/output_channel.h"
+
+namespace CVC4 {
+namespace theory {
+
+LemmaProperty operator|(LemmaProperty lhs, LemmaProperty rhs)
+{
+  return static_cast<LemmaProperty>(static_cast<uint32_t>(lhs)
+                                    | static_cast<uint32_t>(rhs));
+}
+LemmaProperty& operator|=(LemmaProperty& lhs, LemmaProperty rhs)
+{
+  lhs = lhs | rhs;
+  return lhs;
+}
+LemmaProperty operator&(LemmaProperty lhs, LemmaProperty rhs)
+{
+  return static_cast<LemmaProperty>(static_cast<uint32_t>(lhs)
+                                    & static_cast<uint32_t>(rhs));
+}
+LemmaProperty& operator&=(LemmaProperty& lhs, LemmaProperty rhs)
+{
+  lhs = lhs & rhs;
+  return lhs;
+}
+bool isLemmaPropertyRemovable(LemmaProperty p)
+{
+  return (p & LemmaProperty::REMOVABLE) != LemmaProperty::NONE;
+}
+bool isLemmaPropertyPreprocess(LemmaProperty p)
+{
+  return (p & LemmaProperty::PREPROCESS) != LemmaProperty::NONE;
+}
+bool isLemmaPropertySendAtoms(LemmaProperty p)
+{
+  return (p & LemmaProperty::SEND_ATOMS) != LemmaProperty::NONE;
+}
+
+std::ostream& operator<<(std::ostream& out, LemmaProperty p)
+{
+  if (p == LemmaProperty::NONE)
+  {
+    out << "NONE";
+  }
+  else
+  {
+    out << "{";
+    if (isLemmaPropertyRemovable(p))
+    {
+      out << " REMOVABLE";
+    }
+    if (isLemmaPropertyPreprocess(p))
+    {
+      out << " PREPROCESS";
+    }
+    if (isLemmaPropertySendAtoms(p))
+    {
+      out << " SEND_ATOMS";
+    }
+    out << " }";
+  }
+  return out;
+}
+
+LemmaStatus::LemmaStatus(TNode rewrittenLemma, unsigned level)
+    : d_rewrittenLemma(rewrittenLemma), d_level(level)
+{
+}
+
+TNode LemmaStatus::getRewrittenLemma() const { return d_rewrittenLemma; }
+
+unsigned LemmaStatus::getLevel() const { return d_level; }
+
+LemmaStatus OutputChannel::lemma(TNode n, LemmaProperty p)
+{
+  return lemma(n, RULE_INVALID, p);
+}
+
+LemmaStatus OutputChannel::split(TNode n)
+{
+  return splitLemma(n.orNode(n.notNode()));
+}
+
+void OutputChannel::trustedConflict(TrustNode pconf)
+{
+  Unreachable() << "OutputChannel::trustedConflict: no implementation"
+                << std::endl;
+}
+
+LemmaStatus OutputChannel::trustedLemma(TrustNode lem, LemmaProperty p)
+{
+  Unreachable() << "OutputChannel::trustedLemma: no implementation"
+                << std::endl;
+}
+
+}  // namespace theory
+}  // namespace CVC4