GCC Code Coverage Report
Directory: . Exec Total Coverage
File: src/smt/node_command.cpp Lines: 36 56 64.3 %
Date: 2021-03-22 Branches: 30 88 34.1 %

Line Exec Source
1
/*********************                                                        */
2
/*! \file node_command.cpp
3
 ** \verbatim
4
 ** Top contributors (to current version):
5
 **   Abdalrhman Mohamed, Yoni Zohar, 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 Implementation of NodeCommand functions.
13
 **
14
 ** Implementation of NodeCommand functions.
15
 **/
16
17
#include "smt/node_command.h"
18
19
#include <sstream>
20
21
#include "printer/printer.h"
22
23
namespace CVC4 {
24
25
/* -------------------------------------------------------------------------- */
26
/* class NodeCommand                                                          */
27
/* -------------------------------------------------------------------------- */
28
29
283295
NodeCommand::~NodeCommand() {}
30
31
std::string NodeCommand::toString() const
32
{
33
  std::stringstream ss;
34
  toStream(ss);
35
  return ss.str();
36
}
37
38
12
std::ostream& operator<<(std::ostream& out, const NodeCommand& nc)
39
{
40
24
  nc.toStream(out,
41
12
              Node::setdepth::getDepth(out),
42
              Node::dag::getDag(out),
43
12
              Node::setlanguage::getLanguage(out));
44
12
  return out;
45
}
46
47
/* -------------------------------------------------------------------------- */
48
/* class DeclareFunctionNodeCommand                                           */
49
/* -------------------------------------------------------------------------- */
50
51
268573
DeclareFunctionNodeCommand::DeclareFunctionNodeCommand(const std::string& id,
52
                                                       Node expr,
53
268573
                                                       TypeNode type)
54
    : d_id(id),
55
      d_fun(expr),
56
268573
      d_type(type)
57
{
58
268573
}
59
60
10
void DeclareFunctionNodeCommand::toStream(std::ostream& out,
61
                                          int toDepth,
62
                                          size_t dag,
63
                                          OutputLanguage language) const
64
{
65
10
  Printer::getPrinter(language)->toStreamCmdDeclareFunction(out, d_id, d_type);
66
10
}
67
68
8
NodeCommand* DeclareFunctionNodeCommand::clone() const
69
{
70
8
  return new DeclareFunctionNodeCommand(d_id, d_fun, d_type);
71
}
72
73
const Node& DeclareFunctionNodeCommand::getFunction() const { return d_fun; }
74
75
/* -------------------------------------------------------------------------- */
76
/* class DeclareTypeNodeCommand                                               */
77
/* -------------------------------------------------------------------------- */
78
79
9170
DeclareTypeNodeCommand::DeclareTypeNodeCommand(const std::string& id,
80
                                               size_t arity,
81
9170
                                               TypeNode type)
82
9170
    : d_id(id), d_arity(arity), d_type(type)
83
{
84
9170
}
85
86
void DeclareTypeNodeCommand::toStream(std::ostream& out,
87
                                      int toDepth,
88
                                      size_t dag,
89
                                      OutputLanguage language) const
90
{
91
  Printer::getPrinter(language)->toStreamCmdDeclareType(out, d_type);
92
}
93
94
NodeCommand* DeclareTypeNodeCommand::clone() const
95
{
96
  return new DeclareTypeNodeCommand(d_id, d_arity, d_type);
97
}
98
99
const std::string DeclareTypeNodeCommand::getSymbol() const { return d_id; }
100
101
const TypeNode& DeclareTypeNodeCommand::getType() const { return d_type; }
102
103
/* -------------------------------------------------------------------------- */
104
/* class DeclareDatatypeNodeCommand                                           */
105
/* -------------------------------------------------------------------------- */
106
107
2854
DeclareDatatypeNodeCommand::DeclareDatatypeNodeCommand(
108
2854
    const std::vector<TypeNode>& datatypes)
109
2854
    : d_datatypes(datatypes)
110
{
111
2854
}
112
113
void DeclareDatatypeNodeCommand::toStream(std::ostream& out,
114
                                          int toDepth,
115
                                          size_t dag,
116
                                          OutputLanguage language) const
117
{
118
  Printer::getPrinter(language)->toStreamCmdDatatypeDeclaration(out,
119
                                                                d_datatypes);
120
}
121
122
NodeCommand* DeclareDatatypeNodeCommand::clone() const
123
{
124
  return new DeclareDatatypeNodeCommand(d_datatypes);
125
}
126
127
/* -------------------------------------------------------------------------- */
128
/* class DefineFunctionNodeCommand                                            */
129
/* -------------------------------------------------------------------------- */
130
131
2698
DefineFunctionNodeCommand::DefineFunctionNodeCommand(
132
    const std::string& id,
133
    Node fun,
134
    const std::vector<Node>& formals,
135
2698
    Node formula)
136
2698
    : d_id(id), d_fun(fun), d_formals(formals), d_formula(formula)
137
{
138
2698
}
139
140
2
void DefineFunctionNodeCommand::toStream(std::ostream& out,
141
                                         int toDepth,
142
                                         size_t dag,
143
                                         OutputLanguage language) const
144
{
145
4
  TypeNode tn = d_fun.getType();
146
  bool hasRange =
147
2
      (tn.isFunction() || tn.isConstructor() || tn.isSelector());
148
10
  Printer::getPrinter(language)->toStreamCmdDefineFunction(
149
      out,
150
4
      d_fun.toString(),
151
      d_formals,
152
4
      (hasRange ? d_fun.getType().getRangeType() : tn),
153
2
      d_formula);
154
2
}
155
156
NodeCommand* DefineFunctionNodeCommand::clone() const
157
{
158
  return new DefineFunctionNodeCommand(d_id, d_fun, d_formals, d_formula);
159
}
160
161
26676
}  // namespace CVC4