GCC Code Coverage Report
Directory: . Exec Total Coverage
File: src/theory/output_channel.cpp Lines: 15 36 41.7 %
Date: 2021-03-23 Branches: 5 36 13.9 %

Line Exec Source
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-2021 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
1281
LemmaProperty operator|(LemmaProperty lhs, LemmaProperty rhs)
21
{
22
  return static_cast<LemmaProperty>(static_cast<uint32_t>(lhs)
23
1281
                                    | static_cast<uint32_t>(rhs));
24
}
25
1281
LemmaProperty& operator|=(LemmaProperty& lhs, LemmaProperty rhs)
26
{
27
1281
  lhs = lhs | rhs;
28
1281
  return lhs;
29
}
30
741040
LemmaProperty operator&(LemmaProperty lhs, LemmaProperty rhs)
31
{
32
  return static_cast<LemmaProperty>(static_cast<uint32_t>(lhs)
33
741040
                                    & static_cast<uint32_t>(rhs));
34
}
35
LemmaProperty& operator&=(LemmaProperty& lhs, LemmaProperty rhs)
36
{
37
  lhs = lhs & rhs;
38
  return lhs;
39
}
40
461320
bool isLemmaPropertyRemovable(LemmaProperty p)
41
{
42
461320
  return (p & LemmaProperty::REMOVABLE) != LemmaProperty::NONE;
43
}
44
279506
bool isLemmaPropertySendAtoms(LemmaProperty p)
45
{
46
279506
  return (p & LemmaProperty::SEND_ATOMS) != LemmaProperty::NONE;
47
}
48
214
bool isLemmaPropertyNeedsJustify(LemmaProperty p)
49
{
50
214
  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
2
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
26685
}  // namespace CVC4