src/theory/output_channel.cpp

   1 /*********************                                                        */
   2 /*! \file output_channel.cpp
   3  ** \verbatim
   4  ** Top contributors (to current version):
   5  **   Andrew Reynolds
   6  ** This file is part of the CVC4 project.
   7  ** Copyright (c) 2009-2020 by the authors listed in the file AUTHORS
   8  ** in the top-level source directory and their institutional affiliations.
   9  ** All rights reserved.  See the file COPYING in the top-level source
  10  ** directory for licensing information.\endverbatim
  11  **
  12  ** \brief The theory output channel interface
  13  **/
  14
  15 #include "theory/output_channel.h"
  16
  17 namespace CVC4 {
  18 namespace theory {
  19
  20 LemmaProperty operator|(LemmaProperty lhs, LemmaProperty rhs)
  21 {
  22   return static_cast<LemmaProperty>(static_cast<uint32_t>(lhs)
  23                                     | static_cast<uint32_t>(rhs));
  24 }
  25 LemmaProperty& operator|=(LemmaProperty& lhs, LemmaProperty rhs)
  26 {
  27   lhs = lhs | rhs;
  28   return lhs;
  29 }
  30 LemmaProperty operator&(LemmaProperty lhs, LemmaProperty rhs)
  31 {
  32   return static_cast<LemmaProperty>(static_cast<uint32_t>(lhs)
  33                                     & static_cast<uint32_t>(rhs));
  34 }
  35 LemmaProperty& operator&=(LemmaProperty& lhs, LemmaProperty rhs)
  36 {
  37   lhs = lhs & rhs;
  38   return lhs;
  39 }
  40 bool isLemmaPropertyRemovable(LemmaProperty p)
  41 {
  42   return (p & LemmaProperty::REMOVABLE) != LemmaProperty::NONE;
  43 }
  44 bool isLemmaPropertySendAtoms(LemmaProperty p)
  45 {
  46   return (p & LemmaProperty::SEND_ATOMS) != LemmaProperty::NONE;
  47 }
  48 bool isLemmaPropertyNeedsJustify(LemmaProperty p)
  49 {
  50   return (p & LemmaProperty::NEEDS_JUSTIFY) != LemmaProperty::NONE;
  51 }
  52
  53 std::ostream& operator<<(std::ostream& out, LemmaProperty p)
  54 {
  55   if (p == LemmaProperty::NONE)
  56   {
  57     out << "NONE";
  58   }
  59   else
  60   {
  61     out << "{";
  62     if (isLemmaPropertyRemovable(p))
  63     {
  64       out << " REMOVABLE";
  65     }
  66     if (isLemmaPropertySendAtoms(p))
  67     {
  68       out << " SEND_ATOMS";
  69     }
  70     if (isLemmaPropertyNeedsJustify(p))
  71     {
  72       out << " NEEDS_JUSTIFY";
  73     }
  74     out << " }";
  75   }
  76   return out;
  77 }
  78
  79 void OutputChannel::split(TNode n) { splitLemma(n.orNode(n.notNode())); }
  80
  81 void OutputChannel::trustedConflict(TrustNode pconf)
  82 {
  83   Unreachable() << "OutputChannel::trustedConflict: no implementation"
  84                 << std::endl;
  85 }
  86
  87 void OutputChannel::trustedLemma(TrustNode lem, LemmaProperty p)
  88 {
  89   Unreachable() << "OutputChannel::trustedLemma: no implementation"
  90                 << std::endl;
  91 }
  92
  93 }  // namespace theory
  94 }  // namespace CVC4