Branch data Line data Source code
1 : : /******************************************************************************
2 : : * Top contributors (to current version):
3 : : * Andrew Reynolds, Gereon Kremer, Aina Niemetz
4 : : *
5 : : * This file is part of the cvc5 project.
6 : : *
7 : : * Copyright (c) 2009-2024 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 : :
22 : : namespace cvc5::internal {
23 : :
24 : 146500 : bool Subs::empty() const { return d_vars.empty(); }
25 : :
26 : 133677 : size_t Subs::size() const { return d_vars.size(); }
27 : :
28 : 33060 : bool Subs::contains(Node v) const
29 : : {
30 : 33060 : return std::find(d_vars.begin(), d_vars.end(), v) != d_vars.end();
31 : : }
32 : :
33 : 0 : Node Subs::getSubs(Node v) const
34 : : {
35 : : std::vector<Node>::const_iterator it =
36 : 0 : std::find(d_vars.begin(), d_vars.end(), v);
37 [ - - ]: 0 : if (it == d_vars.end())
38 : : {
39 : 0 : return Node::null();
40 : : }
41 : 0 : size_t i = std::distance(d_vars.begin(), it);
42 : 0 : Assert(i < d_subs.size());
43 : 0 : return d_subs[i];
44 : : }
45 : :
46 : 6370460 : std::optional<Node> Subs::find(TNode v) const
47 : : {
48 : 6370460 : auto it = std::find(d_vars.begin(), d_vars.end(), v);
49 [ + + ]: 6370460 : if (it == d_vars.end())
50 : : {
51 : 4689770 : return {};
52 : : }
53 : 1680690 : return d_subs[std::distance(d_vars.begin(), it)];
54 : : }
55 : :
56 : 423 : void Subs::add(Node v)
57 : : {
58 : 423 : SkolemManager* sm = NodeManager::currentNM()->getSkolemManager();
59 : : // default, use a fresh skolem of the same type
60 : 1269 : Node s = sm->mkDummySkolem("sk", v.getType());
61 : 423 : add(v, s);
62 : 423 : }
63 : :
64 : 30 : void Subs::add(const std::vector<Node>& vs)
65 : : {
66 [ + + ]: 67 : for (const Node& v : vs)
67 : : {
68 : 37 : add(v);
69 : : }
70 : 30 : }
71 : :
72 : 2477980 : void Subs::add(const Node& v, const Node& s)
73 : : {
74 : 2477980 : Assert(s.isNull() || v.getType().isComparableTo(s.getType()));
75 : 2477980 : d_vars.push_back(v);
76 : 2477980 : d_subs.push_back(s);
77 : 2477980 : }
78 : :
79 : 1753 : void Subs::add(const std::vector<Node>& vs, const std::vector<Node>& ss)
80 : : {
81 [ - + ][ - + ]: 1753 : Assert(vs.size() == ss.size());
[ - - ]
82 [ + + ]: 3840 : for (size_t i = 0, nvs = vs.size(); i < nvs; i++)
83 : : {
84 : 2087 : add(vs[i], ss[i]);
85 : : }
86 : 1753 : }
87 : :
88 : 0 : void Subs::addEquality(Node eq)
89 : : {
90 : 0 : Assert(eq.getKind() == Kind::EQUAL);
91 : 0 : add(eq[0], eq[1]);
92 : 0 : }
93 : :
94 : 0 : void Subs::append(Subs& s)
95 : : {
96 : : // add the substitution list
97 : 0 : add(s.d_vars, s.d_subs);
98 : 0 : }
99 : :
100 : 101068 : Node Subs::apply(const Node& n) const
101 : : {
102 [ + + ]: 101068 : if (d_vars.empty())
103 : : {
104 : 7884 : return n;
105 : : }
106 : : Node ns =
107 : 186368 : n.substitute(d_vars.begin(), d_vars.end(), d_subs.begin(), d_subs.end());
108 : 93184 : return ns;
109 : : }
110 : 30 : Node Subs::rapply(Node n) const
111 : : {
112 [ - + ]: 30 : if (d_vars.empty())
113 : : {
114 : 0 : return n;
115 : : }
116 : : Node ns =
117 : 60 : n.substitute(d_subs.begin(), d_subs.end(), d_vars.begin(), d_vars.end());
118 : 30 : return ns;
119 : : }
120 : :
121 : 0 : void Subs::applyToRange(Subs& s) const
122 : : {
123 [ - - ]: 0 : if (d_vars.empty())
124 : : {
125 : 0 : return;
126 : : }
127 [ - - ]: 0 : for (size_t i = 0, ns = s.d_subs.size(); i < ns; i++)
128 : : {
129 : 0 : s.d_subs[i] = apply(s.d_subs[i]);
130 : : }
131 : : }
132 : :
133 : 0 : void Subs::rapplyToRange(Subs& s) const
134 : : {
135 [ - - ]: 0 : if (d_vars.empty())
136 : : {
137 : 0 : return;
138 : : }
139 [ - - ]: 0 : for (size_t i = 0, ns = s.d_subs.size(); i < ns; i++)
140 : : {
141 : 0 : s.d_subs[i] = rapply(s.d_subs[i]);
142 : : }
143 : : }
144 : :
145 : 0 : Node Subs::getEquality(size_t i) const
146 : : {
147 : 0 : Assert(i < d_vars.size());
148 : 0 : return d_vars[i].eqNode(d_subs[i]);
149 : : }
150 : :
151 : 0 : std::map<Node, Node> Subs::toMap() const
152 : : {
153 : 0 : std::map<Node, Node> ret;
154 [ - - ]: 0 : for (size_t i = 0, nvs = d_vars.size(); i < nvs; i++)
155 : : {
156 : 0 : ret[d_vars[i]] = d_subs[i];
157 : : }
158 : 0 : return ret;
159 : : }
160 : :
161 : 0 : std::string Subs::toString() const
162 : : {
163 : 0 : std::stringstream ss;
164 : 0 : ss << "[";
165 [ - - ]: 0 : for (size_t i = 0, nvs = d_vars.size(); i < nvs; i++)
166 : : {
167 [ - - ]: 0 : if (i > 0)
168 : : {
169 : 0 : ss << " ";
170 : : }
171 : 0 : ss << d_vars[i] << " -> " << d_subs[i];
172 : : }
173 : 0 : ss << "]";
174 : 0 : return ss.str();
175 : : }
176 : :
177 : 132630 : void Subs::clear()
178 : : {
179 : 132630 : d_vars.clear();
180 : 132630 : d_subs.clear();
181 : 132630 : }
182 : :
183 : 0 : std::ostream& operator<<(std::ostream& out, const Subs& s)
184 : : {
185 : 0 : out << s.toString();
186 : 0 : return out;
187 : : }
188 : :
189 : : } // namespace cvc5::internal
|
