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