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