Branch data Line data Source code
1 : : /******************************************************************************
2 : : * Top contributors (to current version):
3 : : * Andrew Reynolds, Haniel Barbosa, Aina Niemetz
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 : : * Implementation of proof node algorithm utilities.
14 : : */
15 : :
16 : : #include "proof/proof_node_algorithm.h"
17 : :
18 : : #include "proof/proof_node.h"
19 : : #include "proof/proof_rule_checker.h"
20 : : #include "theory/builtin/generic_op.h"
21 : :
22 : : namespace cvc5::internal {
23 : : namespace expr {
24 : :
25 : 550278 : void getFreeAssumptions(ProofNode* pn, std::vector<Node>& assump)
26 : : {
27 : 1100560 : std::map<Node, std::vector<std::shared_ptr<ProofNode>>> amap;
28 : : std::shared_ptr<ProofNode> spn = std::make_shared<ProofNode>(
29 : 1100560 : pn->getRule(), pn->getChildren(), pn->getArguments());
30 : 550278 : getFreeAssumptionsMap(spn, amap);
31 : 797062 : for (const std::pair<const Node, std::vector<std::shared_ptr<ProofNode>>>& p :
32 [ + + ]: 2144400 : amap)
33 : : {
34 : 797062 : assump.push_back(p.first);
35 : : }
36 : 550278 : }
37 : :
38 : 3092040 : void getFreeAssumptionsMap(
39 : : std::shared_ptr<ProofNode> pn,
40 : : std::map<Node, std::vector<std::shared_ptr<ProofNode>>>& amap)
41 : : {
42 : : // proof should not be cyclic
43 : 6184070 : std::unordered_set<ProofNode*> visited;
44 : 3092040 : std::unordered_set<ProofNode*>::iterator it;
45 : 6184070 : std::vector<std::shared_ptr<ProofNode>> visit;
46 : 3092040 : std::shared_ptr<ProofNode> cur;
47 : 3092040 : visit.push_back(pn);
48 : 220281000 : do
49 : : {
50 : 223373000 : cur = visit.back();
51 : 223373000 : visit.pop_back();
52 : 223373000 : it = visited.find(cur.get());
53 : 223373000 : const std::vector<Node>& cargs = cur->getArguments();
54 [ + + ]: 223373000 : if (it == visited.end())
55 : : {
56 : 87350000 : visited.insert(cur.get());
57 : 87350000 : ProofRule id = cur->getRule();
58 [ + + ]: 87350000 : if (id == ProofRule::ASSUME)
59 : : {
60 [ - + ][ - + ]: 22738400 : Assert(cargs.size() == 1);
[ - - ]
61 : 45476800 : Node f = cargs[0];
62 : 22738400 : amap[f].push_back(cur);
63 : : }
64 : : else
65 : : {
66 : 64611600 : const std::vector<std::shared_ptr<ProofNode>>& cs = cur->getChildren();
67 [ + + ]: 64611600 : if (id == ProofRule::SCOPE)
68 : : {
69 : : // make a recursive call, which is bound in depth by the number of
70 : : // nested SCOPE (never expected to be more than 1 or 2).
71 : 2583380 : std::map<Node, std::vector<std::shared_ptr<ProofNode>>> amapTmp;
72 : 1291690 : expr::getFreeAssumptionsMap(cs[0], amapTmp);
73 : 7704510 : for (std::pair<const Node, std::vector<std::shared_ptr<ProofNode>>>&
74 [ + + ]: 16700700 : a : amapTmp)
75 : : {
76 [ + + ]: 7704510 : if (std::find(cargs.begin(), cargs.end(), a.first) == cargs.end())
77 : : {
78 : 563979 : std::vector<std::shared_ptr<ProofNode>>& pfs = amap[a.first];
79 : 563979 : pfs.insert(pfs.end(), a.second.begin(), a.second.end());
80 : : }
81 : : }
82 : 1291690 : continue;
83 : : }
84 : : // traverse on children
85 : 63319900 : visit.insert(visit.end(), cs.begin(), cs.end());
86 : : }
87 : : }
88 [ + + ]: 223373000 : } while (!visit.empty());
89 : 3092040 : }
90 : :
91 : 0 : void getSubproofRule(std::shared_ptr<ProofNode> pn,
92 : : ProofRule r,
93 : : std::vector<std::shared_ptr<ProofNode>>& pfs)
94 : : {
95 : 0 : std::unordered_set<ProofRule> rs{r};
96 : 0 : getSubproofRules(pn, rs, pfs);
97 : 0 : }
98 : :
99 : 12 : void getSubproofRules(std::shared_ptr<ProofNode> pn,
100 : : std::unordered_set<ProofRule> rs,
101 : : std::vector<std::shared_ptr<ProofNode>>& pfs)
102 : : {
103 : : // proof should not be cyclic
104 : 24 : std::unordered_set<ProofNode*> visited;
105 : 12 : std::unordered_set<ProofNode*>::iterator it;
106 : 24 : std::vector<std::shared_ptr<ProofNode>> visit;
107 : 12 : std::shared_ptr<ProofNode> cur;
108 : 12 : visit.push_back(pn);
109 : 114 : do
110 : : {
111 : 126 : cur = visit.back();
112 : 126 : visit.pop_back();
113 : 126 : it = visited.find(cur.get());
114 [ + - ]: 126 : if (it == visited.end())
115 : : {
116 : 126 : visited.insert(cur.get());
117 [ + + ]: 126 : if (rs.find(cur->getRule()) != rs.end())
118 : : {
119 : 50 : pfs.push_back(cur);
120 : : }
121 : : else
122 : : {
123 : 76 : const std::vector<std::shared_ptr<ProofNode>>& cs = cur->getChildren();
124 : : // traverse on children
125 : 76 : visit.insert(visit.end(), cs.begin(), cs.end());
126 : : }
127 : : }
128 [ + + ]: 126 : } while (!visit.empty());
129 : 12 : }
130 : :
131 : 9973420 : bool containsAssumption(const ProofNode* pn,
132 : : std::unordered_map<const ProofNode*, bool>& caMap,
133 : : const std::unordered_set<Node>& allowed)
134 : : {
135 : 19946800 : std::unordered_map<const ProofNode*, bool> visited;
136 : 9973420 : std::unordered_map<const ProofNode*, bool>::iterator it;
137 : 9973420 : std::vector<const ProofNode*> visit;
138 : 9973420 : visit.push_back(pn);
139 : 9973420 : bool foundAssumption = false;
140 : : const ProofNode* cur;
141 [ + + ]: 48657300 : while (!visit.empty())
142 : : {
143 : 38683900 : cur = visit.back();
144 : 38683900 : visit.pop_back();
145 : : // have we already computed?
146 : 38683900 : it = caMap.find(cur);
147 [ + + ]: 38683900 : if (it != caMap.end())
148 : : {
149 : : // if cached, we set found assumption to true if applicable and continue
150 [ + + ]: 19243600 : if (it->second)
151 : : {
152 : 7040140 : foundAssumption = true;
153 : : }
154 : 19243600 : continue;
155 : : }
156 : 19440300 : it = visited.find(cur);
157 [ + + ]: 19440300 : if (it == visited.end())
158 : : {
159 : 10336400 : ProofRule r = cur->getRule();
160 [ + + ]: 10336400 : if (r == ProofRule::ASSUME)
161 : : {
162 : 1232300 : bool ret = allowed.find(cur->getArguments()[0]) == allowed.end();
163 : 1232300 : visited[cur] = ret;
164 : 1232300 : caMap[cur] = ret;
165 : 1232300 : foundAssumption = ret;
166 : : }
167 [ + + ]: 9104120 : else if (!foundAssumption)
168 : : {
169 : : // if we haven't found an assumption yet, recurse. Otherwise, we will
170 : : // not bother computing whether this subproof contains an assumption
171 : : // since we know its parent already contains one by another child.
172 : 9103860 : visited[cur] = false;
173 : 9103860 : visit.push_back(cur);
174 : : const std::vector<std::shared_ptr<ProofNode>>& children =
175 : 9103860 : cur->getChildren();
176 [ + + ]: 28710400 : for (const std::shared_ptr<ProofNode>& cp : children)
177 : : {
178 : 19606600 : visit.push_back(cp.get());
179 : : }
180 : : }
181 : : }
182 [ + - ]: 9103860 : else if (!it->second)
183 : : {
184 : 9103860 : visited[cur] = true;
185 : : // we contain an assumption if we've found an assumption in a child
186 : 9103860 : caMap[cur] = foundAssumption;
187 : : }
188 : : }
189 : 19946800 : return caMap[cur];
190 : : }
191 : 0 : bool containsAssumption(const ProofNode* pn,
192 : : std::unordered_map<const ProofNode*, bool>& caMap)
193 : : {
194 : 0 : std::unordered_set<Node> allowed;
195 : 0 : return containsAssumption(pn, caMap, allowed);
196 : : }
197 : :
198 : 0 : bool containsAssumption(const ProofNode* pn)
199 : : {
200 : 0 : std::unordered_map<const ProofNode*, bool> caMap;
201 : 0 : std::unordered_set<Node> allowed;
202 : 0 : return containsAssumption(pn, caMap, allowed);
203 : : }
204 : :
205 : 0 : bool containsSubproof(ProofNode* pn, ProofNode* pnc)
206 : : {
207 : 0 : std::unordered_set<const ProofNode*> visited;
208 : 0 : return containsSubproof(pn, pnc, visited);
209 : : }
210 : :
211 : 10786 : bool containsSubproof(ProofNode* pn,
212 : : ProofNode* pnc,
213 : : std::unordered_set<const ProofNode*>& visited)
214 : : {
215 : 10786 : std::unordered_map<const ProofNode*, bool>::iterator it;
216 : 21572 : std::vector<const ProofNode*> visit;
217 : 10786 : visit.push_back(pn);
218 : : const ProofNode* cur;
219 [ + + ]: 281231 : while (!visit.empty())
220 : : {
221 : 270445 : cur = visit.back();
222 : 270445 : visit.pop_back();
223 [ + + ]: 270445 : if (visited.find(cur) == visited.end())
224 : : {
225 : 238364 : visited.insert(cur);
226 [ - + ]: 238364 : if (cur == pnc)
227 : : {
228 : 0 : return true;
229 : : }
230 : : const std::vector<std::shared_ptr<ProofNode>>& children =
231 : 238364 : cur->getChildren();
232 [ + + ]: 498023 : for (const std::shared_ptr<ProofNode>& cp : children)
233 : : {
234 : 259659 : visit.push_back(cp.get());
235 : : }
236 : : }
237 : : }
238 : 10786 : return false;
239 : : }
240 : :
241 : 2932550 : ProofRule getCongRule(const Node& n, std::vector<Node>& args)
242 : : {
243 : 2932550 : Kind k = n.getKind();
244 : 2932550 : ProofRule r = ProofRule::CONG;
245 [ + + ][ + + ]: 2932550 : switch (k)
246 : : {
247 : 614071 : case Kind::APPLY_UF:
248 : : case Kind::DISTINCT:
249 : : case Kind::FLOATINGPOINT_LT:
250 : : case Kind::FLOATINGPOINT_LEQ:
251 : : case Kind::FLOATINGPOINT_GT:
252 : : case Kind::FLOATINGPOINT_GEQ:
253 : : case Kind::NULLABLE_LIFT:
254 : : case Kind::APPLY_INDEXED_SYMBOLIC:
255 : : // takes arbitrary but we use CONG
256 : 614071 : break;
257 : 1466 : case Kind::HO_APPLY:
258 : : // Use HO_CONG, since HO_APPLY is encoded as native function application.
259 : : // This requires no arguments so we return.
260 : 1466 : r = ProofRule::HO_CONG;
261 : 1466 : break;
262 : 11070 : case Kind::APPLY_CONSTRUCTOR:
263 : : // tuples are n-ary, others are fixed
264 [ + + ]: 11070 : r = n.getType().isTuple() ? ProofRule::NARY_CONG : ProofRule::CONG;
265 : 11070 : break;
266 : 2305940 : default:
267 [ + + ]: 2305940 : if (NodeManager::isNAryKind(k))
268 : : {
269 : : // n-ary operators that are not handled as exceptions above use
270 : : // NARY_CONG
271 : 973368 : r = ProofRule::NARY_CONG;
272 : : }
273 : 2305940 : break;
274 : : }
275 [ + + ]: 2932550 : if (r != ProofRule::HO_CONG)
276 : : {
277 : 2931090 : args.push_back(n);
278 : : }
279 : 2932550 : return r;
280 : : }
281 : :
282 : : } // namespace expr
283 : : } // namespace cvc5::internal
|
