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 isLemmaPropertyPreprocess(LemmaProperty p)
  45 {
  46   return (p & LemmaProperty::PREPROCESS) != LemmaProperty::NONE;
  47 }
  48 bool isLemmaPropertySendAtoms(LemmaProperty p)
  49 {
  50   return (p & LemmaProperty::SEND_ATOMS) != LemmaProperty::NONE;
  51 }
  52 bool isLemmaPropertyNeedsJustify(LemmaProperty p)
  53 {
  54   return (p & LemmaProperty::NEEDS_JUSTIFY) != LemmaProperty::NONE;
  55 }
  56
  57 std::ostream& operator<<(std::ostream& out, LemmaProperty p)
  58 {
  59   if (p == LemmaProperty::NONE)
  60   {
  61     out << "NONE";
  62   }
  63   else
  64   {
  65     out << "{";
  66     if (isLemmaPropertyRemovable(p))
  67     {
  68       out << " REMOVABLE";
  69     }
  70     if (isLemmaPropertyPreprocess(p))
  71     {
  72       out << " PREPROCESS";
  73     }
  74     if (isLemmaPropertySendAtoms(p))
  75     {
  76       out << " SEND_ATOMS";
  77     }
  78     if (isLemmaPropertyNeedsJustify(p))
  79     {
  80       out << " NEEDS_JUSTIFY";
  81     }
  82     out << " }";
  83   }
  84   return out;
  85 }
  86
  87 LemmaStatus::LemmaStatus(TNode rewrittenLemma, unsigned level)
  88     : d_rewrittenLemma(rewrittenLemma), d_level(level)
  89 {
  90 }
  91
  92 TNode LemmaStatus::getRewrittenLemma() const { return d_rewrittenLemma; }
  93
  94 unsigned LemmaStatus::getLevel() const { return d_level; }
  95
  96 LemmaStatus OutputChannel::split(TNode n)
  97 {
  98   return splitLemma(n.orNode(n.notNode()));
  99 }
 100
 101 void OutputChannel::trustedConflict(TrustNode pconf)
 102 {
 103   Unreachable() << "OutputChannel::trustedConflict: no implementation"
 104                 << std::endl;
 105 }
 106
 107 LemmaStatus OutputChannel::trustedLemma(TrustNode lem, LemmaProperty p)
 108 {
 109   Unreachable() << "OutputChannel::trustedLemma: no implementation"
 110                 << std::endl;
 111 }
 112
 113 }  // namespace theory
 114 }  // namespace CVC4