Branch data Line data Source code
1 : : /******************************************************************************
2 : : * This file is part of the cvc5 project.
3 : : *
4 : : * Copyright (c) 2009-2026 by the authors listed in the file AUTHORS
5 : : * in the top-level source directory and their institutional affiliations.
6 : : * All rights reserved. See the file COPYING in the top-level source
7 : : * directory for licensing information.
8 : : * ****************************************************************************
9 : : *
10 : : * The implementation of the module for Alethe let binding.
11 : : */
12 : :
13 : : #include "proof/alethe/alethe_let_binding.h"
14 : :
15 : : #include <sstream>
16 : :
17 : : namespace cvc5::internal {
18 : :
19 : : namespace proof {
20 : :
21 : 480 : AletheLetBinding::AletheLetBinding(uint32_t thresh) : LetBinding("let", thresh)
22 : : {
23 : 480 : }
24 : :
25 : 2397918 : Node AletheLetBinding::convert(NodeManager* nm,
26 : : Node n,
27 : : const std::string& prefix)
28 : : {
29 [ + + ]: 2397918 : if (d_letMap.empty())
30 : : {
31 : 1130 : return n;
32 : : }
33 : : // terms with a child that is being declared
34 : 2396788 : std::unordered_set<TNode> hasDeclaredChild;
35 : : // For a term being declared, its position relative to the list of children
36 : : // of the parent of this term, its parent, and its declaration value. These
37 : : // are necessary to properly declare letified terms occurring for the first
38 : : // time once conversions start
39 : 2396788 : std::unordered_map<TNode, size_t> declaredPosition;
40 : 2396788 : std::unordered_map<TNode, TNode> parentOf;
41 : 2396788 : std::unordered_map<TNode, Node> declaredValue;
42 : : // visiting utils
43 : 2396788 : std::unordered_map<TNode, Node> visited;
44 : 2396788 : std::unordered_map<TNode, Node>::iterator it;
45 : 2396788 : std::vector<TNode> visit;
46 : 2396788 : TNode cur;
47 : : // start with input
48 : 2396788 : visit.push_back(n);
49 : : do
50 : : {
51 : 15861103 : cur = visit.back();
52 : 15861103 : visit.pop_back();
53 : 15861103 : it = visited.find(cur);
54 [ + + ]: 15861103 : if (it == visited.end())
55 : : {
56 : 9635077 : uint32_t id = getId(cur);
57 : : // do not letify partially applied terms, which may have been generated
58 : : // during RARE elaboration.
59 [ + + ][ + + ]: 9635077 : if (cur.getKind() == Kind::HO_APPLY && cur.getType().isFunction())
[ + + ][ + + ]
[ - - ]
60 : : {
61 : 8 : visited[cur] = cur;
62 : 4194411 : continue;
63 : : }
64 : : // do not letify id 0
65 [ + + ]: 9635069 : if (id > 0)
66 : : {
67 [ + - ]: 9094228 : Trace("alethe-printer-share")
68 : 4547114 : << "Node " << cur << " has id " << id << "\n";
69 : : // if cur has previously been declared, just use the let variable.
70 [ + + ]: 4547114 : if (d_declared.find(cur) != d_declared.end())
71 : : {
72 : : // create the let variable for cur
73 : 4164765 : std::stringstream ss;
74 : 4164765 : ss << prefix << id;
75 : 4164765 : visited[cur] = NodeManager::mkBoundVar(ss.str(), cur.getType());
76 [ + - ]: 8329530 : Trace("alethe-printer-share")
77 : 4164765 : << "\tdeclared, use var " << visited[cur] << "\n";
78 : 4164765 : continue;
79 : 4164765 : }
80 : : // If the input of this method is letified and it has not yet been
81 : : // declared, we will need to declare its post-visit result. So we do
82 : : // nothing at this point other than book-keep. The information is
83 : : // necessary to guarantee that this occurrence, its first in the overall
84 : : // term, is ultimately used as a declaration rather than as just the
85 : : // letified variable. For this we find the parent of this first
86 : : // occurrence of cur and the position in its children in which cur
87 : : // occurs. The declaration will be created when cur is post-visited and
88 : : // used when the parent of this occurrence of cur is post-visited.
89 [ + + ]: 382349 : if (cur != n)
90 : : {
91 : : // The parent of cur will have been set when it was visited
92 [ - + ][ - + ]: 380879 : Assert(parentOf.find(cur) != parentOf.end());
[ - - ]
93 : 380879 : Node parent = parentOf[cur];
94 : 380879 : auto itPos = std::find(parent.begin(), parent.end(), cur);
95 [ - + ][ - + ]: 380879 : Assert(itPos != parent.end());
[ - - ]
96 : 380879 : declaredPosition[cur] = itPos - parent.begin();
97 [ + - ]: 761758 : Trace("alethe-printer-share")
98 : 0 : << "\tset for its parent " << parent << " mark position "
99 : 380879 : << itPos - parent.begin() << "\n";
100 : 380879 : }
101 : : // Mark that future occurrences are just the variable
102 : 382349 : d_declared.insert(cur);
103 : : }
104 [ + + ]: 5470304 : if (cur.isClosure())
105 : : {
106 : : // We do not convert beneath quantifiers, so we need to finish the
107 : : // traversal here. However if id > 0, then we need to declare cur's
108 : : // variable. Since cur is not post-visited the declaration is of cur
109 : : // itself.
110 [ + - ]: 29638 : if (id == 0)
111 : : {
112 : 29638 : visited[cur] = cur;
113 : 29638 : continue;
114 : : }
115 : 0 : std::stringstream ss;
116 : 0 : ss << "(! ";
117 : 0 : options::ioutils::applyOutputLanguage(ss, Language::LANG_SMTLIB_V2_6);
118 : : // We print terms non-flattened and with lambda applications in
119 : : // non-curried manner
120 : 0 : options::ioutils::applyDagThresh(ss, 0);
121 : : // Guarantee we print reals as expected
122 : 0 : options::ioutils::applyPrintArithLitToken(ss, true);
123 : 0 : options::ioutils::applyFlattenHOChains(ss, true);
124 : 0 : cur.toStream(ss);
125 : 0 : ss << " :named " << prefix << id << ")";
126 : 0 : Node letVar = NodeManager::mkRawSymbol(ss.str(), cur.getType());
127 : 0 : visited[cur] = letVar;
128 : 0 : declaredValue[cur] = letVar;
129 : 0 : continue;
130 : 0 : }
131 : 5440666 : visited[cur] = Node::null();
132 : 5440666 : visit.push_back(cur);
133 : : // We now check if any of the children of cur is being declared, in which
134 : : // case we associate cur as the parent of declared children, as will as
135 : : // that cur has declared children.
136 : : //
137 : : // We also use this loop to add the children to be visited. Note we add
138 : : // them in reverse order, since we must do post-order traversal (last
139 : : // added to the list are first visited, thus this entails left-to-right
140 : : // traversal of children)
141 [ + + ]: 13464315 : for (size_t i = 0, size = cur.getNumChildren(); i < size; ++i)
142 : : {
143 : 8023649 : visit.push_back(cur[size - i - 1]);
144 : 8023649 : id = getId(cur[i]);
145 : 8023649 : if (id > 0 && d_declared.find(cur[i]) == d_declared.end())
146 : : {
147 : 406052 : parentOf[cur[i]] = cur;
148 : 406052 : hasDeclaredChild.insert(cur);
149 : : }
150 : : }
151 : : }
152 [ + + ]: 6226026 : else if (it->second.isNull())
153 : : {
154 : 5440666 : Node ret = cur;
155 : 5440666 : bool childChanged = false;
156 : : uint32_t id;
157 : 5440666 : std::vector<Node> children;
158 [ + + ]: 5440666 : if (cur.getMetaKind() == kind::metakind::PARAMETERIZED)
159 : : {
160 : 11708 : children.push_back(cur.getOperator());
161 : : }
162 : : // if cur is a parent has declared child, then for each position we must
163 : : // check if that position is of a child being declared and whose declared
164 : : // position is that one. In this case we use not the value in visited but
165 : : // rather the value in declaredValue
166 : 5440666 : bool checkDeclaredChild = hasDeclaredChild.count(cur);
167 [ + + ]: 5440666 : if (checkDeclaredChild)
168 : : {
169 [ + - ]: 656406 : Trace("alethe-printer-share")
170 : 328203 : << "Post-visiting node " << cur << " with declared child\n";
171 : : }
172 [ + + ]: 13464315 : for (size_t i = 0, size = cur.getNumChildren(); i < size; ++i)
173 : : {
174 : 8023649 : bool useVisited = true;
175 : : // cur has a declared child and if cur[i] is declared and in this
176 : : // position, then we use its declared value rather than visited[cur[i]].
177 [ + + ]: 8023649 : if (checkDeclaredChild)
178 : : {
179 : 861386 : const auto& itDeclPos = declaredPosition.find(cur[i]);
180 : 861386 : useVisited =
181 [ + + ][ + + ]: 861386 : itDeclPos == declaredPosition.end() || itDeclPos->second != i;
182 : : }
183 : 16047298 : Assert(useVisited || getId(cur[i]) > 0)
184 : 8023649 : << "With input " << n << " we got child " << cur[i]
185 : 0 : << " to use declared value but its id is 0\n";
186 : 8023649 : it = useVisited ? visited.find(cur[i]) : declaredValue.find(cur[i]);
187 [ - + ][ - - ]: 8023649 : Assert(it != visited.end())
188 : 8023649 : << "With input " << n << " did not find for term " << cur
189 [ - + ][ - + ]: 8023649 : << " its child " << cur[i] << " in map with useVisited "
[ - - ]
190 : 0 : << useVisited << "\n";
191 [ - + ][ - + ]: 8023649 : Assert(!it->second.isNull());
[ - - ]
192 [ + + ][ + + ]: 8023649 : childChanged = childChanged || cur[i] != it->second;
[ + + ][ - - ]
193 : 8023649 : children.push_back(it->second);
194 : : }
195 [ + + ]: 5440666 : if (childChanged)
196 : : {
197 : 2691730 : ret = nm->mkNode(cur.getKind(), children);
198 : : }
199 : 5440666 : id = getId(cur);
200 : : // if cur has id bigger than 0, then we are declaring its conversion to
201 : : // ret. We save the declaration in declaredValue and set the value in
202 : : // visited to be the let variable, since next occurrences should use that.
203 : : // The use of the declared value will be controlled by the parent. If cur
204 : : // is n, since there is no parent, then we use directly the declared
205 : : // value.
206 [ + + ]: 5440666 : if (id > 0)
207 : : {
208 : 382349 : std::stringstream ss, ssVar;
209 : 382349 : ss << "(! ";
210 : 382349 : options::ioutils::applyOutputLanguage(ss, Language::LANG_SMTLIB_V2_6);
211 : : // We print terms non-flattened and with lambda applications in
212 : : // non-curried manner
213 : 382349 : options::ioutils::applyDagThresh(ss, 0);
214 : : // Guarantee we print reals as expected
215 : 382349 : options::ioutils::applyPrintArithLitToken(ss, true);
216 : 382349 : options::ioutils::applyFlattenHOChains(ss, true);
217 : 382349 : ret.toStream(ss);
218 : 382349 : ssVar << prefix << id;
219 : 382349 : ss << " :named " << ssVar.str() << ")";
220 : 764698 : Node declaration = NodeManager::mkRawSymbol(ss.str(), ret.getType());
221 : 382349 : declaredValue[cur] = declaration;
222 : 382349 : visited[cur] =
223 [ + + ]: 1145577 : cur == n ? declaration
224 : 1145577 : : NodeManager::mkBoundVar(ssVar.str(), cur.getType());
225 : 382349 : continue;
226 : 382349 : }
227 : 5058317 : visited[cur] = ret;
228 [ + + ][ + + ]: 5823015 : }
229 [ + + ]: 15861103 : } while (!visit.empty());
230 [ - + ][ - + ]: 2396788 : Assert(visited.find(n) != visited.end());
[ - - ]
231 [ - + ][ - + ]: 2396788 : Assert(!visited.find(n)->second.isNull());
[ - - ]
232 : 2396788 : return visited[n];
233 : 2396788 : }
234 : :
235 : : } // namespace proof
236 : : } // namespace cvc5::internal
|
