1 |
|
/****************************************************************************** |
2 |
|
* Top contributors (to current version): |
3 |
|
* 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 |
|
* Simple substitution utility. |
14 |
|
*/ |
15 |
|
|
16 |
|
#include "expr/subs.h" |
17 |
|
|
18 |
|
#include <sstream> |
19 |
|
|
20 |
|
#include "expr/skolem_manager.h" |
21 |
|
#include "theory/rewriter.h" |
22 |
|
|
23 |
|
namespace cvc5 { |
24 |
|
|
25 |
12947 |
bool Subs::empty() const { return d_vars.empty(); } |
26 |
|
|
27 |
853 |
size_t Subs::size() const { return d_vars.size(); } |
28 |
|
|
29 |
6623 |
bool Subs::contains(Node v) const |
30 |
|
{ |
31 |
6623 |
return std::find(d_vars.begin(), d_vars.end(), v) != d_vars.end(); |
32 |
|
} |
33 |
|
|
34 |
|
Node Subs::getSubs(Node v) const |
35 |
|
{ |
36 |
|
std::vector<Node>::const_iterator it = |
37 |
|
std::find(d_vars.begin(), d_vars.end(), v); |
38 |
|
if (it == d_vars.end()) |
39 |
|
{ |
40 |
|
return Node::null(); |
41 |
|
} |
42 |
|
size_t i = std::distance(d_vars.begin(), it); |
43 |
|
Assert(i < d_subs.size()); |
44 |
|
return d_subs[i]; |
45 |
|
} |
46 |
|
|
47 |
40839 |
std::optional<Node> Subs::find(TNode v) const |
48 |
|
{ |
49 |
40839 |
auto it = std::find(d_vars.begin(), d_vars.end(), v); |
50 |
40839 |
if (it == d_vars.end()) |
51 |
|
{ |
52 |
32186 |
return {}; |
53 |
|
} |
54 |
8653 |
return d_subs[std::distance(d_vars.begin(), it)]; |
55 |
|
} |
56 |
|
|
57 |
29 |
void Subs::add(Node v) |
58 |
|
{ |
59 |
29 |
SkolemManager* sm = NodeManager::currentNM()->getSkolemManager(); |
60 |
|
// default, use a fresh skolem of the same type |
61 |
58 |
Node s = sm->mkDummySkolem("sk", v.getType()); |
62 |
29 |
add(v, s); |
63 |
29 |
} |
64 |
|
|
65 |
19 |
void Subs::add(const std::vector<Node>& vs) |
66 |
|
{ |
67 |
48 |
for (const Node& v : vs) |
68 |
|
{ |
69 |
29 |
add(v); |
70 |
|
} |
71 |
19 |
} |
72 |
|
|
73 |
7732 |
void Subs::add(Node v, Node s) |
74 |
|
{ |
75 |
7732 |
Assert(s.isNull() || v.getType().isComparableTo(s.getType())); |
76 |
7732 |
d_vars.push_back(v); |
77 |
7732 |
d_subs.push_back(s); |
78 |
7732 |
} |
79 |
|
|
80 |
542 |
void Subs::add(const std::vector<Node>& vs, const std::vector<Node>& ss) |
81 |
|
{ |
82 |
542 |
Assert(vs.size() == ss.size()); |
83 |
1464 |
for (size_t i = 0, nvs = vs.size(); i < nvs; i++) |
84 |
|
{ |
85 |
922 |
add(vs[i], ss[i]); |
86 |
|
} |
87 |
542 |
} |
88 |
|
|
89 |
|
void Subs::addEquality(Node eq) |
90 |
|
{ |
91 |
|
Assert(eq.getKind() == kind::EQUAL); |
92 |
|
add(eq[0], eq[1]); |
93 |
|
} |
94 |
|
|
95 |
|
void Subs::append(Subs& s) |
96 |
|
{ |
97 |
|
// add the substitution list |
98 |
|
add(s.d_vars, s.d_subs); |
99 |
|
} |
100 |
|
|
101 |
4061 |
Node Subs::apply(Node n, bool doRewrite) const |
102 |
|
{ |
103 |
4061 |
if (d_vars.empty()) |
104 |
|
{ |
105 |
994 |
return n; |
106 |
|
} |
107 |
|
Node ns = |
108 |
6134 |
n.substitute(d_vars.begin(), d_vars.end(), d_subs.begin(), d_subs.end()); |
109 |
3067 |
if (doRewrite) |
110 |
|
{ |
111 |
|
ns = theory::Rewriter::rewrite(ns); |
112 |
|
} |
113 |
3067 |
return ns; |
114 |
|
} |
115 |
19 |
Node Subs::rapply(Node n, bool doRewrite) const |
116 |
|
{ |
117 |
19 |
if (d_vars.empty()) |
118 |
|
{ |
119 |
|
return n; |
120 |
|
} |
121 |
|
Node ns = |
122 |
38 |
n.substitute(d_subs.begin(), d_subs.end(), d_vars.begin(), d_vars.end()); |
123 |
19 |
if (doRewrite) |
124 |
|
{ |
125 |
19 |
ns = theory::Rewriter::rewrite(ns); |
126 |
|
} |
127 |
19 |
return ns; |
128 |
|
} |
129 |
|
|
130 |
|
void Subs::applyToRange(Subs& s, bool doRewrite) const |
131 |
|
{ |
132 |
|
if (d_vars.empty()) |
133 |
|
{ |
134 |
|
return; |
135 |
|
} |
136 |
|
for (size_t i = 0, ns = s.d_subs.size(); i < ns; i++) |
137 |
|
{ |
138 |
|
s.d_subs[i] = apply(s.d_subs[i], doRewrite); |
139 |
|
} |
140 |
|
} |
141 |
|
|
142 |
|
void Subs::rapplyToRange(Subs& s, bool doRewrite) const |
143 |
|
{ |
144 |
|
if (d_vars.empty()) |
145 |
|
{ |
146 |
|
return; |
147 |
|
} |
148 |
|
for (size_t i = 0, ns = s.d_subs.size(); i < ns; i++) |
149 |
|
{ |
150 |
|
s.d_subs[i] = rapply(s.d_subs[i], doRewrite); |
151 |
|
} |
152 |
|
} |
153 |
|
|
154 |
|
Node Subs::getEquality(size_t i) const |
155 |
|
{ |
156 |
|
Assert(i < d_vars.size()); |
157 |
|
return d_vars[i].eqNode(d_subs[i]); |
158 |
|
} |
159 |
|
|
160 |
|
std::map<Node, Node> Subs::toMap() const |
161 |
|
{ |
162 |
|
std::map<Node, Node> ret; |
163 |
|
for (size_t i = 0, nvs = d_vars.size(); i < nvs; i++) |
164 |
|
{ |
165 |
|
ret[d_vars[i]] = d_subs[i]; |
166 |
|
} |
167 |
|
return ret; |
168 |
|
} |
169 |
|
|
170 |
|
std::string Subs::toString() const |
171 |
|
{ |
172 |
|
std::stringstream ss; |
173 |
|
ss << "["; |
174 |
|
for (size_t i = 0, nvs = d_vars.size(); i < nvs; i++) |
175 |
|
{ |
176 |
|
if (i > 0) |
177 |
|
{ |
178 |
|
ss << " "; |
179 |
|
} |
180 |
|
ss << d_vars[i] << " -> " << d_subs[i]; |
181 |
|
} |
182 |
|
ss << "]"; |
183 |
|
return ss.str(); |
184 |
|
} |
185 |
|
|
186 |
6381 |
void Subs::clear() |
187 |
|
{ |
188 |
6381 |
d_vars.clear(); |
189 |
6381 |
d_subs.clear(); |
190 |
6381 |
} |
191 |
|
|
192 |
|
std::ostream& operator<<(std::ostream& out, const Subs& s) |
193 |
|
{ |
194 |
|
out << s.toString(); |
195 |
|
return out; |
196 |
|
} |
197 |
|
|
198 |
31137 |
} // namespace cvc5 |