GCC Code Coverage Report
Directory: . Exec Total Coverage
File: src/expr/node_value.cpp Lines: 11 33 33.3 %
Date: 2021-03-22 Branches: 13 82 15.9 %

Line Exec Source
1
/*********************                                                        */
2
/*! \file node_value.cpp
3
 ** \verbatim
4
 ** Top contributors (to current version):
5
 **   Morgan Deters, Aina Niemetz, 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 An expression node.
13
 **
14
 ** An expression node.
15
 **
16
 ** Instances of this class are generally referenced through
17
 ** cvc4::Node rather than by pointer; cvc4::Node maintains the
18
 ** reference count on NodeValue instances and
19
 **/
20
#include "expr/node_value.h"
21
22
#include <sstream>
23
24
#include "expr/kind.h"
25
#include "expr/metakind.h"
26
#include "expr/node.h"
27
#include "options/base_options.h"
28
#include "options/language.h"
29
#include "options/options.h"
30
#include "printer/printer.h"
31
32
using namespace std;
33
34
namespace CVC4 {
35
namespace expr {
36
37
567026
string NodeValue::toString() const {
38
1134052
  stringstream ss;
39
40
1134052
  OutputLanguage outlang = (this == &null()) ? language::output::LANG_AUTO
41
1134052
                                             : options::outputLanguage();
42
567026
  toStream(ss, -1, false, outlang);
43
1134052
  return ss.str();
44
}
45
46
662817
void NodeValue::toStream(std::ostream& out,
47
                         int toDepth,
48
                         size_t dag,
49
                         OutputLanguage language) const
50
{
51
  // Ensure that this node value is live for the length of this call.
52
  // It really breaks things badly if we don't have a nonzero ref
53
  // count, even just for printing.
54
1325634
  RefCountGuard guard(this);
55
56
662831
  Printer::getPrinter(language)->toStream(out, TNode(this), toDepth, dag);
57
662803
}
58
59
void NodeValue::printAst(std::ostream& out, int ind) const {
60
  RefCountGuard guard(this);
61
62
  indent(out, ind);
63
  out << '(';
64
  out << getKind();
65
  if (getMetaKind() == kind::metakind::VARIABLE || getMetaKind() == kind::metakind::NULLARY_OPERATOR ) {
66
    out << ' ' << getId();
67
  } else if (getMetaKind() == kind::metakind::CONSTANT) {
68
    out << ' ';
69
    kind::metakind::NodeValueConstPrinter::toStream(out, this);
70
  } else {
71
    if (nv_begin() != nv_end()) {
72
      for (const_nv_iterator child = nv_begin(); child != nv_end(); ++child) {
73
        out << std::endl;
74
        (*child)->printAst(out, ind + 1);
75
      }
76
      out << std::endl;
77
      indent(out, ind);
78
    }
79
  }
80
  out << ')';
81
}
82
83
NodeValue::iterator<NodeTemplate<true> > operator+(
84
    NodeValue::iterator<NodeTemplate<true> >::difference_type p,
85
    NodeValue::iterator<NodeTemplate<true> > i)
86
{
87
  return i + p;
88
}
89
90
NodeValue::iterator<NodeTemplate<false> > operator+(
91
    NodeValue::iterator<NodeTemplate<false> >::difference_type p,
92
    NodeValue::iterator<NodeTemplate<false> > i)
93
{
94
  return i + p;
95
}
96
97
} /* CVC4::expr namespace */
98
26676
} /* CVC4 namespace */