GCC Code Coverage Report
Directory: . Exec Total Coverage
File: src/expr/dtype_selector.cpp Lines: 27 33 81.8 %
Date: 2021-03-22 Branches: 27 110 24.5 %

Line Exec Source
1
/*********************                                                        */
2
/*! \file dtype_selector.cpp
3
 ** \verbatim
4
 ** Top contributors (to current version):
5
 **   Andrew Reynolds, Tim King, Morgan Deters
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 A class representing a datatype selector.
13
 **/
14
15
#include "expr/dtype_selector.h"
16
17
#include "options/set_language.h"
18
19
using namespace CVC4::kind;
20
21
namespace CVC4 {
22
23
20029
DTypeSelector::DTypeSelector(std::string name, Node selector)
24
20029
    : d_name(name), d_selector(selector), d_resolved(false)
25
{
26
20029
  Assert(name != "");
27
20029
}
28
29
2766
const std::string& DTypeSelector::getName() const { return d_name; }
30
31
1177973
Node DTypeSelector::getSelector() const
32
{
33
1177973
  Assert(d_resolved);
34
1177973
  return d_selector;
35
}
36
37
Node DTypeSelector::getConstructor() const
38
{
39
  Assert(d_resolved);
40
  return d_constructor;
41
}
42
43
1040170
TypeNode DTypeSelector::getType() const { return d_selector.getType(); }
44
45
159082
TypeNode DTypeSelector::getRangeType() const
46
{
47
159082
  return getType().getRangeType();
48
}
49
50
22481
bool DTypeSelector::isResolved() const { return d_resolved; }
51
52
34
void DTypeSelector::toStream(std::ostream& out) const
53
{
54
34
  out << getName() << ": ";
55
34
  TypeNode t;
56
34
  if (d_resolved)
57
  {
58
    // don't try to print the range type of null, instead we print null itself.
59
    if (!getType().isNull())
60
    {
61
      t = getRangeType();
62
    }
63
  }
64
34
  else if (d_selector.isNull())
65
  {
66
44
    std::string typeName = d_name.substr(d_name.find('\0') + 1);
67
22
    out << ((typeName == "") ? "[self]" : typeName);
68
22
    return;
69
  }
70
  else
71
  {
72
12
    out << "unresolved";
73
12
    return;
74
  }
75
  out << t;
76
}
77
78
34
std::ostream& operator<<(std::ostream& os, const DTypeSelector& arg)
79
{
80
  // can only output datatypes in the CVC4 native language
81
68
  language::SetLanguage::Scope ls(os, language::output::LANG_CVC4);
82
34
  arg.toStream(os);
83
68
  return os;
84
}
85
86
26676
}  // namespace CVC4