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 |
75 |
bool Subs::empty() const { return d_vars.empty(); } |
26 |
|
|
27 |
|
size_t Subs::size() const { return d_vars.size(); } |
28 |
|
|
29 |
658 |
bool Subs::contains(Node v) const |
30 |
|
{ |
31 |
658 |
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 |
29 |
void Subs::add(Node v) |
48 |
|
{ |
49 |
29 |
SkolemManager* sm = NodeManager::currentNM()->getSkolemManager(); |
50 |
|
// default, use a fresh skolem of the same type |
51 |
58 |
Node s = sm->mkDummySkolem("sk", v.getType()); |
52 |
29 |
add(v, s); |
53 |
29 |
} |
54 |
|
|
55 |
19 |
void Subs::add(const std::vector<Node>& vs) |
56 |
|
{ |
57 |
48 |
for (const Node& v : vs) |
58 |
|
{ |
59 |
29 |
add(v); |
60 |
|
} |
61 |
19 |
} |
62 |
|
|
63 |
203 |
void Subs::add(Node v, Node s) |
64 |
|
{ |
65 |
203 |
Assert(v.getType().isComparableTo(s.getType())); |
66 |
203 |
d_vars.push_back(v); |
67 |
203 |
d_subs.push_back(s); |
68 |
203 |
} |
69 |
|
|
70 |
|
void Subs::add(const std::vector<Node>& vs, const std::vector<Node>& ss) |
71 |
|
{ |
72 |
|
Assert(vs.size() == ss.size()); |
73 |
|
for (size_t i = 0, nvs = vs.size(); i < nvs; i++) |
74 |
|
{ |
75 |
|
add(vs[i], ss[i]); |
76 |
|
} |
77 |
|
} |
78 |
|
|
79 |
|
void Subs::addEquality(Node eq) |
80 |
|
{ |
81 |
|
Assert(eq.getKind() == kind::EQUAL); |
82 |
|
add(eq[0], eq[1]); |
83 |
|
} |
84 |
|
|
85 |
|
void Subs::append(Subs& s) |
86 |
|
{ |
87 |
|
// add the substitution list |
88 |
|
add(s.d_vars, s.d_subs); |
89 |
|
} |
90 |
|
|
91 |
57 |
Node Subs::apply(Node n, bool doRewrite) const |
92 |
|
{ |
93 |
57 |
if (d_vars.empty()) |
94 |
|
{ |
95 |
|
return n; |
96 |
|
} |
97 |
|
Node ns = |
98 |
114 |
n.substitute(d_vars.begin(), d_vars.end(), d_subs.begin(), d_subs.end()); |
99 |
57 |
if (doRewrite) |
100 |
|
{ |
101 |
|
ns = theory::Rewriter::rewrite(ns); |
102 |
|
} |
103 |
57 |
return ns; |
104 |
|
} |
105 |
19 |
Node Subs::rapply(Node n, bool doRewrite) const |
106 |
|
{ |
107 |
19 |
if (d_vars.empty()) |
108 |
|
{ |
109 |
|
return n; |
110 |
|
} |
111 |
|
Node ns = |
112 |
38 |
n.substitute(d_subs.begin(), d_subs.end(), d_vars.begin(), d_vars.end()); |
113 |
19 |
if (doRewrite) |
114 |
|
{ |
115 |
19 |
ns = theory::Rewriter::rewrite(ns); |
116 |
|
} |
117 |
19 |
return ns; |
118 |
|
} |
119 |
|
|
120 |
|
void Subs::applyToRange(Subs& s, bool doRewrite) const |
121 |
|
{ |
122 |
|
if (d_vars.empty()) |
123 |
|
{ |
124 |
|
return; |
125 |
|
} |
126 |
|
for (size_t i = 0, ns = s.d_subs.size(); i < ns; i++) |
127 |
|
{ |
128 |
|
s.d_subs[i] = apply(s.d_subs[i], doRewrite); |
129 |
|
} |
130 |
|
} |
131 |
|
|
132 |
|
void Subs::rapplyToRange(Subs& s, bool doRewrite) const |
133 |
|
{ |
134 |
|
if (d_vars.empty()) |
135 |
|
{ |
136 |
|
return; |
137 |
|
} |
138 |
|
for (size_t i = 0, ns = s.d_subs.size(); i < ns; i++) |
139 |
|
{ |
140 |
|
s.d_subs[i] = rapply(s.d_subs[i], doRewrite); |
141 |
|
} |
142 |
|
} |
143 |
|
|
144 |
|
Node Subs::getEquality(size_t i) const |
145 |
|
{ |
146 |
|
Assert(i < d_vars.size()); |
147 |
|
return d_vars[i].eqNode(d_subs[i]); |
148 |
|
} |
149 |
|
|
150 |
|
std::map<Node, Node> Subs::toMap() const |
151 |
|
{ |
152 |
|
std::map<Node, Node> ret; |
153 |
|
for (size_t i = 0, nvs = d_vars.size(); i < nvs; i++) |
154 |
|
{ |
155 |
|
ret[d_vars[i]] = d_subs[i]; |
156 |
|
} |
157 |
|
return ret; |
158 |
|
} |
159 |
|
|
160 |
|
std::string Subs::toString() const |
161 |
|
{ |
162 |
|
std::stringstream ss; |
163 |
|
ss << "["; |
164 |
|
for (size_t i = 0, nvs = d_vars.size(); i < nvs; i++) |
165 |
|
{ |
166 |
|
if (i > 0) |
167 |
|
{ |
168 |
|
ss << " "; |
169 |
|
} |
170 |
|
ss << d_vars[i] << " -> " << d_subs[i]; |
171 |
|
} |
172 |
|
ss << "]"; |
173 |
|
return ss.str(); |
174 |
|
} |
175 |
|
|
176 |
|
std::ostream& operator<<(std::ostream& out, const Subs& s) |
177 |
|
{ |
178 |
|
out << s.toString(); |
179 |
|
return out; |
180 |
|
} |
181 |
|
|
182 |
28194 |
} // namespace cvc5 |